(BOOT-STRAP NQTHM) [ 0.0 0.1 0.0 ] GROUND-ZERO (ADD-SHELL CONS-SEQ-FIRST EMPTY-SEQ SEQ-P ((FIRST (NONE-OF) EMPTY-SEQ) (FINAL (ONE-OF SEQ-P) EMPTY-SEQ))) [ 0.0 0.0 0.0 ] CONS-SEQ-FIRST (DEFN EMPTY-SEQ-P (S) (OR (EQUAL S (EMPTY-SEQ)) (NOT (SEQ-P S)))) Note that (OR (FALSEP (EMPTY-SEQ-P S)) (TRUEP (EMPTY-SEQ-P S))) is a theorem. [ 0.0 0.0 0.0 ] EMPTY-SEQ-P (DEFN COERCE-SEQ (S) (IF (SEQ-P S) S (EMPTY-SEQ))) Observe that (SEQ-P (COERCE-SEQ S)) is a theorem. [ 0.0 0.0 0.0 ] COERCE-SEQ (DEFN CONS-SEQ-LAST (S C) (IF (EMPTY-SEQ-P S) (CONS-SEQ-FIRST C S) (CONS-SEQ-FIRST (FIRST S) (CONS-SEQ-LAST (FINAL S) C)))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to show that the measure (COUNT S) decreases according to the well-founded relation LESSP in each recursive call. Hence, CONS-SEQ-LAST is accepted under the definitional principle. From the definition we can conclude that (SEQ-P (CONS-SEQ-LAST S C)) is a theorem. [ 0.0 0.0 0.0 ] CONS-SEQ-LAST (DEFN INITIAL (S) (IF (EMPTY-SEQ-P S) (EMPTY-SEQ) (IF (EQUAL (FINAL S) (EMPTY-SEQ)) (EMPTY-SEQ) (CONS-SEQ-FIRST (FIRST S) (INITIAL (FINAL S)))))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S) decreases according to the well-founded relation LESSP in each recursive call. Hence, INITIAL is accepted under the principle of definition. Observe that (SEQ-P (INITIAL S)) is a theorem. [ 0.0 0.0 0.0 ] INITIAL (DEFN LAST (S) (IF (EMPTY-SEQ-P S) (EMPTY-SEQ) (IF (EQUAL (FINAL S) (EMPTY-SEQ)) (FIRST S) (LAST (FINAL S))))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S) decreases according to the well-founded relation LESSP in each recursive call. Hence, LAST is accepted under the principle of definition. [ 0.0 0.0 0.0 ] LAST (PROVE-LEMMA INITIAL-CONS-SEQ-LAST (REWRITE) (EQUAL (INITIAL (CONS-SEQ-LAST S C)) (IF (SEQ-P S) S (EMPTY-SEQ)))) This simplifies, trivially, to the following two new goals: Case 2. (IMPLIES (NOT (SEQ-P S)) (EQUAL (INITIAL (CONS-SEQ-LAST S C)) (EMPTY-SEQ))). This again simplifies, applying FINAL-TYPE-RESTRICTION and FINAL-CONS-SEQ-FIRST, and unfolding the functions EMPTY-SEQ-P, CONS-SEQ-LAST, EQUAL, SEQ-P, and INITIAL, to: T. Case 1. (IMPLIES (SEQ-P S) (EQUAL (INITIAL (CONS-SEQ-LAST S C)) S)). Call the above 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 (EMPTY-SEQ-P S) (p S C)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (p (FINAL S) C)) (p S C))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (SEQ-P S)) (EQUAL (INITIAL (CONS-SEQ-LAST S C)) S)), which simplifies, applying the lemma FINAL-CONS-SEQ-FIRST, and opening up the definitions of EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST, EQUAL, and INITIAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (INITIAL (CONS-SEQ-LAST (FINAL S) C)) (FINAL S)) (SEQ-P S)) (EQUAL (INITIAL (CONS-SEQ-LAST S C)) S)), which simplifies, rewriting with CONS-SEQ-FIRST-FIRST-FINAL, FIRST-CONS-SEQ-FIRST, and FINAL-CONS-SEQ-FIRST, and opening up the functions EMPTY-SEQ-P, CONS-SEQ-LAST, and INITIAL, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (EQUAL (INITIAL (CONS-SEQ-LAST (FINAL S) C)) (FINAL S)) (SEQ-P S)) (NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C) (EMPTY-SEQ)))), which again simplifies, unfolding the function INITIAL, to the goal: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (EQUAL (EMPTY-SEQ) (FINAL S)) (SEQ-P S)) (NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C) (EMPTY-SEQ)))). This again simplifies, opening up the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-CONS-SEQ-LAST (PROVE-LEMMA INITIAL-NSEQ-P (REWRITE) (IMPLIES (NOT (SEQ-P S)) (EQUAL (INITIAL S) (EMPTY-SEQ)))) This conjecture simplifies, unfolding EMPTY-SEQ-P, INITIAL, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-NSEQ-P (PROVE-LEMMA INITIAL-TYPE-RESTRICTION (REWRITE) (IMPLIES (NOT (SEQ-P S)) (EQUAL (CONS-SEQ-LAST S C) (CONS-SEQ-LAST (EMPTY-SEQ) C)))) This formula simplifies, applying FINAL-TYPE-RESTRICTION, and unfolding EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-TYPE-RESTRICTION (PROVE-LEMMA INITIAL-LESSP (REWRITE) (IMPLIES (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (INITIAL S)) (COUNT S)))) WARNING: Note that the proposed lemma INITIAL-LESSP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY-SEQ-P S) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (p (FINAL S))) (p S))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (INITIAL S)) (COUNT S))). This simplifies, opening up the definition of EMPTY-SEQ-P, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (INITIAL S)) (COUNT S))). This simplifies, expanding EMPTY-SEQ-P, INITIAL, EQUAL, COUNT, and LESSP, to: (IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (NOT (EQUAL (COUNT S) 0))). Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We employ the type restriction lemma noted when FINAL was introduced to restrict the new variables. This produces the new formula: (IMPLIES (AND (SEQ-P X) (EQUAL X (EMPTY-SEQ)) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ)))) (NOT (EQUAL (COUNT (CONS-SEQ-FIRST Z X)) 0))), which further simplifies, applying COUNT-CONS-SEQ-FIRST, and expanding the functions SEQ-P and COUNT, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (LESSP (COUNT (INITIAL (FINAL S))) (COUNT (FINAL S))) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (INITIAL S)) (COUNT S))). This simplifies, applying COUNT-CONS-SEQ-FIRST and SUB1-ADD1, and opening up EMPTY-SEQ-P, INITIAL, and LESSP, to two new conjectures: Case 1.2. (IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (LESSP (COUNT (INITIAL (FINAL S))) (COUNT (FINAL S))) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (NOT (EQUAL (COUNT S) 0))), which again simplifies, using linear arithmetic and applying FINAL-LESSEQP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (LESSP (COUNT (INITIAL (FINAL S))) (COUNT (FINAL S))) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (PLUS (COUNT (FIRST S)) (COUNT (INITIAL (FINAL S)))) (SUB1 (COUNT S)))). Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We rely upon the type restriction lemma noted when FINAL was introduced to constrain the new variables. We must thus prove: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL X (EMPTY-SEQ))) (LESSP (COUNT (INITIAL X)) (COUNT X)) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ)))) (LESSP (PLUS (COUNT Z) (COUNT (INITIAL X))) (SUB1 (COUNT (CONS-SEQ-FIRST Z X))))). This further simplifies, rewriting with the lemmas COUNT-CONS-SEQ-FIRST and SUB1-ADD1, to the goal: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL X (EMPTY-SEQ))) (LESSP (COUNT (INITIAL X)) (COUNT X))) (LESSP (PLUS (COUNT Z) (COUNT (INITIAL X))) (PLUS (COUNT Z) (COUNT X)))). However this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-LESSP (PROVE-LEMMA INITIAL-LESSEQP (REWRITE) (NOT (LESSP (COUNT S) (COUNT (INITIAL S))))) WARNING: Note that the proposed lemma INITIAL-LESSEQP 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 (EMPTY-SEQ-P S) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (p (FINAL S))) (p S))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (NOT (LESSP (COUNT S) (COUNT (INITIAL S))))). This simplifies, applying INITIAL-NSEQ-P, and unfolding the definitions of EMPTY-SEQ-P, COUNT, INITIAL, LESSP, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT S) (COUNT (INITIAL S))))), which simplifies, unfolding the definitions of EMPTY-SEQ-P, INITIAL, EQUAL, COUNT, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT (FINAL S)) (COUNT (INITIAL (FINAL S)))))) (NOT (LESSP (COUNT S) (COUNT (INITIAL S))))), which simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1, and expanding the definitions of EMPTY-SEQ-P, INITIAL, and LESSP, to the following two new goals: Case 1.2. (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT (FINAL S)) (COUNT (INITIAL (FINAL S)))))) (NOT (EQUAL (COUNT S) 0))). However this again simplifies, using linear arithmetic and applying FINAL-LESSEQP and INITIAL-LESSP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT (FINAL S)) (COUNT (INITIAL (FINAL S)))))) (NOT (LESSP (SUB1 (COUNT S)) (PLUS (COUNT (FIRST S)) (COUNT (INITIAL (FINAL S))))))). Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We use the type restriction lemma noted when FINAL was introduced to constrain the new variables. This generates: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ))) (NOT (EQUAL X (EMPTY-SEQ))) (NOT (LESSP (COUNT X) (COUNT (INITIAL X))))) (NOT (LESSP (SUB1 (COUNT (CONS-SEQ-FIRST Z X))) (PLUS (COUNT Z) (COUNT (INITIAL X)))))). This further simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1, to: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL X (EMPTY-SEQ))) (NOT (LESSP (COUNT X) (COUNT (INITIAL X))))) (NOT (LESSP (PLUS (COUNT Z) (COUNT X)) (PLUS (COUNT Z) (COUNT (INITIAL X)))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-LESSEQP (PROVE-LEMMA LAST-CONS-SEQ-LAST (REWRITE) (EQUAL (LAST (CONS-SEQ-LAST S C)) C)) Name 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 (EMPTY-SEQ-P S) (p S C)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (p (FINAL S) C)) (p S C))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (EQUAL (LAST (CONS-SEQ-LAST S C)) C)), which simplifies, applying FIRST-CONS-SEQ-FIRST, FINAL-CONS-SEQ-FIRST, and INITIAL-TYPE-RESTRICTION, and unfolding the functions EMPTY-SEQ-P, CONS-SEQ-LAST, EQUAL, SEQ-P, and LAST, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (LAST (CONS-SEQ-LAST (FINAL S) C)) C)) (EQUAL (LAST (CONS-SEQ-LAST S C)) C)). This simplifies, applying FIRST-CONS-SEQ-FIRST and FINAL-CONS-SEQ-FIRST, and opening up the definitions of EMPTY-SEQ-P, CONS-SEQ-LAST, and LAST, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (EQUAL (LAST (CONS-SEQ-LAST (FINAL S) C)) C) (EQUAL (CONS-SEQ-LAST (FINAL S) C) (EMPTY-SEQ))) (EQUAL (FIRST S) C)). However this again simplifies, unfolding LAST, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (EQUAL (EMPTY-SEQ) C) (EQUAL (CONS-SEQ-LAST (FINAL S) C) (EMPTY-SEQ))) (EQUAL (FIRST S) (EMPTY-SEQ))). This again simplifies, obviously, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (EQUAL (CONS-SEQ-LAST (FINAL S) (EMPTY-SEQ)) (EMPTY-SEQ))) (EQUAL (FIRST S) (EMPTY-SEQ))). Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We rely upon the type restriction lemma noted when FINAL was introduced to restrict the new variables. We would thus like to prove: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ))) (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ)) (EMPTY-SEQ))) (EQUAL Z (EMPTY-SEQ))), which further simplifies, clearly, to the new conjecture: (IMPLIES (AND (SEQ-P X) (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ)) (EMPTY-SEQ))) (EQUAL Z (EMPTY-SEQ))), which has an irrelevant term in it. By eliminating the term we get: (IMPLIES (SEQ-P X) (NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ)) (EMPTY-SEQ)))), which we will finally name *1.1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY-SEQ-P X) (p X)) (IMPLIES (AND (NOT (EMPTY-SEQ-P X)) (p (FINAL X))) (p X))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following two new goals: Case 2. (IMPLIES (AND (EMPTY-SEQ-P X) (SEQ-P X)) (NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ)) (EMPTY-SEQ)))). This simplifies, expanding the functions EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P X)) (NOT (EQUAL (CONS-SEQ-LAST (FINAL X) (EMPTY-SEQ)) (EMPTY-SEQ))) (SEQ-P X)) (NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ)) (EMPTY-SEQ)))). This simplifies, unfolding the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST, 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 ] LAST-CONS-SEQ-LAST (PROVE-LEMMA LAST-NSEQ-P (REWRITE) (IMPLIES (NOT (SEQ-P S)) (EQUAL (LAST S) (EMPTY-SEQ)))) This conjecture simplifies, unfolding EMPTY-SEQ-P, LAST, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LAST-NSEQ-P (PROVE-LEMMA LAST-LESSP (REWRITE) (IMPLIES (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (LAST S)) (COUNT S)))) WARNING: Note that the proposed lemma LAST-LESSP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY-SEQ-P S) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (p (FINAL S))) (p S))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (LAST S)) (COUNT S))). This simplifies, opening up the definition of EMPTY-SEQ-P, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (LAST S)) (COUNT S))). This simplifies, expanding EMPTY-SEQ-P, LAST, and EQUAL, to: (IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (FIRST S)) (COUNT S))), which again simplifies, using linear arithmetic and rewriting with FIRST-LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (LESSP (COUNT (LAST (FINAL S))) (COUNT (FINAL S))) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (LAST S)) (COUNT S))). This simplifies, opening up the functions EMPTY-SEQ-P and LAST, to: (IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (LESSP (COUNT (LAST (FINAL S))) (COUNT (FINAL S))) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (LESSP (COUNT (LAST (FINAL S))) (COUNT S))), which again simplifies, using linear arithmetic and applying FINAL-LESSEQP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LAST-LESSP (PROVE-LEMMA LAST-LESSEQP (REWRITE) (NOT (LESSP (COUNT S) (COUNT (LAST S))))) WARNING: Note that the proposed lemma LAST-LESSEQP 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 (EMPTY-SEQ-P S) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (p (FINAL S))) (p S))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (NOT (LESSP (COUNT S) (COUNT (LAST S))))). This simplifies, applying LAST-NSEQ-P, and unfolding the definitions of EMPTY-SEQ-P, COUNT, LAST, LESSP, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT S) (COUNT (LAST S))))), which simplifies, unfolding the definitions of EMPTY-SEQ-P, LAST, and EQUAL, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT S) (COUNT (FIRST S))))). However this again simplifies, using linear arithmetic and applying FIRST-LESSEQP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT (FINAL S)) (COUNT (LAST (FINAL S)))))) (NOT (LESSP (COUNT S) (COUNT (LAST S))))). This simplifies, unfolding EMPTY-SEQ-P and LAST, to: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (SEQ-P S) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (NOT (LESSP (COUNT (FINAL S)) (COUNT (LAST (FINAL S)))))) (NOT (LESSP (COUNT S) (COUNT (LAST (FINAL S)))))), which again simplifies, using linear arithmetic and appealing to the lemma FINAL-LESSEQP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.3 0.0 ] LAST-LESSEQP (PROVE-LEMMA INITIAL-APPLY-EQUALS NIL (IMPLIES (EQUAL X Y) (EQUAL (INITIAL X) (INITIAL Y)))) This conjecture simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-APPLY-EQUALS (PROVE-LEMMA LAST-APPLY-EQUALS NIL (IMPLIES (EQUAL X Y) (EQUAL (LAST X) (LAST Y)))) This conjecture simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LAST-APPLY-EQUALS (PROVE-LEMMA CONS-SEQ-LAST-EQUAL (REWRITE) (EQUAL (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2)) (AND (IF (SEQ-P S1) (IF (SEQ-P S2) (EQUAL S1 S2) (EQUAL S1 (EMPTY-SEQ))) (IF (SEQ-P S2) (EQUAL (EMPTY-SEQ) S2) T)) (EQUAL C1 C2))) ((USE (INITIAL-APPLY-EQUALS (X (CONS-SEQ-LAST S1 C1)) (Y (CONS-SEQ-LAST S2 C2))) (LAST-APPLY-EQUALS (X (CONS-SEQ-LAST S1 C1)) (Y (CONS-SEQ-LAST S2 C2)))))) This conjecture can be simplified, using the abbreviations AND and LAST-CONS-SEQ-LAST, to the formula: (IMPLIES (AND (IMPLIES (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2)) (EQUAL (INITIAL (CONS-SEQ-LAST S1 C1)) (INITIAL (CONS-SEQ-LAST S2 C2)))) (IMPLIES (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2)) (EQUAL C1 C2))) (EQUAL (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2)) (AND (COND ((SEQ-P S1) (IF (SEQ-P S2) (EQUAL S1 S2) (EQUAL S1 (EMPTY-SEQ)))) ((SEQ-P S2) (EQUAL (EMPTY-SEQ) S2)) (T T)) (EQUAL C1 C2)))). This simplifies, rewriting with INITIAL-CONS-SEQ-LAST, INITIAL-TYPE-RESTRICTION, and CONS-SEQ-FIRST-EQUAL, and opening up IMPLIES, AND, EQUAL, EMPTY-SEQ-P, CONS-SEQ-LAST, and SEQ-P, to five new formulas: Case 5. (IMPLIES (AND (SEQ-P S2) (SEQ-P S1) (EQUAL S1 S2) (NOT (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S1 C2)))) (NOT (EQUAL C1 C2))), which again simplifies, clearly, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2))) (NOT (SEQ-P S1)) (EQUAL (EMPTY-SEQ) S2)) (NOT (EQUAL C1 C2))). This again simplifies, rewriting with INITIAL-TYPE-RESTRICTION, and expanding EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2))) (SEQ-P S1) (SEQ-P S2) (EQUAL S1 S2)) (NOT (EQUAL C1 C2))). This again simplifies, clearly, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2))) (NOT (SEQ-P S2)) (EQUAL S1 (EMPTY-SEQ))) (NOT (EQUAL C1 C2))). However this again simplifies, applying INITIAL-TYPE-RESTRICTION, and unfolding EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1) (CONS-SEQ-LAST S2 C2))) (NOT (SEQ-P S1)) (NOT (SEQ-P S2))) (NOT (EQUAL C1 C2))). But this again simplifies, rewriting with INITIAL-TYPE-RESTRICTION, and unfolding the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. Q.E.D. [ 0.0 0.0 0.0 ] CONS-SEQ-LAST-EQUAL (PROVE-LEMMA CONS-SEQ-LAST-INITIAL-LAST (REWRITE) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) (IF (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) S (CONS-SEQ-LAST (EMPTY-SEQ) (EMPTY-SEQ))))) This formula simplifies, expanding the definitions of NOT, AND, and CONS-SEQ-LAST, to the following three new conjectures: Case 3. (IMPLIES (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S)). Give the above formula the name *1. Case 2. (IMPLIES (NOT (SEQ-P S)) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) (CONS-SEQ-FIRST (EMPTY-SEQ) (EMPTY-SEQ)))). However this again simplifies, applying INITIAL-NSEQ-P and LAST-NSEQ-P, and unfolding the functions CONS-SEQ-LAST and EQUAL, to: T. Case 1. (IMPLIES (EQUAL S (EMPTY-SEQ)) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) (CONS-SEQ-FIRST (EMPTY-SEQ) (EMPTY-SEQ)))). This again simplifies, opening up the definitions of INITIAL, LAST, CONS-SEQ-LAST, and EQUAL, to: T. So next consider: (IMPLIES (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S)), which we named *1 above. Let us appeal to the induction principle. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY-SEQ-P S) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ))) (p S)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (p (FINAL S))) (p S))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S)), which simplifies, opening up the function EMPTY-SEQ-P, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S)), which simplifies, opening up the definitions of EMPTY-SEQ-P, INITIAL, EQUAL, LAST, and CONS-SEQ-LAST, to the conjecture: (IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-FIRST (FIRST S) (EMPTY-SEQ)) S)). Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We rely upon the type restriction lemma noted when FINAL was introduced to constrain the new variables. We must thus prove: (IMPLIES (AND (SEQ-P X) (EQUAL X (EMPTY-SEQ)) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-FIRST Z (EMPTY-SEQ)) (CONS-SEQ-FIRST Z X))). This further simplifies, clearly, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (FINAL S) (EMPTY-SEQ))) (EQUAL (CONS-SEQ-LAST (INITIAL (FINAL S)) (LAST (FINAL S))) (FINAL S)) (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S)). This simplifies, rewriting with CONS-SEQ-FIRST-FIRST-FINAL, FINAL-CONS-SEQ-FIRST, and FIRST-CONS-SEQ-FIRST, and expanding the definitions of EMPTY-SEQ-P, INITIAL, LAST, and CONS-SEQ-LAST, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] CONS-SEQ-LAST-INITIAL-LAST (PROVE-LEMMA INITIAL-LAST-ELIM (ELIM) (IMPLIES (AND (SEQ-P S) (NOT (EQUAL S (EMPTY-SEQ)))) (EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S)) S))) This conjecture simplifies, applying CONS-SEQ-LAST-INITIAL-LAST, to: T. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-LAST-ELIM (PROVE-LEMMA COUNT-CONS-SEQ-LAST (REWRITE) (EQUAL (COUNT (CONS-SEQ-LAST S C)) (ADD1 (PLUS (IF (SEQ-P S) (COUNT S) 0) (COUNT C))))) This formula simplifies, trivially, to two new formulas: Case 2. (IMPLIES (NOT (SEQ-P S)) (EQUAL (COUNT (CONS-SEQ-LAST S C)) (ADD1 (PLUS 0 (COUNT C))))), which again simplifies, appealing to the lemmas INITIAL-TYPE-RESTRICTION, COUNT-CONS-SEQ-FIRST, and ADD1-EQUAL, and unfolding the functions EMPTY-SEQ-P, CONS-SEQ-LAST, SEQ-P, COUNT, EQUAL, and PLUS, to: (IMPLIES (NOT (SEQ-P S)) (EQUAL (PLUS (COUNT C) 0) (COUNT C))). This again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (SEQ-P S) (EQUAL (COUNT (CONS-SEQ-LAST S C)) (ADD1 (PLUS (COUNT S) (COUNT C))))), 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 (EMPTY-SEQ-P S) (p S C)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (p (FINAL S) C)) (p S C))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to show that the measure (COUNT S) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to two new formulas: Case 2. (IMPLIES (AND (EMPTY-SEQ-P S) (SEQ-P S)) (EQUAL (COUNT (CONS-SEQ-LAST S C)) (ADD1 (PLUS (COUNT S) (COUNT C))))), which simplifies, rewriting with COUNT-CONS-SEQ-FIRST and ADD1-EQUAL, and opening up EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST, COUNT, EQUAL, and PLUS, to: (IMPLIES (EQUAL S (EMPTY-SEQ)) (EQUAL (PLUS (COUNT C) 0) (COUNT C))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (EQUAL (COUNT (CONS-SEQ-LAST (FINAL S) C)) (ADD1 (PLUS (COUNT (FINAL S)) (COUNT C)))) (SEQ-P S)) (EQUAL (COUNT (CONS-SEQ-LAST S C)) (ADD1 (PLUS (COUNT S) (COUNT C))))), which simplifies, applying COUNT-CONS-SEQ-FIRST and ADD1-EQUAL, and opening up EMPTY-SEQ-P and CONS-SEQ-LAST, to the new conjecture: (IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ))) (EQUAL (COUNT (CONS-SEQ-LAST (FINAL S) C)) (ADD1 (PLUS (COUNT (FINAL S)) (COUNT C)))) (SEQ-P S)) (EQUAL (PLUS (COUNT (FIRST S)) (COUNT (CONS-SEQ-LAST (FINAL S) C))) (PLUS (COUNT S) (COUNT C)))). Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We use the type restriction lemma noted when FINAL was introduced to restrict the new variables. We would thus like to prove: (IMPLIES (AND (SEQ-P X) (NOT (EQUAL (CONS-SEQ-FIRST Z X) (EMPTY-SEQ))) (EQUAL (COUNT (CONS-SEQ-LAST X C)) (ADD1 (PLUS (COUNT X) (COUNT C))))) (EQUAL (PLUS (COUNT Z) (COUNT (CONS-SEQ-LAST X C))) (PLUS (COUNT (CONS-SEQ-FIRST Z X)) (COUNT C)))), which further simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1, and unfolding PLUS, to the new conjecture: (IMPLIES (AND (SEQ-P X) (EQUAL (COUNT (CONS-SEQ-LAST X C)) (ADD1 (PLUS (COUNT X) (COUNT C))))) (EQUAL (PLUS (COUNT Z) (COUNT (CONS-SEQ-LAST X C))) (ADD1 (PLUS (PLUS (COUNT Z) (COUNT X)) (COUNT C))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] COUNT-CONS-SEQ-LAST (PROVE-LEMMA CONS-SEQ-LAST-NOT-EMPTY-SEQ (REWRITE) (NOT (EQUAL (CONS-SEQ-LAST S C) (EMPTY-SEQ)))) Give the conjecture the name *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY-SEQ-P S) (p S C)) (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (p (FINAL S) C)) (p S C))). Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P establish that the measure (COUNT S) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new conjectures: Case 2. (IMPLIES (EMPTY-SEQ-P S) (NOT (EQUAL (CONS-SEQ-LAST S C) (EMPTY-SEQ)))), which simplifies, applying INITIAL-TYPE-RESTRICTION, and opening up EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S)) (NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C) (EMPTY-SEQ)))) (NOT (EQUAL (CONS-SEQ-LAST S C) (EMPTY-SEQ)))). This simplifies, opening up the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] CONS-SEQ-LAST-NOT-EMPTY-SEQ (DEFN REVERSE1 (S) (IF (EMPTY-SEQ-P S) S (CONS-SEQ-LAST (REVERSE1 (FINAL S)) (FIRST S)))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S) decreases according to the well-founded relation LESSP in each recursive call. Hence, REVERSE1 is accepted under the principle of definition. From the definition we can conclude that: (OR (SEQ-P (REVERSE1 S)) (EQUAL (REVERSE1 S) S)) is a theorem. [ 0.0 0.0 0.0 ] REVERSE1 (DEFN REVERSE2 (S) (IF (EMPTY-SEQ-P S) S (CONS-SEQ-FIRST (LAST S) (REVERSE2 (INITIAL S))))) Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S) decreases according to the well-founded relation LESSP in each recursive call. Hence, REVERSE2 is accepted under the principle of definition. From the definition we can conclude that: (OR (SEQ-P (REVERSE2 S)) (EQUAL (REVERSE2 S) S)) is a theorem. [ 0.0 0.0 0.0 ] REVERSE2 (DEFN CONCAT1 (S1 S2) (IF (EMPTY-SEQ-P S1) (COERCE-SEQ S2) (CONS-SEQ-FIRST (FIRST S1) (CONCAT1 (FINAL S1) S2)))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S1) decreases according to the well-founded relation LESSP in each recursive call. Hence, CONCAT1 is accepted under the definitional principle. Observe that (SEQ-P (CONCAT1 S1 S2)) is a theorem. [ 0.0 0.0 0.0 ] CONCAT1 (DEFN CONCAT2 (S1 S2) (IF (EMPTY-SEQ-P S2) (COERCE-SEQ S1) (CONCAT2 (CONS-SEQ-LAST S1 (FIRST S2)) (FINAL S2)))) Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S2) decreases according to the well-founded relation LESSP in each recursive call. Hence, CONCAT2 is accepted under the definitional principle. Observe that (SEQ-P (CONCAT2 S1 S2)) is a theorem. [ 0.0 0.0 0.0 ] CONCAT2 (DEFN CONCAT3 (S1 S2) (IF (EMPTY-SEQ-P S2) (COERCE-SEQ S1) (CONS-SEQ-LAST (CONCAT3 S1 (INITIAL S2)) (LAST S2)))) Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S2) decreases according to the well-founded relation LESSP in each recursive call. Hence, CONCAT3 is accepted under the definitional principle. Observe that (SEQ-P (CONCAT3 S1 S2)) is a theorem. [ 0.0 0.0 0.0 ] CONCAT3 (DEFN CONCAT4 (S1 S2) (IF (EMPTY-SEQ-P S1) (COERCE-SEQ S2) (CONCAT4 (INITIAL S1) (CONS-SEQ-FIRST (LAST S1) S2)))) Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the definition of EMPTY-SEQ-P inform us that the measure (COUNT S1) decreases according to the well-founded relation LESSP in each recursive call. Hence, CONCAT4 is accepted under the definitional principle. Observe that (SEQ-P (CONCAT4 S1 S2)) is a theorem. [ 0.0 0.0 0.0 ] CONCAT4