(BOOT-STRAP NQTHM) [ 0.1 0.1 0.0 ] GROUND-ZERO (COMPILE-UNCOMPILED-DEFNS "tmp") Loading ./basic/tmp.o Finished loading ./basic/tmp.o /v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp (DEFN RT (X) (IF (ZEROP X) 0 (IF (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X) (ADD1 (RT (SUB1 X))) (RT (SUB1 X))))) Linear arithmetic, the lemmas COUNT-NUMBERP and SUB1-ADD1, and the definitions of ZEROP, TIMES, and PLUS can be used to show that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, RT is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (RT X)) is a theorem. [ 0.0 0.0 0.0 ] RT (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, expanding ZEROP, EQUAL, TIMES, PLUS, and NUMBERP, 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)))), which simplifies, appealing to the lemma SUB1-ADD1, and unfolding the definitions of ZEROP, TIMES, and PLUS, to two new conjectures: 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)))), which again simplifies, opening up 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 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 SQUARE-0 (REWRITE) (EQUAL (EQUAL (TIMES X X) 0) (ZEROP X))) This conjecture simplifies, expanding ZEROP, to the following three new goals: Case 3. (IMPLIES (NOT (EQUAL (TIMES X X) 0)) (NUMBERP X)). However this again simplifies, expanding the definitions of TIMES and EQUAL, to: T. Case 2. (IMPLIES (NOT (EQUAL (TIMES X X) 0)) (NOT (EQUAL X 0))), which again simplifies, expanding the definitions of TIMES and EQUAL, to: T. Case 1. (IMPLIES (AND (EQUAL (TIMES X X) 0) (NOT (EQUAL X 0))) (NOT (NUMBERP 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 (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 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 three new goals: Case 3. (IMPLIES (AND (ZEROP X) (EQUAL (TIMES X X) 0) (NOT (EQUAL X 0))) (NOT (NUMBERP X))). This simplifies, expanding the function ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (TIMES (SUB1 X) (SUB1 X)) 0)) (EQUAL (TIMES X X) 0) (NOT (EQUAL X 0))) (NOT (NUMBERP X))). This simplifies, opening up ZEROP and TIMES, to the new formula: (IMPLIES (AND (NOT (EQUAL (TIMES (SUB1 X) (SUB1 X)) 0)) (EQUAL (PLUS X (TIMES (SUB1 X) X)) 0) (NOT (EQUAL X 0))) (NOT (NUMBERP X))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (SUB1 X) 0) (EQUAL (TIMES X X) 0) (NOT (EQUAL X 0))) (NOT (NUMBERP X))), which simplifies, expanding the functions ZEROP, TIMES, EQUAL, ADD1, and PLUS, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] SQUARE-0 (PROVE-LEMMA SQUARE-MONOTONIC NIL (IMPLIES (NOT (LESSP B A)) (NOT (LESSP (TIMES B B) (TIMES A A))))) Name the conjecture *1. Perhaps we can prove it by induction. Four 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 (OR (EQUAL A 0) (NOT (NUMBERP A))) (p B A)) (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (OR (EQUAL B 0) (NOT (NUMBERP B)))) (p B A)) (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (p (SUB1 B) (SUB1 A))) (p B A))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT B) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for A. The above induction scheme leads to the following four new conjectures: Case 4. (IMPLIES (AND (OR (EQUAL A 0) (NOT (NUMBERP A))) (NOT (LESSP B A))) (NOT (LESSP (TIMES B B) (TIMES A A)))). This simplifies, opening up NOT, OR, EQUAL, LESSP, and TIMES, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (OR (EQUAL B 0) (NOT (NUMBERP B))) (NOT (LESSP B A))) (NOT (LESSP (TIMES B B) (TIMES A A)))). This simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (LESSP (SUB1 B) (SUB1 A)) (NOT (LESSP B A))) (NOT (LESSP (TIMES B B) (TIMES A A)))). This simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP A 1) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (LESSP (SUB1 B) (SUB1 A)) (NOT (LESSP B A))) (NOT (LESSP (TIMES B B) (TIMES A A)))), which again simplifies, unfolding the definitions of SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (LESSP (TIMES (SUB1 B) (SUB1 B)) (TIMES (SUB1 A) (SUB1 A)))) (NOT (LESSP B A))) (NOT (LESSP (TIMES B B) (TIMES A A)))), which simplifies, expanding NOT, OR, LESSP, and TIMES, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP (TIMES (SUB1 B) (SUB1 B)) (TIMES (SUB1 A) (SUB1 A)))) (NOT (LESSP (SUB1 B) (SUB1 A)))) (NOT (LESSP (PLUS B (TIMES (SUB1 B) B)) (PLUS A (TIMES (SUB1 A) A))))). Appealing to the lemma SUB1-ELIM, we now replace B by (ADD1 X) to eliminate (SUB1 B). We use the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove the goal: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL (ADD1 X) 0)) (NOT (LESSP (TIMES X X) (TIMES (SUB1 A) (SUB1 A)))) (NOT (LESSP X (SUB1 A)))) (NOT (LESSP (PLUS (ADD1 X) (TIMES X (ADD1 X))) (PLUS A (TIMES (SUB1 A) A))))). However this further simplifies, appealing to the lemmas TIMES-ADD1 and SUB1-ADD1, and expanding PLUS and LESSP, to: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (LESSP (TIMES X X) (TIMES (SUB1 A) (SUB1 A)))) (NOT (LESSP X (SUB1 A))) (NOT (EQUAL (PLUS A (TIMES (SUB1 A) A)) 0))) (NOT (LESSP (PLUS X X (TIMES X X)) (SUB1 (PLUS A (TIMES (SUB1 A) A)))))). Appealing to the lemma SUB1-ELIM, we now replace A by (ADD1 Z) to eliminate (SUB1 A). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (EQUAL (ADD1 Z) 0)) (NOT (LESSP (TIMES X X) (TIMES Z Z))) (NOT (LESSP X Z)) (NOT (EQUAL (PLUS (ADD1 Z) (TIMES Z (ADD1 Z))) 0))) (NOT (LESSP (PLUS X X (TIMES X X)) (SUB1 (PLUS (ADD1 Z) (TIMES Z (ADD1 Z))))))). However this further simplifies, rewriting with the lemmas TIMES-ADD1 and SUB1-ADD1, and expanding the definition of PLUS, to: (IMPLIES (AND (NUMBERP Z) (NUMBERP X) (NOT (LESSP (TIMES X X) (TIMES Z Z))) (NOT (LESSP X Z))) (NOT (LESSP (PLUS X X (TIMES X X)) (PLUS Z Z (TIMES Z Z))))). But this finally simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] SQUARE-MONOTONIC (PROVE-LEMMA SPEC-FOR-RT NIL (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP Y (ADD1 (PLUS (RT Y) (PLUS (RT Y) (TIMES (RT Y) (RT Y)))))))) This formula can be simplified, using the abbreviations NOT and AND, to the following two new goals: Case 2. (NOT (LESSP Y (TIMES (RT Y) (RT Y)))). Name the above subgoal *1. Case 1. (LESSP Y (ADD1 (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))). This simplifies, appealing to the lemma SUB1-ADD1, and unfolding LESSP, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))). Applying the lemma SUB1-ELIM, replace Y by (ADD1 X) to eliminate (SUB1 Y). We rely upon the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We would thus like to prove the new formula: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0))) (LESSP X (PLUS (RT (ADD1 X)) (RT (ADD1 X)) (TIMES (RT (ADD1 X)) (RT (ADD1 X)))))), which further simplifies, rewriting with ADD1-EQUAL, TIMES-ADD1, and SUB1-ADD1, and opening up PLUS, TIMES, and RT, to the following two new formulas: Case 1.2. (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (PLUS (RT X) (RT X) (TIMES (RT X) (RT X))) X))) (LESSP X (PLUS (RT X) (RT X) (TIMES (RT X) (RT X))))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP Y (ADD1 (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))))). We gave this the name *1 above. Perhaps we can prove it by induction. There are eight plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y))))) (p Y)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p Y)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (p (SUB1 Y))) (p Y))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT 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 six new conjectures: Case 6. (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y))))) (NOT (LESSP Y (TIMES (RT Y) (RT Y))))). This simplifies, applying the lemmas SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and expanding the definitions of RT, TIMES, PLUS, NOT, OR, EQUAL, LESSP, and ADD1, to the following six new formulas: Case 6.6. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (NOT (EQUAL 1 Y))) (NOT (LESSP Y (TIMES 0 0)))). But this again simplifies, unfolding the functions TIMES, PLUS, ADD1, EQUAL, and LESSP, to: T. Case 6.5. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (NOT (NUMBERP Y))) (NOT (LESSP Y (TIMES 0 0)))), which again simplifies, opening up TIMES, PLUS, ADD1, EQUAL, and LESSP, to: T. Case 6.4. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (EQUAL Y 0)) (NOT (LESSP Y (TIMES 0 0)))), which again simplifies, expanding the definitions of TIMES, PLUS, ADD1, EQUAL, SUB1, RT, and LESSP, to: T. Case 6.3. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (EQUAL 1 Y)) (NOT (LESSP Y (TIMES 1 1)))), which again simplifies, expanding TIMES, PLUS, ADD1, and EQUAL, to: T. Case 6.2. (IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y) (EQUAL (ADD1 (RT (SUB1 Y))) 0) (NOT (EQUAL Y 0))) (NOT (LESSP Y (TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))), which again simplifies, using linear arithmetic, to: T. Case 6.1. (IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y) (EQUAL (ADD1 (RT (SUB1 Y))) 0) (EQUAL Y 0)) (NOT (LESSP Y (TIMES 0 0)))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (LESSP Y (TIMES (RT Y) (RT Y))))), which simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and unfolding the definitions of RT, TIMES, PLUS, NOT, and OR, to: T. Case 4. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))) (NOT (LESSP Y (TIMES (RT Y) (RT Y))))). This simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and unfolding the functions RT, TIMES, PLUS, NOT, OR, and LESSP, to the following two new formulas: Case 4.2. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (NOT (EQUAL (RT (SUB1 Y)) 0)) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))) (NOT (LESSP Y (TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))). This again simplifies, using linear arithmetic, to: T. Case 4.1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y) (NOT (EQUAL (ADD1 (RT (SUB1 Y))) 0)) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))) (NOT (LESSP (SUB1 Y) (SUB1 Y)))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y))))) (LESSP Y (ADD1 (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))))), which simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and opening up the functions RT, TIMES, PLUS, NOT, OR, ADD1, NUMBERP, EQUAL, and LESSP, to the following three new goals: Case 3.3. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL 1 Y))) (LESSP (SUB1 Y) (PLUS 0 0 (TIMES 0 0)))). But this again simplifies, opening up the functions TIMES, PLUS, ADD1, EQUAL, and LESSP, to the goal: (IMPLIES (AND (EQUAL (RT (SUB1 Y)) 0) (NOT (EQUAL Y 0)) (NUMBERP Y)) (EQUAL 1 Y)). Appealing to the lemma SUB1-ELIM, we now replace Y by (ADD1 X) to eliminate (SUB1 Y). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. The result is the conjecture: (IMPLIES (AND (NUMBERP X) (EQUAL (RT X) 0) (NOT (EQUAL (ADD1 X) 0))) (EQUAL 1 (ADD1 X))). This further simplifies, applying ADD1-EQUAL, and unfolding the function NUMBERP, to: (IMPLIES (AND (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which we will name *1.1. Case 3.2. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (EQUAL (RT (SUB1 Y)) 0) (NOT (EQUAL Y 0)) (NUMBERP Y) (EQUAL 1 Y)) (LESSP (SUB1 Y) (PLUS 1 1 (TIMES 1 1)))). This again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y) (EQUAL (ADD1 (RT (SUB1 Y))) 0) (NOT (EQUAL Y 0))) (LESSP (SUB1 Y) (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (LESSP Y (ADD1 (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))))), which simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and opening up the definitions of RT, TIMES, PLUS, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (NUMBERP (TIMES (RT Y) (RT Y)))))) (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y)))) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))) (LESSP Y (ADD1 (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))))), which simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, SQUARE-0, and PLUS-ADD1, and expanding the definitions of RT, TIMES, PLUS, NOT, OR, and LESSP, to two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y)) (NOT (EQUAL (RT (SUB1 Y)) 0)) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))) (LESSP (SUB1 Y) (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y) (EQUAL (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) Y) (NOT (EQUAL (ADD1 (RT (SUB1 Y))) 0)) (NOT (LESSP (SUB1 Y) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))) (LESSP (SUB1 Y) (ADD1 (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) (TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))) (NOT (EQUAL (SUB1 Y) 0)) (NOT (EQUAL (SUB1 (SUB1 Y)) 0))) (LESSP (SUB1 (SUB1 (SUB1 Y))) (PLUS (RT (SUB1 Y)) (RT (SUB1 Y)) Y))), which again simplifies, using linear arithmetic, to: T. So next consider: (IMPLIES (AND (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), named *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 X) (p X)) (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X) (p (SUB1 X))) (p X)) (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X)) (p (SUB1 X))) (p X))). Linear arithmetic, the lemmas COUNT-NUMBERP and SUB1-ADD1, and the definitions of ZEROP, TIMES, and PLUS 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 five new formulas: Case 5. (IMPLIES (AND (ZEROP X) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which simplifies, opening up the function ZEROP, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X) (NOT (EQUAL (RT (SUB1 X)) 0)) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which simplifies, rewriting with SUB1-ADD1 and TIMES-ADD1, and opening up the definitions of ZEROP, TIMES, PLUS, and RT, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X) (EQUAL 0 (SUB1 X)) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)). This simplifies, using linear arithmetic, to the new formula: (IMPLIES (AND (EQUAL (TIMES (ADD1 (RT 0)) (ADD1 (RT 0))) 1) (NOT (ZEROP X)) (EQUAL 1 X) (EQUAL 0 (SUB1 X)) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which again simplifies, unfolding RT, ADD1, TIMES, EQUAL, ZEROP, SUB1, and NUMBERP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X)) (NOT (EQUAL (RT (SUB1 X)) 0)) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which simplifies, applying the lemmas SUB1-ADD1 and TIMES-ADD1, and expanding ZEROP, TIMES, PLUS, and RT, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X))) (ADD1 (RT (SUB1 X)))) X)) (EQUAL 0 (SUB1 X)) (NUMBERP X) (EQUAL (RT X) 0)) (EQUAL 0 X)), which simplifies, applying SUB1-ADD1 and TIMES-ADD1, and expanding the functions ZEROP, RT, ADD1, TIMES, and PLUS, to the following two new goals: Case 1.2. (IMPLIES (AND (NOT (EQUAL 1 X)) (EQUAL 0 (SUB1 X)) (NUMBERP X) (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X)) (EQUAL (RT (SUB1 X)) 0)) (EQUAL 0 X)). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL 1 X)) (EQUAL 0 (SUB1 X)) (NUMBERP X) (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X) (EQUAL (ADD1 (RT (SUB1 X))) 0)) (EQUAL 0 X)), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1.1, which finishes the proof of *1. Q.E.D. [ 0.0 0.3 0.0 ] SPEC-FOR-RT (PROVE-LEMMA RT-IS-UNIQUE NIL (IMPLIES (AND (NUMBERP A) (LEQ (TIMES A A) Y) (LESSP Y (TIMES (ADD1 A) (ADD1 A)))) (EQUAL A (RT Y))) ((USE (SPEC-FOR-RT) (SQUARE-MONOTONIC (A (ADD1 A)) (B (RT Y))) (SQUARE-MONOTONIC (A (ADD1 (RT Y))) (B A))))) This formula simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and opening up the definitions of LESSP, RT, EQUAL, NOT, TIMES, PLUS, IMPLIES, ADD1, and NUMBERP, to 20 new conjectures: Case 20.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP 0 (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 0) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0)))) (NOT (LESSP (SUB1 (TIMES (RT 0) (RT 0))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0))))) (NUMBERP A) (NOT (LESSP 0 (TIMES A A)))) (EQUAL A 0)). This again simplifies, obviously, to: T. Case 19.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)). This again simplifies, using linear arithmetic, to two new conjectures: Case 19.2. (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)), which again simplifies, applying SQUARE-0, to: T. Case 19.1. (IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES A A) 0) (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y 0)) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) 0)) (NOT (LESSP (SUB1 0) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) 0))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)). But this again simplifies, appealing to the lemma SQUARE-0, to: T. Case 18.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))), which again simplifies, using linear arithmetic, to two new conjectures: Case 18.2. (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0) (EQUAL (TIMES A A) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A 0))) (NOT (LESSP (SUB1 0) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y 0)) (LESSP (SUB1 Y) (PLUS A A 0))) (EQUAL A (RT Y))). However this again simplifies, rewriting with SQUARE-0, and opening up the functions EQUAL, LESSP, and PLUS, to: T. Case 18.1. (IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES A A) 0) (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y 0)) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) 0)) (NOT (LESSP (SUB1 0) (PLUS A A (TIMES A A)))) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) 0))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). But this again simplifies, rewriting with SQUARE-0, and expanding the functions EQUAL, LESSP, and PLUS, to: T. Case 17.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES (RT 0) (RT 0)) 0) (NOT (LESSP 0 (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 0) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0)))) (NOT (LESSP (SUB1 (TIMES (RT 0) (RT 0))) (PLUS A A (TIMES A A)))) (LESSP (SUB1 A) (RT 0)) (NUMBERP A) (NOT (LESSP 0 (TIMES A A)))) (EQUAL A 0)). This again simplifies, opening up the definitions of RT, TIMES, EQUAL, LESSP, SUB1, and PLUS, to: T. Case 16.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)), which again simplifies, applying SUB1-NNUMBERP, and expanding the definitions of RT, TIMES, EQUAL, LESSP, and PLUS, to: T. Case 15.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). But this again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). However this again simplifies, rewriting with the lemma SQUARE-0, and expanding the definitions of EQUAL, LESSP, and PLUS, to: T. Case 14.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS A A (TIMES A A)))) (EQUAL A 0) (LESSP Y 1)) (EQUAL 0 (RT Y))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y))) (PLUS 0 0 (TIMES 0 0)))) (LESSP Y 1)) (EQUAL 0 (RT Y))). But this again simplifies, rewriting with SQUARE-0, to: T. Case 13.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP 0 (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 0) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 (RT 0)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0))))) (NUMBERP A) (NOT (LESSP 0 (TIMES A A)))) (EQUAL A 0)). This again simplifies, trivially, to: T. Case 12.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)). But this again simplifies, rewriting with SQUARE-0, to: T. Case 11.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (TIMES A A) 0) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (NOT (LESSP (SUB1 (TIMES A A)) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y))))) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))). This again simplifies, applying the lemma SQUARE-0, and expanding EQUAL and LESSP, to: T. Case 10.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (LESSP 0 (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 0) (PLUS (RT 0) (RT 0) (TIMES (RT 0) (RT 0)))) (LESSP (SUB1 (RT 0)) (RT 0)) (LESSP (SUB1 (RT 0)) (RT 0)) (NUMBERP (RT 0)) (NOT (LESSP 0 (TIMES (RT 0) (RT 0))))) (EQUAL (RT 0) 0)). But this again simplifies, expanding RT, TIMES, LESSP, SUB1, and PLUS, to: T. Case 9. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) (RT Y)) (LESSP (SUB1 (RT Y)) (RT Y)) (NUMBERP (RT Y)) (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (NOT (NUMBERP Y))) (EQUAL (RT Y) 0)). However this again simplifies, rewriting with the lemma SUB1-NNUMBERP, and expanding the functions RT, TIMES, EQUAL, LESSP, and PLUS, to: T. Case 8. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (LESSP (SUB1 A) (RT Y)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A (RT Y))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 (RT Y)) A) (EQUAL A 0) (LESSP Y 1)) (EQUAL 0 (RT Y))), which again simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (LESSP A 1) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (LESSP A 1) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (LESSP A 1) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A 0)), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (NOT (LESSP (TIMES A A) 1)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (EQUAL Y 0)) (EQUAL A 0)), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (NOT (LESSP (TIMES A A) 1)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (NOT (NUMBERP Y))) (EQUAL A 0)), which again simplifies, applying SUB1-NNUMBERP, and opening up the functions TIMES, EQUAL, LESSP, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y)))) (LESSP (SUB1 Y) (PLUS (RT Y) (RT Y) (TIMES (RT Y) (RT Y)))) (EQUAL (RT Y) 0) (NOT (LESSP (TIMES A A) 1)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A 0)). This again simplifies, using linear arithmetic, to two new formulas: Case 1.2. (IMPLIES (AND (NOT (NUMBERP Y)) (NOT (LESSP Y (TIMES 0 0))) (LESSP (SUB1 Y) (PLUS 0 0 (TIMES 0 0))) (EQUAL (RT Y) 0) (NOT (LESSP (TIMES A A) 1)) (NUMBERP A) (NOT (LESSP Y (TIMES A A))) (LESSP (SUB1 Y) (PLUS A A (TIMES A A)))) (EQUAL A 0)), which again simplifies, rewriting with SUB1-NNUMBERP, and opening up TIMES, EQUAL, LESSP, and PLUS, to: T. Case 1.1. (IMPLIES (AND (NUMBERP Y) (NOT (LESSP (TIMES 0 0) (TIMES 0 0))) (LESSP (SUB1 (TIMES 0 0)) (PLUS 0 0 (TIMES 0 0))) (EQUAL (RT (TIMES 0 0)) 0) (NOT (LESSP (TIMES A A) 1)) (NUMBERP A) (NOT (LESSP (TIMES 0 0) (TIMES A A))) (LESSP (SUB1 (TIMES 0 0)) (PLUS A A (TIMES A A)))) (EQUAL A 0)). However this again simplifies, unfolding TIMES, LESSP, SUB1, and PLUS, to: T. Q.E.D. [ 0.0 0.3 0.0 ] RT-IS-UNIQUE (PROVE-LEMMA NCONS-LEMMA (REWRITE) (EQUAL (RT (PLUS U (TIMES (PLUS U V) (PLUS U V)))) (PLUS U V)) ((USE (RT-IS-UNIQUE (Y (PLUS U (TIMES (PLUS U V) (PLUS U V)))) (A (PLUS U V)))))) This formula simplifies, rewriting with the lemmas SUB1-ADD1 and TIMES-ADD1, and expanding TIMES, PLUS, LESSP, AND, and IMPLIES, to two new conjectures: Case 2. (IMPLIES (LESSP (PLUS U (TIMES (PLUS U V) (PLUS U V))) (TIMES (PLUS U V) (PLUS U V))) (EQUAL (RT (PLUS U (TIMES (PLUS U V) (PLUS U V)))) (PLUS U V))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL (PLUS U (TIMES (PLUS U V) (PLUS U V))) 0)) (NOT (LESSP (SUB1 (PLUS U (TIMES (PLUS U V) (PLUS U V)))) (PLUS (PLUS U V) (PLUS U V) (TIMES (PLUS U V) (PLUS U V)))))) (EQUAL (RT (PLUS U (TIMES (PLUS U V) (PLUS U V)))) (PLUS U V))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] NCONS-LEMMA (DEFN NCAR (X) (DIFFERENCE X (TIMES (RT X) (RT X)))) Observe that (NUMBERP (NCAR X)) is a theorem. [ 0.0 0.0 0.0 ] NCAR (DEFN NCDR (X) (DIFFERENCE (RT X) (NCAR X))) Observe that (NUMBERP (NCDR X)) is a theorem. [ 0.0 0.0 0.0 ] NCDR (DEFN NCONS (I J) (PLUS I (TIMES (PLUS I J) (PLUS I J)))) Observe that (NUMBERP (NCONS I J)) is a theorem. [ 0.0 0.0 0.0 ] NCONS (PROVE-LEMMA NCAR-NCONS NIL (IMPLIES (NUMBERP I) (EQUAL (NCAR (NCONS I J)) I))) This conjecture simplifies, applying NCONS-LEMMA, and unfolding the functions NCONS and NCAR, to the formula: (IMPLIES (NUMBERP I) (EQUAL (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J))) I)). This again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J))) (NUMBERP I)) (EQUAL (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J))) I)). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NCAR-NCONS (PROVE-LEMMA NCDR-NCONS NIL (IMPLIES (NUMBERP J) (EQUAL (NCDR (NCONS I J)) J))) This conjecture simplifies, applying NCONS-LEMMA, and unfolding the functions NCONS, NCAR, and NCDR, to the formula: (IMPLIES (NUMBERP J) (EQUAL (DIFFERENCE (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) J)). This again simplifies, using linear arithmetic, to two new formulas: Case 2. (IMPLIES (AND (LESSP (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) (NUMBERP J)) (EQUAL (DIFFERENCE (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) J)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J))) (LESSP (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) (NUMBERP J)) (EQUAL (DIFFERENCE (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) J)). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J))) (NUMBERP J)) (EQUAL (DIFFERENCE (PLUS I J) (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J))) (TIMES (PLUS I J) (PLUS I J)))) J)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NCDR-NCONS (DEFN NCADR (X) (NCAR (NCDR X))) From the definition we can conclude that (NUMBERP (NCADR X)) is a theorem. [ 0.0 0.0 0.0 ] NCADR (DEFN NCADDR (X) (NCAR (NCDR (NCDR X)))) Note that (NUMBERP (NCADDR X)) is a theorem. [ 0.0 0.0 0.0 ] NCADDR (PROVE-LEMMA RT-LESSP (REWRITE) (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL X 1))) (LESSP (RT X) X))) WARNING: Note that the proposed lemma RT-LESSP 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, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)). Name the above subgoal *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X))) (p X)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X))))) (p X)) (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X))))) (p (SUB1 X))) (p X))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT 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 five new goals: Case 5. (IMPLIES (AND (OR (EQUAL X 0) (NOT (NUMBERP X))) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)). This simplifies, opening up NOT and OR, to: T. Case 4. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X)))) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)). This simplifies, applying the lemmas SUB1-ADD1 and TIMES-ADD1, and expanding the definitions of NOT, OR, RT, TIMES, PLUS, ADD1, EQUAL, and LESSP, to the new formula: (IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X) (EQUAL (ADD1 (RT (SUB1 X))) 0) (NOT (EQUAL X 0)) (NOT (EQUAL X 1))) (LESSP (RT (SUB1 X)) X)), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X))))) (EQUAL (SUB1 X) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)), which simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X))))) (EQUAL (SUB1 X) 1) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)), which simplifies, rewriting with the lemmas SUB1-ADD1 and TIMES-ADD1, and expanding the definitions of NOT, OR, RT, TIMES, PLUS, and LESSP, to two new goals: Case 2.2. (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X)) (NOT (EQUAL (RT (SUB1 X)) 0)) (EQUAL (SUB1 X) 1) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT (SUB1 X)) X)), which again simplifies, opening up the definitions of RT, TIMES, PLUS, ADD1, EQUAL, LESSP, SUB1, and NUMBERP, to: T. Case 2.1. (IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X) (NOT (EQUAL (ADD1 (RT (SUB1 X))) 0)) (EQUAL (SUB1 X) 1) (NOT (EQUAL X 0)) (NOT (EQUAL X 1))) (LESSP (RT (SUB1 X)) 1)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X)))) (NOT (OR (EQUAL (RT X) 0) (NOT (NUMBERP (RT X))))) (LESSP (RT (SUB1 X)) (SUB1 X)) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT X) X)), which simplifies, rewriting with SUB1-ADD1 and TIMES-ADD1, and unfolding NOT, OR, RT, TIMES, PLUS, and LESSP, to the new formula: (IMPLIES (AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X)) (RT (SUB1 X)) (TIMES (RT (SUB1 X)) (RT (SUB1 X))))) X)) (NOT (EQUAL (RT (SUB1 X)) 0)) (LESSP (RT (SUB1 X)) (SUB1 X)) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL X 1))) (LESSP (RT (SUB1 X)) X)), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RT-LESSP (PROVE-LEMMA RT-LESSEQP (REWRITE) (NOT (LESSP X (RT X))) ((USE (RT-LESSP)))) WARNING: Note that the proposed lemma RT-LESSEQP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, unfolding the definitions of ZEROP, NOT, AND, IMPLIES, RT, LESSP, and EQUAL, to the new goal: (IMPLIES (LESSP (RT X) X) (NOT (LESSP X (RT X)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RT-LESSEQP (PROVE-LEMMA DIFFERENCE-0 (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 ] DIFFERENCE-0 (PROVE-LEMMA LESSP-DIFFERENCE-1 (REWRITE) (EQUAL (LESSP (DIFFERENCE A B) C) (IF (LESSP A B) (LESSP 0 C) (LESSP A (PLUS B C))))) This conjecture simplifies, expanding the functions EQUAL and LESSP, to the following three new formulas: Case 3. (IMPLIES (NOT (LESSP A B)) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))). Call the above conjecture *1. Case 2. (IMPLIES (AND (LESSP A B) (EQUAL C 0)) (EQUAL (LESSP (DIFFERENCE A B) C) F)). This again simplifies, applying DIFFERENCE-0, and expanding the functions LESSP and EQUAL, to: T. Case 1. (IMPLIES (AND (LESSP A B) (NOT (EQUAL C 0))) (EQUAL (LESSP (DIFFERENCE A B) C) (NUMBERP C))). However this again simplifies, rewriting with DIFFERENCE-0, and unfolding EQUAL and LESSP, to: T. So let us turn our attention to: (IMPLIES (NOT (LESSP A B)) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))), named *1 above. Perhaps we can 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 (OR (EQUAL B 0) (NOT (NUMBERP B))) (p A B C)) (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p A B C)) (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p (SUB1 A) (SUB1 B) C)) (p A B C))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT 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 produces the following four new goals: Case 4. (IMPLIES (AND (OR (EQUAL B 0) (NOT (NUMBERP B))) (NOT (LESSP A B))) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))). This simplifies, opening up the definitions of NOT, OR, EQUAL, LESSP, DIFFERENCE, and PLUS, to the following ten new conjectures: Case 4.10. (IMPLIES (AND (EQUAL B 0) (NOT (NUMBERP C)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP A C) (LESSP A 0))). However this again simplifies, unfolding LESSP and EQUAL, to: T. Case 4.9. (IMPLIES (AND (EQUAL B 0) (NOT (NUMBERP C)) (EQUAL A 0)) (EQUAL (LESSP 0 C) (LESSP A 0))), which again simplifies, unfolding LESSP and EQUAL, to: T. Case 4.8. (IMPLIES (AND (EQUAL B 0) (NOT (NUMBERP C)) (NOT (NUMBERP A))) (EQUAL (LESSP 0 C) (LESSP A 0))), which again simplifies, expanding the functions LESSP and EQUAL, to: T. Case 4.7. (IMPLIES (AND (EQUAL B 0) (NUMBERP C) (EQUAL A 0)) (EQUAL (LESSP 0 C) (LESSP A C))), which again simplifies, clearly, to: T. Case 4.6. (IMPLIES (AND (EQUAL B 0) (NUMBERP C) (NOT (NUMBERP A))) (EQUAL (LESSP 0 C) (LESSP A C))). But this again simplifies, unfolding the definitions of EQUAL and LESSP, to: T. Case 4.5. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (NUMBERP C)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (LESSP A C) (LESSP A 0))), which again simplifies, unfolding the functions LESSP and EQUAL, to: T. Case 4.4. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (NUMBERP C)) (EQUAL A 0)) (EQUAL (LESSP 0 C) (LESSP A 0))), which again simplifies, expanding the functions LESSP and EQUAL, to: T. Case 4.3. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (NUMBERP C)) (NOT (NUMBERP A))) (EQUAL (LESSP 0 C) (LESSP A 0))), which again simplifies, expanding LESSP and EQUAL, to: T. Case 4.2. (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP C) (EQUAL A 0)) (EQUAL (LESSP 0 C) (LESSP A C))), which again simplifies, obviously, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP B)) (NUMBERP C) (NOT (NUMBERP A))) (EQUAL (LESSP 0 C) (LESSP A C))). This again simplifies, unfolding 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 (LESSP A B))) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))), which simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (SUB1 A) (SUB1 B)) (NOT (LESSP A B))) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))), which simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP B 1) (NOT (OR (EQUAL B 0) (NOT (NUMBERP B)))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (SUB1 A) (SUB1 B)) (NOT (LESSP A B))) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))). This again simplifies, expanding the functions 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)))) (EQUAL (LESSP (DIFFERENCE (SUB1 A) (SUB1 B)) C) (LESSP (SUB1 A) (PLUS (SUB1 B) C))) (NOT (LESSP A B))) (EQUAL (LESSP (DIFFERENCE A B) C) (LESSP A (PLUS B C)))), which simplifies, applying SUB1-ADD1, and expanding the definitions of NOT, OR, LESSP, DIFFERENCE, and PLUS, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-DIFFERENCE-1 (PROVE-LEMMA NCAR-LESSEQP (REWRITE) (NOT (LESSP X (NCAR X)))) WARNING: Note that the linear lemma NCAR-LESSEQP is being stored under the term (NCAR X), which is unusual because NCAR is a nonrecursive function symbol. WARNING: Note that the proposed lemma NCAR-LESSEQP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, expanding the function NCAR, to: (NOT (LESSP X (DIFFERENCE X (TIMES (RT X) (RT X))))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (LESSP X (TIMES (RT X) (RT X))) (NOT (LESSP X (DIFFERENCE X (TIMES (RT X) (RT X)))))). This again simplifies, rewriting with DIFFERENCE-0, and expanding EQUAL and LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NCAR-LESSEQP (PROVE-LEMMA CROCK (REWRITE) (EQUAL (LESSP X (DIFFERENCE (RT X) D)) F) NIL) This conjecture simplifies, using linear arithmetic and applying RT-LESSEQP, to: (IMPLIES (LESSP (RT X) D) (NOT (LESSP X (DIFFERENCE (RT X) D)))). But this again simplifies, rewriting with DIFFERENCE-0, and unfolding the definitions of EQUAL and LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] CROCK (PROVE-LEMMA NCDR-LESSEQP (REWRITE) (NOT (LESSP X (NCDR X)))) WARNING: Note that the linear lemma NCDR-LESSEQP is being stored under the term (NCDR X), which is unusual because NCDR is a nonrecursive function symbol. WARNING: Note that the proposed lemma NCDR-LESSEQP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, applying CROCK, and opening up the definitions of NCAR and NCDR, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NCDR-LESSEQP (PROVE-LEMMA NCDR-LESSP (REWRITE) (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (NCAR FN) 0)) (NOT (EQUAL (NCAR FN) 1))) (LESSP (NCDR FN) FN))) WARNING: Note that the linear lemma NCDR-LESSP is being stored under the term (NCDR FN), which is unusual because NCDR is a nonrecursive function symbol. WARNING: Note that the proposed lemma NCDR-LESSP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula simplifies, rewriting with LESSP-DIFFERENCE-1, and opening up the functions NCAR, NCDR, EQUAL, and LESSP, to the following two new goals: Case 2. (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 0)) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 1)) (NOT (LESSP (RT FN) (DIFFERENCE FN (TIMES (RT FN) (RT FN)))))) (LESSP (RT FN) (PLUS (DIFFERENCE FN (TIMES (RT FN) (RT FN))) FN))). However this again simplifies, using linear arithmetic, rewriting with RT-LESSEQP and DIFFERENCE-0, and unfolding EQUAL, LESSP, and PLUS, to the following two new goals: Case 2.2. (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 0)) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 1)) (LESSP FN (TIMES (RT FN) (RT FN))) (NOT (LESSP (RT FN) (DIFFERENCE FN (TIMES (RT FN) (RT FN)))))) (LESSP (RT FN) FN)). This again simplifies, using linear arithmetic and appealing to the lemma RT-LESSEQP, to the goal: (IMPLIES (AND (EQUAL (RT FN) FN) (NUMBERP FN) (NOT (EQUAL (DIFFERENCE FN (TIMES FN FN)) 0)) (NOT (EQUAL (DIFFERENCE FN (TIMES FN FN)) 1)) (LESSP FN (TIMES FN FN)) (NOT (LESSP FN (DIFFERENCE FN (TIMES FN FN))))) (LESSP FN FN)). However this again simplifies, applying DIFFERENCE-0, and expanding the function EQUAL, to: T. Case 2.1. (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 0)) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 1)) (NOT (LESSP FN (TIMES (RT FN) (RT FN))))) (LESSP (RT FN) (PLUS (DIFFERENCE FN (TIMES (RT FN) (RT FN))) FN))). But this again simplifies, using linear arithmetic and rewriting with RT-LESSEQP, to: T. Case 1. (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 0)) (NOT (EQUAL (DIFFERENCE FN (TIMES (RT FN) (RT FN))) 1)) (LESSP (RT FN) (DIFFERENCE FN (TIMES (RT FN) (RT FN))))) (NOT (EQUAL FN 0))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP 0 (TIMES (RT 0) (RT 0))) (NUMBERP 0) (NOT (EQUAL (DIFFERENCE 0 (TIMES (RT 0) (RT 0))) 0)) (NOT (EQUAL (DIFFERENCE 0 (TIMES (RT 0) (RT 0))) 1))) (NOT (LESSP (RT 0) (DIFFERENCE 0 (TIMES (RT 0) (RT 0)))))). But this again simplifies, expanding the definitions of RT, TIMES, and LESSP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] NCDR-LESSP (DISABLE NCAR) [ 0.0 0.0 0.0 ] NCAR-OFF (DISABLE NCDR) [ 0.0 0.0 0.0 ] NCDR-OFF (DEFN PR-APPLY (FN ARG) (IF (NOT (NUMBERP FN)) 0 (IF (EQUAL (NCAR FN) 0) 0 (IF (EQUAL (NCAR FN) 1) ARG (IF (EQUAL (NCAR FN) 2) (ADD1 ARG) (IF (EQUAL (NCAR FN) 3) (RT ARG) (IF (EQUAL (NCAR FN) 4) (IF (ZEROP ARG) 0 (PR-APPLY (NCDR FN) (PR-APPLY FN (SUB1 ARG)))) (IF (EQUAL (NCAR FN) 5) (PLUS (PR-APPLY (NCADR FN) ARG) (PR-APPLY (NCADDR FN) ARG)) (IF (EQUAL (NCAR FN) 6) (DIFFERENCE (PR-APPLY (NCADR FN) ARG) (PR-APPLY (NCADDR FN) ARG)) (IF (EQUAL (NCAR FN) 7) (TIMES (PR-APPLY (NCADR FN) ARG) (PR-APPLY (NCADDR FN) ARG)) (IF (EQUAL (NCAR FN) 8) (PR-APPLY (NCADR FN) (PR-APPLY (NCADDR FN) ARG)) 0)))))))))) ((ORD-LESSP (CONS (ADD1 (COUNT FN)) (COUNT ARG))))) Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-EQUAL, COUNT-NUMBERP, NCDR-LESSP, NCAR-LESSEQP, and NCDR-LESSEQP, and the definitions of ORDINALP, LESSP, ORD-LESSP, ZEROP, EQUAL, NCADDR, and NCADR establish that the measure (CONS (ADD1 (COUNT FN)) (COUNT ARG)) decreases according to the well-founded relation ORD-LESSP in each recursive call. Hence, PR-APPLY is accepted under the definitional principle. Observe that: (OR (NUMBERP (PR-APPLY FN ARG)) (EQUAL (PR-APPLY FN ARG) ARG)) is a theorem. [ 0.0 0.0 0.0 ] PR-APPLY (DEFN NON-PR-FN (X) (ADD1 (PR-APPLY X X))) Observe that (NUMBERP (NON-PR-FN X)) is a theorem. [ 0.0 0.0 0.0 ] NON-PR-FN (DEFN COUNTER-EXAMPLE-FOR (X) (FIX X)) Observe that (NUMBERP (COUNTER-EXAMPLE-FOR X)) is a theorem. [ 0.0 0.0 0.0 ] COUNTER-EXAMPLE-FOR (PROVE-LEMMA NON-PR-FUNCTIONS-EXIST NIL (NOT (EQUAL (NON-PR-FN (COUNTER-EXAMPLE-FOR FN)) (PR-APPLY FN (COUNTER-EXAMPLE-FOR FN))))) This formula simplifies, expanding the function COUNTER-EXAMPLE-FOR, to two new conjectures: Case 2. (IMPLIES (NOT (NUMBERP FN)) (NOT (EQUAL (NON-PR-FN 0) (PR-APPLY FN 0)))), which again simplifies, opening up the functions NON-PR-FN, PR-APPLY, and EQUAL, to: T. Case 1. (IMPLIES (NUMBERP FN) (NOT (EQUAL (NON-PR-FN FN) (PR-APPLY FN FN)))), which again simplifies, opening up the definition of NON-PR-FN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NON-PR-FUNCTIONS-EXIST (PROVE-LEMMA COUNTER-EXAMPLE-FOR-NUMERIC (REWRITE) (NUMBERP (COUNTER-EXAMPLE-FOR X))) This simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COUNTER-EXAMPLE-FOR-NUMERIC (DISABLE PR-APPLY) [ 0.0 0.0 0.0 ] PR-APPLY-OFF (DEFN MAX2 (FN I) (IF (ZEROP I) (PR-APPLY FN I) (MAX (PR-APPLY FN I) (MAX2 FN (SUB1 I))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT I) decreases according to the well-founded relation LESSP in each recursive call. Hence, MAX2 is accepted under the definitional principle. Note that: (OR (NUMBERP (MAX2 FN I)) (EQUAL (MAX2 FN I) I)) is a theorem. [ 0.0 0.0 0.0 ] MAX2 (DEFN MAX1 (FN I) (IF (ZEROP FN) (MAX2 FN I) (MAX (MAX2 FN I) (MAX1 (SUB1 FN) I)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT FN) decreases according to the well-founded relation LESSP in each recursive call. Hence, MAX1 is accepted under the definitional principle. Note that: (OR (NUMBERP (MAX1 FN I)) (EQUAL (MAX1 FN I) I)) is a theorem. [ 0.0 0.0 0.0 ] MAX1 (PROVE-LEMMA MAX2-GTE (REWRITE) (NOT (LESSP (MAX2 I J) (PR-APPLY I J)))) WARNING: Note that the proposed lemma MAX2-GTE is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. Name the conjecture *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p I J)) (IMPLIES (AND (NOT (ZEROP J)) (p I (SUB1 J))) (p I J))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT J) 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 J) (NOT (LESSP (MAX2 I J) (PR-APPLY I J)))). This simplifies, expanding ZEROP, EQUAL, and MAX2, to the following two new formulas: Case 2.2. (IMPLIES (EQUAL J 0) (NOT (LESSP (PR-APPLY I 0) (PR-APPLY I 0)))). However this again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (NOT (NUMBERP J)) (NOT (LESSP (PR-APPLY I J) (PR-APPLY I J)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (NOT (LESSP (MAX2 I (SUB1 J)) (PR-APPLY I (SUB1 J))))) (NOT (LESSP (MAX2 I J) (PR-APPLY I J)))), which simplifies, expanding ZEROP, MAX2, and MAX, to two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX2 I (SUB1 J)) (PR-APPLY I (SUB1 J)))) (NOT (LESSP (PR-APPLY I J) (MAX2 I (SUB1 J))))) (NOT (LESSP (PR-APPLY I J) (PR-APPLY I J)))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX2 I (SUB1 J)) (PR-APPLY I (SUB1 J)))) (LESSP (PR-APPLY I J) (MAX2 I (SUB1 J)))) (NOT (LESSP (MAX2 I (SUB1 J)) (PR-APPLY I J)))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] MAX2-GTE (DEFN EXCEED (J) (ADD1 (MAX1 J J))) Observe that (NUMBERP (EXCEED J)) is a theorem. [ 0.0 0.0 0.0 ] EXCEED (DEFN EXCEED-AT (I) I) Note that (EQUAL (EXCEED-AT I) I) is a theorem. [ 0.0 0.0 0.0 ] EXCEED-AT (PROVE-LEMMA MAX1-GTE1 (REWRITE) (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 (PLUS J FN) I) (PR-APPLY FN I))))) WARNING: Note that the proposed lemma MAX1-GTE1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. Name the conjecture *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP J) (p J FN I)) (IMPLIES (AND (NOT (ZEROP J)) (p (SUB1 J) FN I)) (p J FN I))). 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 leads to the following two new conjectures: Case 2. (IMPLIES (AND (ZEROP J) (NUMBERP FN)) (NOT (LESSP (MAX1 (PLUS J FN) I) (PR-APPLY FN I)))). This simplifies, opening up ZEROP, EQUAL, and PLUS, to the following two new conjectures: Case 2.2. (IMPLIES (AND (EQUAL J 0) (NUMBERP FN)) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))). This again simplifies, trivially, to: (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))), which we will name *1.1. Case 2.1. (IMPLIES (AND (NOT (NUMBERP J)) (NUMBERP FN)) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))). Eliminate the irrelevant term. This produces: (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))), which we will name *1.2. Case 1. (IMPLIES (AND (NOT (ZEROP J)) (NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I) (PR-APPLY FN I))) (NUMBERP FN)) (NOT (LESSP (MAX1 (PLUS J FN) I) (PR-APPLY FN I)))). This simplifies, rewriting with SUB1-ADD1, and unfolding the definitions of ZEROP, PLUS, MAX, and MAX1, to two new goals: Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I) (PR-APPLY FN I))) (NUMBERP FN) (NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I) (MAX1 (PLUS (SUB1 J) FN) I))) (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I))) (NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I) (PR-APPLY FN I)))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I) (PR-APPLY FN I))) (NUMBERP FN) (NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I) (MAX1 (PLUS (SUB1 J) FN) I))) (NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)))) (NOT (LESSP 0 (PR-APPLY FN I)))), which again simplifies, opening up LESSP and EQUAL, to two new conjectures: Case 1.1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I) (PR-APPLY FN I))) (NUMBERP FN) (EQUAL (MAX1 (PLUS (SUB1 J) FN) I) 0) (NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I))) (NOT (EQUAL (PR-APPLY FN I) 0))) (NOT (NUMBERP (PR-APPLY FN I)))), which again simplifies, using linear arithmetic, to: T. Case 1.1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I) (PR-APPLY FN I))) (NUMBERP FN) (NOT (NUMBERP (MAX1 (PLUS (SUB1 J) FN) I))) (NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I))) (NOT (EQUAL (PR-APPLY FN I) 0))) (NOT (NUMBERP (PR-APPLY FN I)))), which again simplifies, expanding the function LESSP, to: T. So we now return to: (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))), which is formula *1.2 above. This conjecture is subsumed by formula *1.1 above. So let us turn our attention to: (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))), named *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 FN) (p FN I)) (IMPLIES (AND (NOT (ZEROP FN)) (p (SUB1 FN) I)) (p FN I))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT FN) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new conjectures: Case 2. (IMPLIES (AND (ZEROP FN) (NUMBERP FN)) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))), which simplifies, opening up the functions ZEROP, NUMBERP, EQUAL, and MAX1, to the conjecture: (IMPLIES (EQUAL FN 0) (NOT (LESSP (MAX2 0 I) (PR-APPLY 0 I)))). However this again simplifies, using linear arithmetic and rewriting with MAX2-GTE, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP FN)) (NOT (LESSP (MAX1 (SUB1 FN) I) (PR-APPLY (SUB1 FN) I))) (NUMBERP FN)) (NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))). This simplifies, expanding ZEROP, MAX1, and MAX, to the following three new conjectures: Case 1.3. (IMPLIES (AND (NOT (EQUAL FN 0)) (NOT (LESSP (MAX1 (SUB1 FN) I) (PR-APPLY (SUB1 FN) I))) (NUMBERP FN) (NOT (LESSP (MAX2 FN I) (MAX1 (SUB1 FN) I))) (NUMBERP (MAX2 FN I))) (NOT (LESSP (MAX2 FN I) (PR-APPLY FN I)))). But this again simplifies, using linear arithmetic and rewriting with MAX2-GTE, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL FN 0)) (NOT (LESSP (MAX1 (SUB1 FN) I) (PR-APPLY (SUB1 FN) I))) (NUMBERP FN) (NOT (LESSP (MAX2 FN I) (MAX1 (SUB1 FN) I))) (NOT (NUMBERP (MAX2 FN I)))) (NOT (LESSP 0 (PR-APPLY FN I)))). But this again simplifies, using linear arithmetic and rewriting with MAX2-GTE, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL FN 0)) (NOT (LESSP (MAX1 (SUB1 FN) I) (PR-APPLY (SUB1 FN) I))) (NUMBERP FN) (LESSP (MAX2 FN I) (MAX1 (SUB1 FN) I))) (NOT (LESSP (MAX1 (SUB1 FN) I) (PR-APPLY FN I)))). However this again simplifies, using linear arithmetic and applying MAX2-GTE, to: T. That finishes the proof of *1.1, which, in turn, also finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] MAX1-GTE1 (PROVE-LEMMA MAX1-GTE2 (REWRITE) (IMPLIES (NUMBERP FN) (NOT (LESSP (MAX1 (PLUS J FN) (PLUS J FN)) (PR-APPLY FN (PLUS J FN)))))) WARNING: Note that the proposed lemma MAX1-GTE2 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula simplifies, using linear arithmetic and applying the lemma MAX1-GTE1, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX1-GTE2 (PROVE-LEMMA EXCEED-IS-BIGGER NIL (IMPLIES (NUMBERP FN) (LESSP (PR-APPLY FN (PLUS J (EXCEED-AT FN))) (EXCEED (PLUS J (EXCEED-AT FN)))))) This formula can be simplified, using the abbreviations IMPLIES and EXCEED-AT, to the new conjecture: (IMPLIES (NUMBERP FN) (LESSP (PR-APPLY FN (PLUS J FN)) (EXCEED (PLUS J FN)))), which simplifies, applying SUB1-ADD1, and unfolding the functions EXCEED and LESSP, to the new formula: (IMPLIES (AND (NUMBERP FN) (NOT (EQUAL (PR-APPLY FN (PLUS J FN)) 0))) (LESSP (SUB1 (PR-APPLY FN (PLUS J FN))) (MAX1 (PLUS J FN) (PLUS J FN)))), which again simplifies, using linear arithmetic and applying the lemma MAX1-GTE2, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXCEED-IS-BIGGER