(BOOT-STRAP NQTHM) Nqthm-1992 mods: (PC-NQTHM-1992) [ 0.1 0.1 0.0 ] GROUND-ZERO (CONSTRAIN P-NUM-INTRO (REWRITE) (IMPLIES (AND (NUMBERP X) (NUMBERP Y)) (AND (LESSP 0 (P-NUM X Y)) (NOT (LESSP (BOUND) (P-NUM X Y))) (EQUAL (P-NUM X Y) (P-NUM Y X)))) ((P-NUM (LAMBDA (X Y) 1)) (BOUND (LAMBDA NIL 2)))) WARNING: When the linear lemma P-NUM-INTRO is stored under (BOUND) it contains the free variables Y and X which will be chosen by instantiating the hypotheses (NUMBERP X) and (NUMBERP Y). WARNING: Note that the proposed lemma P-NUM-INTRO is to be stored as zero type prescription rules, zero compound recognizer rules, three linear rules, and one replacement rule. We will verify the consistency and the conservative nature of this constraint by attempting to prove: (IMPLIES (AND (NUMBERP X) (NUMBERP Y)) (AND (LESSP 0 1) (NOT (LESSP 2 1)) (EQUAL 1 1))). This formula simplifies, expanding the definitions of LESSP, NOT, EQUAL, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-NUM-INTRO (DISABLE P-NUM-INTRO) [ 0.0 0.0 0.0 ] P-NUM-INTRO-OFF (DEFN P (X Y) (P-NUM (FIX X) (FIX Y))) [ 0.0 0.0 0.0 ] P (PROVE-LEMMA P-INTRO (REWRITE) (AND (LESSP 0 (P X Y)) (NOT (LESSP (BOUND) (P X Y))) (EQUAL (P X Y) (P Y X))) ((USE (P-NUM-INTRO (X (FIX X)) (Y (FIX Y)))))) WARNING: Note that the linear lemma P-INTRO is being stored under the term (P X Y), which is unusual because P is a nonrecursive function symbol. WARNING: Note that the linear lemma P-INTRO is being stored under the term (P X Y), which is unusual because P is a nonrecursive function symbol. WARNING: Note that the rewrite rule P-INTRO will be stored so as to apply only to terms with the nonrecursive function symbol P. WARNING: Note that the proposed lemma P-INTRO is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and one replacement rule. This conjecture simplifies, unfolding FIX, AND, EQUAL, LESSP, NOT, IMPLIES, and P, to two new goals: Case 2. (IMPLIES (AND (NUMBERP Y) (NOT (NUMBERP X)) (NOT (EQUAL (P-NUM 0 Y) 0)) (NUMBERP (P-NUM 0 Y)) (NOT (LESSP (BOUND) (P-NUM 0 Y))) (EQUAL (P-NUM 0 Y) (P-NUM Y 0))) (NOT (EQUAL (P-NUM Y 0) 0))), which again simplifies, obviously, to: T. Case 1. (IMPLIES (AND (NUMBERP Y) (NOT (NUMBERP X)) (NOT (EQUAL (P-NUM 0 Y) 0)) (NUMBERP (P-NUM 0 Y)) (NOT (LESSP (BOUND) (P-NUM 0 Y))) (EQUAL (P-NUM 0 Y) (P-NUM Y 0))) (NOT (LESSP (BOUND) (P-NUM Y 0)))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-INTRO (DISABLE P) [ 0.0 0.0 0.0 ] P-OFF (DEFN PREHOM-SEQ-1 (A X) (IF (LISTP X) (AND (EQUAL (P (CAAR X) A) (CDAR X)) (PREHOM-SEQ-1 A (CDR X))) T)) 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, PREHOM-SEQ-1 is accepted under the definitional principle. Note that: (OR (FALSEP (PREHOM-SEQ-1 A X)) (TRUEP (PREHOM-SEQ-1 A X))) is a theorem. [ 0.0 0.0 0.0 ] PREHOM-SEQ-1 (DEFN PREHOM-SEQ (X) (IF (LISTP X) (IF (LISTP (CDR X)) (AND (LESSP (CAR (CADR X)) (CAR (CAR X))) (PREHOM-SEQ-1 (CAAR X) (CDR X)) (PREHOM-SEQ (CDR X))) T) T)) 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, PREHOM-SEQ is accepted under the principle of definition. From the definition we can conclude that: (OR (FALSEP (PREHOM-SEQ X)) (TRUEP (PREHOM-SEQ X))) is a theorem. [ 0.0 0.0 0.0 ] PREHOM-SEQ (DEFN-SK EXTENSIBLE (S) (FORALL ABOVE (EXISTS NEXT (AND (LESSP ABOVE NEXT) (PREHOM-SEQ-1 NEXT S))))) Adding the Skolem axiom: (AND (IMPLIES (AND (LESSP (ABOVE S) NEXT) (PREHOM-SEQ-1 NEXT S)) (EXTENSIBLE S)) (IMPLIES (NOT (AND (LESSP ABOVE (NEXT ABOVE S)) (PREHOM-SEQ-1 (NEXT ABOVE S) S))) (NOT (EXTENSIBLE S)))). As this is a DEFN-SK we can conclude that: (OR (TRUEP (EXTENSIBLE S)) (FALSEP (EXTENSIBLE S))) is a theorem. [ 0.0 0.0 0.0 ] EXTENSIBLE (PROVE-LEMMA EXTENSIBLE-SUFF (REWRITE) (IMPLIES (AND (LESSP (ABOVE S) NEXT) (PREHOM-SEQ-1 NEXT S)) (EXTENSIBLE S))) WARNING: Note that EXTENSIBLE-SUFF contains the free variable NEXT which will be chosen by instantiating the hypothesis (LESSP (ABOVE S) NEXT). WARNING: the previously added lemma, EXTENSIBLE, could be applied whenever the newly proposed EXTENSIBLE-SUFF could! This conjecture simplifies, unfolding EXTENSIBLE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXTENSIBLE-SUFF (PROVE-LEMMA EXTENSIBLE-NECC (REWRITE) (IMPLIES (NOT (AND (LESSP ABOVE (NEXT ABOVE S)) (PREHOM-SEQ-1 (NEXT ABOVE S) S))) (NOT (EXTENSIBLE S))) ((USE (EXTENSIBLE)) (DISABLE EXTENSIBLE))) WARNING: Note that EXTENSIBLE-NECC contains the free variable ABOVE which will be chosen by instantiating the hypothesis: (NOT (AND (LESSP ABOVE (NEXT ABOVE S)) (PREHOM-SEQ-1 (NEXT ABOVE S) S))). WARNING: the previously added lemma, EXTENSIBLE, could be applied whenever the newly proposed EXTENSIBLE-NECC could! This formula simplifies, unfolding AND, IMPLIES, and NOT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXTENSIBLE-NECC (DEFN ABOVE-ALL-AUX (A S N) (IF (ZEROP N) 0 (PLUS (ABOVE (CONS (CONS A N) S)) (ABOVE-ALL-AUX A S (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, ABOVE-ALL-AUX is accepted under the definitional principle. From the definition we can conclude that: (NUMBERP (ABOVE-ALL-AUX A S N)) is a theorem. [ 0.0 0.0 0.0 ] ABOVE-ALL-AUX (DEFN ABOVE-ALL (A S) (ABOVE-ALL-AUX A S (BOUND))) Note that (NUMBERP (ABOVE-ALL A S)) is a theorem. [ 0.0 0.0 0.0 ] ABOVE-ALL (PROVE-LEMMA LESSP-ABOVE-ALL-AUX (REWRITE) (IMPLIES (LESSP 0 N) (NOT (LESSP (ABOVE-ALL-AUX A S N) (ABOVE (CONS (CONS A N) S)))))) WARNING: Note that the proposed lemma LESSP-ABOVE-ALL-AUX is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula simplifies, opening up the definitions of EQUAL and LESSP, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (ABOVE-ALL-AUX A S N) (ABOVE (CONS (CONS A N) S))))), 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 (ZEROP N) (p A S N)) (IMPLIES (AND (NOT (ZEROP N)) (p A S (SUB1 N))) (p A S N))). 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 induction step of the scheme. The above induction scheme leads to the following three new formulas: Case 3. (IMPLIES (AND (ZEROP N) (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (ABOVE-ALL-AUX A S N) (ABOVE (CONS (CONS A N) S))))). This simplifies, unfolding the function ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (SUB1 N) 0) (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (ABOVE-ALL-AUX A S N) (ABOVE (CONS (CONS A N) S))))). This simplifies, unfolding the definitions of ZEROP and ABOVE-ALL-AUX, to: (IMPLIES (AND (EQUAL (SUB1 N) 0) (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A N) S)) (ABOVE-ALL-AUX A S (SUB1 N))) (ABOVE (CONS (CONS A N) S))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (NOT (LESSP (ABOVE-ALL-AUX A S (SUB1 N)) (ABOVE (CONS (CONS A (SUB1 N)) S)))) (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (ABOVE-ALL-AUX A S N) (ABOVE (CONS (CONS A N) S))))), which simplifies, unfolding the functions ZEROP and ABOVE-ALL-AUX, to: (IMPLIES (AND (NOT (LESSP (ABOVE-ALL-AUX A S (SUB1 N)) (ABOVE (CONS (CONS A (SUB1 N)) S)))) (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A N) S)) (ABOVE-ALL-AUX A S (SUB1 N))) (ABOVE (CONS (CONS A N) S))))). But this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-ABOVE-ALL-AUX (PROVE-LEMMA ABOVE-ALL-AUX-MONOTONE (REWRITE) (IMPLIES (NOT (LESSP BOUND N)) (NOT (LESSP (ABOVE-ALL-AUX A S BOUND) (ABOVE-ALL-AUX A S N)))) ((INDUCT (ABOVE-ALL-AUX A S BOUND)))) WARNING: When the linear lemma ABOVE-ALL-AUX-MONOTONE is stored under (ABOVE-ALL-AUX A S N) it contains the free variable BOUND which will be chosen by instantiating the hypothesis (NOT (LESSP BOUND N)). WARNING: When the linear lemma ABOVE-ALL-AUX-MONOTONE is stored under: (ABOVE-ALL-AUX A S BOUND) it contains the free variable N which will be chosen by instantiating the hypothesis (NOT (LESSP BOUND N)). WARNING: Note that the proposed lemma ABOVE-ALL-AUX-MONOTONE is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. 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 BOUND) (NOT (LESSP BOUND N))) (NOT (LESSP (ABOVE-ALL-AUX A S BOUND) (ABOVE-ALL-AUX A S N)))). This simplifies, expanding the functions ZEROP, EQUAL, LESSP, and ABOVE-ALL-AUX, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (IMPLIES (NOT (LESSP (SUB1 BOUND) N)) (NOT (LESSP (ABOVE-ALL-AUX A S (SUB1 BOUND)) (ABOVE-ALL-AUX A S N)))) (NOT (LESSP BOUND N))) (NOT (LESSP (ABOVE-ALL-AUX A S BOUND) (ABOVE-ALL-AUX A S N)))). This simplifies, expanding the definitions of NOT, IMPLIES, and ABOVE-ALL-AUX, to the following two new conjectures: Case 1.2. (IMPLIES (AND (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (LESSP (SUB1 BOUND) N) (NOT (LESSP BOUND N))) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND))) (ABOVE-ALL-AUX A S N)))). But this again simplifies, using linear arithmetic, to two new conjectures: Case 1.2.2. (IMPLIES (AND (NOT (NUMBERP N)) (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (LESSP (SUB1 BOUND) N) (NOT (LESSP BOUND N))) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND))) (ABOVE-ALL-AUX A S N)))), which again simplifies, unfolding LESSP, to: T. Case 1.2.1. (IMPLIES (AND (NUMBERP N) (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (LESSP (SUB1 BOUND) BOUND) (NOT (LESSP BOUND BOUND))) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND))) (ABOVE-ALL-AUX A S BOUND)))), which again simplifies, opening up LESSP and ABOVE-ALL-AUX, to the conjecture: (IMPLIES (AND (NUMBERP N) (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (LESSP (SUB1 BOUND) BOUND) (NOT (LESSP (SUB1 BOUND) (SUB1 BOUND)))) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND))) (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (NOT (LESSP (ABOVE-ALL-AUX A S (SUB1 BOUND)) (ABOVE-ALL-AUX A S N))) (NOT (LESSP BOUND N))) (NOT (LESSP (PLUS (ABOVE (CONS (CONS A BOUND) S)) (ABOVE-ALL-AUX A S (SUB1 BOUND))) (ABOVE-ALL-AUX A S N)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ABOVE-ALL-AUX-MONOTONE (PROVE-LEMMA LESSP-ABOVE-ALL-BOUND (REWRITE) (IMPLIES (AND (LESSP 0 N) (NOT (LESSP (BOUND) N))) (NOT (LESSP (ABOVE-ALL A S) (ABOVE (CONS (CONS A N) S)))))) WARNING: Note that the proposed lemma LESSP-ABOVE-ALL-BOUND is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and ABOVE-ALL, to: (IMPLIES (AND (LESSP 0 N) (NOT (LESSP (BOUND) N))) (NOT (LESSP (ABOVE-ALL-AUX A S (BOUND)) (ABOVE (CONS (CONS A N) S))))), which simplifies, using linear arithmetic and applying ABOVE-ALL-AUX-MONOTONE and LESSP-ABOVE-ALL-AUX, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-ABOVE-ALL-BOUND (DEFN NEXT-ELEMENT (A S) (NEXT (ABOVE-ALL A S) S)) [ 0.0 0.0 0.0 ] NEXT-ELEMENT (DEFN NEXT-COLOR (A S) (P A (NEXT-ELEMENT A S))) [ 0.0 0.0 0.0 ] NEXT-COLOR (PROVE-LEMMA NUMBERP-P (REWRITE) (NUMBERP (P X Y)) ((USE (P-INTRO)))) WARNING: Note that the proposed lemma NUMBERP-P is to be stored as one type prescription rule, zero compound recognizer rules, zero linear rules, and zero replacement rules. This simplifies, using linear arithmetic and rewriting with the lemma P-INTRO, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NUMBERP-P (PROVE-LEMMA NEXT-COLOR-BOUND (REWRITE) (AND (LESSP 0 (NEXT-COLOR A S)) (NOT (LESSP (BOUND) (NEXT-COLOR A S))))) WARNING: Note that the linear lemma NEXT-COLOR-BOUND is being stored under the term (NEXT-COLOR A S), which is unusual because NEXT-COLOR is a nonrecursive function symbol. WARNING: Note that the linear lemma NEXT-COLOR-BOUND is being stored under the term (NEXT-COLOR A S), which is unusual because NEXT-COLOR is a nonrecursive function symbol. WARNING: Note that the proposed lemma NEXT-COLOR-BOUND is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. This conjecture can be simplified, using the abbreviations NOT and AND, to two new formulas: Case 2. (LESSP 0 (NEXT-COLOR A S)), which simplifies, expanding NEXT-ELEMENT, ABOVE-ALL, NEXT-COLOR, EQUAL, and LESSP, to: (NOT (EQUAL (P A (NEXT (ABOVE-ALL-AUX A S (BOUND)) S)) 0)). But this again simplifies, using linear arithmetic and applying the lemma P-INTRO, to: T. Case 1. (NOT (LESSP (BOUND) (NEXT-COLOR A S))), which simplifies, opening up the definitions of NEXT-ELEMENT, ABOVE-ALL, and NEXT-COLOR, to: (NOT (LESSP (BOUND) (P A (NEXT (ABOVE-ALL-AUX A S (BOUND)) S)))). However this again simplifies, using linear arithmetic and applying P-INTRO, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NEXT-COLOR-BOUND (DISABLE ABOVE-ALL) [ 0.0 0.0 0.0 ] ABOVE-ALL-OFF (PROVE-LEMMA LESSP-NEXT-ELEMENT (REWRITE) (IMPLIES (EXTENSIBLE S) (LESSP (ABOVE (CONS (CONS A (NEXT-COLOR A S)) S)) (NEXT-ELEMENT A S))) ((USE (EXTENSIBLE-NECC (ABOVE (ABOVE-ALL A S)))))) WARNING: Note that the proposed lemma LESSP-NEXT-ELEMENT is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture simplifies, unfolding the functions AND, NOT, IMPLIES, NEXT-ELEMENT, and NEXT-COLOR, to: (IMPLIES (AND (LESSP (ABOVE-ALL A S) (NEXT (ABOVE-ALL A S) S)) (PREHOM-SEQ-1 (NEXT (ABOVE-ALL A S) S) S) (EXTENSIBLE S)) (LESSP (ABOVE (CONS (CONS A (P A (NEXT (ABOVE-ALL A S) S))) S)) (NEXT (ABOVE-ALL A S) S))), which again simplifies, using linear arithmetic and applying LESSP-ABOVE-ALL-BOUND and P-INTRO, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-NEXT-ELEMENT (PROVE-LEMMA PREHOM-SEQ-1-NEXT-ELEMENT (REWRITE) (IMPLIES (EXTENSIBLE S) (PREHOM-SEQ-1 (NEXT-ELEMENT A S) S)) ((USE (EXTENSIBLE-NECC (ABOVE (ABOVE-ALL A S)))))) This conjecture simplifies, opening up AND, NOT, IMPLIES, and NEXT-ELEMENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PREHOM-SEQ-1-NEXT-ELEMENT (DISABLE NEXT-ELEMENT) [ 0.0 0.0 0.0 ] NEXT-ELEMENT-OFF (PROVE-LEMMA PREHOM-SEQ-1-NEXT-ELEMENT-CONS (REWRITE) (IMPLIES (EXTENSIBLE S) (PREHOM-SEQ-1 (NEXT-ELEMENT A S) (CONS (CONS A (NEXT-COLOR A S)) S)))) This formula simplifies, applying PREHOM-SEQ-1-NEXT-ELEMENT, CDR-CONS, and CAR-CONS, and unfolding NEXT-COLOR and PREHOM-SEQ-1, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PREHOM-SEQ-1-NEXT-ELEMENT-CONS (DISABLE NEXT-COLOR) [ 0.0 0.0 0.0 ] NEXT-COLOR-OFF (PROVE-LEMMA EXTENSIBLE-CONS (REWRITE) (IMPLIES (EXTENSIBLE S) (EXTENSIBLE (CONS (CONS A (NEXT-COLOR A S)) S))) ((USE (EXTENSIBLE-SUFF (NEXT (NEXT-ELEMENT A S)) (S (CONS (CONS A (NEXT-COLOR A S)) S)))))) This simplifies, applying PREHOM-SEQ-1-NEXT-ELEMENT-CONS, and opening up the functions AND and IMPLIES, to: (IMPLIES (AND (NOT (LESSP (ABOVE (CONS (CONS A (NEXT-COLOR A S)) S)) (NEXT-ELEMENT A S))) (EXTENSIBLE S)) (EXTENSIBLE (CONS (CONS A (NEXT-COLOR A S)) S))). This again simplifies, using linear arithmetic and rewriting with LESSP-NEXT-ELEMENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXTENSIBLE-CONS (DEFN NEXT-PAIR (S) (CONS (NEXT (CAAR S) S) (NEXT-COLOR (NEXT (CAAR S) S) S))) From the definition we can conclude that (LISTP (NEXT-PAIR S)) is a theorem. [ 0.0 0.0 0.0 ] NEXT-PAIR (PROVE-LEMMA NEXT-PAIR-EXTENDS (REWRITE) (IMPLIES (EXTENSIBLE S) (EXTENSIBLE (CONS (NEXT-PAIR S) S)))) This formula simplifies, applying the lemma EXTENSIBLE-CONS, and expanding the definition of NEXT-PAIR, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NEXT-PAIR-EXTENDS (DEFN RAMSEY-SEQ-P (S) (AND (EXTENSIBLE S) (PREHOM-SEQ S))) Observe that (OR (FALSEP (RAMSEY-SEQ-P S)) (TRUEP (RAMSEY-SEQ-P S))) is a theorem. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-P (PROVE-LEMMA EXTENSIBLE-NEXT-PROPERTY (REWRITE) (IMPLIES (EXTENSIBLE S) (AND (LESSP A (NEXT A S)) (PREHOM-SEQ-1 (NEXT A S) S)))) WARNING: Note that the proposed lemma EXTENSIBLE-NEXT-PROPERTY is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and one replacement rule. This formula simplifies, applying EXTENSIBLE-NECC, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXTENSIBLE-NEXT-PROPERTY (PROVE-LEMMA RAMSEY-SEQ-P-EXTENDS (REWRITE) (IMPLIES (RAMSEY-SEQ-P S) (RAMSEY-SEQ-P (CONS (NEXT-PAIR S) S)))) WARNING: Note that the rewrite rule RAMSEY-SEQ-P-EXTENDS will be stored so as to apply only to terms with the nonrecursive function symbol RAMSEY-SEQ-P. This conjecture can be simplified, using the abbreviations RAMSEY-SEQ-P and IMPLIES, to the conjecture: (IMPLIES (AND (EXTENSIBLE S) (PREHOM-SEQ S)) (RAMSEY-SEQ-P (CONS (NEXT-PAIR S) S))). This simplifies, applying CDR-CONS, CAR-CONS, EXTENSIBLE-NEXT-PROPERTY, and EXTENSIBLE-CONS, and unfolding the definitions of NEXT-PAIR, PREHOM-SEQ, and RAMSEY-SEQ-P, to: (IMPLIES (AND (EXTENSIBLE S) (PREHOM-SEQ S) (LISTP S)) (LESSP (CAAR S) (NEXT (CAAR S) S))). However this again simplifies, using linear arithmetic and appealing to the lemma EXTENSIBLE-NEXT-PROPERTY, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-P-EXTENDS (PROVE-LEMMA EXTENSIBLE-NLISTP (REWRITE) (IMPLIES (NOT (LISTP S)) (EXTENSIBLE S)) ((USE (EXTENSIBLE (NEXT (ADD1 (ABOVE S))))))) This conjecture simplifies, rewriting with SUB1-ADD1, and unfolding LESSP, PREHOM-SEQ-1, AND, IMPLIES, and NOT, to the new goal: (IMPLIES (AND (NOT (EQUAL (ABOVE S) 0)) (NUMBERP (ABOVE S)) (NOT (LESSP (SUB1 (ABOVE S)) (ABOVE S))) (NOT (LISTP S))) (EXTENSIBLE S)), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EXTENSIBLE-NLISTP (PROVE-LEMMA RAMSEY-SEQ-P-NLISTP (REWRITE) (IMPLIES (NLISTP S) (RAMSEY-SEQ-P S))) WARNING: Note that the rewrite rule RAMSEY-SEQ-P-NLISTP will be stored so as to apply only to terms with the nonrecursive function symbol RAMSEY-SEQ-P. This formula can be simplified, using the abbreviations NLISTP and IMPLIES, to: (IMPLIES (NOT (LISTP S)) (RAMSEY-SEQ-P S)), which simplifies, applying the lemma EXTENSIBLE-NLISTP, and opening up the definitions of PREHOM-SEQ and RAMSEY-SEQ-P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-P-NLISTP (DISABLE RAMSEY-SEQ-P) [ 0.0 0.0 0.0 ] RAMSEY-SEQ-P-OFF (DISABLE NEXT-PAIR) [ 0.0 0.0 0.0 ] NEXT-PAIR-OFF (DEFN RAMSEY-SEQ (N) (IF (ZEROP N) NIL (CONS (NEXT-PAIR (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (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, RAMSEY-SEQ is accepted under the definitional principle. Note that: (OR (LITATOM (RAMSEY-SEQ N)) (LISTP (RAMSEY-SEQ N))) is a theorem. [ 0.0 0.0 0.0 ] RAMSEY-SEQ (PROVE-LEMMA RAMSEY-SEQ-HAS-RAMSEY-SEQ-P (REWRITE) (RAMSEY-SEQ-P (RAMSEY-SEQ N))) 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 (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p N))). 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 induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP N) (RAMSEY-SEQ-P (RAMSEY-SEQ N))), which simplifies, applying RAMSEY-SEQ-P-NLISTP, and expanding the functions ZEROP and RAMSEY-SEQ, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (RAMSEY-SEQ-P (RAMSEY-SEQ (SUB1 N)))) (RAMSEY-SEQ-P (RAMSEY-SEQ N))). This simplifies, applying RAMSEY-SEQ-P-EXTENDS, and unfolding the functions ZEROP and RAMSEY-SEQ, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-HAS-RAMSEY-SEQ-P (DEFN-SK GOOD-COLOR-P (C) (FORALL BIG (EXISTS GOOD-C-INDEX (AND (LESSP BIG GOOD-C-INDEX) (EQUAL C (CDR (CAR (RAMSEY-SEQ GOOD-C-INDEX)))))))) Adding the Skolem axiom: (AND (IMPLIES (AND (LESSP (BIG C) GOOD-C-INDEX) (EQUAL C (CDAR (RAMSEY-SEQ GOOD-C-INDEX)))) (GOOD-COLOR-P C)) (IMPLIES (NOT (AND (LESSP BIG (GOOD-C-INDEX BIG C)) (EQUAL C (CDAR (RAMSEY-SEQ (GOOD-C-INDEX BIG C)))))) (NOT (GOOD-COLOR-P C)))). As this is a DEFN-SK we can conclude that: (OR (TRUEP (GOOD-COLOR-P C)) (FALSEP (GOOD-COLOR-P C))) is a theorem. [ 0.0 0.0 0.0 ] GOOD-COLOR-P (PROVE-LEMMA GOOD-COLOR-P-SUFF (REWRITE) (IMPLIES (AND (LESSP (BIG C) GOOD-C-INDEX) (EQUAL C (CDAR (RAMSEY-SEQ GOOD-C-INDEX)))) (GOOD-COLOR-P C))) WARNING: Note that GOOD-COLOR-P-SUFF contains the free variable GOOD-C-INDEX which will be chosen by instantiating the hypothesis: (LESSP (BIG C) GOOD-C-INDEX). WARNING: the previously added lemma, GOOD-COLOR-P, could be applied whenever the newly proposed GOOD-COLOR-P-SUFF could! This conjecture simplifies, unfolding the definition of GOOD-COLOR-P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GOOD-COLOR-P-SUFF (PROVE-LEMMA GOOD-COLOR-P-NECC (REWRITE) (IMPLIES (NOT (AND (LESSP BIG (GOOD-C-INDEX BIG C)) (EQUAL C (CDAR (RAMSEY-SEQ (GOOD-C-INDEX BIG C)))))) (NOT (GOOD-COLOR-P C))) ((USE (GOOD-COLOR-P)) (DISABLE GOOD-COLOR-P))) WARNING: Note that GOOD-COLOR-P-NECC contains the free variable BIG which will be chosen by instantiating the hypothesis: (NOT (AND (LESSP BIG (GOOD-C-INDEX BIG C)) (EQUAL C (CDAR (RAMSEY-SEQ (GOOD-C-INDEX BIG C)))))). WARNING: the previously added lemma, GOOD-COLOR-P, could be applied whenever the newly proposed GOOD-COLOR-P-NECC could! This conjecture simplifies, expanding the functions AND, IMPLIES, and NOT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GOOD-COLOR-P-NECC (DEFN GOOD-C-INDEX-WIT (BOUND) (IF (ZEROP BOUND) 1 (PLUS (BIG BOUND) (GOOD-C-INDEX-WIT (SUB1 BOUND))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT BOUND) decreases according to the well-founded relation LESSP in each recursive call. Hence, GOOD-C-INDEX-WIT is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (GOOD-C-INDEX-WIT BOUND)) is a theorem. [ 0.0 0.0 0.0 ] GOOD-C-INDEX-WIT (PROVE-LEMMA GOOD-C-INDEX-WIT-POSITIVE (REWRITE) (LESSP 0 (GOOD-C-INDEX-WIT BOUND))) WARNING: Note that the proposed lemma GOOD-C-INDEX-WIT-POSITIVE is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, expanding the functions EQUAL and LESSP, to: (NOT (EQUAL (GOOD-C-INDEX-WIT BOUND) 0)), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP BOUND) (p BOUND)) (IMPLIES (AND (NOT (ZEROP BOUND)) (p (SUB1 BOUND))) (p BOUND))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT BOUND) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (ZEROP BOUND) (NOT (EQUAL (GOOD-C-INDEX-WIT BOUND) 0))). This simplifies, expanding ZEROP, GOOD-C-INDEX-WIT, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP BOUND)) (NOT (EQUAL (GOOD-C-INDEX-WIT (SUB1 BOUND)) 0))) (NOT (EQUAL (GOOD-C-INDEX-WIT BOUND) 0))). This simplifies, unfolding the functions ZEROP and GOOD-C-INDEX-WIT, to the new formula: (IMPLIES (AND (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (NOT (EQUAL (GOOD-C-INDEX-WIT (SUB1 BOUND)) 0))) (NOT (EQUAL (PLUS (BIG BOUND) (GOOD-C-INDEX-WIT (SUB1 BOUND))) 0))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] GOOD-C-INDEX-WIT-POSITIVE (PROVE-LEMMA LESSP-BIG-GOOD-C-INDEX (REWRITE) (IMPLIES (AND (LESSP 0 C) (NOT (LESSP BOUND C))) (EQUAL (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND)) T))) This formula simplifies, unfolding the functions EQUAL and LESSP, to: (IMPLIES (AND (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND))). 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 (ZEROP BOUND) (p C BOUND)) (IMPLIES (AND (NOT (ZEROP BOUND)) (p C (SUB1 BOUND))) (p C BOUND))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT BOUND) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following three new formulas: Case 3. (IMPLIES (AND (ZEROP BOUND) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND))). This simplifies, expanding the functions ZEROP, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP BOUND)) (LESSP (SUB1 BOUND) C) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND))). This simplifies, using linear arithmetic, to the following two new goals: Case 2.2. (IMPLIES (AND (NOT (NUMBERP BOUND)) (NOT (ZEROP BOUND)) (LESSP (SUB1 BOUND) C) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND))). However this again simplifies, unfolding the function ZEROP, to: T. Case 2.1. (IMPLIES (AND (NUMBERP BOUND) (NOT (ZEROP BOUND)) (LESSP (SUB1 BOUND) BOUND) (NOT (EQUAL BOUND 0)) (NOT (LESSP BOUND BOUND))) (LESSP (BIG BOUND) (GOOD-C-INDEX-WIT BOUND))), which again simplifies, unfolding the functions ZEROP, LESSP, and GOOD-C-INDEX-WIT, to the formula: (IMPLIES (AND (NUMBERP BOUND) (LESSP (SUB1 BOUND) BOUND) (NOT (EQUAL BOUND 0)) (NOT (LESSP (SUB1 BOUND) (SUB1 BOUND)))) (LESSP (BIG BOUND) (PLUS (BIG BOUND) (GOOD-C-INDEX-WIT (SUB1 BOUND))))). But this again simplifies, using linear arithmetic and applying GOOD-C-INDEX-WIT-POSITIVE, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP BOUND)) (LESSP (BIG C) (GOOD-C-INDEX-WIT (SUB1 BOUND))) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (GOOD-C-INDEX-WIT BOUND))). This simplifies, opening up the definitions of ZEROP and GOOD-C-INDEX-WIT, to the new conjecture: (IMPLIES (AND (NOT (EQUAL BOUND 0)) (NUMBERP BOUND) (LESSP (BIG C) (GOOD-C-INDEX-WIT (SUB1 BOUND))) (NOT (EQUAL C 0)) (NUMBERP C) (NOT (LESSP BOUND C))) (LESSP (BIG C) (PLUS (BIG BOUND) (GOOD-C-INDEX-WIT (SUB1 BOUND))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.1 ] LESSP-BIG-GOOD-C-INDEX (DISABLE GOOD-C-INDEX-WIT) [ 0.0 0.0 0.0 ] GOOD-C-INDEX-WIT-OFF (DEFN COLOR NIL (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND))))) [ 0.0 0.0 0.0 ] COLOR (PROVE-LEMMA RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS (REWRITE) (IMPLIES (LESSP 0 N) (AND (LESSP 0 (CDAR (RAMSEY-SEQ N))) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N)))))) ((ENABLE NEXT-PAIR NEXT-COLOR))) WARNING: Note that the proposed lemma RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. This formula simplifies, unfolding the functions EQUAL, LESSP, NOT, and AND, to three new goals: Case 3. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (EQUAL (CDAR (RAMSEY-SEQ N)) 0))), which we will name *1. Case 2. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NUMBERP (CDAR (RAMSEY-SEQ N)))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (AND (IMPLIES (LESSP 0 N) (LESSP 0 (CDAR (RAMSEY-SEQ N)))) (IMPLIES (LESSP 0 N) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N)))))), which we named *1 above. We will appeal to induction. The recursive terms in the conjecture suggest four inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N))) (p N)) (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (p N)) (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (p (SUB1 N))) (p N))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT can be used to prove that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces eight new conjectures: Case 8. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N))) (LESSP 0 N)) (LESSP 0 (CDAR (RAMSEY-SEQ N)))), which simplifies, opening up the functions NOT, OR, and LESSP, to: T. Case 7. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (OR (EQUAL 0 0) (NOT (NUMBERP 0))) (LESSP 0 N)) (LESSP 0 (CDAR (RAMSEY-SEQ N)))), which simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the definitions of NOT, OR, EQUAL, NUMBERP, LESSP, RAMSEY-SEQ, NEXT-COLOR, and NEXT-PAIR, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (EQUAL (P (NEXT (CAAR (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N))) (NEXT-ELEMENT (NEXT (CAAR (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N)))) 0))), which again simplifies, using linear arithmetic and appealing to the lemma P-INTRO, to: T. Case 6. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 N))) (LESSP 0 N)) (LESSP 0 (CDAR (RAMSEY-SEQ N)))), which simplifies, using linear arithmetic, to two new conjectures: Case 6.2. (IMPLIES (AND (NOT (NUMBERP N)) (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 N))) (LESSP 0 N)) (LESSP 0 (CDAR (RAMSEY-SEQ N)))), which again simplifies, opening up NOT and OR, to: T. Case 6.1. (IMPLIES (AND (NUMBERP N) (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 1))) (LESSP 0 1)) (LESSP 0 (CDAR (RAMSEY-SEQ 1)))), which again simplifies, opening up the definitions of EQUAL, NUMBERP, NOT, and OR, to: T. Case 5. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (LESSP 0 (CDAR (RAMSEY-SEQ (SUB1 N)))) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ (SUB1 N))))) (LESSP 0 N)) (LESSP 0 (CDAR (RAMSEY-SEQ N)))), which simplifies, expanding the definitions of NOT, OR, EQUAL, and NUMBERP, to: T. Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N))) (LESSP 0 N)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N))))), which simplifies, expanding the functions NOT, OR, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (OR (EQUAL 0 0) (NOT (NUMBERP 0))) (LESSP 0 N)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N))))), which simplifies, rewriting with CAR-CONS and CDR-CONS, and unfolding NOT, OR, EQUAL, NUMBERP, LESSP, RAMSEY-SEQ, NEXT-COLOR, and NEXT-PAIR, to the new conjecture: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (LESSP (BOUND) (P (NEXT (CAAR (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N))) (NEXT-ELEMENT (NEXT (CAAR (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N))) (RAMSEY-SEQ (SUB1 N))))))), which again simplifies, using linear arithmetic and rewriting with the lemma P-INTRO, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 N))) (LESSP 0 N)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N))))), which simplifies, using linear arithmetic, to two new formulas: Case 2.2. (IMPLIES (AND (NOT (NUMBERP N)) (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 N))) (LESSP 0 N)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N))))), which again simplifies, expanding NOT and OR, to: T. Case 2.1. (IMPLIES (AND (NUMBERP N) (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 1))) (LESSP 0 1)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ 1))))), which again simplifies, expanding the functions EQUAL, NUMBERP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (LESSP 0 (CDAR (RAMSEY-SEQ (SUB1 N)))) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ (SUB1 N))))) (LESSP 0 N)) (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ N))))), which simplifies, unfolding the definitions of NOT, OR, EQUAL, and NUMBERP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS (PROVE-LEMMA COLOR-IN-BOUNDS (REWRITE) (AND (LESSP 0 (COLOR)) (NOT (LESSP (BOUND) (COLOR))))) WARNING: Note that the linear lemma COLOR-IN-BOUNDS is being stored under the term (COLOR), which is unusual because COLOR is a nonrecursive function symbol. WARNING: Note that the linear lemma COLOR-IN-BOUNDS is being stored under the term (COLOR), which is unusual because COLOR is a nonrecursive function symbol. WARNING: Note that the proposed lemma COLOR-IN-BOUNDS is to be stored as zero type prescription rules, zero compound recognizer rules, three linear rules, and zero replacement rules. This conjecture can be simplified, using the abbreviations NOT, AND, and COLOR, to two new formulas: Case 2. (LESSP 0 (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND))))), which simplifies, using linear arithmetic and rewriting with RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS and GOOD-C-INDEX-WIT-POSITIVE, to: T. Case 1. (NOT (LESSP (BOUND) (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND)))))). This simplifies, using linear arithmetic and rewriting with RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS and GOOD-C-INDEX-WIT-POSITIVE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COLOR-IN-BOUNDS (PROVE-LEMMA COLOR-IS-GOOD (REWRITE) (GOOD-COLOR-P (COLOR)) ((USE (GOOD-COLOR-P-SUFF (GOOD-C-INDEX (GOOD-C-INDEX-WIT (BOUND))) (C (COLOR)))))) This conjecture can be simplified, using the abbreviation COLOR, to: (IMPLIES (IMPLIES (AND (LESSP (BIG (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND))))) (GOOD-C-INDEX-WIT (BOUND))) (EQUAL (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND)))) (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND)))))) (GOOD-COLOR-P (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND)))))) (GOOD-COLOR-P (CDAR (RAMSEY-SEQ (GOOD-C-INDEX-WIT (BOUND)))))). This simplifies, using linear arithmetic, rewriting with GOOD-C-INDEX-WIT-POSITIVE, RAMSEY-SEQ-HAS-COLORS-IN-BOUNDS, and LESSP-BIG-GOOD-C-INDEX, and expanding the definitions of AND and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COLOR-IS-GOOD (DISABLE COLOR) [ 0.0 0.0 0.0 ] COLOR-OFF (DISABLE *1*COLOR) [ 0.0 0.0 0.0 ] G*1*COLOR-OFF (DEFN RAMSEY-INDEX (N) (IF (ZEROP N) (GOOD-C-INDEX 0 (COLOR)) (GOOD-C-INDEX (RAMSEY-INDEX (SUB1 N)) (COLOR)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, RAMSEY-INDEX is accepted under the definitional principle. [ 0.0 0.0 0.0 ] RAMSEY-INDEX (PROVE-LEMMA COLOR-PROPERTIES (REWRITE) (AND (LESSP BIG (GOOD-C-INDEX BIG (COLOR))) (EQUAL (CDR (CAR (RAMSEY-SEQ (GOOD-C-INDEX BIG (COLOR))))) (COLOR))) ((USE (GOOD-COLOR-P-NECC (C (COLOR)))) (DISABLE GOOD-COLOR-P-NECC))) WARNING: Note that the proposed lemma COLOR-PROPERTIES is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and one replacement rule. This formula simplifies, applying COLOR-IS-GOOD, and opening up the definitions of AND, NOT, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] COLOR-PROPERTIES (PROVE-LEMMA RAMSEY-INDEX-INCREASING (REWRITE) (IMPLIES (LESSP I J) (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX J))) ((INDUCT (PLUS J Q)))) WARNING: When the linear lemma RAMSEY-INDEX-INCREASING is stored under (RAMSEY-INDEX J) it contains the free variable I which will be chosen by instantiating the hypothesis (LESSP I J). WARNING: When the linear lemma RAMSEY-INDEX-INCREASING is stored under (RAMSEY-INDEX I) it contains the free variable J which will be chosen by instantiating the hypothesis (LESSP I J). WARNING: Note that the proposed lemma RAMSEY-INDEX-INCREASING is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. 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 J) (LESSP I J)) (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX J))). This simplifies, expanding the functions ZEROP, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (IMPLIES (LESSP I (SUB1 J)) (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX (SUB1 J)))) (LESSP I J)) (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX J))). This simplifies, opening up the definitions of IMPLIES and RAMSEY-INDEX, to the following two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I (SUB1 J))) (LESSP I J)) (LESSP (RAMSEY-INDEX I) (GOOD-C-INDEX (RAMSEY-INDEX (SUB1 J)) (COLOR)))). But this again simplifies, using linear arithmetic, to: (IMPLIES (AND (NOT (EQUAL (PLUS 1 I) 0)) (NUMBERP (PLUS 1 I)) (NOT (LESSP I (SUB1 (PLUS 1 I)))) (LESSP I (PLUS 1 I))) (LESSP (RAMSEY-INDEX I) (GOOD-C-INDEX (RAMSEY-INDEX (SUB1 (PLUS 1 I))) (COLOR)))). This again simplifies, applying SUB1-ADD1, and expanding the functions SUB1, NUMBERP, EQUAL, PLUS, ADD1, LESSP, and RAMSEY-INDEX, to the following three new conjectures: Case 1.2.3. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (LESSP I 0))) (LESSP (GOOD-C-INDEX 0 (COLOR)) (GOOD-C-INDEX (GOOD-C-INDEX 0 (COLOR)) (COLOR)))). But this again simplifies, using linear arithmetic and rewriting with COLOR-PROPERTIES, to: T. Case 1.2.2. (IMPLIES (AND (NUMBERP I) (NOT (LESSP I I)) (EQUAL I 0)) (LESSP (GOOD-C-INDEX 0 (COLOR)) (GOOD-C-INDEX (GOOD-C-INDEX 0 (COLOR)) (COLOR)))). This again simplifies, using linear arithmetic and rewriting with the lemma COLOR-PROPERTIES, to: T. Case 1.2.1. (IMPLIES (AND (NUMBERP I) (NOT (LESSP I I)) (LESSP (SUB1 I) I)) (LESSP (RAMSEY-INDEX I) (GOOD-C-INDEX (RAMSEY-INDEX I) (COLOR)))), which again simplifies, using linear arithmetic and applying COLOR-PROPERTIES, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX (SUB1 J))) (LESSP I J)) (LESSP (RAMSEY-INDEX I) (GOOD-C-INDEX (RAMSEY-INDEX (SUB1 J)) (COLOR)))). However this again simplifies, using linear arithmetic and applying COLOR-PROPERTIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-INDEX-INCREASING (DEFN RAMSEY (N) (CAR (CAR (RAMSEY-SEQ (RAMSEY-INDEX N))))) [ 0.0 0.0 0.0 ] RAMSEY (PROVE-LEMMA GOOD-C-INDEX-NUMBERP (REWRITE) (NUMBERP (GOOD-C-INDEX BIG (COLOR))) ((USE (COLOR-PROPERTIES)) (DISABLE COLOR-PROPERTIES))) This conjecture simplifies, opening up LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GOOD-C-INDEX-NUMBERP (PROVE-LEMMA RAMSEY-INDEX-NUMBERP (REWRITE) (NUMBERP (RAMSEY-INDEX N))) WARNING: Note that the proposed lemma RAMSEY-INDEX-NUMBERP is to be stored as one type prescription rule, zero compound recognizer rules, zero linear rules, and zero replacement rules. 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 (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p N))). 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 induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP N) (NUMBERP (RAMSEY-INDEX N))), which simplifies, applying GOOD-C-INDEX-NUMBERP, and expanding the functions ZEROP, EQUAL, and RAMSEY-INDEX, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (NUMBERP (RAMSEY-INDEX (SUB1 N)))) (NUMBERP (RAMSEY-INDEX N))). This simplifies, applying GOOD-C-INDEX-NUMBERP, and unfolding the functions ZEROP and RAMSEY-INDEX, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-INDEX-NUMBERP (PROVE-LEMMA CAR-NEXT-PAIR (REWRITE) (EQUAL (CAR (NEXT-PAIR S)) (NEXT (CAAR S) S)) ((ENABLE NEXT-PAIR))) This formula simplifies, applying CAR-CONS, and opening up the function NEXT-PAIR, to: T. Q.E.D. [ 0.0 0.0 0.0 ] CAR-NEXT-PAIR (PROVE-LEMMA RAMSEY-SEQ-EXTENSIBLE (REWRITE) (EXTENSIBLE (RAMSEY-SEQ N))) 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 (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p N))). 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 induction step of the scheme. The above induction scheme leads to two new goals: Case 2. (IMPLIES (ZEROP N) (EXTENSIBLE (RAMSEY-SEQ N))), which simplifies, applying EXTENSIBLE-NLISTP, and expanding the functions ZEROP and RAMSEY-SEQ, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EXTENSIBLE (RAMSEY-SEQ (SUB1 N)))) (EXTENSIBLE (RAMSEY-SEQ N))). This simplifies, applying NEXT-PAIR-EXTENDS, and unfolding the functions ZEROP and RAMSEY-SEQ, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-EXTENSIBLE (PROVE-LEMMA NEXT-NOT-ZEROP (REWRITE) (IMPLIES (EXTENSIBLE S) (AND (NUMBERP (NEXT A S)) (NOT (EQUAL (NEXT A S) 0)))) ((USE (EXTENSIBLE-NEXT-PROPERTY)) (DISABLE EXTENSIBLE-NEXT-PROPERTY))) WARNING: Note that the proposed lemma NEXT-NOT-ZEROP is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This simplifies, opening up the definitions of AND, IMPLIES, and NOT, to the following two new goals: Case 2. (IMPLIES (AND (LESSP A (NEXT A S)) (PREHOM-SEQ-1 (NEXT A S) S) (EXTENSIBLE S)) (NUMBERP (NEXT A S))). But this again simplifies, expanding the definition of LESSP, to: T. Case 1. (IMPLIES (AND (LESSP A (NEXT A S)) (PREHOM-SEQ-1 (NEXT A S) S) (EXTENSIBLE S)) (NOT (EQUAL (NEXT A S) 0))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NEXT-NOT-ZEROP (PROVE-LEMMA RAMSEY-SEQ-INCREASING (REWRITE) (IMPLIES (LESSP I J) (EQUAL (LESSP (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ J))) T)) ((INDUCT (PLUS J Q)))) This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to two new conjectures: Case 2. (IMPLIES (AND (ZEROP J) (LESSP I J)) (EQUAL (LESSP (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ J))) T)), which simplifies, opening up the definitions of ZEROP, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (IMPLIES (LESSP I (SUB1 J)) (EQUAL (LESSP (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ (SUB1 J)))) T)) (LESSP I J)) (EQUAL (LESSP (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ J))) T)), which simplifies, rewriting with the lemmas CAR-CONS and CAR-NEXT-PAIR, and unfolding the functions IMPLIES and RAMSEY-SEQ, to two new formulas: Case 1.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP I (SUB1 J))) (LESSP I J)) (LESSP (CAAR (RAMSEY-SEQ I)) (NEXT (CAAR (RAMSEY-SEQ (SUB1 J))) (RAMSEY-SEQ (SUB1 J))))), which again simplifies, using linear arithmetic, to the goal: (IMPLIES (AND (NOT (EQUAL (PLUS 1 I) 0)) (NUMBERP (PLUS 1 I)) (NOT (LESSP I (SUB1 (PLUS 1 I)))) (LESSP I (PLUS 1 I))) (LESSP (CAAR (RAMSEY-SEQ I)) (NEXT (CAAR (RAMSEY-SEQ (SUB1 (PLUS 1 I)))) (RAMSEY-SEQ (SUB1 (PLUS 1 I)))))). This again simplifies, appealing to the lemmas SUB1-ADD1, NEXT-NOT-ZEROP, and EXTENSIBLE-NLISTP, and opening up SUB1, NUMBERP, EQUAL, PLUS, ADD1, LESSP, RAMSEY-SEQ, and CAR, to the formula: (IMPLIES (AND (NUMBERP I) (NOT (LESSP I I)) (LESSP (SUB1 I) I)) (LESSP (CAAR (RAMSEY-SEQ I)) (NEXT (CAAR (RAMSEY-SEQ I)) (RAMSEY-SEQ I)))). However this again simplifies, using linear arithmetic and applying EXTENSIBLE-NEXT-PROPERTY and RAMSEY-SEQ-EXTENSIBLE, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ (SUB1 J)))) (LESSP I J)) (LESSP (CAAR (RAMSEY-SEQ I)) (NEXT (CAAR (RAMSEY-SEQ (SUB1 J))) (RAMSEY-SEQ (SUB1 J))))). This again simplifies, using linear arithmetic and appealing to the lemmas EXTENSIBLE-NEXT-PROPERTY and RAMSEY-SEQ-EXTENSIBLE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-INCREASING (PROVE-LEMMA RAMSEY-INDEX-INCREASING-REWRITE (REWRITE) (IMPLIES (LESSP I J) (EQUAL (LESSP (RAMSEY-INDEX I) (RAMSEY-INDEX J)) T))) This simplifies, using linear arithmetic and appealing to the lemma RAMSEY-INDEX-INCREASING, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-INDEX-INCREASING-REWRITE (DISABLE RAMSEY-INDEX-INCREASING) [ 0.0 0.0 0.0 ] RAMSEY-INDEX-INCREASING-OFF (PROVE-LEMMA RAMSEY-INCREASING NIL (IMPLIES (LESSP I J) (LESSP (RAMSEY I) (RAMSEY J)))) This formula can be simplified, using the abbreviations IMPLIES and RAMSEY, to: (IMPLIES (LESSP I J) (LESSP (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J))))), which simplifies, appealing to the lemmas RAMSEY-INDEX-INCREASING-REWRITE and RAMSEY-SEQ-INCREASING, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-INCREASING (DEFN RESTN (N L) (IF (LISTP L) (IF (ZEROP N) L (RESTN (SUB1 N) (CDR L))) L)) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, RESTN is accepted under the definitional principle. The definition of RESTN can be justified in another way. Linear arithmetic and the lemma CDR-LESSP can be used to prove that the measure (COUNT L) decreases according to the well-founded relation LESSP in each recursive call. [ 0.0 0.0 0.0 ] RESTN (PROVE-LEMMA RAMSEY-SEQ-RESTN-LENGTH (REWRITE) (EQUAL (RESTN N (RAMSEY-SEQ N)) NIL)) Call the conjecture *1. We will try to 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 (RAMSEY-SEQ N)) (ZEROP N)) (p N)) (IMPLIES (AND (LISTP (RAMSEY-SEQ N)) (NOT (ZEROP N)) (p (SUB1 N))) (p N)) (IMPLIES (NOT (LISTP (RAMSEY-SEQ N))) (p N))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following three new formulas: Case 3. (IMPLIES (AND (LISTP (RAMSEY-SEQ N)) (ZEROP N)) (EQUAL (RESTN N (RAMSEY-SEQ N)) NIL)). This simplifies, expanding the definitions of RAMSEY-SEQ and ZEROP, to: T. Case 2. (IMPLIES (AND (LISTP (RAMSEY-SEQ N)) (NOT (ZEROP N)) (EQUAL (RESTN (SUB1 N) (RAMSEY-SEQ (SUB1 N))) NIL)) (EQUAL (RESTN N (RAMSEY-SEQ N)) NIL)). This simplifies, appealing to the lemma CDR-CONS, and opening up RAMSEY-SEQ, ZEROP, RESTN, and EQUAL, to: T. Case 1. (IMPLIES (NOT (LISTP (RAMSEY-SEQ N))) (EQUAL (RESTN N (RAMSEY-SEQ N)) NIL)). This simplifies, unfolding RAMSEY-SEQ, LISTP, RESTN, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-RESTN-LENGTH (PROVE-LEMMA PREHOM-SEQ-RAMSEY (REWRITE) (PREHOM-SEQ (RAMSEY-SEQ N)) ((USE (RAMSEY-SEQ-HAS-RAMSEY-SEQ-P)) (DISABLE RAMSEY-SEQ-HAS-RAMSEY-SEQ-P) (ENABLE RAMSEY-SEQ-P))) This conjecture can be simplified, using the abbreviation RAMSEY-SEQ-P, to: T. This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PREHOM-SEQ-RAMSEY (DEFN LENGTH (L) (IF (LISTP L) (ADD1 (LENGTH (CDR L))) 0)) Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L) 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 L)) is a theorem. [ 0.0 0.0 0.0 ] LENGTH (PROVE-LEMMA PREHOM-SEQ-1-RESTN (REWRITE) (IMPLIES (AND (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) A) (CDAR (RESTN X S))))) WARNING: the previously added lemma, P-INTRO, could be applied whenever the newly proposed PREHOM-SEQ-1-RESTN could! This formula simplifies, rewriting with P-INTRO, to the new goal: (IMPLIES (AND (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P A (CAAR (RESTN X S))) (CDAR (RESTN X S)))), which we will name *1. We will appeal to induction. The recursive terms in the conjecture suggest seven inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP S) (p A (SUB1 X) (CDR S))) (p A X S)) (IMPLIES (NOT (LISTP S)) (p A X S))). Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT S) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for X. The above induction scheme leads to the following four new formulas: Case 4. (IMPLIES (AND (LISTP S) (NOT (PREHOM-SEQ-1 A (CDR S))) (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P A (CAAR (RESTN X S))) (CDAR (RESTN X S)))). This simplifies, applying the lemma P-INTRO, and expanding the function PREHOM-SEQ-1, to: T. Case 3. (IMPLIES (AND (LISTP S) (NOT (LESSP (SUB1 X) (LENGTH (CDR S)))) (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P A (CAAR (RESTN X S))) (CDAR (RESTN X S)))). This simplifies, appealing to the lemmas P-INTRO and SUB1-ADD1, and opening up PREHOM-SEQ-1, LENGTH, LESSP, EQUAL, and RESTN, to: T. Case 2. (IMPLIES (AND (LISTP S) (EQUAL (P A (CAAR (RESTN (SUB1 X) (CDR S)))) (CDAR (RESTN (SUB1 X) (CDR S)))) (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P A (CAAR (RESTN X S))) (CDAR (RESTN X S)))). This simplifies, applying P-INTRO and SUB1-ADD1, and opening up PREHOM-SEQ-1, LENGTH, LESSP, EQUAL, and RESTN, to: T. Case 1. (IMPLIES (AND (NOT (LISTP S)) (PREHOM-SEQ-1 A S) (LESSP X (LENGTH S))) (EQUAL (P A (CAAR (RESTN X S))) (CDAR (RESTN X S)))), which simplifies, unfolding PREHOM-SEQ-1, LENGTH, EQUAL, and LESSP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] PREHOM-SEQ-1-RESTN (PROVE-LEMMA PREHOM-SEQ-RESTN (REWRITE) (IMPLIES (AND (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S))))) WARNING: the previously added lemma, P-INTRO, could be applied whenever the newly proposed PREHOM-SEQ-RESTN could! This formula simplifies, applying P-INTRO, and expanding the functions EQUAL and LESSP, to the formula: (IMPLIES (AND (PREHOM-SEQ S) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR S) (CAAR (RESTN X S))) (CDAR (RESTN X S)))). Appealing to the lemma CAR-CDR-ELIM, we now replace S by (CONS Z V) to eliminate (CAR S) and (CDR S) and Z by (CONS W D) to eliminate (CAR Z) and (CDR Z). The result is three new goals: Case 3. (IMPLIES (AND (NOT (LISTP S)) (PREHOM-SEQ S) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR S) (CAAR (RESTN X S))) (CDAR (RESTN X S)))), which further simplifies, opening up PREHOM-SEQ, LENGTH, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (LISTP Z)) (PREHOM-SEQ (CONS Z V)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X (LENGTH (CONS Z V)))) (EQUAL (P (CAR Z) (CAAR (RESTN X (CONS Z V)))) (CDAR (RESTN X (CONS Z V))))), which further simplifies, appealing to the lemmas CAR-NLISTP, CAR-CONS, and CDR-CONS, and unfolding LESSP, EQUAL, PREHOM-SEQ, LENGTH, ADD1, RESTN, CAR, and CDR, to: (IMPLIES (AND (NOT (LISTP Z)) (NOT (LISTP V)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X 1)) (EQUAL (P 0 0) 0)). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (PREHOM-SEQ (CONS (CONS W D) V)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X (LENGTH (CONS (CONS W D) V)))) (EQUAL (P W (CAAR (RESTN X (CONS (CONS W D) V)))) (CDAR (RESTN X (CONS (CONS W D) V))))), which further simplifies, rewriting with CAR-CONS, CDR-CONS, CAR-NLISTP, P-INTRO, and SUB1-ADD1, and opening up PREHOM-SEQ, LENGTH, ADD1, RESTN, CAR, CDR, and LESSP, to the following two new conjectures: Case 1.2. (IMPLIES (AND (NOT (LISTP V)) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP X 1)) (EQUAL (P 0 W) 0)). But this again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (LESSP (CAAR V) W) (PREHOM-SEQ-1 W V) (PREHOM-SEQ V) (NOT (EQUAL X 0)) (NUMBERP X) (LESSP (SUB1 X) (LENGTH V))) (EQUAL (P W (CAAR (RESTN (SUB1 X) V))) (CDAR (RESTN (SUB1 X) V)))). Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X). We employ the type restriction lemma noted when SUB1 was introduced to restrict the new variable. This produces: (IMPLIES (AND (NUMBERP Z) (LESSP (CAAR V) W) (PREHOM-SEQ-1 W V) (PREHOM-SEQ V) (NOT (EQUAL (ADD1 Z) 0)) (LESSP Z (LENGTH V))) (EQUAL (P W (CAAR (RESTN Z V))) (CDAR (RESTN Z V)))), which further simplifies, obviously, to: (IMPLIES (AND (NUMBERP Z) (LESSP (CAAR V) W) (PREHOM-SEQ-1 W V) (PREHOM-SEQ V) (LESSP Z (LENGTH V))) (EQUAL (P W (CAAR (RESTN Z V))) (CDAR (RESTN Z V)))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (IMPLIES (AND (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))), named *1. Let us appeal to the induction principle. Eight 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 S) (LISTP (CDR S)) (p (SUB1 X) (CDR S))) (p X S)) (IMPLIES (AND (LISTP S) (NOT (LISTP (CDR S)))) (p X S)) (IMPLIES (NOT (LISTP S)) (p X S))). Linear arithmetic and the lemma CDR-LESSP 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. Note, however, the inductive instance chosen for X. The above induction scheme leads to the following six new goals: Case 6. (IMPLIES (AND (LISTP S) (LISTP (CDR S)) (NOT (PREHOM-SEQ (CDR S))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))). This simplifies, opening up PREHOM-SEQ, to: T. Case 5. (IMPLIES (AND (LISTP S) (LISTP (CDR S)) (NOT (LESSP 0 (SUB1 X))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))). This simplifies, using linear arithmetic, to the following two new formulas: Case 5.2. (IMPLIES (AND (NOT (NUMBERP X)) (LISTP S) (LISTP (CDR S)) (NOT (LESSP 0 (SUB1 X))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))). This again simplifies, opening up PREHOM-SEQ and LESSP, to: T. Case 5.1. (IMPLIES (AND (NUMBERP X) (LISTP S) (LISTP (CDR S)) (NOT (LESSP 0 (SUB1 1))) (PREHOM-SEQ S) (LESSP 0 1) (LESSP 1 (LENGTH S))) (EQUAL (P (CAAR (RESTN 1 S)) (CAAR S)) (CDAR (RESTN 1 S)))), which again simplifies, applying the lemmas SUB1-ADD1 and P-INTRO, and opening up SUB1, LESSP, PREHOM-SEQ, LENGTH, NUMBERP, EQUAL, and RESTN, to: (IMPLIES (AND (NUMBERP X) (LISTP S) (LISTP (CDR S)) (LESSP (CAADR S) (CAAR S)) (PREHOM-SEQ-1 (CAAR S) (CDR S)) (PREHOM-SEQ (CDR S)) (NOT (EQUAL (LENGTH (CDR S)) 0))) (EQUAL (P (CAAR S) (CAADR S)) (CDADR S))). But this again simplifies, rewriting with P-INTRO, and unfolding the function PREHOM-SEQ-1, to: T. Case 4. (IMPLIES (AND (LISTP S) (LISTP (CDR S)) (NOT (LESSP (SUB1 X) (LENGTH (CDR S)))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))). This simplifies, appealing to the lemma SUB1-ADD1, and expanding the definitions of PREHOM-SEQ, LESSP, EQUAL, and LENGTH, to: T. Case 3. (IMPLIES (AND (LISTP S) (LISTP (CDR S)) (EQUAL (P (CAAR (RESTN (SUB1 X) (CDR S))) (CAADR S)) (CDAR (RESTN (SUB1 X) (CDR S)))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))). This simplifies, rewriting with P-INTRO, SUB1-ADD1, and PREHOM-SEQ-1-RESTN, and opening up the functions PREHOM-SEQ, LESSP, EQUAL, LENGTH, and RESTN, to: T. Case 2. (IMPLIES (AND (LISTP S) (NOT (LISTP (CDR S))) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))), which simplifies, appealing to the lemmas SUB1-ADD1 and PREHOM-SEQ-1-RESTN, and opening up the functions PREHOM-SEQ, LESSP, EQUAL, LENGTH, RESTN, and PREHOM-SEQ-1, to: T. Case 1. (IMPLIES (AND (NOT (LISTP S)) (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR (RESTN X S)) (CAAR S)) (CDAR (RESTN X S)))), which simplifies, using linear arithmetic, rewriting with the lemmas P-INTRO, PREHOM-SEQ-1-RESTN, and CAR-NLISTP, and unfolding the functions CDR, RESTN, and PREHOM-SEQ-1, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.1 ] PREHOM-SEQ-RESTN (PROVE-LEMMA RAMSEY-SEQ-PLUS (REWRITE) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS X Y))) (RAMSEY-SEQ Y))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest three inductions. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (AND (LISTP (RAMSEY-SEQ (PLUS X Y))) (ZEROP X)) (p X Y)) (IMPLIES (AND (LISTP (RAMSEY-SEQ (PLUS X Y))) (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y)) (IMPLIES (NOT (LISTP (RAMSEY-SEQ (PLUS X Y)))) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following three new formulas: Case 3. (IMPLIES (AND (LISTP (RAMSEY-SEQ (PLUS X Y))) (ZEROP X)) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS X Y))) (RAMSEY-SEQ Y))). This simplifies, expanding the definitions of PLUS, ZEROP, EQUAL, RAMSEY-SEQ, RESTN, and LISTP, to: T. Case 2. (IMPLIES (AND (LISTP (RAMSEY-SEQ (PLUS X Y))) (NOT (ZEROP X)) (EQUAL (RESTN (SUB1 X) (RAMSEY-SEQ (PLUS (SUB1 X) Y))) (RAMSEY-SEQ Y))) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS X Y))) (RAMSEY-SEQ Y))). This simplifies, applying SUB1-ADD1 and CDR-CONS, and expanding the definitions of PLUS, ZEROP, RAMSEY-SEQ, and RESTN, to: T. Case 1. (IMPLIES (NOT (LISTP (RAMSEY-SEQ (PLUS X Y)))) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS X Y))) (RAMSEY-SEQ Y))), which simplifies, rewriting with the lemmas SUB1-ADD1 and CDR-CONS, and opening up the functions PLUS, RAMSEY-SEQ, RESTN, EQUAL, and LISTP, to the goal: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (LISTP (RAMSEY-SEQ (ADD1 (PLUS (SUB1 X) Y)))))) (EQUAL (RESTN (SUB1 X) (RAMSEY-SEQ (PLUS (SUB1 X) Y))) (RAMSEY-SEQ Y))). However this again simplifies, rewriting with SUB1-ADD1, and opening up RAMSEY-SEQ, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-PLUS (PROVE-LEMMA PLUS-COMM (REWRITE) (EQUAL (PLUS X Y) (PLUS Y X))) This formula simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-COMM (PROVE-LEMMA RAMSEY-SEQ-PLUS-COMMUTED (REWRITE) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS Y X))) (RAMSEY-SEQ Y))) This conjecture simplifies, applying PLUS-COMM and RAMSEY-SEQ-PLUS, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-PLUS-COMMUTED (PROVE-LEMMA LENGTH-RAMSEY-SEQ (REWRITE) (EQUAL (LENGTH (RAMSEY-SEQ N)) (FIX N))) This formula simplifies, unfolding the definition of FIX, to the following two new goals: Case 2. (IMPLIES (NOT (NUMBERP N)) (EQUAL (LENGTH (RAMSEY-SEQ N)) 0)). This again simplifies, unfolding the definitions of RAMSEY-SEQ, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (NUMBERP N) (EQUAL (LENGTH (RAMSEY-SEQ N)) N)), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p N))). 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 induction step of the scheme. The above induction scheme leads to the following two new formulas: Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N)) (EQUAL (LENGTH (RAMSEY-SEQ N)) N)). This simplifies, unfolding the definitions of ZEROP, NUMBERP, RAMSEY-SEQ, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (LENGTH (RAMSEY-SEQ (SUB1 N))) (SUB1 N)) (NUMBERP N)) (EQUAL (LENGTH (RAMSEY-SEQ N)) N)). This simplifies, rewriting with the lemmas ADD1-SUB1 and CDR-CONS, and opening up the functions ZEROP, RAMSEY-SEQ, and LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-RAMSEY-SEQ (PROVE-LEMMA PLUS-DIFFERENCE-ELIM (ELIM) (IMPLIES (AND (NUMBERP J) (NOT (LESSP J I))) (EQUAL (PLUS I (DIFFERENCE J I)) J))) This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-DIFFERENCE-ELIM (PROVE-LEMMA RESTN-DIFFERENCE-RAMSEY-SEQ (REWRITE) (IMPLIES (AND (LESSP 0 I) (LESSP I J)) (EQUAL (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)) (RAMSEY-SEQ I)))) This conjecture simplifies, expanding the functions EQUAL and LESSP, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)) (RAMSEY-SEQ I))). Applying the lemma PLUS-DIFFERENCE-ELIM, replace J by (PLUS I X) to eliminate (DIFFERENCE J I). We employ the type restriction lemma noted when DIFFERENCE was introduced to restrict the new variable. We would thus like to prove the following three new conjectures: Case 3. (IMPLIES (AND (LESSP J I) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)) (RAMSEY-SEQ I))). But this further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)) (RAMSEY-SEQ I))), which further simplifies, unfolding LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NOT (LESSP (PLUS I X) I)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I (PLUS I X))) (EQUAL (RESTN X (RAMSEY-SEQ (PLUS I X))) (RAMSEY-SEQ I))), which further simplifies, rewriting with the lemma RAMSEY-SEQ-PLUS-COMMUTED, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RESTN-DIFFERENCE-RAMSEY-SEQ (PROVE-LEMMA PREHOM-SEQ-RESTN-COMMUTED (REWRITE) (IMPLIES (AND (PREHOM-SEQ S) (LESSP 0 X) (LESSP X (LENGTH S))) (EQUAL (P (CAAR S) (CAAR (RESTN X S))) (CDAR (RESTN X S)))) ((USE (PREHOM-SEQ-RESTN)) (DISABLE PREHOM-SEQ-RESTN))) WARNING: the previously added lemma, P-INTRO, could be applied whenever the newly proposed PREHOM-SEQ-RESTN-COMMUTED could! This simplifies, applying P-INTRO, and expanding the functions EQUAL, LESSP, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PREHOM-SEQ-RESTN-COMMUTED (PROVE-LEMMA RAMSEY-SEQ-PREHOM-LEMMA NIL (IMPLIES (AND (LESSP 0 I) (LESSP I J)) (EQUAL (P (CAAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J))) (CAAR (RAMSEY-SEQ J))) (CDAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J))))) ((DISABLE RESTN-DIFFERENCE-RAMSEY-SEQ RAMSEY-SEQ-PLUS-COMMUTED))) This conjecture simplifies, rewriting with the lemma P-INTRO, and opening up the definitions of EQUAL and LESSP, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (P (CAAR (RAMSEY-SEQ J)) (CAAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)))) (CDAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J))))). Appealing to the lemma PLUS-DIFFERENCE-ELIM, we now replace J by (PLUS I X) to eliminate (DIFFERENCE J I). We rely upon the type restriction lemma noted when DIFFERENCE was introduced to constrain the new variable. This generates three new goals: Case 3. (IMPLIES (AND (LESSP J I) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (P (CAAR (RAMSEY-SEQ J)) (CAAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)))) (CDAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J))))), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I J)) (EQUAL (P (CAAR (RAMSEY-SEQ J)) (CAAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J)))) (CDAR (RESTN (DIFFERENCE J I) (RAMSEY-SEQ J))))), which further simplifies, unfolding the function LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NOT (LESSP (PLUS I X) I)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I (PLUS I X))) (EQUAL (P (CAAR (RAMSEY-SEQ (PLUS I X))) (CAAR (RESTN X (RAMSEY-SEQ (PLUS I X))))) (CDAR (RESTN X (RAMSEY-SEQ (PLUS I X)))))), which further simplifies, using linear arithmetic and rewriting with LENGTH-RAMSEY-SEQ, PREHOM-SEQ-RAMSEY, and PREHOM-SEQ-RESTN-COMMUTED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] RAMSEY-SEQ-PREHOM-LEMMA (PROVE-LEMMA RAMSEY-SEQ-PREHOM (REWRITE) (IMPLIES (AND (LESSP 0 I) (LESSP I J)) (EQUAL (P (CAAR (RAMSEY-SEQ I)) (CAAR (RAMSEY-SEQ J))) (CDAR (RAMSEY-SEQ I)))) ((USE (RAMSEY-SEQ-PREHOM-LEMMA)))) WARNING: the previously added lemma, P-INTRO, could be applied whenever the newly proposed RAMSEY-SEQ-PREHOM could! This conjecture simplifies, appealing to the lemma RESTN-DIFFERENCE-RAMSEY-SEQ, and expanding the definitions of EQUAL, LESSP, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-PREHOM (PROVE-LEMMA CDAR-RAMSEQ-SEQ-RAMSEY-INDEX (REWRITE) (EQUAL (CDAR (RAMSEY-SEQ (RAMSEY-INDEX N))) (COLOR))) 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 (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p 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 induction step of the scheme. The above induction scheme generates two new conjectures: Case 2. (IMPLIES (ZEROP N) (EQUAL (CDAR (RAMSEY-SEQ (RAMSEY-INDEX N))) (COLOR))), which simplifies, applying COLOR-PROPERTIES, and opening up ZEROP, EQUAL, and RAMSEY-INDEX, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (CDAR (RAMSEY-SEQ (RAMSEY-INDEX (SUB1 N)))) (COLOR))) (EQUAL (CDAR (RAMSEY-SEQ (RAMSEY-INDEX N))) (COLOR))). This simplifies, applying the lemma COLOR-PROPERTIES, and unfolding the functions ZEROP and RAMSEY-INDEX, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] CDAR-RAMSEQ-SEQ-RAMSEY-INDEX (PROVE-LEMMA LESSP-GOOD-C-INDEX (REWRITE) (EQUAL (LESSP BIG (GOOD-C-INDEX BIG (COLOR))) T)) This formula simplifies, using linear arithmetic and applying the lemma COLOR-PROPERTIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-GOOD-C-INDEX (DISABLE COLOR-PROPERTIES) [ 0.0 0.0 0.0 ] COLOR-PROPERTIES-OFF (PROVE-LEMMA GOOD-C-INDEX-NON-ZERO (REWRITE) (EQUAL (LESSP 0 (GOOD-C-INDEX BIG (COLOR))) T) ((USE (LESSP-GOOD-C-INDEX)) (DISABLE LESSP-GOOD-C-INDEX))) This simplifies, applying GOOD-C-INDEX-NUMBERP, and expanding the definitions of EQUAL and LESSP, to the new goal: (IMPLIES (LESSP BIG (GOOD-C-INDEX BIG (COLOR))) (NOT (EQUAL (GOOD-C-INDEX BIG (COLOR)) 0))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GOOD-C-INDEX-NON-ZERO (PROVE-LEMMA RAMSEY-INDEX-POSITIVE (REWRITE) (LESSP 0 (RAMSEY-INDEX N)) ((EXPAND (RAMSEY-INDEX N)))) WARNING: Note that the proposed lemma RAMSEY-INDEX-POSITIVE is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, expanding the functions RAMSEY-INDEX, EQUAL, and LESSP, to the following six new goals: Case 6. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N)) (NOT (EQUAL (GOOD-C-INDEX (RAMSEY-INDEX (SUB1 N)) (COLOR)) 0))). Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 X) to eliminate (SUB1 N). We rely upon the type restriction lemma noted when SUB1 was introduced to constrain the new variable. The result is: (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0))) (NOT (EQUAL (GOOD-C-INDEX (RAMSEY-INDEX X) (COLOR)) 0))). This further simplifies, obviously, to: (IMPLIES (NUMBERP X) (NOT (EQUAL (GOOD-C-INDEX (RAMSEY-INDEX X) (COLOR)) 0))), 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: (LESSP 0 (RAMSEY-INDEX N)), named *1. Let us appeal to the induction principle. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N))) (p N))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following two new formulas: Case 2. (IMPLIES (ZEROP N) (LESSP 0 (RAMSEY-INDEX N))). This simplifies, rewriting with the lemma GOOD-C-INDEX-NON-ZERO, and expanding the definitions of ZEROP, EQUAL, and RAMSEY-INDEX, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (LESSP 0 (RAMSEY-INDEX (SUB1 N)))) (LESSP 0 (RAMSEY-INDEX N))). This simplifies, rewriting with GOOD-C-INDEX-NON-ZERO, and opening up the functions ZEROP, EQUAL, LESSP, and RAMSEY-INDEX, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-INDEX-POSITIVE (PROVE-LEMMA RAMSEY-SEQ-HOM-LESSP NIL (IMPLIES (LESSP I J) (EQUAL (P (RAMSEY I) (RAMSEY J)) (COLOR)))) This formula can be simplified, using the abbreviations IMPLIES and RAMSEY, to the new conjecture: (IMPLIES (LESSP I J) (EQUAL (P (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J)))) (COLOR))), which simplifies, using linear arithmetic and rewriting with RAMSEY-INDEX-INCREASING-REWRITE, RAMSEY-INDEX-POSITIVE, CDAR-RAMSEQ-SEQ-RAMSEY-INDEX, and RAMSEY-SEQ-PREHOM, to: T. Q.E.D. [ 0.0 0.0 0.0 ] RAMSEY-SEQ-HOM-LESSP (PROVE-LEMMA P-NUM-IS-P (REWRITE) (IMPLIES (AND (NUMBERP X) (NUMBERP Y)) (EQUAL (P-NUM X Y) (P X Y))) ((ENABLE P))) This conjecture simplifies, expanding the definition of P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-NUM-IS-P (PROVE-LEMMA NUMBERP-RAMSEY (REWRITE) (NUMBERP (CAAR (RAMSEY-SEQ (RAMSEY-INDEX N)))) ((ENABLE NEXT-PAIR) (EXPAND (RAMSEY-SEQ (RAMSEY-INDEX N))))) This simplifies, unfolding RAMSEY-SEQ and NEXT-PAIR, to two new formulas: Case 2. (IMPLIES (NOT (EQUAL (RAMSEY-INDEX N) 0)) (NUMBERP (CAAR (CONS (CONS (NEXT (CAAR (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N)))) (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N)))) (NEXT-COLOR (NEXT (CAAR (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N)))) (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N)))) (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N))))) (RAMSEY-SEQ (SUB1 (RAMSEY-INDEX N))))))), which again simplifies, rewriting with CAR-CONS, RAMSEY-SEQ-EXTENSIBLE, and NEXT-NOT-ZEROP, to: T. Case 1. (IMPLIES (EQUAL (RAMSEY-INDEX N) 0) (NUMBERP (CAAR NIL))). This again simplifies, using linear arithmetic and applying RAMSEY-INDEX-POSITIVE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] NUMBERP-RAMSEY (PROVE-LEMMA RAMSEY-SEQ-HOM (REWRITE) (IMPLIES (AND (NUMBERP I) (NUMBERP J) (NOT (EQUAL I J))) (EQUAL (P-NUM (RAMSEY I) (RAMSEY J)) (COLOR))) ((USE (RAMSEY-SEQ-HOM-LESSP) (RAMSEY-SEQ-HOM-LESSP (I J) (J I))))) This conjecture can be simplified, using the abbreviations NOT, IMPLIES, AND, and RAMSEY, to: (IMPLIES (AND (IMPLIES (LESSP I J) (EQUAL (P (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J)))) (COLOR))) (IMPLIES (LESSP J I) (EQUAL (P (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I)))) (COLOR))) (NUMBERP I) (NUMBERP J) (NOT (EQUAL I J))) (EQUAL (P-NUM (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J)))) (COLOR))). This simplifies, rewriting with the lemmas P-INTRO, NUMBERP-RAMSEY, and P-NUM-IS-P, and unfolding the definition of IMPLIES, to: (IMPLIES (AND (NOT (LESSP I J)) (NOT (LESSP J I)) (NUMBERP I) (NUMBERP J) (NOT (EQUAL I J))) (EQUAL (P (CAAR (RAMSEY-SEQ (RAMSEY-INDEX I))) (CAAR (RAMSEY-SEQ (RAMSEY-INDEX J)))) (COLOR))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] RAMSEY-SEQ-HOM