(BOOT-STRAP NQTHM)
[ 0.0 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
(DCL ABOVE (S))
[ 0.0 0.0 0.0 ]
ABOVE
(DCL NEXT (ABOVE S))
[ 0.0 0.0 0.0 ]
NEXT
(DCL EXTENSIBLE (S))
[ 0.0 0.0 0.0 ]
EXTENSIBLE
(ADD-AXIOM EXTENSIBLE-INTRO
(REWRITE)
(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)))))
WARNING: Note that EXTENSIBLE-INTRO contains the free variable NEXT which
will be chosen by instantiating the hypothesis (LESSP (ABOVE S) NEXT).
WARNING: Note that EXTENSIBLE-INTRO 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: Note that the proposed lemma EXTENSIBLE-INTRO is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
[ 0.0 0.0 0.0 ]
EXTENSIBLE-INTRO
(ADD-AXIOM EXTENSIBLE-BOOLEAN
(REWRITE)
(OR (TRUEP (EXTENSIBLE S))
(FALSEP (EXTENSIBLE S))))
WARNING: Note that the proposed lemma EXTENSIBLE-BOOLEAN is to be stored as
one type prescription rule, zero compound recognizer rules, zero linear rules,
and zero replacement rules.
[ 0.0 0.0 0.0 ]
EXTENSIBLE-BOOLEAN
(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-INTRO, could be applied
whenever the newly proposed EXTENSIBLE-SUFF could!
This conjecture simplifies, rewriting with EXTENSIBLE-INTRO, 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-INTRO))
(DISABLE EXTENSIBLE-INTRO)))
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-INTRO, 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.2 ]
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-INTRO (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
(DCL BIG (C))
[ 0.0 0.0 0.0 ]
BIG
(DCL GOOD-C-INDEX (BIG C))
[ 0.0 0.0 0.0 ]
GOOD-C-INDEX
(DCL GOOD-COLOR-P (C))
[ 0.0 0.0 0.0 ]
GOOD-COLOR-P
(ADD-AXIOM GOOD-COLOR-P-INTRO
(REWRITE)
(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)))))
WARNING: Note that GOOD-COLOR-P-INTRO contains the free variable GOOD-C-INDEX
which will be chosen by instantiating the hypothesis:
(LESSP (BIG C) GOOD-C-INDEX).
WARNING: Note that GOOD-COLOR-P-INTRO 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: Note that the proposed lemma GOOD-COLOR-P-INTRO is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
[ 0.0 0.0 0.0 ]
GOOD-COLOR-P-INTRO
(ADD-AXIOM GOOD-COLOR-P-BOOLEAN
(REWRITE)
(OR (TRUEP (GOOD-COLOR-P C))
(FALSEP (GOOD-COLOR-P C))))
WARNING: Note that the proposed lemma GOOD-COLOR-P-BOOLEAN is to be stored as
one type prescription rule, zero compound recognizer rules, zero linear rules,
and zero replacement rules.
[ 0.0 0.0 0.0 ]
GOOD-COLOR-P-BOOLEAN
(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-INTRO, could be applied
whenever the newly proposed GOOD-COLOR-P-SUFF could!
This conjecture simplifies, rewriting with GOOD-COLOR-P-INTRO, 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-INTRO))
(DISABLE GOOD-COLOR-P-INTRO)))
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-INTRO, 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.0 ]
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.0 ]
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.0 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.0 0.0 ]
RAMSEY-SEQ-HOM