(BOOT-STRAP NQTHM) [ 0.0 0.1 0.0 ] GROUND-ZERO (DEFN ROTATE (N LST) (IF (ZEROP N) LST (ROTATE (SUB1 N) (APPEND (CDR LST) (LIST (CAR LST)))))) 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, ROTATE is accepted under the principle of definition. From the definition we can conclude that: (OR (LISTP (ROTATE N LST)) (EQUAL (ROTATE N LST) LST)) is a theorem. [ 0.0 0.0 0.0 ] ROTATE (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 (DEFN PROPERP (X) (IF (LISTP X) (PROPERP (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, PROPERP is accepted under the principle of definition. From the definition we can conclude that: (OR (FALSEP (PROPERP X)) (TRUEP (PROPERP X))) is a theorem. [ 0.0 0.0 0.0 ] PROPERP (DEFN FIRSTN (N LST) (IF (ZEROP N) NIL (CONS (CAR LST) (FIRSTN (SUB1 N) (CDR LST))))) 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, FIRSTN is accepted under the definitional principle. Note that: (OR (LITATOM (FIRSTN N LST)) (LISTP (FIRSTN N LST))) is a theorem. [ 0.0 0.0 0.0 ] FIRSTN (DEFN NTHCDR (N LST) (IF (ZEROP N) LST (NTHCDR (SUB1 N) (CDR LST)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, NTHCDR is accepted under the principle of definition. [ 0.0 0.0 0.0 ] NTHCDR (PROVE-LEMMA ASSOCIATIVITY-OF-APPEND (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 ] ASSOCIATIVITY-OF-APPEND (PROVE-LEMMA APPEND-NIL (REWRITE) (IMPLIES (PROPERP X) (EQUAL (APPEND X NIL) X))) Name the conjecture *1. 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 produces the following three new formulas: Case 3. (IMPLIES (AND (LISTP X) (NOT (PROPERP (CDR X))) (PROPERP X)) (EQUAL (APPEND X NIL) X)). This simplifies, expanding the definition of PROPERP, to: T. Case 2. (IMPLIES (AND (LISTP X) (EQUAL (APPEND (CDR X) NIL) (CDR X)) (PROPERP X)) (EQUAL (APPEND X NIL) X)). This simplifies, applying CONS-CAR-CDR, and expanding the definitions of PROPERP and APPEND, to: T. Case 1. (IMPLIES (AND (NOT (LISTP X)) (PROPERP X)) (EQUAL (APPEND X NIL) X)), which simplifies, opening up PROPERP, APPEND, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.2 0.0 ] APPEND-NIL (DEFN ROTATE-APPEND-INDUCTION (N LST EXTRA) (IF (OR (EQUAL N 0) (NOT (NUMBERP N))) T (IF (NLISTP LST) T (ROTATE-APPEND-INDUCTION (SUB1 N) (CDR LST) (APPEND EXTRA (LIST (CAR LST))))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of NLISTP, OR, and NOT establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, ROTATE-APPEND-INDUCTION is accepted under the principle of definition. The definition of ROTATE-APPEND-INDUCTION can be justified in another way. Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of NLISTP, OR, and NOT establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. From the definition we can conclude that (TRUEP (ROTATE-APPEND-INDUCTION N LST EXTRA)) is a theorem. [ 0.0 0.0 0.0 ] ROTATE-APPEND-INDUCTION (PROVE-LEMMA PROPERP-APPEND (REWRITE) (EQUAL (PROPERP (APPEND X Y)) (PROPERP 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 (PROPERP (APPEND (CDR X) Y)) (PROPERP Y))) (EQUAL (PROPERP (APPEND X Y)) (PROPERP Y))). This simplifies, applying CDR-CONS, and expanding the functions APPEND and PROPERP, to: T. Case 1. (IMPLIES (NOT (LISTP X)) (EQUAL (PROPERP (APPEND X Y)) (PROPERP 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 ] PROPERP-APPEND (PROVE-LEMMA ROTATE-APPEND NIL (IMPLIES (AND (PROPERP EXTRA) (NOT (LESSP (LENGTH LST) N))) (EQUAL (ROTATE N (APPEND LST EXTRA)) (APPEND (NTHCDR N LST) (APPEND EXTRA (FIRSTN N LST))))) ((INDUCT (ROTATE-APPEND-INDUCTION N LST EXTRA)))) This conjecture can be simplified, using the abbreviations NLISTP, IMPLIES, NOT, OR, AND, ASSOCIATIVITY-OF-APPEND, and PROPERP-APPEND, to three new formulas: Case 3. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N))) (PROPERP EXTRA) (NOT (LESSP (LENGTH LST) N))) (EQUAL (ROTATE N (APPEND LST EXTRA)) (APPEND (NTHCDR N LST) (APPEND EXTRA (FIRSTN N LST))))), which simplifies, rewriting with APPEND-NIL, and unfolding the definitions of NOT, OR, EQUAL, LESSP, ROTATE, NTHCDR, and FIRSTN, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (LISTP LST)) (PROPERP EXTRA) (NOT (LESSP (LENGTH LST) N))) (EQUAL (ROTATE N (APPEND LST EXTRA)) (APPEND (NTHCDR N LST) (APPEND EXTRA (FIRSTN N LST))))). This simplifies, opening up the definitions of LENGTH, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (LISTP LST) (IMPLIES (AND (PROPERP (LIST (CAR LST))) (NOT (LESSP (LENGTH (CDR LST)) (SUB1 N)))) (EQUAL (ROTATE (SUB1 N) (APPEND (CDR LST) (APPEND EXTRA (LIST (CAR LST))))) (APPEND (NTHCDR (SUB1 N) (CDR LST)) (APPEND EXTRA (APPEND (LIST (CAR LST)) (FIRSTN (SUB1 N) (CDR LST))))))) (PROPERP EXTRA) (NOT (LESSP (LENGTH LST) N))) (EQUAL (ROTATE N (APPEND LST EXTRA)) (APPEND (NTHCDR N LST) (APPEND EXTRA (FIRSTN N LST))))). This simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, SUB1-ADD1, and ASSOCIATIVITY-OF-APPEND, and opening up the definitions of PROPERP, NOT, AND, APPEND, LISTP, IMPLIES, LENGTH, LESSP, ROTATE, NTHCDR, and FIRSTN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ROTATE-APPEND (PROVE-LEMMA NTHCDR-LENGTH (REWRITE) (IMPLIES (PROPERP LST) (EQUAL (NTHCDR (LENGTH LST) LST) NIL))) Call the conjecture *1. 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 LST) (p (CDR LST))) (p LST)) (IMPLIES (NOT (LISTP LST)) (p LST))). Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to three new goals: Case 3. (IMPLIES (AND (LISTP LST) (NOT (PROPERP (CDR LST))) (PROPERP LST)) (EQUAL (NTHCDR (LENGTH LST) LST) NIL)), which simplifies, opening up the definition of PROPERP, to: T. Case 2. (IMPLIES (AND (LISTP LST) (EQUAL (NTHCDR (LENGTH (CDR LST)) (CDR LST)) NIL) (PROPERP LST)) (EQUAL (NTHCDR (LENGTH LST) LST) NIL)), which simplifies, applying SUB1-ADD1, and unfolding PROPERP, LENGTH, NTHCDR, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (LISTP LST)) (PROPERP LST)) (EQUAL (NTHCDR (LENGTH LST) LST) NIL)). This simplifies, expanding the functions PROPERP, LENGTH, NTHCDR, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] NTHCDR-LENGTH (PROVE-LEMMA FIRSTN-LENGTH (REWRITE) (IMPLIES (PROPERP LST) (EQUAL (FIRSTN (LENGTH LST) LST) LST))) Name the conjecture *1. 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 LST) (p (CDR LST))) (p LST)) (IMPLIES (NOT (LISTP LST)) (p LST))). Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following three new formulas: Case 3. (IMPLIES (AND (LISTP LST) (NOT (PROPERP (CDR LST))) (PROPERP LST)) (EQUAL (FIRSTN (LENGTH LST) LST) LST)). This simplifies, expanding the definition of PROPERP, to: T. Case 2. (IMPLIES (AND (LISTP LST) (EQUAL (FIRSTN (LENGTH (CDR LST)) (CDR LST)) (CDR LST)) (PROPERP LST)) (EQUAL (FIRSTN (LENGTH LST) LST) LST)). This simplifies, applying CONS-CAR-CDR and SUB1-ADD1, and expanding the definitions of PROPERP, LENGTH, and FIRSTN, to: T. Case 1. (IMPLIES (AND (NOT (LISTP LST)) (PROPERP LST)) (EQUAL (FIRSTN (LENGTH LST) LST) LST)), which simplifies, opening up PROPERP, LENGTH, FIRSTN, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] FIRSTN-LENGTH (PROVE-LEMMA ROTATE-LENGTH NIL (IMPLIES (PROPERP LST) (EQUAL (ROTATE (LENGTH LST) LST) LST)) ((USE (ROTATE-APPEND (EXTRA NIL) (N (LENGTH LST)))))) This conjecture simplifies, applying the lemmas APPEND-NIL, NTHCDR-LENGTH, and FIRSTN-LENGTH, and expanding the definitions of PROPERP, NOT, AND, LISTP, APPEND, and IMPLIES, to: (IMPLIES (AND (LESSP (LENGTH LST) (LENGTH LST)) (PROPERP LST)) (EQUAL (ROTATE (LENGTH LST) LST) LST)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ROTATE-LENGTH