(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