(BOOT-STRAP NQTHM) [ 0.0 0.1 0.0 ] GROUND-ZERO (DEFN S-PLUS (X Y) (IF X (IF Y (PLUS X Y) F) F)) Observe that (OR (FALSEP (S-PLUS X Y)) (NUMBERP (S-PLUS X Y))) is a theorem. [ 0.0 0.0 0.0 ] S-PLUS (DCL APPLY (X Y)) [ 0.0 0.0 0.0 ] APPLY (DCL G-COST (X)) [ 0.0 0.0 0.0 ] G-COST (DCL G (X)) [ 0.0 0.0 0.0 ] G (ADD-AXIOM G-DEFN NIL (EQUAL (G X) (IF (G-COST X) (IF (ZEROP X) 0 (ADD1 (G (G (SUB1 X))))) (APPLY 'G (LIST X))))) [ 0.0 0.0 0.0 ] G-DEFN (ADD-AXIOM G-COST-DEFN NIL (EQUAL (G-COST X) (IF (ZEROP X) 1 (S-PLUS 1 (S-PLUS (G-COST (SUB1 X)) (G-COST (G (SUB1 X)))))))) [ 0.0 0.0 0.0 ] G-COST-DEFN (PROVE-LEMMA G-COST-OPENER (REWRITE) (AND (IMPLIES (ZEROP X) (EQUAL (G-COST X) 1)) (IMPLIES (NOT (ZEROP X)) (EQUAL (G-COST X) (S-PLUS 1 (S-PLUS (G-COST (SUB1 X)) (G-COST (G (SUB1 X)))))))) ((USE (G-COST-DEFN)))) WARNING: Note that the proposed lemma G-COST-OPENER is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This simplifies, applying the lemma SUB1-NNUMBERP, and unfolding ZEROP, S-PLUS, EQUAL, IMPLIES, NOT, AND, and SUB1, to four new conjectures: Case 4. (IMPLIES (AND (EQUAL X 0) (EQUAL (G-COST X) 1)) (EQUAL (G-COST 0) 1)), which again simplifies, obviously, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (G-COST (SUB1 X))) (EQUAL (G-COST X) (S-PLUS 1 F))) (NOT (S-PLUS 1 F))). But this again simplifies, opening up S-PLUS, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (G-COST (G (SUB1 X)))) (EQUAL (G-COST X) (S-PLUS 1 F))) (NOT (S-PLUS 1 F))), which again simplifies, opening up the function S-PLUS, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (G-COST (SUB1 X)) (G-COST (G (SUB1 X))) (EQUAL (G-COST X) (S-PLUS 1 (PLUS (G-COST (SUB1 X)) (G-COST (G (SUB1 X))))))) (EQUAL (G-COST X) (PLUS 1 (G-COST (SUB1 X)) (G-COST (G (SUB1 X)))))), which again simplifies, expanding S-PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] G-COST-OPENER (PROVE-LEMMA G-OPENER (REWRITE) (AND (IMPLIES (ZEROP X) (EQUAL (G X) (IF (G-COST X) 0 (APPLY 'G (LIST X))))) (IMPLIES (NOT (ZEROP X)) (EQUAL (G X) (IF (G-COST X) (ADD1 (G (G (SUB1 X)))) (APPLY 'G (LIST X)))))) ((USE (G-DEFN)))) WARNING: Note that the proposed lemma G-OPENER is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This simplifies, applying G-COST-OPENER and SUB1-NNUMBERP, and unfolding the definitions of ZEROP, IMPLIES, NOT, AND, S-PLUS, SUB1, and EQUAL, to the following four new goals: Case 4. (IMPLIES (AND (G-COST X) (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (G X) (ADD1 (G (G (SUB1 X))))) (NOT (G-COST (SUB1 X))) (NOT (S-PLUS 1 F))) (EQUAL (G X) (APPLY 'G (LIST X)))). However this again simplifies, applying the lemma G-COST-OPENER, and opening up the definition of S-PLUS, to: T. Case 3. (IMPLIES (AND (G-COST X) (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (G X) (ADD1 (G (G (SUB1 X))))) (NOT (G-COST (G (SUB1 X)))) (NOT (S-PLUS 1 F))) (EQUAL (G X) (APPLY 'G (LIST X)))), which again simplifies, applying the lemma G-COST-OPENER, and expanding S-PLUS, to: T. Case 2. (IMPLIES (AND (G-COST X) (NOT (EQUAL X 0)) (NUMBERP X) (EQUAL (G X) (ADD1 (G (G (SUB1 X))))) (G-COST (SUB1 X)) (G-COST (G (SUB1 X))) (NOT (S-PLUS 1 (PLUS (G-COST (SUB1 X)) (G-COST (G (SUB1 X))))))) (EQUAL (G X) (APPLY 'G (LIST X)))), which again simplifies, rewriting with G-COST-OPENER, and unfolding the function S-PLUS, to: T. Case 1. (IMPLIES (AND (G-COST X) (EQUAL X 0) (EQUAL (G X) 0)) (EQUAL (G 0) 0)). This again simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] G-OPENER (PROVE-LEMMA G-THEOREM (REWRITE) (AND (G-COST X) (EQUAL (G X) (FIX X))) ((INDUCT (PLUS X Y)))) WARNING: the newly proposed lemma, G-THEOREM, could be applied whenever the previously added lemma G-OPENER could. WARNING: the newly proposed lemma, G-THEOREM, could be applied whenever the previously added lemma G-OPENER could. WARNING: Note that the proposed lemma G-THEOREM is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, OR, and AND, to two new conjectures: Case 2. (IMPLIES (ZEROP X) (AND (G-COST X) (EQUAL (G X) (FIX X)))), which simplifies, applying G-COST-OPENER and G-OPENER, and unfolding the definitions of ZEROP, FIX, EQUAL, and AND, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (G-COST (SUB1 X)) (EQUAL (G (SUB1 X)) (FIX (SUB1 X)))) (AND (G-COST X) (EQUAL (G X) (FIX X)))). This simplifies, appealing to the lemmas G-COST-OPENER, ADD1-SUB1, and G-OPENER, and opening up the functions FIX, S-PLUS, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] G-THEOREM (DEFN ISUB1 (X) (IF (NEGATIVEP X) (MINUS (ADD1 (NEGATIVE-GUTS X))) (SUB1 X))) Note that (OR (NUMBERP (ISUB1 X)) (NEGATIVEP (ISUB1 X))) is a theorem. [ 0.0 0.0 0.0 ] ISUB1 (DCL FACT-COST (X)) [ 0.0 0.0 0.0 ] FACT-COST (DCL FACT (X)) [ 0.0 0.0 0.0 ] FACT (ADD-AXIOM FACT-DEFN NIL (EQUAL (FACT X) (IF (FACT-COST X) (IF (EQUAL X 0) 1 (FACT (ISUB1 X))) (APPLY 'FACT (LIST X))))) [ 0.0 0.0 0.0 ] FACT-DEFN (ADD-AXIOM FACT-COST-DEFN NIL (EQUAL (FACT-COST X) (IF (EQUAL X 0) 1 (S-PLUS 1 (FACT-COST (ISUB1 X)))))) [ 0.0 0.0 0.0 ] FACT-COST-DEFN (PROVE-LEMMA FACT-COST-OPENER-NUMBERP (REWRITE) (AND (IMPLIES (EQUAL X 0) (EQUAL (FACT-COST X) 1)) (IMPLIES (NOT (ZEROP X)) (EQUAL (FACT-COST X) (S-PLUS 1 (FACT-COST (SUB1 X)))))) ((USE (FACT-COST-DEFN)))) WARNING: Note that the proposed lemma FACT-COST-OPENER-NUMBERP is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula simplifies, rewriting with the lemma SUB1-NNUMBERP, and opening up the functions ISUB1, IMPLIES, ZEROP, NOT, S-PLUS, AND, PLUS, EQUAL, NUMBERP, and SUB1, to four new goals: Case 4. (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (NEGATIVEP X)) (EQUAL (FACT-COST X) (S-PLUS 1 (FACT-COST (SUB1 X)))) (NUMBERP X) (FACT-COST (SUB1 X)) (NOT (NUMBERP (FACT-COST (SUB1 X))))) (EQUAL (FACT-COST X) 1)), which again simplifies, opening up ADD1, PLUS, EQUAL, NUMBERP, SUB1, and S-PLUS, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (NEGATIVEP X)) (EQUAL (FACT-COST X) (S-PLUS 1 (FACT-COST (SUB1 X)))) (NUMBERP X) (FACT-COST (SUB1 X)) (NUMBERP (FACT-COST (SUB1 X)))) (EQUAL (FACT-COST X) (ADD1 (FACT-COST (SUB1 X))))), which again simplifies, unfolding the definitions of PLUS, EQUAL, NUMBERP, SUB1, and S-PLUS, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (NEGATIVEP X)) (EQUAL (FACT-COST X) (S-PLUS 1 (FACT-COST (SUB1 X)))) (NUMBERP X) (NOT (FACT-COST (SUB1 X)))) (EQUAL (FACT-COST X) F)), which again simplifies, unfolding S-PLUS, to: T. Case 1. (IMPLIES (AND (EQUAL X 0) (EQUAL (FACT-COST X) 1)) (EQUAL (FACT-COST 0) 1)), which again simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-COST-OPENER-NUMBERP (PROVE-LEMMA FACT-DEFINED-NUMBERP NIL (IMPLIES (NUMBERP X) (FACT-COST X)) ((INDUCT (PLUS X Y)))) 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 X) (NUMBERP X)) (FACT-COST X)). This simplifies, rewriting with the lemma FACT-COST-OPENER-NUMBERP, and unfolding the functions ZEROP, NUMBERP, and EQUAL, to: (IMPLIES (EQUAL X 0) 1), which again simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (IMPLIES (NUMBERP (SUB1 X)) (FACT-COST (SUB1 X)))) (FACT-COST X)). This simplifies, rewriting with FACT-COST-OPENER-NUMBERP, and opening up the definitions of IMPLIES, PLUS, EQUAL, NUMBERP, SUB1, and S-PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-DEFINED-NUMBERP (PROVE-LEMMA FACT-DEFINED-OTHER NIL (IMPLIES (AND (ZEROP X) (NOT (NEGATIVEP X))) (FACT-COST X)) ((USE (FACT-COST-DEFN)))) This formula simplifies, expanding the definitions of ISUB1, S-PLUS, and ZEROP, to the new goal: (IMPLIES (AND (NOT (EQUAL X 0)) (NOT (FACT-COST (SUB1 X))) (NOT (NUMBERP X)) (NOT (NEGATIVEP X))) (FACT-COST X)), which again simplifies, applying the lemmas SUB1-NNUMBERP and FACT-COST-OPENER-NUMBERP, and expanding the function EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-DEFINED-OTHER (DEFN FACT-UNDEFINED-IND (X N) (IF (ZEROP N) T (FACT-UNDEFINED-IND (ADD1 X) (SUB1 N)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, FACT-UNDEFINED-IND is accepted under the principle of definition. Observe that: (TRUEP (FACT-UNDEFINED-IND X N)) is a theorem. [ 0.0 0.0 0.0 ] FACT-UNDEFINED-IND (PROVE-LEMMA FACT-UNDEFINED-NUMBERP-LEMMA-INDUCTIVE-STEP (REWRITE) (IMPLIES (AND (NOT (ZEROP N)) (FACT-COST (MINUS X)) (IMPLIES (FACT-COST (MINUS (ADD1 X))) (LEQ (SUB1 N) (FACT-COST (MINUS (ADD1 X)))))) (EQUAL (LESSP (FACT-COST (MINUS X)) N) F)) ((USE (FACT-COST-DEFN (X (MINUS X)))))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to the conjecture: (IMPLIES (AND (EQUAL (FACT-COST (MINUS X)) (IF (EQUAL (MINUS X) 0) 1 (S-PLUS 1 (FACT-COST (ISUB1 (MINUS X)))))) (NOT (EQUAL N 0)) (NUMBERP N) (FACT-COST (MINUS X)) (IMPLIES (FACT-COST (MINUS (ADD1 X))) (IF (LESSP (FACT-COST (MINUS (ADD1 X))) (SUB1 N)) F T))) (EQUAL (LESSP (FACT-COST (MINUS X)) N) F)). This simplifies, applying the lemmas NEGATIVE-GUTS-MINUS, NEGATIVE-GUTS-TYPE-RESTRICTION, and SUB1-TYPE-RESTRICTION, and expanding the definitions of ISUB1, MINUS, and IMPLIES, to the following four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (FACT-COST (MINUS X)) (S-PLUS 1 (FACT-COST -1))) (NOT (EQUAL N 0)) (NUMBERP N) (FACT-COST (MINUS 0)) (NOT (FACT-COST -1))) (NOT (LESSP (FACT-COST (MINUS 0)) N))). This again simplifies, applying NEGATIVE-GUTS-TYPE-RESTRICTION, and opening up S-PLUS, to: T. Case 3. (IMPLIES (AND (NOT (NUMBERP X)) (EQUAL (FACT-COST (MINUS X)) (S-PLUS 1 (FACT-COST -1))) (NOT (EQUAL N 0)) (NUMBERP N) (FACT-COST (MINUS 0)) (NOT (LESSP (FACT-COST -1) (SUB1 N)))) (NOT (LESSP (FACT-COST (MINUS 0)) N))). This again simplifies, appealing to the lemma NEGATIVE-GUTS-TYPE-RESTRICTION, and expanding S-PLUS, to: (IMPLIES (AND (NOT (NUMBERP X)) (FACT-COST -1) (EQUAL (FACT-COST (MINUS 0)) (PLUS 1 (FACT-COST -1))) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (LESSP (FACT-COST -1) (SUB1 N)))) (NOT (LESSP (FACT-COST (MINUS 0)) N))). This again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NUMBERP X) (EQUAL (FACT-COST (MINUS X)) (S-PLUS 1 (FACT-COST (MINUS (ADD1 X))))) (NOT (EQUAL N 0)) (NUMBERP N) (FACT-COST (MINUS X)) (NOT (FACT-COST (MINUS (ADD1 X))))) (NOT (LESSP (FACT-COST (MINUS X)) N))), which again simplifies, unfolding S-PLUS, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (FACT-COST (MINUS X)) (S-PLUS 1 (FACT-COST (MINUS (ADD1 X))))) (NOT (EQUAL N 0)) (NUMBERP N) (FACT-COST (MINUS X)) (NOT (LESSP (FACT-COST (MINUS (ADD1 X))) (SUB1 N)))) (NOT (LESSP (FACT-COST (MINUS X)) N))), which again simplifies, unfolding the functions PLUS, EQUAL, NUMBERP, SUB1, S-PLUS, and LESSP, to: (IMPLIES (AND (NUMBERP X) (FACT-COST (MINUS (ADD1 X))) (NUMBERP (FACT-COST (MINUS (ADD1 X)))) (EQUAL (FACT-COST (MINUS X)) (ADD1 (FACT-COST (MINUS (ADD1 X))))) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (LESSP (FACT-COST (MINUS (ADD1 X))) (SUB1 N)))) (NOT (LESSP (FACT-COST (MINUS X)) N))). However this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-UNDEFINED-NUMBERP-LEMMA-INDUCTIVE-STEP (PROVE-LEMMA FACT-UNDEFINED-NEGATIVEP-LEMMA NIL (IMPLIES (FACT-COST (MINUS X)) (EQUAL (LESSP (FACT-COST (MINUS X)) N) F)) ((INDUCT (FACT-UNDEFINED-IND X N)))) This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to the following two new formulas: Case 2. (IMPLIES (AND (ZEROP N) (FACT-COST (MINUS X))) (EQUAL (LESSP (FACT-COST (MINUS X)) N) F)). This simplifies, unfolding ZEROP, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (IMPLIES (FACT-COST (MINUS (ADD1 X))) (EQUAL (LESSP (FACT-COST (MINUS (ADD1 X))) (SUB1 N)) F)) (FACT-COST (MINUS X))) (EQUAL (LESSP (FACT-COST (MINUS X)) N) F)). This simplifies, rewriting with FACT-UNDEFINED-NUMBERP-LEMMA-INDUCTIVE-STEP, and opening up the functions IMPLIES, LESSP, EQUAL, and NUMBERP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-UNDEFINED-NEGATIVEP-LEMMA (PROVE-LEMMA FACT-UNDEFINED-NEGATIVEP (REWRITE) (IMPLIES (NEGATIVEP Z) (EQUAL (FACT-COST Z) F)) ((USE (FACT-UNDEFINED-NEGATIVEP-LEMMA (X (NEGATIVE-GUTS Z)) (N (ADD1 (FACT-COST Z))))))) This formula simplifies, applying MINUS-NEGATIVE-GUTS and SUB1-ADD1, and expanding the functions LESSP and IMPLIES, to the formula: (IMPLIES (AND (NOT (EQUAL (FACT-COST Z) 0)) (NUMBERP (FACT-COST Z)) (NOT (LESSP (SUB1 (FACT-COST Z)) (FACT-COST Z)))) (NOT (NEGATIVEP Z))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-UNDEFINED-NEGATIVEP (PROVE-LEMMA FACT-DOMAIN (REWRITE) (IFF (FACT-COST X) (NOT (NEGATIVEP X))) ((USE (FACT-DEFINED-NUMBERP) (FACT-DEFINED-OTHER)))) This formula simplifies, applying FACT-UNDEFINED-NEGATIVEP, and expanding the functions IMPLIES, ZEROP, NOT, AND, and IFF, to two new formulas: Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (FACT-COST X)) (NOT (NEGATIVEP X))), which again simplifies, rewriting with FACT-UNDEFINED-NEGATIVEP, to: T. Case 1. (IMPLIES (FACT-COST X) (NOT (NEGATIVEP X))). This again simplifies, rewriting with the lemma FACT-UNDEFINED-NEGATIVEP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FACT-DOMAIN (DEFN REV (X) (IF (LISTP X) (APPEND (REV (CDR X)) (LIST (CAR X))) NIL)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, REV is accepted under the principle of definition. Note that (OR (LITATOM (REV X)) (LISTP (REV X))) is a theorem. [ 0.0 0.0 0.0 ] REV (DEFN PLISTP (X) (IF (LISTP X) (PLISTP (CDR X)) (EQUAL X NIL))) Linear arithmetic and the lemma CDR-LESSP can be used to establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, PLISTP is accepted under the principle of definition. From the definition we can conclude that: (OR (FALSEP (PLISTP X)) (TRUEP (PLISTP X))) is a theorem. [ 0.0 0.0 0.0 ] PLISTP (DEFN LENGTH (X) (IF (LISTP X) (ADD1 (LENGTH (CDR X))) 0)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, LENGTH is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (LENGTH X)) is a theorem. [ 0.0 0.0 0.0 ] LENGTH (DCL REV3-COST (X)) [ 0.0 0.0 0.0 ] REV3-COST (DCL REV3 (X)) [ 0.0 0.0 0.0 ] REV3 (ADD-AXIOM REV3-DEFN NIL (EQUAL (REV3 X) (IF (REV3-COST X) (IF (LISTP (CDR X)) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) X) (APPLY 'REV3 (LIST X))))) [ 0.0 0.0 0.0 ] REV3-DEFN (ADD-AXIOM REV3-COST-DEFN NIL (EQUAL (REV3-COST X) (IF (LISTP (CDR X)) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (S-PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) 1))) [ 0.0 0.0 0.0 ] REV3-COST-DEFN (PROVE-LEMMA REV3-COST-OPENER (REWRITE) (AND (IMPLIES (LISTP (CDR X)) (EQUAL (REV3-COST X) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (S-PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (IMPLIES (NLISTP (CDR X)) (EQUAL (REV3-COST X) 1))) ((USE (REV3-COST-DEFN)))) WARNING: Note that the proposed lemma REV3-COST-OPENER is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula simplifies, opening up the definitions of S-PLUS, IMPLIES, NLISTP, EQUAL, and AND, to four new conjectures: Case 4. (IMPLIES (AND (LISTP (CDR X)) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (EQUAL (REV3-COST X) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (NOT (REV3-COST X))), which again simplifies, opening up the definition of S-PLUS, to: T. Case 3. (IMPLIES (AND (LISTP (CDR X)) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (EQUAL (REV3-COST X) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (NOT (REV3-COST X))), which again simplifies, opening up S-PLUS, to: T. Case 2. (IMPLIES (AND (LISTP (CDR X)) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (REV3-COST X) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (NOT (REV3-COST (CDR X)))) (EQUAL (REV3-COST X) (S-PLUS 1 F))), which again simplifies, unfolding the functions S-PLUS and EQUAL, to: T. Case 1. (IMPLIES (AND (LISTP (CDR X)) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (REV3-COST X) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (REV3-COST (CDR X))) (EQUAL (REV3-COST X) (S-PLUS 1 (PLUS (REV3-COST (CDR X)) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))), which again simplifies, unfolding the definition of S-PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REV3-COST-OPENER (PROVE-LEMMA REV3-DEFN-OPENER (REWRITE) (AND (IMPLIES (LISTP (CDR X)) (EQUAL (REV3 X) (IF (REV3-COST X) (IF (LISTP (CDR X)) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) X) (APPLY 'REV3 (LIST X))))) (IMPLIES (NLISTP (CDR X)) (EQUAL (REV3 X) X))) ((USE (REV3-DEFN)))) WARNING: Note that the proposed lemma REV3-DEFN-OPENER is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula simplifies, appealing to the lemma REV3-COST-OPENER, and unfolding the definitions of IMPLIES, NLISTP, AND, and S-PLUS, to four new conjectures: Case 4. (IMPLIES (AND (NOT (REV3-COST X)) (EQUAL (REV3 X) (APPLY 'REV3 (LIST X))) (NOT (LISTP (CDR X)))) (EQUAL (REV3 X) X)), which again simplifies, applying REV3-COST-OPENER, to: T. Case 3. (IMPLIES (AND (REV3-COST X) (LISTP (CDR X)) (EQUAL (REV3 X) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (EQUAL (REV3 X) (APPLY 'REV3 (LIST X)))). However this again simplifies, applying REV3-COST-OPENER, and opening up the definition of S-PLUS, to: T. Case 2. (IMPLIES (AND (REV3-COST X) (LISTP (CDR X)) (EQUAL (REV3 X) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (EQUAL (REV3 X) (APPLY 'REV3 (LIST X)))). However this again simplifies, applying REV3-COST-OPENER, and unfolding the function S-PLUS, to: T. Case 1. (IMPLIES (AND (REV3-COST X) (LISTP (CDR X)) (EQUAL (REV3 X) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (EQUAL (REV3 X) (APPLY 'REV3 (LIST X)))). This again simplifies, appealing to the lemma REV3-COST-OPENER, and expanding the definition of S-PLUS, to: (IMPLIES (AND (NOT (REV3-COST (CDR X))) (S-PLUS 1 F) (LISTP (CDR X)) (EQUAL (REV3 X) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (EQUAL (REV3 X) (APPLY 'REV3 (LIST X)))). This again simplifies, expanding the function S-PLUS, to: T. Q.E.D. [ 0.0 0.3 0.0 ] REV3-DEFN-OPENER (DEFN REV3-INDUCTION (X N) (IF (OR (ZEROP N) (ZEROP (SUB1 N))) T (AND (REV3-INDUCTION (CDR X) (SUB1 N)) (REV3-INDUCTION (CDR (REV3 (CDR X))) (SUB1 (SUB1 N))) (REV3-INDUCTION (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))) (SUB1 N))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of OR and ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, REV3-INDUCTION is accepted under the principle of definition. From the definition we can conclude that (TRUEP (REV3-INDUCTION X N)) is a theorem. [ 0.0 0.0 0.0 ] REV3-INDUCTION (PROVE-LEMMA LENGTH-0 (REWRITE) (AND (EQUAL (EQUAL (LENGTH X) 0) (NOT (LISTP X))) (EQUAL (EQUAL 0 (LENGTH X)) (NOT (LISTP X))))) WARNING: Note that the proposed lemma LENGTH-0 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviation AND, to the following two new goals: Case 2. (EQUAL (EQUAL (LENGTH X) 0) (NOT (LISTP X))). This simplifies, expanding NOT, to the following two new formulas: Case 2.2. (IMPLIES (NOT (EQUAL (LENGTH X) 0)) (LISTP X)). However this again simplifies, expanding the functions LENGTH and EQUAL, to: T. Case 2.1. (IMPLIES (EQUAL (LENGTH X) 0) (NOT (LISTP X))), which we will name *1. Case 1. (EQUAL (EQUAL 0 (LENGTH X)) (NOT (LISTP X))). This simplifies, unfolding the function NOT, to the following two new formulas: Case 1.2. (IMPLIES (NOT (EQUAL 0 (LENGTH X))) (LISTP X)). This again simplifies, opening up the functions LENGTH and EQUAL, to: T. Case 1.1. (IMPLIES (EQUAL 0 (LENGTH X)) (NOT (LISTP X))), 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: (AND (EQUAL (EQUAL (LENGTH X) 0) (NOT (LISTP X))) (EQUAL (EQUAL 0 (LENGTH X)) (NOT (LISTP X)))). We named this *1. We will try to prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP can be used to 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 four new conjectures: Case 4. (IMPLIES (AND (LISTP X) (EQUAL (EQUAL (LENGTH (CDR X)) 0) (NOT (LISTP (CDR X)))) (EQUAL (EQUAL 0 (LENGTH (CDR X))) (NOT (LISTP (CDR X))))) (EQUAL (EQUAL (LENGTH X) 0) (NOT (LISTP X)))). This simplifies, expanding NOT, EQUAL, LENGTH, and ADD1, to: T. Case 3. (IMPLIES (NOT (LISTP X)) (EQUAL (EQUAL (LENGTH X) 0) (NOT (LISTP X)))). This simplifies, unfolding the definitions of LENGTH, EQUAL, and NOT, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (EQUAL (LENGTH (CDR X)) 0) (NOT (LISTP (CDR X)))) (EQUAL (EQUAL 0 (LENGTH (CDR X))) (NOT (LISTP (CDR X))))) (EQUAL (EQUAL 0 (LENGTH X)) (NOT (LISTP X)))). This simplifies, expanding the definitions of NOT, EQUAL, LENGTH, and ADD1, to: T. Case 1. (IMPLIES (NOT (LISTP X)) (EQUAL (EQUAL 0 (LENGTH X)) (NOT (LISTP X)))). This simplifies, expanding the functions LENGTH, EQUAL, and NOT, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-0 (PROVE-LEMMA REV3-LENGTH-AND-DEFINEDNESS-LEMMA NIL (IMPLIES (EQUAL (LENGTH X) N) (AND (REV3-COST X) (EQUAL (LENGTH (REV3 X)) N))) ((INDUCT (REV3-INDUCTION X N)))) This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to the following two new conjectures: Case 2. (IMPLIES (AND (OR (ZEROP N) (ZEROP (SUB1 N))) (EQUAL (LENGTH X) N)) (AND (REV3-COST X) (EQUAL (LENGTH (REV3 X)) N))). This simplifies, appealing to the lemmas LENGTH-0, CDR-NLISTP, REV3-COST-OPENER, and REV3-DEFN-OPENER, and opening up the definitions of ZEROP, OR, LISTP, LENGTH, EQUAL, and AND, to the following two new conjectures: Case 2.2. (IMPLIES (EQUAL (SUB1 (LENGTH X)) 0) (REV3-COST X)). Call the above conjecture *1. Case 2.1. (IMPLIES (EQUAL (SUB1 (LENGTH X)) 0) (EQUAL (LENGTH (REV3 X)) (LENGTH X))). Name the above subgoal *2. Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL (SUB1 N) 0)) (NUMBERP (SUB1 N)) (IMPLIES (EQUAL (LENGTH (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (SUB1 N)) (AND (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (SUB1 N)))) (IMPLIES (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (SUB1 N))) (AND (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (SUB1 N))))) (IMPLIES (EQUAL (LENGTH (CDR X)) (SUB1 N)) (AND (REV3-COST (CDR X)) (EQUAL (LENGTH (REV3 (CDR X))) (SUB1 N)))) (EQUAL (LENGTH X) N)) (AND (REV3-COST X) (EQUAL (LENGTH (REV3 X)) N))). This simplifies, rewriting with SUB1-ADD1, LENGTH-0, CDR-CONS, REV3-COST-OPENER, REV3-DEFN-OPENER, CDR-NLISTP, and CAR-NLISTP, and unfolding the definitions of LENGTH, AND, IMPLIES, S-PLUS, LISTP, CDR, ADD1, and EQUAL, to 18 new conjectures: Case 1.18. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.17. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.16. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). This again simplifies, using linear arithmetic, to: T. Case 1.15. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.14. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.13. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). This again simplifies, using linear arithmetic, to: T. Case 1.12. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (NOT (LISTP (REV3 (CDR X))))) (NOT (EQUAL 0 (LENGTH (CDR X))))), which again simplifies, applying CDR-NLISTP and REV3-DEFN-OPENER, and expanding the definitions of EQUAL, LISTP, CDR, LENGTH, ADD1, and SUB1, to: T. Case 1.11. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.10. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). This again simplifies, using linear arithmetic, to: T. Case 1.9. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). This again simplifies, using linear arithmetic, to: T. Case 1.8. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to the formula: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.7. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (EQUAL (ADD1 (LENGTH (REV3 (CDR (REV3 (CDR X)))))) (LENGTH (CDR X)))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (NOT (LISTP (REV3 (CDR X))))) (NOT (EQUAL 0 (LENGTH (CDR X))))), which again simplifies, applying CDR-NLISTP, REV3-DEFN-OPENER, REV3-COST-OPENER, and LENGTH-0, and opening up EQUAL, LISTP, CDR, LENGTH, ADD1, and SUB1, to: T. Case 1.6. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). But this again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.5. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) (PLUS (REV3-COST (CDR (REV3 (CDR X)))) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). This again simplifies, using linear arithmetic, to: T. Case 1.4. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (NOT (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (APPLY 'REV3 (LIST X))) (ADD1 (LENGTH (CDR X)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.3. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH (CDR X)) 0) (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (LISTP (REV3 (CDR X))) (EQUAL (ADD1 (LENGTH (CDR (REV3 (CDR X))))) (LENGTH (CDR X))) (NOT (REV3-COST (CDR (REV3 (CDR X))))) (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F))) (AND (S-PLUS 1 (S-PLUS (REV3-COST (CDR X)) F)) (EQUAL (LENGTH (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (ADD1 (LENGTH (CDR X)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (NOT (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (LENGTH (CDR X))))) (REV3-COST (CDR X)) (NOT (LISTP (REV3 (CDR X))))) (NOT (EQUAL 0 (LENGTH (CDR X))))), which again simplifies, applying the lemmas CDR-NLISTP, REV3-DEFN-OPENER, CDR-CONS, and REV3-COST-OPENER, and expanding the functions EQUAL, LISTP, CDR, ADD1, and LENGTH, to: T. Case 1.1. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (REV3-COST (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (LENGTH (CDR X))) (REV3-COST (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (REV3 (CDR (REV3 (CDR X))))) (SUB1 (LENGTH (CDR X)))) (REV3-COST (CDR X)) (NOT (LISTP (REV3 (CDR X))))) (NOT (EQUAL 0 (LENGTH (CDR X))))), which again simplifies, rewriting with CDR-NLISTP, REV3-DEFN-OPENER, CDR-CONS, and REV3-COST-OPENER, and opening up the functions EQUAL, LISTP, CDR, ADD1, and LENGTH, to: T. So let us turn our attention to: (IMPLIES (EQUAL (SUB1 (LENGTH X)) 0) (EQUAL (LENGTH (REV3 X)) (LENGTH X))), which is formula *2 above. Perhaps we can prove it by induction. 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 (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP can be used to 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 three new conjectures: Case 3. (IMPLIES (AND (LISTP X) (NOT (EQUAL (SUB1 (LENGTH (CDR X))) 0)) (EQUAL (SUB1 (LENGTH X)) 0)) (EQUAL (LENGTH (REV3 X)) (LENGTH X))), which simplifies, rewriting with SUB1-ADD1, LENGTH-0, and REV3-DEFN-OPENER, and unfolding the function LENGTH, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (LENGTH (REV3 (CDR X))) (LENGTH (CDR X))) (EQUAL (SUB1 (LENGTH X)) 0)) (EQUAL (LENGTH (REV3 X)) (LENGTH X))). This simplifies, appealing to the lemmas SUB1-ADD1, LENGTH-0, and REV3-DEFN-OPENER, and expanding the definition of LENGTH, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (EQUAL (SUB1 (LENGTH X)) 0)) (EQUAL (LENGTH (REV3 X)) (LENGTH X))). This simplifies, applying CDR-NLISTP and REV3-DEFN-OPENER, and unfolding LENGTH, SUB1, EQUAL, and LISTP, to: T. That finishes the proof of *2. So next consider: (IMPLIES (EQUAL (SUB1 (LENGTH X)) 0) (REV3-COST X)), which we 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 (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following three new conjectures: Case 3. (IMPLIES (AND (LISTP X) (NOT (EQUAL (SUB1 (LENGTH (CDR X))) 0)) (EQUAL (SUB1 (LENGTH X)) 0)) (REV3-COST X)). This simplifies, rewriting with the lemmas SUB1-ADD1, LENGTH-0, and REV3-COST-OPENER, and unfolding the function LENGTH, to the new formula: (IMPLIES (AND (LISTP X) (NOT (EQUAL (SUB1 (LENGTH (CDR X))) 0)) (NOT (LISTP (CDR X)))) 1), which again simplifies, clearly, to: T. Case 2. (IMPLIES (AND (LISTP X) (REV3-COST (CDR X)) (EQUAL (SUB1 (LENGTH X)) 0)) (REV3-COST X)). This simplifies, applying the lemmas SUB1-ADD1, LENGTH-0, and REV3-COST-OPENER, and expanding the definition of LENGTH, to: (IMPLIES (AND (LISTP X) (REV3-COST (CDR X)) (NOT (LISTP (CDR X)))) 1), which again simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (EQUAL (SUB1 (LENGTH X)) 0)) (REV3-COST X)). This simplifies, rewriting with CDR-NLISTP and REV3-COST-OPENER, and expanding the definitions of LENGTH, SUB1, EQUAL, and LISTP, to: (IMPLIES (NOT (LISTP X)) 1). This again simplifies, clearly, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] REV3-LENGTH-AND-DEFINEDNESS-LEMMA (PROVE-LEMMA REV3-DEFINED (REWRITE) (REV3-COST X) ((USE (REV3-LENGTH-AND-DEFINEDNESS-LEMMA (N (LENGTH X)))))) This simplifies, expanding the definitions of AND and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REV3-DEFINED (DISABLE REV3-COST-OPENER) [ 0.0 0.0 0.0 ] REV3-COST-OPENER-OFF (PROVE-LEMMA APP-ASSOC (REWRITE) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z)))) 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 (AND (LISTP X) (p (CDR X) Y Z)) (p X Y Z)) (IMPLIES (NOT (LISTP X)) (p X Y Z))). Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (AND (LISTP X) (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) (APPEND Y Z)))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z)))), which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up the definition of APPEND, to: T. Case 1. (IMPLIES (NOT (LISTP X)) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z)))), which simplifies, unfolding the function APPEND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] APP-ASSOC (PROVE-LEMMA REV-REV (REWRITE) (IMPLIES (PLISTP X) (EQUAL (REV (REV X)) X))) Give the conjecture the name *1. 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 (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP 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 three new conjectures: Case 3. (IMPLIES (AND (LISTP X) (NOT (PLISTP (CDR X))) (PLISTP X)) (EQUAL (REV (REV X)) X)), which simplifies, expanding the function PLISTP, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (REV (REV (CDR X))) (CDR X)) (PLISTP X)) (EQUAL (REV (REV X)) X)), which simplifies, opening up the functions PLISTP and REV, to: (IMPLIES (AND (LISTP X) (EQUAL (REV (REV (CDR X))) (CDR X)) (PLISTP (CDR X))) (EQUAL (REV (APPEND (REV (CDR X)) (LIST (CAR X)))) X)). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). The result is the goal: (IMPLIES (AND (EQUAL (REV (REV Z)) Z) (PLISTP Z)) (EQUAL (REV (APPEND (REV Z) (LIST V))) (CONS V Z))). We use the above equality hypothesis by cross-fertilizing (REV (REV Z)) for Z and throwing away the equality. We thus obtain: (IMPLIES (PLISTP Z) (EQUAL (REV (APPEND (REV Z) (LIST V))) (CONS V (REV (REV Z))))), which we generalize by replacing (REV Z) by Y. We must thus prove: (IMPLIES (PLISTP Z) (EQUAL (REV (APPEND Y (LIST V))) (CONS V (REV Y)))). Eliminate the irrelevant term. We thus obtain: (EQUAL (REV (APPEND Y (LIST V))) (CONS V (REV Y))), which we will finally name *1.1. Case 1. (IMPLIES (AND (NOT (LISTP X)) (PLISTP X)) (EQUAL (REV (REV X)) X)). This simplifies, expanding the functions PLISTP, REV, and EQUAL, to: T. So next consider: (EQUAL (REV (APPEND Y (LIST V))) (CONS V (REV Y))), named *1.1 above. Perhaps we can prove it by induction. 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 (AND (LISTP Y) (p (CDR Y) V)) (p Y V)) (IMPLIES (NOT (LISTP Y)) (p Y V))). Linear arithmetic and the lemma CDR-LESSP 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 two new formulas: Case 2. (IMPLIES (AND (LISTP Y) (EQUAL (REV (APPEND (CDR Y) (LIST V))) (CONS V (REV (CDR Y))))) (EQUAL (REV (APPEND Y (LIST V))) (CONS V (REV Y)))). This simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the functions APPEND and REV, to: T. Case 1. (IMPLIES (NOT (LISTP Y)) (EQUAL (REV (APPEND Y (LIST V))) (CONS V (REV Y)))), which simplifies, applying CAR-CONS and CDR-CONS, and unfolding the definitions of APPEND, LISTP, and REV, 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 ] REV-REV (PROVE-LEMMA PLISTP-REV (REWRITE) (PLISTP (REV X))) Call the conjecture *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP 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 two new goals: Case 2. (IMPLIES (AND (LISTP X) (PLISTP (REV (CDR X)))) (PLISTP (REV X))), which simplifies, expanding the definition of REV, to the conjecture: (IMPLIES (AND (LISTP X) (PLISTP (REV (CDR X)))) (PLISTP (APPEND (REV (CDR X)) (LIST (CAR X))))). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). This generates: (IMPLIES (PLISTP (REV Z)) (PLISTP (APPEND (REV Z) (LIST V)))). We will try to prove the above formula by generalizing it, replacing (REV Z) by Y. The result is: (IMPLIES (PLISTP Y) (PLISTP (APPEND Y (LIST V)))). Give the above formula the name *1.1. Case 1. (IMPLIES (NOT (LISTP X)) (PLISTP (REV X))). This simplifies, expanding REV and PLISTP, to: T. So let us turn our attention to: (IMPLIES (PLISTP Y) (PLISTP (APPEND Y (LIST V)))), named *1.1 above. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP Y) (p (CDR Y) V)) (p Y V)) (IMPLIES (NOT (LISTP Y)) (p Y V))). Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT Y) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following three new conjectures: Case 3. (IMPLIES (AND (LISTP Y) (NOT (PLISTP (CDR Y))) (PLISTP Y)) (PLISTP (APPEND Y (LIST V)))). This simplifies, expanding PLISTP, to: T. Case 2. (IMPLIES (AND (LISTP Y) (PLISTP (APPEND (CDR Y) (LIST V))) (PLISTP Y)) (PLISTP (APPEND Y (LIST V)))). This simplifies, applying CDR-CONS, and unfolding PLISTP and APPEND, to: T. Case 1. (IMPLIES (AND (NOT (LISTP Y)) (PLISTP Y)) (PLISTP (APPEND Y (LIST V)))), which simplifies, applying CDR-CONS, and opening up PLISTP, LISTP, and APPEND, to: T. That finishes the proof of *1.1, which, consequently, also finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PLISTP-REV (PROVE-LEMMA PLISTP-APPEND (REWRITE) (EQUAL (PLISTP (APPEND X Y)) (PLISTP Y))) Call the conjecture *1. We will try to prove it by induction. The recursive terms in the conjecture suggest two inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X) Y)) (p X Y)) (IMPLIES (NOT (LISTP X)) (p X Y))). Linear arithmetic and the lemma CDR-LESSP 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 (AND (LISTP X) (EQUAL (PLISTP (APPEND (CDR X) Y)) (PLISTP Y))) (EQUAL (PLISTP (APPEND X Y)) (PLISTP Y))). This simplifies, applying CDR-CONS, and expanding the functions APPEND and PLISTP, to: T. Case 1. (IMPLIES (NOT (LISTP X)) (EQUAL (PLISTP (APPEND X Y)) (PLISTP Y))), which simplifies, opening up the function APPEND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PLISTP-APPEND (PROVE-LEMMA PLISTP-CDR (REWRITE) (IMPLIES (AND (PLISTP X) (LISTP X)) (PLISTP (CDR X)))) This formula simplifies, expanding the function PLISTP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLISTP-CDR (PROVE-LEMMA LISTP-APPEND (REWRITE) (EQUAL (LISTP (APPEND X Y)) (OR (LISTP X) (LISTP Y)))) This simplifies, unfolding the definition of OR, to the following two new goals: Case 2. (IMPLIES (NOT (LISTP X)) (EQUAL (LISTP (APPEND X Y)) (LISTP Y))). This again simplifies, opening up the definition of APPEND, to: T. Case 1. (IMPLIES (LISTP X) (EQUAL (LISTP (APPEND X Y)) T)), which again simplifies, trivially, to: (IMPLIES (LISTP X) (LISTP (APPEND X Y))), which we will name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X) Y)) (p X Y)) (IMPLIES (NOT (LISTP X)) (p X Y))). Linear arithmetic and the lemma CDR-LESSP 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 goals: Case 2. (IMPLIES (AND (NOT (LISTP (CDR X))) (LISTP X)) (LISTP (APPEND X Y))). This simplifies, opening up the function APPEND, to: T. Case 1. (IMPLIES (AND (LISTP (APPEND (CDR X) Y)) (LISTP X)) (LISTP (APPEND X Y))). This simplifies, unfolding the definition of APPEND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LISTP-APPEND (PROVE-LEMMA REV-PROP NIL (IMPLIES (PLISTP X) (EQUAL (REV X) (IF (LISTP (CDR X)) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))) X)))) This formula simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the definitions of PLISTP, REV, CDR, LISTP, and EQUAL, to the following two new conjectures: Case 2. (IMPLIES (AND (LISTP X) (PLISTP (CDR X)) (NOT (LISTP (CDR X)))) (EQUAL (APPEND (REV (CDR X)) (LIST (CAR X))) X)). This again simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the definitions of PLISTP, LISTP, REV, APPEND, and EQUAL, to: T. Case 1. (IMPLIES (AND (LISTP X) (PLISTP (CDR X)) (LISTP (CDR X))) (EQUAL (APPEND (REV (CDR X)) (LIST (CAR X))) (CONS (CAR (REV (CDR X))) (APPEND (REV (REV (CDR (REV (CDR X))))) (LIST (CAR X)))))). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to eliminate (CDR X) and (CAR X). We must thus prove: (IMPLIES (AND (PLISTP Z) (LISTP Z)) (EQUAL (APPEND (REV Z) (LIST V)) (CONS (CAR (REV Z)) (APPEND (REV (REV (CDR (REV Z)))) (LIST V))))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (IMPLIES (PLISTP X) (EQUAL (REV X) (IF (LISTP (CDR X)) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))) X))). We gave this the name *1 above. Perhaps we can prove it by induction. 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 (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following three new goals: Case 3. (IMPLIES (AND (LISTP X) (NOT (PLISTP (CDR X))) (PLISTP X)) (EQUAL (REV X) (IF (LISTP (CDR X)) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))) X))). This simplifies, unfolding the function PLISTP, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (REV (CDR X)) (IF (LISTP (CDDR X)) (CONS (CAR (REV (CDDR X))) (REV (CONS (CADR X) (REV (CDR (REV (CDDR X))))))) (CDR X))) (PLISTP X)) (EQUAL (REV X) (IF (LISTP (CDR X)) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))) X))). This simplifies, appealing to the lemmas CAR-CONS, CDR-CONS, REV-REV, PLISTP-REV, and PLISTP-CDR, and opening up the functions REV, PLISTP, APPEND, and LISTP, to the following four new formulas: Case 2.4. (IMPLIES (AND (LISTP X) (NOT (LISTP (CDDR X))) (EQUAL (REV (CDR X)) (CDR X)) (PLISTP (CDR X)) (NOT (LISTP (CDR X)))) (EQUAL (APPEND (CDR X) (LIST (CAR X))) X)). But this again simplifies, appealing to the lemmas CDR-NLISTP, CAR-CONS, and CDR-CONS, and opening up the definitions of LISTP, APPEND, and UNPACK, to: (IMPLIES (AND (LISTP X) (EQUAL (REV (CDR X)) (CDR X)) (PLISTP (CDR X)) (NOT (LISTP (CDR X)))) (EQUAL (LIST (CAR X)) X)). This further simplifies, appealing to the lemmas CAR-CONS and CDR-CONS, and unfolding REV, PLISTP, LISTP, and EQUAL, to: T. Case 2.3. (IMPLIES (AND (LISTP X) (NOT (LISTP (CDDR X))) (EQUAL (REV (CDR X)) (CDR X)) (PLISTP (CDR X)) (LISTP (CDR X))) (EQUAL (APPEND (CDR X) (LIST (CAR X))) (LIST (CADR X) (CAR X)))), which further simplifies, rewriting with the lemmas CAR-CONS and CDR-CONS, and expanding the functions REV, LISTP, APPEND, and PLISTP, to: T. Case 2.2. (IMPLIES (AND (LISTP X) (LISTP (CDDR X)) (EQUAL (REV (CDR X)) (CONS (CAR (REV (CDDR X))) (APPEND (REV (REV (CDR (REV (CDDR X))))) (LIST (CADR X))))) (PLISTP (CDR X)) (NOT (LISTP (CDR X)))) (EQUAL (APPEND (REV (CDR X)) (LIST (CAR X))) X)), which again simplifies, applying the lemma CDR-NLISTP, and opening up the definition of LISTP, to: T. Case 2.1. (IMPLIES (AND (LISTP X) (LISTP (CDDR X)) (EQUAL (REV (CDR X)) (CONS (CAR (REV (CDDR X))) (APPEND (REV (REV (CDR (REV (CDDR X))))) (LIST (CADR X))))) (PLISTP (CDR X)) (LISTP (CDR X))) (EQUAL (APPEND (REV (CDR X)) (LIST (CAR X))) (CONS (CAR (REV (CDR X))) (APPEND (CDR (REV (CDR X))) (LIST (CAR X)))))), which again simplifies, unfolding the function APPEND, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (PLISTP X)) (EQUAL (REV X) (IF (LISTP (CDR X)) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))) X))), which simplifies, opening up the functions PLISTP, REV, CDR, LISTP, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] REV-PROP (PROVE-LEMMA REV-PROP-REWRITE (REWRITE) (IMPLIES (PLISTP X) (AND (IMPLIES (LISTP (CDR X)) (EQUAL (REV X) (CONS (CAR (REV (CDR X))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X))))))))) (IMPLIES (NLISTP (CDR X)) (EQUAL (REV X) X)))) ((USE (REV-PROP)))) WARNING: Note that the proposed lemma REV-PROP-REWRITE is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This simplifies, applying PLISTP-CDR, CAR-CONS, CDR-CONS, and CONS-EQUAL, and opening up the definitions of PLISTP, REV, IMPLIES, CDR, LISTP, CAR, CONS, EQUAL, NLISTP, AND, and APPEND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REV-PROP-REWRITE (DISABLE REV) [ 0.0 0.0 0.0 ] REV-OFF (PROVE-LEMMA LISTP-REV (REWRITE) (EQUAL (LISTP (REV X)) (LISTP X)) ((EXPAND (REV X)))) This formula simplifies, unfolding the definition of REV, to the following two new goals: Case 2. (IMPLIES (NOT (LISTP X)) (EQUAL (LISTP NIL) (LISTP X))). This again simplifies, obviously, to: T. Case 1. (IMPLIES (LISTP X) (EQUAL (LISTP (APPEND (REV (CDR X)) (LIST (CAR X)))) (LISTP X))). This again simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LISTP-REV (PROVE-LEMMA LENGTH-REV3 (REWRITE) (EQUAL (LENGTH (REV3 X)) (LENGTH X)) ((USE (REV3-LENGTH-AND-DEFINEDNESS-LEMMA (N (LENGTH X)))))) This formula simplifies, expanding the definitions of AND and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-REV3 (PROVE-LEMMA REV3-NIL (REWRITE) (EQUAL (EQUAL (REV3 X) NIL) (EQUAL X NIL)) ((USE (REV3-DEFN)))) This simplifies, rewriting with REV3-DEFINED and REV3-DEFN-OPENER, to the new formula: (IMPLIES (AND (LISTP (CDR X)) (EQUAL (REV3 X) (CONS (CAR (REV3 (CDR X))) (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))))) (NOT (EQUAL X NIL))), which again simplifies, expanding the functions CDR and LISTP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REV3-NIL (PROVE-LEMMA LENGTH-CDR-REV3 (REWRITE) (IMPLIES (LISTP X) (EQUAL (LENGTH (CDR (REV3 X))) (SUB1 (LENGTH X)))) ((USE (REV3-LENGTH-AND-DEFINEDNESS-LEMMA (N (LENGTH X)))) (DISABLE LENGTH-REV3))) This formula simplifies, rewriting with CDR-NLISTP, and opening up the definitions of LENGTH, AND, IMPLIES, SUB1, and EQUAL, to: (IMPLIES (AND (REV3-COST X) (LISTP (REV3 X)) (EQUAL (ADD1 (LENGTH (CDR (REV3 X)))) (LENGTH X)) (LISTP X)) (EQUAL (LENGTH (CDR (REV3 X))) (SUB1 (LENGTH X)))), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (EQUAL (LENGTH X) 0) (REV3-COST X) (LISTP (REV3 X)) (EQUAL (ADD1 (LENGTH (CDR (REV3 X)))) (LENGTH X)) (LISTP X)) (EQUAL (LENGTH (CDR (REV3 X))) (SUB1 (LENGTH X)))). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-CDR-REV3 (PROVE-LEMMA REV3-REV-LEMMA NIL (IMPLIES (AND (PLISTP X) (EQUAL (LENGTH X) N)) (EQUAL (REV3 X) (REV X))) ((INDUCT (REV3-INDUCTION X N)))) This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to two new conjectures: Case 2. (IMPLIES (AND (OR (ZEROP N) (ZEROP (SUB1 N))) (PLISTP X) (EQUAL (LENGTH X) N)) (EQUAL (REV3 X) (REV X))), which simplifies, rewriting with LENGTH-0 and REV3-DEFN-OPENER, and unfolding the functions ZEROP, OR, PLISTP, LISTP, CDR, REV, and EQUAL, to: (IMPLIES (AND (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))), which we will name *1. Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL (SUB1 N) 0)) (NUMBERP (SUB1 N)) (IMPLIES (AND (PLISTP (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (LENGTH (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (SUB1 N))) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (REV (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))))) (IMPLIES (AND (PLISTP (CDR (REV3 (CDR X)))) (EQUAL (LENGTH (CDR (REV3 (CDR X)))) (SUB1 (SUB1 N)))) (EQUAL (REV3 (CDR (REV3 (CDR X)))) (REV (CDR (REV3 (CDR X)))))) (IMPLIES (AND (PLISTP (CDR X)) (EQUAL (LENGTH (CDR X)) (SUB1 N))) (EQUAL (REV3 (CDR X)) (REV (CDR X)))) (PLISTP X) (EQUAL (LENGTH X) N)) (EQUAL (REV3 X) (REV X))). This simplifies, applying SUB1-ADD1, LENGTH-0, CDR-CONS, LENGTH-CDR-REV3, LENGTH-REV3, ADD1-SUB1, PLISTP-CDR, REV3-DEFINED, REV3-DEFN-OPENER, REV-PROP-REWRITE, CAR-CONS, and CONS-EQUAL, and unfolding the functions LENGTH, PLISTP, AND, and IMPLIES, to four new formulas: Case 1.4. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (PLISTP (REV3 (CDR (REV3 (CDR X)))))) (NOT (PLISTP (CDR (REV3 (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))), which again simplifies, appealing to the lemmas LISTP-REV, PLISTP-REV, and PLISTP-CDR, to: T. Case 1.3. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (NOT (PLISTP (REV3 (CDR (REV3 (CDR X)))))) (EQUAL (REV3 (CDR (REV3 (CDR X)))) (REV (CDR (REV3 (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))), which again simplifies, trivially, to: (IMPLIES (AND (LISTP X) (LISTP (CDR X)) (NOT (PLISTP (REV3 (CDR (REV (CDR X)))))) (EQUAL (REV3 (CDR (REV (CDR X)))) (REV (CDR (REV (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))), which again simplifies, applying PLISTP-REV, to: T. Case 1.2. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (REV (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (NOT (PLISTP (CDR (REV3 (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))). But this again simplifies, applying LISTP-REV, PLISTP-REV, and PLISTP-CDR, to: T. Case 1.1. (IMPLIES (AND (LISTP X) (NOT (EQUAL (ADD1 (LENGTH (CDR X))) 0)) (LISTP (CDR X)) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV3 (CDR X)))))) (REV (CONS (CAR X) (REV3 (CDR (REV3 (CDR X))))))) (EQUAL (REV3 (CDR (REV3 (CDR X)))) (REV (CDR (REV3 (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))). This again simplifies, clearly, to the new conjecture: (IMPLIES (AND (LISTP X) (LISTP (CDR X)) (EQUAL (REV3 (CONS (CAR X) (REV3 (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV3 (CDR (REV (CDR X))))))) (EQUAL (REV3 (CDR (REV (CDR X)))) (REV (CDR (REV (CDR X))))) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (PLISTP (CDR X))) (EQUAL (REV3 (CONS (CAR X) (REV (CDR (REV (CDR X)))))) (REV (CONS (CAR X) (REV (CDR (REV (CDR X)))))))), which again simplifies, trivially, to: T. So next consider: (IMPLIES (AND (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))), which is formula *1 above. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP X) (p (CDR X))) (p X)) (IMPLIES (NOT (LISTP X)) (p X))). Linear arithmetic and the lemma CDR-LESSP 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 the following four new formulas: Case 4. (IMPLIES (AND (LISTP X) (NOT (EQUAL (SUB1 (LENGTH (CDR X))) 0)) (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))). This simplifies, rewriting with the lemmas SUB1-ADD1, LENGTH-0, REV3-DEFN-OPENER, and REV-PROP-REWRITE, and opening up the functions LENGTH and PLISTP, to: T. Case 3. (IMPLIES (AND (LISTP X) (NOT (PLISTP (CDR X))) (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))). This simplifies, rewriting with SUB1-ADD1 and LENGTH-0, and unfolding the functions LENGTH and PLISTP, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (REV3 (CDR X)) (REV (CDR X))) (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))), which simplifies, appealing to the lemmas SUB1-ADD1, LENGTH-0, REV3-DEFN-OPENER, and REV-PROP-REWRITE, and unfolding the definitions of LENGTH and PLISTP, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (EQUAL (SUB1 (LENGTH X)) 0) (PLISTP X)) (EQUAL (REV3 X) (REV X))), which simplifies, rewriting with REV3-DEFN-OPENER, and opening up LENGTH, SUB1, EQUAL, PLISTP, LISTP, CDR, and REV, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.1 ] REV3-REV-LEMMA (PROVE-LEMMA REV3-REV (REWRITE) (IMPLIES (PLISTP X) (EQUAL (REV3 X) (REV X))) ((USE (REV3-REV-LEMMA (N (LENGTH X)))))) This simplifies, applying PLISTP-CDR, and unfolding the functions PLISTP, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REV3-REV