(BOOT-STRAP) [ 0.0 0.0 0.0 ] GROUND-ZERO (COMPILE-UNCOMPILED-DEFNS "tmp") Loading ./hunt/tmp.o Finished loading ./hunt/tmp.o /v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/hunt/tmp.lisp (PROVE-LEMMA PLUS-1 (REWRITE) (EQUAL (PLUS 1 X) (ADD1 X))) This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-1 (PROVE-LEMMA PLUS-RIGHT-ID (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-ID (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 (PLUS Y Z)) (PLUS Y (PLUS 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-ID could. WARNING: the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the previously added lemma PLUS-1 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 (PLUS 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-ID 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-ID, 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-ID, 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 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-ID, 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-ID, 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-ID, 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-ID, 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-ID 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 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-ID 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-ID 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, PLUS-1, and ADD1-SUB1, and unfolding TIMES, 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)))). However this 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 (TIMES Y Z)) (TIMES Y (TIMES 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 (TIMES 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 (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 EQUAL-BOOLS (REWRITE) (IMPLIES (AND (OR (EQUAL BOOL1 T) (EQUAL BOOL1 F)) (OR (EQUAL BOOL2 T) (EQUAL BOOL2 F))) (EQUAL (EQUAL BOOL1 BOOL2) (AND (IMPLIES BOOL1 BOOL2) (IMPLIES BOOL2 BOOL1))))) This conjecture simplifies, unfolding the functions OR, EQUAL, IMPLIES, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-BOOLS (DISABLE EQUAL-BOOLS) [ 0.0 0.0 0.0 ] EQUAL-BOOLS-OFF (PROVE-LEMMA LESSP-TIMES (REWRITE) (EQUAL (LESSP (TIMES Y X) (TIMES X Z)) (AND (NOT (ZEROP X)) (LESSP Y Z))) ((ENABLE EQUAL-BOOLS))) This conjecture simplifies, rewriting with COMMUTATIVITY-OF-TIMES and EQUAL-BOOLS, and expanding the definitions of ZEROP, NOT, AND, and OR, to the following four new goals: Case 4. (IMPLIES (AND (NOT (LESSP (TIMES X Y) (TIMES X Z))) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP Y Z))). Call the above conjecture *1. Case 3. (IMPLIES (LESSP (TIMES X Y) (TIMES X Z)) (LESSP Y Z)), 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 Y X) (TIMES X Z)) (AND (NOT (ZEROP X)) (LESSP Y Z))). We gave this the name *1 above. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest four inductions. They merge into two likely candidate inductions, both of which are flawed. We limit our consideration to the two suggested by the largest number of nonprimitive recursive functions in the conjecture. However, one of these is more likely than the other. We will induct according to the following scheme: (AND (IMPLIES (ZEROP Y) (p Y X Z)) (IMPLIES (AND (NOT (ZEROP Y)) (p (SUB1 Y) X (SUB1 Z))) (p Y X Z))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP 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 Z. The above induction scheme produces two new conjectures: Case 2. (IMPLIES (ZEROP Y) (EQUAL (LESSP (TIMES Y X) (TIMES X Z)) (AND (NOT (ZEROP X)) (LESSP Y Z)))), which simplifies, applying EQUAL-TIMES-0, EQUAL-BOOLS, TIMES-ZERO2, and COMMUTATIVITY-OF-TIMES, and unfolding ZEROP, EQUAL, TIMES, LESSP, NOT, AND, and OR, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP Y)) (EQUAL (LESSP (TIMES (SUB1 Y) X) (TIMES X (SUB1 Z))) (AND (NOT (ZEROP X)) (LESSP (SUB1 Y) (SUB1 Z))))) (EQUAL (LESSP (TIMES Y X) (TIMES X Z)) (AND (NOT (ZEROP X)) (LESSP Y Z)))). This simplifies, applying EQUAL-BOOLS and COMMUTATIVITY-OF-TIMES, and unfolding the definitions of ZEROP, NOT, AND, OR, LESSP, TIMES, and EQUAL, to four new formulas: Case 1.4. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (LESSP (TIMES (SUB1 Y) X) (TIMES X (SUB1 Z)))) (NOT (LESSP (SUB1 Y) (SUB1 Z)))) (NOT (LESSP (TIMES X Y) (TIMES X Z)))), which further simplifies, applying COMMUTATIVITY-OF-TIMES, to the new formula: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (LESSP (TIMES X (SUB1 Y)) (TIMES X (SUB1 Z)))) (NOT (LESSP (SUB1 Y) (SUB1 Z)))) (NOT (LESSP (TIMES X Y) (TIMES X Z)))). Applying the lemma SUB1-ELIM, replace Y by (ADD1 V) to eliminate (SUB1 Y). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain: (IMPLIES (AND (NUMBERP V) (NOT (EQUAL (ADD1 V) 0)) (NOT (LESSP (TIMES X V) (TIMES X (SUB1 Z)))) (NOT (LESSP V (SUB1 Z)))) (NOT (LESSP (TIMES X (ADD1 V)) (TIMES X Z)))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ADD1, to the new formula: (IMPLIES (AND (NUMBERP V) (NOT (LESSP (TIMES V X) (TIMES X (SUB1 Z)))) (NOT (LESSP V (SUB1 Z)))) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X Z)))). Applying the lemma SUB1-ELIM, replace Z by (ADD1 W) to eliminate (SUB1 Z). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces the following three new goals: Case 1.4.3. (IMPLIES (AND (EQUAL Z 0) (NUMBERP V) (NOT (LESSP (TIMES V X) (TIMES X (SUB1 Z)))) (NOT (LESSP V (SUB1 Z)))) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X Z)))). This finally simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding SUB1, EQUAL, TIMES, and LESSP, to: T. Case 1.4.2. (IMPLIES (AND (NOT (NUMBERP Z)) (NUMBERP V) (NOT (LESSP (TIMES V X) (TIMES X (SUB1 Z)))) (NOT (LESSP V (SUB1 Z)))) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X Z)))). This finally simplifies, applying the lemmas SUB1-NNUMBERP, COMMUTATIVITY-OF-TIMES, and TIMES-ZERO2, and expanding the definitions of EQUAL, TIMES, and LESSP, to: T. Case 1.4.1. (IMPLIES (AND (NUMBERP W) (NOT (EQUAL (ADD1 W) 0)) (NUMBERP V) (NOT (LESSP (TIMES V X) (TIMES X W))) (NOT (LESSP V W))) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X (ADD1 W))))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ADD1, to: (IMPLIES (AND (NUMBERP W) (NUMBERP V) (NOT (LESSP (TIMES V X) (TIMES W X))) (NOT (LESSP V W))) (NOT (LESSP (PLUS X (TIMES V X)) (PLUS X (TIMES W X))))), which finally simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (TIMES (SUB1 Y) X) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (SUB1 Y) (SUB1 Z)) (NOT (LESSP (TIMES X Y) (TIMES X Z))) (NOT (EQUAL Z 0))) (NOT (NUMBERP Z))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (TIMES X (SUB1 Y)) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (SUB1 Y) (SUB1 Z)) (NOT (LESSP (TIMES X Y) (TIMES X Z))) (NOT (EQUAL Z 0))) (NOT (NUMBERP Z))). Applying the lemma SUB1-ELIM, replace Y by (ADD1 V) to eliminate (SUB1 Y). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove the new goal: (IMPLIES (AND (NUMBERP V) (NOT (EQUAL (ADD1 V) 0)) (LESSP (TIMES X V) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP V (SUB1 Z)) (NOT (LESSP (TIMES X (ADD1 V)) (TIMES X Z))) (NOT (EQUAL Z 0))) (NOT (NUMBERP Z))), which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ADD1, to: (IMPLIES (AND (NUMBERP V) (LESSP (TIMES V X) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP V (SUB1 Z)) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X Z))) (NOT (EQUAL Z 0))) (NOT (NUMBERP Z))). Applying the lemma SUB1-ELIM, replace Z by (ADD1 W) to eliminate (SUB1 Z). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new goal: (IMPLIES (AND (NUMBERP W) (NUMBERP V) (LESSP (TIMES V X) (TIMES X W)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP V W) (NOT (LESSP (PLUS X (TIMES V X)) (TIMES X (ADD1 W))))) (EQUAL (ADD1 W) 0)), which further simplifies, applying COMMUTATIVITY-OF-TIMES and TIMES-ADD1, to: (IMPLIES (AND (NUMBERP W) (NUMBERP V) (LESSP (TIMES V X) (TIMES W X)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP V W)) (LESSP (PLUS X (TIMES V X)) (PLUS X (TIMES W X)))), which finally simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (TIMES (SUB1 Y) X) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (SUB1 Y) (SUB1 Z)) (LESSP (TIMES X Y) (TIMES X Z))) (NUMBERP Z)), which again simplifies, applying SUB1-NNUMBERP and COMMUTATIVITY-OF-TIMES, and expanding EQUAL, TIMES, and LESSP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (TIMES (SUB1 Y) X) (TIMES X (SUB1 Z))) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (SUB1 Y) (SUB1 Z)) (LESSP (TIMES X Y) (TIMES X Z))) (NOT (EQUAL Z 0))). This again simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, and unfolding the functions SUB1, EQUAL, TIMES, and LESSP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] LESSP-TIMES (PROVE-LEMMA TIMES-2-NOT-1 (REWRITE) (NOT (EQUAL (TIMES 2 X) 1))) This formula simplifies, applying the lemma TIMES-1, and expanding the definitions of SUB1, NUMBERP, EQUAL, and TIMES, to two new conjectures: Case 2. (IMPLIES (NOT (NUMBERP X)) (NOT (EQUAL (PLUS X 0) 1))), which again simplifies, applying PLUS-RIGHT-ID and COMMUTATIVITY-OF-PLUS, and opening up NUMBERP and EQUAL, to: T. Case 1. (IMPLIES (NUMBERP X) (NOT (EQUAL (PLUS X X) 1))). Give the above formula the 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 X)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X))) (p X))). 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 generates two new formulas: Case 2. (IMPLIES (AND (ZEROP X) (NUMBERP X)) (NOT (EQUAL (PLUS X X) 1))), which simplifies, opening up ZEROP, NUMBERP, PLUS, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (PLUS (SUB1 X) (SUB1 X)) 1)) (NUMBERP X)) (NOT (EQUAL (PLUS X X) 1))), which simplifies, applying COMMUTATIVITY-OF-PLUS and ADD1-EQUAL, and expanding the functions ZEROP, PLUS, and NUMBERP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-2-NOT-1 (PROVE-LEMMA LESSP-CROCK1 (REWRITE) (EQUAL (LESSP (PLUS Z (TIMES 2 V W)) W) (AND (ZEROP V) (LESSP Z W)))) This formula simplifies, applying the lemma TIMES-1, and unfolding SUB1, NUMBERP, EQUAL, TIMES, ZEROP, and AND, to the following three new goals: Case 3. (IMPLIES (NOT (NUMBERP V)) (EQUAL (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W) (LESSP Z W))). However this again simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and opening up the definitions of TIMES, PLUS, and EQUAL, to: (IMPLIES (AND (NOT (NUMBERP V)) (NOT (NUMBERP Z))) (EQUAL (LESSP 0 W) (LESSP Z W))), which again simplifies, opening up EQUAL and LESSP, to: T. Case 2. (IMPLIES (EQUAL V 0) (EQUAL (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W) (LESSP Z W))), which again simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and expanding EQUAL, TIMES, and PLUS, to: (IMPLIES (NOT (NUMBERP Z)) (EQUAL (LESSP 0 W) (LESSP Z W))). However this again simplifies, opening up the functions EQUAL and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V)) (EQUAL (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W) F)), which again simplifies, clearly, to the new goal: (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W))), which we will name *1. We will appeal to induction. The recursive terms in the conjecture suggest four inductions. They merge into three likely candidate inductions, two of which are unflawed. However, one of these is more likely than the other. We will induct according to the following scheme: (AND (IMPLIES (ZEROP V) (p Z V W)) (IMPLIES (AND (NOT (ZEROP V)) (p Z (SUB1 V) W)) (p Z V W))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to prove that the measure (COUNT V) 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 V) (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W))), which simplifies, unfolding ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP V)) (EQUAL (SUB1 V) 0) (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W))), which simplifies, applying EQUAL-TIMES-0, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and expanding the functions ZEROP, TIMES, EQUAL, and PLUS, to: (IMPLIES (AND (EQUAL (SUB1 V) 0) (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS W W Z (TIMES (SUB1 V) W)) W))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP V)) (NOT (LESSP (PLUS Z (TIMES (SUB1 V) W) (TIMES (SUB1 V) W)) W)) (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS Z (TIMES V W) (TIMES V W)) W))), which simplifies, applying the lemmas COMMUTATIVITY2-OF-PLUS and ASSOCIATIVITY-OF-PLUS, and opening up the definitions of ZEROP and TIMES, to: (IMPLIES (AND (NOT (LESSP (PLUS Z (TIMES (SUB1 V) W) (TIMES (SUB1 V) W)) W)) (NOT (EQUAL V 0)) (NUMBERP V)) (NOT (LESSP (PLUS W W Z (TIMES (SUB1 V) W) (TIMES (SUB1 V) W)) W))). This again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-CROCK1 (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, appealing to the lemma TIMES-1, and unfolding ZEROP, EQUAL, PLUS, and EXP, to two new formulas: Case 2.2. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP K))) (EQUAL (EXP I 0) (EXP I K))), which again simplifies, expanding the functions EQUAL and EXP, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP K))) (EQUAL (EXP I 0) (EXP I K))), which again simplifies, opening up the definitions of EQUAL and EXP, 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, applying COMMUTATIVITY-OF-TIMES, SUB1-ADD1, and ASSOCIATIVITY-OF-TIMES, and unfolding 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 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-2-NEVER-0 (REWRITE) (LESSP 0 (EXP 2 I))) WARNING: Note that the proposed lemma EXP-2-NEVER-0 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, unfolding EQUAL and LESSP, to: (NOT (EQUAL (EXP 2 I) 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 I) (p I)) (IMPLIES (AND (NOT (ZEROP I)) (p (SUB1 I))) (p I))). 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 generates two new goals: Case 2. (IMPLIES (ZEROP I) (NOT (EQUAL (EXP 2 I) 0))), which simplifies, opening up the functions ZEROP, EXP, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (NOT (EQUAL (EXP 2 (SUB1 I)) 0))) (NOT (EQUAL (EXP 2 I) 0))), which simplifies, applying TIMES-1 and PLUS-EQUAL-0, and unfolding ZEROP, EXP, SUB1, NUMBERP, EQUAL, and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EXP-2-NEVER-0 (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 DIFFERENCE-2 (REWRITE) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))) This formula simplifies, using linear arithmetic, to three new conjectures: Case 3. (IMPLIES (LESSP X 2) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))). Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X) and Z by (ADD1 V) to eliminate (SUB1 Z). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces the following four new conjectures: Case 3.4. (IMPLIES (AND (EQUAL X 0) (LESSP X 2)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))). However this further simplifies, opening up the functions LESSP, DIFFERENCE, SUB1, and EQUAL, to: T. Case 3.3. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 2)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))), which further simplifies, applying the lemma SUB1-NNUMBERP, and opening up NUMBERP, EQUAL, LESSP, DIFFERENCE, and SUB1, to: T. Case 3.2. (IMPLIES (AND (EQUAL Z 0) (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (LESSP (ADD1 Z) 2)) (EQUAL (DIFFERENCE (ADD1 Z) 2) (SUB1 Z))), which further simplifies, opening up NUMBERP, EQUAL, LESSP, DIFFERENCE, and SUB1, to: T. Case 3.1. (IMPLIES (AND (NUMBERP V) (NOT (EQUAL (ADD1 V) 0)) (NOT (EQUAL (ADD1 (ADD1 V)) 0)) (LESSP (ADD1 (ADD1 V)) 2)) (EQUAL (DIFFERENCE (ADD1 (ADD1 V)) 2) V)), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (EQUAL (SUB1 X) 0) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))), which again simplifies, opening up the definitions of DIFFERENCE, SUB1, NUMBERP, and EQUAL, to: T. Case 1. (IMPLIES (LESSP X 1) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))). Applying the lemma DIFFERENCE-ELIM, replace X by (PLUS 2 Z) to eliminate (DIFFERENCE X 2). We use the type restriction lemma noted when DIFFERENCE was introduced to restrict the new variable. We thus obtain the following three new goals: Case 1.3. (IMPLIES (AND (LESSP X 2) (LESSP X 1)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))). Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate (SUB1 X) and Z by (ADD1 V) to eliminate (SUB1 Z). We rely upon the type restriction lemma noted when SUB1 was introduced to constrain the new variable. The result is four new conjectures: Case 1.3.4. (IMPLIES (AND (EQUAL X 0) (LESSP X 2) (LESSP X 1)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))), which further simplifies, expanding the functions LESSP, DIFFERENCE, SUB1, and EQUAL, to: T. Case 1.3.3. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 2) (LESSP X 1)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))), which further simplifies, applying SUB1-NNUMBERP, and unfolding the definitions of NUMBERP, EQUAL, LESSP, DIFFERENCE, and SUB1, to: T. Case 1.3.2. (IMPLIES (AND (EQUAL Z 0) (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (LESSP (ADD1 Z) 2) (LESSP (ADD1 Z) 1)) (EQUAL (DIFFERENCE (ADD1 Z) 2) (SUB1 Z))). This further simplifies, using linear arithmetic, to: T. Case 1.3.1. (IMPLIES (AND (NUMBERP V) (NOT (EQUAL (ADD1 V) 0)) (NOT (EQUAL (ADD1 (ADD1 V)) 0)) (LESSP (ADD1 (ADD1 V)) 2) (LESSP (ADD1 (ADD1 V)) 1)) (EQUAL (DIFFERENCE (ADD1 (ADD1 V)) 2) V)), which further simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 1)) (EQUAL (DIFFERENCE X 2) (SUB1 (SUB1 X)))), which further simplifies, rewriting with the lemma SUB1-NNUMBERP, and expanding NUMBERP, EQUAL, LESSP, DIFFERENCE, and SUB1, to: T. Case 1.1. (IMPLIES (AND (NUMBERP Z) (NOT (LESSP (PLUS 2 Z) 2)) (LESSP (PLUS 2 Z) 1)) (EQUAL Z (SUB1 (SUB1 (PLUS 2 Z))))), which further simplifies, using linear arithmetic, to two new formulas: Case 1.1.2. (IMPLIES (AND (EQUAL (SUB1 (PLUS 2 Z)) 0) (NUMBERP Z) (NOT (LESSP (PLUS 2 Z) 2)) (LESSP (PLUS 2 Z) 1)) (EQUAL Z (SUB1 (SUB1 (PLUS 2 Z))))), which again simplifies, using linear arithmetic, to: T. Case 1.1.1. (IMPLIES (AND (EQUAL (PLUS 2 Z) 0) (NUMBERP Z) (NOT (LESSP (PLUS 2 Z) 2)) (LESSP (PLUS 2 Z) 1)) (EQUAL Z (SUB1 (SUB1 (PLUS 2 Z))))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-2 (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) (EQUAL (DIFFERENCE (PLUS J X) J) (FIX X))) This conjecture simplifies, opening up the function FIX, to the following two new goals: Case 2. (IMPLIES (NOT (NUMBERP X)) (EQUAL (DIFFERENCE (PLUS J X) J) 0)). But this again simplifies, applying PLUS-RIGHT-ID, to the following two new formulas: Case 2.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (NUMBERP J))) (EQUAL (DIFFERENCE 0 J) 0)). However this again simplifies, unfolding the definitions of EQUAL and DIFFERENCE, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NUMBERP J)) (EQUAL (DIFFERENCE J J) 0)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP J J) (NOT (NUMBERP X)) (NUMBERP J)) (EQUAL (DIFFERENCE J J) 0)). This again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (NUMBERP X) (EQUAL (DIFFERENCE (PLUS J X) J) X)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS J X) J) (NUMBERP X)) (EQUAL (DIFFERENCE (PLUS J X) J) X)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION (REWRITE) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))) This simplifies, using linear arithmetic, to the following two new conjectures: Case 2. (IMPLIES (LESSP (PLUS A X) (PLUS A Y)) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))). Appealing to the lemma DIFFERENCE-ELIM, we now replace X by (PLUS Y Z) to eliminate (DIFFERENCE X Y). We employ the type restriction lemma noted when DIFFERENCE was introduced to constrain the new variable. This generates three new conjectures: Case 2.3. (IMPLIES (AND (LESSP X Y) (LESSP (PLUS A X) (PLUS A Y))) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE 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 (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y)). We named this *1. We will try to prove it by induction. 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 A) (p A X Y)) (IMPLIES (AND (NOT (ZEROP A)) (p (SUB1 A) X Y)) (p A 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 A) 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 A) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))). This simplifies, using linear arithmetic, to the following two new goals: Case 2.2. (IMPLIES (AND (LESSP (PLUS A X) (PLUS A Y)) (ZEROP A)) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))). But this again simplifies, applying PLUS-RIGHT-ID, and opening up the functions PLUS, ZEROP, NUMBERP, DIFFERENCE, and EQUAL, to: T. Case 2.1. (IMPLIES (AND (LESSP X Y) (ZEROP A)) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))). But this again simplifies, expanding the definitions of ZEROP, EQUAL, and PLUS, to six new formulas: Case 2.1.6. (IMPLIES (AND (LESSP X Y) (EQUAL A 0) (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 0) (DIFFERENCE X Y))), which again simplifies, expanding LESSP, to: T. Case 2.1.5. (IMPLIES (AND (LESSP X Y) (EQUAL A 0) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X 0) (DIFFERENCE X Y))), which again simplifies, unfolding the definition of LESSP, to: T. Case 2.1.4. (IMPLIES (AND (LESSP X Y) (EQUAL A 0) (NUMBERP Y) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 Y) (DIFFERENCE X Y))), which again simplifies, expanding LESSP, EQUAL, and DIFFERENCE, to: T. Case 2.1.3. (IMPLIES (AND (LESSP X Y) (NOT (NUMBERP A)) (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 0) (DIFFERENCE X Y))), which again simplifies, unfolding the definition of LESSP, to: T. Case 2.1.2. (IMPLIES (AND (LESSP X Y) (NOT (NUMBERP A)) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL (DIFFERENCE X 0) (DIFFERENCE X Y))), which again simplifies, opening up the definition of LESSP, to: T. Case 2.1.1. (IMPLIES (AND (LESSP X Y) (NOT (NUMBERP A)) (NUMBERP Y) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 Y) (DIFFERENCE X Y))), which again simplifies, expanding LESSP, EQUAL, and DIFFERENCE, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL (DIFFERENCE (PLUS (SUB1 A) X) (PLUS (SUB1 A) Y)) (DIFFERENCE X Y))) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))), which simplifies, using linear arithmetic, to two new goals: Case 1.2. (IMPLIES (AND (LESSP (PLUS A X) (PLUS A Y)) (NOT (ZEROP A)) (EQUAL (DIFFERENCE (PLUS (SUB1 A) X) (PLUS (SUB1 A) Y)) (DIFFERENCE X Y))) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))), which again simplifies, applying SUB1-ADD1, and expanding the definitions of PLUS, ZEROP, and DIFFERENCE, to: T. Case 1.1. (IMPLIES (AND (LESSP X Y) (NOT (ZEROP A)) (EQUAL (DIFFERENCE (PLUS (SUB1 A) X) (PLUS (SUB1 A) Y)) (DIFFERENCE X Y))) (EQUAL (DIFFERENCE (PLUS A X) (PLUS A Y)) (DIFFERENCE X Y))). However this again simplifies, applying SUB1-ADD1, and expanding the functions ZEROP, PLUS, and DIFFERENCE, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELLATION (PROVE-LEMMA PATHOLOGICAL-DIFFERENCE (REWRITE) (IMPLIES (LESSP X Y) (EQUAL (DIFFERENCE X Y) 0))) Give the conjecture the name *1. We will try to prove it by induction. There are four plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL Y 0) (NOT (NUMBERP Y))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (OR (EQUAL X 0) (NOT (NUMBERP X)))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (p (SUB1 X) (SUB1 Y))) (p X Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for Y. The above induction scheme generates four new goals: Case 4. (IMPLIES (AND (OR (EQUAL Y 0) (NOT (NUMBERP Y))) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, expanding NOT, OR, EQUAL, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (OR (EQUAL X 0) (NOT (NUMBERP X))) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, opening up the functions NOT, OR, EQUAL, LESSP, and DIFFERENCE, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (LESSP (SUB1 X) (SUB1 Y))) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (LESSP (SUB1 X) (SUB1 Y))) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)). But this again simplifies, unfolding the functions SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, using linear arithmetic, to two new goals: Case 1.2. (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y)) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, expanding NOT, OR, LESSP, DIFFERENCE, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (LESSP X Y)) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PATHOLOGICAL-DIFFERENCE (PROVE-LEMMA DIFFERENCE-CROCK1 (REWRITE) (EQUAL (DIFFERENCE (PLUS X (DIFFERENCE Y Z)) Y) (IF (LESSP Y Z) (DIFFERENCE X Y) (DIFFERENCE X Z)))) This formula simplifies, trivially, to two new formulas: Case 2. (IMPLIES (NOT (LESSP Y Z)) (EQUAL (DIFFERENCE (PLUS X (DIFFERENCE Y Z)) Y) (DIFFERENCE X Z))), which again simplifies, using linear arithmetic, to two new goals: Case 2.2. (IMPLIES (AND (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (NOT (LESSP Y Z))) (EQUAL (DIFFERENCE (PLUS X (DIFFERENCE Y Z)) Y) (DIFFERENCE X Z))), which again simplifies, using linear arithmetic, rewriting with PATHOLOGICAL-DIFFERENCE, and opening up the definition of EQUAL, to: T. Case 2.1. (IMPLIES (AND (LESSP X Z) (NOT (LESSP Y Z))) (EQUAL (DIFFERENCE (PLUS X (DIFFERENCE Y Z)) Y) (DIFFERENCE X Z))). But this again simplifies, using linear arithmetic, rewriting with the lemma PATHOLOGICAL-DIFFERENCE, and expanding EQUAL, to: T. Case 1. (IMPLIES (LESSP Y Z) (EQUAL (DIFFERENCE (PLUS X (DIFFERENCE Y Z)) Y) (DIFFERENCE X Y))), which again simplifies, applying PATHOLOGICAL-DIFFERENCE and COMMUTATIVITY-OF-PLUS, and unfolding EQUAL and PLUS, to the new formula: (IMPLIES (AND (LESSP Y Z) (NOT (NUMBERP X))) (EQUAL (DIFFERENCE 0 Y) (DIFFERENCE X Y))), which again simplifies, expanding the functions EQUAL and DIFFERENCE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-CROCK1 (PROVE-LEMMA DIFFERENCE-DIFFERENCE (REWRITE) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z)))) This simplifies, using linear arithmetic, to the following three new conjectures: Case 3. (IMPLIES (LESSP (DIFFERENCE X Y) Z) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z)))). But this again simplifies, using linear arithmetic, applying PATHOLOGICAL-DIFFERENCE, and opening up the function EQUAL, to: T. Case 2. (IMPLIES (LESSP X Y) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z)))). But this again simplifies, using linear arithmetic, applying the lemma PATHOLOGICAL-DIFFERENCE, and expanding EQUAL and DIFFERENCE, to: T. Case 1. (IMPLIES (LESSP X (PLUS Y Z)) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z)))), which again simplifies, using linear arithmetic, applying the lemma PATHOLOGICAL-DIFFERENCE, and opening up the function EQUAL, to: (IMPLIES (AND (LESSP X (PLUS Y Z)) (LESSP X Y)) (EQUAL (DIFFERENCE (DIFFERENCE X Y) Z) (DIFFERENCE X (PLUS Y Z)))). But this again simplifies, rewriting with the lemma PATHOLOGICAL-DIFFERENCE, and expanding the functions EQUAL and DIFFERENCE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-DIFFERENCE (PROVE-LEMMA LESSP-DIFFERENCE (REWRITE) (EQUAL (LESSP (DIFFERENCE X Y) X) (AND (NOT (ZEROP X)) (NOT (ZEROP Y))))) This formula simplifies, expanding ZEROP, NOT, and AND, to five new conjectures: Case 5. (IMPLIES (EQUAL Y 0) (EQUAL (LESSP (DIFFERENCE X Y) X) F)), which again simplifies, expanding the definitions of EQUAL and DIFFERENCE, to three new goals: Case 5.3. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP X X))), which again simplifies, using linear arithmetic, to: T. Case 5.2. (IMPLIES (EQUAL X 0) (NOT (LESSP 0 X))), which again simplifies, using linear arithmetic, to: T. Case 5.1. (IMPLIES (NOT (NUMBERP X)) (NOT (LESSP 0 X))), which again simplifies, expanding the definition of LESSP, to: T. Case 4. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (LESSP (DIFFERENCE X Y) X) F)), which again simplifies, expanding the function DIFFERENCE, to three new conjectures: Case 4.3. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP X X))), which again simplifies, using linear arithmetic, to: T. Case 4.2. (IMPLIES (AND (NOT (NUMBERP Y)) (EQUAL X 0)) (NOT (LESSP 0 X))), which again simplifies, using linear arithmetic, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (NOT (LESSP 0 X))), which again simplifies, unfolding the function LESSP, to: T. Case 3. (IMPLIES (NOT (NUMBERP X)) (EQUAL (LESSP (DIFFERENCE X Y) X) F)), which again simplifies, unfolding the functions DIFFERENCE, LESSP, and EQUAL, to: T. Case 2. (IMPLIES (EQUAL X 0) (EQUAL (LESSP (DIFFERENCE X Y) X) F)), which again simplifies, expanding EQUAL, DIFFERENCE, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (LESSP (DIFFERENCE X Y) X) T)), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (DIFFERENCE X Y) X)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X Y) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (DIFFERENCE X Y) X)). But this again simplifies, applying the lemma PATHOLOGICAL-DIFFERENCE, and opening up the definitions of EQUAL and LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-DIFFERENCE (PROVE-LEMMA DIFFERENCE-ADD1 NIL (EQUAL (DIFFERENCE (ADD1 X) Y) (IF (LESSP Y (ADD1 X)) (ADD1 (DIFFERENCE X Y)) 0))) This simplifies, appealing to the lemma SUB1-ADD1, and opening up the functions DIFFERENCE and LESSP, to six new formulas: Case 6. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (ADD1 X) (ADD1 (DIFFERENCE X Y)))), which again simplifies, applying the lemma ADD1-EQUAL, and opening up DIFFERENCE, to: T. Case 5. (IMPLIES (EQUAL Y 0) (EQUAL (ADD1 X) (ADD1 (DIFFERENCE X Y)))), which again simplifies, using linear arithmetic, to: (IMPLIES (LESSP X 0) (EQUAL (ADD1 X) (ADD1 (DIFFERENCE X 0)))). This again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X) (NOT (LESSP (SUB1 Y) X))) (EQUAL (DIFFERENCE X (SUB1 Y)) 0)). Applying the lemma DIFFERENCE-ELIM, replace X by (PLUS (SUB1 Y) Z) to eliminate (DIFFERENCE X (SUB1 Y)). We rely upon the type restriction lemma noted when DIFFERENCE was introduced to restrict the new variable. We would thus like to prove the following two new formulas: Case 4.2. (IMPLIES (AND (LESSP X (SUB1 Y)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X) (NOT (LESSP (SUB1 Y) X))) (EQUAL (DIFFERENCE X (SUB1 Y)) 0)). But this further simplifies, rewriting with the lemma PATHOLOGICAL-DIFFERENCE, and opening up the definition of EQUAL, to: T. Case 4.1. (IMPLIES (AND (NUMBERP Z) (NOT (LESSP (PLUS (SUB1 Y) Z) (SUB1 Y))) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (LESSP (SUB1 Y) (PLUS (SUB1 Y) Z)))) (EQUAL Z 0)), which further simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X) (LESSP (SUB1 Y) X)) (EQUAL (DIFFERENCE X (SUB1 Y)) (ADD1 (DIFFERENCE X Y)))), which again simplifies, using linear arithmetic, to two new conjectures: Case 3.2. (IMPLIES (AND (LESSP X (SUB1 Y)) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X) (LESSP (SUB1 Y) X)) (EQUAL (DIFFERENCE X (SUB1 Y)) (ADD1 (DIFFERENCE X Y)))), which again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (LESSP X Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP X) (LESSP (SUB1 Y) X)) (EQUAL (DIFFERENCE X (SUB1 Y)) (ADD1 (DIFFERENCE X Y)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (NUMBERP X)) (NOT (LESSP (SUB1 Y) 0))) (EQUAL (DIFFERENCE 0 (SUB1 Y)) 0)), which again simplifies, opening up the functions EQUAL, LESSP, and DIFFERENCE, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (NUMBERP X)) (LESSP (SUB1 Y) 0)) (EQUAL (DIFFERENCE 0 (SUB1 Y)) (ADD1 (DIFFERENCE X Y)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ADD1 (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-BY-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-BY-1 (PROVE-LEMMA REMAINDER-BY-NONNUMBER (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-BY-NONNUMBER (PROVE-LEMMA LESSP-REMAINDER (REWRITE GENERALIZE) (EQUAL (LESSP (REMAINDER X Y) Y) (NOT (ZEROP Y)))) This conjecture simplifies, expanding ZEROP and NOT, to the following three new goals: Case 3. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (LESSP (REMAINDER X Y) Y) F)). However this again simplifies, applying REMAINDER-BY-NONNUMBER, and expanding the definitions of LESSP and EQUAL, to: T. Case 2. (IMPLIES (EQUAL Y 0) (EQUAL (LESSP (REMAINDER X Y) Y) F)). This again simplifies, expanding the definitions of EQUAL, REMAINDER, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (LESSP (REMAINDER X Y) Y) T)), which again simplifies, trivially, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)), 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 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 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 three new formulas: Case 3. (IMPLIES (AND (ZEROP Y) (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)). This simplifies, opening up ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y) (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)). This simplifies, opening up the definitions of ZEROP and REMAINDER, to: (IMPLIES (AND (LESSP X Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (NUMBERP X))) (LESSP 0 Y)), which 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 (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)), which simplifies, unfolding the functions ZEROP and REMAINDER, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-REMAINDER (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 REMAINDER-X-X (REWRITE) (EQUAL (REMAINDER X X) 0)) This conjecture simplifies, rewriting with DIFFERENCE-X-X, 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-PLUS (REWRITE) (EQUAL (REMAINDER (PLUS J X) J) (REMAINDER X J))) This formula simplifies, applying the lemma DIFFERENCE-PLUS, and expanding the definitions of REMAINDER, EQUAL, and PLUS, to six new conjectures: Case 6. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (PLUS J X) J)) (NOT (NUMBERP X))) (EQUAL (REMAINDER 0 J) (REMAINDER X J))), which again simplifies, applying PLUS-RIGHT-ID, and opening up NUMBERP, LESSP, EQUAL, and REMAINDER, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (PLUS J X) J)) (EQUAL (PLUS J X) (REMAINDER X J))). But this again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (EQUAL J 0) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER X J))), which again simplifies, opening up the definitions of EQUAL and REMAINDER, to: T. Case 3. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER X J))), which again simplifies, appealing to the lemma REMAINDER-BY-NONNUMBER, and opening up EQUAL, to: T. Case 2. (IMPLIES (AND (EQUAL J 0) (NUMBERP X)) (EQUAL X (REMAINDER X J))), which again simplifies, expanding the definitions of EQUAL and REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP J)) (NUMBERP X)) (EQUAL X (REMAINDER X J))), which again simplifies, rewriting with REMAINDER-BY-NONNUMBER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-PLUS (PROVE-LEMMA REMAINDER-PLUS-TIMES (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-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following four new conjectures: Case 4. (IMPLIES (NOT (NUMBERP X)) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))). But this simplifies, opening up the definitions of PLUS, LESSP, and REMAINDER, to the conjecture: (IMPLIES (NOT (NUMBERP X)) (EQUAL (REMAINDER (TIMES I J) J) 0)), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J)), which we named *1 above. We will appeal to induction. There are three plausible 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 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 two new goals: Case 2. (IMPLIES (ZEROP I) (EQUAL (REMAINDER (PLUS X (TIMES I J)) J) (REMAINDER X J))). This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding the functions ZEROP, EQUAL, TIMES, and PLUS, to two new conjectures: Case 2.2. (IMPLIES (AND (EQUAL I 0) (NOT (NUMBERP X))) (EQUAL (REMAINDER 0 J) (REMAINDER X J))), which again simplifies, expanding 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, expanding 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 REMAINDER-PLUS, and expanding ZEROP and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.2 ] REMAINDER-PLUS-TIMES (PROVE-LEMMA REMAINDER-PLUS-TIMES-COMMUTED (REWRITE) (EQUAL (REMAINDER (PLUS X (TIMES J I)) J) (REMAINDER X J))) This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and REMAINDER-PLUS-TIMES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-PLUS-TIMES-COMMUTED (PROVE-LEMMA REMAINDER-TIMES (REWRITE) (EQUAL (REMAINDER (TIMES J I) J) 0) ((USE (REMAINDER-PLUS-TIMES (X 0))) (DISABLE REMAINDER-PLUS-TIMES))) This conjecture simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, and unfolding the functions EQUAL, PLUS, LESSP, NUMBERP, and REMAINDER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-TIMES (PROVE-LEMMA REMAINDER-ADD1-TIMES (REWRITE) (EQUAL (REMAINDER (ADD1 (TIMES J I)) J) (REMAINDER 1 J)) ((USE (REMAINDER-PLUS-TIMES (X 1))) (DISABLE REMAINDER-PLUS-TIMES))) This formula can be simplified, using the abbreviation PLUS-1, to: (IMPLIES (EQUAL (REMAINDER (ADD1 (TIMES I J)) J) (REMAINDER 1 J)) (EQUAL (REMAINDER (ADD1 (TIMES J I)) J) (REMAINDER 1 J))), which simplifies, applying COMMUTATIVITY-OF-TIMES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-ADD1-TIMES (PROVE-LEMMA QUOTIENT-PLUS-TIMES (REWRITE) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT X J))))) This simplifies, expanding ZEROP, to three new goals: Case 3. (IMPLIES (NOT (NUMBERP J)) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) 0)), which again simplifies, applying the lemmas TIMES-ZERO2 and COMMUTATIVITY-OF-PLUS, and opening up the functions EQUAL, PLUS, and QUOTIENT, to: T. Case 2. (IMPLIES (EQUAL J 0) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) 0)), which again simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS, and unfolding the definitions of EQUAL, TIMES, PLUS, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J)) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) (PLUS I (QUOTIENT X J)))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES J Z)) to eliminate (QUOTIENT X J) and (REMAINDER X J). We employ LESSP-REMAINDER, 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 two new goals: Case 1.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL J 0)) (NUMBERP J)) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) (PLUS I (QUOTIENT X J)))). This further simplifies, applying COMMUTATIVITY-OF-PLUS, and expanding the functions PLUS, LESSP, QUOTIENT, and EQUAL, to the following two new formulas: Case 1.2.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL J 0)) (NUMBERP J) (NOT (NUMBERP I))) (EQUAL (QUOTIENT (TIMES I J) J) 0)). But this again simplifies, unfolding the definitions of TIMES, LESSP, EQUAL, and QUOTIENT, to: T. Case 1.2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (EQUAL J 0)) (NUMBERP J) (NUMBERP I)) (EQUAL (QUOTIENT (TIMES I J) J) I)), 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 (TIMES I J)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT X J)))). We named this *1. We will try to prove it by induction. Four inductions are suggested by terms in the conjecture. They merge into three likely candidate 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 can be used to 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 the following two new conjectures: Case 2. (IMPLIES (ZEROP I) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT X J))))). This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and opening up the definitions of ZEROP, EQUAL, TIMES, and PLUS, to ten new conjectures: Case 2.10. (IMPLIES (AND (EQUAL I 0) (NOT (NUMBERP J)) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) 0)), which again simplifies, opening up QUOTIENT and EQUAL, to: T. Case 2.9. (IMPLIES (AND (EQUAL I 0) (EQUAL J 0) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) 0)), which again simplifies, unfolding the definitions of QUOTIENT and EQUAL, to: T. Case 2.8. (IMPLIES (AND (EQUAL I 0) (NOT (NUMBERP J)) (NUMBERP X)) (EQUAL (QUOTIENT X J) 0)), which again simplifies, opening up QUOTIENT and EQUAL, to: T. Case 2.7. (IMPLIES (AND (EQUAL I 0) (EQUAL J 0) (NUMBERP X)) (EQUAL (QUOTIENT X J) 0)), which again simplifies, unfolding the functions EQUAL and QUOTIENT, to: T. Case 2.6. (IMPLIES (AND (EQUAL I 0) (NOT (EQUAL J 0)) (NUMBERP J) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) (QUOTIENT X J))), which again simplifies, opening up LESSP, EQUAL, and QUOTIENT, to: T. Case 2.5. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (NUMBERP J)) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) 0)), which again simplifies, expanding the definitions of QUOTIENT and EQUAL, to: T. Case 2.4. (IMPLIES (AND (NOT (NUMBERP I)) (EQUAL J 0) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) 0)), which again simplifies, opening up the definitions of QUOTIENT and EQUAL, to: T. Case 2.3. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (NUMBERP J)) (NUMBERP X)) (EQUAL (QUOTIENT X J) 0)), which again simplifies, expanding QUOTIENT and EQUAL, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP I)) (EQUAL J 0) (NUMBERP X)) (EQUAL (QUOTIENT X J) 0)), which again simplifies, expanding EQUAL and QUOTIENT, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (EQUAL J 0)) (NUMBERP J) (NOT (NUMBERP X))) (EQUAL (QUOTIENT 0 J) (QUOTIENT X J))), which again simplifies, expanding LESSP, EQUAL, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (EQUAL (QUOTIENT (PLUS X (TIMES (SUB1 I) J)) J) (IF (ZEROP J) 0 (PLUS (SUB1 I) (QUOTIENT X J))))) (EQUAL (QUOTIENT (PLUS X (TIMES I J)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT X J))))), which simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-PLUS, COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-PLUS, and DIFFERENCE-PLUS, and opening up the functions ZEROP, EQUAL, PLUS, QUOTIENT, and TIMES, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0)) (NUMBERP J) (EQUAL (QUOTIENT (PLUS X (TIMES (SUB1 I) J)) J) (PLUS (SUB1 I) (QUOTIENT X J))) (LESSP (PLUS J X (TIMES (SUB1 I) J)) J)) (EQUAL 0 (ADD1 (PLUS (SUB1 I) (QUOTIENT X J))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] QUOTIENT-PLUS-TIMES (PROVE-LEMMA QUOTIENT-PLUS-TIMES-COMMUTED (REWRITE) (EQUAL (QUOTIENT (PLUS X (TIMES J I)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT X J))))) This simplifies, applying COMMUTATIVITY-OF-TIMES and QUOTIENT-PLUS-TIMES, and unfolding ZEROP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-TIMES-COMMUTED (PROVE-LEMMA QUOTIENT-TIMES (REWRITE) (EQUAL (QUOTIENT (TIMES J I) J) (IF (ZEROP J) 0 (FIX I))) ((USE (QUOTIENT-PLUS-TIMES (X 0))) (DISABLE QUOTIENT-PLUS-TIMES))) This conjecture simplifies, rewriting with COMMUTATIVITY-OF-PLUS, TIMES-ZERO2, and COMMUTATIVITY-OF-TIMES, and expanding the functions EQUAL, PLUS, ZEROP, LESSP, QUOTIENT, TIMES, and FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-TIMES (PROVE-LEMMA QUOTIENT-ADD1-TIMES (REWRITE) (EQUAL (QUOTIENT (ADD1 (TIMES J I)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT 1 J)))) ((USE (QUOTIENT-PLUS-TIMES (X 1))) (DISABLE QUOTIENT-PLUS-TIMES))) This formula can be simplified, using the abbreviation PLUS-1, to the new conjecture: (IMPLIES (EQUAL (QUOTIENT (ADD1 (TIMES I J)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT 1 J)))) (EQUAL (QUOTIENT (ADD1 (TIMES J I)) J) (IF (ZEROP J) 0 (PLUS I (QUOTIENT 1 J))))), which simplifies, applying the lemmas TIMES-ZERO2 and COMMUTATIVITY-OF-TIMES, and unfolding the functions ZEROP, ADD1, QUOTIENT, EQUAL, and TIMES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-ADD1-TIMES (DISABLE TIMES) [ 0.0 0.0 0.0 ] TIMES-OFF (PROVE-LEMMA TIMES-DISTRIBUTES-OVER-REMAINDER (REWRITE) (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z))) ((EXPAND (REMAINDER (TIMES V X) (TIMES X Z))))) . Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by (PLUS V (TIMES Z W)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z). We use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. The result is four new goals: Case 4. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z)))), which simplifies, appealing to the lemmas TIMES-ZERO2, EQUAL-TIMES-0, and COMMUTATIVITY-OF-TIMES, and unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Case 3. (IMPLIES (EQUAL Z 0) (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z)))), which simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES and EQUAL-TIMES-0, and expanding the functions EQUAL and REMAINDER, to the goal: (IMPLIES (NOT (NUMBERP Y)) (EQUAL (TIMES X Y) (TIMES X 0))). But this again simplifies, applying TIMES-ZERO2, COMMUTATIVITY-OF-TIMES, and EQUAL-TIMES-0, and unfolding EQUAL, to: T. Case 2. (IMPLIES (NOT (NUMBERP Z)) (EQUAL (REMAINDER (TIMES X Y) (TIMES X Z)) (TIMES X (REMAINDER Y Z)))). But this simplifies, appealing to the lemmas TIMES-ZERO2 and REMAINDER-BY-NONNUMBER, and unfolding the functions EQUAL and REMAINDER, to the goal: (IMPLIES (AND (NOT (NUMBERP Z)) (NOT (NUMBERP Y))) (EQUAL (TIMES X Y) (TIMES X 0))). This again simplifies, applying the lemmas TIMES-ZERO2, COMMUTATIVITY-OF-TIMES, and EQUAL-TIMES-0, and opening up 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 (REMAINDER (TIMES X (PLUS V (TIMES Z W))) (TIMES X Z)) (TIMES X V))), which simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, EQUAL-TIMES-0, LESSP-TIMES, and REMAINDER-PLUS-TIMES, and expanding the definitions of ZEROP, NOT, and REMAINDER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-DISTRIBUTES-OVER-REMAINDER (PROVE-LEMMA REMAINDER-OF-1 (REWRITE) (EQUAL (REMAINDER 1 X) (IF (EQUAL X 1) 0 1)) ((EXPAND (REMAINDER 1 X)))) This simplifies, unfolding the functions REMAINDER and NUMBERP, to the following five new formulas: Case 5. (IMPLIES (EQUAL X 1) (EQUAL (REMAINDER (DIFFERENCE 1 X) X) 0)). But this again simplifies, opening up the functions DIFFERENCE, REMAINDER, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL X 1)) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (LESSP 1 X))) (EQUAL (REMAINDER (DIFFERENCE 1 X) X) 1)), 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, obviously, 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 (PROVE-LEMMA REMAINDER-CROCK1 (REWRITE) (IMPLIES (AND (NUMBERP X) (LESSP X Z) (NUMBERP V) (NUMBERP Z) (NOT (EQUAL Z 0))) (EQUAL (REMAINDER (ADD1 (PLUS (TIMES 2 X) (TIMES 2 V Z))) (TIMES 2 Z)) (ADD1 (TIMES 2 X)))) ((USE (REMAINDER-PLUS-TIMES (X (ADD1 (TIMES 2 X))) (I V) (J (TIMES 2 Z)))) (DISABLE REMAINDER-PLUS-TIMES))) This formula simplifies, using linear arithmetic, applying COMMUTATIVITY2-OF-TIMES, SUB1-ADD1, PATHOLOGICAL-DIFFERENCE, and EQUAL-TIMES-0, and unfolding the functions PLUS, LESSP, NUMBERP, EQUAL, and REMAINDER, to the formula: (IMPLIES (AND (NOT (LESSP (TIMES 2 X) (SUB1 (TIMES 2 Z)))) (EQUAL (REMAINDER (ADD1 (PLUS (TIMES 2 X) (TIMES 2 V Z))) (TIMES 2 Z)) 0) (NUMBERP X) (LESSP X Z) (NUMBERP V) (NUMBERP Z)) (EQUAL Z 0)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-CROCK1 (PROVE-LEMMA TIMES-2-DISTRIBUTES-OVER-REMAINDER-ADD1 (REWRITE) (EQUAL (REMAINDER (ADD1 (TIMES 2 Y)) (TIMES 2 Z)) (ADD1 (TIMES 2 (REMAINDER Y Z))))) . Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by (PLUS X (TIMES Z V)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z). We use LESSP-REMAINDER, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. This generates four new goals: Case 4. (IMPLIES (NOT (NUMBERP Y)) (EQUAL (REMAINDER (ADD1 (TIMES 2 Y)) (TIMES 2 Z)) (ADD1 (TIMES 2 (REMAINDER Y Z))))), which simplifies, rewriting with the lemmas TIMES-ZERO2, TIMES-2-NOT-1, and REMAINDER-OF-1, and unfolding the functions ADD1, LESSP, REMAINDER, TIMES, and EQUAL, to: T. Case 3. (IMPLIES (EQUAL Z 0) (EQUAL (REMAINDER (ADD1 (TIMES 2 Y)) (TIMES 2 Z)) (ADD1 (TIMES 2 (REMAINDER Y Z))))), which simplifies, appealing to the lemma ADD1-EQUAL, and unfolding the definitions of TIMES, EQUAL, and REMAINDER, to the formula: (IMPLIES (NOT (NUMBERP Y)) (EQUAL (TIMES 2 Y) (TIMES 2 0))). However this again simplifies, applying the lemma TIMES-ZERO2, and unfolding the functions TIMES and EQUAL, to: T. Case 2. (IMPLIES (NOT (NUMBERP Z)) (EQUAL (REMAINDER (ADD1 (TIMES 2 Y)) (TIMES 2 Z)) (ADD1 (TIMES 2 (REMAINDER Y Z))))), which simplifies, rewriting with TIMES-ZERO2, REMAINDER-BY-NONNUMBER, and ADD1-EQUAL, and expanding the functions EQUAL and REMAINDER, to: (IMPLIES (AND (NOT (NUMBERP Z)) (NOT (NUMBERP Y))) (EQUAL (TIMES 2 Y) (TIMES 2 0))), which again simplifies, appealing to the lemma TIMES-ZERO2, and expanding the functions TIMES and EQUAL, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X Z) (NOT (ZEROP Z))) (NUMBERP V) (NUMBERP Z) (NOT (EQUAL Z 0))) (EQUAL (REMAINDER (ADD1 (TIMES 2 (PLUS X (TIMES Z V)))) (TIMES 2 Z)) (ADD1 (TIMES 2 X)))), which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and REMAINDER-CROCK1, and unfolding ZEROP and NOT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-2-DISTRIBUTES-OVER-REMAINDER-ADD1 (PROVE-LEMMA REMAINDER-CROCK2 (REWRITE) (IMPLIES (LESSP V (EXP 2 (SUB1 SIZE))) (EQUAL (REMAINDER (PLUS (TIMES 2 V) (TIMES 2 W (EXP 2 (SUB1 SIZE)))) (TIMES 2 (EXP 2 (SUB1 SIZE)))) (TIMES 2 V))) ((USE (REMAINDER-PLUS-TIMES (X (TIMES 2 V)) (I W) (J (TIMES 2 (EXP 2 (SUB1 SIZE)))))) (DISABLE REMAINDER-PLUS-TIMES))) This conjecture can be simplified, using the abbreviations IMPLIES and TIMES-DISTRIBUTES-OVER-REMAINDER, to the conjecture: (IMPLIES (AND (EQUAL (REMAINDER (PLUS (TIMES 2 V) (TIMES W 2 (EXP 2 (SUB1 SIZE)))) (TIMES 2 (EXP 2 (SUB1 SIZE)))) (TIMES 2 (REMAINDER V (EXP 2 (SUB1 SIZE))))) (LESSP V (EXP 2 (SUB1 SIZE)))) (EQUAL (REMAINDER (PLUS (TIMES 2 V) (TIMES 2 W (EXP 2 (SUB1 SIZE)))) (TIMES 2 (EXP 2 (SUB1 SIZE)))) (TIMES 2 V))). This simplifies, appealing to the lemmas COMMUTATIVITY2-OF-TIMES, TIMES-ZERO2, TIMES-DISTRIBUTES-OVER-REMAINDER, and EQUAL-TIMES-0, and expanding the definitions of REMAINDER, LESSP, EQUAL, PLUS, and NUMBERP, to: (IMPLIES (AND (NOT (NUMBERP V)) (EQUAL (REMAINDER (PLUS (TIMES 2 V) (TIMES 2 W (EXP 2 (SUB1 SIZE)))) (TIMES 2 (EXP 2 (SUB1 SIZE)))) (TIMES 2 0)) (NOT (EQUAL (EXP 2 (SUB1 SIZE)) 0))) (EQUAL (REMAINDER (TIMES W (EXP 2 (SUB1 SIZE))) (EXP 2 (SUB1 SIZE))) 0)), which again simplifies, rewriting with TIMES-ZERO2, TIMES-DISTRIBUTES-OVER-REMAINDER, and EQUAL-TIMES-0, and expanding EQUAL, PLUS, TIMES, and NUMBERP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-CROCK2 (PROVE-LEMMA REMAINDER-CROCK3 (REWRITE) (EQUAL (REMAINDER (PLUS X (DIFFERENCE Y Z)) Y) (IF (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (PLUS X (DIFFERENCE Y Z)) (IF (LESSP Y Z) (REMAINDER X Y) (REMAINDER (DIFFERENCE X Z) Y))))) This conjecture simplifies, rewriting with DIFFERENCE-CROCK1 and COMMUTATIVITY-OF-PLUS, and opening up REMAINDER, EQUAL, DIFFERENCE, and PLUS, to 13 new formulas: Case 13.(IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (LESSP Y Z) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL (REMAINDER (DIFFERENCE X Y) Y) (REMAINDER X Y))), which again simplifies, using linear arithmetic, rewriting with PATHOLOGICAL-DIFFERENCE and COMMUTATIVITY-OF-PLUS, and expanding the functions EQUAL, PLUS, NUMBERP, LESSP, and REMAINDER, to: T. Case 12.(IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (LESSP Y Z) (EQUAL Y 0) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER X Y))). This again simplifies, rewriting with PATHOLOGICAL-DIFFERENCE, PLUS-RIGHT-ID, and COMMUTATIVITY-OF-PLUS, and unfolding NUMBERP, LESSP, EQUAL, and REMAINDER, to: T. Case 11.(IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (LESSP Y Z) (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER X Y))). This again simplifies, rewriting with PATHOLOGICAL-DIFFERENCE, PLUS-RIGHT-ID, COMMUTATIVITY-OF-PLUS, and REMAINDER-BY-NONNUMBER, and unfolding the definitions of NUMBERP, LESSP, and EQUAL, to: T. Case 10.(IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (LESSP Y Z) (EQUAL Y 0) (NUMBERP X)) (EQUAL X (REMAINDER X Y))). This again simplifies, applying PATHOLOGICAL-DIFFERENCE and COMMUTATIVITY-OF-PLUS, and opening up the functions EQUAL, PLUS, LESSP, and REMAINDER, to: T. Case 9. (IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (LESSP Y Z) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL X (REMAINDER X Y))). However this again simplifies, applying PATHOLOGICAL-DIFFERENCE, COMMUTATIVITY-OF-PLUS, and REMAINDER-BY-NONNUMBER, and unfolding EQUAL, PLUS, and LESSP, to: T. Case 8. (IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (NOT (LESSP Y Z)) (EQUAL Y 0) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER (DIFFERENCE X Z) Y))). This again simplifies, applying PLUS-RIGHT-ID and COMMUTATIVITY-OF-PLUS, and expanding the functions EQUAL, DIFFERENCE, NUMBERP, LESSP, and REMAINDER, to: T. Case 7. (IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (NOT (LESSP Y Z)) (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL 0 (REMAINDER (DIFFERENCE X Z) Y))). But this again simplifies, rewriting with the lemmas PLUS-RIGHT-ID, COMMUTATIVITY-OF-PLUS, and REMAINDER-BY-NONNUMBER, and opening up the definitions of DIFFERENCE, NUMBERP, LESSP, and EQUAL, to: T. Case 6. (IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (NOT (LESSP Y Z)) (EQUAL Y 0) (NUMBERP X)) (EQUAL X (REMAINDER (DIFFERENCE X Z) Y))), which again simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and opening up the definitions of EQUAL, DIFFERENCE, PLUS, LESSP, and REMAINDER, to: T. Case 5. (IMPLIES (AND (NOT (LESSP (PLUS X (DIFFERENCE Y Z)) Y)) (NOT (LESSP Y Z)) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL X (REMAINDER (DIFFERENCE X Z) Y))). However this again simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and REMAINDER-BY-NONNUMBER, and opening up DIFFERENCE, EQUAL, PLUS, and LESSP, to: T. Case 4. (IMPLIES (AND (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (EQUAL Y 0) (NOT (NUMBERP X))) (EQUAL 0 (PLUS X (DIFFERENCE Y Z)))), which again simplifies, rewriting with PLUS-RIGHT-ID and COMMUTATIVITY-OF-PLUS, and opening up the definitions of EQUAL, DIFFERENCE, NUMBERP, and LESSP, to: T. Case 3. (IMPLIES (AND (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (NOT (NUMBERP Y)) (NOT (NUMBERP X))) (EQUAL 0 (PLUS X (DIFFERENCE Y Z)))). However this again simplifies, applying PLUS-RIGHT-ID and COMMUTATIVITY-OF-PLUS, and expanding the definitions of DIFFERENCE, NUMBERP, and LESSP, to: T. Case 2. (IMPLIES (AND (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (EQUAL Y 0) (NUMBERP X)) (EQUAL X (PLUS X (DIFFERENCE Y Z)))). This again simplifies, using linear arithmetic, applying PATHOLOGICAL-DIFFERENCE and COMMUTATIVITY-OF-PLUS, and expanding the definitions of EQUAL, PLUS, and LESSP, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS X (DIFFERENCE Y Z)) Y) (NOT (NUMBERP Y)) (NUMBERP X)) (EQUAL X (PLUS X (DIFFERENCE Y Z)))). This again simplifies, appealing to the lemma COMMUTATIVITY-OF-PLUS, and opening up the definitions of DIFFERENCE, EQUAL, PLUS, and LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-CROCK3 (PROVE-LEMMA REMAINDER-OF-0 (REWRITE) (EQUAL (REMAINDER 0 X) 0)) This simplifies, unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-OF-0 (PROVE-LEMMA REMAINDER-CROCK4 (REWRITE) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (IF (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (ADD1 (PLUS X (DIFFERENCE Y Z))) (IF (LESSP Y Z) (REMAINDER (ADD1 X) Y) (IF (LESSP Z (ADD1 X)) (REMAINDER (ADD1 (DIFFERENCE X Z)) Y) 0)))) ((USE (REMAINDER-CROCK3 (X (ADD1 X))) (DIFFERENCE-ADD1 (X X) (Y Z))) (DISABLE REMAINDER-CROCK3 DIFFERENCE LESSP REMAINDER))) This conjecture simplifies, rewriting with SUB1-ADD1, COMMUTATIVITY-OF-PLUS, PATHOLOGICAL-DIFFERENCE, SUB1-TYPE-RESTRICTION, PLUS-RIGHT-ID, and REMAINDER-OF-1, and opening up the functions PLUS, EQUAL, NUMBERP, and ADD1, to the following 26 new formulas: Case 26.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (LESSP Y Z) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (ADD1 X) Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (LESSP (ADD1 X) Y)) (EQUAL (REMAINDER (ADD1 X) Y) (ADD1 X))). But this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (ADD1 X) Z) (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (LESSP Y Z) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (ADD1 X) Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (LESSP (ADD1 X) Y)) (EQUAL (REMAINDER (ADD1 X) Y) (ADD1 X))). This again simplifies, appealing to the lemma PATHOLOGICAL-DIFFERENCE, and unfolding the functions EQUAL and PLUS, to: T. Case 25.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (LESSP Y Z) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (ADD1 X) Y)) (LESSP Z (ADD1 X)) (EQUAL (DIFFERENCE (ADD1 X) Z) (ADD1 (DIFFERENCE X Z))) (LESSP (ADD1 X) Y)) (EQUAL (REMAINDER (ADD1 X) Y) (ADD1 X))), which again simplifies, using linear arithmetic, to: T. Case 24.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (DIFFERENCE (ADD1 X) Z) Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (NOT (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y))) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) 0)), which again simplifies, using linear arithmetic, to two new conjectures: Case 24.2. (IMPLIES (AND (NOT (NUMBERP Z)) (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER 0 Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (NOT (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y))) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) 0)), which again simplifies, rewriting with COMMUTATIVITY-OF-PLUS and REMAINDER-OF-0, to: T. Case 24.1. (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y (PLUS 1 X)) X)) Y)) (NOT (LESSP Y (PLUS 1 X))) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y (PLUS 1 X)) X)) Y) (REMAINDER 0 Y)) (NOT (LESSP (PLUS 1 X) (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) (PLUS 1 X)) 0) (NOT (LESSP (ADD1 (PLUS X (DIFFERENCE Y (PLUS 1 X)))) Y))) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y (PLUS 1 X)))) Y) 0)). This again simplifies, applying PLUS-1, COMMUTATIVITY-OF-PLUS, REMAINDER-OF-0, and DIFFERENCE-X-X, and unfolding the function EQUAL, to: T. Case 23.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (DIFFERENCE (ADD1 X) Z) Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y)) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (ADD1 (PLUS X (DIFFERENCE Y Z))))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (ADD1 X) Z) (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER 0 Y)) (NOT (LESSP Z (ADD1 X))) (EQUAL (DIFFERENCE (ADD1 X) Z) 0) (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y)) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (ADD1 (PLUS X (DIFFERENCE Y Z))))). However this again simplifies, using linear arithmetic, to: T. Case 22.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (DIFFERENCE (ADD1 X) Z) Y)) (LESSP Z (ADD1 X)) (EQUAL (DIFFERENCE (ADD1 X) Z) (ADD1 (DIFFERENCE X Z))) (NOT (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y))) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (REMAINDER (ADD1 (DIFFERENCE X Z)) Y))), which again simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, to: T. Case 21.(IMPLIES (AND (NUMBERP X) (NOT (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y)) (NOT (LESSP Y Z)) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (REMAINDER (DIFFERENCE (ADD1 X) Z) Y)) (LESSP Z (ADD1 X)) (EQUAL (DIFFERENCE (ADD1 X) Z) (ADD1 (DIFFERENCE X Z))) (LESSP (ADD1 (PLUS X (DIFFERENCE Y Z))) Y)) (EQUAL (REMAINDER (ADD1 (PLUS X (DIFFERENCE Y Z))) Y) (ADD1 (PLUS X (DIFFERENCE Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 20.(IMPLIES (AND (NUMBERP X) (LESSP (ADD1 (PLUS (DIFFERENCE Y Z) X)) Y) (EQUAL (REMAINDER (ADD1 (PLUS (DIFFERENCE Y Z) X))