(BOOT-STRAP NQTHM) Nqthm-1992 mods: (PC-NQTHM-1992) [ 0.1 0.1 0.0 ] GROUND-ZERO (PROVE-LEMMA PLUS-RIGHT-ID2 (REWRITE) (IMPLIES (NOT (NUMBERP Y)) (EQUAL (PLUS X Y) (FIX X)))) This simplifies, unfolding the definition of FIX, to the following two new goals: Case 2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (PLUS X Y) 0)). This again simplifies, opening up the definitions of PLUS and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (PLUS X Y) X)), which we will name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition of ZEROP 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 two new formulas: Case 2. (IMPLIES (AND (ZEROP X) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (PLUS X Y) X)). This simplifies, expanding the functions ZEROP, NUMBERP, EQUAL, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (PLUS (SUB1 X) Y) (SUB1 X)) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (PLUS X Y) X)). This simplifies, using linear arithmetic, to the new conjecture: (IMPLIES (AND (EQUAL X 0) (NOT (ZEROP X)) (EQUAL (PLUS (SUB1 X) Y) (SUB1 X)) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (PLUS X Y) X)), which again simplifies, expanding the function ZEROP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-RIGHT-ID2 (PROVE-LEMMA PLUS-ADD1 (REWRITE) (EQUAL (PLUS X (ADD1 Y)) (IF (NUMBERP Y) (ADD1 (PLUS X Y)) (ADD1 X)))) This simplifies, obviously, to two new formulas: Case 2. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (PLUS X (ADD1 Y)) (ADD1 X))), which again simplifies, rewriting with the lemma SUB1-TYPE-RESTRICTION, to the conjecture: (IMPLIES (NOT (NUMBERP Y)) (EQUAL (PLUS X 1) (ADD1 X))). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (NUMBERP Y) (EQUAL (PLUS X (ADD1 Y)) (ADD1 (PLUS X Y)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-ADD1 (PROVE-LEMMA COMMUTATIVITY2-OF-PLUS (REWRITE) (EQUAL (PLUS X Y Z) (PLUS Y X Z))) This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COMMUTATIVITY2-OF-PLUS (PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE) (EQUAL (PLUS X Y) (PLUS Y X))) WARNING: the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the previously added lemma COMMUTATIVITY2-OF-PLUS could. WARNING: the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the previously added lemma PLUS-ADD1 could. WARNING: the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the previously added lemma PLUS-RIGHT-ID2 could. This formula simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COMMUTATIVITY-OF-PLUS (PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X Y Z))) WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the newly proposed ASSOCIATIVITY-OF-PLUS could! This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-PLUS (PROVE-LEMMA PLUS-EQUAL-0 (REWRITE) (EQUAL (EQUAL (PLUS A B) 0) (AND (ZEROP A) (ZEROP B)))) This simplifies, opening up the functions ZEROP and AND, to six new conjectures: Case 6. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0)) (NOT (NUMBERP A))) (NOT (EQUAL B 0))), which again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and unfolding the functions NUMBERP and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0)) (NOT (NUMBERP A))) (NUMBERP B)). However this again simplifies, applying PLUS-RIGHT-ID2, and unfolding the function EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0)) (EQUAL A 0)) (NOT (EQUAL B 0))). This again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0)) (EQUAL A 0)) (NUMBERP B)), which again simplifies, applying the lemma PLUS-RIGHT-ID2, and opening up the definitions of NUMBERP and EQUAL, to: T. Case 2. (IMPLIES (AND (EQUAL (PLUS A B) 0) (NOT (EQUAL A 0))) (NOT (NUMBERP A))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (EQUAL (PLUS A B) 0) (NOT (EQUAL B 0))) (NOT (NUMBERP B))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-EQUAL-0 (PROVE-LEMMA DIFFERENCE-X-X (REWRITE) (EQUAL (DIFFERENCE X X) 0)) This conjecture simplifies, using linear arithmetic, to: (IMPLIES (LESSP X X) (EQUAL (DIFFERENCE X X) 0)). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-X-X (PROVE-LEMMA DIFFERENCE-PLUS (REWRITE) (AND (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y)))) WARNING: Note that the proposed lemma DIFFERENCE-PLUS is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviation AND, to the following two new conjectures: Case 2. (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y)). This simplifies, unfolding the function FIX, to the following two new formulas: Case 2.2. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (DIFFERENCE (PLUS X Y) X) 0)). However this again simplifies, applying PLUS-RIGHT-ID2, to the following two new goals: Case 2.2.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 X) 0)). But this again simplifies, expanding EQUAL and DIFFERENCE, to: T. Case 2.2.1. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X X) 0)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X X) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X X) 0)). However this again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (NUMBERP Y) (EQUAL (DIFFERENCE (PLUS X Y) X) Y)), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (LESSP (PLUS X Y) X) (NUMBERP Y)) (EQUAL (DIFFERENCE (PLUS X Y) X) Y)). This again simplifies, using linear arithmetic, to: T. Case 1. (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y)), which simplifies, applying the lemma COMMUTATIVITY-OF-PLUS, and unfolding FIX, to two new conjectures: Case 1.2. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (DIFFERENCE (PLUS X Y) X) 0)), which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, to two new formulas: Case 1.2.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 X) 0)), which again simplifies, expanding the definitions of EQUAL and DIFFERENCE, to: T. Case 1.2.1. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X X) 0)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X X) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X X) 0)). However this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (NUMBERP Y) (EQUAL (DIFFERENCE (PLUS X Y) X) Y)), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP (PLUS X Y) X) (NUMBERP Y)) (EQUAL (DIFFERENCE (PLUS X Y) X) Y)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS (PROVE-LEMMA PLUS-CANCELLATION (REWRITE) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) (EQUAL (FIX B) (FIX C)))) This conjecture simplifies, expanding the definition of FIX, to the following seven new formulas: Case 7. (IMPLIES (AND (NUMBERP C) (NUMBERP B) (NOT (EQUAL B C))) (NOT (EQUAL (PLUS A B) (PLUS A C)))). This again simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (NUMBERP C) (NOT (NUMBERP B)) (NOT (EQUAL 0 C))) (NOT (EQUAL (PLUS A B) (PLUS A C)))), which again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two new conjectures: Case 6.2. (IMPLIES (AND (NUMBERP C) (NOT (NUMBERP B)) (NOT (EQUAL 0 C)) (NOT (NUMBERP A))) (NOT (EQUAL 0 (PLUS A C)))). This again simplifies, using linear arithmetic, to: T. Case 6.1. (IMPLIES (AND (NUMBERP C) (NOT (NUMBERP B)) (NOT (EQUAL 0 C)) (NUMBERP A)) (NOT (EQUAL A (PLUS A C)))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (NUMBERP C)) (NUMBERP B) (NOT (EQUAL B 0))) (NOT (EQUAL (PLUS A B) (PLUS A C)))), which again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two new goals: Case 5.2. (IMPLIES (AND (NOT (NUMBERP C)) (NUMBERP B) (NOT (EQUAL B 0)) (NOT (NUMBERP A))) (NOT (EQUAL (PLUS A B) 0))). This again simplifies, using linear arithmetic, to: T. Case 5.1. (IMPLIES (AND (NOT (NUMBERP C)) (NUMBERP B) (NOT (EQUAL B 0)) (NUMBERP A)) (NOT (EQUAL (PLUS A B) A))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (NUMBERP C)) (NOT (NUMBERP B))) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) T)), which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, and opening up EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (NUMBERP C)) (EQUAL B 0)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) T)), which again simplifies, rewriting with COMMUTATIVITY-OF-PLUS and PLUS-RIGHT-ID2, and expanding the functions EQUAL and PLUS, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP B)) (EQUAL 0 C)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) T)). This again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and opening up EQUAL and PLUS, to: T. Case 1. (IMPLIES (AND (NUMBERP C) (NUMBERP B) (EQUAL B C)) (EQUAL (EQUAL (PLUS A B) (PLUS A C)) T)). But this again simplifies, expanding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-CANCELLATION (PROVE-LEMMA DIFFERENCE-0 (REWRITE) (IMPLIES (NOT (LESSP Y X)) (EQUAL (DIFFERENCE X Y) 0))) Name the conjecture *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p (SUB1 X) (SUB1 Y))) (p X Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT can be used to show that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for X. The above induction scheme leads to the following four new goals: Case 4. (IMPLIES (AND (OR (EQUAL X 0) (NOT (NUMBERP X))) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, expanding the definitions of NOT, OR, EQUAL, LESSP, and DIFFERENCE, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL Y 0) (NOT (NUMBERP Y))) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, unfolding NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (LESSP (SUB1 Y) (SUB1 X)) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (LESSP (SUB1 Y) (SUB1 X)) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, using linear arithmetic, to three new conjectures: Case 1.3. (IMPLIES (AND (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, using linear arithmetic, to two new conjectures: Case 1.3.2. (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y)) (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, unfolding the functions LESSP, NOT, OR, DIFFERENCE, and EQUAL, to: T. Case 1.3.1. (IMPLIES (AND (LESSP X 1) (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1.2. (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y)) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, expanding the definitions of NOT, OR, LESSP, DIFFERENCE, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-0 (PROVE-LEMMA EQUAL-DIFFERENCE-0 (REWRITE) (EQUAL (EQUAL 0 (DIFFERENCE X Y)) (NOT (LESSP Y X)))) This conjecture simplifies, unfolding NOT, to two new conjectures: Case 2. (IMPLIES (NOT (EQUAL 0 (DIFFERENCE X Y))) (LESSP Y X)), which again simplifies, rewriting with the lemma DIFFERENCE-0, and opening up the definition of EQUAL, to: T. Case 1. (IMPLIES (EQUAL 0 (DIFFERENCE X Y)) (NOT (LESSP Y X))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-DIFFERENCE-0 (PROVE-LEMMA DIFFERENCE-CANCELLATION-0 (REWRITE) (EQUAL (EQUAL X (DIFFERENCE X Y)) (AND (NUMBERP X) (OR (EQUAL X 0) (ZEROP Y))))) This simplifies, opening up the functions ZEROP, OR, and AND, to five new goals: Case 5. (IMPLIES (EQUAL X (DIFFERENCE X Y)) (NUMBERP X)), which again simplifies, obviously, to: T. Case 4. (IMPLIES (AND (EQUAL X (DIFFERENCE X Y)) (NOT (EQUAL X 0)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))). But this again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (LESSP X Y) (EQUAL X (DIFFERENCE X Y)) (NOT (EQUAL X 0)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))). This again simplifies, using linear arithmetic and applying DIFFERENCE-0, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y))) (NUMBERP X)) (NUMBERP Y)). But this again simplifies, expanding the definition of DIFFERENCE, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y))) (NUMBERP X)) (NOT (EQUAL Y 0))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X 0) (NOT (EQUAL X (DIFFERENCE X 0)))) (NOT (NUMBERP X))). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y))) (NUMBERP X)) (NOT (EQUAL X 0))), which again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-0, and expanding EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-CANCELLATION-0 (PROVE-LEMMA DIFFERENCE-CANCELLATION-1 (REWRITE) (EQUAL (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (IF (LESSP X Y) (NOT (LESSP Y Z)) (IF (LESSP Z Y) (NOT (LESSP Y X)) (EQUAL (FIX X) (FIX Z)))))) This simplifies, opening up NOT and FIX, to the following 11 new goals: Case 11.(IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NOT (NUMBERP Z)) (NUMBERP X)) (EQUAL (EQUAL X 0) T)). This again simplifies, using linear arithmetic, applying DIFFERENCE-0 and EQUAL-DIFFERENCE-0, and expanding LESSP, to the following two new conjectures: Case 11.2. (IMPLIES (AND (NOT (LESSP Y X)) (NOT (LESSP X Y)) (EQUAL Y 0) (NOT (NUMBERP Z)) (NUMBERP X)) (EQUAL X 0)). But this again simplifies, using linear arithmetic, to: T. Case 11.1. (IMPLIES (AND (NOT (LESSP Y X)) (NOT (LESSP X Y)) (NOT (NUMBERP Y)) (NOT (NUMBERP Z)) (NUMBERP X)) (EQUAL X 0)), which again simplifies, unfolding the definition of LESSP, to: T. Case 10.(IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NUMBERP Z) (NOT (NUMBERP X))) (EQUAL (EQUAL 0 Z) T)), which again simplifies, using linear arithmetic, rewriting with DIFFERENCE-0 and EQUAL-DIFFERENCE-0, and opening up the functions LESSP and EQUAL, to the following two new formulas: Case 10.2. (IMPLIES (AND (NOT (LESSP Y Z)) (EQUAL Y 0) (NUMBERP Z) (NOT (NUMBERP X))) (EQUAL 0 Z)). But this again simplifies, using linear arithmetic, to: T. Case 10.1. (IMPLIES (AND (NOT (LESSP Y Z)) (NOT (NUMBERP Y)) (NUMBERP Z) (NOT (NUMBERP X))) (EQUAL 0 Z)), which again simplifies, expanding the function LESSP, to: T. Case 9. (IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NUMBERP Z) (NUMBERP X)) (EQUAL (EQUAL X Z) T)), which again simplifies, obviously, to the new formula: (IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NUMBERP Z) (NUMBERP X)) (EQUAL X Z)), which again simplifies, using linear arithmetic, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NOT (NUMBERP Z))) (NOT (EQUAL X 0))), which again simplifies, using linear arithmetic, appealing to the lemma DIFFERENCE-0, and unfolding the function EQUAL, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NOT (NUMBERP X))) (NOT (EQUAL 0 Z))), which again simplifies, using linear arithmetic, applying DIFFERENCE-0, and unfolding the function EQUAL, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NUMBERP Z) (NUMBERP X)) (NOT (EQUAL X Z))). This again simplifies, clearly, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (LESSP X Y)) (LESSP Y Z)). However this again simplifies, using linear arithmetic, applying DIFFERENCE-0, and expanding the function EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (NOT (LESSP Z Y)) (NOT (NUMBERP Z))) (NUMBERP X)). However this again simplifies, using linear arithmetic, applying DIFFERENCE-0, and unfolding the definition of EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (LESSP Z Y)) (LESSP Y X)). But this again simplifies, using linear arithmetic, to three new goals: Case 3.3. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (LESSP Z Y)) (LESSP Y X)), which again simplifies, appealing to the lemma DIFFERENCE-0, and expanding the definitions of DIFFERENCE and LESSP, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y))) (NOT (LESSP X Y)) (LESSP Z Y)) (LESSP Y X)), which again simplifies, using linear arithmetic, applying DIFFERENCE-0, and unfolding the function EQUAL, to: T. Case 3.1. (IMPLIES (AND (NUMBERP X) (NUMBERP Y) (NOT (EQUAL (DIFFERENCE X X) (DIFFERENCE Z X))) (NOT (LESSP X X)) (LESSP Z X)) (LESSP X X)). However this again simplifies, using linear arithmetic, applying DIFFERENCE-0, and expanding the function EQUAL, to: T. Case 2. (IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (LESSP X Y)) (NOT (LESSP Y Z))). However this again simplifies, using linear arithmetic and rewriting with the lemmas DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to: T. Case 1. (IMPLIES (AND (EQUAL (DIFFERENCE X Y) (DIFFERENCE Z Y)) (NOT (LESSP X Y)) (LESSP Z Y)) (NOT (LESSP Y X))), which again simplifies, using linear arithmetic and rewriting with DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-CANCELLATION-1 (PROVE-LEMMA TIMES-ZERO2 (REWRITE) (IMPLIES (NOT (NUMBERP Y)) (EQUAL (TIMES X Y) 0))) Call the conjecture *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to prove 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 two new goals: Case 2. (IMPLIES (AND (ZEROP X) (NOT (NUMBERP Y))) (EQUAL (TIMES X Y) 0)), which simplifies, opening up the definitions of ZEROP, EQUAL, and TIMES, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) Y) 0) (NOT (NUMBERP Y))) (EQUAL (TIMES X Y) 0)), which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and unfolding ZEROP, TIMES, NUMBERP, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-ZERO2 (PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (REWRITE) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z)))) Call the conjecture *1. We will try to prove it by induction. There are four plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y Z)) (p X Y Z))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 generates two new goals: Case 2. (IMPLIES (ZEROP X) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z)))), which simplifies, opening up the functions ZEROP, EQUAL, TIMES, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) (PLUS Y Z)) (PLUS (TIMES (SUB1 X) Y) (TIMES (SUB1 X) Z)))) (EQUAL (TIMES X (PLUS Y Z)) (PLUS (TIMES X Y) (TIMES X Z)))), which simplifies, applying ASSOCIATIVITY-OF-PLUS and COMMUTATIVITY2-OF-PLUS, and unfolding the functions ZEROP and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] DISTRIBUTIVITY-OF-TIMES-OVER-PLUS (PROVE-LEMMA TIMES-ADD1 (REWRITE) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X)))) This conjecture simplifies, unfolding the definition of FIX, to three new conjectures: Case 3. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (TIMES X (ADD1 Y)) X)), which again simplifies, rewriting with SUB1-TYPE-RESTRICTION, to the new formula: (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (TIMES X 1) X)), which we will name *1. Case 2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (TIMES X (ADD1 Y)) 0)). However this again simplifies, applying SUB1-TYPE-RESTRICTION, and opening up the definitions of TIMES and EQUAL, to: T. Case 1. (IMPLIES (NUMBERP Y) (EQUAL (TIMES X (ADD1 Y)) (PLUS X (TIMES X Y)))), 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: (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X))), which we named *1 above. We will appeal to induction. The recursive terms in the conjecture suggest three inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following two new formulas: Case 2. (IMPLIES (ZEROP X) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X)))). This simplifies, rewriting with PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and expanding the definitions of ZEROP, EQUAL, TIMES, PLUS, FIX, and NUMBERP, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (IF (NUMBERP Y) (PLUS (SUB1 X) (TIMES (SUB1 X) Y)) (FIX (SUB1 X))))) (EQUAL (TIMES X (ADD1 Y)) (IF (NUMBERP Y) (PLUS X (TIMES X Y)) (FIX X)))), which simplifies, applying SUB1-TYPE-RESTRICTION and SUB1-ADD1, and unfolding the functions ZEROP, FIX, TIMES, and PLUS, to the following two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (NUMBERP Y)) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (SUB1 X))) (EQUAL (TIMES X 1) X)). But this further simplifies, rewriting with SUB1-TYPE-RESTRICTION, and unfolding TIMES, to the new formula: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (NUMBERP Y)) (EQUAL (TIMES (SUB1 X) 1) (SUB1 X))) (EQUAL (PLUS 1 (SUB1 X)) X)), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NUMBERP Y) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (PLUS (SUB1 X) (TIMES (SUB1 X) Y)))) (EQUAL (ADD1 (PLUS Y (TIMES (SUB1 X) (ADD1 Y)))) (PLUS X Y (TIMES (SUB1 X) Y)))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-ADD1 (PROVE-LEMMA COMMUTATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES X Y) (TIMES Y X))) WARNING: the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the previously added lemma TIMES-ADD1 could. WARNING: the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the previously added lemma DISTRIBUTIVITY-OF-TIMES-OVER-PLUS could. WARNING: the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the previously added lemma TIMES-ZERO2 could. Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture, both of which are flawed. We limit our consideration to the two suggested by the largest number of nonprimitive recursive functions in the conjecture. Since both of these are equally likely, we will choose arbitrarily. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 produces the following two new conjectures: Case 2. (IMPLIES (ZEROP X) (EQUAL (TIMES X Y) (TIMES Y X))). This simplifies, applying TIMES-ZERO2, and opening up the functions ZEROP, EQUAL, and TIMES, to: (IMPLIES (EQUAL X 0) (EQUAL 0 (TIMES Y 0))). This again simplifies, obviously, to: (EQUAL 0 (TIMES Y 0)), which we will name *1.1. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) Y) (TIMES Y (SUB1 X)))) (EQUAL (TIMES X Y) (TIMES Y X))). This simplifies, unfolding the definitions of ZEROP and TIMES, to the new goal: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (TIMES (SUB1 X) Y) (TIMES Y (SUB1 X)))) (EQUAL (PLUS Y (TIMES Y (SUB1 X))) (TIMES Y X))). 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. This produces the new goal: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (TIMES Z Y) (TIMES Y Z))) (EQUAL (PLUS Y (TIMES Y Z)) (TIMES Y (ADD1 Z)))), which further simplifies, applying the lemma TIMES-ADD1, to: T. So we now return to: (EQUAL 0 (TIMES Y 0)), which is formula *1.1 above. 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 Y) (p Y)) (IMPLIES (AND (NOT (ZEROP Y)) (p (SUB1 Y))) (p Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces two new conjectures: Case 2. (IMPLIES (ZEROP Y) (EQUAL 0 (TIMES Y 0))), which simplifies, unfolding ZEROP, TIMES, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (EQUAL 0 (TIMES (SUB1 Y) 0))) (EQUAL 0 (TIMES Y 0))), which simplifies, unfolding the definitions of ZEROP, TIMES, PLUS, and EQUAL, to: T. That finishes the proof of *1.1, which, in turn, finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] COMMUTATIVITY-OF-TIMES (PROVE-LEMMA COMMUTATIVITY2-OF-TIMES (REWRITE) (EQUAL (TIMES X Y Z) (TIMES Y X Z))) WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed COMMUTATIVITY2-OF-TIMES could! Call the conjecture *1. Perhaps we can prove it by induction. Four inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions, both of which are unflawed. Since both of these are equally likely, we will choose arbitrarily. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Y) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP Y)) (p X (SUB1 Y) Z)) (p X Y Z))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to prove that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP Y) (EQUAL (TIMES X Y Z) (TIMES Y X Z))), which simplifies, applying the lemma COMMUTATIVITY-OF-TIMES, and opening up the definitions of ZEROP, EQUAL, and TIMES, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (EQUAL (TIMES X (SUB1 Y) Z) (TIMES (SUB1 Y) X Z))) (EQUAL (TIMES X Y Z) (TIMES Y X Z))), which simplifies, rewriting with DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and opening up the functions ZEROP and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] COMMUTATIVITY2-OF-TIMES (PROVE-LEMMA ASSOCIATIVITY-OF-TIMES (REWRITE) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X Y Z))) WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed ASSOCIATIVITY-OF-TIMES could! This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and COMMUTATIVITY2-OF-TIMES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-TIMES (PROVE-LEMMA EQUAL-TIMES-0 (REWRITE) (EQUAL (EQUAL (TIMES X Y) 0) (OR (ZEROP X) (ZEROP Y)))) This simplifies, opening up the functions ZEROP and OR, to five new conjectures: Case 5. (IMPLIES (NOT (EQUAL (TIMES X Y) 0)) (NUMBERP Y)), which again simplifies, applying TIMES-ZERO2, and unfolding the function EQUAL, to: T. Case 4. (IMPLIES (NOT (EQUAL (TIMES X Y) 0)) (NOT (EQUAL Y 0))). However this again simplifies, applying COMMUTATIVITY-OF-TIMES, and unfolding the functions EQUAL and TIMES, to: T. Case 3. (IMPLIES (NOT (EQUAL (TIMES X Y) 0)) (NUMBERP X)). This again simplifies, opening up the definitions of TIMES and EQUAL, to: T. Case 2. (IMPLIES (NOT (EQUAL (TIMES X Y) 0)) (NOT (EQUAL X 0))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (EQUAL (TIMES X Y) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p Y X)) (IMPLIES (AND (NOT (ZEROP X)) (p Y (SUB1 X))) (p Y X))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 produces three new conjectures: Case 3. (IMPLIES (AND (ZEROP X) (EQUAL (TIMES X Y) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, unfolding the function ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (TIMES (SUB1 X) Y) 0)) (EQUAL (TIMES X Y) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, rewriting with the lemma PLUS-EQUAL-0, and expanding the functions ZEROP and TIMES, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (SUB1 X) 0) (EQUAL (TIMES X Y) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, rewriting with the lemma PLUS-EQUAL-0, and expanding the definitions of ZEROP and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-TIMES-0 (DEFN EXP (I J) (IF (ZEROP J) 1 (TIMES I (EXP I (SUB1 J))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT J) decreases according to the well-founded relation LESSP in each recursive call. Hence, EXP is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (EXP I J)) is a theorem. [ 0.0 0.0 0.0 ] EXP (PROVE-LEMMA EXP-PLUS (REWRITE) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K)))) Call the conjecture *1. We will try to prove it by induction. There are three plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p I J K)) (IMPLIES (AND (NOT (ZEROP J)) (p I (SUB1 J) K)) (p I J K))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition of ZEROP inform us that the measure (COUNT J) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (ZEROP J) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K)))), which simplifies, opening up the functions ZEROP, EQUAL, PLUS, and EXP, to four new formulas: Case 2.4. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K))) (EQUAL (EXP I 0) (TIMES 1 (EXP I K)))), which again simplifies, opening up EQUAL, EXP, and TIMES, to: T. Case 2.3. (IMPLIES (AND (EQUAL J 0) (NUMBERP K)) (EQUAL (EXP I K) (TIMES 1 (EXP I K)))), which again simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP K))) (EQUAL (EXP I 0) (TIMES 1 (EXP I K)))), which again simplifies, opening up the definitions of EQUAL, EXP, and TIMES, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP J)) (NUMBERP K)) (EQUAL (EXP I K) (TIMES 1 (EXP I K)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (EQUAL (EXP I (PLUS (SUB1 J) K)) (TIMES (EXP I (SUB1 J)) (EXP I K)))) (EQUAL (EXP I (PLUS J K)) (TIMES (EXP I J) (EXP I K)))), which simplifies, rewriting with COMMUTATIVITY-OF-TIMES, SUB1-ADD1, and ASSOCIATIVITY-OF-TIMES, and opening up the functions ZEROP, PLUS, and EXP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EXP-PLUS (PROVE-LEMMA EQUAL-LESSP (REWRITE) (EQUAL (EQUAL (LESSP X Y) Z) (IF (LESSP X Y) (EQUAL T Z) (EQUAL F Z)))) This simplifies, clearly, to the following four new formulas: Case 4. (IMPLIES (AND (EQUAL (LESSP X Y) Z) (NOT (LESSP X Y))) (NOT Z)). This again simplifies, trivially, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (LESSP X Y) Z)) (NOT (LESSP X Y))) Z). This again simplifies, clearly, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL (LESSP X Y) Z)) (LESSP X Y)) (NOT (EQUAL T Z))). This again simplifies, obviously, to: T. Case 1. (IMPLIES (AND (EQUAL (LESSP X Y) Z) (LESSP X Y)) (EQUAL (EQUAL T Z) T)). This again simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-LESSP (PROVE-LEMMA DIFFERENCE-ELIM (ELIM) (IMPLIES (AND (NUMBERP Y) (NOT (LESSP Y X))) (EQUAL (PLUS X (DIFFERENCE Y X)) Y))) This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ELIM (PROVE-LEMMA REMAINDER-QUOTIENT (REWRITE) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) (FIX X))) WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the newly proposed REMAINDER-QUOTIENT could! This formula simplifies, opening up the function FIX, to the following two new goals: Case 2. (IMPLIES (NOT (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) 0)). However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and opening up LESSP, REMAINDER, QUOTIENT, EQUAL, TIMES, and PLUS, to: T. Case 1. (IMPLIES (NUMBERP X) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)). Call the above conjecture *1. 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 (ZEROP Y) (p X Y)) (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y)) (p X Y)) (IMPLIES (AND (NOT (ZEROP Y)) (NOT (LESSP X Y)) (p (DIFFERENCE X Y) Y)) (p X Y))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP can be used to show that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces three new goals: Case 3. (IMPLIES (AND (ZEROP Y) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)), which simplifies, applying COMMUTATIVITY-OF-PLUS, TIMES-ZERO2, and COMMUTATIVITY-OF-TIMES, and unfolding the functions ZEROP, EQUAL, REMAINDER, QUOTIENT, TIMES, and PLUS, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)). This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and opening up the functions ZEROP, REMAINDER, QUOTIENT, EQUAL, TIMES, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (NOT (LESSP X Y)) (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y) (TIMES Y (QUOTIENT (DIFFERENCE X Y) Y))) (DIFFERENCE X Y)) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)). This simplifies, rewriting with TIMES-ADD1 and COMMUTATIVITY2-OF-PLUS, and opening up the functions ZEROP, REMAINDER, and QUOTIENT, to the goal: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (LESSP X Y)) (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y) (TIMES Y (QUOTIENT (DIFFERENCE X Y) Y))) (DIFFERENCE X Y)) (NUMBERP X)) (EQUAL (PLUS Y (DIFFERENCE X Y)) X)). But this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-QUOTIENT (PROVE-LEMMA REMAINDER-WRT-1 (REWRITE) (EQUAL (REMAINDER Y 1) 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 1) (p Y)) (IMPLIES (AND (NOT (ZEROP 1)) (LESSP Y 1)) (p Y)) (IMPLIES (AND (NOT (ZEROP 1)) (NOT (LESSP Y 1)) (p (DIFFERENCE Y 1))) (p Y))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP can be used to establish that the measure (COUNT Y) 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 1) (EQUAL (REMAINDER Y 1) 0)). This simplifies, expanding the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP 1)) (LESSP Y 1)) (EQUAL (REMAINDER Y 1) 0)). This simplifies, opening up the functions ZEROP, REMAINDER, EQUAL, and NUMBERP, to the new goal: (IMPLIES (AND (LESSP Y 1) (NUMBERP Y)) (EQUAL Y 0)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP 1)) (NOT (LESSP Y 1)) (EQUAL (REMAINDER (DIFFERENCE Y 1) 1) 0)) (EQUAL (REMAINDER Y 1) 0)), which simplifies, expanding ZEROP, REMAINDER, EQUAL, and NUMBERP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-WRT-1 (PROVE-LEMMA REMAINDER-WRT-12 (REWRITE) (IMPLIES (NOT (NUMBERP X)) (EQUAL (REMAINDER Y X) (FIX Y)))) This simplifies, unfolding the definitions of REMAINDER and FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-WRT-12 (PROVE-LEMMA LESSP-REMAINDER2 (REWRITE GENERALIZE) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y)))) This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions ZEROP and NOT, to three new goals: Case 3. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which we will name *1. Case 2. (IMPLIES (LESSP (REMAINDER X Y) Y) (NUMBERP Y)). This again simplifies, applying REMAINDER-WRT-12, and unfolding the definition of LESSP, to: T. Case 1. (IMPLIES (LESSP (REMAINDER X Y) Y) (NOT (EQUAL Y 0))). This again simplifies, using linear arithmetic, to: T. So next consider: (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), named *1 above. Let us appeal to the induction principle. The recursive terms in the conjecture suggest two inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Y) (p Y X)) (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y)) (p Y X)) (IMPLIES (AND (NOT (ZEROP Y)) (NOT (LESSP X Y)) (p Y (DIFFERENCE X Y))) (p Y 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 produces three new conjectures: Case 3. (IMPLIES (AND (ZEROP Y) (NOT (LESSP (REMAINDER X Y) Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, unfolding the function ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y) (NOT (LESSP (REMAINDER X Y) Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, unfolding ZEROP and REMAINDER, to: (IMPLIES (AND (LESSP X Y) (NOT (NUMBERP X)) (NOT (LESSP 0 Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))). This again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (NOT (LESSP X Y)) (LESSP (REMAINDER (DIFFERENCE X Y) Y) Y) (NOT (LESSP (REMAINDER X Y) Y)) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which simplifies, expanding the functions ZEROP and REMAINDER, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-REMAINDER2 (PROVE-LEMMA REMAINDER-X-X (REWRITE) (EQUAL (REMAINDER X X) 0)) This conjecture simplifies, rewriting with DIFFERENCE-0, and expanding the functions NUMBERP, REMAINDER, LESSP, and EQUAL, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP X X))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-X-X (PROVE-LEMMA REMAINDER-QUOTIENT-ELIM (ELIM) (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)), which simplifies, rewriting with REMAINDER-QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-QUOTIENT-ELIM (PROVE-LEMMA LESSP-TIMES-1 (REWRITE) (IMPLIES (NOT (ZEROP I)) (NOT (LESSP (TIMES I J) J)))) WARNING: Note that the proposed lemma LESSP-TIMES-1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES I J) J))), which we will name *1. We will appeal to induction. There are two plausible inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP I) (p I J)) (IMPLIES (AND (NOT (ZEROP I)) (p (SUB1 I) J)) (p I J))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces three new conjectures: Case 3. (IMPLIES (AND (ZEROP I) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES I J) J))), which simplifies, opening up the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP I)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES I J) J))), which simplifies, unfolding the functions ZEROP and TIMES, to the goal: (IMPLIES (AND (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (PLUS J (TIMES (SUB1 I) J)) J))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (NOT (LESSP (TIMES (SUB1 I) J) J)) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES I J) J))), which simplifies, opening up ZEROP and TIMES, to: (IMPLIES (AND (NOT (LESSP (TIMES (SUB1 I) J) J)) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (PLUS J (TIMES (SUB1 I) J)) J))). But this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-TIMES-1 (PROVE-LEMMA LESSP-TIMES-2 (REWRITE) (IMPLIES (NOT (ZEROP I)) (NOT (LESSP (TIMES J I) J)))) WARNING: Note that the proposed lemma LESSP-TIMES-2 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES J I) J))), which simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (TIMES I J) J))). But this again simplifies, using linear arithmetic and applying the lemma LESSP-TIMES-1, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-TIMES-2 (PROVE-LEMMA LESSP-QUOTIENT1 (REWRITE) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1)))))) This formula simplifies, rewriting with EQUAL-LESSP, and opening up the definitions of ZEROP, NOT, OR, and AND, to the following six new formulas: Case 6. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I)) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL J 0))). But this again simplifies, opening up EQUAL, QUOTIENT, and LESSP, to: T. Case 5. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I)) (NOT (EQUAL I 0)) (NUMBERP I)) (NUMBERP J)), which again simplifies, unfolding the definitions of QUOTIENT, EQUAL, and LESSP, to: T. Case 4. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I)) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL J 1)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by (PLUS Z (TIMES J X)) to eliminate (QUOTIENT I J) and (REMAINDER I J). We employ LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to restrict the new variables. We thus obtain the following three new formulas: Case 4.3. (IMPLIES (AND (EQUAL J 0) (NOT (LESSP (QUOTIENT I J) I)) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL J 1)). However this further simplifies, opening up the definitions of EQUAL, QUOTIENT, and LESSP, to: T. Case 4.2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (LESSP (QUOTIENT I J) I)) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL J 1)), which further simplifies, opening up QUOTIENT, EQUAL, and LESSP, to: T. Case 4.1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z J) (NOT (ZEROP J))) (NUMBERP J) (NOT (EQUAL J 0)) (NOT (LESSP X (PLUS Z (TIMES J X)))) (NOT (EQUAL (PLUS Z (TIMES J X)) 0))) (EQUAL J 1)), which further simplifies, rewriting with the lemmas EQUAL-TIMES-0 and PLUS-EQUAL-0, and expanding the functions ZEROP and NOT, to two new goals: Case 4.1.2. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (LESSP Z J) (NUMBERP J) (NOT (EQUAL J 0)) (NOT (LESSP X (PLUS Z (TIMES J X)))) (NOT (EQUAL Z 0))) (EQUAL J 1)), which again simplifies, using linear arithmetic and applying LESSP-TIMES-1, to: T. Case 4.1.1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (LESSP Z J) (NUMBERP J) (NOT (EQUAL J 0)) (NOT (LESSP X (PLUS Z (TIMES J X)))) (NOT (EQUAL X 0))) (EQUAL J 1)), 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: (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1))))). We gave this the name *1 above. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture, both of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p I J)) (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J)) (p I J)) (IMPLIES (AND (NOT (ZEROP J)) (NOT (LESSP I J)) (p (DIFFERENCE I J) J)) (p I J))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP inform us that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following three new formulas: Case 3. (IMPLIES (ZEROP J) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1)))))). This simplifies, expanding the definitions of ZEROP, EQUAL, QUOTIENT, LESSP, NOT, OR, and AND, to the following four new goals: Case 3.4. (IMPLIES (AND (EQUAL J 0) (NOT (EQUAL I 0)) (NOT (NUMBERP I))) (EQUAL (NUMBERP I) F)). This again simplifies, clearly, to: T. Case 3.3. (IMPLIES (AND (EQUAL J 0) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (NUMBERP I) T)). This again simplifies, clearly, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NOT (NUMBERP I))) (EQUAL (NUMBERP I) F)). This again simplifies, clearly, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (NUMBERP I) T)). This again simplifies, trivially, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J)) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1)))))). This simplifies, expanding the definitions of ZEROP, QUOTIENT, EQUAL, LESSP, NOT, OR, and AND, to the following three new goals: Case 2.3. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP I J) (NOT (EQUAL I 0)) (EQUAL J 1)) (EQUAL (NUMBERP I) F)). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (NUMBERP I)) (NOT (EQUAL 1 0)) (NUMBERP 1) (LESSP I 1) (NOT (EQUAL I 0))) (EQUAL (NUMBERP I) F)). This again simplifies, clearly, to: T. Case 2.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP I J) (NOT (EQUAL I 0)) (NOT (NUMBERP I))) (EQUAL (NUMBERP I) F)). This again simplifies, obviously, to: T. Case 2.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP I J) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 1))) (EQUAL (NUMBERP I) T)). This again simplifies, obviously, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (NOT (LESSP I J)) (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J)) (AND (NOT (ZEROP (DIFFERENCE I J))) (OR (ZEROP J) (NOT (EQUAL J 1)))))) (EQUAL (LESSP (QUOTIENT I J) I) (AND (NOT (ZEROP I)) (OR (ZEROP J) (NOT (EQUAL J 1)))))). This simplifies, applying EQUAL-DIFFERENCE-0, EQUAL-LESSP, and SUB1-ADD1, and unfolding the functions ZEROP, NOT, OR, AND, EQUAL, QUOTIENT, and LESSP, to four new goals: Case 1.4. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I J)) (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J))) (EQUAL J 1)) (NOT (LESSP (QUOTIENT I 1) I))), which again simplifies, unfolding EQUAL and NUMBERP, to the goal: (IMPLIES (AND (NOT (LESSP I 1)) (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1) (DIFFERENCE I 1)))) (NOT (LESSP (QUOTIENT I 1) I))). However this again simplifies, applying SUB1-ADD1, and opening up the functions NUMBERP, EQUAL, QUOTIENT, and LESSP, to the new formula: (IMPLIES (AND (NOT (LESSP I 1)) (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1) (DIFFERENCE I 1))) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1) (SUB1 I)))), which again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I J)) (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J))) (NOT (LESSP J I)) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL J 1)) (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J) (SUB1 I)) F)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (EQUAL 1 0)) (NUMBERP 1) (NOT (LESSP 1 1)) (NOT (LESSP (QUOTIENT (DIFFERENCE 1 1) 1) (DIFFERENCE 1 1))) (NOT (LESSP 1 1)) (NOT (EQUAL 1 0)) (NUMBERP 1)) (EQUAL (LESSP (QUOTIENT (DIFFERENCE 1 1) 1) (SUB1 1)) F)). However this again simplifies, unfolding EQUAL, NUMBERP, LESSP, DIFFERENCE, QUOTIENT, and SUB1, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I J)) (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J))) (NOT (LESSP J I)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 1))) (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J) (SUB1 I)) T)), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (NOT (LESSP I I)) (NOT (LESSP (QUOTIENT (DIFFERENCE I I) I) (DIFFERENCE I I))) (NOT (LESSP I I)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL I 1))) (EQUAL (LESSP (QUOTIENT (DIFFERENCE I I) I) (SUB1 I)) T)). This again simplifies, applying DIFFERENCE-0, and expanding the definitions of LESSP, EQUAL, and QUOTIENT, to the new formula: (IMPLIES (AND (NOT (LESSP I I)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL I 1))) (NOT (EQUAL (SUB1 I) 0))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I J)) (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J)) (LESSP J I) (NOT (EQUAL J 1)) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J) (SUB1 I)) T)), which again simplifies, obviously, to: (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I J)) (LESSP (QUOTIENT (DIFFERENCE I J) J) (DIFFERENCE I J)) (LESSP J I) (NOT (EQUAL J 1)) (NOT (EQUAL I 0)) (NUMBERP I)) (LESSP (QUOTIENT (DIFFERENCE I J) J) (SUB1 I))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] LESSP-QUOTIENT1 (PROVE-LEMMA LESSP-REMAINDER1 (REWRITE) (EQUAL (LESSP (REMAINDER X Y) X) (AND (NOT (ZEROP Y)) (NOT (ZEROP X)) (NOT (LESSP X Y))))) This formula simplifies, rewriting with EQUAL-LESSP, and opening up the definitions of ZEROP, NOT, and AND, to the following six new formulas: Case 6. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) X)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL X 0)) (NUMBERP X)) (LESSP X Y)). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by (PLUS Z (TIMES Y V)) to eliminate (REMAINDER X Y) and (QUOTIENT X Y). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove: (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z Y) (NOT (ZEROP Y))) (NUMBERP V) (NOT (LESSP Z (PLUS Z (TIMES Y V)))) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (PLUS Z (TIMES Y V)) 0))) (LESSP (PLUS Z (TIMES Y V)) Y)). However this further simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES, EQUAL-TIMES-0, and PLUS-EQUAL-0, and unfolding the definitions of ZEROP and NOT, to two new conjectures: Case 6.2. (IMPLIES (AND (NUMBERP Z) (LESSP Z Y) (NUMBERP V) (NOT (LESSP Z (PLUS Z (TIMES V Y)))) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Z 0))) (LESSP (PLUS Z (TIMES V Y)) Y)), which again simplifies, using linear arithmetic, to: T. Case 6.1. (IMPLIES (AND (NUMBERP Z) (LESSP Z Y) (NUMBERP V) (NOT (LESSP Z (PLUS Z (TIMES V Y)))) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL V 0))) (LESSP (PLUS Z (TIMES V Y)) Y)), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (LESSP (REMAINDER X Y) X) (NOT (LESSP X Y))), which again simplifies, unfolding the functions REMAINDER and LESSP, to two new formulas: Case 5.2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP 0 X) (NOT (EQUAL Y 0))) (NOT (NUMBERP Y))), which again simplifies, opening up LESSP, to: T. Case 5.1. (IMPLIES (AND (NUMBERP X) (LESSP X X)) (NOT (LESSP X Y))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (LESSP (REMAINDER X Y) X) (NUMBERP X)), which again simplifies, expanding the functions LESSP and REMAINDER, to: T. Case 3. (IMPLIES (LESSP (REMAINDER X Y) X) (NOT (EQUAL X 0))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (LESSP (REMAINDER X Y) X) (NUMBERP Y)), which again simplifies, rewriting with REMAINDER-WRT-12, to the following two new conjectures: Case 2.2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP 0 X)) (NUMBERP Y)). However this again simplifies, unfolding the function LESSP, to: T. Case 2.1. (IMPLIES (AND (NUMBERP X) (LESSP X X)) (NUMBERP Y)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (LESSP (REMAINDER X Y) X) (NOT (EQUAL Y 0))), which again simplifies, opening up the definitions of EQUAL and REMAINDER, to two new formulas: Case 1.2. (IMPLIES (NOT (NUMBERP X)) (NOT (LESSP 0 X))), which again simplifies, unfolding the function LESSP, to: T. Case 1.1. (IMPLIES (NUMBERP X) (NOT (LESSP X X))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-REMAINDER1 (PROVE-LEMMA DIFFERENCE-PLUS1 (REWRITE) (EQUAL (DIFFERENCE (PLUS X Y) X) (FIX Y))) WARNING: the previously added lemma, DIFFERENCE-PLUS, could be applied whenever the newly proposed DIFFERENCE-PLUS1 could! This conjecture simplifies, appealing to the lemma DIFFERENCE-PLUS, and expanding the function FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS1 (PROVE-LEMMA DIFFERENCE-PLUS2 (REWRITE) (EQUAL (DIFFERENCE (PLUS Y X) X) (FIX Y))) WARNING: the previously added lemma, DIFFERENCE-PLUS, could be applied whenever the newly proposed DIFFERENCE-PLUS2 could! This conjecture simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and DIFFERENCE-PLUS1, and expanding the function FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS2 (PROVE-LEMMA DIFFERENCE-PLUS-CANCELATION (REWRITE) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z))) This simplifies, using linear arithmetic, to the following two new conjectures: Case 2. (IMPLIES (LESSP (PLUS X Y) (PLUS X Z)) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z))). But this again simplifies, using linear arithmetic, applying DIFFERENCE-0, and opening up the function EQUAL, to: T. Case 1. (IMPLIES (LESSP Y Z) (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z)) (DIFFERENCE Y Z))). But this again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-0, and expanding EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELATION (PROVE-LEMMA TIMES-DIFFERENCE (REWRITE) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X)))) WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed TIMES-DIFFERENCE could! . Appealing to the lemma DIFFERENCE-ELIM, we now replace C by (PLUS W Z) to eliminate (DIFFERENCE C W). We use the type restriction lemma noted when DIFFERENCE was introduced to constrain the new variable. The result is three new goals: Case 3. (IMPLIES (LESSP C W) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X)))), which simplifies, using linear arithmetic, appealing to the lemmas DIFFERENCE-0, COMMUTATIVITY-OF-TIMES, and EQUAL-DIFFERENCE-0, and unfolding EQUAL and TIMES, to: (IMPLIES (LESSP C W) (NOT (LESSP (TIMES W X) (TIMES C X)))), 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: (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X))), which we named *1 above. We will appeal to induction. There are five plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP C) (p X C W)) (IMPLIES (AND (NOT (ZEROP C)) (ZEROP W)) (p X C W)) (IMPLIES (AND (NOT (ZEROP C)) (NOT (ZEROP W)) (p X (SUB1 C) (SUB1 W))) (p X C W))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT C) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for W. The above induction scheme produces the following three new goals: Case 3. (IMPLIES (ZEROP C) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X)))). This simplifies, using linear arithmetic, rewriting with DIFFERENCE-0 and COMMUTATIVITY-OF-TIMES, and unfolding the functions ZEROP, EQUAL, and TIMES, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP C)) (ZEROP W)) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X)))), which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES, PLUS-EQUAL-0, and EQUAL-TIMES-0, and unfolding the functions ZEROP, EQUAL, DIFFERENCE, and TIMES, to four new conjectures: Case 2.4. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL W 0) (NOT (NUMBERP X))) (EQUAL (PLUS X (TIMES (SUB1 C) X)) 0)), which again simplifies, applying EQUAL-TIMES-0, and opening up the function PLUS, to: T. Case 2.3. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (EQUAL W 0) (EQUAL X 0)) (EQUAL (PLUS X (TIMES (SUB1 C) X)) 0)). But this again simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding the functions EQUAL, TIMES, and PLUS, to: T. Case 2.2. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (NOT (NUMBERP W)) (NOT (NUMBERP X))) (EQUAL (PLUS X (TIMES (SUB1 C) X)) 0)). This again simplifies, applying EQUAL-TIMES-0, and unfolding the definition of PLUS, to: T. Case 2.1. (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (NOT (NUMBERP W)) (EQUAL X 0)) (EQUAL (PLUS X (TIMES (SUB1 C) X)) 0)). However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding the definitions of EQUAL, TIMES, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP C)) (NOT (ZEROP W)) (EQUAL (TIMES X (DIFFERENCE (SUB1 C) (SUB1 W))) (DIFFERENCE (TIMES (SUB1 C) X) (TIMES (SUB1 W) X)))) (EQUAL (TIMES X (DIFFERENCE C W)) (DIFFERENCE (TIMES C X) (TIMES W X)))). This simplifies, rewriting with DIFFERENCE-PLUS-CANCELATION, and unfolding the definitions of ZEROP, DIFFERENCE, and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-DIFFERENCE (DEFN DIVIDES (X Y) (ZEROP (REMAINDER Y X))) Note that (OR (FALSEP (DIVIDES X Y)) (TRUEP (DIVIDES X Y))) is a theorem. [ 0.0 0.0 0.0 ] DIVIDES (PROVE-LEMMA DIVIDES-TIMES (REWRITE) (EQUAL (REMAINDER (TIMES X Z) Z) 0)) Name the conjecture *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Z)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z)) (p X Z))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new goals: Case 2. (IMPLIES (ZEROP X) (EQUAL (REMAINDER (TIMES X Z) Z) 0)). This simplifies, expanding ZEROP, EQUAL, TIMES, LESSP, NUMBERP, and REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z) 0)) (EQUAL (REMAINDER (TIMES X Z) Z) 0)). This simplifies, rewriting with DIFFERENCE-PLUS1, and unfolding the definitions of ZEROP, TIMES, and REMAINDER, to three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z) 0) (NOT (NUMBERP Z))) (EQUAL (PLUS Z (TIMES (SUB1 X) Z)) 0)), which again simplifies, applying REMAINDER-WRT-12 and EQUAL-TIMES-0, and unfolding the function PLUS, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z) 0) (EQUAL Z 0)) (EQUAL (PLUS Z (TIMES (SUB1 X) Z)) 0)). However this again simplifies, applying COMMUTATIVITY-OF-TIMES, and unfolding the functions EQUAL, TIMES, REMAINDER, and PLUS, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z) 0) (LESSP (PLUS Z (TIMES (SUB1 X) Z)) Z)) (EQUAL (PLUS Z (TIMES (SUB1 X) Z)) 0)). However this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] DIVIDES-TIMES (PROVE-LEMMA DIFFERENCE-PLUS3 (REWRITE) (EQUAL (DIFFERENCE (PLUS B A C) A) (PLUS B C))) This simplifies, using linear arithmetic, to: (IMPLIES (LESSP (PLUS B A C) A) (EQUAL (DIFFERENCE (PLUS B A C) A) (PLUS B C))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS3 (PROVE-LEMMA DIFFERENCE-ADD1-CANCELLATION (REWRITE) (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z) (ADD1 Y))) This conjecture simplifies, using linear arithmetic, to: (IMPLIES (LESSP (ADD1 (PLUS Y Z)) Z) (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z) (ADD1 Y))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ADD1-CANCELLATION (PROVE-LEMMA REMAINDER-ADD1 (REWRITE) (IMPLIES (AND (NOT (ZEROP Y)) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y) 0)))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y) 0))). Name the above subgoal *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 the following two new formulas: Case 2. (IMPLIES (AND (ZEROP X) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y) 0))). This simplifies, using linear arithmetic, applying the lemma DIFFERENCE-0, and opening up the definitions of ZEROP, EQUAL, TIMES, ADD1, NUMBERP, REMAINDER, and LESSP, to the following two new goals: Case 2.2. (IMPLIES (AND (EQUAL X 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (LESSP 1 Y)). This again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (LESSP 1 Y)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (REMAINDER (ADD1 (TIMES (SUB1 X) Y)) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y) 0))), which simplifies, expanding the functions ZEROP and TIMES, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL (REMAINDER (ADD1 (TIMES (SUB1 X) Y)) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES (SUB1 X) Y))) Y) 0))). But this further simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y (SUB1 X))) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y (SUB1 X)))) Y) 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. We must thus prove the conjecture: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y Z)) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y Z))) Y) 0))). This further simplifies, trivially, to the new goal: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y Z)) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y Z))) Y) 0))), which we generalize by replacing (TIMES Y Z) by A. We restrict the new variable by recalling the type restriction lemma noted when TIMES was introduced. We would thus like to prove: (IMPLIES (AND (NUMBERP A) (NUMBERP Z) (NOT (EQUAL (REMAINDER (ADD1 A) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1))) (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y A)) Y) 0))), which further simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS, DIFFERENCE-ADD1-CANCELLATION, and SUB1-ADD1, and unfolding LESSP and REMAINDER, to: (IMPLIES (AND (NUMBERP A) (NUMBERP Z) (NOT (EQUAL (REMAINDER (ADD1 A) Y) 0)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL Y 1)) (LESSP (PLUS A Y) (SUB1 Y))) (NOT (EQUAL (ADD1 (PLUS A Y)) 0))). This finally simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.2 0.0 ] REMAINDER-ADD1 (PROVE-LEMMA DIVIDES-PLUS-REWRITE1 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES Z W)) to eliminate (REMAINDER X Z) and (QUOTIENT X Z). We employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We would thus like to prove the following four new conjectures: Case 4. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)). However this simplifies, expanding LESSP, REMAINDER, EQUAL, and PLUS, to the conjecture: (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (REMAINDER Y Z) 0) (NOT (NUMBERP Y))) (EQUAL (REMAINDER 0 Z) 0)). But this again simplifies, expanding the definitions of LESSP, REMAINDER, EQUAL, and NUMBERP, to: T. Case 3. (IMPLIES (AND (EQUAL Z 0) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)), which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and expanding the definitions of EQUAL, REMAINDER, PLUS, and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP Z)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)). But this simplifies, applying REMAINDER-WRT-12, PLUS-RIGHT-ID2, and COMMUTATIVITY-OF-PLUS, and opening up the definitions of PLUS, NUMBERP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NUMBERP V) (EQUAL (LESSP V Z) (NOT (ZEROP Z))) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (EQUAL V 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z W)) Y) Z) 0)). However this simplifies, applying COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and unfolding the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to the new formula: (IMPLIES (AND (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z) 0)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES Z D)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following two new formulas: Case 1.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z) 0)). However this further simplifies, rewriting with DIVIDES-TIMES, and opening up LESSP, REMAINDER, EQUAL, and PLUS, to: T. Case 1.1. (IMPLIES (AND (NUMBERP V) (EQUAL (LESSP V Z) (NOT (ZEROP Z))) (NUMBERP D) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (EQUAL V 0)) (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z D)) (TIMES W Z)) Z) 0)). However this further simplifies, applying COMMUTATIVITY-OF-TIMES, and opening up NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: (IMPLIES (AND (NUMBERP D) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0))) (EQUAL (REMAINDER (PLUS (TIMES D Z) (TIMES W Z)) Z) 0)), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)). We named this *1. We will try to prove it by induction. There are three plausible inductions, two of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Z) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z)) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (p (DIFFERENCE X Z) Y Z)) (p X Y Z))). 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 produces four new goals: Case 4. (IMPLIES (AND (ZEROP Z) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)), which simplifies, rewriting with the lemmas PLUS-RIGHT-ID2, COMMUTATIVITY-OF-PLUS, and REMAINDER-WRT-12, and expanding ZEROP, EQUAL, REMAINDER, PLUS, and NUMBERP, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)), which simplifies, unfolding ZEROP, REMAINDER, EQUAL, and PLUS, to two new conjectures: Case 3.2. (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP X Z) (EQUAL X 0) (EQUAL (REMAINDER Y Z) 0) (NOT (NUMBERP Y))) (EQUAL (REMAINDER 0 Z) 0)), which again simplifies, unfolding EQUAL, LESSP, REMAINDER, and NUMBERP, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP X Z) (NOT (NUMBERP X)) (EQUAL (REMAINDER Y Z) 0) (NOT (NUMBERP Y))) (EQUAL (REMAINDER 0 Z) 0)), which again simplifies, unfolding the functions LESSP, REMAINDER, EQUAL, and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (NOT (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)), which simplifies, unfolding the definitions of ZEROP and REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (EQUAL (REMAINDER (PLUS (DIFFERENCE X Z) Y) Z) 0) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)), which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and opening up ZEROP and REMAINDER, to: (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP X Z)) (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z)) Z) 0) (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)). Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace X by (PLUS Z V) to eliminate (DIFFERENCE X Z) and V by (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z). We use the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following two new conjectures: Case 1.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP X Z)) (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z)) Z) 0) (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS X Y) Z) 0)). This further simplifies, unfolding the function LESSP, to: T. Case 1.1. (IMPLIES (AND (NUMBERP W) (EQUAL (LESSP W Z) (NOT (ZEROP Z))) (NUMBERP D) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP (PLUS Z W (TIMES Z D)) Z)) (EQUAL (REMAINDER (PLUS Y W (TIMES Z D)) Z) 0) (EQUAL W 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (REMAINDER (PLUS (PLUS Z W (TIMES Z D)) Y) Z) 0)), which further simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and DIFFERENCE-PLUS3, and unfolding the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, PLUS, and REMAINDER, to: (IMPLIES (AND (NUMBERP D) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP (PLUS Z (TIMES D Z)) Z)) (EQUAL (REMAINDER (PLUS Y (TIMES D Z)) Z) 0) (EQUAL (REMAINDER Y Z) 0) (LESSP (PLUS Y Z (TIMES D Z)) Z)) (EQUAL (PLUS Y Z (TIMES D Z)) 0)). However this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.1 ] DIVIDES-PLUS-REWRITE1 (PROVE-LEMMA DIVIDES-PLUS-REWRITE2 (REWRITE) (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0)))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES Z W)) to eliminate (REMAINDER X Z) and (QUOTIENT X Z). We use LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We would thus like to prove the following four new formulas: Case 4. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))). But this simplifies, unfolding the definitions of LESSP, REMAINDER, EQUAL, and PLUS, to: (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL (REMAINDER Y Z) 0)) (NOT (NUMBERP Y))) (NOT (EQUAL (REMAINDER 0 Z) 0))). This again simplifies, expanding the functions LESSP, REMAINDER, and EQUAL, to: T. Case 3. (IMPLIES (AND (EQUAL Z 0) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, expanding the functions EQUAL, REMAINDER, and PLUS, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP Z)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, rewriting with REMAINDER-WRT-12, and expanding EQUAL and PLUS, to: T. Case 1. (IMPLIES (AND (NUMBERP V) (EQUAL (LESSP V Z) (NOT (ZEROP Z))) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (EQUAL V 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z W)) Y) Z) 0))). This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and expanding the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: (IMPLIES (AND (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z) 0))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES Z D)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following two new conjectures: Case 1.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z) 0))). This further simplifies, unfolding the definitions of LESSP, REMAINDER, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NUMBERP V) (EQUAL (LESSP V Z) (NOT (ZEROP Z))) (NUMBERP D) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL V 0))) (NOT (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z D)) (TIMES W Z)) Z) 0))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and ASSOCIATIVITY-OF-PLUS, and opening up ZEROP and NOT, to: (IMPLIES (AND (NUMBERP V) (LESSP V Z) (NUMBERP D) (NUMBERP W) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL V 0))) (NOT (EQUAL (REMAINDER (PLUS V (TIMES D Z) (TIMES W Z)) Z) 0))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))). We named this *1. We will try to prove it by induction. Three inductions are suggested by terms in the conjecture, two of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Z) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z)) (p X Y Z)) (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (p (DIFFERENCE X Z) Y Z)) (p X Y Z))). 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 generates four new formulas: Case 4. (IMPLIES (AND (ZEROP Z) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, rewriting with the lemma REMAINDER-WRT-12, and unfolding the definitions of ZEROP, EQUAL, REMAINDER, and PLUS, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, expanding the functions ZEROP, REMAINDER, EQUAL, and PLUS, to two new goals: Case 3.2. (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP X Z) (EQUAL X 0) (NOT (EQUAL (REMAINDER Y Z) 0)) (NOT (NUMBERP Y))) (NOT (EQUAL (REMAINDER 0 Z) 0))), which again simplifies, opening up EQUAL, LESSP, and REMAINDER, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP X Z) (NOT (NUMBERP X)) (NOT (EQUAL (REMAINDER Y Z) 0)) (NOT (NUMBERP Y))) (NOT (EQUAL (REMAINDER 0 Z) 0))), which again simplifies, expanding the functions LESSP, REMAINDER, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (NOT (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, unfolding the functions ZEROP and REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Z)) (NOT (LESSP X Z)) (NOT (EQUAL (REMAINDER (PLUS (DIFFERENCE X Z) Y) Z) 0)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and opening up the definitions of ZEROP and REMAINDER, to the goal: (IMPLIES (AND (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP X Z)) (NOT (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z)) Z) 0)) (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))). Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we now replace X by (PLUS Z V) to eliminate (DIFFERENCE X Z) and V by (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z). We use the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove two new formulas: Case 1.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP X Z)) (NOT (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z)) Z) 0)) (EQUAL (REMAINDER (DIFFERENCE X Z) Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which further simplifies, opening up LESSP, to: T. Case 1.1. (IMPLIES (AND (NUMBERP W) (EQUAL (LESSP W Z) (NOT (ZEROP Z))) (NUMBERP D) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP (PLUS Z W (TIMES Z D)) Z)) (NOT (EQUAL (REMAINDER (PLUS Y W (TIMES Z D)) Z) 0)) (EQUAL W 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS (PLUS Z W (TIMES Z D)) Y) Z) 0))), which further simplifies, applying COMMUTATIVITY-OF-TIMES, COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and DIFFERENCE-PLUS3, and unfolding the definitions of NUMBERP, EQUAL, LESSP, ZEROP, NOT, PLUS, and REMAINDER, to: (IMPLIES (AND (NUMBERP D) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (LESSP (PLUS Z (TIMES D Z)) Z)) (NOT (EQUAL (REMAINDER (PLUS Y (TIMES D Z)) Z) 0)) (NOT (EQUAL (REMAINDER Y Z) 0)) (LESSP (PLUS Y Z (TIMES D Z)) Z)) (NOT (EQUAL (PLUS Y Z (TIMES D Z)) 0))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.2 0.0 ] DIVIDES-PLUS-REWRITE2 (PROVE-LEMMA DIVIDES-PLUS-REWRITE (REWRITE) (IMPLIES (EQUAL (REMAINDER X Z) 0) (EQUAL (EQUAL (REMAINDER (PLUS X Y) Z) 0) (EQUAL (REMAINDER Y Z) 0)))) This conjecture simplifies, clearly, to two new conjectures: Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER Y Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))), which again simplifies, applying DIVIDES-PLUS-REWRITE2, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER Y Z) 0)) (EQUAL (EQUAL (REMAINDER (PLUS X Y) Z) 0) T)). However this again simplifies, applying DIVIDES-PLUS-REWRITE1, and unfolding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIVIDES-PLUS-REWRITE (PROVE-LEMMA LESSP-PLUS-CANCELATION (REWRITE) (EQUAL (LESSP (PLUS X Y) (PLUS X Z)) (LESSP Y Z))) This simplifies, rewriting with EQUAL-LESSP, to two new formulas: Case 2. (IMPLIES (NOT (LESSP (PLUS X Y) (PLUS X Z))) (NOT (LESSP Y Z))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (LESSP (PLUS X Y) (PLUS X Z)) (LESSP Y Z)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-PLUS-CANCELATION (PROVE-LEMMA DIVIDES-PLUS-REWRITE-COMMUTED (REWRITE) (IMPLIES (EQUAL (REMAINDER X Z) 0) (EQUAL (EQUAL (REMAINDER (PLUS Y X) Z) 0) (EQUAL (REMAINDER Y Z) 0)))) This conjecture simplifies, applying COMMUTATIVITY-OF-PLUS and DIVIDES-PLUS-REWRITE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIVIDES-PLUS-REWRITE-COMMUTED (PROVE-LEMMA EUCLID (REWRITE) (IMPLIES (EQUAL (REMAINDER X Z) 0) (EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0) (IF (LESSP X Y) (EQUAL (REMAINDER Y Z) 0) T)))) This formula simplifies, obviously, to the following three new conjectures: Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0))) (LESSP X Y)). This again simplifies, applying DIFFERENCE-0, and expanding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0))) (NOT (EQUAL (REMAINDER Y Z) 0))). Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we now replace Y by (PLUS X V) to eliminate (DIFFERENCE Y X) and V by (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z). We rely upon the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove five new goals: Case 2.5. (IMPLIES (AND (LESSP Y X) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0))) (NOT (EQUAL (REMAINDER Y Z) 0))), which further simplifies, using linear arithmetic, rewriting with DIFFERENCE-0, and expanding the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2.4. (IMPLIES (AND (NOT (NUMBERP Y)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0))) (NOT (EQUAL (REMAINDER Y Z) 0))). However this further simplifies, using linear arithmetic, rewriting with the lemma DIFFERENCE-0, and unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2.3. (IMPLIES (AND (EQUAL Z 0) (NUMBERP V) (NOT (LESSP (PLUS X V) X)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER V Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X V) Z) 0))), which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS and PLUS-RIGHT-ID2, and opening up the functions EQUAL, REMAINDER, and PLUS, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP Z)) (NUMBERP V) (NOT (LESSP (PLUS X V) X)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL (REMAINDER V Z) 0))) (NOT (EQUAL (REMAINDER (PLUS X V) Z) 0))). But this further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, REMAINDER-WRT-12, and PLUS-RIGHT-ID2, and expanding the functions EQUAL and PLUS, to: T. Case 2.1. (IMPLIES (AND (NUMBERP W) (EQUAL (LESSP W Z) (NOT (ZEROP Z))) (NUMBERP D) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (LESSP (PLUS X W (TIMES Z D)) X)) (EQUAL (REMAINDER X Z) 0) (NOT (EQUAL W 0))) (NOT (EQUAL (REMAINDER (PLUS X W (TIMES Z D)) Z) 0))). But this further simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-PLUS, DIVIDES-PLUS-REWRITE1, DIVIDES-TIMES, and DIVIDES-PLUS-REWRITE-COMMUTED, and expanding the functions ZEROP, NOT, EQUAL, and REMAINDER, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0) (LESSP X Y)) (EQUAL (EQUAL (REMAINDER Y Z) 0) T)), which again simplifies, trivially, to the new formula: (IMPLIES (AND (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0) (LESSP X Y)) (EQUAL (REMAINDER Y Z) 0)). Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS X V) to eliminate (DIFFERENCE Y X) and V by (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z). We use the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We would thus like to prove the following five new goals: Case 1.5. (IMPLIES (AND (LESSP Y X) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0) (LESSP X Y)) (EQUAL (REMAINDER Y Z) 0)). But this further simplifies, using linear arithmetic, to: T. Case 1.4. (IMPLIES (AND (NOT (NUMBERP Y)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER (DIFFERENCE Y X) Z) 0) (LESSP X Y)) (EQUAL (REMAINDER Y Z) 0)), which further simplifies, expanding DIFFERENCE, LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 1.3. (IMPLIES (AND (EQUAL Z 0) (NUMBERP V) (NOT (LESSP (PLUS X V) X)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER V Z) 0) (LESSP X (PLUS X V))) (EQUAL (REMAINDER (PLUS X V) Z) 0)), which further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS and PLUS-RIGHT-ID2, and opening up the functions EQUAL, REMAINDER, PLUS, LESSP, and NUMBERP, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP Z)) (NUMBERP V) (NOT (LESSP (PLUS X V) X)) (EQUAL (REMAINDER X Z) 0) (EQUAL (REMAINDER V Z) 0) (LESSP X (PLUS X V))) (EQUAL (REMAINDER (PLUS X V) Z) 0)), which further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS, REMAINDER-WRT-12, and PLUS-RIGHT-ID2, and opening up PLUS, LESSP, NUMBERP, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NUMBERP W) (EQUAL (LESSP W Z) (NOT (ZEROP Z))) (NUMBERP D) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (LESSP (PLUS X W (TIMES Z D)) X)) (EQUAL (REMAINDER X Z) 0) (EQUAL W 0) (LESSP X (PLUS X W (TIMES Z D)))) (EQUAL (REMAINDER (PLUS X W (TIMES Z D)) Z) 0)), which further simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES, DIVIDES-TIMES, and DIVIDES-PLUS-REWRITE1, and opening up NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EUCLID (PROVE-LEMMA LESSP-TIMES-CANCELLATION (REWRITE) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y)))) This conjecture simplifies, rewriting with EQUAL-LESSP, and expanding the definitions of ZEROP, NOT, and AND, to the following four new goals: Case 4. (IMPLIES (AND (NOT (LESSP (TIMES X Z) (TIMES Y Z))) (NOT (EQUAL Z 0)) (NUMBERP Z)) (NOT (LESSP X Y))). Call the above conjecture *1. Case 3. (IMPLIES (LESSP (TIMES X Z) (TIMES Y Z)) (LESSP X Y)), 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: (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y))). We gave this the name *1 above. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Z Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z (SUB1 Y))) (p X Z Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for Y. The above induction scheme produces two new conjectures: Case 2. (IMPLIES (ZEROP X) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y)))), which simplifies, expanding ZEROP, EQUAL, TIMES, LESSP, NOT, and AND, to ten new conjectures: Case 2.10. (IMPLIES (AND (EQUAL X 0) (EQUAL Z 0) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)), which again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding the functions EQUAL, TIMES, and PLUS, to: T. Case 2.9. (IMPLIES (AND (EQUAL X 0) (NOT (NUMBERP Z)) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)). This again simplifies, applying EQUAL-TIMES-0, and opening up the definition of PLUS, to: T. Case 2.8. (IMPLIES (AND (EQUAL X 0) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (EQUAL Y 0)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)) (EQUAL F (NUMBERP Y))). But this again simplifies, using linear arithmetic, to: T. Case 2.7. (IMPLIES (AND (EQUAL X 0) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (EQUAL Y 0)) (NOT (NUMBERP Y))) (EQUAL F (NUMBERP Y))), which again simplifies, trivially, to: T. Case 2.6. (IMPLIES (AND (EQUAL X 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0))) (EQUAL T (NUMBERP Y))). This again simplifies, obviously, to: T. Case 2.5. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL Z 0) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)). However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding EQUAL, TIMES, and PLUS, to: T. Case 2.4. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (NUMBERP Z)) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)). However this again simplifies, applying the lemma EQUAL-TIMES-0, and expanding PLUS, to: T. Case 2.3. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (EQUAL Y 0)) (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0)) (EQUAL F (NUMBERP Y))), which again simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Z 0)) (NUMBERP Z) (NOT (EQUAL Y 0)) (NOT (NUMBERP Y))) (EQUAL F (NUMBERP Y))), which again simplifies, clearly, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0))) (EQUAL T (NUMBERP Y))). This again simplifies, clearly, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z)) (AND (NOT (ZEROP Z)) (LESSP (SUB1 X) (SUB1 Y))))) (EQUAL (LESSP (TIMES X Z) (TIMES Y Z)) (AND (NOT (ZEROP Z)) (LESSP X Y)))). This simplifies, applying EQUAL-LESSP, TIMES-ZERO2, and COMMUTATIVITY-OF-TIMES, and unfolding the definitions of ZEROP, NOT, AND, TIMES, LESSP, and EQUAL, to six new goals: Case 1.6. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z))) (NOT (LESSP (SUB1 X) (SUB1 Y))) (NOT (EQUAL Y 0)) (NUMBERP Y)) (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z)) (PLUS Z (TIMES (SUB1 Y) Z))))), which again simplifies, using linear arithmetic, to: T. Case 1.5. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z))) (NOT (LESSP (SUB1 X) (SUB1 Y))) (EQUAL Y 0)) (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z)) 0))), which again simplifies, using linear arithmetic, to: T. Case 1.4. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z))) (NOT (LESSP (SUB1 X) (SUB1 Y))) (NOT (NUMBERP Y))) (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z)) 0))), which again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z)) (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP (SUB1 X) (SUB1 Y)) (NOT (NUMBERP Y))) (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z)) 0))), which again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z)) (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP (SUB1 X) (SUB1 Y)) (EQUAL Y 0)) (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z)) 0))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (TIMES (SUB1 X) Z) (TIMES (SUB1 Y) Z)) (NOT (EQUAL Z 0)) (NUMBERP Z) (LESSP (SUB1 X) (SUB1 Y)) (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (PLUS Z (TIMES (SUB1 X) Z)) (PLUS Z (TIMES (SUB1 Y) Z)))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-TIMES-CANCELLATION (PROVE-LEMMA LESSP-PLUS-CANCELLATION3 (REWRITE) (EQUAL (LESSP Y (PLUS X Y)) (NOT (ZEROP X)))) This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions ZEROP and NOT, to three new goals: Case 3. (IMPLIES (AND (NOT (LESSP Y (PLUS X Y))) (NOT (EQUAL X 0))) (NOT (NUMBERP X))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (LESSP Y (PLUS X Y)) (NUMBERP X)), which again simplifies, expanding PLUS, to two new conjectures: Case 2.2. (IMPLIES (AND (NOT (NUMBERP Y)) (LESSP Y 0)) (NUMBERP X)), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (NUMBERP Y) (LESSP Y Y)) (NUMBERP X)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (LESSP Y (PLUS X Y)) (NOT (EQUAL X 0))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-PLUS-CANCELLATION3 (PROVE-LEMMA QUOTIENT-TIMES1 (REWRITE) (IMPLIES (AND (NUMBERP Y) (NUMBERP X) (NOT (EQUAL X 0)) (DIVIDES X Y)) (EQUAL (TIMES X (QUOTIENT Y X)) Y))) WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed QUOTIENT-TIMES1 could! This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (NUMBERP Y) (NUMBERP X) (NOT (EQUAL X 0)) (EQUAL (REMAINDER Y X) 0)) (EQUAL (TIMES X (QUOTIENT Y X)) Y)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS Z (TIMES X V)) to eliminate (REMAINDER Y X) and (QUOTIENT Y X). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain: (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z X) (NOT (ZEROP X))) (NUMBERP V) (NUMBERP X) (NOT (EQUAL X 0)) (EQUAL Z 0)) (EQUAL (TIMES X V) (PLUS Z (TIMES X V)))), which simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-TIMES1 (PROVE-LEMMA QUOTIENT-LESSP (REWRITE) (IMPLIES (AND (NOT (ZEROP X)) (LESSP X Y)) (NOT (EQUAL (QUOTIENT Y X) 0)))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X Y)) (NOT (EQUAL (QUOTIENT Y X) 0))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES X Z)) to eliminate (QUOTIENT Y X) and (REMAINDER Y X). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to restrict the new variables. We thus obtain the following two new goals: Case 2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X Y)) (NOT (EQUAL (QUOTIENT Y X) 0))). However this simplifies, opening up the definition of LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V X) (NOT (ZEROP X))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X (PLUS V (TIMES X Z)))) (NOT (EQUAL Z 0))), which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and expanding the definitions of NUMBERP, ZEROP, NOT, EQUAL, TIMES, and PLUS, to: (IMPLIES (AND (NUMBERP V) (LESSP V X) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP X V))). However this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-LESSP (DEFN GREATEREQPR (W Z) (IF (ZEROP W) (ZEROP Z) (IF (EQUAL W Z) T (GREATEREQPR (SUB1 W) Z)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to establish that the measure (COUNT W) decreases according to the well-founded relation LESSP in each recursive call. Hence, GREATEREQPR is accepted under the principle of definition. Note that: (OR (FALSEP (GREATEREQPR W Z)) (TRUEP (GREATEREQPR W Z))) is a theorem. [ 0.0 0.0 0.0 ] GREATEREQPR (PROVE-LEMMA TIMES-ID-IFF-1 (REWRITE) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z 0) (EQUAL W 1))))) This conjecture simplifies, expanding the functions OR and AND, to the following four new formulas: Case 4. (IMPLIES (AND (EQUAL Z (TIMES W Z)) (NOT (EQUAL Z 0))) (EQUAL (EQUAL W 1) T)). This again simplifies, clearly, to the new conjecture: (IMPLIES (AND (EQUAL Z (TIMES W Z)) (NOT (EQUAL Z 0))) (EQUAL W 1)). We use the above equality hypothesis by substituting (TIMES W Z) for Z and keeping the equality hypothesis. The result is: (IMPLIES (AND (EQUAL Z (TIMES W Z)) (NOT (EQUAL (TIMES W Z) 0))) (EQUAL W 1)). This further simplifies, obviously, to: (IMPLIES (AND (EQUAL Z (TIMES W Z)) (NOT (EQUAL Z 0))) (EQUAL W 1)), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z 0) (EQUAL W 1)))), named *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP W) (p Z W)) (IMPLIES (AND (NOT (ZEROP W)) (p Z (SUB1 W))) (p Z W))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT W) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces two new goals: Case 2. (IMPLIES (ZEROP W) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z 0) (EQUAL W 1))))), which simplifies, expanding the functions ZEROP, EQUAL, TIMES, OR, and AND, to four new formulas: Case 2.4. (IMPLIES (AND (EQUAL W 0) (EQUAL Z 0)) (EQUAL (EQUAL Z 0) T)), which again simplifies, unfolding EQUAL, to: T. Case 2.3. (IMPLIES (AND (EQUAL W 0) (EQUAL Z 0)) (NUMBERP Z)), which again simplifies, clearly, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP W)) (EQUAL Z 0)) (EQUAL (EQUAL Z 0) T)). This again simplifies, opening up EQUAL, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP W)) (EQUAL Z 0)) (NUMBERP Z)), which again simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP W)) (EQUAL (EQUAL Z (TIMES (SUB1 W) Z)) (AND (NUMBERP Z) (OR (EQUAL Z 0) (EQUAL (SUB1 W) 1))))) (EQUAL (EQUAL Z (TIMES W Z)) (AND (NUMBERP Z) (OR (EQUAL Z 0) (EQUAL W 1))))). This simplifies, applying TIMES-ZERO2 and COMMUTATIVITY-OF-TIMES, and expanding ZEROP, OR, AND, TIMES, EQUAL, and NUMBERP, to six new goals: Case 1.6. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (EQUAL Z (TIMES (SUB1 W) Z)) (NUMBERP Z) (EQUAL (EQUAL (SUB1 W) 1) T) (NOT (EQUAL Z (PLUS Z Z)))) (NOT (EQUAL Z 0))), which again simplifies, using linear arithmetic, to: T. Case 1.5. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (EQUAL Z (TIMES (SUB1 W) Z)) (NUMBERP Z) (EQUAL (EQUAL (SUB1 W) 1) T) (NOT (EQUAL Z (PLUS Z Z)))) (NOT (EQUAL W 1))), which again simplifies, opening up the definitions of EQUAL, NUMBERP, SUB1, and TIMES, to: T. Case 1.4. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (EQUAL Z (TIMES (SUB1 W) Z)) (NUMBERP Z) (EQUAL (EQUAL (SUB1 W) 1) T) (EQUAL Z (PLUS Z Z)) (NOT (EQUAL Z 0))) (EQUAL (EQUAL W 1) T)), which again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (EQUAL Z (TIMES (SUB1 W) Z))) (NOT (EQUAL Z 0)) (NOT (EQUAL (SUB1 W) 1)) (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z)))) (EQUAL (EQUAL W 1) T)), which again simplifies, obviously, to the new formula: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (EQUAL Z (TIMES (SUB1 W) Z))) (NOT (EQUAL Z 0)) (NOT (EQUAL (SUB1 W) 1)) (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z)))) (EQUAL W 1)), which again simplifies, using linear arithmetic and applying LESSP-TIMES-2, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (EQUAL Z (TIMES (SUB1 W) Z))) (NOT (EQUAL Z 0)) (NOT (EQUAL (SUB1 W) 1)) (NOT (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z)))) (NUMBERP Z)) (NOT (EQUAL W 1))). However this again simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and unfolding EQUAL, NUMBERP, SUB1, TIMES, and PLUS, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (EQUAL Z (TIMES (SUB1 W) Z))) (NOT (EQUAL Z 0)) (NOT (EQUAL (SUB1 W) 1)) (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z)))) (NUMBERP Z)), which again simplifies, clearly, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-ID-IFF-1 (PROVE-LEMMA GREATEREQPR-LESSP (REWRITE) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y)))) This conjecture simplifies, opening up the function NOT, to the following two new goals: Case 2. (IMPLIES (NOT (LESSP X Y)) (EQUAL (GREATEREQPR X Y) T)). This again simplifies, clearly, to: (IMPLIES (NOT (LESSP X Y)) (GREATEREQPR X Y)), which we will name *1. Case 1. (IMPLIES (LESSP X Y) (EQUAL (GREATEREQPR X Y) F)). This again simplifies, obviously, to: (IMPLIES (LESSP X Y) (NOT (GREATEREQPR X Y))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y))), named *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 (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (EQUAL X Y)) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL X Y)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 formulas: Case 3. (IMPLIES (ZEROP X) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y)))), which simplifies, opening up the functions ZEROP, EQUAL, GREATEREQPR, LESSP, and NOT, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL X Y)) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y)))), which simplifies, unfolding the functions ZEROP, GREATEREQPR, and NOT, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (NOT (LESSP Y Y))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL X Y)) (EQUAL (GREATEREQPR (SUB1 X) Y) (NOT (LESSP (SUB1 X) Y)))) (EQUAL (GREATEREQPR X Y) (NOT (LESSP X Y)))), which simplifies, expanding ZEROP, NOT, and GREATEREQPR, to two new conjectures: Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X Y)) (NOT (LESSP (SUB1 X) Y)) (EQUAL (GREATEREQPR (SUB1 X) Y) T)) (NOT (LESSP X Y))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X Y)) (LESSP (SUB1 X) Y) (EQUAL (GREATEREQPR (SUB1 X) Y) F)) (LESSP X Y)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X Y)) (LESSP (SUB1 X) Y) (EQUAL (GREATEREQPR (SUB1 X) Y) F)) (LESSP X Y)). This again simplifies, expanding the function LESSP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] GREATEREQPR-LESSP (PROVE-LEMMA GREATEREQPR-REMAINDER (REWRITE) (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (DIVIDES Z (ADD1 V))) (GREATEREQPR V Z))) This formula can be simplified, using the abbreviations GREATEREQPR-LESSP, NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (EQUAL (REMAINDER (ADD1 V) Z) 0)) (NOT (LESSP V Z))), which simplifies, using linear arithmetic, rewriting with DIFFERENCE-0 and SUB1-ADD1, and expanding the functions LESSP, REMAINDER, NUMBERP, and EQUAL, to the following four new goals: Case 4. (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (NUMBERP V))) (LESSP 0 (SUB1 Z))). This again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (NOT (EQUAL 1 (ADD1 V))) (NUMBERP 1) (NOT (EQUAL 1 0)) (NOT (NUMBERP V))) (LESSP 0 (SUB1 1))). However this again simplifies, applying the lemma SUB1-TYPE-RESTRICTION, and expanding the definition of EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (NUMBERP Z) (NOT (EQUAL Z 0)) (NUMBERP V) (NOT (LESSP V (SUB1 Z)))) (NOT (LESSP V Z))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (NUMBERP Z) (NUMBERP V) (LESSP V (SUB1 Z)) (EQUAL (ADD1 V) 0)) (NOT (LESSP V Z))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL Z (ADD1 V))) (NUMBERP Z) (NOT (NUMBERP V)) (LESSP 0 (SUB1 Z)) (EQUAL (ADD1 V) 0)) (EQUAL Z 0)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GREATEREQPR-REMAINDER (PROVE-LEMMA DIVIDES-TIMES1 (REWRITE) (IMPLIES (EQUAL A (TIMES Z Y)) (EQUAL (REMAINDER A Z) 0))) WARNING: Note that DIVIDES-TIMES1 contains the free variable Y which will be chosen by instantiating the hypothesis (EQUAL A (TIMES Z Y)). This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and DIVIDES-TIMES, and expanding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIVIDES-TIMES1 (PROVE-LEMMA TIMES-IDENTITY1 (REWRITE) (IMPLIES (AND (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y))))) . We now use the above equality hypothesis by substituting (TIMES X Y) for X and keeping the equality hypothesis. This generates: (IMPLIES (AND (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL (TIMES X Y) 0))) (NOT (EQUAL X (TIMES X Y)))). This simplifies, clearly, to: (IMPLIES (AND (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y)))), 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 (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y)))), named *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 generates three new conjectures: Case 3. (IMPLIES (AND (ZEROP X) (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y)))), which simplifies, unfolding the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (SUB1 X) 0) (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y)))), which simplifies, opening up ZEROP and TIMES, to: (IMPLIES (AND (EQUAL (SUB1 X) 0) (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (EQUAL X (PLUS Y (TIMES (SUB1 X) Y))))). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))) (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0))) (NOT (EQUAL X (TIMES X Y)))), which simplifies, expanding the functions ZEROP and TIMES, to the formula: (IMPLIES (AND (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))) (NUMBERP Y) (NOT (EQUAL Y 1)) (NOT (EQUAL Y 0)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (EQUAL X (PLUS Y (TIMES (SUB1 X) Y))))). However this again simplifies, using linear arithmetic and rewriting with the lemma LESSP-TIMES-2, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-IDENTITY1 (PROVE-LEMMA TIMES-IDENTITY (REWRITE) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X 0) (AND (NUMBERP X) (EQUAL Y 1))))) This conjecture simplifies, expanding the functions AND and OR, to the following four new formulas: Case 4. (IMPLIES (AND (EQUAL X (TIMES X Y)) (NOT (EQUAL X 0))) (EQUAL (EQUAL Y 1) T)). This again simplifies, clearly, to the new conjecture: (IMPLIES (AND (EQUAL X (TIMES X Y)) (NOT (EQUAL X 0))) (EQUAL Y 1)). We use the above equality hypothesis by substituting (TIMES X Y) for X and keeping the equality hypothesis. The result is: (IMPLIES (AND (EQUAL X (TIMES X Y)) (NOT (EQUAL (TIMES X Y) 0))) (EQUAL Y 1)). This further simplifies, obviously, to: (IMPLIES (AND (EQUAL X (TIMES X Y)) (NOT (EQUAL X 0))) (EQUAL Y 1)), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X 0) (AND (NUMBERP X) (EQUAL Y 1)))), named *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 produces two new goals: Case 2. (IMPLIES (ZEROP X) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X 0) (AND (NUMBERP X) (EQUAL Y 1))))), which simplifies, expanding the functions ZEROP, EQUAL, TIMES, NUMBERP, AND, and OR, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)) (OR (EQUAL (SUB1 X) 0) (AND (NUMBERP (SUB1 X)) (EQUAL Y 1))))) (EQUAL (EQUAL X (TIMES X Y)) (OR (EQUAL X 0) (AND (NUMBERP X) (EQUAL Y 1))))), which simplifies, unfolding ZEROP, AND, OR, and TIMES, to four new formulas: Case 1.4. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)) (EQUAL (EQUAL Y 1) T)) (EQUAL X (PLUS Y (SUB1 X)))), which again simplifies, applying ADD1-SUB1, and opening up the definitions of SUB1, NUMBERP, EQUAL, and PLUS, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))) (NOT (EQUAL (SUB1 X) 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y (TIMES (SUB1 X) Y))))). This again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))) (NOT (EQUAL (SUB1 X) 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y (TIMES (SUB1 X) Y))))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ID-IFF-1, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (EQUAL (SUB1 X) 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y (TIMES Y (SUB1 X)))))). 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. This produces the following two new conjectures: Case 1.3.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL X 0)) (NOT (EQUAL (SUB1 X) 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y (TIMES Y (SUB1 X)))))). This further simplifies, clearly, to: T. Case 1.3.1. (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))). This further simplifies, obviously, to the new formula: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))), which we will finally name *1.1. Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)) (EQUAL (SUB1 X) 0) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y (SUB1 X))))). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL 0 (TIMES 0 Y)) (EQUAL (SUB1 X) 0) (NOT (EQUAL Y 1))) (NOT (EQUAL X (PLUS Y 0)))). But this again simplifies, rewriting with PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and unfolding the definitions of NUMBERP and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)) (EQUAL (SUB1 X) 0) (EQUAL Y 1)) (EQUAL (EQUAL X (PLUS Y (SUB1 X))) T)). This again simplifies, unfolding the functions TIMES, EQUAL, and PLUS, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (SUB1 X) 0)) (EQUAL X 1)). This again simplifies, using linear arithmetic, to: T. So let us turn our attention to: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))), named *1.1 above. We will try to prove it by induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Y) (p Z Y)) (IMPLIES (AND (NOT (ZEROP Y)) (p Z (SUB1 Y))) (p Z Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates three new formulas: Case 3. (IMPLIES (AND (ZEROP Y) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))), which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and expanding the functions ZEROP, EQUAL, TIMES, PLUS, and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Y)) (EQUAL (SUB1 Y) 1) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))). This simplifies, unfolding the functions ZEROP and TIMES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (EQUAL (SUB1 Y) 1) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y Z (TIMES (SUB1 Y) Z))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (NOT (EQUAL (ADD1 Z) (PLUS (SUB1 Y) (TIMES (SUB1 Y) Z)))) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y (TIMES Y Z))))), which simplifies, expanding the definitions of ZEROP and TIMES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (ADD1 Z) (PLUS (SUB1 Y) (TIMES (SUB1 Y) Z)))) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (EQUAL Y 1))) (NOT (EQUAL (ADD1 Z) (PLUS Y Z (TIMES (SUB1 Y) Z))))). This again simplifies, using linear arithmetic and rewriting with the lemma LESSP-TIMES-2, to: T. That finishes the proof of *1.1, which finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] TIMES-IDENTITY (PROVE-LEMMA QUOTIENT-DIVIDES (REWRITE) (IMPLIES (AND (NUMBERP Y) (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y))) (NOT (EQUAL (REMAINDER Y X) 0)))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES X Z)) to eliminate (QUOTIENT Y X) and (REMAINDER Y X). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to restrict the new variables. This produces the following three new conjectures: Case 3. (IMPLIES (AND (EQUAL X 0) (NUMBERP Y) (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y))) (NOT (EQUAL (REMAINDER Y X) 0))). But this simplifies, opening up the functions EQUAL, QUOTIENT, TIMES, and REMAINDER, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (NUMBERP Y) (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y))) (NOT (EQUAL (REMAINDER Y X) 0))), which simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-TIMES, and REMAINDER-WRT-12, and opening up the definition of QUOTIENT, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V X) (NOT (ZEROP X))) (NUMBERP X) (NOT (EQUAL X 0)) (NOT (EQUAL (TIMES X Z) (PLUS V (TIMES X Z))))) (NOT (EQUAL V 0))). But this simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-DIVIDES (PROVE-LEMMA REMAINDER-TIMES (REWRITE) (EQUAL (REMAINDER (TIMES Y X) Y) 0)) This conjecture simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and DIVIDES-TIMES, and expanding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-TIMES (PROVE-LEMMA QUOTIENT-TIMES (REWRITE) (EQUAL (QUOTIENT (TIMES Y X) Y) (IF (ZEROP Y) 0 (FIX X)))) This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding the functions ZEROP and FIX, to four new conjectures: Case 4. (IMPLIES (EQUAL Y 0) (EQUAL (QUOTIENT (TIMES X Y) Y) 0)), which again simplifies, applying COMMUTATIVITY-OF-TIMES, and opening up EQUAL, TIMES, and QUOTIENT, to: T. Case 3. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (QUOTIENT (TIMES X Y) Y) 0)). This again simplifies, applying TIMES-ZERO2, and opening up the functions QUOTIENT and EQUAL, to: T. Case 2. (IMPLIES (NOT (NUMBERP X)) (EQUAL (QUOTIENT (TIMES X Y) Y) 0)). However this again simplifies, unfolding the definitions of TIMES, LESSP, EQUAL, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (EQUAL (QUOTIENT (TIMES X Y) Y) X)), which we will name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, 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 two new goals: Case 2. (IMPLIES (AND (ZEROP X) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (EQUAL (QUOTIENT (TIMES X Y) Y) X)), which simplifies, opening up ZEROP, NUMBERP, EQUAL, TIMES, LESSP, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (QUOTIENT (TIMES (SUB1 X) Y) Y) (SUB1 X)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (EQUAL (QUOTIENT (TIMES X Y) Y) X)), which simplifies, rewriting with ADD1-SUB1 and DIFFERENCE-PLUS1, and expanding the functions ZEROP, TIMES, and QUOTIENT, to the new formula: (IMPLIES (AND (NOT (EQUAL X 0)) (EQUAL (QUOTIENT (TIMES (SUB1 X) Y) Y) (SUB1 X)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X)) (NOT (LESSP (PLUS Y (TIMES (SUB1 X) Y)) Y))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-TIMES (PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES (REWRITE) (IMPLIES (AND (NOT (ZEROP A)) (DIVIDES A W)) (EQUAL (TIMES C (QUOTIENT W A)) (QUOTIENT (TIMES C W) A)))) WARNING: the newly proposed lemma, DISTRIBUTIVITY-OF-DIVIDES, could be applied whenever the previously added lemma QUOTIENT-TIMES1 could. WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed DISTRIBUTIVITY-OF-DIVIDES could! This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (REMAINDER W A) 0)) (EQUAL (TIMES C (QUOTIENT W A)) (QUOTIENT (TIMES C W) A))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace W by (PLUS X (TIMES A Z)) to eliminate (REMAINDER W A) and (QUOTIENT W A). We use LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. This generates two new conjectures: Case 2. (IMPLIES (AND (NOT (NUMBERP W)) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (REMAINDER W A) 0)) (EQUAL (TIMES C (QUOTIENT W A)) (QUOTIENT (TIMES C W) A))), which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ZERO2, and opening up LESSP, REMAINDER, EQUAL, QUOTIENT, and TIMES, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X A) (NOT (ZEROP A))) (NUMBERP Z) (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL X 0)) (EQUAL (TIMES C Z) (QUOTIENT (TIMES C (PLUS X (TIMES A Z))) A))). But this simplifies, rewriting with COMMUTATIVITY2-OF-TIMES and QUOTIENT-TIMES, and expanding the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DISTRIBUTIVITY-OF-DIVIDES (PROVE-LEMMA IF-TIMES-THEN-DIVIDES (REWRITE) (IMPLIES (AND (NOT (ZEROP C)) (NOT (DIVIDES C X))) (NOT (EQUAL (TIMES C Y) X)))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, IMPLIES, and DIVIDES, to the new conjecture: (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (NOT (EQUAL (REMAINDER X C) 0))) (NOT (EQUAL (TIMES C Y) X))), which simplifies, applying REMAINDER-TIMES, and unfolding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] IF-TIMES-THEN-DIVIDES (PROVE-LEMMA TIMES-EQUAL-1 (REWRITE) (EQUAL (EQUAL (TIMES A B) 1) (AND (NOT (EQUAL A 0)) (NOT (EQUAL B 0)) (NUMBERP A) (NUMBERP B) (EQUAL (SUB1 A) 0) (EQUAL (SUB1 B) 0)))) This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and opening up the definitions of TIMES, NOT, and AND, to the following five new formulas: Case 5. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (PLUS B (SUB1 A) (TIMES (SUB1 A) (SUB1 B))) 1)) (EQUAL (EQUAL (SUB1 B) 0) T)). But this again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (NOT (EQUAL 1 0)) (NUMBERP 1) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (PLUS B (SUB1 1) (TIMES (SUB1 1) (SUB1 B))) 1)) (EQUAL (EQUAL (SUB1 B) 0) T)). This again simplifies, applying the lemma COMMUTATIVITY-OF-PLUS, and opening up the functions EQUAL, NUMBERP, SUB1, TIMES, and PLUS, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL (PLUS B (SUB1 A) (TIMES (SUB1 A) (SUB1 B))) 1)) (EQUAL (SUB1 A) 0)) (NOT (EQUAL (SUB1 B) 0))), which again simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and expanding the functions TIMES, PLUS, and EQUAL, to the goal: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL B 1)) (EQUAL (SUB1 A) 0)) (NOT (EQUAL (SUB1 B) 0))). But this again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL B 0)) (NOT (EQUAL (PLUS B 0) 1))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (NUMBERP B))) (NOT (EQUAL (PLUS B 0) 1))), which again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and expanding NUMBERP and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (PLUS B (SUB1 A) (TIMES (SUB1 A) (SUB1 B))) 1)) (EQUAL (SUB1 A) 0)). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-EQUAL-1 (PROVE-LEMMA DIVIDES-IMPLIES-TIMES (REWRITE) (IMPLIES (AND (NOT (ZEROP A)) (NUMBERP C) (EQUAL (TIMES A C) B)) (EQUAL (EQUAL C (QUOTIENT B A)) T))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NUMBERP C) (EQUAL (TIMES A C) B)) (EQUAL (EQUAL C (QUOTIENT B A)) T)). This simplifies, applying the lemma QUOTIENT-TIMES, and opening up EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIVIDES-IMPLIES-TIMES (PROVE-LEMMA DIFFERENCE-1 (REWRITE) (EQUAL (DIFFERENCE X 1) (SUB1 X))) This simplifies, using linear arithmetic, to: (IMPLIES (LESSP X 1) (EQUAL (DIFFERENCE X 1) (SUB1 X))). However this again simplifies, using linear arithmetic and applying DIFFERENCE-0, to: (IMPLIES (LESSP X 1) (EQUAL 0 (SUB1 X))). Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X). We rely upon the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove the following three new conjectures: Case 3. (IMPLIES (AND (EQUAL X 0) (LESSP X 1)) (EQUAL 0 (SUB1 X))). But this further simplifies, unfolding the functions LESSP, SUB1, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 1)) (EQUAL 0 (SUB1 X))), which further simplifies, rewriting with SUB1-NNUMBERP, and expanding the definitions of NUMBERP, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (LESSP (ADD1 Z) 1)) (EQUAL 0 Z)). This further simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-1 (PROVE-LEMMA DIFFERENCE-2 (REWRITE) (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2) (FIX X))) This formula simplifies, applying DIFFERENCE-1 and SUB1-ADD1, and opening up the functions SUB1, NUMBERP, EQUAL, DIFFERENCE, and FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-2 (PROVE-LEMMA HALF-PLUS (REWRITE) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))) . Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by (PLUS V (TIMES 2 Z)) to eliminate (QUOTIENT Y 2) and (REMAINDER Y 2). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to constrain the new variables. The result is four new conjectures: Case 4. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))), which simplifies, rewriting with the lemmas PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and unfolding the functions LESSP, NUMBERP, EQUAL, QUOTIENT, and PLUS, to two new formulas: Case 4.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (QUOTIENT (PLUS X 0) 2) 0)), which again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and expanding the definitions of NUMBERP, QUOTIENT, and EQUAL, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (QUOTIENT (PLUS X X) 2) X)). This again simplifies, using linear arithmetic, rewriting with DIVIDES-IMPLIES-TIMES, and expanding EQUAL, to: T. Case 3. (IMPLIES (EQUAL 2 0) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))). However this simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (NOT (NUMBERP 2)) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))), which simplifies, clearly, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V 2) (NOT (ZEROP 2))) (NOT (EQUAL 2 0))) (EQUAL (QUOTIENT (PLUS X X V (TIMES 2 Z)) 2) (PLUS X Z))). This simplifies, applying COMMUTATIVITY2-OF-PLUS, and unfolding the functions ZEROP, NOT, and EQUAL, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (LESSP V 2)) (EQUAL (QUOTIENT (PLUS V X X (TIMES 2 Z)) 2) (PLUS X Z))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2))), named *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest four inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition of ZEROP can be used to prove 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 the following two new formulas: Case 2. (IMPLIES (ZEROP X) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))). This simplifies, opening up ZEROP, EQUAL, and PLUS, to the following two new goals: Case 2.2. (IMPLIES (AND (EQUAL X 0) (NOT (NUMBERP Y))) (EQUAL (QUOTIENT 0 2) (QUOTIENT Y 2))). This again simplifies, expanding the definitions of QUOTIENT, LESSP, NUMBERP, and EQUAL, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (NUMBERP Y))) (EQUAL (QUOTIENT 0 2) (QUOTIENT Y 2))), which again simplifies, expanding the functions QUOTIENT, LESSP, NUMBERP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (QUOTIENT (PLUS (SUB1 X) (SUB1 X) Y) 2) (PLUS (SUB1 X) (QUOTIENT Y 2)))) (EQUAL (QUOTIENT (PLUS X X Y) 2) (PLUS X (QUOTIENT Y 2)))), which simplifies, applying PLUS-ADD1, DIFFERENCE-2, and SUB1-ADD1, and expanding ZEROP, PLUS, LESSP, SUB1, NUMBERP, EQUAL, and QUOTIENT, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] HALF-PLUS (PROVE-LEMMA TIMES-1 (REWRITE) (EQUAL (TIMES 1 X) (FIX X))) WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied whenever the newly proposed TIMES-1 could! This simplifies, unfolding FIX, to two new formulas: Case 2. (IMPLIES (NOT (NUMBERP X)) (EQUAL (TIMES 1 X) 0)), which again simplifies, rewriting with TIMES-ZERO2, and unfolding the definition of EQUAL, to: T. Case 1. (IMPLIES (NUMBERP X) (EQUAL (TIMES 1 X) X)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-1 (PROVE-LEMMA EXP-OF-0 (REWRITE) (EQUAL (EXP 0 K) (IF (ZEROP K) 1 0))) This simplifies, opening up the functions TIMES, EQUAL, EXP, and ZEROP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXP-OF-0 (PROVE-LEMMA EXP-OF-1 (REWRITE) (EQUAL (EXP 1 K) 1)) 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 K) (p K)) (IMPLIES (AND (NOT (ZEROP K)) (p (SUB1 K))) (p K))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to establish that the measure (COUNT K) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following two new formulas: Case 2. (IMPLIES (ZEROP K) (EQUAL (EXP 1 K) 1)). This simplifies, expanding the definitions of ZEROP, EXP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP K)) (EQUAL (EXP 1 (SUB1 K)) 1)) (EQUAL (EXP 1 K) 1)). This simplifies, opening up the functions ZEROP, EXP, TIMES, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EXP-OF-1 (PROVE-LEMMA EXP-BY-0 (REWRITE) (EQUAL (EXP X 0) 1)) This simplifies, unfolding EQUAL and EXP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXP-BY-0 (PROVE-LEMMA EXP-TIMES (REWRITE) (EQUAL (EXP (TIMES I J) K) (TIMES (EXP I K) (EXP J K)))) Call the conjecture *1. We will try to prove it by induction. There are four plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP K) (p I J K)) (IMPLIES (AND (NOT (ZEROP K)) (p I J (SUB1 K))) (p I J K))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT K) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (ZEROP K) (EQUAL (EXP (TIMES I J) K) (TIMES (EXP I K) (EXP J K)))), which simplifies, appealing to the lemma EXP-BY-0, and unfolding ZEROP, TIMES, EQUAL, and EXP, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP K)) (EQUAL (EXP (TIMES I J) (SUB1 K)) (TIMES (EXP I (SUB1 K)) (EXP J (SUB1 K))))) (EQUAL (EXP (TIMES I J) K) (TIMES (EXP I K) (EXP J K)))), which simplifies, rewriting with the lemmas ASSOCIATIVITY-OF-TIMES and COMMUTATIVITY2-OF-TIMES, and expanding the functions ZEROP and EXP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EXP-TIMES (PROVE-LEMMA EXP-EXP (REWRITE) (EQUAL (EXP (EXP I J) K) (EXP I (TIMES J K)))) Call the conjecture *1. Perhaps we can prove it by 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 (ZEROP J) (p I J K)) (IMPLIES (AND (NOT (ZEROP J)) (p I (SUB1 J) K)) (p I J K))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to prove that the measure (COUNT J) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP J) (EQUAL (EXP (EXP I J) K) (EXP I (TIMES J K)))), which simplifies, applying the lemmas EXP-BY-0 and EXP-OF-1, and opening up the definitions of ZEROP, EQUAL, TIMES, and EXP, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (EQUAL (EXP (EXP I (SUB1 J)) K) (EXP I (TIMES (SUB1 J) K)))) (EQUAL (EXP (EXP I J) K) (EXP I (TIMES J K)))), which simplifies, rewriting with EXP-TIMES and EXP-PLUS, and opening up the functions ZEROP, EXP, and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EXP-EXP (PROVE-LEMMA REMAINDER-PLUS-TIMES-1 (REWRITE) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS Z (TIMES J V)) to eliminate (REMAINDER X J) and (QUOTIENT X J). We rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following four new conjectures: Case 4. (IMPLIES (NOT (NUMBERP X)) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))). But this simplifies, applying the lemma DIVIDES-TIMES, and opening up the definitions of PLUS, LESSP, REMAINDER, and EQUAL, to: T. Case 3. (IMPLIES (EQUAL J 0) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))), which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and opening up the functions EQUAL, TIMES, PLUS, and REMAINDER, to: T. Case 2. (IMPLIES (NOT (NUMBERP J)) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))). But this simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-PLUS, and REMAINDER-WRT-12, and opening up the functions EQUAL and PLUS, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z J) (NOT (ZEROP J))) (NUMBERP V) (NUMBERP J) (NOT (EQUAL J 0))) (EQUAL (REMAINDER (PLUS (PLUS Z (TIMES J V)) (TIMES I J)) J) Z)). But this simplifies, applying COMMUTATIVITY-OF-PLUS and ASSOCIATIVITY-OF-PLUS, and opening up the functions ZEROP and NOT, to: (IMPLIES (AND (NUMBERP Z) (LESSP Z J) (NUMBERP V) (NUMBERP J) (NOT (EQUAL J 0))) (EQUAL (REMAINDER (PLUS Z (TIMES I J) (TIMES J V)) J) Z)), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J)), named *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest three inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP I) (p X I J)) (IMPLIES (AND (NOT (ZEROP I)) (p X (SUB1 I) J)) (p X I J))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new formulas: Case 2. (IMPLIES (ZEROP I) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))), which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding ZEROP, EQUAL, TIMES, and PLUS, to the following two new conjectures: Case 2.2. (IMPLIES (AND (EQUAL I 0) (NOT (NUMBERP X))) (EQUAL (REMAINDER 0 J) (REMAINDER X J))). However this again simplifies, unfolding the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (NUMBERP X))) (EQUAL (REMAINDER 0 J) (REMAINDER X J))), which again simplifies, opening up the definitions of LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (EQUAL (REMAINDER (PLUS X (TIMES (SUB1 I) J)) J) (REMAINDER X J))) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))), which simplifies, applying COMMUTATIVITY2-OF-PLUS and DIFFERENCE-PLUS1, and unfolding ZEROP, TIMES, REMAINDER, EQUAL, and PLUS, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (REMAINDER (PLUS X (TIMES (SUB1 I) J)) J) (REMAINDER X J)) (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (PLUS J X (TIMES (SUB1 I) J)) J)) (EQUAL (PLUS J X (TIMES (SUB1 I) J)) (REMAINDER X J))). But this again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (REMAINDER (PLUS X (TIMES (SUB1 I) J)) J) (REMAINDER X J)) (EQUAL J 0)) (EQUAL (PLUS X (TIMES (SUB1 I) J)) (REMAINDER X J))), which again simplifies, applying COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and unfolding EQUAL, TIMES, PLUS, and REMAINDER, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (REMAINDER (PLUS X (TIMES (SUB1 I) J)) J) (REMAINDER X J)) (NOT (NUMBERP J))) (EQUAL (PLUS X (TIMES (SUB1 I) J)) (REMAINDER X J))). This again simplifies, applying the lemmas REMAINDER-WRT-12 and EQUAL-TIMES-0, and opening up the function PLUS, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-PLUS-TIMES-1 (PROVE-LEMMA REMAINDER-PLUS-TIMES-2 (REWRITE) (EQUAL (REMAINDER (PLUS X (TIMES J I)) J) (REMAINDER X J))) This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and REMAINDER-PLUS-TIMES-1, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-PLUS-TIMES-2 (PROVE-LEMMA REMAINDER-TIMES-1 (REWRITE) (EQUAL (REMAINDER (TIMES B A C) A) 0)) This formula simplifies, applying COMMUTATIVITY2-OF-TIMES and REMAINDER-TIMES, and opening up the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-TIMES-1 (PROVE-LEMMA REMAINDER-OF-1 (REWRITE) (EQUAL (REMAINDER 1 X) (IF (EQUAL X 1) 0 1))) This simplifies, rewriting with DIFFERENCE-0, and opening up DIFFERENCE, EQUAL, SUB1, LESSP, NUMBERP, and REMAINDER, to four new conjectures: Case 4. (IMPLIES (AND (NOT (EQUAL X 1)) (NOT (EQUAL X 0)) (NUMBERP X)) (LESSP 1 X)), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (EQUAL X 1) (NOT (LESSP 1 X))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (EQUAL X 1) (NUMBERP X)), which again simplifies, trivially, to: T. Case 1. (IMPLIES (EQUAL X 1) (NOT (EQUAL X 0))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-OF-1 (DEFN LENGTH (LST) (IF (LISTP LST) (ADD1 (LENGTH (CDR LST))) 0)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, LENGTH is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (LENGTH LST)) is a theorem. [ 0.0 0.0 0.0 ] LENGTH (PROVE-LEMMA EQUAL-LENGTH-0 (REWRITE) (EQUAL (EQUAL (LENGTH X) 0) (NLISTP X))) This formula simplifies, opening up the definition of NLISTP, to two new conjectures: Case 2. (IMPLIES (NOT (EQUAL (LENGTH X) 0)) (LISTP X)), which again simplifies, unfolding the definitions of LENGTH and EQUAL, to: T. Case 1. (IMPLIES (EQUAL (LENGTH X) 0) (NOT (LISTP X))), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces two new formulas: Case 2. (IMPLIES (AND (NOT (EQUAL (LENGTH (CDR X)) 0)) (EQUAL (LENGTH X) 0)) (NOT (LISTP X))), which simplifies, opening up LENGTH, to: T. Case 1. (IMPLIES (AND (NOT (LISTP (CDR X))) (EQUAL (LENGTH X) 0)) (NOT (LISTP X))), which simplifies, opening up LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-LENGTH-0 (PROVE-LEMMA REMAINDER-DIFFERENCE-TIMES (REWRITE) (EQUAL (REMAINDER (DIFFERENCE (TIMES P X) (TIMES P Y)) P) 0) ((USE (DIVIDES-TIMES (X (DIFFERENCE X Y)))) (DISABLE DIVIDES-TIMES))) This formula simplifies, appealing to the lemmas TIMES-DIFFERENCE, COMMUTATIVITY-OF-TIMES, REMAINDER-TIMES, and EUCLID, and expanding the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-DIFFERENCE-TIMES (PROVE-LEMMA LESSP-REMAINDER-DIVISOR (REWRITE) (IMPLIES (NOT (ZEROP Y)) (LESSP (REMAINDER X Y) Y))) WARNING: Note that the proposed lemma LESSP-REMAINDER-DIVISOR is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)), which simplifies, appealing to the lemma LESSP-REMAINDER2, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-REMAINDER-DIVISOR (MAKE-LIB "arith") Making the lib for "arith". Finished making the lib for "arith". (/stage/ftp/pub/boyer/pc-nqthm/pc-nqthm-1992/examples/basic/arith.lib /stage/ftp/pub/boyer/pc-nqthm/pc-nqthm-1992/examples/basic/arith.lisp)