(BOOT-STRAP NQTHM) [ 0.0 0.1 0.0 ] GROUND-ZERO (DEFN RATE-PROXIMITY (W R) (AND (NOT (LESSP (TIMES 18 W) (TIMES 17 R))) (NOT (LESSP (TIMES 19 R) (TIMES 18 W))))) From the definition we can conclude that: (OR (FALSEP (RATE-PROXIMITY W R)) (TRUEP (RATE-PROXIMITY W R))) is a theorem. [ 0.0 0.0 0.0 ] RATE-PROXIMITY (PROVE-LEMMA PLUS-ADD1 (REWRITE) (EQUAL (PLUS X (ADD1 Y)) (ADD1 (PLUS X Y)))) This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-ADD1 (PROVE-LEMMA PLUS-COMMUTES1 (REWRITE) (EQUAL (PLUS X Y) (PLUS Y X))) WARNING: the newly proposed lemma, PLUS-COMMUTES1, could be applied whenever the previously added lemma PLUS-ADD1 could. This formula simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-COMMUTES1 (PROVE-LEMMA PLUS-COMMUTES2 (REWRITE) (EQUAL (PLUS X Y Z) (PLUS Y X Z))) WARNING: the previously added lemma, PLUS-COMMUTES1, could be applied whenever the newly proposed PLUS-COMMUTES2 could! This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-COMMUTES2 (PROVE-LEMMA PLUS-ASSOCIATES (REWRITE) (EQUAL (PLUS (PLUS X Y) Z) (PLUS X Y Z))) WARNING: the previously added lemma, PLUS-COMMUTES1, could be applied whenever the newly proposed PLUS-ASSOCIATES could! This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-ASSOCIATES (PROVE-LEMMA TIMES-0 (REWRITE) (EQUAL (TIMES X 0) 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 X) (p X)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X))) (p 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 generates the following two new formulas: Case 2. (IMPLIES (ZEROP X) (EQUAL (TIMES X 0) 0)). This simplifies, expanding the definitions of ZEROP, TIMES, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) 0) 0)) (EQUAL (TIMES X 0) 0)). This simplifies, opening up the functions ZEROP, TIMES, PLUS, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-0 (PROVE-LEMMA TIMES-NON-NUMBERP (REWRITE) (IMPLIES (NOT (NUMBERP Z)) (EQUAL (TIMES X Z) 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 Z)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z)) (p X Z))). 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 Z))) (EQUAL (TIMES X Z) 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) Z) 0) (NOT (NUMBERP Z))) (EQUAL (TIMES X Z) 0)), which simplifies, applying PLUS-COMMUTES1, and unfolding ZEROP, TIMES, EQUAL, and PLUS, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-NON-NUMBERP (PROVE-LEMMA TIMES-ADD1 (REWRITE) (EQUAL (TIMES X (ADD1 Y)) (PLUS X (TIMES X Y)))) Give the conjecture the name *1. We will try to prove it by induction. There are three plausible 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 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 (ADD1 Y)) (PLUS X (TIMES X Y)))), which simplifies, applying PLUS-COMMUTES1, and unfolding the functions ZEROP, EQUAL, TIMES, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (PLUS (SUB1 X) (TIMES (SUB1 X) Y)))) (EQUAL (TIMES X (ADD1 Y)) (PLUS X (TIMES X Y)))). This simplifies, rewriting with the lemma SUB1-ADD1, and expanding the functions ZEROP, TIMES, and PLUS, to the following two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (PLUS (SUB1 X) (TIMES (SUB1 X) Y))) (NOT (NUMBERP Y))) (EQUAL (ADD1 (PLUS 0 (TIMES (SUB1 X) (ADD1 Y)))) (PLUS X Y (TIMES (SUB1 X) Y)))). But this again simplifies, unfolding the functions EQUAL and PLUS, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (TIMES (SUB1 X) (ADD1 Y)) (PLUS (SUB1 X) (TIMES (SUB1 X) Y))) (NUMBERP Y)) (EQUAL (ADD1 (PLUS Y (TIMES (SUB1 X) (ADD1 Y)))) (PLUS X Y (TIMES (SUB1 X) Y)))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-ADD1 (PROVE-LEMMA TIMES-DISTRIBUTES1 (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 PLUS-ASSOCIATES and PLUS-COMMUTES2, and unfolding the functions ZEROP and TIMES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-DISTRIBUTES1 (PROVE-LEMMA TIMES-COMMUTES1 (REWRITE) (EQUAL (TIMES X Y) (TIMES Y X))) WARNING: the newly proposed lemma, TIMES-COMMUTES1, could be applied whenever the previously added lemma TIMES-DISTRIBUTES1 could. WARNING: the newly proposed lemma, TIMES-COMMUTES1, could be applied whenever the previously added lemma TIMES-ADD1 could. WARNING: the newly proposed lemma, TIMES-COMMUTES1, could be applied whenever the previously added lemma TIMES-NON-NUMBERP could. WARNING: the newly proposed lemma, TIMES-COMMUTES1, could be applied whenever the previously added lemma TIMES-0 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-0 and TIMES-NON-NUMBERP, and opening up the functions ZEROP, EQUAL, and TIMES, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (SUB1 X) Y) (TIMES Y (SUB1 X)))) (EQUAL (TIMES X Y) (TIMES Y X))), which simplifies, unfolding the functions ZEROP and TIMES, to: (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))). Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate (SUB1 X). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove: (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)))). However this further simplifies, applying the lemma TIMES-ADD1, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-COMMUTES1 (PROVE-LEMMA TIMES-COMMUTES2 (REWRITE) (EQUAL (TIMES X Y Z) (TIMES Y X Z))) WARNING: the previously added lemma, TIMES-COMMUTES1, could be applied whenever the newly proposed TIMES-COMMUTES2 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 TIMES-COMMUTES1, 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 TIMES-DISTRIBUTES1, 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 ] TIMES-COMMUTES2 (PROVE-LEMMA TIMES-ASSOCIATES (REWRITE) (EQUAL (TIMES (TIMES X Y) Z) (TIMES X Y Z))) WARNING: the previously added lemma, TIMES-COMMUTES1, could be applied whenever the newly proposed TIMES-ASSOCIATES could! This simplifies, rewriting with TIMES-COMMUTES1 and TIMES-COMMUTES2, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-ASSOCIATES (PROVE-LEMMA TIMES-DISTRIBUTES2 (REWRITE) (EQUAL (TIMES (PLUS X Y) Z) (PLUS (TIMES X Z) (TIMES Y Z)))) WARNING: the previously added lemma, TIMES-COMMUTES1, could be applied whenever the newly proposed TIMES-DISTRIBUTES2 could! This simplifies, appealing to the lemmas TIMES-COMMUTES1 and TIMES-DISTRIBUTES1, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-DISTRIBUTES2 (PROVE-LEMMA DIFFERENCE-IS-0 (REWRITE) (IMPLIES (NOT (LESSP Y X)) (EQUAL (DIFFERENCE X Y) 0))) Name the conjecture *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p X Y)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p (SUB1 X) (SUB1 Y))) (p X Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT can be used to show that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for X. The above induction scheme leads to the following four new goals: Case 4. (IMPLIES (AND (OR (EQUAL X 0) (NOT (NUMBERP X))) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, expanding the definitions of NOT, OR, EQUAL, LESSP, and DIFFERENCE, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL Y 0) (NOT (NUMBERP Y))) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, unfolding NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (LESSP (SUB1 Y) (SUB1 X)) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)). This simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (LESSP (SUB1 Y) (SUB1 X)) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which simplifies, using linear arithmetic, to three new conjectures: Case 1.3. (IMPLIES (AND (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, using linear arithmetic, to two new conjectures: Case 1.3.2. (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y)) (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, unfolding the functions LESSP, NOT, OR, DIFFERENCE, and EQUAL, to: T. Case 1.3.1. (IMPLIES (AND (LESSP X 1) (LESSP X Y) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1.2. (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y)) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, expanding the definitions of NOT, OR, LESSP, DIFFERENCE, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (LESSP X 1) (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y)) 0) (NOT (LESSP Y X))) (EQUAL (DIFFERENCE X Y) 0)), which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] DIFFERENCE-IS-0 (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION1 (REWRITE) (EQUAL (DIFFERENCE (PLUS I X) I) (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 I X) I) 0)). But this again simplifies, using linear arithmetic, applying DIFFERENCE-IS-0, and expanding EQUAL, to: T. Case 1. (IMPLIES (NUMBERP X) (EQUAL (DIFFERENCE (PLUS I X) I) X)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS I X) I) (NUMBERP X)) (EQUAL (DIFFERENCE (PLUS I X) I) X)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELLATION1 (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION2 (REWRITE) (EQUAL (DIFFERENCE (PLUS I X) (PLUS I Y)) (DIFFERENCE X Y))) This simplifies, using linear arithmetic, to the following two new conjectures: Case 2. (IMPLIES (LESSP (PLUS I X) (PLUS I Y)) (EQUAL (DIFFERENCE (PLUS I X) (PLUS I Y)) (DIFFERENCE X Y))). But this again simplifies, using linear arithmetic, applying DIFFERENCE-IS-0, and opening up the function EQUAL, to: T. Case 1. (IMPLIES (LESSP X Y) (EQUAL (DIFFERENCE (PLUS I X) (PLUS I Y)) (DIFFERENCE X Y))). But this again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-IS-0, and expanding EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELLATION2 (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION3 (REWRITE) (EQUAL (DIFFERENCE (PLUS I J X) J) (PLUS I X))) This simplifies, using linear arithmetic, to: (IMPLIES (LESSP (PLUS I J X) J) (EQUAL (DIFFERENCE (PLUS I J X) J) (PLUS I X))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELLATION3 (PROVE-LEMMA LESSP-REMAINDER (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, expanding the definitions of REMAINDER, LESSP, and EQUAL, to: T. Case 2. (IMPLIES (EQUAL Y 0) (EQUAL (LESSP (REMAINDER X Y) Y) F)), which 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 the new formula: (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 REWRITE) (IMPLIES (NUMBERP X) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X))) WARNING: the previously added lemma, PLUS-COMMUTES1, could be applied whenever the newly proposed REMAINDER-QUOTIENT-ELIM could! Give the conjecture the name *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest three inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP 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 generates the following three new conjectures: Case 3. (IMPLIES (AND (ZEROP Y) (NUMBERP X)) (EQUAL (PLUS (REMAINDER X Y) (TIMES Y (QUOTIENT X Y))) X)). This simplifies, appealing to the lemmas PLUS-COMMUTES1, TIMES-NON-NUMBERP, and TIMES-COMMUTES1, and expanding 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, applying TIMES-COMMUTES1 and PLUS-COMMUTES1, and expanding the definitions of 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)), which simplifies, applying TIMES-ADD1 and PLUS-COMMUTES2, and opening up ZEROP, REMAINDER, and QUOTIENT, to: (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)), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-QUOTIENT-ELIM (PROVE-LEMMA QUOTIENT-PLUS-TIMES (REWRITE) (IMPLIES (NOT (ZEROP W)) (EQUAL (QUOTIENT (PLUS V (TIMES W I)) W) (PLUS I (QUOTIENT V W)))) ((INDUCT (TIMES I W)))) This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to the following two new conjectures: Case 2. (IMPLIES (AND (ZEROP I) (NOT (EQUAL W 0)) (NUMBERP W)) (EQUAL (QUOTIENT (PLUS V (TIMES W I)) W) (PLUS I (QUOTIENT V W)))). This simplifies, applying the lemmas TIMES-COMMUTES1 and PLUS-COMMUTES1, and unfolding ZEROP, EQUAL, TIMES, and PLUS, to the following two new formulas: Case 2.2. (IMPLIES (AND (EQUAL I 0) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (NUMBERP V))) (EQUAL (QUOTIENT 0 W) (QUOTIENT V W))). This again simplifies, expanding the functions LESSP, EQUAL, and QUOTIENT, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (NUMBERP V))) (EQUAL (QUOTIENT 0 W) (QUOTIENT V W))), which again simplifies, unfolding the definitions of LESSP, EQUAL, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (IMPLIES (NOT (ZEROP W)) (EQUAL (QUOTIENT (PLUS V (TIMES W (SUB1 I))) W) (PLUS (SUB1 I) (QUOTIENT V W)))) (NOT (EQUAL W 0)) (NUMBERP W)) (EQUAL (QUOTIENT (PLUS V (TIMES W I)) W) (PLUS I (QUOTIENT V W)))), which simplifies, applying TIMES-COMMUTES1 and DIFFERENCE-PLUS-CANCELLATION3, and opening up the functions ZEROP, NOT, IMPLIES, TIMES, QUOTIENT, and PLUS, to the new formula: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL (QUOTIENT (PLUS V (TIMES W (SUB1 I))) W) (PLUS (SUB1 I) (QUOTIENT V W))) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP (PLUS V W (TIMES W (SUB1 I))) W)) (EQUAL 0 (ADD1 (PLUS (SUB1 I) (QUOTIENT V W))))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-TIMES (DEFN LEN (X) (IF (NLISTP X) 0 (ADD1 (LEN (CDR X))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, LEN is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (LEN X)) is a theorem. [ 0.0 0.0 0.0 ] LEN (PROVE-LEMMA EQUAL-LEN-0 (REWRITE) (EQUAL (EQUAL (LEN X) 0) (NLISTP X))) This formula simplifies, opening up the definition of NLISTP, to two new conjectures: Case 2. (IMPLIES (NOT (EQUAL (LEN X) 0)) (LISTP X)), which again simplifies, unfolding the definitions of LEN and EQUAL, to: T. Case 1. (IMPLIES (EQUAL (LEN X) 0) (NOT (LISTP X))), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X)) (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X))) (p X))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces three new formulas: Case 3. (IMPLIES (AND (NLISTP X) (EQUAL (LEN X) 0)) (NOT (LISTP X))), which simplifies, opening up NLISTP, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (LEN (CDR X)) 0)) (EQUAL (LEN X) 0)) (NOT (LISTP X))), which simplifies, opening up NLISTP and LEN, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (NOT (LISTP (CDR X))) (EQUAL (LEN X) 0)) (NOT (LISTP X))), which simplifies, expanding the definitions of NLISTP and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-LEN-0 (DEFN APP (X Y) (IF (NLISTP X) Y (CONS (CAR X) (APP (CDR X) Y)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, APP is accepted under the definitional principle. From the definition we can conclude that (OR (LISTP (APP X Y)) (EQUAL (APP X Y) Y)) is a theorem. [ 0.0 0.0 0.0 ] APP (PROVE-LEMMA APP-CANCELLATION (REWRITE) (EQUAL (EQUAL (APP A B) (APP A C)) (EQUAL B C))) This simplifies, obviously, to two new formulas: Case 2. (IMPLIES (NOT (EQUAL B C)) (NOT (EQUAL (APP A B) (APP A C)))), which we will name *1. Case 1. (IMPLIES (EQUAL B C) (EQUAL (EQUAL (APP A B) (APP A C)) T)). This again simplifies, opening up the definition of EQUAL, to: T. So next consider: (IMPLIES (NOT (EQUAL B C)) (NOT (EQUAL (APP A B) (APP A C)))), which we named *1 above. Let us appeal to the induction principle. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP A) (p A B C)) (IMPLIES (AND (NOT (NLISTP A)) (p (CDR A) B C)) (p A B C))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (AND (NLISTP A) (NOT (EQUAL B C))) (NOT (EQUAL (APP A B) (APP A C)))), which simplifies, opening up the functions NLISTP and APP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP A)) (NOT (EQUAL (APP (CDR A) B) (APP (CDR A) C))) (NOT (EQUAL B C))) (NOT (EQUAL (APP A B) (APP A C)))), which simplifies, applying the lemmas CAR-CONS and CDR-CONS, and opening up NLISTP and APP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] APP-CANCELLATION (PROVE-LEMMA APP-ASSOC (REWRITE) (EQUAL (APP (APP A B) C) (APP A (APP B C)))) Call the conjecture *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (NLISTP A) (p A B C)) (IMPLIES (AND (NOT (NLISTP A)) (p (CDR A) B C)) (p A B C))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (NLISTP A) (EQUAL (APP (APP A B) C) (APP A (APP B C)))), which simplifies, opening up the definitions of NLISTP and APP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP A)) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))), which simplifies, applying CDR-CONS and CAR-CONS, and unfolding NLISTP and APP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] APP-ASSOC (PROVE-LEMMA LEN-APP (REWRITE) (EQUAL (LEN (APP A B)) (PLUS (LEN A) (LEN B)))) Call the conjecture *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (NLISTP A) (p A B)) (IMPLIES (AND (NOT (NLISTP A)) (p (CDR A) B)) (p A B))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (NLISTP A) (EQUAL (LEN (APP A B)) (PLUS (LEN A) (LEN B)))), which simplifies, opening up the definitions of NLISTP, APP, LEN, EQUAL, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP A)) (EQUAL (LEN (APP (CDR A) B)) (PLUS (LEN (CDR A)) (LEN B)))) (EQUAL (LEN (APP A B)) (PLUS (LEN A) (LEN B)))), which simplifies, applying PLUS-COMMUTES1, CDR-CONS, and PLUS-ADD1, and unfolding NLISTP, APP, and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LEN-APP (PROVE-LEMMA QUOTIENT-X-X (REWRITE) (IMPLIES (NOT (ZEROP X)) (EQUAL (QUOTIENT X X) 1))) This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X)) (EQUAL (QUOTIENT X X) 1)), which simplifies, rewriting with the lemma DIFFERENCE-IS-0, and expanding the functions QUOTIENT, LESSP, EQUAL, and ADD1, to the goal: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP X X))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-X-X (PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT (REWRITE) (NOT (LESSP N (TIMES W (QUOTIENT N W))))) WARNING: Note that the proposed lemma NOT-LESSP-TIMES-QUOTIENT is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace N by (PLUS Z (TIMES W X)) to eliminate (QUOTIENT N W) and (REMAINDER N W). We use 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. We thus obtain the following two new goals: Case 2. (IMPLIES (NOT (NUMBERP N)) (NOT (LESSP N (TIMES W (QUOTIENT N W))))). This simplifies, rewriting with TIMES-COMMUTES1, and expanding LESSP, QUOTIENT, EQUAL, and TIMES, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z W) (NOT (ZEROP W)))) (NOT (LESSP (PLUS Z (TIMES W X)) (TIMES W X)))). However this simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NOT-LESSP-TIMES-QUOTIENT (PROVE-LEMMA TIMES-MONOTONIC (REWRITE) (IMPLIES (AND (NOT (ZEROP W)) (LESSP A B)) (LESSP (TIMES W A) (TIMES W B)))) WARNING: When the linear lemma TIMES-MONOTONIC is stored under (TIMES W B) it contains the free variable A which will be chosen by instantiating the hypothesis (LESSP A B). WARNING: When the linear lemma TIMES-MONOTONIC is stored under (TIMES W A) it contains the free variable B which will be chosen by instantiating the hypothesis (LESSP A B). WARNING: Note that the proposed lemma TIMES-MONOTONIC is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES W A) (TIMES W B))). This simplifies, applying TIMES-COMMUTES1, to the formula: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))). Give the above formula the name *1. We will appeal to induction. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL B 0) (NOT (NUMBERP B))) (p A W B)) (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p A W B)) (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p (SUB1 A) W (SUB1 B))) (p A W B))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for B. The above induction scheme leads to the following four new conjectures: Case 4. (IMPLIES (AND (OR (EQUAL B 0) (NOT (NUMBERP B))) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))). This simplifies, expanding the definitions of NOT, OR, EQUAL, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (OR (EQUAL A 0) (NOT (NUMBERP A))) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))). This simplifies, unfolding NOT, OR, EQUAL, LESSP, and TIMES, to the following two new formulas: Case 3.2. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL A 0) (NOT (EQUAL W 0)) (NUMBERP W)) (NOT (EQUAL (PLUS W (TIMES (SUB1 B) W)) 0))). However this again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (NUMBERP A)) (NOT (EQUAL W 0)) (NUMBERP W)) (NOT (EQUAL (PLUS W (TIMES (SUB1 B) W)) 0))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))), which simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP A 1) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))). This again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (TIMES (SUB1 A) W) (TIMES (SUB1 B) W)) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP A B)) (LESSP (TIMES A W) (TIMES B W))), which simplifies, opening up the definitions of NOT, OR, LESSP, and TIMES, to: (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 0)) (NUMBERP A) (LESSP (TIMES (SUB1 A) W) (TIMES (SUB1 B) W)) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP (SUB1 A) (SUB1 B))) (LESSP (PLUS W (TIMES (SUB1 A) W)) (PLUS W (TIMES (SUB1 B) W)))). 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-MONOTONIC (PROVE-LEMMA DIFFERENCE-PLUS (REWRITE) (EQUAL (DIFFERENCE (PLUS X Y) Y) (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 X Y) Y) 0)). But this again simplifies, expanding the definition of PLUS, to two new conjectures: Case 2.2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (NUMBERP Y))) (EQUAL (DIFFERENCE 0 Y) 0)), which again simplifies, using linear arithmetic, rewriting with DIFFERENCE-IS-0, and expanding the definition of EQUAL, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP X)) (NUMBERP Y)) (EQUAL (DIFFERENCE Y Y) 0)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP Y Y) (NOT (NUMBERP X)) (NUMBERP Y)) (EQUAL (DIFFERENCE Y Y) 0)). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (NUMBERP X) (EQUAL (DIFFERENCE (PLUS X Y) Y) X)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS X Y) Y) (NUMBERP X)) (EQUAL (DIFFERENCE (PLUS X Y) Y) X)). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS (PROVE-LEMMA NSIG*-ALG-LEMMA-HACK1 (REWRITE) (IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W)) (NUMBERP W) (NOT (EQUAL W 0))) (EQUAL (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X)) T)) ((DISABLE TIMES-MONOTONIC) (USE (TIMES-MONOTONIC (A N) (B (QUOTIENT (PLUS R X) W)))))) This formula simplifies, rewriting with TIMES-COMMUTES1, and unfolding ZEROP, NOT, AND, and IMPLIES, to the goal: (IMPLIES (AND (LESSP (TIMES N W) (TIMES W (QUOTIENT (PLUS R X) W))) (LESSP N (QUOTIENT (PLUS R X) W)) (NUMBERP W) (NOT (EQUAL W 0))) (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))). This again simplifies, using linear arithmetic and applying NOT-LESSP-TIMES-QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NSIG*-ALG-LEMMA-HACK1 (PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION-4 (REWRITE) (EQUAL (DIFFERENCE (PLUS R TS X) (PLUS TS Y)) (DIFFERENCE (PLUS R X) Y))) This simplifies, using linear arithmetic, to the following two new goals: Case 2. (IMPLIES (LESSP (PLUS R TS X) (PLUS TS Y)) (EQUAL (DIFFERENCE (PLUS R TS X) (PLUS TS Y)) (DIFFERENCE (PLUS R X) Y))). However this again simplifies, using linear arithmetic, rewriting with the lemma DIFFERENCE-IS-0, and opening up the function EQUAL, to: T. Case 1. (IMPLIES (LESSP (PLUS R X) Y) (EQUAL (DIFFERENCE (PLUS R TS X) (PLUS TS Y)) (DIFFERENCE (PLUS R X) Y))), which again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-IS-0, and opening up the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-PLUS-CANCELLATION-4 (PROVE-LEMMA NTS*-ALG-LEMMA2-HACK1 (REWRITE) (IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W)) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (TIMES N W) (PLUS R X))) (NUMBERP N) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP X W)) (EQUAL (EQUAL (QUOTIENT (PLUS R X) W) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W)) T)) ((DISABLE TIMES-MONOTONIC) (USE (TIMES-MONOTONIC (A N) (B (QUOTIENT (PLUS R X) W)) (W W))))) This conjecture simplifies, rewriting with TIMES-COMMUTES1, and opening up ZEROP, NOT, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (LESSP (TIMES N W) (TIMES W (QUOTIENT (PLUS R X) W))) (LESSP N (QUOTIENT (PLUS R X) W)) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (TIMES N W) (PLUS R X))) (NUMBERP N) (NOT (EQUAL W 0)) (NUMBERP W) (LESSP X W)) (EQUAL (QUOTIENT (PLUS R X) W) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W))), which again simplifies, using linear arithmetic and rewriting with the lemma NOT-LESSP-TIMES-QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NTS*-ALG-LEMMA2-HACK1 (PROVE-LEMMA TIMES-CANCELLATION1 (REWRITE) (IMPLIES (NOT (ZEROP I)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) (EQUAL (FIX J) (FIX K)))) ((INDUCT (LESSP J K)))) This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to three new conjectures: Case 3. (IMPLIES (AND (OR (EQUAL K 0) (NOT (NUMBERP K))) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) (EQUAL (FIX J) (FIX K)))), which simplifies, rewriting with TIMES-COMMUTES1 and TIMES-NON-NUMBERP, and opening up the functions NOT, OR, EQUAL, TIMES, and FIX, to the following six new formulas: Case 3.6. (IMPLIES (AND (EQUAL K 0) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))). This again simplifies, obviously, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), which we will name *1. Case 3.5. (IMPLIES (AND (EQUAL K 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (NUMBERP J))) (EQUAL (EQUAL (TIMES I J) 0) T)). However this again simplifies, rewriting with the lemma TIMES-NON-NUMBERP, and expanding the definition of EQUAL, to: T. Case 3.4. (IMPLIES (AND (EQUAL K 0) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL J 0)) (EQUAL (EQUAL (TIMES I J) 0) T)), which again simplifies, rewriting with TIMES-COMMUTES1, and expanding the definitions of EQUAL and TIMES, to: T. Case 3.3. (IMPLIES (AND (NOT (NUMBERP K)) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))). Name the above subgoal *2. Case 3.2. (IMPLIES (AND (NOT (NUMBERP K)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (NUMBERP J))) (EQUAL (EQUAL (TIMES I J) 0) T)). But this again simplifies, rewriting with the lemma TIMES-NON-NUMBERP, and opening up the function EQUAL, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP K)) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL J 0)) (EQUAL (EQUAL (TIMES I J) 0) T)), which again simplifies, rewriting with TIMES-COMMUTES1, and expanding the definitions of EQUAL and TIMES, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (OR (EQUAL J 0) (NOT (NUMBERP J))) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) (EQUAL (FIX J) (FIX K)))). This simplifies, applying TIMES-COMMUTES1 and TIMES-NON-NUMBERP, and expanding the definitions of NOT, OR, EQUAL, TIMES, and FIX, to two new formulas: Case 2.2. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (EQUAL J 0) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL 0 (TIMES I K)))), which again simplifies, clearly, to: (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL 0 (TIMES I K)))), which we will name *3. Case 2.1. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL 0 (TIMES I K)))). Give the above formula the name *4. Case 1. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL J 0)) (NUMBERP J) (IMPLIES (NOT (ZEROP I)) (EQUAL (EQUAL (TIMES I (SUB1 J)) (TIMES I (SUB1 K))) (EQUAL (FIX (SUB1 J)) (FIX (SUB1 K))))) (NOT (EQUAL I 0)) (NUMBERP I)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) (EQUAL (FIX J) (FIX K)))). This simplifies, unfolding ZEROP, NOT, FIX, and IMPLIES, to the following four new conjectures: Case 1.4. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL (SUB1 J) (SUB1 K))) (NOT (EQUAL (TIMES I (SUB1 J)) (TIMES I (SUB1 K)))) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J K))) (NOT (EQUAL (TIMES I J) (TIMES I K)))). Appealing to the lemma SUB1-ELIM, we now replace J by (ADD1 X) to eliminate (SUB1 J). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. The result is: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL (ADD1 X) 0)) (NOT (EQUAL X (SUB1 K))) (NOT (EQUAL (TIMES I X) (TIMES I (SUB1 K)))) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL (ADD1 X) K))) (NOT (EQUAL (TIMES I (ADD1 X)) (TIMES I K)))). However this further simplifies, applying TIMES-ADD1, to: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL X (SUB1 K))) (NOT (EQUAL (TIMES I X) (TIMES I (SUB1 K)))) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL (ADD1 X) K))) (NOT (EQUAL (PLUS I (TIMES I X)) (TIMES I K)))). Applying the lemma SUB1-ELIM, replace K by (ADD1 Z) to eliminate (SUB1 K). We rely upon the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL (ADD1 Z) 0)) (NOT (EQUAL X Z)) (NOT (EQUAL (TIMES I X) (TIMES I Z))) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL (ADD1 X) (ADD1 Z)))) (NOT (EQUAL (PLUS I (TIMES I X)) (TIMES I (ADD1 Z))))), which further simplifies, applying ADD1-EQUAL and TIMES-ADD1, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL X Z)) (NOT (EQUAL (TIMES I X) (TIMES I Z))) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL (PLUS I (TIMES I X)) (PLUS I (TIMES I Z))))), which finally simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL J 0)) (NUMBERP J) (NOT (EQUAL (SUB1 J) (SUB1 K))) (NOT (EQUAL (TIMES I (SUB1 J)) (TIMES I (SUB1 K)))) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL J K)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) T)), which again simplifies, clearly, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL J 0)) (NUMBERP J) (EQUAL (SUB1 J) (SUB1 K)) (EQUAL (EQUAL (TIMES I (SUB1 J)) (TIMES I (SUB1 K))) T) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J K))) (NOT (EQUAL (TIMES I J) (TIMES I K)))). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL J 0)) (NUMBERP J) (EQUAL (SUB1 J) (SUB1 K)) (EQUAL (EQUAL (TIMES I (SUB1 J)) (TIMES I (SUB1 K))) T) (NOT (EQUAL I 0)) (NUMBERP I) (EQUAL J K)) (EQUAL (EQUAL (TIMES I J) (TIMES I K)) T)), which again simplifies, unfolding the function EQUAL, to: T. So next consider: (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL 0 (TIMES I K)))), which is formula *4 above. Ah ha! This conjecture is subsumed by another subgoal awaiting our attention, namely *3 above. So let us turn our attention to: (IMPLIES (AND (NOT (EQUAL K 0)) (NUMBERP K) (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (EQUAL 0 (TIMES I K)))), which we named *3 above. Ah ha! This conjecture is subsumed by formula *1 above. So let us turn our attention to: (IMPLIES (AND (NOT (NUMBERP K)) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), named *2 above. Ah ha! This conjecture is subsumed by another subgoal awaiting our attention, namely *1 above. So next consider: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), named *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 I) (p I J)) (IMPLIES (AND (NOT (ZEROP I)) (p (SUB1 I) J)) (p I J))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP 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 three new formulas: Case 3. (IMPLIES (AND (ZEROP I) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), which simplifies, opening up ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP I)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), which simplifies, opening up the definitions of ZEROP and TIMES, to: (IMPLIES (AND (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (PLUS J (TIMES (SUB1 I) J)) 0))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (NOT (EQUAL (TIMES (SUB1 I) J) 0)) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (TIMES I J) 0))), which simplifies, unfolding ZEROP and TIMES, to: (IMPLIES (AND (NOT (EQUAL (TIMES (SUB1 I) J) 0)) (NOT (EQUAL I 0)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL J 0))) (NOT (EQUAL (PLUS J (TIMES (SUB1 I) J)) 0))). This again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-CANCELLATION1 (PROVE-LEMMA TIMES-CANCELLATION2 (REWRITE) (IMPLIES (NOT (ZEROP W)) (EQUAL (EQUAL (PLUS (TIMES W X) (TIMES W Y)) (TIMES W Z)) (EQUAL (PLUS X Y) (FIX Z)))) ((DISABLE TIMES-CANCELLATION1) (USE (TIMES-CANCELLATION1 (I W) (J (PLUS X Y)) (K Z))))) This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (IMPLIES (NOT (ZEROP W)) (EQUAL (EQUAL (TIMES W (PLUS X Y)) (TIMES W Z)) (EQUAL (FIX (PLUS X Y)) (FIX Z)))) (NOT (EQUAL W 0)) (NUMBERP W)) (EQUAL (EQUAL (PLUS (TIMES W X) (TIMES W Y)) (TIMES W Z)) (EQUAL (PLUS X Y) (FIX Z)))), which simplifies, applying TIMES-DISTRIBUTES1 and TIMES-NON-NUMBERP, and unfolding the definitions of ZEROP, NOT, FIX, IMPLIES, and EQUAL, to the following two new formulas: Case 2. (IMPLIES (AND (NOT (NUMBERP Z)) (NOT (EQUAL (PLUS X Y) 0)) (NOT (EQUAL (PLUS (TIMES W X) (TIMES W Y)) (TIMES W Z))) (NOT (EQUAL W 0)) (NUMBERP W)) (NOT (EQUAL (PLUS (TIMES W X) (TIMES W Y)) 0))). But this again simplifies, applying TIMES-NON-NUMBERP, and opening up EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (NUMBERP Z)) (EQUAL (PLUS X Y) 0) (EQUAL (EQUAL (PLUS (TIMES W X) (TIMES W Y)) (TIMES W Z)) T) (NOT (EQUAL W 0)) (NUMBERP W)) (EQUAL (PLUS (TIMES W X) (TIMES W Y)) 0)). But this again simplifies, applying TIMES-NON-NUMBERP, and expanding EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-CANCELLATION2 (PROVE-LEMMA DIFFERENCE-DIFFERENCE (REWRITE) (IMPLIES (NOT (LESSP B C)) (EQUAL (DIFFERENCE A (DIFFERENCE B C)) (DIFFERENCE (PLUS A C) B)))) This formula simplifies, using linear arithmetic, to the following two new formulas: Case 2. (IMPLIES (AND (LESSP A (DIFFERENCE B C)) (NOT (LESSP B C))) (EQUAL (DIFFERENCE A (DIFFERENCE B C)) (DIFFERENCE (PLUS A C) B))). However this again simplifies, using linear arithmetic, applying DIFFERENCE-IS-0, and unfolding the function EQUAL, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS A C) B) (NOT (LESSP B C))) (EQUAL (DIFFERENCE A (DIFFERENCE B C)) (DIFFERENCE (PLUS A C) B))). But this again simplifies, using linear arithmetic, rewriting with DIFFERENCE-IS-0, and opening up the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-DIFFERENCE (PROVE-LEMMA DIFFERENCE-DIFFERENCE-OTHER (REWRITE) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))) This simplifies, using linear arithmetic, to the following three new conjectures: Case 3. (IMPLIES (LESSP (DIFFERENCE A B) C) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))). But this again simplifies, using linear arithmetic, applying DIFFERENCE-IS-0, and opening up the function EQUAL, to: (IMPLIES (AND (LESSP (DIFFERENCE A B) C) (LESSP A B)) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))), which again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-IS-0, and expanding EQUAL and LESSP, to: T. Case 2. (IMPLIES (LESSP A B) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))), which again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-IS-0, and opening up the function EQUAL, to: T. Case 1. (IMPLIES (LESSP A (PLUS B C)) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))), which again simplifies, using linear arithmetic, applying the lemma DIFFERENCE-IS-0, and opening up EQUAL, to: (IMPLIES (AND (LESSP A (PLUS B C)) (LESSP A B)) (EQUAL (DIFFERENCE (DIFFERENCE A B) C) (DIFFERENCE A (PLUS B C)))). But this again simplifies, using linear arithmetic, rewriting with the lemma DIFFERENCE-IS-0, and expanding the definition of EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-DIFFERENCE-OTHER (PROVE-LEMMA QUOTIENT-PLUS-TIMES2 (REWRITE) (IMPLIES (NOT (ZEROP W)) (EQUAL (QUOTIENT (PLUS V (TIMES I W) (TIMES W J)) W) (PLUS I J (QUOTIENT V W)))) ((DISABLE QUOTIENT-PLUS-TIMES) (USE (QUOTIENT-PLUS-TIMES (I (PLUS I J)))))) This formula can be simplified, using the abbreviations ZEROP, NOT, IMPLIES, and PLUS-ASSOCIATES, to: (IMPLIES (AND (IMPLIES (NOT (ZEROP W)) (EQUAL (QUOTIENT (PLUS V (TIMES W (PLUS I J))) W) (PLUS I J (QUOTIENT V W)))) (NOT (EQUAL W 0)) (NUMBERP W)) (EQUAL (QUOTIENT (PLUS V (TIMES I W) (TIMES W J)) W) (PLUS I J (QUOTIENT V W)))), which simplifies, applying TIMES-COMMUTES1 and TIMES-DISTRIBUTES1, and unfolding the definitions of ZEROP, NOT, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-TIMES2 (PROVE-LEMMA DIFFERENCE-ELIM (ELIM) (IMPLIES (AND (NUMBERP I) (NOT (LESSP I J))) (EQUAL (PLUS J (DIFFERENCE I J)) I))) This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ELIM (PROVE-LEMMA QUOTIENT-DIFFERENCE (REWRITE) (IMPLIES (AND (NOT (ZEROP W)) (NOT (LESSP A (TIMES W B)))) (EQUAL (QUOTIENT (DIFFERENCE A (TIMES W B)) W) (DIFFERENCE (QUOTIENT A W) B)))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to the formula: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A (TIMES W B)))) (EQUAL (QUOTIENT (DIFFERENCE A (TIMES W B)) W) (DIFFERENCE (QUOTIENT A W) B))). This simplifies, applying TIMES-COMMUTES1, to the formula: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A (TIMES B W)))) (EQUAL (QUOTIENT (DIFFERENCE A (TIMES B W)) W) (DIFFERENCE (QUOTIENT A W) B))). Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we now replace A by (PLUS (TIMES B W) X) to eliminate (DIFFERENCE A (TIMES B W)) and X by (PLUS V (TIMES W Z)) to eliminate (QUOTIENT X W) and (REMAINDER X W). We rely upon the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to constrain the new variables. This generates two new goals: Case 2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A (TIMES B W)))) (EQUAL (QUOTIENT (DIFFERENCE A (TIMES B W)) W) (DIFFERENCE (QUOTIENT A W) B))), which further simplifies, using linear arithmetic, rewriting with DIFFERENCE-IS-0, and opening up the functions LESSP, EQUAL, and QUOTIENT, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V W) (NOT (ZEROP W))) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS (TIMES B W) V (TIMES W Z)) (TIMES B W)))) (EQUAL Z (DIFFERENCE (QUOTIENT (PLUS (TIMES B W) V (TIMES W Z)) W) B))). However this further simplifies, rewriting with the lemmas PLUS-COMMUTES2, PLUS-COMMUTES1, QUOTIENT-PLUS-TIMES2, and DIFFERENCE-PLUS-CANCELLATION1, and expanding the functions ZEROP, NOT, QUOTIENT, EQUAL, and PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-DIFFERENCE (PROVE-LEMMA QUOTIENT-MONOTONIC-LEMMA (REWRITE) (IMPLIES (AND (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP X V)) (EQUAL (LESSP (PLUS Z1 (TIMES Y X)) (PLUS Z2 (TIMES V Y))) T)) ((INDUCT (LESSP X V)))) This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR, and AND, to three new conjectures: Case 3. (IMPLIES (AND (OR (EQUAL V 0) (NOT (NUMBERP V))) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP X V)) (EQUAL (LESSP (PLUS Z1 (TIMES Y X)) (PLUS Z2 (TIMES V Y))) T)), which simplifies, opening up the functions NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (OR (EQUAL X 0) (NOT (NUMBERP X))) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP X V)) (EQUAL (LESSP (PLUS Z1 (TIMES Y X)) (PLUS Z2 (TIMES V Y))) T)), which simplifies, appealing to the lemmas TIMES-COMMUTES1 and PLUS-COMMUTES1, and opening up the definitions of NOT, OR, EQUAL, LESSP, TIMES, and PLUS, to four new formulas: Case 2.4. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (EQUAL X 0) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (NUMBERP Z1))) (LESSP 0 (PLUS Z2 (TIMES V Y)))), which again simplifies, using linear arithmetic and rewriting with TIMES-MONOTONIC and TIMES-NON-NUMBERP, to: T. Case 2.3. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (EQUAL X 0) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))). This again simplifies, obviously, to the new formula: (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), which we will name *1. Case 2.2. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (NOT (NUMBERP X)) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (NUMBERP Z1))) (LESSP 0 (PLUS Z2 (TIMES V Y)))). This again simplifies, using linear arithmetic and rewriting with TIMES-MONOTONIC and TIMES-NON-NUMBERP, to: T. Case 2.1. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (NOT (NUMBERP X)) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))). Name the above subgoal *2. Case 1. (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (NOT (EQUAL X 0)) (NUMBERP X) (IMPLIES (AND (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (SUB1 X) (SUB1 V))) (EQUAL (LESSP (PLUS Z1 (TIMES Y (SUB1 X))) (PLUS Z2 (TIMES (SUB1 V) Y))) T)) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP X V)) (EQUAL (LESSP (PLUS Z1 (TIMES Y X)) (PLUS Z2 (TIMES V Y))) T)). This simplifies, applying the lemmas TIMES-COMMUTES1 and PLUS-COMMUTES2, and opening up NOT, AND, IMPLIES, LESSP, and TIMES, to the new goal: (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (PLUS Z1 (TIMES Y (SUB1 X))) (PLUS Z2 (TIMES Y (SUB1 V)))) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (LESSP (SUB1 X) (SUB1 V))) (LESSP (PLUS Y Z1 (TIMES Y (SUB1 X))) (PLUS Y Z2 (TIMES Y (SUB1 V))))), which again simplifies, using linear arithmetic, to: T. So next consider: (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (NOT (NUMBERP X)) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), named *2 above. Ah ha! This conjecture is subsumed by another subgoal awaiting our attention, namely *1 above. So next consider: (IMPLIES (AND (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), which is formula *1 above. We will try to prove it by induction. There are seven 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 V) (p Z1 Z2 V Y)) (IMPLIES (AND (NOT (ZEROP V)) (p Z1 Z2 (SUB1 V) Y)) (p Z1 Z2 V Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT V) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas: Case 3. (IMPLIES (AND (ZEROP V) (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), which simplifies, unfolding the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP V)) (EQUAL (SUB1 V) 0) (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), which simplifies, applying PLUS-COMMUTES2, and opening up the definitions of ZEROP and TIMES, to: (IMPLIES (AND (EQUAL (SUB1 V) 0) (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Y Z2 (TIMES (SUB1 V) Y)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP V)) (LESSP Z1 (PLUS Z2 (TIMES (SUB1 V) Y))) (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Z2 (TIMES V Y)))), which simplifies, rewriting with PLUS-COMMUTES2, and expanding the functions ZEROP and TIMES, to: (IMPLIES (AND (LESSP Z1 (PLUS Z2 (TIMES (SUB1 V) Y))) (NOT (EQUAL V 0)) (NUMBERP V) (LESSP Z1 Y) (LESSP Z2 Y) (NOT (EQUAL Y 0)) (NUMBERP Y) (NUMBERP Z1)) (LESSP Z1 (PLUS Y Z2 (TIMES (SUB1 V) Y)))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-MONOTONIC-LEMMA (PROVE-LEMMA NTR*-ALG-LEMMA2-HACK1 (REWRITE) (IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W)) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))) (NUMBERP N) (NUMBERP TS) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS TS X) TS)) (LESSP (PLUS TS X) (PLUS TS W))) (EQUAL (EQUAL (PLUS R TS X) (PLUS TS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R)))) T)) ((DISABLE TIMES-MONOTONIC) (USE (TIMES-MONOTONIC (A N) (B (QUOTIENT (PLUS R X) W)) (W W))))) This conjecture simplifies, applying the lemmas TIMES-COMMUTES1 and NSIG*-ALG-LEMMA-HACK1, and expanding the functions ZEROP, NOT, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NTR*-ALG-LEMMA2-HACK1 (PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT-OTHER (REWRITE) (IMPLIES (NOT (LESSP X R)) (NOT (LESSP (TIMES R (QUOTIENT X R)) R)))) WARNING: Note that the proposed lemma NOT-LESSP-TIMES-QUOTIENT-OTHER is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES R Z)) to eliminate (QUOTIENT X R) and (REMAINDER X R). We rely upon 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 conjectures: Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (NOT (LESSP X R))) (NOT (LESSP (TIMES R (QUOTIENT X R)) R))). This simplifies, rewriting with TIMES-NON-NUMBERP and TIMES-COMMUTES1, and opening up the definitions of LESSP, EQUAL, QUOTIENT, and TIMES, to: T. Case 1. (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V R) (NOT (ZEROP R))) (NOT (LESSP (PLUS V (TIMES R Z)) R))) (NOT (LESSP (TIMES R Z) R))). This simplifies, applying the lemma PLUS-COMMUTES1, and unfolding ZEROP, NOT, TIMES, EQUAL, PLUS, and LESSP, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (NOT (EQUAL R 0)) (NUMBERP R) (EQUAL (LESSP V R) T) (NOT (LESSP (PLUS V (TIMES R Z)) R))) (NOT (LESSP (TIMES R Z) R))). This again simplifies, clearly, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP V) (NOT (EQUAL R 0)) (NUMBERP R) (LESSP V R) (NOT (LESSP (PLUS V (TIMES R Z)) R))) (NOT (LESSP (TIMES R Z) R))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (IMPLIES (NOT (LESSP X R)) (NOT (LESSP (TIMES R (QUOTIENT X R)) R))). We named this *1. We will try to prove it by induction. The recursive terms in the conjecture suggest five inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP R) (p R X)) (IMPLIES (AND (NOT (ZEROP R)) (LESSP X R)) (p R X)) (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP X R)) (p R (DIFFERENCE X R))) (p R X))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new formulas: Case 3. (IMPLIES (AND (ZEROP R) (NOT (LESSP X R))) (NOT (LESSP (TIMES R (QUOTIENT X R)) R))), which simplifies, appealing to the lemmas TIMES-NON-NUMBERP and TIMES-COMMUTES1, and expanding ZEROP, EQUAL, LESSP, QUOTIENT, and TIMES, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP R)) (LESSP (DIFFERENCE X R) R) (NOT (LESSP X R))) (NOT (LESSP (TIMES R (QUOTIENT X R)) R))), which simplifies, rewriting with TIMES-ADD1, and unfolding the functions ZEROP and QUOTIENT, to: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R) (LESSP (DIFFERENCE X R) R) (NOT (LESSP X R))) (NOT (LESSP (PLUS R (TIMES R (QUOTIENT (DIFFERENCE X R) R))) R))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP (TIMES R (QUOTIENT (DIFFERENCE X R) R)) R)) (NOT (LESSP X R))) (NOT (LESSP (TIMES R (QUOTIENT X R)) R))), which simplifies, rewriting with the lemma TIMES-ADD1, and expanding the definitions of ZEROP and QUOTIENT, to: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (TIMES R (QUOTIENT (DIFFERENCE X R) R)) R)) (NOT (LESSP X R))) (NOT (LESSP (PLUS R (TIMES R (QUOTIENT (DIFFERENCE X R) R))) R))). But this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] NOT-LESSP-TIMES-QUOTIENT-OTHER (PROVE-LEMMA QUOTIENT-MONOTONIC (REWRITE) (IMPLIES (AND (NOT (ZEROP W)) (NOT (LESSP A B))) (EQUAL (LESSP (QUOTIENT A W) (QUOTIENT B W)) F))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A B))) (EQUAL (LESSP (QUOTIENT A W) (QUOTIENT B W)) F)), which simplifies, obviously, to: (IMPLIES (AND (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A B))) (NOT (LESSP (QUOTIENT A W) (QUOTIENT B W)))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS Z (TIMES W X)) to eliminate (QUOTIENT A W) and (REMAINDER A W). We use 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. We thus obtain the following two new formulas: Case 2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP A B))) (NOT (LESSP (QUOTIENT A W) (QUOTIENT B W)))). However this further simplifies, expanding LESSP, QUOTIENT, and EQUAL, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z W) (NOT (ZEROP W))) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS Z (TIMES W X)) B))) (NOT (LESSP X (QUOTIENT B W)))), which further simplifies, opening up ZEROP and NOT, to: (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (LESSP Z W) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS Z (TIMES W X)) B))) (NOT (LESSP X (QUOTIENT B W)))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace B by (PLUS D (TIMES W V)) to eliminate (QUOTIENT B W) and (REMAINDER B W). We rely upon LESSP-REMAINDER, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to constrain the new variables. The result is two new goals: Case 1.2. (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP X) (NUMBERP Z) (LESSP Z W) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS Z (TIMES W X)) B))) (NOT (LESSP X (QUOTIENT B W)))), which further simplifies, unfolding the functions LESSP, QUOTIENT, and EQUAL, to: T. Case 1.1. (IMPLIES (AND (NUMBERP V) (NUMBERP D) (EQUAL (LESSP D W) (NOT (ZEROP W))) (NUMBERP X) (NUMBERP Z) (LESSP Z W) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS Z (TIMES W X)) (PLUS D (TIMES W V))))) (NOT (LESSP X V))), which further simplifies, applying TIMES-COMMUTES1 and QUOTIENT-MONOTONIC-LEMMA, and expanding the definitions of ZEROP and NOT, to: T. Q.E.D. [ 0.0 0.1 0.0 ] QUOTIENT-MONOTONIC (PROVE-LEMMA NLST*-ALG-LEMMA2-HACK1 (REWRITE) (IMPLIES (AND (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))) (NUMBERP N) (NUMBERP TS) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS TS X) TS)) (LESSP (PLUS TS X) (PLUS TS W))) (EQUAL (PLUS (QUOTIENT (PLUS R X) W) (QUOTIENT (DIFFERENCE (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) (TIMES W (QUOTIENT (PLUS R X) W))) W)) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W))) ((DISABLE QUOTIENT-DIFFERENCE) (USE (QUOTIENT-DIFFERENCE (W W) (A (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R)))) (B (QUOTIENT (PLUS R X) W)))))) WARNING: Note that NLST*-ALG-LEMMA2-HACK1 contains the free variable TS which will be chosen by instantiating the hypothesis: (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))). WARNING: the previously added lemma, PLUS-COMMUTES1, could be applied whenever the newly proposed NLST*-ALG-LEMMA2-HACK1 could! This conjecture simplifies, unfolding the definitions of ZEROP, NOT, AND, and IMPLIES, to the following two new conjectures: Case 2. (IMPLIES (AND (LESSP (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) (TIMES W (QUOTIENT (PLUS R X) W))) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))) (NUMBERP N) (NUMBERP TS) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS TS X) TS)) (LESSP (PLUS TS X) (PLUS TS W))) (EQUAL (PLUS (QUOTIENT (PLUS R X) W) (QUOTIENT (DIFFERENCE (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) (TIMES W (QUOTIENT (PLUS R X) W))) W)) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W))). However this again simplifies, using linear arithmetic and applying NOT-LESSP-TIMES-QUOTIENT-OTHER and NOT-LESSP-TIMES-QUOTIENT, to: T. Case 1. (IMPLIES (AND (EQUAL (QUOTIENT (DIFFERENCE (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) (TIMES W (QUOTIENT (PLUS R X) W))) W) (DIFFERENCE (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W) (QUOTIENT (PLUS R X) W))) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))) (NUMBERP N) (NUMBERP TS) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS TS X) TS)) (LESSP (PLUS TS X) (PLUS TS W))) (EQUAL (PLUS (QUOTIENT (PLUS R X) W) (DIFFERENCE (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W) (QUOTIENT (PLUS R X) W))) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W) (QUOTIENT (PLUS R X) W)) (EQUAL (QUOTIENT (DIFFERENCE (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) (TIMES W (QUOTIENT (PLUS R X) W))) W) (DIFFERENCE (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W) (QUOTIENT (PLUS R X) W))) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (PLUS TS (TIMES N W)) (PLUS R TS X))) (NUMBERP N) (NUMBERP TS) (NOT (EQUAL W 0)) (NUMBERP W) (NOT (LESSP (PLUS TS X) TS)) (LESSP (PLUS TS X) (PLUS TS W))) (EQUAL (PLUS (QUOTIENT (PLUS R X) W) (DIFFERENCE (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W) (QUOTIENT (PLUS R X) W))) (QUOTIENT (PLUS X (TIMES R (QUOTIENT (DIFFERENCE (TIMES N W) X) R))) W))). However this again simplifies, using linear arithmetic and rewriting with NOT-LESSP-TIMES-QUOTIENT-OTHER and QUOTIENT-MONOTONIC, to: T. Q.E.D. [ 0.0 0.3 0.0 ] NLST*-ALG-LEMMA2-HACK1 (PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA1 (REWRITE) (IMPLIES (NOT (ZEROP R)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) (DIFFERENCE TR TS)) R))))) WARNING: Note that the proposed lemma NSIG*-UPPER-BOUND-LEMMA1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to the formula: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) (DIFFERENCE TR TS)) R)))). Appealing to the lemma DIFFERENCE-ELIM, we now replace TR by (PLUS TS X) to eliminate (DIFFERENCE TR TS). We employ the type restriction lemma noted when DIFFERENCE was introduced to constrain the new variable. This generates three new conjectures: Case 3. (IMPLIES (AND (LESSP TR TS) (NOT (EQUAL R 0)) (NUMBERP R)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) (DIFFERENCE TR TS)) R)))), which simplifies, using linear arithmetic, rewriting with DIFFERENCE-IS-0, and opening up the functions EQUAL and DIFFERENCE, to the following two new formulas: Case 3.2. (IMPLIES (AND (LESSP TR TS) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL (TIMES N W) 0))) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (TIMES N W) R)))). However this again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (LESSP TR TS) (NOT (EQUAL R 0)) (NUMBERP R) (EQUAL (TIMES N W) 0)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT 0 R)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP TR)) (NOT (EQUAL R 0)) (NUMBERP R)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) (DIFFERENCE TR TS)) R)))), which simplifies, using linear arithmetic, rewriting with DIFFERENCE-IS-0, and unfolding the functions EQUAL and DIFFERENCE, to the following two new goals: Case 2.2. (IMPLIES (AND (NOT (NUMBERP TR)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL (TIMES N W) 0))) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (TIMES N W) R)))). This again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP TR)) (NOT (EQUAL R 0)) (NUMBERP R) (EQUAL (TIMES N W) 0)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT 0 R)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NOT (LESSP (PLUS TS X) TS)) (NOT (EQUAL R 0)) (NUMBERP R)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) X) R)))), which simplifies, using linear arithmetic and applying QUOTIENT-MONOTONIC, to the new conjecture: (IMPLIES (AND (NUMBERP X) (NOT (LESSP (PLUS TS X) TS)) (NOT (EQUAL R 0)) (NUMBERP R) (LESSP (TIMES N W) X)) (NOT (LESSP (QUOTIENT (TIMES N W) R) (QUOTIENT (DIFFERENCE (TIMES N W) X) R)))), which again simplifies, using linear arithmetic, applying DIFFERENCE-IS-0, and unfolding LESSP, EQUAL, and QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NSIG*-UPPER-BOUND-LEMMA1 (PROVE-LEMMA QUOTIENT-TIMES (REWRITE) (IMPLIES (NOT (ZEROP R)) (EQUAL (QUOTIENT (TIMES N R) R) (FIX N))) ((DISABLE QUOTIENT-PLUS-TIMES) (USE (QUOTIENT-PLUS-TIMES (W R) (V 0) (I N))))) This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (IMPLIES (NOT (ZEROP R)) (EQUAL (QUOTIENT (PLUS 0 (TIMES R N)) R) (PLUS N (QUOTIENT 0 R)))) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (QUOTIENT (TIMES N R) R) (FIX N))), which simplifies, applying the lemmas TIMES-COMMUTES1 and PLUS-COMMUTES1, and opening up the definitions of ZEROP, NOT, EQUAL, PLUS, LESSP, QUOTIENT, IMPLIES, TIMES, and FIX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-TIMES (PROVE-LEMMA MULTIPLY-BOTH-SIDES-OF-LESSP (REWRITE) (IMPLIES (NOT (ZEROP R)) (EQUAL (LESSP (TIMES A R) (TIMES B R)) (LESSP A B)))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (TIMES A R) (TIMES B R)) (LESSP A B))). Name the above subgoal *1. Perhaps we can 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 (ZEROP A) (p A R B)) (IMPLIES (AND (NOT (ZEROP A)) (p (SUB1 A) R (SUB1 B))) (p A R B))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for B. The above induction scheme leads to the following two new goals: Case 2. (IMPLIES (AND (ZEROP A) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (TIMES A R) (TIMES B R)) (LESSP A B))). This simplifies, opening up ZEROP, EQUAL, TIMES, and LESSP, to the following six new conjectures: Case 2.6. (IMPLIES (AND (EQUAL A 0) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (EQUAL (PLUS R (TIMES (SUB1 B) R)) 0)) (EQUAL F (NUMBERP B))). This again simplifies, using linear arithmetic, to: T. Case 2.5. (IMPLIES (AND (EQUAL A 0) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NOT (NUMBERP B))) (EQUAL F (NUMBERP B))), which again simplifies, clearly, to: T. Case 2.4. (IMPLIES (AND (EQUAL A 0) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL (PLUS R (TIMES (SUB1 B) R)) 0))) (EQUAL T (NUMBERP B))). This again simplifies, obviously, to: T. Case 2.3. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (EQUAL (PLUS R (TIMES (SUB1 B) R)) 0)) (EQUAL F (NUMBERP B))). However this again simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NOT (NUMBERP B))) (EQUAL F (NUMBERP B))), which again simplifies, clearly, to: T. Case 2.1. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL (PLUS R (TIMES (SUB1 B) R)) 0))) (EQUAL T (NUMBERP B))). This again simplifies, clearly, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (EQUAL (LESSP (TIMES (SUB1 A) R) (TIMES (SUB1 B) R)) (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (TIMES A R) (TIMES B R)) (LESSP A B))). This simplifies, expanding ZEROP, TIMES, and LESSP, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP (TIMES (SUB1 A) R) (TIMES (SUB1 B) R)) (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (PLUS R (TIMES (SUB1 A) R)) (PLUS R (TIMES (SUB1 B) R))) (LESSP (SUB1 A) (SUB1 B)))). However this further simplifies, rewriting with TIMES-COMMUTES1, to the new formula: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP (TIMES R (SUB1 A)) (TIMES R (SUB1 B))) (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (PLUS R (TIMES R (SUB1 A))) (PLUS R (TIMES R (SUB1 B)))) (LESSP (SUB1 A) (SUB1 B)))). Applying the lemma SUB1-ELIM, replace A by (ADD1 X) to eliminate (SUB1 A). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0)) (EQUAL (LESSP (TIMES R X) (TIMES R (SUB1 B))) (LESSP X (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (PLUS R (TIMES R X)) (PLUS R (TIMES R (SUB1 B)))) (LESSP X (SUB1 B)))), which further simplifies, clearly, to: (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP (TIMES R X) (TIMES R (SUB1 B))) (LESSP X (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL B 0)) (NUMBERP B)) (EQUAL (LESSP (PLUS R (TIMES R X)) (PLUS R (TIMES R (SUB1 B)))) (LESSP X (SUB1 B)))). Applying the lemma SUB1-ELIM, replace B by (ADD1 Z) to eliminate (SUB1 B). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove the new conjecture: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (EQUAL (LESSP (TIMES R X) (TIMES R Z)) (LESSP X Z)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (EQUAL (ADD1 Z) 0))) (EQUAL (LESSP (PLUS R (TIMES R X)) (PLUS R (TIMES R Z))) (LESSP X Z))), which further simplifies, obviously, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (EQUAL (LESSP (TIMES R X) (TIMES R Z)) (LESSP X Z)) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R (TIMES R X)) (PLUS R (TIMES R Z))) (LESSP X Z))). We now use the above equality hypothesis by substituting: (LESSP (TIMES R X) (TIMES R Z)) for (LESSP X Z) and throwing away the equality. The result is: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R (TIMES R X)) (PLUS R (TIMES R Z))) (LESSP (TIMES R X) (TIMES R Z)))). We will try to prove the above formula by generalizing it, replacing (TIMES R Z) by Y and (TIMES R X) by U. We restrict the new variables by recalling the type restriction lemma noted when TIMES was introduced. This produces: (IMPLIES (AND (NUMBERP Y) (NUMBERP U) (NUMBERP Z) (NUMBERP X) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))), which has two irrelevant terms in it. By eliminating these terms we get the new formula: (IMPLIES (AND (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))), which we will finally name *1.1. Case 1.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP (TIMES (SUB1 A) R) (TIMES (SUB1 B) R)) (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (EQUAL B 0)) (EQUAL (LESSP (PLUS R (TIMES (SUB1 A) R)) 0) F)). But this again simplifies, unfolding the functions SUB1, EQUAL, TIMES, and LESSP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL (LESSP (TIMES (SUB1 A) R) (TIMES (SUB1 B) R)) (LESSP (SUB1 A) (SUB1 B))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (NUMBERP B))) (EQUAL (LESSP (PLUS R (TIMES (SUB1 A) R)) 0) F)), which again simplifies, opening up EQUAL and LESSP, to: T. So next consider: (IMPLIES (AND (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))), which we named *1.1 above. Let us appeal to the induction principle. There are four plausible inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP R) (p R U Y)) (IMPLIES (AND (NOT (ZEROP R)) (p (SUB1 R) U Y)) (p R U Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition of ZEROP can be used to prove that the measure (COUNT R) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following three new conjectures: Case 3. (IMPLIES (AND (ZEROP R) (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))). This simplifies, unfolding ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP R)) (EQUAL (SUB1 R) 0) (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))). This simplifies, applying SUB1-ADD1, and unfolding ZEROP, PLUS, and LESSP, to: (IMPLIES (AND (EQUAL (SUB1 R) 0) (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS (SUB1 R) U) (PLUS (SUB1 R) Y)) (LESSP U Y))). But this again simplifies, unfolding the functions EQUAL and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP R)) (EQUAL (LESSP (PLUS (SUB1 R) U) (PLUS (SUB1 R) Y)) (LESSP U Y)) (NUMBERP Y) (NUMBERP U) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (PLUS R U) (PLUS R Y)) (LESSP U Y))), which simplifies, applying SUB1-ADD1, and unfolding the functions ZEROP, PLUS, and LESSP, to: T. That finishes the proof of *1.1, which, in turn, also finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] MULTIPLY-BOTH-SIDES-OF-LESSP (PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1 NIL (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP (QUOTIENT X R) N))) (NOT (LESSP X (TIMES N R)))) ((DISABLE MULTIPLY-BOTH-SIDES-OF-LESSP) (USE (MULTIPLY-BOTH-SIDES-OF-LESSP (A (QUOTIENT X R)) (B N))))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (IMPLIES (NOT (ZEROP R)) (EQUAL (LESSP (TIMES (QUOTIENT X R) R) (TIMES N R)) (LESSP (QUOTIENT X R) N))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (QUOTIENT X R) N))) (NOT (LESSP X (TIMES N R)))). This simplifies, applying TIMES-COMMUTES1, and unfolding the functions ZEROP, NOT, and IMPLIES, to the goal: (IMPLIES (AND (NOT (LESSP (TIMES R (QUOTIENT X R)) (TIMES N R))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP (QUOTIENT X R) N))) (NOT (LESSP X (TIMES N R)))). However this again simplifies, using linear arithmetic and rewriting with the lemma NOT-LESSP-TIMES-QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1 (PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2 NIL (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP X (TIMES N R)))) (NOT (LESSP (QUOTIENT X R) N))) ((DISABLE QUOTIENT-MONOTONIC) (USE (QUOTIENT-MONOTONIC (A X) (B (TIMES N R)) (W R))))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP X (TIMES N R)))) (EQUAL (LESSP (QUOTIENT X R) (QUOTIENT (TIMES N R) R)) F)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP X (TIMES N R)))) (NOT (LESSP (QUOTIENT X R) N))), which simplifies, applying QUOTIENT-TIMES, and opening up the functions ZEROP, NOT, AND, IMPLIES, TIMES, EQUAL, and LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2 (PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES (REWRITE) (IMPLIES (NOT (ZEROP R)) (EQUAL (LESSP (QUOTIENT X R) N) (LESSP X (TIMES N R)))) ((USE (LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1) (LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2)))) WARNING: the newly proposed lemma, LESSP-QUOTIENT-TO-LESSP-TIMES, could be applied whenever the previously added lemma QUOTIENT-MONOTONIC could. This formula can be simplified, using the abbreviations ZEROP, NOT, IMPLIES, and AND, to the new formula: (IMPLIES (AND (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP (QUOTIENT X R) N))) (NOT (LESSP X (TIMES N R)))) (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP X (TIMES N R)))) (NOT (LESSP (QUOTIENT X R) N))) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (LESSP (QUOTIENT X R) N) (LESSP X (TIMES N R)))), which simplifies, unfolding the definitions of ZEROP, NOT, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-QUOTIENT-TO-LESSP-TIMES (PROVE-LEMMA QUOTIENT-PLUS-TIMES1 (REWRITE) (IMPLIES (NOT (ZEROP R)) (EQUAL (QUOTIENT (PLUS (TIMES N R) Z) R) (PLUS N (QUOTIENT Z R)))) ((DISABLE QUOTIENT-PLUS-TIMES) (USE (QUOTIENT-PLUS-TIMES (V Z) (I N) (W R))))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to the formula: (IMPLIES (AND (IMPLIES (NOT (ZEROP R)) (EQUAL (QUOTIENT (PLUS Z (TIMES R N)) R) (PLUS N (QUOTIENT Z R)))) (NOT (EQUAL R 0)) (NUMBERP R)) (EQUAL (QUOTIENT (PLUS (TIMES N R) Z) R) (PLUS N (QUOTIENT Z R)))). This simplifies, rewriting with the lemmas TIMES-COMMUTES1 and PLUS-COMMUTES1, and unfolding the definitions of ZEROP, NOT, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-TIMES1 (PROVE-LEMMA EQUAL-TIMES-0 (REWRITE) (EQUAL (EQUAL (TIMES I J) 0) (OR (ZEROP I) (ZEROP J)))) This simplifies, opening up the functions ZEROP and OR, to five new conjectures: Case 5. (IMPLIES (NOT (EQUAL (TIMES I J) 0)) (NUMBERP J)), which again simplifies, applying TIMES-NON-NUMBERP, and unfolding the function EQUAL, to: T. Case 4. (IMPLIES (NOT (EQUAL (TIMES I J) 0)) (NOT (EQUAL J 0))). However this again simplifies, applying TIMES-COMMUTES1, and unfolding the functions EQUAL and TIMES, to: T. Case 3. (IMPLIES (NOT (EQUAL (TIMES I J) 0)) (NUMBERP I)). This again simplifies, opening up the definitions of TIMES and EQUAL, to: T. Case 2. (IMPLIES (NOT (EQUAL (TIMES I J) 0)) (NOT (EQUAL I 0))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (EQUAL (TIMES I J) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))), 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 I) (p J I)) (IMPLIES (AND (NOT (ZEROP I)) (p J (SUB1 I))) (p J I))). 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 produces three new conjectures: Case 3. (IMPLIES (AND (ZEROP I) (EQUAL (TIMES I J) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))), which simplifies, unfolding the function ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP I)) (NOT (EQUAL (TIMES (SUB1 I) J) 0)) (EQUAL (TIMES I J) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))), which simplifies, opening up ZEROP and TIMES, to: (IMPLIES (AND (NOT (EQUAL (TIMES (SUB1 I) J) 0)) (EQUAL (PLUS J (TIMES (SUB1 I) J)) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP I)) (EQUAL (SUB1 I) 0) (EQUAL (TIMES I J) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))), which simplifies, expanding the definitions of ZEROP and TIMES, to the conjecture: (IMPLIES (AND (EQUAL (SUB1 I) 0) (EQUAL (PLUS J (TIMES (SUB1 I) J)) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0))) (NOT (NUMBERP J))). This again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-TIMES-0 (PROVE-LEMMA NSIG*-UPPER-BOUND-HACK1 (REWRITE) (IMPLIES (AND (NOT (ZEROP R)) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (EQUAL (LESSP (TIMES N DELTA) R) T))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (EQUAL (LESSP (TIMES N DELTA) R) T)), which simplifies, applying TIMES-COMMUTES1, to: (IMPLIES (AND (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (LESSP (TIMES DELTA N) R)), 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. Since both of these are equally likely, we will choose arbitrarily. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA)))) (p DELTA N R)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA))))) (OR (EQUAL R 0) (NOT (NUMBERP R)))) (p DELTA N R)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA))))) (NOT (OR (EQUAL R 0) (NOT (NUMBERP R)))) (p DELTA N (SUB1 R))) (p DELTA N R))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT can be used to show that the measure (COUNT R) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to five new formulas: Case 5. (IMPLIES (AND (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA)))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (LESSP (TIMES DELTA N) R)), which simplifies, applying the lemmas EQUAL-TIMES-0 and TIMES-NON-NUMBERP, and opening up the definitions of EQUAL, NUMBERP, NOT, OR, TIMES, and LESSP, to: T. Case 4. (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA))))) (OR (EQUAL R 0) (NOT (NUMBERP R))) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (LESSP (TIMES DELTA N) R)), which simplifies, applying EQUAL-TIMES-0, and unfolding EQUAL, NUMBERP, NOT, and OR, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA))))) (NOT (OR (EQUAL R 0) (NOT (NUMBERP R)))) (EQUAL (SUB1 R) 0) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (LESSP (TIMES DELTA N) R)). This simplifies, applying EQUAL-TIMES-0, and opening up the functions EQUAL, NUMBERP, NOT, OR, and LESSP, to: (IMPLIES (AND (NOT (EQUAL DELTA 0)) (NUMBERP DELTA) (EQUAL (SUB1 R) 0) (NOT (EQUAL R 0)) (NUMBERP R) (EQUAL (SUB1 (TIMES 18 DELTA)) 0) (LESSP N 18) (NOT (EQUAL N 0))) (NOT (NUMBERP N))). But this again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0) (NOT (NUMBERP (TIMES 18 DELTA))))) (NOT (OR (EQUAL R 0) (NOT (NUMBERP R)))) (LESSP (SUB1 R) (TIMES 18 DELTA)) (NOT (EQUAL R 0)) (NUMBERP R) (NOT (LESSP R (TIMES 18 DELTA))) (LESSP N 18)) (LESSP (TIMES DELTA N) R)), which simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (OR (EQUAL (TIMES 18 DELTA) 0)