(NOTE-LIB "extras" T)
Loading ./numbers/extras.lib
Finished loading ./numbers/extras.lib
Loading ./numbers/extras.o
Finished loading ./numbers/extras.o
(#./numbers/extras.lib #./numbers/extras)
(PROVE-LEMMA IREM-IGCD-ARG1
(REWRITE)
(EQUAL (EQUAL (IREM (IGCD A B) C) 0)
(AND (EQUAL (IREM A C) 0)
(EQUAL (IREM B C) 0)))
((ENABLE IREM-IS-MY-IREM IABS IGCD MY-IREM FIX-INT INTEGERP INEG)))
This formula can be simplified, using the abbreviations IREM-IS-MY-IREM and
IGCD, to:
(EQUAL (EQUAL (MY-IREM (GCD (IABS A) (IABS B)) C)
0)
(AND (EQUAL (MY-IREM A C) 0)
(EQUAL (MY-IREM B C) 0))),
which simplifies, applying EQUAL-GCD-0 and FIX-INT-REMOVER, and opening up the
definitions of IABS, INTEGERP, MY-IREM, FIX-INT, and AND, to the following 192
new formulas:
Case 192.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, using linear arithmetic, rewriting with the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding the definitions of NEGATIVEP,
NUMBERP, EQUAL, and INEG, to:
T.
Case 191.
(IMPLIES (AND (NOT (NEGATIVEP A))
(EQUAL A 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)),
which again simplifies, clearly, to:
T.
Case 190.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, clearly, to:
T.
Case 189.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, applying the lemma REMAINDER-GCD-ARG1, and expanding
the functions EQUAL and INEG, to:
T.
Case 188.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL,
NUMBERP, and INEG, to:
T.
Case 187.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, clearly, to:
T.
Case 186.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, clearly, to:
T.
Case 185.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
However this again simplifies, rewriting with REMAINDER-GCD-ARG1, and
unfolding INEG and EQUAL, to:
T.
Case 184.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NOT (NUMBERP A))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL, NUMBERP, and INEG, to:
T.
Case 183.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, obviously, to:
T.
Case 182.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NEGATIVEP C)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, trivially, to:
T.
Case 181.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NOT (NUMBERP A))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, trivially, to:
T.
Case 180.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, trivially, to:
T.
Case 179.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0)
T)).
This again simplifies, clearly, to:
T.
Case 178.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding NEGATIVEP, NUMBERP, EQUAL,
and INEG, to:
T.
Case 177.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
This again simplifies, obviously, to:
T.
Case 176.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and opening up
the functions EQUAL and INEG, to:
T.
Case 175.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL, NUMBERP, and INEG, to:
T.
Case 174.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL A 0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
This again simplifies, trivially, to:
T.
Case 173.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and expanding
the definition of INEG, to:
T.
Case 172.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
This again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG,
to:
T.
Case 171.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL A 0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
This again simplifies, obviously, to:
T.
Case 170.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B)
(NEGATIVE-GUTS C)))
0))).
This again simplifies, obviously, to:
T.
Case 169.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)).
This again simplifies, trivially, to:
T.
Case 168.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0)
(NOT (NUMBERP A)))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)).
This again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to:
T.
Case 167.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)),
which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and
REMAINDER-GCD-ARG1, to:
T.
Case 166.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD 0 B)
(NEGATIVE-GUTS C))
0))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)).
This again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and opening up the functions EQUAL and
NUMBERP, to:
T.
Case 165.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0)
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)),
which again simplifies, rewriting with REMAINDER-GCD-ARG1, and opening up
the definition of EQUAL, to:
T.
Case 164.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0))
(EQUAL (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0)
T)).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions NEGATIVEP,
NUMBERP, and EQUAL, to:
T.
Case 163.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0))
(EQUAL A 0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))).
This again simplifies, clearly, to:
T.
Case 162.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))).
However this again simplifies, using linear arithmetic, applying
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL and
NUMBERP, to:
T.
Case 161.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))).
But this again simplifies, rewriting with COMMUTATIVITY-OF-GCD and
REMAINDER-GCD-ARG1, and expanding the functions EQUAL and INEG, to:
T.
Case 160.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD 0 B)
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))).
But this again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and opening up the definitions of EQUAL
and NUMBERP, to:
T.
Case 159.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))),
which again simplifies, rewriting with COMMON-DIVISOR-DIVIDES-GCD, and
expanding EQUAL, to:
T.
Case 158.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (REMAINDER B (NEGATIVE-GUTS C))
0))).
But this again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding NEGATIVEP, NUMBERP, and
EQUAL, to:
T.
Case 157.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)),
which again simplifies, using linear arithmetic, applying REMAINDER-NOOP,
GCD-REMAINDER, and REMAINDER-ZERO, and expanding NEGATIVEP, NUMBERP, EQUAL,
and ZEROP, to:
T.
Case 156.
(IMPLIES (AND (NOT (NEGATIVEP A))
(EQUAL A 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, obviously, to:
T.
Case 155.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, obviously, to:
T.
Case 154.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0)
(EQUAL (REMAINDER A 0) 0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
But this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0,
and expanding the function ZEROP, to:
T.
Case 153.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
0)
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding EQUAL,
NUMBERP, and ZEROP, to:
T.
Case 152.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, clearly, to:
T.
Case 151.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, trivially, to:
T.
Case 150.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
But this again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and
expanding ZEROP, to:
T.
Case 149.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(NOT (NUMBERP A))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, using linear arithmetic, applying REMAINDER-NOOP,
GCD-REMAINDER, and REMAINDER-ZERO, and expanding the definitions of EQUAL,
NUMBERP, and ZEROP, to:
T.
Case 148.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, clearly, to:
T.
Case 147.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, clearly, to:
T.
Case 146.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NOT (NUMBERP A))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, trivially, to:
T.
Case 145.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, clearly, to:
T.
Case 144.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0)
T)).
This again simplifies, clearly, to:
T.
Case 143.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and
expanding the definitions of NEGATIVEP, NUMBERP, EQUAL, ZEROP, and INEG, to:
T.
Case 142.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0))
(EQUAL (REMAINDER A 0) 0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
This again simplifies, clearly, to:
T.
Case 141.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0))
(EQUAL (REMAINDER A 0) 0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
But this again simplifies, appealing to the lemmas REMAINDER-ZERO,
EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and expanding ZEROP and INEG, to:
T.
Case 140.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
0)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))),
which again simplifies, using linear arithmetic, applying REMAINDER-NOOP,
GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and opening up the
definitions of EQUAL, NUMBERP, ZEROP, and INEG, to:
T.
Case 139.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL A 0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
This again simplifies, trivially, to:
T.
Case 138.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
However this again simplifies, rewriting with the lemmas REMAINDER-ZERO,
EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and unfolding the functions ZEROP and
INEG, to:
T.
Case 137.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))),
which again simplifies, using linear arithmetic, rewriting with the lemmas
REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and
expanding the functions EQUAL, NUMBERP, ZEROP, and INEG, to:
T.
Case 136.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL A 0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))),
which again simplifies, trivially, to:
T.
Case 135.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) 0))
0))).
This again simplifies, trivially, to:
T.
Case 134.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
This again simplifies, clearly, to:
T.
Case 133.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0)
(NOT (NUMBERP A)))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
But this again simplifies, using linear arithmetic, applying REMAINDER-NOOP,
GCD-REMAINDER, and REMAINDER-ZERO, and unfolding the functions EQUAL,
NUMBERP, and ZEROP, to:
T.
Case 132.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
This again simplifies, rewriting with COMMUTATIVITY-OF-GCD, REMAINDER-ZERO,
and EQUAL-GCD-0, and opening up the definition of ZEROP, to:
T.
Case 131.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD 0 B) 0) 0))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up the
definitions of EQUAL, NUMBERP, and ZEROP, to:
T.
Case 130.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B) 0) 0)
(EQUAL (REMAINDER A 0) 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
But this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0,
and opening up the function ZEROP, to:
T.
Case 129.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD A B) 0) 0))
(EQUAL (EQUAL (REMAINDER B 0) 0) T)).
This again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up the
functions NEGATIVEP, NUMBERP, EQUAL, and ZEROP, to:
T.
Case 128.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0))
(EQUAL A 0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B 0) 0))),
which again simplifies, trivially, to:
T.
Case 127.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (REMAINDER B 0) 0))).
However this again simplifies, rewriting with the lemma GCD-REMAINDER, and
unfolding the functions NUMBERP, REMAINDER, and EQUAL, to:
T.
Case 126.
(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(NOT (EQUAL (REMAINDER B 0) 0))),
which again simplifies, appealing to the lemmas COMMUTATIVITY-OF-GCD,
REMAINDER-ZERO, EQUAL-GCD-0, and MINUS-NEGATIVE-GUTS, and opening up the
definitions of ZEROP and INEG, to:
T.
Case 125.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD 0 B) 0) 0)))
(NOT (EQUAL (REMAINDER B 0) 0))),
which again simplifies, applying the lemma GCD-REMAINDER, and unfolding
NUMBERP, REMAINDER, and EQUAL, to:
T.
Case 124.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B) 0) 0))
(EQUAL (REMAINDER A 0) 0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B 0) 0))),
which again simplifies, rewriting with COMMON-DIVISOR-DIVIDES-GCD, and
opening up the function EQUAL, to:
T.
Case 123.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD A B) 0) 0)))
(NOT (EQUAL (REMAINDER B 0) 0))).
But this again simplifies, rewriting with GCD-REMAINDER, and opening up
NEGATIVEP, NUMBERP, REMAINDER, and EQUAL, to:
T.
Case 122.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
But this again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and opening up the functions NEGATIVEP,
NUMBERP, EQUAL, and INEG, to:
T.
Case 121.
(IMPLIES (AND (NOT (NEGATIVEP A))
(EQUAL A 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)),
which again simplifies, trivially, to:
T.
Case 120.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, clearly, to:
T.
Case 119.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0)
(EQUAL (REMAINDER A C) 0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
But this again simplifies, applying REMAINDER-GCD-ARG1, and expanding the
definitions of EQUAL and INEG, to:
T.
Case 118.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
C)
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
But this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG,
to:
T.
Case 117.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, clearly, to:
T.
Case 116.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, trivially, to:
T.
Case 115.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
But this again simplifies, applying the lemma REMAINDER-GCD-ARG1, and
expanding INEG and EQUAL, to:
T.
Case 114.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(NOT (NUMBERP A))
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG,
to:
T.
Case 113.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, obviously, to:
T.
Case 112.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, clearly, to:
T.
Case 111.
(IMPLIES (AND (EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NOT (NUMBERP A))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, clearly, to:
T.
Case 110.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(EQUAL A 0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, clearly, to:
T.
Case 109.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)
(NUMBERP B)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0)
T)).
This again simplifies, obviously, to:
T.
Case 108.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))).
This again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of NEGATIVEP,
NUMBERP, EQUAL, and INEG, to:
T.
Case 107.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0))
(EQUAL (REMAINDER A C) 0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))),
which again simplifies, clearly, to:
T.
Case 106.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0))
(EQUAL (REMAINDER A C) 0)
(NOT (NUMBERP B))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (EQUAL B 0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))).
But this again simplifies, applying REMAINDER-GCD-ARG1, and opening up the
functions EQUAL and INEG, to:
T.
Case 105.
(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
C)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))).
However this again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL, NUMBERP,
and INEG, to:
T.
Case 104.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL A 0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))),
which again simplifies, trivially, to:
T.
Case 103.
(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))).
But this again simplifies, appealing to the lemma REMAINDER-GCD-ARG1, and
unfolding INEG, to:
T.
Case 102.
(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))),
which again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG,
to:
T.
Case 101.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL A 0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))),
which again simplifies, obviously, to:
T.
Case 100.
(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)
(NUMBERP B))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS B) C))
0))).
This again simplifies, trivially, to:
T.
Case 99.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0)
(EQUAL A 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B C) 0) T)).
This again simplifies, obviously, to:
T.
Case 98.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0)
(NOT (NUMBERP A)))
(EQUAL (EQUAL (REMAINDER B C) 0) T)).
However this again simplifies, using linear arithmetic, rewriting with the
lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of
EQUAL and NUMBERP, to:
T.
Case 97.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0)
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(EQUAL (EQUAL (REMAINDER B C) 0) T)),
which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and
REMAINDER-GCD-ARG1, to:
T.
Case 96.(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD 0 B) C) 0))
(EQUAL (EQUAL (REMAINDER B C) 0) T)).
But this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and expanding EQUAL and NUMBERP, to:
T.
Case 95.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B) C) 0)
(EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0)))
(EQUAL (EQUAL (REMAINDER B C) 0) T)).
But this again simplifies, applying REMAINDER-GCD-ARG1, and opening up EQUAL,
to:
T.
Case 94.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD A B) C) 0))
(EQUAL (EQUAL (REMAINDER B C) 0) T)).
This again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of NEGATIVEP,
NUMBERP, and EQUAL, to:
T.
Case 93.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0))
(EQUAL A 0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B C) 0))).
This again simplifies, clearly, to:
T.
Case 92.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL (REMAINDER B C) 0))).
But this again simplifies, using linear arithmetic, rewriting with the
lemmas REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL
and NUMBERP, to:
T.
Case 91.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(NOT (EQUAL (REMAINDER B C) 0))),
which again simplifies, rewriting with COMMUTATIVITY-OF-GCD and
REMAINDER-GCD-ARG1, and unfolding the functions EQUAL and INEG, to:
T.
Case 90.(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD 0 B) C) 0)))
(NOT (EQUAL (REMAINDER B C) 0))).
However this again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions EQUAL and
NUMBERP, to:
T.
Case 89.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B) C) 0))
(EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0)))
(NOT (EQUAL (REMAINDER B C) 0))),
which again simplifies, appealing to the lemma COMMON-DIVISOR-DIVIDES-GCD,
and unfolding the definition of EQUAL, to:
T.
Case 88.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD A B) C) 0)))
(NOT (EQUAL (REMAINDER B C) 0))),
which again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding NEGATIVEP, NUMBERP, and
EQUAL, to:
T.
Case 87.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL B 0))),
which again simplifies, obviously, to:
T.
Case 86.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0)))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 85.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(EQUAL A 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0)))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 84.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)).
This again simplifies, applying REMAINDER-GCD-ARG1, to:
T.
Case 83.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 82.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
But this again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and expanding the definitions of EQUAL and
NUMBERP, to:
T.
Case 81.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD A 0)
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to:
T.
Case 80.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD A 0)
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0))).
However this again simplifies, using linear arithmetic, appealing to the
lemmas REMAINDER-NOOP and GCD-REMAINDER, and unfolding EQUAL and NUMBERP, to:
T.
Case 79.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0)),
which again simplifies, rewriting with REMAINDER-GCD-ARG1, to:
T.
Case 78.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B)
(NEGATIVE-GUTS C))
0))
(EQUAL (REMAINDER A (NEGATIVE-GUTS C))
0))
(NOT (EQUAL B 0))).
But this again simplifies, using linear arithmetic, applying REMAINDER-NOOP
and GCD-REMAINDER, and opening up the definitions of NEGATIVEP, NUMBERP, and
EQUAL, to:
T.
Case 77.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0))
(EQUAL (REMAINDER A 0) 0)).
This again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and
unfolding ZEROP, to:
T.
Case 76.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0))
(EQUAL (REMAINDER A 0) 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 75.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
0)
0))
(EQUAL (REMAINDER A 0) 0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, using linear arithmetic, applying REMAINDER-NOOP,
GCD-REMAINDER, and REMAINDER-ZERO, and expanding the functions EQUAL,
NUMBERP, and ZEROP, to:
T.
Case 74.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD A 0) 0) 0))
(EQUAL (REMAINDER A 0) 0)).
This again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and opening up EQUAL,
NUMBERP, and ZEROP, to:
T.
Case 73.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD A 0) 0) 0)))
(NOT (EQUAL (REMAINDER A 0) 0))).
This again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the
functions EQUAL, NUMBERP, and ZEROP, to:
T.
Case 72.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B) 0) 0))
(EQUAL (REMAINDER A 0) 0)).
This again simplifies, applying REMAINDER-ZERO and EQUAL-GCD-0, and
expanding ZEROP, to:
T.
Case 71.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B) 0) 0))
(EQUAL (REMAINDER A 0) 0))
(NOT (EQUAL B 0))).
This again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the
functions NEGATIVEP, NUMBERP, EQUAL, and ZEROP, to:
T.
Case 70.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0))
(EQUAL (REMAINDER A C) 0)),
which again simplifies, rewriting with REMAINDER-GCD-ARG1, to:
T.
Case 69.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0))
(EQUAL (REMAINDER A C) 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 68.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD A (NEGATIVE-GUTS B))
C)
0))
(EQUAL (REMAINDER A C) 0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and
GCD-REMAINDER, and unfolding the definitions of EQUAL and NUMBERP, to:
T.
Case 67.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD A 0) C) 0))
(EQUAL (REMAINDER A C) 0)).
But this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL and NUMBERP, to:
T.
Case 66.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD A 0) C) 0)))
(NOT (EQUAL (REMAINDER A C) 0))).
However this again simplifies, using linear arithmetic, appealing to the
lemmas REMAINDER-NOOP and GCD-REMAINDER, and opening up EQUAL and NUMBERP,
to:
T.
Case 65.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD A B) C) 0))
(EQUAL (REMAINDER A C) 0)),
which again simplifies, applying REMAINDER-GCD-ARG1, to:
T.
Case 64.(IMPLIES (AND (NOT (NEGATIVEP A))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD A B) C) 0))
(EQUAL (REMAINDER A C) 0))
(NOT (EQUAL B 0))).
However this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions NEGATIVEP,
NUMBERP, and EQUAL, to:
T.
Case 63.(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 62.(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
0)
0)))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 61.(IMPLIES (AND (NOT (NEGATIVEP A))
(NOT (NUMBERP A))
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD 0 (NEGATIVE-GUTS B))
C)
0)))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 60.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, obviously, to:
T.
Case 59.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, trivially, to:
T.
Case 58.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, clearly, to:
T.
Case 57.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(EQUAL B 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, obviously, to:
T.
Case 56.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(EQUAL B 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, clearly, to:
T.
Case 55.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(EQUAL B 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, clearly, to:
T.
Case 54.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, clearly, to:
T.
Case 53.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, trivially, to:
T.
Case 52.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, clearly, to:
T.
Case 51.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, trivially, to:
T.
Case 50.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 49.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 48.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NEGATIVEP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(NOT (NUMBERP A)))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 47.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, obviously, to:
T.
Case 46.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 45.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 44.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 43.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, trivially, to:
T.
Case 42.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 41.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 40.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(NOT (EQUAL (NEGATIVE-GUTS B) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(NOT (NUMBERP A)))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 39.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NEGATIVEP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, clearly, to:
T.
Case 38.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, clearly, to:
T.
Case 37.(IMPLIES (AND (NEGATIVEP A)
(EQUAL (NEGATIVE-GUTS A) 0)
(NEGATIVEP B)
(EQUAL (NEGATIVE-GUTS B) 0)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NEGATIVEP C))
(NUMBERP C))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, clearly, to:
T.
Case 36.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
However this again simplifies, rewriting with the lemma REMAINDER-GCD-ARG1,
and opening up the functions INEG and EQUAL, to:
T.
Case 35.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and opening up the definitions of EQUAL,
NUMBERP, and INEG, to:
T.
Case 34.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 33.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL A 0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, trivially, to:
T.
Case 32.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
(NEGATIVE-GUTS C))
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 31.(IMPLIES (AND (NEGATIVEP A)
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
(NEGATIVE-GUTS C))
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
This again simplifies, trivially, to:
T.
Case 30.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
(NEGATIVE-GUTS C))
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
However this again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP,
and INEG, to:
T.
Case 29.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))),
which again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP,
and INEG, to:
T.
Case 28.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
(NEGATIVE-GUTS C))
0)))
(NOT (EQUAL A 0))),
which again simplifies, obviously, to:
T.
Case 27.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0)).
But this again simplifies, applying COMMUTATIVITY-OF-GCD and
REMAINDER-GCD-ARG1, and opening up the functions INEG and EQUAL, to:
T.
Case 26.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A)
(NEGATIVE-GUTS C)))
0))
(NOT (EQUAL B 0))).
This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and
GCD-REMAINDER, and expanding the functions NEGATIVEP, NUMBERP, EQUAL, and
INEG, to:
T.
Case 25.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NEGATIVEP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
(NEGATIVE-GUTS C))
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 24.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
However this again simplifies, rewriting with REMAINDER-ZERO and EQUAL-GCD-0,
and opening up ZEROP, to:
T.
Case 23.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, using linear arithmetic, applying the lemmas
REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and
unfolding EQUAL, NUMBERP, ZEROP, and INEG, to:
T.
Case 22.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(NOT (EQUAL B 0))),
which again simplifies, obviously, to:
T.
Case 21.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL A 0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, obviously, to:
T.
Case 20.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
0)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Case 19.(IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
0)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, clearly, to:
T.
Case 18.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
0)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
This again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP, GCD-REMAINDER, and REMAINDER-ZERO, and expanding the
functions EQUAL, NUMBERP, and ZEROP, to:
T.
Case 17.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
0)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and MINUS-NEGATIVE-GUTS, and
opening up the definitions of EQUAL, NUMBERP, ZEROP, and INEG, to:
T.
Case 16.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
0)
0)))
(NOT (EQUAL A 0))).
This again simplifies, obviously, to:
T.
Case 15.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0)).
However this again simplifies, rewriting with COMMUTATIVITY-OF-GCD,
REMAINDER-ZERO, and EQUAL-GCD-0, and expanding ZEROP, to:
T.
Case 14.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) 0))
0))
(NOT (EQUAL B 0))).
However this again simplifies, using linear arithmetic, appealing to the
lemmas REMAINDER-NOOP, GCD-REMAINDER, REMAINDER-ZERO, and
MINUS-NEGATIVE-GUTS, and opening up the functions NEGATIVEP, NUMBERP, EQUAL,
ZEROP, and INEG, to:
T.
Case 13.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NOT (NUMBERP C))
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
0)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))),
which again simplifies, trivially, to:
T.
Case 12.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
But this again simplifies, rewriting with REMAINDER-GCD-ARG1, and unfolding
the definitions of INEG and EQUAL, to:
T.
Case 11.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
But this again simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the functions EQUAL, NUMBERP,
and INEG, to:
T.
Case 10.(IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(NOT (EQUAL B 0))).
This again simplifies, clearly, to:
T.
Case 9. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL A 0)
(NOT (NUMBERP B)))
(NOT (EQUAL (NEGATIVE-GUTS B) 0))).
This again simplifies, obviously, to:
T.
Case 8. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NEGATIVEP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A)
(NEGATIVE-GUTS B))
C)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, trivially, to:
T.
Case 7. (IMPLIES (AND (NEGATIVEP A)
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
C)
0)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, clearly, to:
T.
Case 6. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
C)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, using linear arithmetic, applying REMAINDER-NOOP and
GCD-REMAINDER, and opening up EQUAL, NUMBERP, and INEG, to:
T.
Case 5. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
C)
0)))
(NOT (EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))).
But this again simplifies, using linear arithmetic, appealing to the lemmas
REMAINDER-NOOP and GCD-REMAINDER, and unfolding the definitions of EQUAL,
NUMBERP, and INEG, to:
T.
Case 4. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) 0)
C)
0)))
(NOT (EQUAL A 0))),
which again simplifies, trivially, to:
T.
Case 3. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0)
(NOT (EQUAL A 0)))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0)).
This again simplifies, applying COMMUTATIVITY-OF-GCD and REMAINDER-GCD-ARG1,
and opening up the functions INEG and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0))
(EQUAL (INEG (REMAINDER (NEGATIVE-GUTS A) C))
0))
(NOT (EQUAL B 0))).
However this again simplifies, using linear arithmetic, applying
REMAINDER-NOOP and GCD-REMAINDER, and expanding the functions NEGATIVEP,
NUMBERP, EQUAL, and INEG, to:
T.
Case 1. (IMPLIES (AND (NEGATIVEP A)
(NOT (EQUAL (NEGATIVE-GUTS A) 0))
(NOT (NEGATIVEP C))
(NUMBERP C)
(NOT (NEGATIVEP B))
(NUMBERP B)
(NOT (EQUAL (REMAINDER (GCD (NEGATIVE-GUTS A) B)
C)
0))
(EQUAL A 0))
(NOT (EQUAL B 0))).
This again simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 4.0 0.1 ]
IREM-IGCD-ARG1
(PROVE-LEMMA IREM-X-X
(REWRITE)
(EQUAL (IREM X X) 0)
((ENABLE-THEORY INTEGER-DEFNS)))
This conjecture simplifies, rewriting with IQUO-X-X, and expanding the
functions IZEROP, FIX-INT, INTEGERP, and IREM, to the following six new
conjectures:
Case 6. (IMPLIES (AND (NUMBERP X) (NOT (EQUAL X 0)))
(EQUAL (IDIFFERENCE X (ITIMES X 1))
0)).
This again simplifies, applying FIX-INT-REMOVER, ITIMES-1-ARG1,
COMMUTATIVITY-OF-ITIMES, and IDIFFERENCE-X-X, and unfolding the functions
INTEGERP and EQUAL, to:
T.
Case 5. (IMPLIES (AND (NEGATIVEP X)
(NOT (EQUAL (NEGATIVE-GUTS X) 0))
(NOT (EQUAL X 0)))
(EQUAL (IDIFFERENCE X (ITIMES X 1))
0)).
However this again simplifies, applying the lemmas FIX-INT-REMOVER,
ITIMES-1-ARG1, COMMUTATIVITY-OF-ITIMES, and IDIFFERENCE-X-X, and unfolding
INTEGERP and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NUMBERP X) (EQUAL X 0))
(EQUAL (IDIFFERENCE X (ITIMES X 0))
0)),
which again simplifies, unfolding NUMBERP, ITIMES, IDIFFERENCE, and EQUAL,
to:
T.
Case 3. (IMPLIES (AND (NEGATIVEP X)
(NOT (EQUAL (NEGATIVE-GUTS X) 0))
(EQUAL X 0))
(EQUAL (IDIFFERENCE X (ITIMES X 0))
0)),
which again simplifies, obviously, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP X))
(NOT (NEGATIVEP X)))
(EQUAL (IDIFFERENCE 0 (ITIMES X 0))
0)).
However this again simplifies, applying the lemmas ITIMES-0-LEFT and
COMMUTATIVITY-OF-ITIMES, and expanding IDIFFERENCE and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (NEGATIVE-GUTS X) 0))
(EQUAL (IDIFFERENCE 0 (ITIMES X 0))
0)),
which again simplifies, rewriting with ITIMES-0-LEFT and
COMMUTATIVITY-OF-ITIMES, and expanding the definitions of IDIFFERENCE and
EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
IREM-X-X
(PROVE-LEMMA GCD-TIMES-EASY-PROOF-HELPER-HELPER NIL
(IMPLIES (AND (NUMBERP A)
(NUMBERP B)
(NUMBERP C))
(EQUAL (REMAINDER (TIMES C (GCD A B))
(GCD A (TIMES B C)))
0))
((USE (GCD-FACTORS-GIVES-LINEAR-COMBINATION (X A)
(Y B)))
(INDUCT (APPEND X Y))
(ENABLE-THEORY NATS-TO-INTS)
(DISABLE IREM-0-BACKCHAIN NOT-INTEGERP IREM-NOOP)))
This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-ITIMES,
GCD-IS-IGCD, NUMBERP-ILESSP, ILESSP-STRICT, ITIMES-0-LEFT, TIMES-TO-ITIMES,
IABS-SIMPLIFY, IGCD-0-BETTER, ILESSP-FIX-INT-2, ITIMES-FIX-INT2, IREM-OF-0,
REMAINDER-TO-IREM, CORRECTNESS-OF-CANCEL-FACTORS-ILESSP-0, IREM-FIX-INT2,
IREM-X-X, EQUAL-IREM-ITIMES-0, FIX-INT-ITIMES, IGCD-NON-NEGATIVE, and
ILESSP-0-IGCD, and opening up the functions AND, IMPLIES, GCD, TIMES,
REMAINDER, EQUAL, ILESSP, FIX-INT, OR, and IZEROP, to:
(IMPLIES (AND (NOT (ILESSP A 0))
(NOT (ILESSP B 0))
(EQUAL (IPLUS (ITIMES A (CAR (GCD-FACTORS A B)))
(ITIMES B (CDR (GCD-FACTORS A B))))
(IGCD A B))
(NOT (LISTP X))
(ILESSP 0 A)
(ILESSP 0 B)
(ILESSP 0 C))
(EQUAL (IREM (ITIMES C (IGCD A B))
(IGCD A (ITIMES B C)))
0)),
which again simplifies, applying ILESSP-STRICT, to:
(IMPLIES (AND (EQUAL (IPLUS (ITIMES A (CAR (GCD-FACTORS A B)))
(ITIMES B (CDR (GCD-FACTORS A B))))
(IGCD A B))
(NOT (LISTP X))
(ILESSP 0 A)
(ILESSP 0 B)
(ILESSP 0 C))
(EQUAL (IREM (ITIMES C (IGCD A B))
(IGCD A (ITIMES B C)))
0)).
We use the above equality hypothesis by substituting:
(IPLUS (ITIMES A (CAR (GCD-FACTORS A B)))
(ITIMES B (CDR (GCD-FACTORS A B))))
for (IGCD A B) and throwing away the equality. We must thus prove:
(IMPLIES (AND (NOT (LISTP X))
(ILESSP 0 A)
(ILESSP 0 B)
(ILESSP 0 C))
(EQUAL (IREM (ITIMES C
(IPLUS (ITIMES A (CAR (GCD-FACTORS A B)))
(ITIMES B (CDR (GCD-FACTORS A B)))))
(IGCD A (ITIMES B C)))
0)).
But this further simplifies, applying COMMUTATIVITY2-OF-ITIMES,
ITIMES-DISTRIBUTES-OVER-IPLUS, IREM-ITIMES-IGCD, IREM-ITIMES-BASE,
IREM-ITIMES-CANCEL, COMMUTATIVITY-OF-ITIMES, ITIMES-0-LEFT, and IREM-IPLUS-0,
and opening up the definition of EQUAL, to:
T.
Q.E.D.
[ 0.0 0.9 0.0 ]
GCD-TIMES-EASY-PROOF-HELPER-HELPER
(PROVE-LEMMA GCD-TIMES-EASY-PROOF-HELPER NIL
(EQUAL (REMAINDER (TIMES C (GCD A B))
(GCD A (TIMES B C)))
0)
((USE (GCD-TIMES-EASY-PROOF-HELPER-HELPER))
(DISABLE REMAINDER-TIMES1)))
This conjecture simplifies, rewriting with REMAINDER-OF-NON-NUMBER,
GCD-REMAINDER, REMAINDER-TIMES2, COMMUTATIVITY-OF-TIMES,
QUOTIENT-OF-NON-NUMBER, REMAINDER-TIMES1-INSTANCE, QUOTIENT-TIMES-INSTANCE,
EQUAL-TIMES-0, and TIMES-ZERO, and opening up AND, IMPLIES, REMAINDER, NUMBERP,
EQUAL, LESSP, TIMES, QUOTIENT, and ZEROP, to two new formulas:
Case 2. (IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL C 0))
(NUMBERP C)
(NOT (NUMBERP B)))
(EQUAL (REMAINDER 0 B) 0)),
which again simplifies, appealing to the lemma REMAINDER-ZERO, and unfolding
the functions ZEROP, NUMBERP, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL C 0))
(NUMBERP C)
(NUMBERP B))
(EQUAL (REMAINDER B B) 0)),
which again simplifies, appealing to the lemma REMAINDER-X-X, and unfolding
the definition of EQUAL, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
GCD-TIMES-EASY-PROOF-HELPER
(PROVE-LEMMA GCD-TIMES-EASY-PROOF NIL
(IMPLIES (EQUAL (GCD A B) 1)
(EQUAL (GCD A (TIMES B C)) (GCD A C)))
((ENABLE EQUAL-GCD-GCD-AS-REMAINDER REMAINDER-GCD
REMAINDER-GCD-ARG1 REMAINDER-TIMES1)
(USE (GCD-TIMES-EASY-PROOF-HELPER))
(DISABLE-THEORY REMAINDERS)))
This simplifies, applying the lemmas TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES,
TIMES-ZERO, GCD-REMAINDER, REMAINDER-TIMES1, COMMON-DIVISOR-DIVIDES-GCD,
REMAINDER-GCD, and EQUAL-GCD-GCD-AS-REMAINDER, and opening up the functions
ZEROP, REMAINDER, NUMBERP, EQUAL, and LESSP, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
GCD-TIMES-EASY-PROOF
(PROVE-LEMMA GCD-TIMES-EASY
(REWRITE)
(IMPLIES (EQUAL (GCD A B) 1)
(AND (EQUAL (GCD A (TIMES B C)) (GCD A C))
(EQUAL (GCD A (TIMES C B))
(GCD A C))))
((USE (GCD-TIMES-EASY-PROOF))
(ENABLE COMMUTATIVITY-OF-TIMES)
(DISABLE-THEORY NATURALS)))
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-TIMES-EASY could!
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-TIMES-EASY could!
WARNING: Note that the proposed lemma GCD-TIMES-EASY is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and two replacement rules.
This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and unfolding
EQUAL, IMPLIES, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GCD-TIMES-EASY
(PROVE-LEMMA LESSP-GCD3
(REWRITE)
(AND (EQUAL (LESSP (GCD A B) A)
(AND (NOT (EQUAL (REMAINDER B A) 0))
(NOT (ZEROP A))
(NOT (ZEROP B))))
(EQUAL (LESSP (GCD B A) A)
(AND (NOT (EQUAL (REMAINDER B A) 0))
(NOT (ZEROP A))
(NOT (ZEROP B)))))
((USE (EQUAL-X-GCD-X-Y (X A) (Y B))
(LESSP-GCD2 (B A) (A B)))
(DISABLE-THEORY NATURALS)
(ENABLE GCD-ZERO)))
WARNING: Note that the proposed lemma LESSP-GCD3 is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and two
replacement rules.
This conjecture simplifies, rewriting with GCD-ZERO, and expanding AND,
IMPLIES, ZEROP, LESSP, NOT, REMAINDER, EQUAL, and NUMBERP, to eight new
formulas:
Case 8. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(NOT (NUMBERP B)))
(EQUAL (LESSP (GCD A B) A) F)),
which again simplifies, rewriting with GCD-ZERO, and expanding the
definition of ZEROP, to:
T.
Case 7. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(EQUAL B 0))
(EQUAL (LESSP (GCD A B) A) F)).
But this again simplifies, appealing to the lemma GCD-ZERO, and unfolding
the definition of ZEROP, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (GCD A B) A) T)),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (LESSP A (GCD B A)))
(NOT (LESSP A (GCD A B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(LESSP (GCD A B) A)),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(NOT (NUMBERP B)))
(EQUAL (LESSP (GCD B A) A) F)),
which again simplifies, rewriting with GCD-ZERO, and opening up the function
ZEROP, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(EQUAL B 0))
(EQUAL (LESSP (GCD B A) A) F)).
This again simplifies, appealing to the lemma GCD-ZERO, and expanding the
definition of ZEROP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (GCD B A) A) T)),
which again simplifies, obviously, to:
(IMPLIES (AND (NOT (EQUAL A (GCD A B)))
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (LESSP A (GCD B A)))
(NOT (LESSP A (GCD A B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(LESSP (GCD B A) A)),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NUMBERP A)
(EQUAL (EQUAL (REMAINDER B A) 0) T)
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B))))
(NOT (LESSP (GCD A B) A))),
which again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NUMBERP A)
(EQUAL (EQUAL (REMAINDER B A) 0) T)
(NOT (EQUAL A (GCD B A)))
(NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(EQUAL (LESSP A (GCD B A)) F)
(NOT (LESSP A (GCD A B))))
(NOT (LESSP (GCD B A) A))).
This again simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
LESSP-GCD3
(PROVE-LEMMA EQUAL-REMAINDER-GCD-0-PROOF NIL
(EQUAL (EQUAL (REMAINDER (GCD A B) A) 0)
(EQUAL (REMAINDER B A) 0)))
This conjecture simplifies, rewriting with REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1,
LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and
expanding the definitions of NUMBERP, EQUAL, LESSP, and REMAINDER, to the
following five new goals:
Case 5. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NUMBERP B)).
However this again simplifies, rewriting with the lemma
REMAINDER-OF-NON-NUMBER, and unfolding the functions LESSP, EQUAL, NUMBERP,
and REMAINDER, to:
T.
Case 4. (IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL B 0))),
which again simplifies, expanding the functions LESSP, EQUAL, NUMBERP, and
REMAINDER, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A))
(NOT (EQUAL (GCD A B) 0))),
which again simplifies, applying EQUAL-GCD-0, to:
T.
Case 2. (IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(NOT (NUMBERP A))
(NUMBERP B))
(EQUAL (EQUAL B 0) T)).
This again simplifies, rewriting with REMAINDER-ZERO, and expanding ZEROP,
to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(EQUAL A 0)
(NUMBERP B))
(EQUAL (EQUAL B 0) T)).
However this again simplifies, rewriting with the lemma REMAINDER-ZERO, and
expanding the definition of ZEROP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
EQUAL-REMAINDER-GCD-0-PROOF
(PROVE-LEMMA EQUAL-REMAINDER-GCD-0
(REWRITE)
(AND (EQUAL (EQUAL (REMAINDER (GCD A B) A) 0)
(EQUAL (REMAINDER B A) 0))
(EQUAL (EQUAL (REMAINDER (GCD B A) A) 0)
(EQUAL (REMAINDER B A) 0))))
WARNING: the previously added lemma, REMAINDER-GCD-ARG1, could be applied
whenever the newly proposed EQUAL-REMAINDER-GCD-0 could!
WARNING: the previously added lemma, REMAINDER-GCD-ARG1, could be applied
whenever the newly proposed EQUAL-REMAINDER-GCD-0 could!
WARNING: Note that the proposed lemma EQUAL-REMAINDER-GCD-0 is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
This formula can be simplified, using the abbreviation AND, to the following
two new goals:
Case 2. (EQUAL (EQUAL (REMAINDER (GCD A B) A) 0)
(EQUAL (REMAINDER B A) 0)).
This simplifies, rewriting with REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1,
LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and
expanding the functions NUMBERP, EQUAL, LESSP, and REMAINDER, to five new
conjectures:
Case 2.5.
(IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NUMBERP B)),
which again simplifies, applying REMAINDER-OF-NON-NUMBER, and unfolding
LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 2.4.
(IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL B 0))).
However this again simplifies, expanding LESSP, EQUAL, NUMBERP, and
REMAINDER, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A))
(NOT (EQUAL (GCD A B) 0))),
which again simplifies, applying EQUAL-GCD-0, to:
T.
Case 2.2.
(IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(NOT (NUMBERP A))
(NUMBERP B))
(EQUAL (EQUAL B 0) T)).
This again simplifies, applying REMAINDER-ZERO, and opening up the
function ZEROP, to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(EQUAL A 0)
(NUMBERP B))
(EQUAL (EQUAL B 0) T)).
However this again simplifies, applying REMAINDER-ZERO, and unfolding
ZEROP, to:
T.
Case 1. (EQUAL (EQUAL (REMAINDER (GCD B A) A) 0)
(EQUAL (REMAINDER B A) 0)).
This simplifies, rewriting with COMMUTATIVITY-OF-GCD, REMAINDER-NOOP,
DIFFERENCE-LEQ-ARG1, LESSP-GCD2, LESSP-GCD3, GCD-REMAINDER, and
REMAINDER-OF-NON-NUMBER, and expanding the definitions of NUMBERP, EQUAL,
LESSP, and REMAINDER, to five new goals:
Case 1.5.
(IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NUMBERP B)),
which again simplifies, rewriting with the lemma REMAINDER-OF-NON-NUMBER,
and opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 1.4.
(IMPLIES (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL B 0))),
which again simplifies, unfolding the functions LESSP, EQUAL, NUMBERP, and
REMAINDER, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL (REMAINDER B A) 0))
(NOT (EQUAL A 0))
(NUMBERP A))
(NOT (EQUAL (GCD A B) 0))),
which again simplifies, rewriting with EQUAL-GCD-0, to:
T.
Case 1.2.
(IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(NOT (NUMBERP A))
(NUMBERP B))
(EQUAL (EQUAL B 0) T)).
But this again simplifies, rewriting with the lemma REMAINDER-ZERO, and
opening up ZEROP, to:
T.
Case 1.1.
(IMPLIES (AND (EQUAL (REMAINDER B A) 0)
(EQUAL A 0)
(NUMBERP B))
(EQUAL (EQUAL B 0) T)),
which again simplifies, applying REMAINDER-ZERO, and opening up ZEROP, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
EQUAL-REMAINDER-GCD-0
(PROVE-LEMMA EQUAL-REMAINDER-X-Y-X
(REWRITE)
(EQUAL (EQUAL (REMAINDER X Y) X)
(OR (AND (NUMBERP X) (LESSP X Y))
(EQUAL X 0)
(AND (EQUAL (FIX Y) 0) (NUMBERP X)))))
This simplifies, expanding AND, FIX, and OR, to ten new formulas:
Case 10.(IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X))
(NOT (NUMBERP Y)))
(NOT (NUMBERP X))),
which again simplifies, applying REMAINDER-ZERO, and unfolding ZEROP, to:
T.
Case 9. (IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X))
(EQUAL Y 0))
(NOT (NUMBERP X))).
But this again simplifies, rewriting with the lemma REMAINDER-ZERO, and
opening up the definition of ZEROP, to:
T.
Case 8. (IMPLIES (NOT (EQUAL (REMAINDER X Y) X))
(NOT (EQUAL X 0))),
which again simplifies, opening up LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 7. (IMPLIES (AND (NOT (EQUAL (REMAINDER X Y) X))
(NUMBERP X))
(NOT (LESSP X Y))),
which again simplifies, rewriting with the lemma REMAINDER-NOOP, to:
T.
Case 6. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (NUMBERP X))
(NOT (EQUAL X 0))
(NUMBERP Y))
(EQUAL Y 0)),
which again simplifies, clearly, to:
T.
Case 5. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (LESSP X Y))
(NOT (EQUAL X 0))
(NUMBERP Y))
(EQUAL Y 0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
(PLUS Z (TIMES Y V)) to eliminate (REMAINDER X Y) and (QUOTIENT X Y). We
use LESSP-REMAINDER, 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 goals:
Case 5.2.
(IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X Y) X)
(NOT (LESSP X Y))
(NOT (EQUAL X 0))
(NUMBERP Y))
(EQUAL Y 0)),
which further simplifies, clearly, to:
T.
Case 5.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z Y) (NOT (ZEROP Y)))
(NUMBERP V)
(EQUAL Z (PLUS Z (TIMES Y V)))
(NOT (LESSP (PLUS Z (TIMES Y V)) Y))
(NOT (EQUAL (PLUS Z (TIMES Y V)) 0))
(NUMBERP Y))
(EQUAL Y 0)).
But this further simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
CORRECTNESS-OF-CANCEL-EQUAL-PLUS, EQUAL-TIMES-0, and PLUS-ZERO-ARG2, and
expanding ZEROP, NOT, FIX, EQUAL, and TIMES, to:
T.
Case 4. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (NUMBERP X))
(NOT (EQUAL X 0))
(NOT (NUMBERP Y)))
(EQUAL (NUMBERP X) T)).
This again simplifies, trivially, to:
T.
Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (NUMBERP X))
(NOT (EQUAL X 0))
(EQUAL Y 0))
(EQUAL (NUMBERP X) T)).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (LESSP X Y))
(NOT (EQUAL X 0))
(NOT (NUMBERP Y)))
(EQUAL (NUMBERP X) T)).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Y) X)
(NOT (LESSP X Y))
(NOT (EQUAL X 0))
(EQUAL Y 0))
(EQUAL (NUMBERP X) T)).
This again simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EQUAL-REMAINDER-X-Y-X
(PROVE-LEMMA GCD-A-GCD-EXP-A
(REWRITE)
(EQUAL (GCD A (EXP A B))
(IF (ZEROP B) 1 (FIX A))))
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-A-GCD-EXP-A could!
This conjecture simplifies, expanding the definitions of ZEROP and FIX, to the
following four new formulas:
Case 4. (IMPLIES (NOT (NUMBERP B))
(EQUAL (GCD A (EXP A B)) 1)).
This again simplifies, applying EXP-ZERO, REMAINDER-1-ARG2, and
GCD-REMAINDER, and opening up ZEROP, EQUAL, and NUMBERP, to:
T.
Case 3. (IMPLIES (EQUAL B 0)
(EQUAL (GCD A (EXP A B)) 1)).
This again simplifies, applying EXP-0-ARG2, REMAINDER-1-ARG2, and
GCD-REMAINDER, and opening up the functions EQUAL and NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL B 0))
(NUMBERP B)
(NUMBERP A))
(EQUAL (GCD A (EXP A B)) A)).
However this again simplifies, rewriting with REMAINDER-EXP and
GCD-REMAINDER, and expanding the function EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL B 0))
(NUMBERP B)
(NOT (NUMBERP A)))
(EQUAL (GCD A (EXP A B)) 0)).
This again simplifies, rewriting with REMAINDER-ZERO and GCD-REMAINDER, and
expanding the definitions of TIMES, EXP, EQUAL, NUMBERP, and ZEROP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
GCD-A-GCD-EXP-A
(PROVE-LEMMA EQUAL-GCD-TIMES-1-HELP1 NIL
(IMPLIES (AND (EQUAL (GCD A B) 1)
(EQUAL (GCD A C) 1))
(EQUAL (GCD A (TIMES B C)) 1)))
This conjecture simplifies, applying GCD-TIMES-EASY, and unfolding the
definition of EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
EQUAL-GCD-TIMES-1-HELP1
(PROVE-LEMMA REMAINDER-GCD-GCD-0-HACK
(REWRITE)
(EQUAL (REMAINDER (GCD A (TIMES B C))
(GCD A C))
0))
This formula can be simplified, using the abbreviations REMAINDER-GCD and
REMAINDER-GCD-ARG1, to the following two new goals:
Case 2. (EQUAL 0 0).
This simplifies, obviously, to:
T.
Case 1. (EQUAL (REMAINDER (TIMES B C) (GCD A C))
0).
This simplifies, rewriting with the lemmas REMAINDER-TIMES1-INSTANCE and
REMAINDER-GCD-0, and unfolding EQUAL, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
REMAINDER-GCD-GCD-0-HACK
(PROVE-LEMMA LESSP-GCD-TIMES NIL
(IMPLIES (OR (NOT (ZEROP A))
(NOT (ZEROP (TIMES B C))))
(NOT (LESSP (GCD A (TIMES B C))
(GCD A C))))
((USE (REMAINDER-GCD-GCD-0-HACK))
(DISABLE REMAINDER-GCD-GCD-0-HACK)
(DISABLE-THEORY NATURALS)
(ENABLE REMAINDER-NOOP EQUAL-TIMES-0 EQUAL-GCD-0)))
This simplifies, rewriting with REMAINDER-NOOP, EQUAL-TIMES-0, and EQUAL-GCD-0,
and opening up the functions ZEROP, NOT, EQUAL, TIMES, and OR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-GCD-TIMES
(PROVE-LEMMA LESSP-1-HACK
(REWRITE)
(EQUAL (LESSP 1 X)
(AND (NOT (ZEROP X))
(NOT (EQUAL X 1)))))
WARNING: the newly proposed lemma, LESSP-1-HACK, could be applied whenever
the previously added lemma LESSP-1-TIMES could.
This conjecture simplifies, unfolding the definitions of ZEROP, NOT, and AND,
to four new conjectures:
Case 4. (IMPLIES (EQUAL X 0)
(EQUAL (LESSP 1 X) F)),
which again simplifies, unfolding the functions LESSP and EQUAL, to:
T.
Case 3. (IMPLIES (NOT (NUMBERP X))
(EQUAL (LESSP 1 X) F)),
which again simplifies, unfolding the functions LESSP and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL X 1)
(EQUAL (LESSP 1 X) F)),
which again simplifies, expanding the functions LESSP and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(EQUAL (LESSP 1 X) T)),
which again simplifies, clearly, to the new formula:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP 1 X)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-1-HACK
(PROVE-LEMMA EQUAL-GCD-TIMES-1-HELP2 NIL
(IMPLIES (EQUAL (GCD A (TIMES B C)) 1)
(EQUAL (GCD A C) 1))
((USE (LESSP-GCD-TIMES))
(DISABLE-THEORY REMAINDERS)
(ENABLE-THEORY MULTIPLICATION)))
This formula simplifies, applying EQUAL-TIMES-0, EQUAL-GCD-0, LESSP-1-HACK,
GCD-REMAINDER, COMMUTATIVITY-OF-TIMES, and TIMES-ZERO, and expanding the
definitions of ZEROP, NOT, OR, IMPLIES, EQUAL, TIMES, REMAINDER, NUMBERP, and
GCD, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EQUAL-GCD-TIMES-1-HELP2
(PROVE-LEMMA EQUAL-GCD-TIMES-1
(REWRITE)
(EQUAL (EQUAL (GCD A (TIMES B C)) 1)
(AND (EQUAL (GCD A B) 1)
(EQUAL (GCD A C) 1)))
((USE (EQUAL-GCD-TIMES-1-HELP1)
(EQUAL-GCD-TIMES-1-HELP2)
(EQUAL-GCD-TIMES-1-HELP2 (B C) (C B)))
(DISABLE-THEORY NATURALS)))
This conjecture simplifies, applying GCD-TIMES-EASY, and expanding the
functions AND, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
EQUAL-GCD-TIMES-1
(PROVE-LEMMA GCD-EXP-1
(REWRITE)
(AND (EQUAL (EQUAL (GCD A (EXP B C)) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C)))
(EQUAL (EQUAL (GCD (EXP B C) A) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C))))
((INDUCT (EXP B C))))
WARNING: Note that the proposed lemma GCD-EXP-1 is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and two
replacement rules.
This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new conjectures:
Case 2. (IMPLIES (ZEROP C)
(AND (EQUAL (EQUAL (GCD A (EXP B C)) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C)))
(EQUAL (EQUAL (GCD (EXP B C) A) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C))))).
This simplifies, appealing to the lemmas EXP-0-ARG2, REMAINDER-1-ARG2,
GCD-REMAINDER, and EXP-ZERO, and unfolding ZEROP, EQUAL, NUMBERP, OR, and
AND, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL C 0))
(NUMBERP C)
(EQUAL (EQUAL (GCD A (EXP B (SUB1 C))) 1)
(OR (EQUAL (GCD A B) 1)
(ZEROP (SUB1 C))))
(EQUAL (EQUAL (GCD (EXP B (SUB1 C)) A) 1)
(OR (EQUAL (GCD A B) 1)
(ZEROP (SUB1 C)))))
(AND (EQUAL (EQUAL (GCD A (EXP B C)) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C)))
(EQUAL (EQUAL (GCD (EXP B C) A) 1)
(OR (EQUAL (GCD A B) 1) (ZEROP C))))).
This simplifies, rewriting with the lemmas EQUAL-SUB1-0, EXP-ZERO,
REMAINDER-1-ARG2, GCD-REMAINDER, COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1,
COMMUTATIVITY-OF-GCD, EQUAL-GCD-TIMES-1, and GCD-TIMES-EASY, and expanding
the definitions of ZEROP, OR, EQUAL, NUMBERP, EXP, and AND, to the following
three new goals:
Case 1.3.
(IMPLIES (AND (NOT (EQUAL C 0))
(NUMBERP C)
(EQUAL (GCD A (EXP B (SUB1 C))) 1)
(EQUAL (EQUAL C 1) T)
(NOT (EQUAL (GCD A B) 1))
(NOT (NUMBERP B)))
(NOT (EQUAL (GCD A 0) 1))).
However this again simplifies, applying EQUAL-SUB1-0, EXP-ZERO,
REMAINDER-1-ARG2, GCD-REMAINDER, REMAINDER-OF-NON-NUMBER, and
REMAINDER-ZERO, and expanding the functions ZEROP, EQUAL, NUMBERP,
REMAINDER, and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL C 0))
(NUMBERP C)
(EQUAL (GCD A (EXP B (SUB1 C))) 1)
(EQUAL (EQUAL C 1) T)
(EQUAL (GCD A B) 1)
(NUMBERP B))
(EQUAL (EQUAL (GCD A B) 1) T)).
But this again simplifies, rewriting with EQUAL-SUB1-0, EXP-ZERO,
REMAINDER-1-ARG2, and GCD-REMAINDER, and expanding the definitions of
ZEROP, EQUAL, and NUMBERP, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL C 0))
(NUMBERP C)
(EQUAL (GCD A (EXP B (SUB1 C))) 1)
(EQUAL (EQUAL C 1) T)
(EQUAL (GCD A B) 1)
(NOT (NUMBERP B)))
(EQUAL (EQUAL (GCD A 0) 1) T)).
This again simplifies, rewriting with EQUAL-SUB1-0, EXP-ZERO,
REMAINDER-1-ARG2, GCD-REMAINDER, and REMAINDER-OF-NON-NUMBER, and opening
up the functions ZEROP, EQUAL, NUMBERP, REMAINDER, LESSP, and GCD, to:
T.
Q.E.D.
[ 0.0 2.1 0.0 ]
GCD-EXP-1
(PROVE-LEMMA GCD-REMAINDER-TIMES-FACT1-PROOF2
(REWRITE)
(IMPLIES (EQUAL (GCD A B) 1)
(EQUAL (EQUAL (REMAINDER (TIMES C B) A) 0)
(EQUAL (REMAINDER C A) 0))))
This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES and
GCD-REMAINDER-TIMES-FACT1-PROOF, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
GCD-REMAINDER-TIMES-FACT1-PROOF2
(PROVE-LEMMA TIMES-QUOTIENT-BETTER
(REWRITE)
(IMPLIES (EQUAL (REMAINDER X Y) 0)
(AND (EQUAL (TIMES (QUOTIENT X Y) Y)
(IF (ZEROP Y) 0 (FIX X)))
(EQUAL (TIMES Y (QUOTIENT X Y))
(IF (ZEROP Y) 0 (FIX X))))))
WARNING: the newly proposed lemma, TIMES-QUOTIENT-BETTER, could be applied
whenever the previously added lemma TIMES-QUOTIENT could.
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-QUOTIENT-BETTER could!
WARNING: the newly proposed lemma, TIMES-QUOTIENT-BETTER, could be applied
whenever the previously added lemma TIMES-QUOTIENT could.
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-QUOTIENT-BETTER could!
WARNING: Note that the proposed lemma TIMES-QUOTIENT-BETTER is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding
ZEROP, FIX, and AND, to the following four new conjectures:
Case 4. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0)
(EQUAL Y 0))
(EQUAL (TIMES Y (QUOTIENT X Y)) 0)).
This again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0)
(NOT (NUMBERP Y)))
(EQUAL (TIMES Y (QUOTIENT X Y)) 0)),
which again simplifies, applying REMAINDER-ZERO, QUOTIENT-ZERO, TIMES-ZERO,
and COMMUTATIVITY-OF-TIMES, and unfolding the definitions of ZEROP and EQUAL,
to:
T.
Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0)
(NOT (NUMBERP X)))
(EQUAL (TIMES Y (QUOTIENT X Y)) 0)).
This again simplifies, rewriting with REMAINDER-OF-NON-NUMBER,
QUOTIENT-OF-NON-NUMBER, and COMMUTATIVITY-OF-TIMES, and expanding the
functions LESSP, EQUAL, NUMBERP, REMAINDER, QUOTIENT, and TIMES, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (TIMES Y (QUOTIENT X Y)) X)).
But this again simplifies, applying TIMES-QUOTIENT, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
TIMES-QUOTIENT-BETTER
(PROVE-LEMMA EQUAL-REMAINDER-EXP-0
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER A C) 0)
(NOT (ZEROP B)))
(EQUAL (REMAINDER (EXP A B) C) 0)))
This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to:
(IMPLIES (AND (EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (REMAINDER (EXP A B) C) 0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z))
to eliminate (REMAINDER A C) and (QUOTIENT A C). We employ LESSP-REMAINDER,
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. (IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (REMAINDER (EXP A B) C) 0)).
But this simplifies, rewriting with REMAINDER-OF-NON-NUMBER, and expanding
LESSP, EQUAL, NUMBERP, REMAINDER, TIMES, and EXP, to:
T.
Case 3. (IMPLIES (AND (EQUAL C 0)
(EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (REMAINDER (EXP A B) C) 0)).
This simplifies, appealing to the lemmas REMAINDER-ZERO and EXP-0-ARG1, and
opening up ZEROP, REMAINDER, EQUAL, TIMES, and EXP, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP C))
(EQUAL (REMAINDER A C) 0)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (REMAINDER (EXP A B) C) 0)),
which simplifies, applying the lemmas REMAINDER-ZERO and EXP-0-ARG1, and
expanding the definitions of ZEROP, NUMBERP, EQUAL, TIMES, and EXP, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL X 0)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (REMAINDER (EXP (PLUS X (TIMES C Z)) B)
C)
0)),
which simplifies, applying EXP-TIMES, REMAINDER-EXP, and REMAINDER-TIMES1,
and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
EQUAL-REMAINDER-EXP-0
(PROVE-LEMMA REMAINDER-2-HACK
(REWRITE)
(EQUAL (REMAINDER 2 X)
(IF (OR (EQUAL X 1) (EQUAL X 2))
0 2)))
This simplifies, unfolding the definition of OR, to the following three new
formulas:
Case 3. (IMPLIES (EQUAL X 2)
(EQUAL (REMAINDER 2 X) 0)).
This again simplifies, opening up REMAINDER and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL X 1)
(EQUAL (REMAINDER 2 X) 0)),
which again simplifies, unfolding the definitions of REMAINDER and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL X 1))
(NOT (EQUAL X 2)))
(EQUAL (REMAINDER 2 X) 2)),
which again simplifies, applying REMAINDER-NOOP, DIFFERENCE-LEQ-ARG1,
EQUAL-SUB1-0, and LESSP-1-HACK, and unfolding the functions LESSP, EQUAL,
SUB1, NUMBERP, and REMAINDER, to the new formula:
(IMPLIES (AND (NOT (EQUAL X 1))
(NOT (EQUAL X 2))
(NOT (EQUAL X 0))
(NUMBERP X))
(NOT (EQUAL (SUB1 X) 1))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
REMAINDER-2-HACK
(PROVE-LEMMA REMAINDER-TIMES-HACK2
(REWRITE)
(IMPLIES (NOT (EQUAL (REMAINDER A B) 0))
(AND (NOT (EQUAL (REMAINDER A (TIMES B C)) 0))
(NOT (EQUAL (REMAINDER A (TIMES C B))
0)))))
WARNING: Note that the proposed lemma REMAINDER-TIMES-HACK2 is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding
the definitions of NOT and AND, to:
(IMPLIES (NOT (EQUAL (REMAINDER A B) 0))
(NOT (EQUAL (REMAINDER A (TIMES B C)) 0))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES B Z))
to eliminate (REMAINDER A B) and (QUOTIENT A B). We rely upon LESSP-REMAINDER,
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 conjectures:
Case 4. (IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL (REMAINDER A B) 0)))
(NOT (EQUAL (REMAINDER A (TIMES B C)) 0))).
However this further simplifies, applying REMAINDER-OF-NON-NUMBER, and
opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 3. (IMPLIES (AND (EQUAL B 0)
(NOT (EQUAL (REMAINDER A B) 0)))
(NOT (EQUAL (REMAINDER A (TIMES B C)) 0))).
However this further simplifies, applying REMAINDER-ZERO, and opening up
ZEROP, EQUAL, and TIMES, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER A B) 0)))
(NOT (EQUAL (REMAINDER A (TIMES B C)) 0))).
But this further simplifies, rewriting with REMAINDER-ZERO, and unfolding
the functions ZEROP and TIMES, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X B) (NOT (ZEROP B)))
(NUMBERP Z)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (EQUAL X 0)))
(NOT (EQUAL (REMAINDER (PLUS X (TIMES B Z))
(TIMES B C))
0))).
However this further simplifies, appealing to the lemmas
REMAINDER-TIMES2-INSTANCE, REMAINDER-PLUS-TIMES-TIMES, and EQUAL-PLUS-0, and
opening up the definitions of ZEROP and NOT, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
REMAINDER-TIMES-HACK2
(PROVE-LEMMA GCD-A-ADD1-A
(REWRITE)
(EQUAL (GCD A (ADD1 A)) 1))
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-A-ADD1-A could!
This simplifies, using linear arithmetic, rewriting with GCD-REMAINDER,
REMAINDER-NOOP, DIFFERENCE-ADD1-ARG2, DIFFERENCE-SUB1-ARG2, DIFFERENCE-X-X,
SUB1-ADD1, and SUB1-TYPE-RESTRICTION, and unfolding NUMBERP, EQUAL, SUB1, ADD1,
DIFFERENCE, LESSP, and GCD, to the following three new conjectures:
Case 3. (IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (LESSP (SUB1 A) A)))
(EQUAL (ADD1 A) 1)).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(LESSP (SUB1 A) A)
(LESSP A A))
(EQUAL (GCD A 0) 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(LESSP (SUB1 A) A)
(NOT (LESSP A A)))
(EQUAL (GCD A 1) 1)),
which again simplifies, applying REMAINDER-1-ARG2 and GCD-REMAINDER, and
opening up the functions EQUAL and NUMBERP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
GCD-A-ADD1-A
(PROVE-LEMMA REMAINDER-TIMES-TIMES-HACK
(REWRITE)
(EQUAL (REMAINDER (TIMES B (TIMES A C))
(TIMES A X))
(TIMES A (REMAINDER (TIMES B C) X))))
This simplifies, appealing to the lemmas COMMUTATIVITY2-OF-TIMES and
REMAINDER-TIMES2-INSTANCE, to:
T.
Q.E.D.
[ 0.0 1.4 0.0 ]
REMAINDER-TIMES-TIMES-HACK
(PROVE-LEMMA REMAINDER-PLUS-TIMES-HACK
(REWRITE)
(EQUAL (REMAINDER (PLUS (TIMES A X)
(TIMES B (TIMES C (TIMES A Y))))
(TIMES A Z))
(TIMES A
(REMAINDER (PLUS X (TIMES B (TIMES C Y)))
Z)))
((USE (REMAINDER-TIMES-TIMES-PROOF (Y (PLUS X (TIMES B (TIMES C Y))))
(X A)
(Z Z)))
(DISABLE-THEORY NATURALS)
(ENABLE TIMES-DISTRIBUTES-OVER-PLUS COMMUTATIVITY2-OF-TIMES)))
This formula simplifies, appealing to the lemmas TIMES-DISTRIBUTES-OVER-PLUS
and COMMUTATIVITY2-OF-TIMES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
REMAINDER-PLUS-TIMES-HACK
(DEFN FIB
(X)
(IF (ZEROP X)
0
(IF (EQUAL X 1)
1
(PLUS (FIB (SUB1 (SUB1 X)))
(FIB (SUB1 X))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each recursive call. Hence, FIB is accepted under the
principle of definition. Note that (NUMBERP (FIB X)) is a theorem.
[ 0.0 0.0 0.0 ]
FIB
(PROVE-LEMMA FIB-PLUS
(REWRITE)
(EQUAL (FIB (PLUS J K))
(IF (ZEROP J)
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB J))
(TIMES (FIB (SUB1 J)) (FIB K))))))
This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and
COMMUTATIVITY-OF-TIMES, and expanding the definitions of PLUS and ZEROP, to
the following three new formulas:
Case 3. (IMPLIES (AND (NOT (NUMBERP J))
(NOT (NUMBERP K)))
(EQUAL (FIB 0) (FIB K))).
But this again simplifies, unfolding the definitions of FIB and EQUAL, to:
T.
Case 2. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K)))
(EQUAL (FIB 0) (FIB K))),
which again simplifies, expanding FIB and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J))
(EQUAL (FIB (ADD1 (PLUS K (SUB1 J))))
(PLUS (TIMES (FIB J) (FIB (ADD1 K)))
(TIMES (FIB K) (FIB (SUB1 J)))))).
Applying the lemma SUB1-ELIM, replace J by (ADD1 X) to eliminate (SUB1 J).
We use the type restriction lemma noted when SUB1 was introduced to restrict
the new variable. We would thus like to prove the new goal:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (FIB (ADD1 (PLUS K X)))
(PLUS (TIMES (FIB (ADD1 X)) (FIB (ADD1 K)))
(TIMES (FIB K) (FIB X))))),
which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY-OF-PLUS, to the new goal:
(IMPLIES (NUMBERP X)
(EQUAL (FIB (ADD1 (PLUS K X)))
(PLUS (TIMES (FIB K) (FIB X))
(TIMES (FIB (ADD1 K))
(FIB (ADD1 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:
(EQUAL (FIB (PLUS J K))
(IF (ZEROP J)
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB J))
(TIMES (FIB (SUB1 J)) (FIB K))))),
named *1. Let us appeal to the induction principle. There are four plausible
inductions. They merge into two likely candidate inductions. However, only
one is unflawed. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP J) (p J K))
(IMPLIES (AND (NOT (ZEROP J)) (EQUAL J 1))
(p J K))
(IMPLIES (AND (NOT (ZEROP J))
(NOT (EQUAL J 1))
(p (SUB1 (SUB1 J)) K)
(p (SUB1 J) K))
(p J K))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT J) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme leads to three new goals:
Case 3. (IMPLIES (ZEROP J)
(EQUAL (FIB (PLUS J K))
(IF (ZEROP J)
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB J))
(TIMES (FIB (SUB1 J)) (FIB K)))))),
which simplifies, expanding the functions ZEROP, EQUAL, and PLUS, to two new
conjectures:
Case 3.2.
(IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K)))
(EQUAL (FIB 0) (FIB K))),
which again simplifies, unfolding the functions FIB and EQUAL, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (NUMBERP J))
(NOT (NUMBERP K)))
(EQUAL (FIB 0) (FIB K))),
which again simplifies, opening up FIB and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP J)) (EQUAL J 1))
(EQUAL (FIB (PLUS J K))
(IF (ZEROP J)
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB J))
(TIMES (FIB (SUB1 J)) (FIB K)))))),
which simplifies, applying PLUS-ADD1-ARG1, TIMES-1-ARG1,
COMMUTATIVITY-OF-TIMES, and PLUS-ZERO-ARG2, and expanding the functions
ZEROP, EQUAL, PLUS, FIB, SUB1, and TIMES, to:
(IMPLIES (NOT (NUMBERP K))
(EQUAL (FIB 1) (FIB (ADD1 K)))),
which again simplifies, rewriting with SUB1-TYPE-RESTRICTION, and opening up
the functions FIB and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP J))
(NOT (EQUAL J 1))
(EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K))
(IF (ZEROP (SUB1 (SUB1 J)))
(FIB K)
(PLUS (TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))
(TIMES (FIB (SUB1 (SUB1 (SUB1 J))))
(FIB K)))))
(EQUAL (FIB (PLUS (SUB1 J) K))
(IF (ZEROP (SUB1 J))
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB (SUB1 J)))
(TIMES (FIB (SUB1 (SUB1 J)))
(FIB K))))))
(EQUAL (FIB (PLUS J K))
(IF (ZEROP J)
(FIB K)
(PLUS (TIMES (FIB (ADD1 K)) (FIB J))
(TIMES (FIB (SUB1 J)) (FIB K)))))).
This simplifies, applying EQUAL-SUB1-0, COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY-OF-PLUS, TIMES-DISTRIBUTES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS,
and ASSOCIATIVITY-OF-PLUS, and unfolding ZEROP, PLUS, and FIB, to two new
goals:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL J 1))
(NOT (EQUAL (SUB1 J) 1))
(EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K))
(PLUS (TIMES (FIB K)
(FIB (SUB1 (SUB1 (SUB1 J)))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))))
(EQUAL (FIB (PLUS (SUB1 J) K))
(PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 J))))))
(EQUAL (FIB (ADD1 (PLUS (SUB1 J) K)))
(PLUS (TIMES (FIB K) (FIB (SUB1 J)))
(TIMES (FIB (ADD1 K)) (FIB (SUB1 J)))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))))),
which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS,
EQUAL-SUB1-0, TIMES-DISTRIBUTES-OVER-PLUS, and ASSOCIATIVITY-OF-PLUS, and
unfolding the function FIB, to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL J 1))
(NOT (EQUAL (SUB1 J) 1))
(EQUAL (FIB (PLUS K (SUB1 (SUB1 J))))
(PLUS (TIMES (FIB K)
(FIB (SUB1 (SUB1 (SUB1 J)))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))))
(EQUAL (FIB (PLUS K (SUB1 J)))
(PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 (SUB1 J))))))))
(EQUAL (FIB (ADD1 (PLUS K (SUB1 J))))
(PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J))))
(TIMES (FIB K)
(FIB (SUB1 (SUB1 (SUB1 J)))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 (SUB1 J)))))))).
Applying the lemma SUB1-ELIM, replace J by (ADD1 X) to eliminate (SUB1 J),
X by (ADD1 Z) to eliminate (SUB1 X), and Z by (ADD1 X) to eliminate
(SUB1 Z). We rely upon the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. This produces the following
three new formulas:
Case 1.2.3.
(IMPLIES (AND (EQUAL X 0)
(NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 X) 1))
(NOT (EQUAL X 1))
(EQUAL (FIB (PLUS K (SUB1 X)))
(PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 X))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 X)))))
(EQUAL (FIB (PLUS K X))
(PLUS (TIMES (FIB K) (FIB (SUB1 X)))
(TIMES (FIB (ADD1 K)) (FIB (SUB1 X)))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 X)))))))
(EQUAL (FIB (ADD1 (PLUS K X)))
(PLUS (TIMES (FIB K) (FIB (SUB1 X)))
(TIMES (FIB K) (FIB (SUB1 (SUB1 X))))
(TIMES (FIB (ADD1 K)) (FIB (SUB1 X)))
(TIMES (FIB (ADD1 K)) (FIB (SUB1 X)))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 X))))))).
This further simplifies, trivially, to:
T.
Case 1.2.2.
(IMPLIES (AND (EQUAL Z 0)
(NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 1))
(NOT (EQUAL (ADD1 Z) 1))
(EQUAL (FIB (PLUS K Z))
(PLUS (TIMES (FIB K) (FIB (SUB1 Z)))
(TIMES (FIB (ADD1 K)) (FIB Z))))
(EQUAL (FIB (PLUS K (ADD1 Z)))
(PLUS (TIMES (FIB K) (FIB Z))
(TIMES (FIB (ADD1 K)) (FIB Z))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 Z))))))
(EQUAL (FIB (ADD1 (PLUS K (ADD1 Z))))
(PLUS (TIMES (FIB K) (FIB Z))
(TIMES (FIB K) (FIB (SUB1 Z)))
(TIMES (FIB (ADD1 K)) (FIB Z))
(TIMES (FIB (ADD1 K)) (FIB Z))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 Z)))))).
This further simplifies, trivially, to:
T.
Case 1.2.1.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 (ADD1 X)) 0))
(NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 0))
(NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 1))
(NOT (EQUAL (ADD1 (ADD1 X)) 1))
(EQUAL (FIB (PLUS K (ADD1 X)))
(PLUS (TIMES (FIB K) (FIB X))
(TIMES (FIB (ADD1 K))
(FIB (ADD1 X)))))
(EQUAL (FIB (PLUS K (ADD1 (ADD1 X))))
(PLUS (TIMES (FIB K) (FIB (ADD1 X)))
(TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))
(TIMES (FIB (ADD1 K)) (FIB X)))))
(EQUAL (FIB (ADD1 (PLUS K (ADD1 (ADD1 X)))))
(PLUS (TIMES (FIB K) (FIB (ADD1 X)))
(TIMES (FIB K) (FIB X))
(TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))
(TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))
(TIMES (FIB (ADD1 K)) (FIB X))))).
But this further simplifies, appealing to the lemmas ADD1-EQUAL,
PLUS-ADD1-ARG2, SUB1-ADD1, COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS,
and COMMUTATIVITY2-OF-PLUS, and opening up NUMBERP and FIB, to:
(IMPLIES (AND (NUMBERP X)
(EQUAL (FIB (ADD1 (PLUS K X)))
(PLUS (TIMES (FIB K) (FIB X))
(TIMES (FIB (ADD1 K))
(FIB (ADD1 X)))))
(EQUAL (PLUS (FIB (PLUS K X))
(FIB (ADD1 (PLUS K X))))
(PLUS (TIMES (FIB K) (FIB (ADD1 X)))
(TIMES (FIB X) (FIB (ADD1 K)))
(TIMES (FIB (ADD1 K))
(FIB (ADD1 X))))))
(EQUAL (PLUS (FIB (PLUS K X))
(FIB (ADD1 (PLUS K X)))
(FIB (ADD1 (PLUS K X))))
(PLUS (TIMES (FIB K) (FIB X))
(TIMES (FIB K) (FIB (ADD1 X)))
(TIMES (FIB X) (FIB (ADD1 K)))
(TIMES (FIB (ADD1 K)) (FIB (ADD1 X)))
(TIMES (FIB (ADD1 K))
(FIB (ADD1 X)))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL J 1))
(EQUAL (SUB1 J) 1)
(EQUAL (FIB (PLUS (SUB1 (SUB1 J)) K))
(FIB K))
(EQUAL (FIB (PLUS (SUB1 J) K))
(PLUS (TIMES (FIB K) (FIB (SUB1 (SUB1 J))))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 J))))))
(EQUAL (FIB (ADD1 (PLUS (SUB1 J) K)))
(PLUS (TIMES (FIB K) (FIB (SUB1 J)))
(TIMES (FIB (ADD1 K)) (FIB (SUB1 J)))
(TIMES (FIB (ADD1 K))
(FIB (SUB1 (SUB1 J))))))),
which again simplifies, applying PLUS-ADD1-ARG1, TIMES-1-ARG1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, ADD1-EQUAL, and PLUS-ZERO-ARG2, and
expanding the definitions of SUB1, EQUAL, PLUS, FIB, TIMES, NUMBERP, and
ZEROP, to the following two new conjectures:
Case 1.1.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL J 1))
(EQUAL (SUB1 J) 1)
(EQUAL (FIB 0) (FIB K))
(EQUAL (FIB 1) (FIB (ADD1 K)))
(NOT (NUMBERP K)))
(EQUAL (PLUS (FIB 0) (FIB 1)) 1)).
But this again simplifies, applying SUB1-TYPE-RESTRICTION, and expanding
the definitions of FIB, EQUAL, and PLUS, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL J 1))
(EQUAL (SUB1 J) 1)
(EQUAL (FIB 0) (FIB K))
(EQUAL (FIB 1) (FIB (ADD1 K)))
(NUMBERP K))
(EQUAL (PLUS (FIB K) (FIB (ADD1 K)))
1)).
However this again simplifies, opening up FIB, PLUS, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.8 0.0 ]
FIB-PLUS
(PROVE-LEMMA GCD-FIB-NEXT-FIB
(REWRITE)
(EQUAL (GCD (FIB N) (FIB (ADD1 N)))
1))
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-FIB-NEXT-FIB could!
Give the conjecture the name *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))
(IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(p N))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(p (SUB1 N))
(p (SUB1 (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
generates three new goals:
Case 3. (IMPLIES (ZEROP N)
(EQUAL (GCD (FIB N) (FIB (ADD1 N)))
1)),
which simplifies, applying SUB1-TYPE-RESTRICTION, and unfolding the
functions ZEROP, FIB, ADD1, GCD, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(EQUAL (GCD (FIB N) (FIB (ADD1 N)))
1)).
This simplifies, opening up ZEROP, FIB, GCD, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(EQUAL (GCD (FIB (SUB1 N))
(FIB (ADD1 (SUB1 N))))
1)
(EQUAL (GCD (FIB (SUB1 (SUB1 N)))
(FIB (ADD1 (SUB1 (SUB1 N)))))
1))
(EQUAL (GCD (FIB N) (FIB (ADD1 N)))
1)).
This simplifies, applying ADD1-SUB1, COMMUTATIVITY-OF-PLUS,
GCD-PLUS-INSTANCE, EQUAL-SUB1-0, COMMUTATIVITY-OF-GCD, SUB1-ADD1, ADD1-EQUAL,
REMAINDER-X-X, and GCD-PLUS, and unfolding the definitions of ZEROP, FIB,
EQUAL, and NUMBERP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
GCD-FIB-NEXT-FIB
(PROVE-LEMMA GCD-FIB
(REWRITE)
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A B)))
((DISABLE GCD-DIFFERENCE2 REMAINDER-DIFFERENCE1)))
WARNING: the newly proposed lemma, GCD-FIB, could be applied whenever the
previously added lemma GCD-FIB-NEXT-FIB could.
WARNING: the previously added lemma, COMMUTATIVITY-OF-GCD, could be applied
whenever the newly proposed GCD-FIB could!
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture, all 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 A) (p A B))
(IMPLIES (AND (NOT (ZEROP A)) (ZEROP B))
(p A B))
(IMPLIES (AND (NOT (ZEROP A))
(NOT (ZEROP B))
(LESSP A B)
(p A (DIFFERENCE B A)))
(p A B))
(IMPLIES (AND (NOT (ZEROP A))
(NOT (ZEROP B))
(NOT (LESSP A B))
(p (DIFFERENCE A B) B))
(p A B))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, and ADD1-EQUAL,
and the definitions of ORDINALP, FIX, LESSP, ORD-LESSP, and ZEROP can be used
to prove that the measure (CONS (ADD1 A) (FIX B)) decreases according to the
well-founded relation ORD-LESSP in each induction step of the scheme. The
above induction scheme leads to four new goals:
Case 4. (IMPLIES (ZEROP A)
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A B)))),
which simplifies, applying the lemmas GCD-REMAINDER and
REMAINDER-OF-NON-NUMBER, and opening up the definitions of ZEROP, FIB,
REMAINDER, NUMBERP, EQUAL, and LESSP, to two new formulas:
Case 4.2.
(IMPLIES (AND (EQUAL A 0) (NOT (NUMBERP B)))
(EQUAL (FIB B) (FIB 0))),
which again simplifies, opening up the definitions of FIB and EQUAL, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (NUMBERP B)))
(EQUAL (FIB B) (FIB 0))),
which again simplifies, unfolding the functions FIB and EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A B)))),
which simplifies, rewriting with the lemmas GCD-REMAINDER, REMAINDER-NOOP,
and REMAINDER-OF-NON-NUMBER, and expanding the functions ZEROP, FIB,
REMAINDER, NUMBERP, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP A))
(NOT (ZEROP B))
(LESSP A B)
(EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A)))
(FIB (GCD A (DIFFERENCE B A)))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A B)))),
which simplifies, opening up ZEROP and GCD, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL B 0))
(NUMBERP B)
(LESSP A B)
(EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A)))
(FIB (GCD A (DIFFERENCE B A)))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A (DIFFERENCE B A))))).
Appealing to the lemma DIFFERENCE-ELIM, we now replace B by (PLUS A X) to
eliminate (DIFFERENCE B A). We employ the type restriction lemma noted when
DIFFERENCE was introduced to constrain the new variable. The result is two
new formulas:
Case 2.2.
(IMPLIES (AND (LESSP B A)
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL B 0))
(NUMBERP B)
(LESSP A B)
(EQUAL (GCD (FIB A) (FIB (DIFFERENCE B A)))
(FIB (GCD A (DIFFERENCE B A)))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A (DIFFERENCE B A))))),
which further simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP X)
(NOT (LESSP (PLUS A X) A))
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL (PLUS A X) 0))
(LESSP A (PLUS A X))
(EQUAL (GCD (FIB A) (FIB X))
(FIB (GCD A X))))
(EQUAL (GCD (FIB A) (FIB (PLUS A X)))
(FIB (GCD A X)))),
which further simplifies, rewriting with CORRECTNESS-OF-CANCEL-LESSP-PLUS,
EQUAL-PLUS-0, COMMUTATIVITY-OF-TIMES, FIB-PLUS, REMAINDER-TIMES1-INSTANCE,
and GCD-PLUS, and expanding the definitions of FIX, ZEROP, NOT, and EQUAL,
to:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL X 0))
(EQUAL (GCD (FIB A) (FIB X))
(FIB (GCD A X))))
(EQUAL (GCD (FIB A)
(TIMES (FIB X) (FIB (SUB1 A))))
(FIB (GCD A X)))).
Applying the lemma SUB1-ELIM, replace A by (ADD1 Z) to eliminate (SUB1 A).
We employ the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We thus obtain the new conjecture:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL X 0))
(EQUAL (GCD (FIB (ADD1 Z)) (FIB X))
(FIB (GCD (ADD1 Z) X))))
(EQUAL (GCD (FIB (ADD1 Z))
(TIMES (FIB X) (FIB Z)))
(FIB (GCD (ADD1 Z) X)))),
which further simplifies, applying COMMUTATIVITY-OF-GCD, GCD-FIB-NEXT-FIB,
and GCD-TIMES-EASY, and unfolding EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP A))
(NOT (ZEROP B))
(NOT (LESSP A B))
(EQUAL (GCD (FIB (DIFFERENCE A B)) (FIB B))
(FIB (GCD (DIFFERENCE A B) B))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD A B)))).
This simplifies, appealing to the lemma COMMUTATIVITY-OF-GCD, and expanding
the definitions of ZEROP and GCD, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (LESSP A B))
(EQUAL (GCD (FIB B) (FIB (DIFFERENCE A B)))
(FIB (GCD (DIFFERENCE A B) B))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD (DIFFERENCE A B) B)))),
which further simplifies, rewriting with COMMUTATIVITY-OF-GCD, to the new
conjecture:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (LESSP A B))
(EQUAL (GCD (FIB B) (FIB (DIFFERENCE A B)))
(FIB (GCD B (DIFFERENCE A B)))))
(EQUAL (GCD (FIB A) (FIB B))
(FIB (GCD B (DIFFERENCE A B))))).
Applying the lemma DIFFERENCE-ELIM, replace A by (PLUS B X) to eliminate
(DIFFERENCE A B). We use the type restriction lemma noted when DIFFERENCE
was introduced to restrict the new variable. We thus obtain:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (PLUS B X) 0))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (LESSP (PLUS B X) B))
(EQUAL (GCD (FIB B) (FIB X))
(FIB (GCD B X))))
(EQUAL (GCD (FIB (PLUS B X)) (FIB B))
(FIB (GCD B X)))),
which further simplifies, applying EQUAL-PLUS-0,
CORRECTNESS-OF-CANCEL-LESSP-PLUS, COMMUTATIVITY-OF-TIMES, FIB-PLUS,
REMAINDER-TIMES1-INSTANCE, and GCD-PLUS, and unfolding EQUAL, to:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL B 0))
(NUMBERP B)
(EQUAL (GCD (FIB B) (FIB X))
(FIB (GCD B X))))
(EQUAL (GCD (FIB B)
(TIMES (FIB X) (FIB (SUB1 B))))
(FIB (GCD B X)))).
Applying the lemma SUB1-ELIM, replace B by (ADD1 Z) to eliminate (SUB1 B).
We rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (GCD (FIB (ADD1 Z)) (FIB X))
(FIB (GCD (ADD1 Z) X))))
(EQUAL (GCD (FIB (ADD1 Z))
(TIMES (FIB X) (FIB Z)))
(FIB (GCD (ADD1 Z) X)))),
which finally simplifies, applying the lemmas COMMUTATIVITY-OF-GCD,
GCD-FIB-NEXT-FIB, and GCD-TIMES-EASY, and opening up the function EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 6.2 0.0 ]
GCD-FIB
(PROVE-LEMMA EQUAL-FIB-CONSTANT
(REWRITE)
(AND (EQUAL (EQUAL (FIB A) 0) (ZEROP A))
(EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2)))))
WARNING: Note that the proposed lemma EQUAL-FIB-CONSTANT is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
This conjecture can be simplified, using the abbreviation AND, to two new
goals:
Case 2. (EQUAL (EQUAL (FIB A) 0) (ZEROP A)),
which simplifies, unfolding ZEROP, to three new goals:
Case 2.3.
(IMPLIES (NOT (EQUAL (FIB A) 0))
(NUMBERP A)),
which again simplifies, unfolding the functions FIB and EQUAL, to:
T.
Case 2.2.
(IMPLIES (NOT (EQUAL (FIB A) 0))
(NOT (EQUAL A 0))),
which again simplifies, opening up FIB and EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL (FIB A) 0)
(NOT (EQUAL A 0)))
(NOT (NUMBERP A))),
which we will name *1.
Case 1. (EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2))).
This simplifies, unfolding the function OR, to the following three new
conjectures:
Case 1.3.
(IMPLIES (NOT (EQUAL (FIB A) 1))
(NOT (EQUAL A 1))).
However this again simplifies, unfolding FIB and EQUAL, to:
T.
Case 1.2.
(IMPLIES (NOT (EQUAL (FIB A) 1))
(NOT (EQUAL A 2))),
which again simplifies, expanding the functions FIB and EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (EQUAL (FIB A) 1)
(NOT (EQUAL A 1)))
(EQUAL (EQUAL A 2) T)),
which again simplifies, obviously, to the new conjecture:
(IMPLIES (AND (EQUAL (FIB A) 1)
(NOT (EQUAL A 1)))
(EQUAL A 2)),
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:
(AND (EQUAL (EQUAL (FIB A) 0) (ZEROP A))
(EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2)))),
named *1. Let us appeal to the induction principle. Two inductions are
suggested by terms in the conjecture. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP A) (p A))
(IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1))
(p A))
(IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(p (SUB1 A))
(p (SUB1 (SUB1 A))))
(p A))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT A) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to six new formulas:
Case 6. (IMPLIES (ZEROP A)
(EQUAL (EQUAL (FIB A) 0) (ZEROP A))),
which simplifies, expanding the definitions of ZEROP, FIB, and EQUAL, to:
T.
Case 5. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1))
(EQUAL (EQUAL (FIB A) 0) (ZEROP A))),
which simplifies, expanding ZEROP, FIB, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(EQUAL (EQUAL (FIB (SUB1 A)) 0)
(ZEROP (SUB1 A)))
(EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0)
(ZEROP (SUB1 (SUB1 A))))
(EQUAL (EQUAL (FIB (SUB1 A)) 1)
(OR (EQUAL (SUB1 A) 1)
(EQUAL (SUB1 A) 2)))
(EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 1)
(OR (EQUAL (SUB1 (SUB1 A)) 1)
(EQUAL (SUB1 (SUB1 A)) 2))))
(EQUAL (EQUAL (FIB A) 0) (ZEROP A))),
which simplifies, applying the lemmas EQUAL-SUB1-0, PLUS-ADD1-ARG1,
COMMUTATIVITY-OF-PLUS, EQUAL-PLUS-0, PLUS-ZERO-ARG2, and PLUS-ADD1-ARG2, and
opening up the definitions of ZEROP, OR, FIB, EQUAL, PLUS, SUB1, and NUMBERP,
to:
T.
Case 3. (IMPLIES (ZEROP A)
(EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2)))),
which simplifies, expanding the functions ZEROP, FIB, EQUAL, and OR, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1))
(EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2)))),
which simplifies, expanding the functions ZEROP, FIB, EQUAL, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(EQUAL (EQUAL (FIB (SUB1 A)) 0)
(ZEROP (SUB1 A)))
(EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0)
(ZEROP (SUB1 (SUB1 A))))
(EQUAL (EQUAL (FIB (SUB1 A)) 1)
(OR (EQUAL (SUB1 A) 1)
(EQUAL (SUB1 A) 2)))
(EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 1)
(OR (EQUAL (SUB1 (SUB1 A)) 1)
(EQUAL (SUB1 (SUB1 A)) 2))))
(EQUAL (EQUAL (FIB A) 1)
(OR (EQUAL A 1) (EQUAL A 2)))),
which simplifies, applying EQUAL-SUB1-0, PLUS-ADD1-ARG1, ADD1-EQUAL,
COMMUTATIVITY-OF-PLUS, PLUS-ZERO-ARG2, and PLUS-ADD1-ARG2, and expanding the
functions ZEROP, OR, FIB, EQUAL, PLUS, NUMBERP, and SUB1, to the following
six new conjectures:
Case 1.6.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(NOT (EQUAL (SUB1 A) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0))
(NOT (EQUAL (SUB1 A) 2))
(NOT (EQUAL (FIB (SUB1 A)) 1))
(EQUAL (FIB (SUB1 (SUB1 A))) 1)
(EQUAL (EQUAL (SUB1 (SUB1 A)) 2) T))
(NOT (EQUAL A 2))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(NOT (EQUAL (SUB1 A) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0))
(NOT (EQUAL (SUB1 A) 2))
(NOT (EQUAL (FIB (SUB1 A)) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(NOT (EQUAL (SUB1 (SUB1 A)) 2))
(NOT (EQUAL A 2)))
(NOT (EQUAL (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
1))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(NOT (EQUAL (SUB1 A) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0))
(NOT (EQUAL (SUB1 A) 2))
(NOT (EQUAL (FIB (SUB1 A)) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(NOT (EQUAL (SUB1 (SUB1 A)) 2))
(EQUAL A 2))
(EQUAL (EQUAL (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
1)
T)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(NOT (EQUAL (SUB1 A) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0))
(NOT (EQUAL (SUB1 A) 2))
(NOT (EQUAL (FIB (SUB1 A)) 1))
(EQUAL (FIB (SUB1 (SUB1 A))) 1)
(EQUAL (SUB1 (SUB1 A)) 1))
(NOT (EQUAL A 2))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (SUB1 2) 0)
(NOT (EQUAL 2 0))
(NUMBERP 2)
(NOT (EQUAL 2 1))
(NOT (EQUAL (FIB (SUB1 2)) 0))
(NOT (EQUAL (SUB1 2) 1))
(NOT (EQUAL 1 0))
(NOT (EQUAL (SUB1 2) 2))
(NOT (EQUAL (FIB (SUB1 2)) 1))
(EQUAL (FIB 1) 1))
(NOT (EQUAL (SUB1 (SUB1 2)) 1))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(NOT (EQUAL (SUB1 A) 1))
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 0))
(EQUAL (SUB1 A) 2)
(EQUAL (EQUAL (FIB (SUB1 A)) 1) T)
(EQUAL (FIB (SUB1 (SUB1 A))) 1))
(NOT (EQUAL A 2))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (EQUAL (FIB (SUB1 A)) 0))
(EQUAL (SUB1 A) 1)
(EQUAL (EQUAL (FIB (SUB1 (SUB1 A))) 0)
T)
(EQUAL (FIB (SUB1 A)) 1)
(NOT (EQUAL (FIB (SUB1 (SUB1 A))) 1)))
(EQUAL A 2)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
EQUAL-FIB-CONSTANT
(PROVE-LEMMA FIB-SMALL
(REWRITE)
(IMPLIES (LESSP A 3)
(EQUAL (FIB A) (IF (ZEROP A) 0 1))))
This formula simplifies, opening up ZEROP, to the following three new formulas:
Case 3. (IMPLIES (AND (LESSP A 3) (NOT (NUMBERP A)))
(EQUAL (FIB A) 0)).
This again simplifies, opening up the functions NUMBERP, EQUAL, LESSP, and
FIB, to:
T.
Case 2. (IMPLIES (AND (LESSP A 3) (EQUAL A 0))
(EQUAL (FIB A) 0)),
which again simplifies, unfolding the functions LESSP, FIB, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (LESSP A 3)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (FIB A) 1)),
which again simplifies, applying EQUAL-FIB-CONSTANT, to:
(IMPLIES (AND (LESSP A 3)
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1)))
(EQUAL A 2)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FIB-SMALL
(DEFN DOUBLE-FIB-INDUCTION
(A B)
(IF (OR (LESSP A 3) (LESSP B 3))
T
(AND (DOUBLE-FIB-INDUCTION (SUB1 A)
(SUB1 B))
(DOUBLE-FIB-INDUCTION (SUB1 (SUB1 A))
(SUB1 (SUB1 B))))))
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of OR establish that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each recursive call. Hence,
DOUBLE-FIB-INDUCTION is accepted under the definitional principle. The
definition of DOUBLE-FIB-INDUCTION can be justified in another way. Linear
arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition
of OR inform us that the measure (COUNT B) decreases according to the
well-founded relation LESSP in each recursive call. From the definition we
can conclude that (TRUEP (DOUBLE-FIB-INDUCTION A B)) is a theorem.
[ 0.0 0.0 0.0 ]
DOUBLE-FIB-INDUCTION
(PROVE-LEMMA LESSP-FIB-FIB
(REWRITE)
(EQUAL (LESSP (FIB A) (FIB B))
(AND (LESSP A B)
(NOT (AND (EQUAL A 1) (EQUAL B 2)))))
((INDUCT (DOUBLE-FIB-INDUCTION A B))))
This formula can be simplified, using the abbreviations NOT, OR, and AND, to
the following two new formulas:
Case 2. (IMPLIES (OR (LESSP A 3) (LESSP B 3))
(EQUAL (LESSP (FIB A) (FIB B))
(AND (LESSP A B)
(NOT (AND (EQUAL A 1) (EQUAL B 2)))))).
This simplifies, applying FIB-SMALL, and expanding the definitions of OR,
AND, and NOT, to 24 new formulas:
Case 2.24.
(IMPLIES (AND (LESSP A 3)
(EQUAL A 1)
(EQUAL B 2)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP 1 (FIB B)) F)),
which again simplifies, expanding the definitions of LESSP, EQUAL, NUMBERP,
and FIB, to:
T.
Case 2.23.
(IMPLIES (AND (LESSP A 3)
(NOT (LESSP A B))
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP 1 (FIB B)) F)),
which again simplifies, using linear arithmetic and rewriting with
FIB-SMALL and LESSP-1-HACK, to:
T.
Case 2.22.
(IMPLIES (AND (LESSP A 3)
(NOT (LESSP A B))
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 (FIB B)) F)).
However this again simplifies, using linear arithmetic, rewriting with
FIB-SMALL, and unfolding NUMBERP, EQUAL, LESSP, and FIB, to:
T.
Case 2.21.
(IMPLIES (AND (LESSP A 3)
(NOT (LESSP A B))
(EQUAL A 0))
(EQUAL (LESSP 0 (FIB B)) F)).
However this again simplifies, using linear arithmetic, rewriting with the
lemma FIB-SMALL, and unfolding the definitions of LESSP, EQUAL, and FIB,
to:
T.
Case 2.20.
(IMPLIES (AND (LESSP A 3)
(EQUAL A 1)
(EQUAL B 2)
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 (FIB B)) F)),
which again simplifies, trivially, to:
T.
Case 2.19.
(IMPLIES (AND (LESSP A 3)
(EQUAL A 1)
(EQUAL B 2)
(EQUAL A 0))
(EQUAL (LESSP 0 (FIB B)) F)).
However this again simplifies, using linear arithmetic, to:
T.
Case 2.18.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP 1 (FIB B)) T)),
which again simplifies, applying EQUAL-FIB-CONSTANT and LESSP-1-HACK, to
the following three new goals:
Case 2.18.3.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (EQUAL A 0))
(NUMBERP A))
(NOT (EQUAL B 0))).
This again simplifies, using linear arithmetic, to:
T.
Case 2.18.2.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (EQUAL A 0))
(NUMBERP A))
(NUMBERP B)),
which again simplifies, expanding the definition of LESSP, to:
T.
Case 2.18.1.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (EQUAL A 0))
(NUMBERP A))
(NOT (EQUAL B 1))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.17.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP 1 (FIB B)) T)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP 2 3)
(LESSP 2 B)
(NOT (EQUAL 2 1))
(NOT (EQUAL 2 0))
(NUMBERP 2))
(EQUAL (LESSP 1 (FIB B)) T)).
This again simplifies, applying LESSP-1-HACK, EQUAL-SUB1-0, and
EQUAL-FIB-CONSTANT, and unfolding LESSP, SUB1, NUMBERP, and EQUAL, to:
(IMPLIES (AND (NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (EQUAL (SUB1 B) 1)))
(NOT (EQUAL B 2))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.16.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 (FIB B)) T)),
which again simplifies, appealing to the lemma EQUAL-FIB-CONSTANT, and
unfolding the functions NUMBERP, EQUAL, and LESSP, to:
T.
Case 2.15.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL A 1))
(EQUAL A 0))
(EQUAL (LESSP 0 (FIB B)) T)),
which again simplifies, applying EQUAL-FIB-CONSTANT, and expanding the
definitions of LESSP and EQUAL, to:
T.
Case 2.14.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 (FIB B)) T)).
This again simplifies, applying EQUAL-FIB-CONSTANT, and expanding NUMBERP,
EQUAL, and LESSP, to:
T.
Case 2.13.
(IMPLIES (AND (LESSP A 3)
(LESSP A B)
(NOT (EQUAL B 2))
(EQUAL A 0))
(EQUAL (LESSP 0 (FIB B)) T)).
But this again simplifies, applying EQUAL-FIB-CONSTANT, and unfolding the
functions LESSP and EQUAL, to:
T.
Case 2.12.
(IMPLIES (AND (LESSP B 3)
(EQUAL A 1)
(EQUAL B 2)
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (FIB A) 1) F)).
But this again simplifies, expanding LESSP, EQUAL, NUMBERP, and FIB, to:
T.
Case 2.11.
(IMPLIES (AND (LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (FIB A) 1) F)),
which again simplifies, clearly, to:
(IMPLIES (AND (LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which we will name *1.
Case 2.10.
(IMPLIES (AND (LESSP B 3)
(NOT (LESSP A B))
(NOT (NUMBERP B)))
(EQUAL (LESSP (FIB A) 0) F)).
But this again simplifies, expanding NUMBERP, EQUAL, and LESSP, to:
T.
Case 2.9.
(IMPLIES (AND (LESSP B 3)
(NOT (LESSP A B))
(EQUAL B 0))
(EQUAL (LESSP (FIB A) 0) F)),
which again simplifies, expanding LESSP and EQUAL, to:
T.
Case 2.8.
(IMPLIES (AND (LESSP B 3)
(EQUAL A 1)
(EQUAL B 2)
(NOT (NUMBERP B)))
(EQUAL (LESSP (FIB A) 0) F)),
which again simplifies, obviously, to:
T.
Case 2.7.
(IMPLIES (AND (LESSP B 3)
(EQUAL A 1)
(EQUAL B 2)
(EQUAL B 0))
(EQUAL (LESSP (FIB A) 0) F)).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.6.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (FIB A) 1) T)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP 1 3)
(LESSP A 1)
(NOT (EQUAL 1 2))
(NOT (EQUAL 1 0))
(NUMBERP 1))
(EQUAL (LESSP (FIB A) 1) T)).
However this again simplifies, using linear arithmetic, rewriting with the
lemma FIB-SMALL, and expanding the definitions of LESSP, EQUAL, and
NUMBERP, to three new conjectures:
Case 2.6.3.
(IMPLIES (AND (LESSP A 1)
(NOT (EQUAL A 0))
(NUMBERP A))
(LESSP 1 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.6.2.
(IMPLIES (AND (LESSP A 1) (EQUAL A 0))
(LESSP 0 1)),
which again simplifies, trivially, to:
T.
Case 2.6.1.
(IMPLIES (AND (LESSP A 1) (NOT (NUMBERP A)))
(LESSP 0 1)).
This again simplifies, using linear arithmetic, to:
T.
Case 2.5.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (EQUAL B 0))
(NUMBERP B))
(EQUAL (LESSP (FIB A) 1) T)),
which again simplifies, using linear arithmetic and rewriting with
FIB-SMALL, to the following three new formulas:
Case 2.5.3.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (NUMBERP A)))
(EQUAL (LESSP (FIB A) 1) T)).
But this again simplifies, using linear arithmetic, rewriting with
FIB-SMALL, and expanding the definitions of LESSP and EQUAL, to:
T.
Case 2.5.2.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A 0)))
(LESSP 1 1)).
This again simplifies, using linear arithmetic, to:
T.
Case 2.5.1.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NUMBERP A)
(EQUAL A 0))
(LESSP 0 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.4.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(NOT (NUMBERP B)))
(EQUAL (LESSP (FIB A) 0) T)),
which again simplifies, unfolding the functions NUMBERP, EQUAL, and LESSP,
to:
T.
Case 2.3.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL A 1))
(EQUAL B 0))
(EQUAL (LESSP (FIB A) 0) T)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL B 2))
(NOT (NUMBERP B)))
(EQUAL (LESSP (FIB A) 0) T)),
which again simplifies, unfolding the functions NUMBERP, EQUAL, and LESSP,
to:
T.
Case 2.1.
(IMPLIES (AND (LESSP B 3)
(LESSP A B)
(NOT (EQUAL B 2))
(EQUAL B 0))
(EQUAL (LESSP (FIB A) 0) T)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP A 3))
(NOT (LESSP B 3))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
(AND (LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (AND (EQUAL (SUB1 (SUB1 A)) 1)
(EQUAL (SUB1 (SUB1 B)) 2)))))
(EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))
(AND (LESSP (SUB1 A) (SUB1 B))
(NOT (AND (EQUAL (SUB1 A) 1)
(EQUAL (SUB1 B) 2))))))
(EQUAL (LESSP (FIB A) (FIB B))
(AND (LESSP A B)
(NOT (AND (EQUAL A 1) (EQUAL B 2)))))),
which simplifies, applying EQUAL-SUB1-0, FIB-SMALL, LESSP-1-HACK,
PLUS-ADD1-ARG1, and COMMUTATIVITY-OF-PLUS, and expanding the definitions of
SUB1, NUMBERP, EQUAL, LESSP, AND, NOT, PLUS, FIB, and ADD1, to the following
five new formulas:
Case 1.5.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(NOT (LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B))))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
F)
(NOT (LESSP (FIB (SUB1 A))
(FIB (SUB1 B)))))
(NOT (LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B))))))).
This again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(NOT (LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B))))
(NOT (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B)))))
(NOT (LESSP (FIB (SUB1 A))
(FIB (SUB1 B)))))
(NOT (LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 B)) 2))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
T)
(NOT (EQUAL (SUB1 A) 1))
(EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))
T))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 B)) 2))
(LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
(NOT (EQUAL (SUB1 A) 1))
(LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 B)) 2))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
T)
(NOT (EQUAL (SUB1 B) 2))
(EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))
T))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 B)) 2))
(LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
(NOT (EQUAL (SUB1 B) 2))
(LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
T)
(NOT (EQUAL (SUB1 A) 1))
(EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))
T))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
(NOT (EQUAL (SUB1 A) 1))
(LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(EQUAL (LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
T)
(NOT (EQUAL (SUB1 B) 2))
(EQUAL (LESSP (FIB (SUB1 A)) (FIB (SUB1 B)))
T))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (SUB1 (SUB1 A)) 1))
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (EQUAL B 1))
(NOT (LESSP (SUB1 (SUB1 B)) 1))
(LESSP (SUB1 (SUB1 A))
(SUB1 (SUB1 B)))
(NOT (EQUAL (SUB1 (SUB1 A)) 1))
(LESSP (FIB (SUB1 (SUB1 A)))
(FIB (SUB1 (SUB1 B))))
(NOT (EQUAL (SUB1 B) 2))
(LESSP (FIB (SUB1 A)) (FIB (SUB1 B))))
(LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
(PLUS (FIB (SUB1 B))
(FIB (SUB1 (SUB1 B)))))),
which again simplifies, using linear arithmetic, to:
T.
So next consider:
(IMPLIES (AND (LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which we named *1 above. We will try to prove it by induction. The recursive
terms in the conjecture suggest four inductions. However, they merge into one
likely candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP A) (p A B))
(IMPLIES (AND (NOT (ZEROP A)) (EQUAL A 1))
(p A B))
(IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(p (SUB1 (SUB1 A)) B)
(p (SUB1 A) (SUB1 B)))
(p A B))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT A) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for B. The above induction scheme
produces the following ten new conjectures:
Case 10.(IMPLIES (AND (ZEROP A)
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))).
This simplifies, expanding the definitions of ZEROP, EQUAL, and LESSP, to:
T.
Case 9. (IMPLIES (AND (NOT (ZEROP A))
(EQUAL A 1)
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (ZEROP 1))
(LESSP 1 3)
(NOT (LESSP 1 1))
(NOT (EQUAL 1 0))
(NUMBERP 1))
(NOT (LESSP (FIB 1) 1))),
which again simplifies, opening up ZEROP, LESSP, EQUAL, NUMBERP, and FIB, to:
T.
Case 8. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(NOT (LESSP (SUB1 B) 3))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(NOT (LESSP (SUB1 B) 3))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(LESSP (SUB1 A) (SUB1 B))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(LESSP (SUB1 A) (SUB1 B))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(EQUAL (SUB1 B) 0)
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, using linear arithmetic, to two new formulas:
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (ZEROP A))
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(EQUAL (SUB1 B) 0)
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which again simplifies, unfolding the function ZEROP, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP A)
(NOT (ZEROP 2))
(NOT (EQUAL 2 1))
(LESSP (SUB1 (SUB1 2)) B)
(EQUAL (SUB1 B) 0)
(LESSP B 3)
(NOT (LESSP 2 B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB 2) 1))),
which again simplifies, applying EQUAL-SUB1-0, and expanding ZEROP, EQUAL,
SUB1, LESSP, NUMBERP, and FIB, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(EQUAL (SUB1 B) 0)
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))).
This simplifies, appealing to the lemmas EQUAL-SUB1-0 and
COMMUTATIVITY-OF-PLUS, and unfolding the definitions of ZEROP, SUB1, NUMBERP,
EQUAL, LESSP, and FIB, to the new goal:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(EQUAL B 1)
(LESSP B 3))
(NOT (LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
1))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(NOT (LESSP (FIB (SUB1 A)) 1))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding the
definitions of ZEROP, LESSP, and FIB, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(LESSP (SUB1 (SUB1 A)) B)
(NOT (LESSP (FIB (SUB1 A)) 1))
(LESSP B 3)
(NOT (LESSP (SUB1 A) (SUB1 B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
1))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP A))
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(NOT (LESSP (FIB (SUB1 A)) 1))
(LESSP B 3)
(NOT (LESSP A B))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (FIB A) 1))),
which simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and
unfolding the functions ZEROP, LESSP, and FIB, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL A 1))
(NOT (LESSP (FIB (SUB1 (SUB1 A))) 1))
(NOT (LESSP (FIB (SUB1 A)) 1))
(LESSP B 3)
(NOT (LESSP (SUB1 A) (SUB1 B)))
(NOT (EQUAL B 0))
(NUMBERP B))
(NOT (LESSP (PLUS (FIB (SUB1 A))
(FIB (SUB1 (SUB1 A))))
1))).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 1.4 0.1 ]
LESSP-FIB-FIB
(PROVE-LEMMA REMAINDER-FIB-FIB-0
(REWRITE)
(EQUAL (EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(OR (EQUAL (REMAINDER A B) 0)
(EQUAL B 2)))
((USE (EQUAL-REMAINDER-GCD-0-PROOF (A (FIB B))
(B (FIB A))))
(DISABLE EQUAL-REMAINDER-GCD-0 GCD-REMAINDER)))
This formula can be simplified, using the abbreviation GCD-FIB, to the new
conjecture:
(IMPLIES (EQUAL (EQUAL (REMAINDER (FIB (GCD B A)) (FIB B))
0)
(EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(EQUAL (EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(OR (EQUAL (REMAINDER A B) 0)
(EQUAL B 2)))),
which simplifies, rewriting with COMMUTATIVITY-OF-GCD, and opening up OR and
EQUAL, to the following three new conjectures:
Case 3. (IMPLIES (AND (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)))
(NOT (EQUAL (REMAINDER A B) 0))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We
rely upon LESSP-REMAINDER, 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 3.4.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)))
(NOT (EQUAL (REMAINDER A B) 0))),
which further simplifies, using linear arithmetic, rewriting with the
lemmas FIB-SMALL and EQUAL-FIB-CONSTANT, and expanding the definitions of
LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 3.3.
(IMPLIES (AND (EQUAL B 0)
(NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)))
(NOT (EQUAL (REMAINDER A B) 0))),
which further simplifies, rewriting with the lemmas REMAINDER-ZERO,
EQUAL-FIB-CONSTANT, and GCD-0, and expanding the functions FIB and ZEROP,
to:
T.
Case 3.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)))
(NOT (EQUAL (REMAINDER A B) 0))),
which further simplifies, using linear arithmetic, applying FIB-SMALL,
REMAINDER-ZERO, and EQUAL-FIB-CONSTANT, and expanding ZEROP and GCD, to:
T.
Case 3.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X B) (NOT (ZEROP B)))
(NUMBERP Z)
(NUMBERP B)
(NOT (EQUAL B 0))
(NOT (EQUAL (REMAINDER (FIB (PLUS X (TIMES B Z)))
(FIB B))
0))
(NOT (EQUAL (REMAINDER (FIB (GCD (PLUS X (TIMES B Z)) B))
(FIB B))
0)))
(NOT (EQUAL X 0))).
However this further simplifies, applying GCD-TIMES, COMMUTATIVITY-OF-GCD,
and REMAINDER-X-X, and opening up the functions NUMBERP, EQUAL, LESSP,
ZEROP, NOT, and PLUS, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (REMAINDER (FIB A) (FIB B)) 0))
(NOT (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)))
(NOT (EQUAL B 2))).
But this again simplifies, rewriting with the lemma REMAINDER-1-ARG2, and
expanding the definitions of FIB and EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(EQUAL (EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)
T)
(NOT (EQUAL (REMAINDER A B) 0)))
(EQUAL B 2)),
which again simplifies, obviously, to:
(IMPLIES (AND (EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)
(NOT (EQUAL (REMAINDER A B) 0)))
(EQUAL B 2)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by
(PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We
rely upon LESSP-REMAINDER, 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 conjectures:
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)
(NOT (EQUAL (REMAINDER A B) 0)))
(EQUAL B 2)).
But this further simplifies, using linear arithmetic, rewriting with
FIB-SMALL, EQUAL-FIB-CONSTANT, REMAINDER-ZERO, and REMAINDER-OF-NON-NUMBER,
and unfolding the definitions of LESSP, EQUAL, NUMBERP, REMAINDER, GCD,
and ZEROP, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL B 0)
(EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)
(NOT (EQUAL (REMAINDER A B) 0)))
(EQUAL B 2)).
But this further simplifies, rewriting with REMAINDER-ZERO,
EQUAL-FIB-CONSTANT, and GCD-0, and opening up FIB, ZEROP, GCD, REMAINDER,
and EQUAL, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP B))
(EQUAL (REMAINDER (FIB A) (FIB B)) 0)
(EQUAL (REMAINDER (FIB (GCD A B)) (FIB B))
0)
(NOT (EQUAL (REMAINDER A B) 0)))
(EQUAL B 2)).
This further simplifies, using linear arithmetic, rewriting with FIB-SMALL,
REMAINDER-ZERO, EQUAL-FIB-CONSTANT, and GCD-0, and unfolding the
definitions of ZEROP, FIB, REMAINDER, EQUAL, NUMBERP, and GCD, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X B) (NOT (ZEROP B)))
(NUMBERP Z)
(NUMBERP B)
(NOT (EQUAL B 0))
(EQUAL (REMAINDER (FIB (PLUS X (TIMES B Z)))
(FIB B))
0)
(EQUAL (REMAINDER (FIB (GCD (PLUS X (TIMES B Z)) B))
(FIB B))
0)
(NOT (EQUAL X 0)))
(EQUAL B 2)).
This further simplifies, applying COMMUTATIVITY-OF-TIMES, FIB-PLUS,
REMAINDER-TIMES1-INSTANCE, GCD-PLUS, LESSP-FIB-FIB, LESSP-GCD3,
REMAINDER-NOOP, EQUAL-GCD-0, and EQUAL-FIB-CONSTANT, and expanding ZEROP,
NOT, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.9 0.0 ]
REMAINDER-FIB-FIB-0
(PROVE-LEMMA FIB-TIMES-OPEN
(REWRITE)
(IMPLIES (LESSP 0 K)
(EQUAL (FIB (TIMES K N))
(PLUS (TIMES (FIB N)
(FIB (ADD1 (TIMES (SUB1 K) N))))
(TIMES (FIB (SUB1 N))
(FIB (TIMES (SUB1 K) N))))))
((USE (FIB-PLUS (J (TIMES (SUB1 K) N))
(K N)))
(DISABLE FIB-PLUS)))
This simplifies, using linear arithmetic, applying COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY-OF-PLUS, TIMES-ZERO, FIB-SMALL, SUB1-NNUMBERP,
COMMUTATIVITY2-OF-PLUS, PLUS-ZERO-ARG2, ADD1-SUB1, and TIMES-1-ARG1, and
unfolding the definitions of TIMES, ZEROP, EQUAL, LESSP, FIB, ADD1, PLUS, and
SUB1, to:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))
0))
(EQUAL (FIB (PLUS N
(SUB1 K)
(TIMES (SUB1 K) (SUB1 N))))
(PLUS (TIMES (FIB N)
(FIB (SUB1 (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N))))))
(TIMES (FIB (ADD1 N))
(FIB (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))))))
(NOT (EQUAL K 0))
(NUMBERP K))
(EQUAL (FIB (ADD1 (PLUS (SUB1 K)
(SUB1 N)
(TIMES (SUB1 K) (SUB1 N)))))
(PLUS (TIMES (FIB N)
(FIB (ADD1 (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N))))))
(TIMES (FIB (SUB1 N))
(FIB (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))))))),
which again simplifies, rewriting with EQUAL-SUB1-0, EQUAL-TIMES-0,
EQUAL-PLUS-0, COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL,
TIMES-DISTRIBUTES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS,
and expanding the functions EQUAL, NUMBERP, and FIB, to:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL K 1))
(EQUAL (FIB (PLUS N
(SUB1 K)
(TIMES (SUB1 K) (SUB1 N))))
(PLUS (TIMES (FIB N)
(FIB (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))))
(TIMES (FIB N)
(FIB (SUB1 (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N))))))
(TIMES (FIB (SUB1 N))
(FIB (PLUS (SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))))))
(NOT (EQUAL K 0))
(NUMBERP K))
(EQUAL (FIB (ADD1 (PLUS (SUB1 K)
(SUB1 N)
(TIMES (SUB1 K) (SUB1 N)))))
(FIB (PLUS N
(SUB1 K)
(TIMES (SUB1 K) (SUB1 N)))))).
Applying the lemma SUB1-ELIM, replace K by (ADD1 X) to eliminate (SUB1 K). We
use the type restriction lemma noted when SUB1 was introduced to restrict the
new variable. We thus obtain:
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (ADD1 X) 1))
(EQUAL (FIB (PLUS N X (TIMES X (SUB1 N))))
(PLUS (TIMES (FIB N)
(FIB (PLUS X (TIMES X (SUB1 N)))))
(TIMES (FIB N)
(FIB (SUB1 (PLUS X (TIMES X (SUB1 N))))))
(TIMES (FIB (SUB1 N))
(FIB (PLUS X (TIMES X (SUB1 N)))))))
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (FIB (ADD1 (PLUS X (SUB1 N) (TIMES X (SUB1 N)))))
(FIB (PLUS N X (TIMES X (SUB1 N)))))),
which further simplifies, rewriting with ADD1-EQUAL, and expanding NUMBERP, to:
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(EQUAL (FIB (PLUS N X (TIMES X (SUB1 N))))
(PLUS (TIMES (FIB N)
(FIB (PLUS X (TIMES X (SUB1 N)))))
(TIMES (FIB N)
(FIB (SUB1 (PLUS X (TIMES X (SUB1 N))))))
(TIMES (FIB (SUB1 N))
(FIB (PLUS X (TIMES X (SUB1 N))))))))
(EQUAL (FIB (ADD1 (PLUS X (SUB1 N) (TIMES X (SUB1 N)))))
(FIB (PLUS N X (TIMES X (SUB1 N)))))).
Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We
use the type restriction lemma noted when SUB1 was introduced to restrict the
new variable. We would thus like to prove:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL X 0))
(EQUAL (FIB (PLUS (ADD1 Z) X (TIMES X Z)))
(PLUS (TIMES (FIB (ADD1 Z))
(FIB (PLUS X (TIMES X Z))))
(TIMES (FIB (ADD1 Z))
(FIB (SUB1 (PLUS X (TIMES X Z)))))
(TIMES (FIB Z)
(FIB (PLUS X (TIMES X Z)))))))
(EQUAL (FIB (ADD1 (PLUS X Z (TIMES X Z))))
(FIB (PLUS (ADD1 Z) X (TIMES X Z))))),
which finally simplifies, applying COMMUTATIVITY2-OF-PLUS, PLUS-ADD1-ARG1, and
COMMUTATIVITY-OF-PLUS, to:
T.
Q.E.D.
[ 0.0 1.6 0.0 ]
FIB-TIMES-OPEN
(DISABLE FIB-TIMES-OPEN)
[ 0.0 0.0 0.0 ]
FIB-TIMES-OPEN-OFF
(PROVE-LEMMA FIB-ADD1-TIMES-OPEN
(REWRITE)
(IMPLIES (LESSP 0 K)
(EQUAL (FIB (ADD1 (TIMES K N)))
(PLUS (TIMES (FIB (ADD1 (TIMES (SUB1 K) N)))
(FIB (ADD1 N)))
(TIMES (FIB (TIMES (SUB1 K) N))
(FIB N)))))
((USE (FIB-PLUS (J (ADD1 (TIMES (SUB1 K) N)))
(K N)))
(DISABLE FIB-PLUS)))
This conjecture can be simplified, using the abbreviations IMPLIES and
PLUS-ADD1-ARG1, to the conjecture:
(IMPLIES
(AND (EQUAL (FIB (ADD1 (PLUS (TIMES (SUB1 K) N) N)))
(IF (ZEROP (ADD1 (TIMES (SUB1 K) N)))
(FIB N)
(PLUS (TIMES (FIB (ADD1 N))
(FIB (ADD1 (TIMES (SUB1 K) N))))
(TIMES (FIB (SUB1 (ADD1 (TIMES (SUB1 K) N))))
(FIB N)))))
(LESSP 0 K))
(EQUAL (FIB (ADD1 (TIMES K N)))
(PLUS (TIMES (FIB (ADD1 (TIMES (SUB1 K) N)))
(FIB (ADD1 N)))
(TIMES (FIB (TIMES (SUB1 K) N))
(FIB N))))).
This simplifies, applying COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, and
SUB1-ADD1, and unfolding the functions ZEROP, EQUAL, LESSP, and TIMES, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
FIB-ADD1-TIMES-OPEN
(DISABLE FIB-ADD1-TIMES-OPEN)
[ 0.0 0.0 0.0 ]
FIB-ADD1-TIMES-OPEN-OFF
(PROVE-LEMMA FIB-TIMES-SPECIAL-STEP
(REWRITE)
(IMPLIES
(LESSP 1 K)
(EQUAL (REMAINDER (TIMES K
(TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB (SUB1 N))
(TIMES (SUB1 K)
(TIMES (FIB N)
(EXP (FIB (ADD1 N))
(SUB1 (SUB1 K)))))))
(TIMES (FIB N) (FIB N)))))
((DISABLE-THEORY GCDS)
(DISABLE GCD-REMAINDER-TIMES-FACT1-PROOF2 DIFFERENCE-LEQ-ARG1
GCD-REMAINDER-TIMES-FACT1-PROOF EQUAL-REMAINDER-PLUS-0
REMAINDER-NOOP LESSP-1-HACK)))
WARNING: the previously added lemma, REMAINDER-TIMES-TIMES-HACK, could be
applied whenever the newly proposed FIB-TIMES-SPECIAL-STEP could!
This formula can be simplified, using the abbreviations IMPLIES,
REMAINDER-PLUS-TIMES-HACK, and REMAINDER-TIMES-TIMES-HACK, to:
(IMPLIES
(LESSP 1 K)
(EQUAL
(TIMES (FIB N)
(REMAINDER (TIMES K
(EXP (FIB (ADD1 N)) (SUB1 K)))
(FIB N)))
(TIMES (FIB N)
(REMAINDER (PLUS (EXP (FIB (ADD1 N)) (SUB1 K))
(TIMES (FIB (SUB1 N))
(SUB1 K)
(EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))))
(FIB N))))),
which simplifies, rewriting with EQUAL-SUB1-0,
CORRECTNESS-OF-CANCEL-EQUAL-TIMES, and EQUAL-FIB-CONSTANT, and unfolding EXP,
TIMES, ZEROP, FIX, and OR, to the following four new formulas:
Case 4. (IMPLIES (AND (LESSP 1 K)
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL K 1))
(EQUAL (REMAINDER (TIMES K 1) (FIB N))
(REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0))
(FIB N)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (LESSP 1 K)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NUMBERP K)))
(EQUAL (REMAINDER (TIMES K 1) (FIB N))
(REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0))
(FIB N)))),
which again simplifies, unfolding the definition of LESSP, to:
T.
Case 2. (IMPLIES (AND (LESSP 1 K)
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL K 0))
(EQUAL (REMAINDER (TIMES K 1) (FIB N))
(REMAINDER (PLUS 1 (TIMES (FIB (SUB1 N)) 0))
(FIB N)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (LESSP 1 K)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL K 0))
(NUMBERP K)
(NOT (EQUAL K 1)))
(EQUAL
(REMAINDER (TIMES K
(FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))
(FIB N))
(REMAINDER (PLUS (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))
(TIMES (FIB (SUB1 N))
(PLUS (EXP (FIB (ADD1 N)) (SUB1 (SUB1 K)))
(TIMES (SUB1 (SUB1 K))
(EXP (FIB (ADD1 N))
(SUB1 (SUB1 K)))))))
(FIB N)))),
which again simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS,
SUB1-ADD1, ADD1-EQUAL, TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES1,
REMAINDER-TIMES1-INSTANCE, REMAINDER-PLUS, and ASSOCIATIVITY-OF-PLUS, and
opening up the functions NUMBERP, FIB, and EQUAL, to:
(IMPLIES
(AND (LESSP 1 K)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL K 0))
(NUMBERP K)
(NOT (EQUAL K 1)))
(EQUAL (REMAINDER (TIMES K
(FIB (SUB1 N))
(EXP (PLUS (FIB N) (FIB (SUB1 N)))
(SUB1 (SUB1 K))))
(FIB N))
(REMAINDER (PLUS (TIMES (FIB (SUB1 N))
(EXP (PLUS (FIB N) (FIB (SUB1 N)))
(SUB1 (SUB1 K))))
(TIMES (FIB (SUB1 N))
(EXP (PLUS (FIB N) (FIB (SUB1 N)))
(SUB1 (SUB1 K))))
(TIMES (FIB (SUB1 N))
(SUB1 (SUB1 K))
(EXP (PLUS (FIB N) (FIB (SUB1 N)))
(SUB1 (SUB1 K)))))
(FIB N)))).
Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 X) to eliminate
(SUB1 N). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES
(AND (NUMBERP X)
(LESSP 1 K)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL K 0))
(NUMBERP K)
(NOT (EQUAL K 1)))
(EQUAL (REMAINDER (TIMES K
(FIB X)
(EXP (PLUS (FIB (ADD1 X)) (FIB X))
(SUB1 (SUB1 K))))
(FIB (ADD1 X)))
(REMAINDER (PLUS (TIMES (FIB X)
(EXP (PLUS (FIB (ADD1 X)) (FIB X))
(SUB1 (SUB1 K))))
(TIMES (FIB X)
(EXP (PLUS (FIB (ADD1 X)) (FIB X))
(SUB1 (SUB1 K))))
(TIMES (FIB X)
(SUB1 (SUB1 K))
(EXP (PLUS (FIB (ADD1 X)) (FIB X))
(SUB1 (SUB1 K)))))
(FIB (ADD1 X))))).
However this further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, to:
(IMPLIES
(AND (NUMBERP X)
(LESSP 1 K)
(NOT (EQUAL K 0))
(NUMBERP K)
(NOT (EQUAL K 1)))
(EQUAL (REMAINDER (TIMES K
(FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 (SUB1 K))))
(FIB (ADD1 X)))
(REMAINDER (PLUS (TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 (SUB1 K))))
(TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 (SUB1 K))))
(TIMES (FIB X)
(SUB1 (SUB1 K))
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 (SUB1 K)))))
(FIB (ADD1 X))))).
Applying the lemma SUB1-ELIM, replace K by (ADD1 Z) to eliminate (SUB1 K)
and Z by (ADD1 V) to eliminate (SUB1 Z). We use the type restriction lemma
noted when SUB1 was introduced to restrict the new variable. This produces
the following two new goals:
Case 1.2.
(IMPLIES
(AND (EQUAL Z 0)
(NUMBERP Z)
(NUMBERP X)
(LESSP 1 (ADD1 Z))
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL (ADD1 Z) 1)))
(EQUAL (REMAINDER (TIMES (ADD1 Z)
(FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 Z)))
(FIB (ADD1 X)))
(REMAINDER (PLUS (TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 Z)))
(TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 Z)))
(TIMES (FIB X)
(SUB1 Z)
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
(SUB1 Z))))
(FIB (ADD1 X))))).
This finally simplifies, trivially, to:
T.
Case 1.1.
(IMPLIES
(AND (NUMBERP V)
(NOT (EQUAL (ADD1 V) 0))
(NUMBERP X)
(LESSP 1 (ADD1 (ADD1 V)))
(NOT (EQUAL (ADD1 (ADD1 V)) 0))
(NOT (EQUAL (ADD1 (ADD1 V)) 1)))
(EQUAL
(REMAINDER (TIMES (ADD1 (ADD1 V))
(FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X))) V))
(FIB (ADD1 X)))
(REMAINDER (PLUS (TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X))) V))
(TIMES (FIB X)
(EXP (PLUS (FIB X) (FIB (ADD1 X))) V))
(TIMES (FIB X)
V
(EXP (PLUS (FIB X) (FIB (ADD1 X)))
V)))
(FIB (ADD1 X))))).
However this finally simplifies, rewriting with SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY2-OF-TIMES, and TIMES-DISTRIBUTES-OVER-PLUS, and expanding
SUB1, NUMBERP, EQUAL, LESSP, and TIMES, to:
T.
Q.E.D.
[ 0.0 3.4 0.0 ]
FIB-TIMES-SPECIAL-STEP
(PROVE-LEMMA FIB-REMAINDER-HACK
(REWRITE)
(EQUAL (REMAINDER (FIB (TIMES X Y)) (FIB X))
0))
This formula can be simplified, using the abbreviations
REMAINDER-TIMES1-INSTANCE and REMAINDER-FIB-FIB-0, to:
(IMPLIES (NOT (EQUAL 0 0))
(EQUAL X 2)),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FIB-REMAINDER-HACK
(PROVE-LEMMA REMAINDER-BACKCHAIN-PROOF1 NIL
(IMPLIES (EQUAL (REMAINDER A C)
(REMAINDER B C))
(EQUAL (REMAINDER (TIMES A D) C)
(REMAINDER (TIMES B D) C))))
.
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z))
to eliminate (REMAINDER A C) and (QUOTIENT A C). We use LESSP-REMAINDER, 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 A))
(EQUAL (REMAINDER A C)
(REMAINDER B C)))
(EQUAL (REMAINDER (TIMES A D) C)
(REMAINDER (TIMES B D) C))).
This simplifies, applying REMAINDER-OF-NON-NUMBER and REMAINDER-TIMES1, and
expanding the functions LESSP, EQUAL, NUMBERP, REMAINDER, and TIMES, to:
T.
Case 3. (IMPLIES (AND (EQUAL C 0)
(EQUAL (REMAINDER A C)
(REMAINDER B C)))
(EQUAL (REMAINDER (TIMES A D) C)
(REMAINDER (TIMES B D) C))).
However this simplifies, rewriting with REMAINDER-ZERO, and unfolding ZEROP,
TIMES, REMAINDER, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP C))
(EQUAL (REMAINDER A C)
(REMAINDER B C)))
(EQUAL (REMAINDER (TIMES A D) C)
(REMAINDER (TIMES B D) C))).
But this simplifies, applying the lemma REMAINDER-ZERO, and opening up ZEROP,
TIMES, NUMBERP, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL X (REMAINDER B C)))
(EQUAL (REMAINDER (TIMES (PLUS X (TIMES C Z)) D)
C)
(REMAINDER (TIMES B D) C))),
which simplifies, rewriting with LESSP-REMAINDER, COMMUTATIVITY-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, TIMES-DISTRIBUTES-OVER-PLUS,
REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and opening up the
definitions of ZEROP, NOT, and EQUAL, to:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (TIMES D (REMAINDER B C))
C)
(REMAINDER (TIMES B D) C))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by
(PLUS X (TIMES C V)) to eliminate (REMAINDER B C) and (QUOTIENT B C). We
employ LESSP-REMAINDER, 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 formulas:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (TIMES D (REMAINDER B C))
C)
(REMAINDER (TIMES B D) C))).
However this further simplifies, using linear arithmetic, applying
REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, and COMMUTATIVITY-OF-TIMES, and
opening up the definitions of NUMBERP, EQUAL, and TIMES, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (TIMES D X) C)
(REMAINDER (TIMES (PLUS X (TIMES C V)) D)
C))).
But this further simplifies, applying COMMUTATIVITY-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, TIMES-DISTRIBUTES-OVER-PLUS,
REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding the functions
ZEROP, NOT, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
REMAINDER-BACKCHAIN-PROOF1
(PROVE-LEMMA REMAINDER-BACKCHAIN-PROOF2 NIL
(IMPLIES (AND (EQUAL (REMAINDER A C)
(REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS A D) C)
(REMAINDER (PLUS B E) C))))
.
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES C Z))
to eliminate (REMAINDER A C) and (QUOTIENT A C). We rely upon LESSP-REMAINDER,
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. (IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A C)
(REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS A D) C)
(REMAINDER (PLUS B E) C))).
However this simplifies, applying REMAINDER-OF-NON-NUMBER and REMAINDER-PLUS,
and unfolding the functions LESSP, EQUAL, NUMBERP, REMAINDER, and PLUS, to:
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL 0 (REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C))
(NOT (NUMBERP D)))
(EQUAL (REMAINDER 0 C)
(REMAINDER D C))),
which again simplifies, applying the lemma REMAINDER-OF-NON-NUMBER, and
opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Case 3. (IMPLIES (AND (EQUAL C 0)
(EQUAL (REMAINDER A C)
(REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS A D) C)
(REMAINDER (PLUS B E) C))),
which simplifies, applying REMAINDER-ZERO and PLUS-ZERO-ARG2, and unfolding
ZEROP, PLUS, EQUAL, REMAINDER, and NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP C))
(EQUAL (REMAINDER A C)
(REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS A D) C)
(REMAINDER (PLUS B E) C))).
But this simplifies, appealing to the lemmas REMAINDER-ZERO and
PLUS-ZERO-ARG2, and unfolding the functions ZEROP, PLUS, EQUAL, and NUMBERP,
to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL X (REMAINDER B C))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS (PLUS X (TIMES C Z)) D)
C)
(REMAINDER (PLUS B E) C))),
which simplifies, rewriting with the lemmas LESSP-REMAINDER,
COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS,
REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and expanding the functions
ZEROP, NOT, and EQUAL, to the goal:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS D (REMAINDER B C)) C)
(REMAINDER (PLUS B E) C))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace D by
(PLUS X (TIMES C V)) to eliminate (REMAINDER D C) and (QUOTIENT D C). We
rely upon LESSP-REMAINDER, 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 two new
conjectures:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP D))
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL (REMAINDER D C)
(REMAINDER E C)))
(EQUAL (REMAINDER (PLUS D (REMAINDER B C)) C)
(REMAINDER (PLUS B E) C))),
which further simplifies, using linear arithmetic, applying REMAINDER-NOOP,
REMAINDER-OF-NON-NUMBER, REMAINDER-X-X, REMAINDER-REMAINDER, and
REMAINDER-PLUS, and expanding NUMBERP, PLUS, and EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(EQUAL X (REMAINDER E C)))
(EQUAL (REMAINDER (PLUS (PLUS X (TIMES C V))
(REMAINDER B C))
C)
(REMAINDER (PLUS B E) C))).
However this further simplifies, applying LESSP-REMAINDER,
COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS,
REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding ZEROP, NOT,
and EQUAL, to:
(IMPLIES (AND (NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS (REMAINDER B C) (REMAINDER E C))
C)
(REMAINDER (PLUS B E) C))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by
(PLUS X (TIMES C W)) to eliminate (REMAINDER B C) and (QUOTIENT B C). We
use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was
introduced to restrict the new variables. We thus obtain the following
two new formulas:
Case 1.1.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS (REMAINDER B C) (REMAINDER E C))
C)
(REMAINDER (PLUS B E) C))).
This further simplifies, using linear arithmetic, rewriting with
REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, REMAINDER-X-X, and
REMAINDER-REMAINDER, and expanding the functions NUMBERP, EQUAL, and
PLUS, to the new conjecture:
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0))
(NOT (NUMBERP E)))
(EQUAL (REMAINDER E C)
(REMAINDER 0 C))),
which finally simplifies, using linear arithmetic, applying
REMAINDER-NOOP and REMAINDER-OF-NON-NUMBER, and unfolding NUMBERP and
EQUAL, to:
T.
Case 1.1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X C) (NOT (ZEROP C)))
(NUMBERP W)
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C)
(REMAINDER (PLUS (PLUS X (TIMES C W)) E)
C))).
This further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, REMAINDER-TIMES1-INSTANCE,
and REMAINDER-PLUS, and opening up the functions ZEROP, NOT, and EQUAL,
to the goal:
(IMPLIES (AND (NUMBERP X)
(LESSP X C)
(NUMBERP W)
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C)
(REMAINDER (PLUS E X) C))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace E by
(PLUS X1 (TIMES C Z1)) to eliminate (REMAINDER E C) and (QUOTIENT E C).
We employ LESSP-REMAINDER, 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 two new goals:
Case 1.1.1.2.
(IMPLIES (AND (NOT (NUMBERP E))
(NUMBERP X)
(LESSP X C)
(NUMBERP W)
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS X (REMAINDER E C)) C)
(REMAINDER (PLUS E X) C))),
which finally simplifies, using linear arithmetic, applying
REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, and PLUS-ZERO-ARG2, and
expanding the definitions of NUMBERP, ZEROP, and PLUS, to:
T.
Case 1.1.1.1.
(IMPLIES (AND (NUMBERP X1)
(EQUAL (LESSP X1 C) (NOT (ZEROP C)))
(NUMBERP Z1)
(NUMBERP X)
(LESSP X C)
(NUMBERP W)
(NUMBERP V)
(NUMBERP Z)
(NUMBERP C)
(NOT (EQUAL C 0)))
(EQUAL (REMAINDER (PLUS X X1) C)
(REMAINDER (PLUS (PLUS X1 (TIMES C Z1)) X)
C))).
But this finally simplifies, appealing to the lemmas
COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS,
REMAINDER-TIMES1-INSTANCE, and REMAINDER-PLUS, and unfolding the
definitions of ZEROP, NOT, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.7 0.0 ]
REMAINDER-BACKCHAIN-PROOF2
(PROVE-LEMMA REMAINDER-FIB-BACKCHAIN
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER (FIB X) C)
(REMAINDER (EXP P Q) C))
(EQUAL (REMAINDER (FIB Y) C)
(REMAINDER (TIMES R S) C)))
(EQUAL (REMAINDER (PLUS (TIMES A (FIB X))
(TIMES B (FIB Y)))
C)
(REMAINDER (PLUS (TIMES A (EXP P Q))
(TIMES B (TIMES R S)))
C)))
((USE (REMAINDER-BACKCHAIN-PROOF2 (A (TIMES A (FIB X)))
(B (TIMES A (EXP P Q)))
(D (TIMES B (FIB Y)))
(E (TIMES B (TIMES R S)))
(C C))
(REMAINDER-BACKCHAIN-PROOF1 (A (FIB Y))
(B (TIMES R S))
(C C)
(D B))
(REMAINDER-BACKCHAIN-PROOF1 (A (FIB X))
(B (EXP P Q))
(C C)
(D A)))
(DISABLE-THEORY NATURALS)
(ENABLE COMMUTATIVITY-OF-TIMES)))
WARNING: Note that REMAINDER-FIB-BACKCHAIN contains the free variables S, R,
Q, and P which will be chosen by instantiating the hypotheses:
(EQUAL (REMAINDER (FIB X) C)
(REMAINDER (EXP P Q) C))
and (EQUAL (REMAINDER (FIB Y) C) (REMAINDER (TIMES R S) C)).
This formula simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and unfolding
the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
REMAINDER-FIB-BACKCHAIN
(PROVE-LEMMA FIB-TIMES-SPECIAL NIL
(IMPLIES (LESSP 1 K)
(AND (EQUAL (REMAINDER (FIB (TIMES K N))
(EXP (FIB N) 2))
(REMAINDER (TIMES K
(TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(EXP (FIB N) 2)))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES K N)))
(EXP (FIB N) 2))
(REMAINDER (EXP (FIB (ADD1 N)) K)
(EXP (FIB N) 2)))))
((INDUCT (TIMES K N))
(DISABLE TIMES EQUAL-SUB1-0 REMAINDER-TIMES2-INSTANCE DIFFERENCE-LEQ-ARG1
GCD-REMAINDER-TIMES-FACT1-PROOF2 LESSP-FIB-FIB REMAINDER-NOOP
LESSP-1-HACK REMAINDER-TIMES-TIMES-HACK EXP
REMAINDER-PLUS-TIMES-HACK REMAINDER-TIMES2 COMMUTATIVITY2-OF-TIMES
COMMUTATIVITY-OF-PLUS)
(ENABLE FIB-ADD1-TIMES-OPEN FIB-TIMES-OPEN REMAINDER-TIMES-TIMES)
(DISABLE-THEORY GCDS)))
This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP K) (LESSP 1 K))
(AND (EQUAL (REMAINDER (FIB (TIMES K N))
(EXP (FIB N) 2))
(REMAINDER (TIMES K
(FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(EXP (FIB N) 2)))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES K N)))
(EXP (FIB N) 2))
(REMAINDER (EXP (FIB (ADD1 N)) K)
(EXP (FIB N) 2))))).
This simplifies, opening up the definitions of ZEROP and LESSP, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EQUAL K 0))
(NUMBERP K)
(IMPLIES
(LESSP 1 (SUB1 K))
(AND (EQUAL (REMAINDER (FIB (TIMES (SUB1 K) N))
(EXP (FIB N) 2))
(REMAINDER (TIMES (SUB1 K)
(FIB N)
(EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))
(EXP (FIB N) 2)))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES (SUB1 K) N)))
(EXP (FIB N) 2))
(REMAINDER (EXP (FIB (ADD1 N)) (SUB1 K))
(EXP (FIB N) 2)))))
(LESSP 1 K))
(AND (EQUAL (REMAINDER (FIB (TIMES K N))
(EXP (FIB N) 2))
(REMAINDER (TIMES K
(FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(EXP (FIB N) 2)))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES K N)))
(EXP (FIB N) 2))
(REMAINDER (EXP (FIB (ADD1 N)) K)
(EXP (FIB N) 2))))).
This simplifies, using linear arithmetic, applying the lemmas
COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, TIMES-1-ARG1, EXP-ADD1, FIB-TIMES-OPEN,
FIB-TIMES-SPECIAL-STEP, FIB-ADD1-TIMES-OPEN, REMAINDER-TIMES-TIMES,
FIB-REMAINDER-HACK, REMAINDER-PLUS, REMAINDER-FIB-BACKCHAIN,
REMAINDER-TIMES1, and REMAINDER-TIMES1-INSTANCE, and opening up the
functions SUB1, NUMBERP, EQUAL, LESSP, AND, and IMPLIES, to the following
three new goals:
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL K 0))
(NUMBERP K)
(EQUAL (SUB1 (SUB1 K)) 0)
(NOT (EQUAL (SUB1 K) 0)))
(EQUAL (REMAINDER (PLUS (TIMES (FIB N)
(FIB (ADD1 (TIMES N (SUB1 K)))))
(TIMES (FIB (SUB1 N))
(FIB (TIMES N (SUB1 K)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB (SUB1 N))
(FIB N)
(SUB1 K)))
(TIMES (FIB N) (FIB N))))).
Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to
eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the
type restriction lemma noted when SUB1 was introduced to constrain the new
variable. We must thus prove the formula:
(IMPLIES
(AND (NUMBERP Z)
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(EQUAL Z 0)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (REMAINDER (PLUS (TIMES (FIB N)
(FIB (ADD1 (TIMES N (ADD1 Z)))))
(TIMES (FIB (SUB1 N))
(FIB (TIMES N (ADD1 Z)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (ADD1 Z)))
(TIMES (FIB (SUB1 N))
(FIB N)
(ADD1 Z)))
(TIMES (FIB N) (FIB N))))).
But this further simplifies, applying TIMES-1-ARG1, COMMUTATIVITY-OF-TIMES,
EXP-0-ARG2, and EXP-ADD1, and opening up the definitions of NUMBERP and
EQUAL, to the following two new formulas:
Case 1.3.2.
(IMPLIES (NOT (NUMBERP N))
(EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB 1))
(TIMES (FIB (SUB1 N)) (FIB 0)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
(TIMES (FIB N) (FIB (SUB1 N))))
(TIMES (FIB N) (FIB N))))).
However this again simplifies, using linear arithmetic, applying the
lemmas FIB-SMALL, SUB1-NNUMBERP, and SUB1-TYPE-RESTRICTION, and
expanding the functions FIB, TIMES, PLUS, REMAINDER, and EQUAL, to:
T.
Case 1.3.1.
(IMPLIES (NUMBERP N)
(EQUAL (REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
(TIMES (FIB (SUB1 N)) (FIB N)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
(TIMES (FIB N) (FIB (SUB1 N))))
(TIMES (FIB N) (FIB N))))),
which again simplifies, applying SUB1-ADD1, ADD1-EQUAL, and
COMMUTATIVITY-OF-TIMES, and unfolding NUMBERP and FIB, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL K 0))
(NUMBERP K)
(EQUAL (SUB1 (SUB1 K)) 0)
(NOT (EQUAL (SUB1 K) 0)))
(EQUAL (REMAINDER (TIMES (FIB (ADD1 N))
(FIB (ADD1 (TIMES N (SUB1 K)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) K)
(TIMES (FIB N) (FIB N))))).
Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to
eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the
type restriction lemma noted when SUB1 was introduced to constrain the new
variable. We must thus prove:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(EQUAL Z 0)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (REMAINDER (TIMES (FIB (ADD1 N))
(FIB (ADD1 (TIMES N (ADD1 Z)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) (ADD1 (ADD1 Z)))
(TIMES (FIB N) (FIB N))))).
This further simplifies, applying the lemmas TIMES-1-ARG1,
COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, and EXP-ADD1, and unfolding NUMBERP
and EQUAL, to the conjecture:
(IMPLIES (NOT (NUMBERP N))
(EQUAL (REMAINDER (TIMES (FIB (ADD1 N)) (FIB 1))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (FIB (ADD1 N)) (FIB (ADD1 N)))
(TIMES (FIB N) (FIB N))))).
However this again simplifies, using linear arithmetic, rewriting with
SUB1-TYPE-RESTRICTION and FIB-SMALL, and unfolding the functions FIB,
TIMES, REMAINDER, and EQUAL, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL K 0))
(NUMBERP K)
(EQUAL (REMAINDER (FIB (TIMES N (SUB1 K)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (SUB1 K)
(FIB N)
(EXP (FIB (ADD1 N)) (SUB1 (SUB1 K))))
(TIMES (FIB N) (FIB N))))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES N (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) (SUB1 K))
(TIMES (FIB N) (FIB N))))
(NOT (EQUAL (SUB1 K) 0)))
(EQUAL (REMAINDER (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) K)
(TIMES (FIB N) (FIB N))))).
Appealing to the lemma SUB1-ELIM, we now replace K by (ADD1 X) to
eliminate (SUB1 K) and X by (ADD1 Z) to eliminate (SUB1 X). We rely upon
the type restriction lemma noted when SUB1 was introduced to constrain the
new variable. This generates the goal:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(EQUAL (REMAINDER (FIB (TIMES N (ADD1 Z)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (ADD1 Z)
(FIB N)
(EXP (FIB (ADD1 N)) Z))
(TIMES (FIB N) (FIB N))))
(EQUAL (REMAINDER (FIB (ADD1 (TIMES N (ADD1 Z))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) (ADD1 Z))
(TIMES (FIB N) (FIB N))))
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (REMAINDER (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (ADD1 Z)))
(TIMES (FIB N) (FIB N)))
(REMAINDER (EXP (FIB (ADD1 N)) (ADD1 (ADD1 Z)))
(TIMES (FIB N) (FIB N))))).
But this further simplifies, using linear arithmetic, rewriting with
TIMES-ADD1, EQUAL-TIMES-0, FIB-SMALL, COMMUTATIVITY-OF-TIMES,
FIB-ADD1-TIMES-OPEN, ASSOCIATIVITY-OF-TIMES, TIMES-DISTRIBUTES-OVER-PLUS,
FIB-TIMES-OPEN, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, FIB-PLUS,
EXP-ADD1, EQUAL-TIMES-X-X, PLUS-ZERO-ARG2, EXP-1-ARG1, and
SUB1-TYPE-RESTRICTION, and opening up the functions LESSP, EQUAL, NUMBERP,
ZEROP, ADD1, FIB, TIMES, and REMAINDER, to:
T.
Q.E.D.
[ 0.0 2.3 0.1 ]
FIB-TIMES-SPECIAL
(PROVE-LEMMA FIB-REMAINDER-TIMES-SPECIAL
(REWRITE)
(EQUAL (REMAINDER (FIB (TIMES N K))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES K
(TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N))))
((USE (FIB-TIMES-SPECIAL))
(DISABLE REMAINDER-TIMES-TIMES-HACK)
(DISABLE-THEORY NATURALS)
(ENABLE-THEORY EXPONENTIATION MULTIPLICATION)))
This conjecture simplifies, rewriting with LESSP-1-HACK,
COMMUTATIVITY-OF-TIMES, EXP-0-ARG2, TIMES-1-ARG1, EXP-ADD1,
COMMUTATIVITY2-OF-TIMES, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, and SUB1-NNUMBERP,
and opening up TIMES, EXP, AND, IMPLIES, FIB, LESSP, EQUAL, NUMBERP, REMAINDER,
and SUB1, to the following four new goals:
Case 4. (IMPLIES (AND (EQUAL K 1) (NOT (NUMBERP N)))
(EQUAL (REMAINDER (FIB 0)
(TIMES (FIB N) (FIB N)))
(REMAINDER (FIB N)
(TIMES (FIB N) (FIB N))))).
However this again simplifies, using linear arithmetic, rewriting with the
lemma FIB-SMALL, and unfolding the definitions of FIB, TIMES, REMAINDER, and
EQUAL, to:
T.
Case 3. (IMPLIES
(AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N)
(SUB1 K)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N))))
(EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N) (FIB N))))
(NOT (EQUAL K 0))
(NUMBERP K))
(EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N)
(SUB1 K)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N))))),
which again simplifies, clearly, to:
T.
Case 2. (IMPLIES
(AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N)
(SUB1 K)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N))))
(EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N) (FIB N))))
(EQUAL K 0))
(EQUAL (REMAINDER (FIB 0)
(TIMES (FIB N) (FIB N)))
(REMAINDER 0
(TIMES (FIB N) (FIB N))))).
But this again simplifies, using linear arithmetic, applying
COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1, FIB-PLUS, EXP-0-ARG2, LESSP-TIMES1,
EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, TIMES-ZERO, FIB-SMALL, and
SUB1-TYPE-RESTRICTION, and opening up the definitions of SUB1, EQUAL, TIMES,
FIB, ADD1, NUMBERP, LESSP, REMAINDER, PLUS, EXP, and ZEROP, to:
T.
Case 1. (IMPLIES
(AND (EQUAL (REMAINDER (FIB (PLUS N (TIMES N (SUB1 K))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (PLUS (TIMES (FIB N)
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N)
(SUB1 K)
(EXP (FIB (ADD1 N)) (SUB1 K))))
(TIMES (FIB N) (FIB N))))
(EQUAL (REMAINDER (FIB (ADD1 (PLUS N (TIMES N (SUB1 K)))))
(TIMES (FIB N) (FIB N)))
(REMAINDER (TIMES (FIB (ADD1 N))
(EXP (FIB (ADD1 N)) (SUB1 K)))
(TIMES (FIB N) (FIB N))))
(NOT (NUMBERP K)))
(EQUAL (REMAINDER (FIB 0)
(TIMES (FIB N) (FIB N)))
(REMAINDER 0
(TIMES (FIB N) (FIB N))))).
But this again simplifies, using linear arithmetic, rewriting with
SUB1-NNUMBERP, COMMUTATIVITY-OF-TIMES, TIMES-1-ARG1, FIB-PLUS, EXP-0-ARG2,
LESSP-TIMES1, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT, TIMES-ZERO, FIB-SMALL, and
SUB1-TYPE-RESTRICTION, and unfolding the definitions of EQUAL, TIMES, FIB,
ADD1, NUMBERP, LESSP, REMAINDER, PLUS, EXP, and ZEROP, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
FIB-REMAINDER-TIMES-SPECIAL
(PROVE-LEMMA REMAINDER-TIMES-TIMES-HACK2
(REWRITE)
(EQUAL (REMAINDER (TIMES K N) (TIMES N P))
(TIMES N (REMAINDER K P))))
This simplifies, appealing to the lemmas REMAINDER-TIMES1-INSTANCE,
QUOTIENT-TIMES-INSTANCE, REMAINDER-TIMES2, and
CORRECTNESS-OF-CANCEL-EQUAL-TIMES, and opening up the definitions of EQUAL,
ZEROP, FIX, and OR, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NUMBERP K)))
(EQUAL (REMAINDER 0 P)
(REMAINDER K P))).
This again simplifies, appealing to the lemma REMAINDER-OF-NON-NUMBER, and
unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
REMAINDER-TIMES-TIMES-HACK2
(PROVE-LEMMA MATIJASEVICH-LEMMA-HELPER NIL
(IMPLIES (AND (LESSP 2 N)
(EQUAL (REMAINDER M N) 0))
(EQUAL (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
((DISABLE TIMES-ADD1 REMAINDER-TIMES2 LESSP-1-HACK FIB GCD
GCD-REMAINDER REMAINDER-TIMES2-INSTANCE)
(ENABLE REMAINDER-TIMES-TIMES)))
This conjecture simplifies, clearly, to the following two new formulas:
Case 2. (IMPLIES (AND (LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(NOT (EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
(NOT (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by
(PLUS X (TIMES N Z)) to eliminate (REMAINDER M N) and (QUOTIENT M N). We
employ LESSP-REMAINDER, 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 M))
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(NOT (EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
(NOT (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0))),
which further simplifies, using linear arithmetic, applying REMAINDER-NOOP,
REMAINDER-OF-NON-NUMBER, EQUAL-TIMES-0, and EQUAL-FIB-CONSTANT, and
opening up the definitions of NUMBERP, EQUAL, LESSP, and REMAINDER, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL N 0)
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(NOT (EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
(NOT (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0))).
However this further simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(NOT (EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
(NOT (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0))),
which further simplifies, opening up LESSP, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X N) (NOT (ZEROP N)))
(NUMBERP Z)
(NUMBERP N)
(NOT (EQUAL N 0))
(LESSP 2 N)
(EQUAL X 0)
(NOT (EQUAL (REMAINDER (PLUS X (TIMES N Z))
(TIMES N (FIB N)))
0)))
(NOT (EQUAL (REMAINDER (FIB (PLUS X (TIMES N Z)))
(TIMES (FIB N) (FIB N)))
0))),
which further simplifies, rewriting with REMAINDER-TIMES-TIMES,
EQUAL-TIMES-0, REMAINDER-TIMES-TIMES-HACK, FIB-REMAINDER-TIMES-SPECIAL,
EQUAL-FIB-CONSTANT, GCD-EXP-1, GCD-FIB, GCD-A-ADD1-A, and
GCD-REMAINDER-TIMES-FACT1-PROOF2, and expanding NUMBERP, EQUAL, LESSP,
ZEROP, NOT, PLUS, and FIB, to:
T.
Case 1. (IMPLIES (AND (LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0))
(EQUAL (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)
T)).
This again simplifies, clearly, to:
(IMPLIES (AND (LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0))
(EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace M by
(PLUS X (TIMES N Z)) to eliminate (REMAINDER M N) and (QUOTIENT M N). We
rely upon LESSP-REMAINDER, 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 conjectures:
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP M))
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0))
(EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)).
However this further simplifies, using linear arithmetic, applying
REMAINDER-NOOP, REMAINDER-OF-NON-NUMBER, EQUAL-TIMES-0, EQUAL-FIB-CONSTANT,
and FIB-SMALL, and unfolding NUMBERP, EQUAL, LESSP, and REMAINDER, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL N 0)
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0))
(EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)).
However this further simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP N))
(LESSP 2 N)
(EQUAL (REMAINDER M N) 0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0))
(EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)),
which further simplifies, expanding the function LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X N) (NOT (ZEROP N)))
(NUMBERP Z)
(NUMBERP N)
(NOT (EQUAL N 0))
(LESSP 2 N)
(EQUAL X 0)
(EQUAL (REMAINDER (PLUS X (TIMES N Z))
(TIMES N (FIB N)))
0))
(EQUAL (REMAINDER (FIB (PLUS X (TIMES N Z)))
(TIMES (FIB N) (FIB N)))
0)),
which further simplifies, rewriting with REMAINDER-TIMES-TIMES,
EQUAL-TIMES-0, REMAINDER-TIMES1, COMMUTATIVITY-OF-TIMES,
REMAINDER-TIMES-TIMES-HACK, and FIB-REMAINDER-TIMES-SPECIAL, and expanding
NUMBERP, EQUAL, LESSP, ZEROP, NOT, PLUS, and TIMES, to:
T.
Q.E.D.
[ 0.0 0.7 0.0 ]
MATIJASEVICH-LEMMA-HELPER
(PROVE-LEMMA MATIJASEVICH-LEMMA
(REWRITE)
(IMPLIES (LESSP 2 N)
(EQUAL (EQUAL (REMAINDER (FIB M)
(TIMES (FIB N) (FIB N)))
0)
(EQUAL (REMAINDER M (TIMES N (FIB N)))
0)))
((USE (MATIJASEVICH-LEMMA-HELPER))))
This simplifies, using linear arithmetic, rewriting with LESSP-1-HACK,
EQUAL-SUB1-0, REMAINDER-FIB-FIB-0, and REMAINDER-TIMES-HACK2, and expanding
the definitions of SUB1, NUMBERP, EQUAL, LESSP, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
MATIJASEVICH-LEMMA