(NOTE-LIB "proveall" T)
Loading ./basic/proveall.lib
Finished loading ./basic/proveall.lib
Loading ./basic/proveall.o
Finished loading ./basic/proveall.o
(#./basic/proveall.lib #./basic/proveall)
(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./basic/tmp.o
Finished loading ./basic/tmp.o
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp
(DEFN BC
(N M)
(IF (ZEROP M)
1
(IF (LESSP N M)
0
(PLUS (BC (SUB1 N) M)
(BC (SUB1 N) (SUB1 M))))))
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT N) decreases according
to the well-founded relation LESSP in each recursive call. Hence, BC is
accepted under the definitional principle. Observe that (NUMBERP (BC N M)) is
a theorem.
[ 0.0 0.0 0.0 ]
BC
(DISABLE EVAL$)
[ 0.0 0.0 0.0 ]
EVAL$-OFF
(PROVE-LEMMA FOR-APPEND-SUM
(REWRITE)
(EQUAL (FOR X
(APPEND A B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X A TEST 'SUM BODY ALIST)
(FOR X B TEST 'SUM BODY ALIST))))
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest three inductions. They merge into two likely candidate
inductions. However, only one is unflawed. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP A)
(p X (CDR A) B TEST BODY ALIST))
(p X A B TEST BODY ALIST))
(IMPLIES (NOT (LISTP A))
(p X A B TEST BODY ALIST))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to the
following two new goals:
Case 2. (IMPLIES (AND (LISTP A)
(EQUAL (FOR X
(APPEND (CDR A) B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X (CDR A) TEST 'SUM BODY ALIST)
(FOR X B TEST 'SUM BODY ALIST))))
(EQUAL (FOR X
(APPEND A B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X A TEST 'SUM BODY ALIST)
(FOR X B TEST 'SUM BODY ALIST)))).
This simplifies, applying COMMUTATIVITY-OF-PLUS, CDR-CONS, and CAR-CONS, and
opening up the definitions of APPEND, QUANTIFIER-OPERATION, EQUAL, and FOR,
to two new goals:
Case 2.2.
(IMPLIES (AND (LISTP A)
(EQUAL (FOR X
(APPEND (CDR A) B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X B TEST 'SUM BODY ALIST)
(FOR X
(CDR A)
TEST 'SUM
BODY ALIST)))
(NOT (EVAL$ T TEST
(CONS (CONS X (CAR A)) ALIST))))
(EQUAL (FOR X
(APPEND (CDR A) B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X B TEST 'SUM BODY ALIST)
(FOR X
(CDR A)
TEST 'SUM
BODY ALIST)))),
which again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP A)
(EQUAL (FOR X
(APPEND (CDR A) B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X B TEST 'SUM BODY ALIST)
(FOR X
(CDR A)
TEST 'SUM
BODY ALIST)))
(EVAL$ T TEST
(CONS (CONS X (CAR A)) ALIST)))
(EQUAL (PLUS (EVAL$ T BODY
(CONS (CONS X (CAR A)) ALIST))
(FOR X
(APPEND (CDR A) B)
TEST 'SUM
BODY ALIST))
(PLUS (FOR X B TEST 'SUM BODY ALIST)
(EVAL$ T BODY
(CONS (CONS X (CAR A)) ALIST))
(FOR X
(CDR A)
TEST 'SUM
BODY ALIST)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (NOT (LISTP A))
(EQUAL (FOR X
(APPEND A B)
TEST 'SUM
BODY ALIST)
(PLUS (FOR X A TEST 'SUM BODY ALIST)
(FOR X B TEST 'SUM BODY ALIST)))),
which simplifies, unfolding the definitions of APPEND, FOR,
QUANTIFIER-INITIAL-VALUE, EQUAL, and PLUS, to the conjecture:
(IMPLIES (AND (NOT (LISTP A))
(NOT (NUMBERP (FOR X B TEST 'SUM BODY ALIST))))
(EQUAL (FOR X B TEST 'SUM BODY ALIST)
0)).
This again simplifies, clearly, to the new conjecture:
(IMPLIES (NOT (LISTP A))
(NUMBERP (FOR X B TEST 'SUM BODY ALIST))),
which has an irrelevant term in it. By eliminating the term we get the new
formula:
(NUMBERP (FOR X B TEST 'SUM BODY ALIST)),
which we will name *1.1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (NLISTP B)
(p X B TEST BODY ALIST))
(IMPLIES (AND (NOT (NLISTP B))
(EVAL$ T TEST
(CONS (CONS X (CAR B)) ALIST))
(p X (CDR B) TEST BODY ALIST))
(p X B TEST BODY ALIST))
(IMPLIES (AND (NOT (NLISTP B))
(NOT (EVAL$ T TEST
(CONS (CONS X (CAR B)) ALIST)))
(p X (CDR B) TEST BODY ALIST))
(p X B TEST BODY ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT B) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following three new formulas:
Case 3. (IMPLIES (NLISTP B)
(NUMBERP (FOR X B TEST 'SUM BODY ALIST))).
This simplifies, opening up the functions NLISTP, FOR,
QUANTIFIER-INITIAL-VALUE, and NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP B))
(EVAL$ T TEST
(CONS (CONS X (CAR B)) ALIST))
(NUMBERP (FOR X
(CDR B)
TEST 'SUM
BODY ALIST)))
(NUMBERP (FOR X B TEST 'SUM BODY ALIST))).
This simplifies, unfolding the definitions of NLISTP, FOR, EQUAL, and
QUANTIFIER-OPERATION, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP B))
(NOT (EVAL$ T TEST
(CONS (CONS X (CAR B)) ALIST)))
(NUMBERP (FOR X
(CDR B)
TEST 'SUM
BODY ALIST)))
(NUMBERP (FOR X B TEST 'SUM BODY ALIST))).
This simplifies, opening up the definitions of NLISTP and FOR, to:
T.
That finishes the proof of *1.1, which, in turn, also finishes the proof
of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FOR-APPEND-SUM
(PROVE-LEMMA BC-X-X1
(REWRITE)
(EQUAL (BC X (ADD1 X)) 0))
Call the conjecture *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 (ADD1 X)) (p X))
(IMPLIES (AND (NOT (ZEROP (ADD1 X)))
(LESSP X (ADD1 X)))
(p X))
(IMPLIES (AND (NOT (ZEROP (ADD1 X)))
(NOT (LESSP X (ADD1 X)))
(p (SUB1 X)))
(p X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP can be used to establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following three new
formulas:
Case 3. (IMPLIES (ZEROP (ADD1 X))
(EQUAL (BC X (ADD1 X)) 0)).
This simplifies, expanding the definition of ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP (ADD1 X)))
(LESSP X (ADD1 X)))
(EQUAL (BC X (ADD1 X)) 0)).
This simplifies, appealing to the lemmas SUB1-ADD1 and SUB1-TYPE-RESTRICTION,
and opening up ZEROP, LESSP, ADD1, BC, EQUAL, and NUMBERP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP (ADD1 X)))
(NOT (LESSP X (ADD1 X)))
(EQUAL (BC (SUB1 X) (ADD1 (SUB1 X)))
0))
(EQUAL (BC X (ADD1 X)) 0)).
This simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BC-X-X1
(PROVE-LEMMA BC-X-X
(REWRITE)
(EQUAL (BC X X) 1))
Name the conjecture *1.
Let us appeal to the induction principle. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X))
(IMPLIES (AND (NOT (ZEROP X)) (LESSP X X))
(p X))
(IMPLIES (AND (NOT (ZEROP X))
(NOT (LESSP X X))
(p (SUB1 X)))
(p X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to three new conjectures:
Case 3. (IMPLIES (ZEROP X)
(EQUAL (BC X X) 1)),
which simplifies, expanding ZEROP, BC, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP X)) (LESSP X X))
(EQUAL (BC X X) 1)),
which simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(NOT (LESSP X X))
(EQUAL (BC (SUB1 X) (SUB1 X)) 1))
(EQUAL (BC X X) 1)),
which simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS and
CORRECTNESS-OF-CANCEL, and unfolding ZEROP, LESSP, BC, NUMBERP, and FIX, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (LESSP (SUB1 X) (SUB1 X)))
(EQUAL (BC (SUB1 X) (SUB1 X)) 1))
(EQUAL (BC (SUB1 X) X) 0)).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
(SUB1 X). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. The result is:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (LESSP Z Z))
(EQUAL (BC Z Z) 1))
(EQUAL (BC Z (ADD1 Z)) 0)).
However this further simplifies, applying the lemma BC-X-X1, and expanding
EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BC-X-X
(PROVE-LEMMA FROM-TO-OPENS-AT-BTM
(REWRITE)
(EQUAL (FROM-TO 0 B)
(CONS 0 (FROM-TO 1 B))))
Call the conjecture *1.
We will try to prove it by induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (LESSP B 0) (p B))
(IMPLIES (AND (NOT (LESSP B 0))
(EQUAL (FIX 0) (FIX B)))
(p B))
(IMPLIES (AND (NOT (LESSP B 0))
(NOT (EQUAL (FIX 0) (FIX B)))
(p (SUB1 B)))
(p B))).
Linear arithmetic, the lemmas COUNT-NUMBERP, SUB1-NNUMBERP, and
COUNT-NOT-LESSP, and the definitions of LESSP, EQUAL, COUNT, and FIX inform us
that the measure (COUNT B) 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 (LESSP B 0)
(EQUAL (FROM-TO 0 B)
(CONS 0 (FROM-TO 1 B)))),
which simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP B 0))
(EQUAL (FIX 0) (FIX B)))
(EQUAL (FROM-TO 0 B)
(CONS 0 (FROM-TO 1 B)))),
which simplifies, unfolding EQUAL, LESSP, FIX, FROM-TO, CONS, and NUMBERP,
to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP B 0))
(NOT (EQUAL (FIX 0) (FIX B)))
(EQUAL (FROM-TO 0 (SUB1 B))
(CONS 0 (FROM-TO 1 (SUB1 B)))))
(EQUAL (FROM-TO 0 B)
(CONS 0 (FROM-TO 1 B)))),
which simplifies, rewriting with the lemma CAR-CONS, and expanding the
functions EQUAL, LESSP, FIX, FROM-TO, NUMBERP, SUB1, and CONS, to two new
conjectures:
Case 1.2.
(IMPLIES (AND (NUMBERP B)
(NOT (EQUAL 0 B))
(EQUAL (FROM-TO 0 (SUB1 B))
(CONS 0 (FROM-TO 1 (SUB1 B))))
(NOT (EQUAL 1 B)))
(EQUAL (APPEND (FROM-TO 0 (SUB1 B)) (LIST B))
(CONS 0
(APPEND (FROM-TO 1 (SUB1 B))
(LIST B))))).
Applying the lemma SUB1-ELIM, replace B by (ADD1 X) to eliminate (SUB1 B).
We use the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove the following two
new formulas:
Case 1.2.2.
(IMPLIES (AND (EQUAL B 0)
(NUMBERP B)
(NOT (EQUAL 0 B))
(EQUAL (FROM-TO 0 (SUB1 B))
(CONS 0 (FROM-TO 1 (SUB1 B))))
(NOT (EQUAL 1 B)))
(EQUAL (APPEND (FROM-TO 0 (SUB1 B)) (LIST B))
(CONS 0
(APPEND (FROM-TO 1 (SUB1 B))
(LIST B))))).
This further simplifies, trivially, to:
T.
Case 1.2.1.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL 0 (ADD1 X)))
(EQUAL (FROM-TO 0 X)
(CONS 0 (FROM-TO 1 X)))
(NOT (EQUAL 1 (ADD1 X))))
(EQUAL (APPEND (FROM-TO 0 X) (LIST (ADD1 X)))
(CONS 0
(APPEND (FROM-TO 1 X)
(LIST (ADD1 X)))))).
However this further simplifies, applying the lemmas ADD1-EQUAL and
CAR-CONS, and opening up NUMBERP, to:
(IMPLIES (AND (NUMBERP X)
(EQUAL (FROM-TO 0 X)
(CONS 0 (FROM-TO 1 X)))
(NOT (EQUAL 0 X)))
(EQUAL (APPEND (FROM-TO 0 X) (LIST (ADD1 X)))
(CONS 0
(APPEND (FROM-TO 1 X)
(LIST (ADD1 X)))))).
We use the above equality hypothesis by substituting
(CONS 0 (FROM-TO 1 X)) for (FROM-TO 0 X) and throwing away the equality.
We thus obtain:
(IMPLIES (AND (NUMBERP X) (NOT (EQUAL 0 X)))
(EQUAL (APPEND (CONS 0 (FROM-TO 1 X))
(LIST (ADD1 X)))
(CONS 0
(APPEND (FROM-TO 1 X)
(LIST (ADD1 X)))))),
which further simplifies, applying CDR-CONS and CAR-CONS, and expanding
the function APPEND, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP B)
(NOT (EQUAL 0 B))
(EQUAL (FROM-TO 0 (SUB1 B))
(CONS 0 (FROM-TO 1 (SUB1 B))))
(EQUAL 1 B))
(EQUAL (APPEND (FROM-TO 0 (SUB1 B)) (LIST B))
'(0 1))).
This again simplifies, expanding NUMBERP, EQUAL, SUB1, FROM-TO, CONS, and
APPEND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FROM-TO-OPENS-AT-BTM
(PROVE-LEMMA MEMBER-FROM-TO
(REWRITE)
(EQUAL (MEMBER I (FROM-TO A B))
(AND (NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP B I))))
((INDUCT (FROM-TO A B))))
This formula can be simplified, using the abbreviations NOT, OR, and AND, to
the following three new goals:
Case 3. (IMPLIES (LESSP B A)
(EQUAL (MEMBER I (FROM-TO A B))
(AND (NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP B I))))).
This simplifies, opening up the definitions of FROM-TO, LISTP, MEMBER, NOT,
and AND, to:
(IMPLIES (AND (LESSP B A)
(NUMBERP I)
(NOT (LESSP I A)))
(LESSP B I)),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP B A))
(EQUAL (FIX A) (FIX B)))
(EQUAL (MEMBER I (FROM-TO A B))
(AND (NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP B I))))),
which simplifies, rewriting with FROM-TO-OPENS-AT-BTM, and expanding the
functions FIX, FROM-TO, NOT, AND, CONS, EQUAL, NUMBERP, LESSP, CDR, CAR,
LISTP, and MEMBER, to the following 11 new conjectures:
Case 2.11.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(NOT (NUMBERP I))
(NOT (LESSP A A)))
(EQUAL (MEMBER I (LIST A)) F)).
This again simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding
the definitions of MEMBER, LISTP, and EQUAL, to:
T.
Case 2.10.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(LESSP I A)
(NOT (LESSP A A)))
(EQUAL (MEMBER I (LIST A)) F)).
However this again simplifies, applying the lemmas CDR-CONS and CAR-CONS,
and opening up the definitions of MEMBER and LISTP, to:
(IMPLIES (AND (NUMBERP B)
(LESSP I B)
(NOT (LESSP B B)))
(NOT (EQUAL I B))).
This again simplifies, clearly, to:
T.
Case 2.9.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(LESSP A I)
(NOT (LESSP A A)))
(EQUAL (MEMBER I (LIST A)) F)).
But this again simplifies, rewriting with CDR-CONS and CAR-CONS, and
unfolding the definitions of MEMBER and LISTP, to:
(IMPLIES (AND (NUMBERP B)
(LESSP B I)
(NOT (LESSP B B)))
(NOT (EQUAL I B))),
which again simplifies, clearly, to:
T.
Case 2.8.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(NOT (NUMBERP I))
(LESSP A A))
(EQUAL (MEMBER I NIL) F)).
This again simplifies, obviously, to:
T.
Case 2.7.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(LESSP I A)
(LESSP A A))
(EQUAL (MEMBER I NIL) F)).
This again simplifies, clearly, to:
T.
Case 2.6.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(LESSP A I)
(LESSP A A))
(EQUAL (MEMBER I NIL) F)).
This again simplifies, clearly, to:
T.
Case 2.5.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP A I))
(NOT (LESSP A A)))
(EQUAL (MEMBER I (LIST A)) T)).
But this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (LESSP B B))
(NUMBERP B)
(NUMBERP B)
(NUMBERP B)
(NOT (LESSP B B))
(NOT (LESSP B B))
(NOT (LESSP B B)))
(EQUAL (MEMBER B (LIST B)) T)).
However this again simplifies, rewriting with the lemma CAR-CONS, and
unfolding the definitions of MEMBER and EQUAL, to:
T.
Case 2.4.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(EQUAL A B)
(NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP A I))
(LESSP A A))
(EQUAL (MEMBER I NIL) T)),
which again simplifies, clearly, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (LESSP B A))
(NOT (NUMBERP A))
(EQUAL 0 B)
(EQUAL I 0))
(NUMBERP I)).
This again simplifies, trivially, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (LESSP B A))
(NOT (NUMBERP B))
(EQUAL A 0)
(EQUAL I 0))
(NUMBERP I)).
This again simplifies, obviously, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (LESSP B A))
(NOT (NUMBERP B))
(NOT (NUMBERP A))
(EQUAL I 0))
(NUMBERP I)).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP B A))
(NOT (EQUAL (FIX A) (FIX B)))
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
(AND (NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP (SUB1 B) I)))))
(EQUAL (MEMBER I (FROM-TO A B))
(AND (NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP B I))))).
This simplifies, rewriting with SUB1-NNUMBERP, CDR-CONS, CAR-CONS, and
MEMBER-APPEND, and expanding FIX, LESSP, EQUAL, FROM-TO, LISTP, MEMBER, NOT,
and AND, to ten new formulas:
Case 1.10.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NOT (NUMBERP A))
(NOT (EQUAL 0 B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(EQUAL I B))
(NUMBERP I)),
which again simplifies, obviously, to:
T.
Case 1.9.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NOT (NUMBERP A))
(NOT (EQUAL 0 B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(EQUAL I B))
(NOT (LESSP B I))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.8.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NOT (NUMBERP A))
(NOT (EQUAL 0 B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(NOT (EQUAL I B))
(NUMBERP I))
(LESSP B I)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.7.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NOT (NUMBERP A))
(NOT (EQUAL 0 B))
(NUMBERP I)
(NOT (LESSP (SUB1 B) I))
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
T))
(NOT (LESSP B I))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL B 0)
(NOT (LESSP B A))
(NUMBERP B)
(NOT (NUMBERP A))
(NOT (EQUAL 0 B))
(NUMBERP I)
(NOT (LESSP (SUB1 B) I))
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
T))
(NOT (LESSP B I))).
This again simplifies, trivially, to:
T.
Case 1.6.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(LESSP I A)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F))
(NOT (EQUAL I B))).
This again simplifies, trivially, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(NOT (EQUAL I B))
(NUMBERP I)
(NOT (LESSP I A)))
(LESSP B I)).
This again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(EQUAL I B))
(NOT (LESSP B I))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(EQUAL I B))
(NOT (LESSP I A))),
which again simplifies, obviously, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(LESSP (SUB1 B) I)
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
F)
(EQUAL I B))
(NUMBERP I)).
This again simplifies, trivially, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP (SUB1 B) I))
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
T))
(NOT (LESSP B I))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL B 0)
(NOT (LESSP B A))
(NUMBERP B)
(NUMBERP A)
(NOT (EQUAL A B))
(NUMBERP I)
(NOT (LESSP I A))
(NOT (LESSP (SUB1 B) I))
(EQUAL (MEMBER I (FROM-TO A (SUB1 B)))
T))
(NOT (LESSP B I))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
MEMBER-FROM-TO
(PROVE-LEMMA FOR-SUM-PLUS
(REWRITE)
(EQUAL (FOR I RANGE TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I RANGE TEST 'SUM A ALIST)
(FOR I RANGE TEST 'SUM B ALIST)))
((ENABLE EVAL$)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP RANGE)
(p I RANGE TEST A B ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T TEST
(CONS (CONS I (CAR RANGE)) ALIST))
(p I (CDR RANGE) TEST A B ALIST))
(p I RANGE TEST A B ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T TEST
(CONS (CONS I (CAR RANGE)) ALIST)))
(p I (CDR RANGE) TEST A B ALIST))
(p I RANGE TEST A B ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT RANGE) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme produces the following three new formulas:
Case 3. (IMPLIES (NLISTP RANGE)
(EQUAL (FOR I RANGE TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I RANGE TEST 'SUM A ALIST)
(FOR I RANGE TEST 'SUM B ALIST)))).
This simplifies, unfolding the functions NLISTP, FOR,
QUANTIFIER-INITIAL-VALUE, PLUS, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T TEST
(CONS (CONS I (CAR RANGE)) ALIST))
(EQUAL (FOR I
(CDR RANGE)
TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I (CDR RANGE) TEST 'SUM A ALIST)
(FOR I
(CDR RANGE)
TEST 'SUM
B ALIST))))
(EQUAL (FOR I RANGE TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I RANGE TEST 'SUM A ALIST)
(FOR I RANGE TEST 'SUM B ALIST)))).
This simplifies, applying REWRITE-EVAL$, CAR-CONS, CDR-CONS,
ASSOCIATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and unfolding the
definitions of NLISTP, FOR, EQUAL, and QUANTIFIER-OPERATION, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T TEST
(CONS (CONS I (CAR RANGE)) ALIST)))
(EQUAL (FOR I
(CDR RANGE)
TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I (CDR RANGE) TEST 'SUM A ALIST)
(FOR I
(CDR RANGE)
TEST 'SUM
B ALIST))))
(EQUAL (FOR I RANGE TEST 'SUM
(LIST 'PLUS A B)
ALIST)
(PLUS (FOR I RANGE TEST 'SUM A ALIST)
(FOR I RANGE TEST 'SUM B ALIST)))),
which simplifies, opening up the functions NLISTP and FOR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FOR-SUM-PLUS
(PROVE-LEMMA TIMES-PLUS-DISTRIBUTIVITY-AGAIN
(REWRITE)
(EQUAL (TIMES (PLUS A B) C)
(PLUS (TIMES A C) (TIMES B C))))
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-PLUS-DISTRIBUTIVITY-AGAIN could!
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-PLUS-DISTRIBUTIVITY-AGAIN
(PROVE-LEMMA DIFFERENCE-SUB1-2
(REWRITE)
(IMPLIES (AND (NOT (ZEROP I))
(NOT (LESSP X I)))
(EQUAL (DIFFERENCE X (SUB1 I))
(ADD1 (DIFFERENCE X I)))))
This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP X I)))
(EQUAL (DIFFERENCE X (SUB1 I))
(ADD1 (DIFFERENCE X I)))).
This simplifies, using linear arithmetic, to the new goal:
(IMPLIES (AND (LESSP X (SUB1 I))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP X I)))
(EQUAL (DIFFERENCE X (SUB1 I))
(ADD1 (DIFFERENCE X I)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DIFFERENCE-SUB1-2
(PROVE-LEMMA OUT-WITH-THE-FACTORS
(REWRITE)
(IMPLIES (AND (NLISTP ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (EVAL$ (TRUE) ONE ALIST)
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST))))
((ENABLE EVAL$)))
This conjecture can be simplified, using the abbreviations NOT, NLISTP, AND,
and IMPLIES, to the formula:
(IMPLIES (AND (NOT (LISTP ONE))
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (EVAL$ T ONE ALIST)
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, opening up EQUAL and EVAL$, to the following two new
conjectures:
Case 2. (IMPLIES (AND (NOT (LISTP ONE))
(NOT (EQUAL ONE VAR))
(NOT (LITATOM ONE)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
Give the above formula the name *1.
Case 1. (IMPLIES (AND (NOT (LISTP ONE))
(NOT (EQUAL ONE VAR))
(LITATOM ONE))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This again simplifies, obviously, to:
(IMPLIES (AND (NOT (EQUAL ONE VAR))
(LITATOM ONE))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(IMPLIES (AND (NLISTP ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (EVAL$ T ONE ALIST)
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
named *1. Let us appeal to the induction principle. There are three
plausible inductions. They merge into two likely candidate inductions, both
of which are unflawed. So we will choose the one suggested by the largest
number of nonprimitive recursive functions. We will induct according to the
following scheme:
(AND (IMPLIES (LITATOM ONE)
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (LITATOM ONE)) (NLISTP ONE))
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (LITATOM ONE))
(NOT (NLISTP ONE))
(EQUAL (CAR ONE) 'QUOTE))
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (LITATOM ONE))
(NOT (NLISTP ONE))
(NOT (EQUAL (CAR ONE) 'QUOTE))
(p VAR RANGE CONDITION
(CDR ONE)
TWO ALIST))
(p VAR RANGE CONDITION ONE TWO ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP, CDR-LESSP, CAR-LESSEQP, and
CAR-LESSP, and the definition of NLISTP can be used to prove that the measure
(COUNT ONE) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates the
following two new conjectures:
Case 2. (IMPLIES (AND (LITATOM ONE)
(NLISTP ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (EVAL$ T ONE ALIST)
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, unfolding NLISTP, EVAL$, and EQUAL, to:
(IMPLIES (AND (LITATOM ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which we will name *1.1.
Case 1. (IMPLIES (AND (NOT (LITATOM ONE))
(NLISTP ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (EVAL$ T ONE ALIST)
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, unfolding the definitions of NLISTP, EVAL$, and EQUAL, to:
(IMPLIES (AND (NOT (LITATOM ONE))
(NOT (LISTP ONE))
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which we will name *1.2.
We will appeal to induction. The recursive terms in the conjecture
suggest three inductions. They merge into two likely candidate inductions,
both of which are unflawed. However, one of these is more likely than the
other. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP RANGE)
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST))
(p VAR
(CDR RANGE)
CONDITION ONE TWO ALIST))
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST)))
(p VAR
(CDR RANGE)
CONDITION ONE TWO ALIST))
(p VAR RANGE CONDITION ONE TWO ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT RANGE) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates the following three new conjectures:
Case 3. (IMPLIES (AND (NLISTP RANGE)
(NOT (LITATOM ONE))
(NOT (LISTP ONE))
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, and
opening up NLISTP, FOR, QUANTIFIER-INITIAL-VALUE, EQUAL, and TIMES, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST))
(EQUAL (FOR VAR
(CDR RANGE)
CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR
(CDR RANGE)
CONDITION 'SUM
TWO ALIST)))
(NOT (LITATOM ONE))
(NOT (LISTP ONE))
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, applying the lemmas REWRITE-EVAL$, CAR-CONS, CDR-CONS, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and expanding the definitions of NLISTP,
FOR, EQUAL, EVAL$, and QUANTIFIER-OPERATION, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST)))
(EQUAL (FOR VAR
(CDR RANGE)
CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR
(CDR RANGE)
CONDITION 'SUM
TWO ALIST)))
(NOT (LITATOM ONE))
(NOT (LISTP ONE))
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES ONE
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, unfolding the functions NLISTP and FOR, to:
T.
That finishes the proof of *1.2.
So we now return to:
(IMPLIES (AND (LITATOM ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which is formula *1.1 above. We will appeal to induction. Three inductions
are suggested by terms in the conjecture. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP RANGE)
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST))
(p VAR
(CDR RANGE)
CONDITION ONE TWO ALIST))
(p VAR RANGE CONDITION ONE TWO ALIST))
(IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST)))
(p VAR
(CDR RANGE)
CONDITION ONE TWO ALIST))
(p VAR RANGE CONDITION ONE TWO ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT RANGE) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following three new formulas:
Case 3. (IMPLIES (AND (NLISTP RANGE)
(LITATOM ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))).
This simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and opening up the
functions NLISTP, FOR, QUANTIFIER-INITIAL-VALUE, EQUAL, and TIMES, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP RANGE))
(EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST))
(EQUAL (FOR VAR
(CDR RANGE)
CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR
(CDR RANGE)
CONDITION 'SUM
TWO ALIST)))
(LITATOM ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which simplifies, applying the lemmas REWRITE-EVAL$, CAR-CONS, CDR-CONS, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and expanding the definitions of NLISTP,
FOR, ASSOC, EQUAL, EVAL$, and QUANTIFIER-OPERATION, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP RANGE))
(NOT (EVAL$ T CONDITION
(CONS (CONS VAR (CAR RANGE)) ALIST)))
(EQUAL (FOR VAR
(CDR RANGE)
CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR
(CDR RANGE)
CONDITION 'SUM
TWO ALIST)))
(LITATOM ONE)
(NOT (EQUAL ONE VAR)))
(EQUAL (FOR VAR RANGE CONDITION 'SUM
(LIST 'TIMES ONE TWO)
ALIST)
(TIMES (CDR (ASSOC ONE ALIST))
(FOR VAR RANGE CONDITION 'SUM
TWO ALIST)))),
which simplifies, expanding the functions NLISTP and FOR, to:
T.
That finishes the proof of *1.1, which finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
OUT-WITH-THE-FACTORS
(PROVE-LEMMA LESSP-1
(REWRITE)
(EQUAL (LESSP I 1) (ZEROP I)))
This simplifies, rewriting with EQUAL-LESSP, and unfolding ZEROP, to the
following three new conjectures:
Case 3. (IMPLIES (NOT (LESSP I 1))
(NUMBERP I)).
However this again simplifies, expanding the definitions of NUMBERP, EQUAL,
and LESSP, to:
T.
Case 2. (IMPLIES (NOT (LESSP I 1))
(NOT (EQUAL I 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP I 1) (NOT (EQUAL I 0)))
(NOT (NUMBERP I))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-1
(PROVE-LEMMA LESSP-CROCK1
(REWRITE)
(IMPLIES (NOT (ZEROP I))
(EQUAL (LESSP X (SUB1 I))
(AND (LESSP X I)
(NOT (EQUAL (FIX X) (SUB1 I)))))))
This conjecture can be simplified, using the abbreviations ZEROP, NOT, and
IMPLIES, to the formula:
(IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
(EQUAL (LESSP X (SUB1 I))
(AND (LESSP X I)
(NOT (EQUAL (FIX X) (SUB1 I)))))).
This simplifies, rewriting with EQUAL-LESSP, and expanding the functions FIX,
NOT, and AND, to five new conjectures:
Case 5. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP X (SUB1 I)))
(LESSP X I)
(NOT (NUMBERP X)))
(EQUAL 0 (SUB1 I))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL (PLUS 1 X) 0))
(NUMBERP (PLUS 1 X))
(NOT (LESSP X (SUB1 (PLUS 1 X))))
(LESSP X (PLUS 1 X))
(NOT (NUMBERP X)))
(EQUAL 0 (SUB1 (PLUS 1 X)))).
But this again simplifies, rewriting with PLUS-RIGHT-ID2 and LESSP-1, and
unfolding NUMBERP, EQUAL, SUB1, and LESSP, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP X (SUB1 I)))
(LESSP X I)
(NUMBERP X))
(EQUAL X (SUB1 I))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(LESSP X (SUB1 I))
(NUMBERP X))
(NOT (EQUAL X (SUB1 I)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(LESSP X (SUB1 I))
(NOT (NUMBERP X)))
(NOT (EQUAL 0 (SUB1 I)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(LESSP X (SUB1 I)))
(LESSP X I)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-CROCK1
(PROVE-LEMMA ZERO-SUM
(REWRITE)
(EQUAL (FOR I L COND 'SUM ''0 ALIST)
0)
((ENABLE EVAL$)))
Call the conjecture *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 (NLISTP L)
(p I L COND ALIST))
(IMPLIES (AND (NOT (NLISTP L))
(EVAL$ T COND
(CONS (CONS I (CAR L)) ALIST))
(p I (CDR L) COND ALIST))
(p I L COND ALIST))
(IMPLIES (AND (NOT (NLISTP L))
(NOT (EVAL$ T COND
(CONS (CONS I (CAR L)) ALIST)))
(p I (CDR L) COND ALIST))
(p I L COND ALIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates three new goals:
Case 3. (IMPLIES (NLISTP L)
(EQUAL (FOR I L COND 'SUM ''0 ALIST)
0)),
which simplifies, opening up the functions NLISTP, FOR,
QUANTIFIER-INITIAL-VALUE, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(EVAL$ T COND
(CONS (CONS I (CAR L)) ALIST))
(EQUAL (FOR I (CDR L) COND 'SUM ''0 ALIST)
0))
(EQUAL (FOR I L COND 'SUM ''0 ALIST)
0)),
which simplifies, applying EVAL$-QUOTE, and unfolding the functions NLISTP,
FOR, CAR, QUANTIFIER-OPERATION, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (EVAL$ T COND
(CONS (CONS I (CAR L)) ALIST)))
(EQUAL (FOR I (CDR L) COND 'SUM ''0 ALIST)
0))
(EQUAL (FOR I L COND 'SUM ''0 ALIST)
0)).
This simplifies, opening up the functions NLISTP, FOR, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ZERO-SUM
(PROVE-LEMMA SHIFT-INDICIAL-UP-CROCK
(REWRITE)
(IMPLIES (NOT (ZEROP N))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(TIMES (BC X (SUB1 I))
(EXP B (DIFFERENCE X I)))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(TIMES (BC X I)
(EXP B (DIFFERENCE X (ADD1 I)))))))))
This conjecture can be simplified, using the abbreviations ZEROP, NOT, IMPLIES,
and FROM-TO-OPENS-AT-BTM, to:
(IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(CONS 0 (FROM-TO 1 (SUB1 N)))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))).
This simplifies, rewriting with LESSP-1, ASSOCIATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, SUB1-ADD1, CAR-CONS, CDR-CONS, MEMBER-FROM-TO,
COMMUTATIVITY-OF-PLUS, COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, and
REWRITE-EVAL$, and expanding the functions CONS, NUMBERP, FROM-TO, EVAL$,
DIFFERENCE, EXP, MEMBER, QUANTIFIER-OPERATION, LESSP, EQUAL, TIMES, BC, and
FOR, to 14 new goals:
Case 14.(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(NOT (EQUAL 1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 N)) (LIST N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
(TIMES A (EXP B (SUB1 X)))))),
which again simplifies, rewriting with MEMBER-APPEND, CAR-CONS, CDR-CONS,
MEMBER-FROM-TO, LESSP-1, COMMUTATIVITY-OF-PLUS, ASSOCIATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, REWRITE-EVAL$, FOR-APPEND-SUM, and
OUT-WITH-THE-FACTORS, and expanding the functions LISTP, MEMBER, EVAL$,
QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR,
and EXP, to:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(NOT (EQUAL 1 N)))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 N))
(EXP A (SUB1 N))
(EXP B (DIFFERENCE X N))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
Applying the lemma DIFFERENCE-ELIM, replace X by (PLUS N Z) to eliminate
(DIFFERENCE X N). We rely upon the type restriction lemma noted when
DIFFERENCE was introduced to restrict the new variable. We would thus like
to prove the following two new formulas:
Case 14.2.
(IMPLIES
(AND (LESSP X N)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(NOT (EQUAL 1 N)))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 N))
(EXP A (SUB1 N))
(EXP B (DIFFERENCE X N))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
This further simplifies, using linear arithmetic, rewriting with
MEMBER-FROM-TO, LESSP-1, DIFFERENCE-0, EXP-BY-0, TIMES-1, and
COMMUTATIVITY-OF-TIMES, and unfolding EVAL$, to:
(IMPLIES
(AND (LESSP X N)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(NOT (EQUAL 1 N)))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 N))
(EXP A (SUB1 N))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X).
We use the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove the new conjecture:
(IMPLIES
(AND (NUMBERP Z)
(LESSP (ADD1 Z) N)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 N)))
(EQUAL
(PLUS (FOR 'I
(FROM-TO 1 (SUB1 N))
(LIST 'QUOTE T)
'SUM
'(TIMES (EXP A I)
(TIMES (BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'X (ADD1 Z))))
(TIMES A
(BC (ADD1 Z) (SUB1 N))
(EXP A (SUB1 N))))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR 'I
(FROM-TO 1 (SUB1 N))
(LIST 'QUOTE T)
'SUM
'(TIMES (BC X I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'X (ADD1 Z)))))))),
which further simplifies, applying SUB1-ADD1, LESSP-CROCK1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, LESSP-1, BC-X-X, BC-X-X1, and
COMMUTATIVITY2-OF-TIMES, and expanding LESSP, DIFFERENCE, BC, EVAL$, and
PLUS, to the following three new goals:
Case 14.2.3.
(IMPLIES
(AND (NUMBERP Z)
(LESSP Z N)
(NOT (EQUAL Z (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 N))
(EQUAL (SUB1 N) 0))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL (SUB1 I) 0)
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
1))
((LESSP Z I)
(COND ((EQUAL Z (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))
((EQUAL (ADD1 Z) (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))
(T (TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
0))))
(T (TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))))
(TIMES A (EXP A (SUB1 N)) 1))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (LESSP Z I)
(IF (EQUAL Z (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
(PLUS (BC Z I) (BC Z (SUB1 I))))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
0))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
(PLUS (BC Z I)
(BC Z (SUB1 I)))))))))).
But this finally simplifies, using linear arithmetic, to:
T.
Case 14.2.2.
(IMPLIES
(AND (NUMBERP Z)
(LESSP Z N)
(NOT (EQUAL Z (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 N))
(EQUAL (ADD1 Z) (SUB1 N)))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL (SUB1 I) 0)
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
1))
((LESSP Z I)
(COND ((EQUAL Z (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))
((EQUAL (ADD1 Z) (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))
(T (TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
0))))
(T (TIMES (EXP A I)
(EXP B (DIFFERENCE Z (SUB1 I)))
(PLUS (BC Z (SUB1 I))
(BC Z (SUB1 (SUB1 I))))))))
(TIMES A (EXP A (SUB1 N)) 1))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (LESSP Z I)
(IF (EQUAL Z (SUB1 I))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
(PLUS (BC Z I) (BC Z (SUB1 I))))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
0))
(TIMES (EXP A I)
(EXP B (DIFFERENCE Z I))
(PLUS (BC Z I)
(BC Z (SUB1 I)))))))))),
which again simplifies, using linear arithmetic, applying SUB1-ADD1,
ADD1-EQUAL, LESSP-1, BC-X-X1, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, BC-X-X,
DIFFERENCE-0, EXP-BY-0, TIMES-1, COMMUTATIVITY-OF-TIMES, MEMBER-APPEND,
CAR-CONS, CDR-CONS, MEMBER-FROM-TO, COMMUTATIVITY2-OF-TIMES,
DIFFERENCE-SUB1-2, COMMUTATIVITY-OF-PLUS, ASSOCIATIVITY-OF-PLUS,
ASSOCIATIVITY-OF-TIMES, REWRITE-EVAL$, COMMUTATIVITY2-OF-PLUS,
FOR-APPEND-SUM, TIMES-PLUS-DISTRIBUTIVITY-AGAIN, FOR-SUM-PLUS, and
CORRECTNESS-OF-CANCEL, and unfolding the functions NUMBERP, FROM-TO,
TIMES, PLUS, DIFFERENCE, EQUAL, EXP, LISTP, MEMBER, EVAL$,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR, LESSP,
and BC, to:
(IMPLIES
(AND (NUMBERP Z)
(LESSP Z N)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 N))
(EQUAL (ADD1 Z) (SUB1 N)))
(EQUAL (PLUS (TIMES A (EXP A Z))
(FOR I IN
(FROM-TO 1 Z)
SUM
(IF (EQUAL (SUB1 I) 0)
(IF (NUMBERP A) (TIMES A (EXP B Z)) 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B (DIFFERENCE Z I))))))
(TIMES A (EXP A Z) (BC Z (SUB1 Z))))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (BC Z I)
(EXP A I)
(EXP B (DIFFERENCE Z I)))))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))))))).
Applying the lemma SUB1-ELIM, replace N by (ADD1 V) to eliminate
(SUB1 N). We employ the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. We thus obtain:
(IMPLIES
(AND (NUMBERP V)
(NUMBERP Z)
(LESSP Z (ADD1 V))
(NOT (EQUAL (ADD1 V) 0))
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 (ADD1 V)))
(EQUAL (ADD1 Z) V))
(EQUAL (PLUS (TIMES A (EXP A Z))
(FOR I IN
(FROM-TO 1 Z)
SUM
(IF (EQUAL (SUB1 I) 0)
(IF (NUMBERP A) (TIMES A (EXP B Z)) 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B (DIFFERENCE Z I))))))
(TIMES A (EXP A Z) (BC Z (SUB1 Z))))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (BC Z I)
(EXP A I)
(EXP B (DIFFERENCE Z I)))))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))))))),
which further simplifies, applying the lemmas SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, LESSP-1, DIFFERENCE-0,
COMMUTATIVITY-OF-PLUS, and MEMBER-FROM-TO, and opening up the functions
LESSP, NUMBERP, EXP, APPEND, LISTP, FROM-TO, CONS, DIFFERENCE, EQUAL,
EVAL$, and BC, to nine new formulas:
Case 14.2.2.9.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 Z))
(NOT (NUMBERP B))
(NOT (NUMBERP A)))
(EQUAL
(PLUS (TIMES A 0)
(TIMES A 0)
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A 0)
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))),
which finally simplifies, using linear arithmetic, to:
T.
Case 14.2.2.8.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 Z))
(NOT (NUMBERP B))
(NUMBERP A))
(EQUAL
(PLUS (TIMES A A)
(TIMES A A)
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A 0)
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))),
which finally simplifies, using linear arithmetic, to:
T.
Case 14.2.2.7.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 Z))
(NUMBERP B)
(NOT (NUMBERP A)))
(EQUAL
(PLUS (TIMES A 0)
(TIMES A 0)
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A B)
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))),
which finally simplifies, using linear arithmetic, to:
T.
Case 14.2.2.6.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(NOT (EQUAL 1 Z))
(NUMBERP B)
(NUMBERP A))
(EQUAL
(PLUS (TIMES A A)
(TIMES A A)
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A B)
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
(LIST Z)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))),
which finally simplifies, using linear arithmetic, to:
T.
Case 14.2.2.5.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(EQUAL 1 Z)
(NOT (NUMBERP B))
(NOT (NUMBERP A)))
(EQUAL
(PLUS (TIMES A 0)
(TIMES A 0)
(FOR I IN
'(1)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A 0)
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))),
which finally simplifies, applying TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
ZERO-SUM, EXP-BY-0, and TIMES-1, and opening up NUMBERP, SUB1, EQUAL,
MEMBER, LISTP, CAR, CDR, EVAL$, PLUS, TIMES, EXP, and BC, to:
T.
Case 14.2.2.4.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(EQUAL 1 Z)
(NOT (NUMBERP B))
(NUMBERP A))
(EQUAL
(PLUS (TIMES A A)
(TIMES A A)
(FOR I IN
'(1)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A 0)
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))).
However this finally simplifies, applying COMMUTATIVITY-OF-TIMES,
ZERO-SUM, COMMUTATIVITY-OF-PLUS, EXP-BY-0, TIMES-1, REWRITE-EVAL$, and
CORRECTNESS-OF-CANCEL, and unfolding the definitions of NUMBERP, SUB1,
EQUAL, TIMES, MEMBER, LISTP, CAR, CDR, EVAL$, PLUS, EXP, BC,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, FOR, CONS, and
FIX, to:
T.
Case 14.2.2.3.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(EQUAL 1 Z)
(NUMBERP B)
(NOT (NUMBERP A)))
(EQUAL
(PLUS (TIMES A 0)
(TIMES A 0)
(FOR I IN
'(1)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A B)
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))).
This finally simplifies, rewriting with TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, ZERO-SUM, EXP-BY-0, and TIMES-1, and opening
up the functions NUMBERP, SUB1, EQUAL, MEMBER, LISTP, CAR, CDR, EVAL$,
PLUS, TIMES, EXP, and BC, to:
T.
Case 14.2.2.2.
(IMPLIES
(AND (NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(NOT (EQUAL Z 0))
(EQUAL 1 Z)
(NUMBERP B)
(NUMBERP A))
(EQUAL
(PLUS (TIMES A A)
(TIMES A A)
(FOR I IN
'(1)
SUM
(COND ((EQUAL (SUB1 I) 0)
(IF (NUMBERP A)
(IF (NUMBERP B)
(TIMES A B)
(TIMES A 0))
0))
((EQUAL I 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z))))
((NUMBERP I)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B 0))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B 0))))
(T (PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B Z))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B Z)))))))
(PLUS (TIMES A B)
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (BC Z I) (EXP A I) (EXP B Z)))
((NUMBERP I)
(TIMES (BC Z I) (EXP A I) (EXP B 0)))
(T (TIMES (BC Z I)
(EXP A I)
(EXP B Z))))))
(TIMES A
(FOR I IN
'(1)
SUM
(COND ((EQUAL I 0)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z)))
((NUMBERP I)
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B 0)))
(T (TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B Z))))))))).
However this finally simplifies, rewriting with REWRITE-EVAL$,
COMMUTATIVITY-OF-PLUS, OUT-WITH-THE-FACTORS, EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, and COMMUTATIVITY2-OF-PLUS, and opening up
NUMBERP, SUB1, EQUAL, MEMBER, LISTP, CAR, CDR, EVAL$,
QUANTIFIER-OPERATION, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, FOR, CONS,
EXP, BC, and TIMES, to:
T.
Case 14.2.2.1.
(IMPLIES
(AND (NUMBERP Z)
(LESSP (SUB1 (SUB1 Z)) Z)
(NOT (EQUAL Z 0)))
(EQUAL (PLUS (TIMES A (EXP A Z))
(FOR I IN
(FROM-TO 1 Z)
SUM
(IF (EQUAL (SUB1 I) 0)
(IF (NUMBERP A) (TIMES A (EXP B Z)) 0)
(PLUS (TIMES B
(EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))
(TIMES B
(EXP A I)
(BC Z (SUB1 (SUB1 I)))
(EXP B (DIFFERENCE Z I))))))
(TIMES A (EXP A Z) (BC Z (SUB1 Z))))
(PLUS (TIMES A (EXP B Z))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (BC Z I)
(EXP A I)
(EXP B (DIFFERENCE Z I)))))
(TIMES A
(FOR I IN
(FROM-TO 1 Z)
SUM
(TIMES (EXP A I)
(BC Z (SUB1 I))
(EXP B (DIFFERENCE Z I)))))))),
which we would usually push and work on later by induction. But if we
must use induction to prove the input conjecture, we prefer to induct
on the original formulation of the problem. Thus we will disregard
all that we have previously done, give the name *1 to the original
input, and work on it.
So now let us consider:
(IMPLIES (NOT (ZEROP N))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))),
which we named *1 above. We will appeal to induction. There is only one
plausible induction. We will induct according to the following scheme:
(AND (IMPLIES (LESSP N 1) (p N A B X))
(IMPLIES (AND (NOT (LESSP N 1))
(EQUAL (FIX 1) (FIX N)))
(p N A B X))
(IMPLIES (AND (NOT (LESSP N 1))
(NOT (EQUAL (FIX 1) (FIX N)))
(p (SUB1 N) A B X))
(p N A B X))).
Linear arithmetic, the lemmas COUNT-NUMBERP, SUB1-NNUMBERP, and
COUNT-NOT-LESSP, and the definitions of LESSP, EQUAL, COUNT, and FIX can be
used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces four new goals:
Case 4. (IMPLIES (AND (LESSP N 1) (NOT (ZEROP N)))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))),
which simplifies, applying the lemma LESSP-1, and unfolding ZEROP, to:
T.
Case 3. (IMPLIES (AND (NOT (LESSP N 1))
(EQUAL (FIX 1) (FIX N))
(NOT (ZEROP N)))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))),
which simplifies, rewriting with LESSP-1, DIFFERENCE-1, EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, and REWRITE-EVAL$, and
expanding the functions FIX, ZEROP, FROM-TO, BC, EXP, EQUAL, NUMBERP, SUB1,
MEMBER, LISTP, CAR, CDR, EVAL$, QUANTIFIER-OPERATION, PLUS,
QUANTIFIER-INITIAL-VALUE, ASSOC, FOR, TIMES, CONS, and ADD1, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP N 1))
(NOT (EQUAL (FIX 1) (FIX N)))
(ZEROP (SUB1 N))
(NOT (ZEROP N)))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))).
This simplifies, applying LESSP-1, MEMBER-APPEND, CAR-CONS, CDR-CONS,
MEMBER-FROM-TO, COMMUTATIVITY-OF-PLUS, EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, REWRITE-EVAL$, FOR-APPEND-SUM, and DIFFERENCE-1, and
opening up FIX, ZEROP, FROM-TO, NUMBERP, LISTP, MEMBER, LESSP, EQUAL, EVAL$,
FOR, CDR, ASSOC, QUANTIFIER-INITIAL-VALUE, QUANTIFIER-OPERATION, PLUS, BC,
EXP, SUB1, ADD1, CAR, TIMES, and CONS, to two new goals:
Case 2.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 N) 0)
(NOT (NUMBERP A)))
(EQUAL (TIMES 0 (EXP B (DIFFERENCE X N)))
0)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 N) 0)
(NUMBERP A))
(EQUAL (TIMES A (EXP B (DIFFERENCE X N)))
(TIMES A (EXP B (SUB1 X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP N 1))
(NOT (EQUAL (FIX 1) (FIX N)))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))
(NOT (ZEROP N)))
(EQUAL (FOR I IN
(FROM-TO 1 N)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(FOR I IN
(FROM-TO 0 (SUB1 N))
SUM
(TIMES (EXP A (ADD1 I))
(BC X I)
(EXP B (DIFFERENCE X (ADD1 I))))))),
which simplifies, using linear arithmetic, rewriting with LESSP-1,
MEMBER-FROM-TO, FROM-TO-OPENS-AT-BTM, ASSOCIATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, SUB1-ADD1, CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-PLUS, COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0,
REWRITE-EVAL$, MEMBER-APPEND, FOR-APPEND-SUM, OUT-WITH-THE-FACTORS,
DIFFERENCE-0, LESSP-CROCK1, and ZERO-SUM, and unfolding FIX, EVAL$,
DIFFERENCE, EXP, MEMBER, QUANTIFIER-OPERATION, LESSP, EQUAL, TIMES, BC,
NUMBERP, CONS, FOR, ZEROP, FROM-TO, LISTP, PLUS, QUANTIFIER-INITIAL-VALUE,
ASSOC, CDR, and SUB1, to the following 13 new formulas:
Case 1.13.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
(TIMES A (EXP B (SUB1 X)))))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 N))
(EXP B (DIFFERENCE X N))
A
(EXP A (SUB1 (SUB1 N)))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
However this again simplifies, applying MEMBER-FROM-TO, LESSP-1,
REWRITE-EVAL$, OUT-WITH-THE-FACTORS, COMMUTATIVITY-OF-PLUS,
COMMUTATIVITY-OF-TIMES, and COMMUTATIVITY2-OF-TIMES, and opening up the
definitions of EVAL$ and EQUAL, to the new formula:
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(EQUAL
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A A
(BC X (SUB1 N))
(EXP A (SUB1 (SUB1 N)))
(EXP B (DIFFERENCE X N))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))),
which further simplifies, appealing to the lemmas LESSP-1, MEMBER-FROM-TO,
MEMBER-APPEND, CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-PLUS,
ASSOCIATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES, REWRITE-EVAL$,
FOR-APPEND-SUM, ASSOCIATIVITY-OF-PLUS, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
DIFFERENCE-1, EXP-BY-0, TIMES-1, and COMMUTATIVITY-OF-TIMES, and unfolding
the definitions of CONS, NUMBERP, FROM-TO, EVAL$, LISTP, MEMBER,
QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR,
FOR, EXP, BC, SUB1, CAR, TIMES, and DIFFERENCE, to two new formulas:
Case 1.13.2.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL
(FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 (SUB1 N)))
(EXP A (SUB1 (SUB1 N)))
(EXP B (DIFFERENCE X (SUB1 N))))
(TIMES A A
(BC X (SUB1 N))
(EXP A (SUB1 (SUB1 N)))
(EXP B (DIFFERENCE X N))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))
(TIMES A A
(BC X (SUB1 N))
(EXP A (SUB1 (SUB1 N)))
(EXP B
(DIFFERENCE (SUB1 X) (SUB1 N))))))),
which again simplifies, rewriting with MEMBER-APPEND, CAR-CONS, CDR-CONS,
MEMBER-FROM-TO, LESSP-1, COMMUTATIVITY-OF-PLUS, ASSOCIATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, REWRITE-EVAL$, FOR-APPEND-SUM, and
CORRECTNESS-OF-CANCEL, and opening up the definitions of LISTP, MEMBER,
EVAL$, QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE,
ASSOC, CDR, FOR, EXP, and DIFFERENCE, to:
T.
Case 1.13.1.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(EQUAL 1 (SUB1 N))
(EQUAL
(FOR I IN
'(1)
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))
(NOT (NUMBERP A)))
(EQUAL (PLUS 0
(TIMES A A
(BC X 1)
(EXP B (SUB1 (SUB1 X)))))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A 0)))).
But this again simplifies, applying DIFFERENCE-1, EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, ZERO-SUM, and TIMES-ZERO2, and unfolding the
definitions of TIMES, BC, EXP, EQUAL, NUMBERP, SUB1, MEMBER, LISTP, CAR,
CDR, EVAL$, FROM-TO, FOR, ASSOC, QUANTIFIER-INITIAL-VALUE, and PLUS, to:
T.
Case 1.12.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 X) 0))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
(TIMES A (EXP B (SUB1 X)))))
(EQUAL (SUB1 N) 0))
(EQUAL
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(TIMES A
(BC X (SUB1 N))
(EXP B (DIFFERENCE X N))
1))
(PLUS (TIMES A (EXP B (SUB1 X)))
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.11.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(EQUAL X (SUB1 N)))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
(TIMES A 1 A (EXP A (SUB1 (SUB1 N)))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))),
which again simplifies, rewriting with EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, LESSP-CROCK1, LESSP-1, and
COMMUTATIVITY-OF-PLUS, and unfolding the definitions of TIMES, DIFFERENCE,
BC, EXP, NUMBERP, EQUAL, LESSP, EVAL$, FROM-TO, MEMBER, LISTP, FOR, CDR,
ASSOC, QUANTIFIER-INITIAL-VALUE, and PLUS, to:
T.
Case 1.10.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N))))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
(TIMES A 0 A (EXP A (SUB1 (SUB1 N)))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))).
However this again simplifies, using linear arithmetic, rewriting with the
lemmas COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0,
MEMBER-FROM-TO, LESSP-1, REWRITE-EVAL$, OUT-WITH-THE-FACTORS, and
COMMUTATIVITY-OF-PLUS, and unfolding DIFFERENCE, LESSP, EQUAL, EVAL$,
TIMES, and PLUS, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N))))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))).
This further simplifies, rewriting with LESSP-1, MEMBER-FROM-TO,
MEMBER-APPEND, CAR-CONS, CDR-CONS, ASSOCIATIVITY-OF-TIMES, LESSP-CROCK1,
COMMUTATIVITY-OF-PLUS, REWRITE-EVAL$, FOR-APPEND-SUM, EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, CORRECTNESS-OF-CANCEL, and EQUAL-TIMES-0, and
opening up the definitions of CONS, NUMBERP, FROM-TO, EVAL$, LISTP, MEMBER,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR, PLUS,
LESSP, EQUAL, BC, EXP, TIMES, SUB1, CAR, and FIX, to the following seven
new conjectures:
Case 1.10.7.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I)))))
(EQUAL (SUB1 (SUB1 N)) 0))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 1))
(PLUS A (TIMES A 0)))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.10.6.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I)))))
(EQUAL X (SUB1 (SUB1 N))))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 1))
(PLUS A (TIMES A 0)))),
which again simplifies, applying LESSP-1, LESSP-CROCK1,
COMMUTATIVITY-OF-PLUS, MEMBER-APPEND, CAR-CONS, CDR-CONS, EXP-BY-0,
TIMES-1, COMMUTATIVITY-OF-TIMES, REWRITE-EVAL$, FOR-APPEND-SUM, and
BC-X-X, and expanding the definitions of APPEND, LISTP, FROM-TO, CONS,
NUMBERP, PLUS, LESSP, EQUAL, BC, MEMBER, EVAL$, TIMES, EXP,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR, SUB1,
and CAR, to:
T.
Case 1.10.5.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I)))))
(NOT (EQUAL (SUB1 (SUB1 N)) 0))
(NOT (EQUAL X (SUB1 (SUB1 N)))))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 0))
(PLUS A (TIMES A 0)))).
But this again simplifies, applying MEMBER-APPEND, CAR-CONS, CDR-CONS,
MEMBER-FROM-TO, LESSP-1, ASSOCIATIVITY-OF-TIMES, COMMUTATIVITY-OF-TIMES,
LESSP-CROCK1, REWRITE-EVAL$, COMMUTATIVITY-OF-PLUS, FOR-APPEND-SUM,
TIMES-ZERO2, EXP-OF-0, and ZERO-SUM, and expanding the functions LISTP,
MEMBER, EVAL$, QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC,
CDR, FOR, TIMES, BC, LESSP, EQUAL, NUMBERP, EXP, PLUS, and CONS, to:
T.
Case 1.10.4.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))
(EQUAL (SUB1 (SUB1 N)) 0))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 1))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.10.3.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))
(EQUAL X (SUB1 (SUB1 N))))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 1))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))),
which again simplifies, applying LESSP-1, LESSP-CROCK1,
COMMUTATIVITY-OF-PLUS, MEMBER-APPEND, CAR-CONS, CDR-CONS, EXP-BY-0,
TIMES-1, COMMUTATIVITY-OF-TIMES, REWRITE-EVAL$, FOR-APPEND-SUM, and
BC-X-X, and unfolding the definitions of APPEND, LISTP, FROM-TO, CONS,
NUMBERP, PLUS, LESSP, EQUAL, BC, MEMBER, EVAL$, TIMES, EXP,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR, SUB1,
and CAR, to:
T.
Case 1.10.2.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(NOT (EQUAL 1 (SUB1 N)))
(EQUAL (FOR I IN
(APPEND (FROM-TO 1 (SUB1 (SUB1 N)))
(LIST (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL (SUB1 N) 0))
(NOT (EQUAL X (SUB1 N)))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))
(NOT (EQUAL (SUB1 (SUB1 N)) 0))
(NOT (EQUAL X (SUB1 (SUB1 N)))))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(TIMES A (EXP A (SUB1 (SUB1 N))) 0))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))).
This again simplifies, rewriting with MEMBER-APPEND, CAR-CONS, CDR-CONS,
MEMBER-FROM-TO, LESSP-1, ASSOCIATIVITY-OF-TIMES, COMMUTATIVITY-OF-TIMES,
LESSP-CROCK1, REWRITE-EVAL$, COMMUTATIVITY-OF-PLUS, FOR-APPEND-SUM, and
PLUS-RIGHT-ID2, and unfolding the definitions of LISTP, MEMBER, EVAL$,
QUANTIFIER-OPERATION, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR, TIMES,
BC, LESSP, EQUAL, NUMBERP, EXP, and PLUS, to:
T.
Case 1.10.1.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL 1 (SUB1 N))
(EQUAL (FOR I IN
'(1)
SUM
(TIMES (EXP A I) (BC X (SUB1 I))))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(TIMES (BC X I) (EXP A I))))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(EQUAL 0 A)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.9.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (SUB1 N) 0))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
(TIMES A 1 1))
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.8.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(EQUAL X 0)
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
0)
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))),
which again simplifies, using linear arithmetic, applying
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, LESSP-CROCK1,
MEMBER-FROM-TO, LESSP-1, ZERO-SUM, and COMMUTATIVITY-OF-PLUS, and
expanding the definitions of SUB1, EQUAL, BC, LESSP, NUMBERP, EVAL$, PLUS,
TIMES, and EXP, to the following two new goals:
Case 1.8.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))))
(EQUAL 0 A)).
But this again simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and opening up the
definitions of TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.8.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))
A)).
This again simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and expanding the
definitions of TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.7.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (NUMBERP X))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
0)
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))).
However this again simplifies, using linear arithmetic, rewriting with
SUB1-NNUMBERP, COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0,
LESSP-CROCK1, MEMBER-FROM-TO, LESSP-1, ZERO-SUM, and COMMUTATIVITY-OF-PLUS,
and opening up the definitions of EQUAL, BC, LESSP, EVAL$, PLUS, TIMES,
and EXP, to the following two new formulas:
Case 1.7.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (NUMBERP X))
(NOT (EQUAL (SUB1 N) 0))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))))
(EQUAL 0 A)).
However this again simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and unfolding the
functions TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.7.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (NUMBERP X))
(NOT (EQUAL (SUB1 N) 0))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))
A)).
But this again simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and expanding TIMES,
EQUAL, EXP, and EVAL$, to:
T.
Case 1.6.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(EQUAL X 0)
(EQUAL (SUB1 N) 0))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
A)
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.5.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL (SUB1 X) 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (NUMBERP X))
(EQUAL (SUB1 N) 0))
(EQUAL (PLUS (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(COND ((EQUAL X 0)
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
((NUMBERP X)
(TIMES (EXP A I) (BC X (SUB1 I))))
((EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I)))
(T (TIMES 0 (EXP A I)))))
A)
(PLUS A
(TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC X I) (EXP A I))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (NUMBERP X))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL (PLUS 0
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))
A)),
which again simplifies, using linear arithmetic, applying
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, LESSP-CROCK1,
MEMBER-FROM-TO, LESSP-1, and ZERO-SUM, and expanding BC, LESSP, EVAL$,
EQUAL, and PLUS, to the following two new formulas:
Case 1.4.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (NUMBERP X))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))))
(EQUAL 0 A)).
This again simplifies, applying the lemmas EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and opening up the
functions TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.4.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (NUMBERP X))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))
A)),
which again simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and expanding TIMES,
EQUAL, EXP, and EVAL$, to:
T.
Case 1.3.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NOT (NUMBERP X))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(EQUAL (SUB1 N) 0))
(EQUAL (PLUS A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))
A)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL X 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(NOT (EQUAL (SUB1 N) 0)))
(EQUAL (PLUS 0
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))
A)),
which again simplifies, using linear arithmetic, applying
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, LESSP-CROCK1,
MEMBER-FROM-TO, LESSP-1, and ZERO-SUM, and opening up BC, EQUAL, LESSP,
NUMBERP, EVAL$, and PLUS, to the following two new conjectures:
Case 1.2.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NOT (NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))))
(EQUAL 0 A)).
But this again simplifies, rewriting with EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and unfolding the
definitions of TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.2.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0)
(TIMES 1 (EXP A I))
(TIMES 0 (EXP A I))))
A)
(NOT (EQUAL (SUB1 N) 0))
(NUMBERP (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))))
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0))
A)).
But this again simplifies, rewriting with EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, MEMBER-FROM-TO, and LESSP-1, and opening up
TIMES, EQUAL, EXP, and EVAL$, to:
T.
Case 1.1.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL 1 N))
(EQUAL X 0)
(NUMBERP A)
(EQUAL (FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC X (SUB1 I))
(EXP B (DIFFERENCE X I))))
(PLUS (FOR I IN
(FROM-TO 1 (SUB1 (SUB1 N)))
SUM
(COND ((EQUAL X 0) 0)
((NUMBERP X)
(TIMES A
(BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(T 0)))
A))
(EQUAL (SUB1 N) 0))
(EQUAL (PLUS A
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(IF (EQUAL (SUB1 I) 0) A 0)))
A)).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 4.6 0.1 ]
SHIFT-INDICIAL-UP-CROCK
(PROVE-LEMMA GOAL1
(REWRITE)
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(NOT (EQUAL 1 X))
(NOT (EQUAL (SUB1 X) 0)))
(EQUAL (TIMES A
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE X I))))))
(TIMES A
(TIMES B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(TIMES (EXP A I)
(EXP B
(DIFFERENCE (SUB1 X) I))))))))))
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed GOAL1 could!
.
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X). We
employ the type restriction lemma noted when SUB1 was introduced to restrict
the new variable. We would thus like to prove the new formula:
(IMPLIES
(AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL 1 (ADD1 Z)))
(NOT (EQUAL Z 0)))
(EQUAL (TIMES A
(FOR 'I
(FROM-TO 1 Z)
(LIST 'QUOTE T)
'SUM
'(TIMES (BC X I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE X I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'X (ADD1 Z)))))
(TIMES A B
(FOR 'I
(FROM-TO 1 Z)
(LIST 'QUOTE T)
'SUM
'(TIMES (BC X I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'X (ADD1 Z))))))),
which simplifies, applying ADD1-EQUAL, TIMES-PLUS-DISTRIBUTIVITY-AGAIN,
COMMUTATIVITY2-OF-TIMES, DIFFERENCE-SUB1-2, SUB1-ADD1, LESSP-CROCK1,
MEMBER-FROM-TO, LESSP-1, REWRITE-EVAL$, OUT-WITH-THE-FACTORS, FOR-SUM-PLUS,
and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and unfolding the functions NUMBERP,
EXP, DIFFERENCE, BC, LESSP, EVAL$, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
GOAL1
(PROVE-LEMMA NEWTON
(REWRITE)
(EQUAL (EXP (PLUS A B) N)
(FOR I IN
(FROM-TO 0 N)
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I)))))
((INDUCT (EXP A N))))
This formula can be simplified, using the abbreviations ZEROP, NOT, OR, AND,
and FROM-TO-OPENS-AT-BTM, to the following two new goals:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (EXP (PLUS A B) N)
(FOR I IN
(CONS 0 (FROM-TO 1 N))
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I)))))).
This simplifies, using linear arithmetic, applying EXP-BY-0, LESSP-1, and
DIFFERENCE-0, and opening up the definitions of ZEROP, FROM-TO, CONS, TIMES,
DIFFERENCE, BC, MEMBER, LISTP, CAR, CDR, EVAL$, QUANTIFIER-OPERATION, FOR,
EQUAL, and EXP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EXP (PLUS A B) (SUB1 N))
(FOR 'I
(CONS 0 (FROM-TO 1 (SUB1 N)))
(LIST 'QUOTE T)
'SUM
'(TIMES (BC N I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE N I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'N (SUB1 N))))))
(EQUAL (EXP (PLUS A B) N)
(FOR I IN
(CONS 0 (FROM-TO 1 N))
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I)))))),
which simplifies, rewriting with the lemmas COMMUTATIVITY2-OF-TIMES,
CAR-CONS, CDR-CONS, LESSP-1, MEMBER-FROM-TO, TIMES-1, EXP-BY-0,
REWRITE-EVAL$, TIMES-PLUS-DISTRIBUTIVITY-AGAIN, COMMUTATIVITY-OF-TIMES,
DIFFERENCE-0, and CORRECTNESS-OF-CANCEL, and unfolding the functions MEMBER,
EVAL$, QUANTIFIER-OPERATION, DIFFERENCE, BC, EQUAL, CONS, FOR, EXP, NUMBERP,
FROM-TO, APPEND, LISTP, LESSP, and FIX, to six new goals:
Case 1.6.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS (EXP B (SUB1 N))
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(NOT (EQUAL 1 N)))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) (SUB1 N)))
(TIMES B (EXP (PLUS A B) (SUB1 N))))
(PLUS (TIMES B (EXP B (SUB1 N)))
(FOR I IN
(APPEND (FROM-TO 1 (SUB1 N)) (LIST N))
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I))))))),
which again simplifies, using linear arithmetic, applying the lemmas
MEMBER-FROM-TO, LESSP-1, MEMBER-APPEND, CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, BC-X-X,
COMMUTATIVITY-OF-PLUS, REWRITE-EVAL$, FOR-APPEND-SUM, and
COMMUTATIVITY2-OF-PLUS, and expanding EVAL$, LISTP, MEMBER,
QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR,
FOR, and EXP, to the formula:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS (EXP B (SUB1 N))
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(NOT (EQUAL 1 N)))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) (SUB1 N)))
(TIMES B (EXP (PLUS A B) (SUB1 N))))
(PLUS (TIMES A (EXP A (SUB1 N)))
(TIMES B (EXP B (SUB1 N)))
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I))))))).
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. This generates the goal:
(IMPLIES
(AND
(NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL X 0))
(EQUAL (EXP (PLUS A B) X)
(PLUS (EXP B X)
(FOR 'I
(FROM-TO 1 X)
(LIST 'QUOTE T)
'SUM
'(TIMES (EXP A I)
(TIMES (BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'N (ADD1 X))))))
(NOT (EQUAL 1 (ADD1 X))))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP B X))
(FOR 'I
(FROM-TO 1 X)
(LIST 'QUOTE T)
'SUM
'(TIMES (BC N I)
(TIMES (EXP A I)
(EXP B (DIFFERENCE N I))))
(LIST (CONS 'A A)
(CONS 'B B)
(CONS 'N (ADD1 X))))))).
However this further simplifies, rewriting with COMMUTATIVITY2-OF-TIMES,
SUB1-ADD1, MEMBER-FROM-TO, LESSP-1, ADD1-EQUAL,
TIMES-PLUS-DISTRIBUTIVITY-AGAIN, DIFFERENCE-SUB1-2, LESSP-CROCK1,
REWRITE-EVAL$, OUT-WITH-THE-FACTORS, FROM-TO-OPENS-AT-BTM,
ASSOCIATIVITY-OF-TIMES, CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-PLUS, TIMES-1,
EXP-BY-0, COMMUTATIVITY-OF-TIMES, SHIFT-INDICIAL-UP-CROCK,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and FOR-SUM-PLUS, and unfolding the
functions EVAL$, NUMBERP, EXP, DIFFERENCE, BC, LESSP, EQUAL, MEMBER,
QUANTIFIER-OPERATION, CONS, and FOR, to the following three new goals:
Case 1.6.3.
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL (EXP (PLUS A B) X)
(PLUS (EXP B X)
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(NOT (EQUAL (SUB1 X) 0)))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP B X))
(TIMES B
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))
(TIMES B A (EXP B (SUB1 X)))))).
But this again simplifies, using linear arithmetic, applying the lemmas
LESSP-1, MEMBER-APPEND, CAR-CONS, CDR-CONS, MEMBER-FROM-TO,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, BC-X-X,
COMMUTATIVITY-OF-PLUS, REWRITE-EVAL$, FOR-APPEND-SUM,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY2-OF-TIMES,
COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and opening up the
functions EXP, CONS, NUMBERP, FROM-TO, EVAL$, LISTP, MEMBER,
QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR,
FOR, and SUB1, to:
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(NOT (EQUAL 1 X))
(EQUAL (EXP (PLUS A B) X)
(PLUS (TIMES B (EXP B (SUB1 X)))
(FOR I IN
(APPEND (FROM-TO 1 (SUB1 X)) (LIST X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(NOT (EQUAL (SUB1 X) 0)))
(EQUAL
(PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP A X))
(TIMES A B (EXP B (SUB1 X)))
(TIMES B B (EXP B (SUB1 X)))
(TIMES B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
This again simplifies, using linear arithmetic, rewriting with the
lemmas MEMBER-APPEND, CAR-CONS, CDR-CONS, MEMBER-FROM-TO, LESSP-1,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, DIFFERENCE-0, BC-X-X,
COMMUTATIVITY-OF-PLUS, REWRITE-EVAL$, FOR-APPEND-SUM, and
COMMUTATIVITY2-OF-PLUS, and expanding the definitions of LISTP, MEMBER,
EVAL$, QUANTIFIER-OPERATION, EQUAL, PLUS, QUANTIFIER-INITIAL-VALUE,
ASSOC, CDR, and FOR, to:
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(NOT (EQUAL 1 X))
(EQUAL (EXP (PLUS A B) X)
(PLUS (EXP A X)
(TIMES B (EXP B (SUB1 X)))
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(NOT (EQUAL (SUB1 X) 0)))
(EQUAL
(PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP A X))
(TIMES A B (EXP B (SUB1 X)))
(TIMES B B (EXP B (SUB1 X)))
(TIMES B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))).
We use the above equality hypothesis by substituting:
(PLUS (EXP A X)
(TIMES B (EXP B (SUB1 X)))
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
for (EXP (PLUS A B) X) and throwing away the equality. We thus obtain:
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(NOT (EQUAL 1 X))
(NOT (EQUAL (SUB1 X) 0)))
(EQUAL
(PLUS (TIMES A
(PLUS (EXP A X)
(TIMES B (EXP B (SUB1 X)))
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(TIMES B
(PLUS (EXP A X)
(TIMES B (EXP B (SUB1 X)))
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP A X))
(TIMES A B (EXP B (SUB1 X)))
(TIMES B B (EXP B (SUB1 X)))
(TIMES B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))))),
which finally simplifies, rewriting with MEMBER-FROM-TO, LESSP-1, GOAL1,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and unfolding the
function EVAL$, to:
T.
Case 1.6.2.
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL (EXP (PLUS A B) X)
(PLUS (EXP B X)
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(EQUAL (SUB1 X) 0)
(NUMBERP A))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP B X))
(TIMES B
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))
(TIMES B A)))).
This again simplifies, using linear arithmetic, rewriting with
TIMES-PLUS-DISTRIBUTIVITY-AGAIN, COMMUTATIVITY-OF-TIMES, TIMES-1,
EXP-BY-0, LESSP-1, DIFFERENCE-0, CORRECTNESS-OF-CANCEL,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS,
ASSOCIATIVITY-OF-PLUS, BC-X-X, CAR-CONS, CDR-CONS, COMMUTATIVITY-OF-PLUS,
and REWRITE-EVAL$, and unfolding the functions EXP, APPEND, LISTP,
FROM-TO, CONS, NUMBERP, DIFFERENCE, LESSP, EQUAL, EVAL$, FIX, BC, MEMBER,
QUANTIFIER-OPERATION, PLUS, QUANTIFIER-INITIAL-VALUE, ASSOC, CDR, FOR,
TIMES, SUB1, and CAR, to the following two new goals:
Case 1.6.2.2.
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(NOT (EQUAL 1 X))
(EQUAL A
(FIX (FOR I IN
(LIST X)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC X I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))
(EQUAL (SUB1 X) 0)
(NOT (NUMBERP B)))
(EQUAL (TIMES A 0) (TIMES A B))).
But this finally simplifies, using linear arithmetic, to:
T.
Case 1.6.2.1.
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL 1 X)
(EQUAL A
(FIX (FOR I IN
'(1)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC X I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))
(NOT (NUMBERP B)))
(EQUAL (TIMES A 0) (TIMES A B))),
which finally simplifies, applying EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, REWRITE-EVAL$, and
TIMES-ZERO2, and opening up NUMBERP, EQUAL, EXP, SUB1, BC, MEMBER,
LISTP, CAR, CDR, EVAL$, QUANTIFIER-OPERATION, PLUS,
QUANTIFIER-INITIAL-VALUE, ASSOC, FOR, CONS, FIX, and TIMES, to:
T.
Case 1.6.1.
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL X 0))
(EQUAL (EXP (PLUS A B) X)
(PLUS (EXP B X)
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I))))))
(EQUAL (SUB1 X) 0)
(NOT (NUMBERP A)))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) X))
(TIMES B (EXP (PLUS A B) X)))
(PLUS (TIMES A (EXP A X))
(TIMES B (EXP B X))
(TIMES B
(FOR I IN
(FROM-TO 1 X)
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE X I)))))
(TIMES A B
(FOR I IN
(FROM-TO 1 (SUB1 X))
SUM
(TIMES (BC X I)
(EXP A I)
(EXP B (DIFFERENCE (SUB1 X) I)))))
(TIMES B 0)))).
However this again simplifies, using linear arithmetic, rewriting with
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, LESSP-1, DIFFERENCE-0,
CORRECTNESS-OF-CANCEL, TIMES-ZERO2, BC-X-X, CAR-CONS, CDR-CONS,
REWRITE-EVAL$, COMMUTATIVITY-OF-PLUS, and ZERO-SUM, and expanding PLUS,
EXP, APPEND, LISTP, FROM-TO, CONS, NUMBERP, DIFFERENCE, LESSP, EQUAL,
TIMES, EVAL$, BC, MEMBER, QUANTIFIER-OPERATION, FOR, CDR, ASSOC,
QUANTIFIER-INITIAL-VALUE, SUB1, and CAR, to:
T.
Case 1.5.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS (EXP B (SUB1 N))
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(EQUAL 1 N))
(EQUAL (PLUS (TIMES A (EXP (PLUS A B) (SUB1 N)))
(TIMES B (EXP (PLUS A B) (SUB1 N))))
(PLUS (TIMES B (EXP B (SUB1 N)))
(FOR I IN
'(1)
SUM
(TIMES (BC N I)
(EXP A I)
(EXP B (DIFFERENCE N I))))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (SUB1 N) 0)
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS 1
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(NOT (EQUAL 1 N))
(NOT (NUMBERP A)))
(EQUAL 0
(FIX (FOR I IN
(LIST N)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC N I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (SUB1 N) 0)
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS 1
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(NOT (EQUAL 1 N))
(NUMBERP A))
(EQUAL A
(FIX (FOR I IN
(LIST N)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC N I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (SUB1 N) 0)
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS 1
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(EQUAL 1 N)
(NOT (NUMBERP A)))
(EQUAL 0
(FIX (FOR I IN
'(1)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC N I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))),
which again simplifies, appealing to the lemmas EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, and ZERO-SUM, and expanding the definitions of
EQUAL, NUMBERP, SUB1, PLUS, FROM-TO, MEMBER, LISTP, FOR, CDR, ASSOC,
QUANTIFIER-INITIAL-VALUE, TIMES, EXP, BC, CAR, EVAL$, and FIX, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (SUB1 N) 0)
(EQUAL (EXP (PLUS A B) (SUB1 N))
(PLUS 1
(FOR I IN
(FROM-TO 1 (SUB1 N))
SUM
(TIMES (EXP A I)
(BC (SUB1 N) I)
(EXP B (DIFFERENCE (SUB1 N) I))))))
(EQUAL 1 N)
(NUMBERP A))
(EQUAL A
(FIX (FOR I IN
'(1)
SUM
(COND ((EQUAL I 0) (IF (NUMBERP B) B 0))
((NUMBERP I)
(TIMES (BC N I) (EXP A I)))
((NUMBERP B) B)
(T 0)))))),
which again simplifies, rewriting with EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, and REWRITE-EVAL$, and
unfolding the definitions of EQUAL, NUMBERP, SUB1, FROM-TO, MEMBER, LISTP,
FOR, CDR, ASSOC, QUANTIFIER-INITIAL-VALUE, PLUS, EXP, BC, CAR, EVAL$,
QUANTIFIER-OPERATION, CONS, and FIX, to:
T.
Q.E.D.
[ 0.0 1.4 0.0 ]
NEWTON