(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(DEFN RAMSEY
(P Q)
(IF (ZEROP P)
1
(IF (ZEROP Q)
1
(PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))
((LESSP (PLUS P Q))))
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of ZEROP,
LESSP, and PLUS inform us that the measure (PLUS P Q) decreases according to
the well-founded relation LESSP in each recursive call. Hence, RAMSEY is
accepted under the principle of definition. Observe that
(NUMBERP (RAMSEY P Q)) is a theorem.
[ 0.0 0.0 0.0 ]
RAMSEY
(DEFN RELATED
(I J PAIRS)
(OR (MEMBER (CONS I J) PAIRS)
(MEMBER (CONS J I) PAIRS)))
Note that (OR (FALSEP (RELATED I J PAIRS)) (TRUEP (RELATED I J PAIRS)))
is a theorem.
[ 0.0 0.0 0.0 ]
RELATED
(DEFN PARTITION
(N REST PAIRS)
(IF (LISTP REST)
(IF (RELATED N (CAR REST) PAIRS)
(CONS (CONS (CAR REST)
(CAR (PARTITION N (CDR REST) PAIRS)))
(CDR (PARTITION N (CDR REST) PAIRS)))
(CONS (CAR (PARTITION N (CDR REST) PAIRS))
(CONS (CAR REST)
(CDR (PARTITION N (CDR REST) PAIRS)))))
(CONS NIL NIL)))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT REST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, PARTITION is accepted under the definitional principle.
Observe that (LISTP (PARTITION N REST PAIRS)) is a theorem.
[ 0.0 0.0 0.0 ]
PARTITION
(DEFN LENGTH
(LST)
(IF (LISTP LST)
(ADD1 (LENGTH (CDR LST)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) 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 LST)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN WIT
(PAIRS DOMAIN P Q)
(IF (LISTP DOMAIN)
(IF (ZEROP P)
(CONS NIL 1)
(IF (ZEROP Q)
(CONS NIL 2)
(IF (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(IF (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))
(CONS (CONS (CAR DOMAIN)
(CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
2))
(IF (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)
(CONS (CONS (CAR DOMAIN)
(CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
1)))))
(CONS NIL 1))
((LESSP (PLUS P Q))))
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP,
PLUS, and ZEROP establish that the measure (PLUS P Q) decreases according to
the well-founded relation LESSP in each recursive call. Hence, WIT is
accepted under the principle of definition. From the definition we can
conclude that (LISTP (WIT PAIRS DOMAIN P Q)) is a theorem.
[ 0.0 0.0 0.0 ]
WIT
(DEFN HOMOGENEOUS1
(N DOMAIN PAIRS FLG)
(IF (LISTP DOMAIN)
(AND (IF (EQUAL FLG 1)
(RELATED N (CAR DOMAIN) PAIRS)
(NOT (RELATED N (CAR DOMAIN) PAIRS)))
(HOMOGENEOUS1 N
(CDR DOMAIN)
PAIRS FLG))
T))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT DOMAIN) decreases according to the well-founded relation LESSP in each
recursive call. Hence, HOMOGENEOUS1 is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (HOMOGENEOUS1 N DOMAIN PAIRS FLG))
(TRUEP (HOMOGENEOUS1 N DOMAIN PAIRS FLG)))
is a theorem.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS1
(DEFN HOMOGENEOUS
(DOMAIN PAIRS FLG)
(IF (LISTP DOMAIN)
(AND (HOMOGENEOUS1 (CAR DOMAIN)
(CDR DOMAIN)
PAIRS FLG)
(HOMOGENEOUS (CDR DOMAIN) PAIRS FLG))
T))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT DOMAIN) decreases according to the well-founded relation LESSP in each
recursive call. Hence, HOMOGENEOUS is accepted under the principle of
definition. Note that:
(OR (FALSEP (HOMOGENEOUS DOMAIN PAIRS FLG))
(TRUEP (HOMOGENEOUS DOMAIN PAIRS FLG)))
is a theorem.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS
(DEFN SUBSETP
(X Y)
(IF (NLISTP X)
T
(IF (MEMBER (CAR X) Y)
(SUBSETP (CDR X) Y)
F)))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call. Hence, SUBSETP is
accepted under the definitional principle. Note that:
(OR (FALSEP (SUBSETP X Y))
(TRUEP (SUBSETP X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBSETP
(PROVE-LEMMA MEMBER-CONS
(REWRITE)
(IMPLIES (MEMBER A L)
(MEMBER A (CONS X L))))
This formula simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
expanding the definition of MEMBER, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-CONS
(PROVE-LEMMA SUBSETP-CONS
(REWRITE)
(IMPLIES (SUBSETP L M)
(SUBSETP L (CONS A M))))
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (p L A M))
(IMPLIES (AND (NOT (NLISTP L))
(MEMBER (CAR L) M)
(p (CDR L) A M))
(p L A M))
(IMPLIES (AND (NOT (NLISTP L))
(NOT (MEMBER (CAR L) M)))
(p L A M))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (NLISTP L) (SUBSETP L M))
(SUBSETP L (CONS A M))),
which simplifies, expanding the functions NLISTP and SUBSETP, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(MEMBER (CAR L) M)
(NOT (SUBSETP (CDR L) M))
(SUBSETP L M))
(SUBSETP L (CONS A M))),
which simplifies, opening up the functions NLISTP and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(MEMBER (CAR L) M)
(SUBSETP (CDR L) (CONS A M))
(SUBSETP L M))
(SUBSETP L (CONS A M))),
which simplifies, applying the lemma MEMBER-CONS, and opening up NLISTP and
SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (MEMBER (CAR L) M))
(SUBSETP L M))
(SUBSETP L (CONS A M))),
which simplifies, opening up NLISTP and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-CONS
(PROVE-LEMMA SUBSETP-REFLEXIVITY
(REWRITE)
(SUBSETP X X))
Give the conjecture the 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 (NLISTP X) (p X))
(IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) X)
(p (CDR X)))
(p X))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) X)))
(p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates the following three new formulas:
Case 3. (IMPLIES (NLISTP X) (SUBSETP X X)).
This simplifies, expanding the functions NLISTP and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) X)
(SUBSETP (CDR X) (CDR X)))
(SUBSETP X X)).
This simplifies, opening up the functions NLISTP, MEMBER, and SUBSETP, to:
(IMPLIES (AND (LISTP X)
(SUBSETP (CDR X) (CDR X)))
(SUBSETP (CDR X) X)).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate
(CDR X) and (CAR X). This produces:
(IMPLIES (SUBSETP Z Z)
(SUBSETP Z (CONS V Z))),
which further simplifies, applying SUBSETP-CONS, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) X)))
(SUBSETP X X)).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
SUBSETP-REFLEXIVITY
(PROVE-LEMMA CDR-SUBSETP
(REWRITE)
(SUBSETP (CDR X) X))
.
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X)
and (CAR X). We would thus like to prove the following two new conjectures:
Case 2. (IMPLIES (NOT (LISTP X))
(SUBSETP (CDR X) X)).
This simplifies, applying CDR-NLISTP, and expanding LISTP and SUBSETP, to:
T.
Case 1. (SUBSETP Z (CONS V Z)).
But this simplifies, rewriting with the lemmas SUBSETP-REFLEXIVITY and
SUBSETP-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CDR-SUBSETP
(PROVE-LEMMA MEMBER-SUBSETP
(REWRITE)
(IMPLIES (AND (MEMBER X Y) (SUBSETP Y Z))
(MEMBER X Z)))
WARNING: Note that MEMBER-SUBSETP contains the free variable Y which will be
chosen by instantiating the hypothesis (MEMBER X Y).
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP Y) (p X Z Y))
(IMPLIES (AND (NOT (NLISTP Y))
(EQUAL X (CAR Y)))
(p X Z Y))
(IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(p X Z (CDR Y)))
(p X Z Y))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT Y) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to four new goals:
Case 4. (IMPLIES (AND (NLISTP Y)
(MEMBER X Y)
(SUBSETP Y Z))
(MEMBER X Z)),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP Y))
(EQUAL X (CAR Y))
(MEMBER X Y)
(SUBSETP Y Z))
(MEMBER X Z)),
which simplifies, expanding NLISTP, MEMBER, and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(NOT (MEMBER X (CDR Y)))
(MEMBER X Y)
(SUBSETP Y Z))
(MEMBER X Z)),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(NOT (SUBSETP (CDR Y) Z))
(MEMBER X Y)
(SUBSETP Y Z))
(MEMBER X Z)),
which simplifies, unfolding the functions NLISTP, MEMBER, and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-SUBSETP
(PROVE-LEMMA SUBSETP-IS-TRANSITIVE
(REWRITE)
(IMPLIES (AND (SUBSETP X Y) (SUBSETP Y Z))
(SUBSETP X Z)))
WARNING: Note that SUBSETP-IS-TRANSITIVE contains the free variable Y which
will be chosen by instantiating the hypothesis (SUBSETP X Y).
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP X) (p X Z Y))
(IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) Y)
(p (CDR X) Z Y))
(p X Z Y))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) Y)))
(p X Z Y))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to four new goals:
Case 4. (IMPLIES (AND (NLISTP X)
(SUBSETP X Y)
(SUBSETP Y Z))
(SUBSETP X Z)),
which simplifies, opening up the definitions of NLISTP and SUBSETP, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) Y)
(NOT (SUBSETP (CDR X) Y))
(SUBSETP X Y)
(SUBSETP Y Z))
(SUBSETP X Z)),
which simplifies, applying SUBSETP-REFLEXIVITY and MEMBER-SUBSETP, and
unfolding NLISTP and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) Y)
(SUBSETP (CDR X) Z)
(SUBSETP X Y)
(SUBSETP Y Z))
(SUBSETP X Z)).
This simplifies, applying SUBSETP-REFLEXIVITY and MEMBER-SUBSETP, and
opening up the functions NLISTP and SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) Y))
(SUBSETP X Y)
(SUBSETP Y Z))
(SUBSETP X Z)),
which simplifies, opening up the definitions of NLISTP and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-IS-TRANSITIVE
(PROVE-LEMMA SUBSETP-CDR-PARTITION
(REWRITE)
(SUBSETP (CDR (PARTITION X Z PAIRS))
Z))
Give the conjecture the name *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(p X (CDR Z) PAIRS))
(p X Z PAIRS))
(IMPLIES (AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(p X (CDR Z) PAIRS))
(p X Z PAIRS))
(IMPLIES (NOT (LISTP Z))
(p X Z PAIRS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
conjectures:
Case 3. (IMPLIES (AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(SUBSETP (CDR (PARTITION X (CDR Z) PAIRS))
(CDR Z)))
(SUBSETP (CDR (PARTITION X Z PAIRS))
Z)).
This simplifies, applying MEMBER-SUBSETP, SUBSETP-REFLEXIVITY, CDR-CONS,
CDR-SUBSETP, and SUBSETP-IS-TRANSITIVE, and opening up the functions RELATED
and PARTITION, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(SUBSETP (CDR (PARTITION X (CDR Z) PAIRS))
(CDR Z)))
(SUBSETP (CDR (PARTITION X Z PAIRS))
Z)),
which simplifies, rewriting with CDR-CONS, SUBSETP-IS-TRANSITIVE,
CDR-SUBSETP, and CAR-CONS, and opening up RELATED, PARTITION, MEMBER, and
SUBSETP, to:
T.
Case 1. (IMPLIES (NOT (LISTP Z))
(SUBSETP (CDR (PARTITION X Z PAIRS))
Z)).
This simplifies, unfolding the definitions of PARTITION, CDR, LISTP, and
SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-CDR-PARTITION
(PROVE-LEMMA SUBSETP-HOM-SET-DOMAIN-1
(REWRITE)
(IMPLIES (SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P Q))
(CDR (PARTITION X Z PAIRS)))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P Q))
(CONS X Z)))
((USE (SUBSETP-CDR-PARTITION))
(DISABLE SUBSETP-CDR-PARTITION)))
This formula simplifies, applying SUBSETP-IS-TRANSITIVE, SUBSETP-REFLEXIVITY,
and SUBSETP-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-HOM-SET-DOMAIN-1
(PROVE-LEMMA SUBSETP-CAR-PARTITION
(REWRITE)
(SUBSETP (CAR (PARTITION X Z PAIRS))
Z))
Give the conjecture the name *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(p X (CDR Z) PAIRS))
(p X Z PAIRS))
(IMPLIES (AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(p X (CDR Z) PAIRS))
(p X Z PAIRS))
(IMPLIES (NOT (LISTP Z))
(p X Z PAIRS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
conjectures:
Case 3. (IMPLIES (AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(SUBSETP (CAR (PARTITION X (CDR Z) PAIRS))
(CDR Z)))
(SUBSETP (CAR (PARTITION X Z PAIRS))
Z)).
This simplifies, applying MEMBER-SUBSETP, SUBSETP-REFLEXIVITY, CAR-CONS,
SUBSETP-IS-TRANSITIVE, CDR-SUBSETP, and CDR-CONS, and opening up the
functions RELATED, PARTITION, MEMBER, and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(SUBSETP (CAR (PARTITION X (CDR Z) PAIRS))
(CDR Z)))
(SUBSETP (CAR (PARTITION X Z PAIRS))
Z)),
which simplifies, rewriting with CAR-CONS, CDR-SUBSETP, and
SUBSETP-IS-TRANSITIVE, and opening up RELATED and PARTITION, to:
T.
Case 1. (IMPLIES (NOT (LISTP Z))
(SUBSETP (CAR (PARTITION X Z PAIRS))
Z)).
This simplifies, unfolding the definitions of PARTITION, CAR, LISTP, and
SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-CAR-PARTITION
(PROVE-LEMMA SUBSETP-HOM-SET-DOMAIN-2
(REWRITE)
(IMPLIES (SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
P Q))
(CAR (PARTITION X Z PAIRS)))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
P Q))
(CONS X Z)))
((USE (SUBSETP-CAR-PARTITION))
(DISABLE SUBSETP-CAR-PARTITION)))
This formula simplifies, applying SUBSETP-IS-TRANSITIVE, SUBSETP-REFLEXIVITY,
and SUBSETP-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-HOM-SET-DOMAIN-2
(PROVE-LEMMA SUBSETP-HOM-SET-DOMAIN
(REWRITE)
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN))
Call the conjecture *1.
We will try to prove it by induction. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP DOMAIN) (ZEROP P))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (NOT (LISTP DOMAIN))
(p PAIRS DOMAIN P Q))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and ZEROP can be used to establish that the measure (PLUS P Q) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. Note, however, the inductive instances chosen for DOMAIN. The above
induction scheme generates the following seven new formulas:
Case 7. (IMPLIES (AND (LISTP DOMAIN) (ZEROP P))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)).
This simplifies, expanding the definitions of ZEROP, EQUAL, WIT, CAR, LISTP,
and SUBSETP, to:
T.
Case 6. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)).
This simplifies, opening up the functions ZEROP, EQUAL, WIT, CAR, LISTP, and
SUBSETP, to:
T.
Case 5. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)).
This simplifies, opening up the definitions of ZEROP, WIT, and EQUAL, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
DOMAIN)).
Applying the lemma CAR-CDR-ELIM, replace DOMAIN by (CONS X Z) to eliminate
(CAR DOMAIN) and (CDR DOMAIN). We would thus like to prove:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION X Z PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
1)
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION X Z PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
(CONS X Z))),
which further simplifies, appealing to the lemma SUBSETP-HOM-SET-DOMAIN-1,
to:
T.
Case 4. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)),
which simplifies, rewriting with the lemmas CAR-CONS and CDR-CONS, and
opening up the definitions of ZEROP, WIT, MEMBER, and SUBSETP, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
DOMAIN)).
Appealing to the lemma CAR-CDR-ELIM, we now replace DOMAIN by (CONS X Z) to
eliminate (CAR DOMAIN) and (CDR DOMAIN). This generates:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION X Z PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
1))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
(CDR (PARTITION X Z PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CDR (PARTITION X Z PAIRS))
P
(SUB1 Q)))
(CONS X Z))).
However this further simplifies, appealing to the lemma
SUBSETP-HOM-SET-DOMAIN-1, to:
T.
Case 3. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)),
which simplifies, opening up ZEROP, WIT, and EQUAL, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
DOMAIN)).
Appealing to the lemma CAR-CDR-ELIM, we now replace DOMAIN by (CONS X Z) to
eliminate (CAR DOMAIN) and (CDR DOMAIN). This generates:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION X Z PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
2)
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION X Z PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
(CONS X Z))).
This further simplifies, applying SUBSETP-HOM-SET-DOMAIN-2, to:
T.
Case 2. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)).
This simplifies, applying CAR-CONS and CDR-CONS, and expanding the
definitions of ZEROP, WIT, MEMBER, and SUBSETP, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
DOMAIN)).
Appealing to the lemma CAR-CDR-ELIM, we now replace DOMAIN by (CONS X Z) to
eliminate (CAR DOMAIN) and (CDR DOMAIN). This generates the goal:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION X Z PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
2))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
(CAR (PARTITION X Z PAIRS))))
(SUBSETP (CAR (WIT PAIRS
(CAR (PARTITION X Z PAIRS))
(SUB1 P)
Q))
(CONS X Z))).
But this further simplifies, applying SUBSETP-HOM-SET-DOMAIN-2, to:
T.
Case 1. (IMPLIES (NOT (LISTP DOMAIN))
(SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)).
This simplifies, opening up WIT, CAR, LISTP, and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
SUBSETP-HOM-SET-DOMAIN
(DEFN GOOD-HOM-SET
(PAIRS DOMAIN P Q FLG)
(AND (HOMOGENEOUS (CAR (WIT PAIRS DOMAIN P Q))
PAIRS FLG)
(NOT (LESSP (LENGTH (CAR (WIT PAIRS DOMAIN P Q)))
(IF (EQUAL FLG 1) P Q)))))
Observe that:
(OR (FALSEP (GOOD-HOM-SET PAIRS DOMAIN P Q FLG))
(TRUEP (GOOD-HOM-SET PAIRS DOMAIN P Q FLG)))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-HOM-SET
(PROVE-LEMMA HOMOGENEOUS1-SUBSET
(REWRITE)
(IMPLIES (AND (SUBSETP X DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG))
(HOMOGENEOUS1 ELT X PAIRS FLG)))
WARNING: Note that HOMOGENEOUS1-SUBSET contains the free variable DOMAIN
which will be chosen by instantiating the hypothesis (SUBSETP X DOMAIN).
Name the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP X)
(p ELT X PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) DOMAIN)
(p ELT (CDR X) PAIRS FLG DOMAIN))
(p ELT X PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) DOMAIN)))
(p ELT X PAIRS FLG DOMAIN))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP X)
(SUBSETP X DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG))
(HOMOGENEOUS1 ELT X PAIRS FLG)).
This simplifies, opening up NLISTP, SUBSETP, and HOMOGENEOUS1, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) DOMAIN)
(NOT (SUBSETP (CDR X) DOMAIN))
(SUBSETP X DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG))
(HOMOGENEOUS1 ELT X PAIRS FLG)).
This simplifies, rewriting with SUBSETP-REFLEXIVITY and MEMBER-SUBSETP, and
expanding the functions NLISTP and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(MEMBER (CAR X) DOMAIN)
(HOMOGENEOUS1 ELT (CDR X) PAIRS FLG)
(SUBSETP X DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG))
(HOMOGENEOUS1 ELT X PAIRS FLG)),
which simplifies, rewriting with SUBSETP-REFLEXIVITY and MEMBER-SUBSETP, and
unfolding NLISTP, SUBSETP, HOMOGENEOUS1, and RELATED, to the following three
new goals:
Case 2.3.
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) DOMAIN)
(HOMOGENEOUS1 ELT (CDR X) PAIRS FLG)
(SUBSETP (CDR X) DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS (CAR X) ELT) PAIRS))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to
eliminate (CAR X) and (CDR X). We must thus prove:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
Name the above subgoal *1.1.
Case 2.2.
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) DOMAIN)
(HOMOGENEOUS1 ELT (CDR X) PAIRS FLG)
(SUBSETP (CDR X) DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT (CAR X)) PAIRS))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to
eliminate (CAR X) and (CDR X). We must thus prove the goal:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
Call the above conjecture *1.2.
Case 2.1.
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) DOMAIN)
(HOMOGENEOUS1 ELT (CDR X) PAIRS FLG)
(SUBSETP (CDR X) DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(EQUAL FLG 1)
(NOT (MEMBER (CONS ELT (CAR X)) PAIRS)))
(MEMBER (CONS (CAR X) ELT) PAIRS)).
This again simplifies, clearly, to:
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) DOMAIN)
(HOMOGENEOUS1 ELT (CDR X) PAIRS 1)
(SUBSETP (CDR X) DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT (CAR X)) PAIRS)))
(MEMBER (CONS (CAR X) ELT) PAIRS)).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate
(CAR X) and (CDR X). This produces:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS 1)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)),
which we will name *1.3.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (MEMBER (CAR X) DOMAIN))
(SUBSETP X DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG))
(HOMOGENEOUS1 ELT X PAIRS FLG)).
This simplifies, opening up NLISTP and SUBSETP, to:
T.
So next consider:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS 1)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)),
named *1.3 above. Perhaps we can prove it by induction. Six inductions are
suggested by terms in the conjecture. They merge into three likely candidate
inductions. However, only one is unflawed. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP V)
(p Z ELT PAIRS DOMAIN (CDR V)))
(p Z ELT PAIRS DOMAIN V))
(IMPLIES (NOT (LISTP V))
(p Z ELT PAIRS DOMAIN V))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT V)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to the following three new
goals:
Case 3. (IMPLIES (AND (LISTP V)
(NOT (HOMOGENEOUS1 ELT (CDR V) PAIRS 1))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS 1)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, unfolding the definitions of HOMOGENEOUS1, EQUAL, and
RELATED, to:
T.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (SUBSETP (CDR V) DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS 1)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, opening up HOMOGENEOUS1, EQUAL, RELATED, and SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS 1)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, expanding HOMOGENEOUS1 and SUBSETP, to:
(IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)),
which we will name *1.3.1.
We will appeal to induction. The recursive terms in the conjecture
suggest four inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP DOMAIN)
(p Z ELT PAIRS DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN)))
(p Z ELT PAIRS DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(p Z ELT PAIRS (CDR DOMAIN)))
(p Z ELT PAIRS DOMAIN))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT DOMAIN) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following four new formulas:
Case 4. (IMPLIES (AND (NLISTP DOMAIN)
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, unfolding the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, expanding the definitions of NLISTP, MEMBER, HOMOGENEOUS1,
EQUAL, and RELATED, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (MEMBER Z (CDR DOMAIN)))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, unfolding NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (HOMOGENEOUS1 ELT
(CDR DOMAIN)
PAIRS 1))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS 1)
(NOT (MEMBER (CONS ELT Z) PAIRS)))
(MEMBER (CONS Z ELT) PAIRS)).
This simplifies, expanding NLISTP, MEMBER, HOMOGENEOUS1, EQUAL, and RELATED,
to:
T.
That finishes the proof of *1.3.1, which, consequently, also finishes the
proof of *1.3.
So we now return to:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))),
which we named *1.2 above. Perhaps we can prove it by induction. Five
inductions are suggested by terms in the conjecture. They merge into three
likely candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP V)
(p ELT Z PAIRS FLG DOMAIN (CDR V)))
(p ELT Z PAIRS FLG DOMAIN V))
(IMPLIES (NOT (LISTP V))
(p ELT Z PAIRS FLG DOMAIN V))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT V)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following three new
goals:
Case 3. (IMPLIES (AND (LISTP V)
(NOT (HOMOGENEOUS1 ELT (CDR V) PAIRS FLG))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
This simplifies, expanding the functions HOMOGENEOUS1 and RELATED, to:
T.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (SUBSETP (CDR V) DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
This simplifies, unfolding HOMOGENEOUS1, RELATED, and SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
This simplifies, unfolding HOMOGENEOUS1 and SUBSETP, to:
(IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))),
which has an irrelevant term in it. By eliminating the term we get the new
conjecture:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))),
which we will name *1.2.1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (NLISTP DOMAIN)
(p ELT Z PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN)))
(p ELT Z PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(p ELT Z PAIRS FLG (CDR DOMAIN)))
(p ELT Z PAIRS FLG DOMAIN))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT DOMAIN) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (NLISTP DOMAIN)
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))),
which simplifies, rewriting with MEMBER-SUBSETP and SUBSETP-REFLEXIVITY, and
expanding NLISTP, MEMBER, HOMOGENEOUS1, and RELATED, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (MEMBER Z (CDR DOMAIN)))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (HOMOGENEOUS1 ELT
(CDR DOMAIN)
PAIRS FLG))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS ELT Z) PAIRS))).
This simplifies, expanding the functions NLISTP, MEMBER, HOMOGENEOUS1, and
RELATED, to:
T.
That finishes the proof of *1.2.1, which, in turn, also finishes the
proof of *1.2.
So we now return to:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))),
which we named *1.1 above. Perhaps we can prove it by induction. There are
five plausible inductions. They merge into three likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP V)
(p Z ELT PAIRS FLG DOMAIN (CDR V)))
(p Z ELT PAIRS FLG DOMAIN V))
(IMPLIES (NOT (LISTP V))
(p Z ELT PAIRS FLG DOMAIN V))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT V)
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 (LISTP V)
(NOT (HOMOGENEOUS1 ELT (CDR V) PAIRS FLG))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
This simplifies, unfolding the functions HOMOGENEOUS1 and RELATED, to:
T.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (SUBSETP (CDR V) DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
This simplifies, opening up HOMOGENEOUS1, RELATED, and SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT V PAIRS FLG)
(SUBSETP V DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
This simplifies, opening up the definitions of HOMOGENEOUS1 and SUBSETP, to:
(IMPLIES (AND (NOT (LISTP V))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (AND (MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))),
which we will name *1.1.1.
We will appeal to induction. Three inductions are suggested by terms in
the conjecture. They merge into two likely candidate inductions. However,
only one is unflawed. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP DOMAIN)
(p Z ELT PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN)))
(p Z ELT PAIRS FLG DOMAIN))
(IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(p Z ELT PAIRS FLG (CDR DOMAIN)))
(p Z ELT PAIRS FLG DOMAIN))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT DOMAIN) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP DOMAIN)
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
This simplifies, unfolding NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(EQUAL Z (CAR DOMAIN))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))).
This simplifies, rewriting with MEMBER-SUBSETP and SUBSETP-REFLEXIVITY, and
expanding NLISTP, MEMBER, HOMOGENEOUS1, and RELATED, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (MEMBER Z (CDR DOMAIN)))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))),
which simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP DOMAIN))
(NOT (EQUAL Z (CAR DOMAIN)))
(NOT (HOMOGENEOUS1 ELT
(CDR DOMAIN)
PAIRS FLG))
(MEMBER Z DOMAIN)
(HOMOGENEOUS1 ELT DOMAIN PAIRS FLG)
(NOT (EQUAL FLG 1)))
(NOT (MEMBER (CONS Z ELT) PAIRS))),
which simplifies, opening up the functions NLISTP, MEMBER, HOMOGENEOUS1, and
RELATED, to:
T.
That finishes the proof of *1.1.1, which, consequently, finishes the
proof of *1.1, which, consequently, finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.1 ]
HOMOGENEOUS1-SUBSET
(PROVE-LEMMA HOMOGENEOUS1-CDR-PARTITION
(REWRITE)
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT DOM PAIRS))
PAIRS 2))
Name the conjecture *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP DOM)
(RELATED ELT (CAR DOM) PAIRS)
(p ELT (CDR DOM) PAIRS))
(p ELT DOM PAIRS))
(IMPLIES (AND (LISTP DOM)
(NOT (RELATED ELT (CAR DOM) PAIRS))
(p ELT (CDR DOM) PAIRS))
(p ELT DOM PAIRS))
(IMPLIES (NOT (LISTP DOM))
(p ELT DOM PAIRS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT DOM) 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 DOM)
(RELATED ELT (CAR DOM) PAIRS)
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT (CDR DOM) PAIRS))
PAIRS 2))
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT DOM PAIRS))
PAIRS 2)).
This simplifies, applying MEMBER-SUBSETP, SUBSETP-REFLEXIVITY, and CDR-CONS,
and expanding RELATED and PARTITION, to:
T.
Case 2. (IMPLIES (AND (LISTP DOM)
(NOT (RELATED ELT (CAR DOM) PAIRS))
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT (CDR DOM) PAIRS))
PAIRS 2))
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT DOM PAIRS))
PAIRS 2)),
which simplifies, applying CDR-CONS and CAR-CONS, and expanding the
functions RELATED, PARTITION, EQUAL, and HOMOGENEOUS1, to:
T.
Case 1. (IMPLIES (NOT (LISTP DOM))
(HOMOGENEOUS1 ELT
(CDR (PARTITION ELT DOM PAIRS))
PAIRS 2)).
This simplifies, unfolding the functions PARTITION, CDR, LISTP, and
HOMOGENEOUS1, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS1-CDR-PARTITION
(PROVE-LEMMA LENGTH-PARTITION-1 NIL
(EQUAL (LENGTH Z)
(PLUS (LENGTH (CAR (PARTITION X Z PAIRS)))
(LENGTH (CDR (PARTITION X Z PAIRS))))))
Call the conjecture *1.
Let us appeal to the induction principle. There are three plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(p (CDR Z) X PAIRS))
(p Z X PAIRS))
(IMPLIES (AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(p (CDR Z) X PAIRS))
(p Z X PAIRS))
(IMPLIES (NOT (LISTP Z))
(p Z X PAIRS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces three new formulas:
Case 3. (IMPLIES
(AND (LISTP Z)
(RELATED X (CAR Z) PAIRS)
(EQUAL (LENGTH (CDR Z))
(PLUS (LENGTH (CAR (PARTITION X (CDR Z) PAIRS)))
(LENGTH (CDR (PARTITION X (CDR Z) PAIRS))))))
(EQUAL (LENGTH Z)
(PLUS (LENGTH (CAR (PARTITION X Z PAIRS)))
(LENGTH (CDR (PARTITION X Z PAIRS)))))),
which simplifies, applying the lemmas MEMBER-SUBSETP, SUBSETP-REFLEXIVITY,
CAR-CONS, CDR-CONS, and SUB1-ADD1, and opening up RELATED, LENGTH, PARTITION,
and PLUS, to:
T.
Case 2. (IMPLIES
(AND (LISTP Z)
(NOT (RELATED X (CAR Z) PAIRS))
(EQUAL (LENGTH (CDR Z))
(PLUS (LENGTH (CAR (PARTITION X (CDR Z) PAIRS)))
(LENGTH (CDR (PARTITION X (CDR Z) PAIRS))))))
(EQUAL (LENGTH Z)
(PLUS (LENGTH (CAR (PARTITION X Z PAIRS)))
(LENGTH (CDR (PARTITION X Z PAIRS)))))),
which simplifies, applying CAR-CONS and CDR-CONS, and unfolding the
definitions of RELATED, LENGTH, and PARTITION, to:
(IMPLIES
(AND (LISTP Z)
(NOT (MEMBER (CONS X (CAR Z)) PAIRS))
(NOT (MEMBER (CONS (CAR Z) X) PAIRS))
(EQUAL (LENGTH (CDR Z))
(PLUS (LENGTH (CAR (PARTITION X (CDR Z) PAIRS)))
(LENGTH (CDR (PARTITION X (CDR Z) PAIRS))))))
(EQUAL (ADD1 (LENGTH (CDR Z)))
(PLUS (LENGTH (CAR (PARTITION X (CDR Z) PAIRS)))
(ADD1 (LENGTH (CDR (PARTITION X (CDR Z) PAIRS))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (NOT (LISTP Z))
(EQUAL (LENGTH Z)
(PLUS (LENGTH (CAR (PARTITION X Z PAIRS)))
(LENGTH (CDR (PARTITION X Z PAIRS)))))),
which simplifies, expanding LENGTH, PARTITION, CAR, CDR, PLUS, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-PARTITION-1
(PROVE-LEMMA LENGTH-PARTITION
(REWRITE)
(EQUAL (LENGTH (CAR (PARTITION X Z PAIRS)))
(DIFFERENCE (LENGTH Z)
(LENGTH (CDR (PARTITION X Z PAIRS)))))
((USE (LENGTH-PARTITION-1))))
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (LENGTH Z)
(LENGTH (CDR (PARTITION X Z PAIRS))))
(EQUAL (LENGTH Z)
(PLUS (LENGTH (CAR (PARTITION X Z PAIRS)))
(LENGTH (CDR (PARTITION X Z PAIRS))))))
(EQUAL (LENGTH (CAR (PARTITION X Z PAIRS)))
(DIFFERENCE (LENGTH Z)
(LENGTH (CDR (PARTITION X Z PAIRS)))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-PARTITION
(PROVE-LEMMA RAMSEY-NOT-ZERO
(REWRITE)
(LESSP 0 (RAMSEY P Q)))
WARNING: Note that the proposed lemma RAMSEY-NOT-ZERO 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 definitions of EQUAL and LESSP, to
the conjecture:
(NOT (EQUAL (RAMSEY P Q) 0)).
Name the above subgoal *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (ZEROP P) (p P Q))
(IMPLIES (AND (NOT (ZEROP P)) (ZEROP Q))
(p P Q))
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP Q))
(p P (SUB1 Q))
(p (SUB1 P) Q))
(p P Q))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of ZEROP, LESSP,
and PLUS can be used to prove that the measure (PLUS P Q) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates three new conjectures:
Case 3. (IMPLIES (ZEROP P)
(NOT (EQUAL (RAMSEY P Q) 0))),
which simplifies, unfolding ZEROP, EQUAL, and RAMSEY, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP P)) (ZEROP Q))
(NOT (EQUAL (RAMSEY P Q) 0))),
which simplifies, unfolding ZEROP, EQUAL, and RAMSEY, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (EQUAL (RAMSEY P (SUB1 Q)) 0))
(NOT (EQUAL (RAMSEY (SUB1 P) Q) 0)))
(NOT (EQUAL (RAMSEY P Q) 0))),
which simplifies, unfolding the functions ZEROP and RAMSEY, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL (RAMSEY P (SUB1 Q)) 0))
(NOT (EQUAL (RAMSEY (SUB1 P) Q) 0)))
(NOT (EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))).
But this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
RAMSEY-NOT-ZERO
(PROVE-LEMMA HOMOGENEOUS1-CAR-WIT-CDR-PARTITION
(REWRITE)
(HOMOGENEOUS1 ELT
(CAR (WIT PAIRS
(CDR (PARTITION ELT DOM PAIRS))
P Q))
PAIRS 2)
((USE (HOMOGENEOUS1-SUBSET (DOMAIN (CDR (PARTITION ELT DOM PAIRS)))
(FLG 2)
(X (CAR (WIT PAIRS
(CDR (PARTITION ELT DOM PAIRS))
P Q)))))
(DISABLE HOMOGENEOUS1-SUBSET)))
This formula simplifies, rewriting with SUBSETP-HOM-SET-DOMAIN and
HOMOGENEOUS1-CDR-PARTITION, and unfolding AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS1-CAR-WIT-CDR-PARTITION
(PROVE-LEMMA HOMOGENEOUS1-CAR-PARTITION
(REWRITE)
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT DOM PAIRS))
PAIRS 1))
Name the conjecture *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP DOM)
(RELATED ELT (CAR DOM) PAIRS)
(p ELT (CDR DOM) PAIRS))
(p ELT DOM PAIRS))
(IMPLIES (AND (LISTP DOM)
(NOT (RELATED ELT (CAR DOM) PAIRS))
(p ELT (CDR DOM) PAIRS))
(p ELT DOM PAIRS))
(IMPLIES (NOT (LISTP DOM))
(p ELT DOM PAIRS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT DOM) 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 DOM)
(RELATED ELT (CAR DOM) PAIRS)
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT (CDR DOM) PAIRS))
PAIRS 1))
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT DOM PAIRS))
PAIRS 1)).
This simplifies, applying MEMBER-SUBSETP, SUBSETP-REFLEXIVITY, CAR-CONS, and
CDR-CONS, and expanding RELATED, PARTITION, EQUAL, and HOMOGENEOUS1, to:
T.
Case 2. (IMPLIES (AND (LISTP DOM)
(NOT (RELATED ELT (CAR DOM) PAIRS))
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT (CDR DOM) PAIRS))
PAIRS 1))
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT DOM PAIRS))
PAIRS 1)),
which simplifies, applying CAR-CONS, and expanding the functions RELATED and
PARTITION, to:
T.
Case 1. (IMPLIES (NOT (LISTP DOM))
(HOMOGENEOUS1 ELT
(CAR (PARTITION ELT DOM PAIRS))
PAIRS 1)).
This simplifies, unfolding the functions PARTITION, CAR, LISTP, and
HOMOGENEOUS1, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS1-CAR-PARTITION
(PROVE-LEMMA HOMOGENEOUS1-CAR-WIT-CAR-PARTITION
(REWRITE)
(HOMOGENEOUS1 ELT
(CAR (WIT PAIRS
(CAR (PARTITION ELT DOM PAIRS))
P Q))
PAIRS 1)
((USE (HOMOGENEOUS1-SUBSET (DOMAIN (CAR (PARTITION ELT DOM PAIRS)))
(FLG 1)
(X (CAR (WIT PAIRS
(CAR (PARTITION ELT DOM PAIRS))
P Q)))))
(DISABLE HOMOGENEOUS1-SUBSET)))
This formula simplifies, rewriting with SUBSETP-HOM-SET-DOMAIN and
HOMOGENEOUS1-CAR-PARTITION, and unfolding AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
HOMOGENEOUS1-CAR-WIT-CAR-PARTITION
(PROVE-LEMMA CDR-WIT-IS-1-OR-2
(REWRITE)
(IMPLIES (NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)))
Call the conjecture *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture. However, they merge into one likely candidate induction. We
will induct according to the following scheme:
(AND
(IMPLIES (AND (LISTP DOM) (ZEROP P))
(p PAIRS DOM P Q))
(IMPLIES (AND (LISTP DOM)
(NOT (ZEROP P))
(ZEROP Q))
(p PAIRS DOM P Q))
(IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
1)
(p PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
(p PAIRS DOM P Q))
(IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
1))
(p PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
(p PAIRS DOM P Q))
(IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
2)
(p PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
(p PAIRS DOM P Q))
(IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
2))
(p PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
(p PAIRS DOM P Q))
(IMPLIES (NOT (LISTP DOM))
(p PAIRS DOM P Q))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and ZEROP inform us that the measure (PLUS P Q) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for DOM. The above induction scheme
leads to the following seven new conjectures:
Case 7. (IMPLIES (AND (LISTP DOM)
(ZEROP P)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)).
This simplifies, unfolding the functions ZEROP, EQUAL, WIT, and CDR, to:
T.
Case 6. (IMPLIES (AND (LISTP DOM)
(NOT (ZEROP P))
(ZEROP Q)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)).
This simplifies, expanding ZEROP, EQUAL, WIT, and CDR, to:
T.
Case 5. (IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
1)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)).
This simplifies, rewriting with LENGTH-PARTITION, and opening up the
functions ZEROP, WIT, and EQUAL, to:
T.
Case 4. (IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
1))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
P
(SUB1 Q)))
2)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)),
which simplifies, rewriting with LENGTH-PARTITION and CDR-CONS, and opening
up the functions ZEROP, EQUAL, and WIT, to:
T.
Case 3. (IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
2))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
1)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)).
This simplifies, applying LENGTH-PARTITION and CDR-CONS, and opening up the
functions ZEROP, EQUAL, and WIT, to:
T.
Case 2. (IMPLIES
(AND (LISTP DOM)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOM)
(CDR DOM)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOM) (CDR DOM) PAIRS))
(SUB1 P)
Q))
2)
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)),
which simplifies, rewriting with LENGTH-PARTITION, and opening up ZEROP, WIT,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP DOM))
(NOT (EQUAL (CDR (WIT PAIRS DOM P Q)) 1)))
(EQUAL (CDR (WIT PAIRS DOM P Q)) 2)).
This simplifies, expanding the definitions of WIT, CDR, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CDR-WIT-IS-1-OR-2
(PROVE-LEMMA WIT-YIELDS-GOOD-HOM-SET
(REWRITE)
(IMPLIES (NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q)))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))))
WARNING: Note that the rewrite rule WIT-YIELDS-GOOD-HOM-SET will be stored so
as to apply only to terms with the nonrecursive function symbol GOOD-HOM-SET.
This simplifies, expanding GOOD-HOM-SET, to three new goals:
Case 3. (IMPLIES (NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q)))
(HOMOGENEOUS (CAR (WIT PAIRS DOMAIN P Q))
PAIRS
(CDR (WIT PAIRS DOMAIN P Q)))),
which we will name *1.
Case 2. (IMPLIES (AND (NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q)))
(NOT (EQUAL (CDR (WIT PAIRS DOMAIN P Q))
1)))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS DOMAIN P Q)))
Q))),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q)))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which we named *1 above. We will appeal to induction. Three 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 DOMAIN) (ZEROP P))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (NOT (LISTP DOMAIN))
(p PAIRS DOMAIN P Q))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and ZEROP establish that the measure (PLUS P Q) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for DOMAIN. The above induction
scheme produces the following nine new formulas:
Case 9. (IMPLIES (AND (LISTP DOMAIN)
(ZEROP P)
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with the lemma SUB1-ADD1, and unfolding ZEROP,
LENGTH, EQUAL, RAMSEY, SUB1, NUMBERP, LESSP, WIT, CDR, HOMOGENEOUS, LISTP,
CAR, and GOOD-HOM-SET, to:
T.
Case 8. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q)
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with SUB1-ADD1, and expanding the functions ZEROP,
LENGTH, EQUAL, RAMSEY, SUB1, NUMBERP, LESSP, WIT, CDR, HOMOGENEOUS, LISTP,
CAR, and GOOD-HOM-SET, to:
T.
Case 7. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which simplifies, rewriting with the lemma SUB1-ADD1, and unfolding the
definitions of ZEROP, LENGTH, RAMSEY, LESSP, WIT, EQUAL, and GOOD-HOM-SET,
to four new formulas:
Case 7.4.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 7.3.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
P))),
which again simplifies, using linear arithmetic, to:
T.
Case 7.2.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 1)),
which further simplifies, applying the lemma LENGTH-PARTITION, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 1)).
This again simplifies, using linear arithmetic, to:
T.
Case 7.1.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
P))),
which further simplifies, rewriting with the lemma LENGTH-PARTITION, to
the goal:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
P))).
However this again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(GOOD-HOM-SET PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)
(CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which simplifies, applying SUB1-ADD1, and expanding ZEROP, EQUAL,
GOOD-HOM-SET, LENGTH, RAMSEY, LESSP, and WIT, to:
T.
Case 5. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))).
This simplifies, appealing to the lemmas SUB1-ADD1, CDR-WIT-IS-1-OR-2,
CDR-CONS, HOMOGENEOUS1-CAR-WIT-CDR-PARTITION, and CAR-CONS, and unfolding
ZEROP, LENGTH, RAMSEY, LESSP, WIT, EQUAL, HOMOGENEOUS, and GOOD-HOM-SET, to
the following four new formulas:
Case 5.4.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 2)).
This again simplifies, using linear arithmetic, to:
T.
Case 5.3.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(SUB1 Q)))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.2.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 2)),
which further simplifies, applying LENGTH-PARTITION, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
PAIRS 2)),
which again simplifies, using linear arithmetic, to:
T.
Case 5.1.
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(SUB1 Q)))),
which further simplifies, rewriting with LENGTH-PARTITION, to the new
formula:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(LESSP (LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY P (SUB1 Q)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(SUB1 Q)))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(GOOD-HOM-SET PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)
(CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which simplifies, applying the lemmas CDR-WIT-IS-1-OR-2, SUB1-ADD1, CDR-CONS,
HOMOGENEOUS1-CAR-WIT-CDR-PARTITION, and CAR-CONS, and expanding ZEROP, EQUAL,
GOOD-HOM-SET, LENGTH, RAMSEY, LESSP, WIT, and HOMOGENEOUS, to:
T.
Case 3. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(GOOD-HOM-SET PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which simplifies, rewriting with SUB1-ADD1 and CDR-WIT-IS-1-OR-2, and
opening up the functions ZEROP, EQUAL, GOOD-HOM-SET, LENGTH, RAMSEY, LESSP,
and WIT, to:
T.
Case 2. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(GOOD-HOM-SET PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with SUB1-ADD1, CDR-CONS,
HOMOGENEOUS1-CAR-WIT-CAR-PARTITION, CAR-CONS, and CDR-WIT-IS-1-OR-2, and
unfolding the functions ZEROP, GOOD-HOM-SET, LENGTH, RAMSEY, LESSP, WIT,
EQUAL, and HOMOGENEOUS, to four new goals:
Case 2.4.
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
1)
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(SUB1 P)))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS 1)),
which again simplifies, obviously, to:
T.
Case 2.3.
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
1)
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(SUB1 P)))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS 1)).
This again simplifies, clearly, to:
T.
Case 2.2.
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
1))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
Q))
(EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS 2)).
This again simplifies, using linear arithmetic and rewriting with
RAMSEY-NOT-ZERO, to:
T.
Case 2.1.
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS
(CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
1))
(NOT (LESSP (LENGTH (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
Q))
(NOT (LESSP (LENGTH (CDR DOMAIN))
(SUB1 (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))))))
(HOMOGENEOUS (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
PAIRS 2)).
But this again simplifies, rewriting with the lemma CDR-WIT-IS-1-OR-2, and
opening up the function EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP DOMAIN))
(NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q))))
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))),
which simplifies, unfolding the functions LENGTH, RAMSEY, EQUAL, LESSP, WIT,
CDR, HOMOGENEOUS, LISTP, CAR, and GOOD-HOM-SET, to:
(IMPLIES (AND (NOT (LISTP DOMAIN))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q))
(NOT (EQUAL (PLUS (RAMSEY (SUB1 P) Q)
(RAMSEY P (SUB1 Q)))
0))).
But this again simplifies, using linear arithmetic and applying
RAMSEY-NOT-ZERO, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.1 ]
WIT-YIELDS-GOOD-HOM-SET
(DEFN SETP
(X)
(IF (LISTP X)
(AND (NOT (MEMBER (CAR X) (CDR X)))
(SETP (CDR X)))
T))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SETP is accepted under the principle of definition.
From the definition we can conclude that:
(OR (FALSEP (SETP X))
(TRUEP (SETP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SETP
(PROVE-LEMMA SETP-PARTITION
(REWRITE)
(IMPLIES (SETP X)
(AND (SETP (CAR (PARTITION A X PAIRS)))
(SETP (CDR (PARTITION A X PAIRS))))))
WARNING: Note that the proposed lemma SETP-PARTITION 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 function AND, to two new goals:
Case 2. (IMPLIES (SETP X)
(SETP (CAR (PARTITION A X PAIRS)))),
which we will name *1.
Case 1. (IMPLIES (SETP X)
(SETP (CDR (PARTITION A X PAIRS)))),
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 (SETP X)
(SETP (CAR (PARTITION A X PAIRS))))
(IMPLIES (SETP X)
(SETP (CDR (PARTITION A X PAIRS))))).
We gave this the name *1 above. Perhaps we can prove it by induction. There
are four plausible inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X)
(RELATED A (CAR X) PAIRS)
(p A (CDR X) PAIRS))
(p A X PAIRS))
(IMPLIES (AND (LISTP X)
(NOT (RELATED A (CAR X) PAIRS))
(p A (CDR X) PAIRS))
(p A X PAIRS))
(IMPLIES (NOT (LISTP X))
(p A X PAIRS))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates ten new
formulas:
Case 10.(IMPLIES (AND (LISTP X)
(RELATED A (CAR X) PAIRS)
(NOT (SETP (CDR X)))
(SETP X))
(SETP (CAR (PARTITION A X PAIRS)))),
which simplifies, opening up RELATED and SETP, to:
T.
Case 9. (IMPLIES (AND (LISTP X)
(RELATED A (CAR X) PAIRS)
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(SETP X))
(SETP (CAR (PARTITION A X PAIRS)))),
which simplifies, applying MEMBER-SUBSETP, SUBSETP-REFLEXIVITY, CAR-CONS,
and CDR-CONS, and unfolding RELATED, SETP, and PARTITION, to the following
two new goals:
Case 9.2.
(IMPLIES (AND (LISTP X)
(MEMBER (CONS A (CAR X)) PAIRS)
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(NOT (MEMBER (CAR X) (CDR X)))
(SETP (CDR X)))
(NOT (MEMBER (CAR X)
(CAR (PARTITION A (CDR X) PAIRS))))).
But this again simplifies, applying the lemmas SUBSETP-CAR-PARTITION and
MEMBER-SUBSETP, to:
T.
Case 9.1.
(IMPLIES (AND (LISTP X)
(MEMBER (CONS (CAR X) A) PAIRS)
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(NOT (MEMBER (CAR X) (CDR X)))
(SETP (CDR X)))
(NOT (MEMBER (CAR X)
(CAR (PARTITION A (CDR X) PAIRS))))),
which again simplifies, rewriting with the lemmas SUBSETP-CAR-PARTITION
and MEMBER-SUBSETP, to:
T.
Case 8. (IMPLIES (AND (LISTP X)
(NOT (RELATED A (CAR X) PAIRS))
(NOT (SETP (CDR X)))
(SETP X))
(SETP (CAR (PARTITION A X PAIRS)))),
which simplifies, opening up RELATED and SETP, to:
T.
Case 7. (IMPLIES (AND (LISTP X)
(NOT (RELATED A (CAR X) PAIRS))
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(SETP X))
(SETP (CAR (PARTITION A X PAIRS)))),
which simplifies, applying CAR-CONS, and expanding the functions RELATED,
SETP, and PARTITION, to:
T.
Case 6. (IMPLIES (AND (NOT (LISTP X)) (SETP X))
(SETP (CAR (PARTITION A X PAIRS)))).
This simplifies, opening up the definitions of SETP, PARTITION, and CAR, to:
T.
Case 5. (IMPLIES (AND (LISTP X)
(RELATED A (CAR X) PAIRS)
(NOT (SETP (CDR X)))
(SETP X))
(SETP (CDR (PARTITION A X PAIRS)))).
This simplifies, unfolding the definitions of RELATED and SETP, to:
T.
Case 4. (IMPLIES (AND (LISTP X)
(RELATED A (CAR X) PAIRS)
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(SETP X))
(SETP (CDR (PARTITION A X PAIRS)))).
This simplifies, rewriting with the lemmas MEMBER-SUBSETP,
SUBSETP-REFLEXIVITY, and CDR-CONS, and expanding RELATED, SETP, and
PARTITION, to:
T.
Case 3. (IMPLIES (AND (LISTP X)
(NOT (RELATED A (CAR X) PAIRS))
(NOT (SETP (CDR X)))
(SETP X))
(SETP (CDR (PARTITION A X PAIRS)))).
This simplifies, opening up the functions RELATED and SETP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (RELATED A (CAR X) PAIRS))
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(SETP X))
(SETP (CDR (PARTITION A X PAIRS)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
functions RELATED, SETP, and PARTITION, to:
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CONS A (CAR X)) PAIRS))
(NOT (MEMBER (CONS (CAR X) A) PAIRS))
(SETP (CAR (PARTITION A (CDR X) PAIRS)))
(SETP (CDR (PARTITION A (CDR X) PAIRS)))
(NOT (MEMBER (CAR X) (CDR X)))
(SETP (CDR X)))
(NOT (MEMBER (CAR X)
(CDR (PARTITION A (CDR X) PAIRS))))).
But this again simplifies, applying the lemmas SUBSETP-CDR-PARTITION and
MEMBER-SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X)) (SETP X))
(SETP (CDR (PARTITION A X PAIRS)))),
which simplifies, unfolding SETP, PARTITION, and CDR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SETP-PARTITION
(PROVE-LEMMA NOT-MEMBER-CAR-WIT-CDR-PARTITION
(REWRITE)
(IMPLIES (NOT (MEMBER Z X))
(NOT (MEMBER Z
(CAR (WIT PAIRS
(CDR (PARTITION Z X PAIRS))
P Q)))))
((USE (MEMBER-SUBSETP (Y (CAR (WIT PAIRS
(CDR (PARTITION Z X PAIRS))
P Q)))
(X Z)
(Z X))
(SUBSETP-IS-TRANSITIVE (X (CAR (WIT PAIRS
(CDR (PARTITION Z X PAIRS))
P Q)))
(Y (CDR (PARTITION Z X PAIRS)))
(Z X)))))
This simplifies, applying SUBSETP-REFLEXIVITY, MEMBER-SUBSETP,
SUBSETP-HOM-SET-DOMAIN, and SUBSETP-CDR-PARTITION, and expanding AND and
IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NOT-MEMBER-CAR-WIT-CDR-PARTITION
(PROVE-LEMMA NOT-MEMBER-CAR-WIT-CAR-PARTITION
(REWRITE)
(IMPLIES (NOT (MEMBER Z X))
(NOT (MEMBER Z
(CAR (WIT PAIRS
(CAR (PARTITION Z X PAIRS))
P Q)))))
((USE (MEMBER-SUBSETP (Y (CAR (WIT PAIRS
(CAR (PARTITION Z X PAIRS))
P Q)))
(X Z)
(Z X))
(SUBSETP-IS-TRANSITIVE (X (CAR (WIT PAIRS
(CAR (PARTITION Z X PAIRS))
P Q)))
(Y (CAR (PARTITION Z X PAIRS)))
(Z X)))))
This simplifies, applying SUBSETP-REFLEXIVITY, MEMBER-SUBSETP,
SUBSETP-HOM-SET-DOMAIN, and SUBSETP-CAR-PARTITION, and expanding AND and
IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NOT-MEMBER-CAR-WIT-CAR-PARTITION
(PROVE-LEMMA SETP-HOM-SET
(REWRITE)
(IMPLIES (SETP DOMAIN)
(SETP (CAR (WIT PAIRS DOMAIN P Q)))))
Give the conjecture the name *1.
We will try to prove it by induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP DOMAIN) (ZEROP P))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(p PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(p PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
(p PAIRS DOMAIN P Q))
(IMPLIES (NOT (LISTP DOMAIN))
(p PAIRS DOMAIN P Q))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and ZEROP inform us that the measure (PLUS P Q) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for DOMAIN. The above induction
scheme generates 11 new goals:
Case 11.(IMPLIES (AND (LISTP DOMAIN)
(ZEROP P)
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, expanding ZEROP, SETP, EQUAL, WIT, and CAR, to:
T.
Case 10.(IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(ZEROP Q)
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, opening up the functions ZEROP, SETP, EQUAL, WIT, and CAR,
to:
T.
Case 9. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(NOT (SETP (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, applying the lemma LENGTH-PARTITION, and unfolding the
definitions of ZEROP, SETP, WIT, and EQUAL, to the formula:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(NOT (SETP (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(NOT (MEMBER (CAR DOMAIN) (CDR DOMAIN)))
(SETP (CDR DOMAIN)))
(SETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))).
But this further simplifies, appealing to the lemma SETP-PARTITION, to:
T.
Case 8. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1)
(SETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, applying LENGTH-PARTITION, and unfolding the functions
ZEROP, SETP, WIT, and EQUAL, to:
T.
Case 7. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(NOT (SETP (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with LENGTH-PARTITION, CDR-WIT-IS-1-OR-2,
CAR-CONS, NOT-MEMBER-CAR-WIT-CDR-PARTITION, and CDR-CONS, and expanding
ZEROP, SETP, WIT, and EQUAL, to:
(IMPLIES (AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(NOT (SETP (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(NOT (MEMBER (CAR DOMAIN) (CDR DOMAIN)))
(SETP (CDR DOMAIN)))
(SETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))).
But this further simplifies, appealing to the lemma SETP-PARTITION, to:
T.
Case 6. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q))
(NOT (EQUAL (CDR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q)))
1))
(SETP (CAR (WIT PAIRS
(CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
P
(SUB1 Q))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, rewriting with LENGTH-PARTITION, CDR-WIT-IS-1-OR-2,
CAR-CONS, NOT-MEMBER-CAR-WIT-CDR-PARTITION, and CDR-CONS, and unfolding the
functions ZEROP, SETP, WIT, and EQUAL, to:
T.
Case 5. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(NOT (SETP (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))).
This simplifies, applying LENGTH-PARTITION and CDR-WIT-IS-1-OR-2, and
opening up the functions ZEROP, SETP, WIT, and EQUAL, to the goal:
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(NOT (SETP (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(NOT (MEMBER (CAR DOMAIN) (CDR DOMAIN)))
(SETP (CDR DOMAIN)))
(SETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))).
This further simplifies, applying SETP-PARTITION, to:
T.
Case 4. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2)
(SETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with LENGTH-PARTITION and CDR-WIT-IS-1-OR-2, and
expanding the definitions of ZEROP, SETP, WIT, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(NOT (SETP (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, rewriting with the lemmas LENGTH-PARTITION, CAR-CONS,
NOT-MEMBER-CAR-WIT-CAR-PARTITION, and CDR-CONS, and unfolding the functions
ZEROP, SETP, and WIT, to:
(IMPLIES
(AND (LISTP DOMAIN)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (LESSP (DIFFERENCE (LENGTH (CDR DOMAIN))
(LENGTH (CDR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(NOT (SETP (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))))
(NOT (MEMBER (CAR DOMAIN) (CDR DOMAIN)))
(SETP (CDR DOMAIN)))
(SETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))).
But this further simplifies, applying SETP-PARTITION, to:
T.
Case 2. (IMPLIES (AND (LISTP DOMAIN)
(NOT (ZEROP P))
(NOT (ZEROP Q))
(NOT (LESSP (LENGTH (CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS)))
(RAMSEY (SUB1 P) Q)))
(NOT (EQUAL (CDR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q))
2))
(SETP (CAR (WIT PAIRS
(CAR (PARTITION (CAR DOMAIN)
(CDR DOMAIN)
PAIRS))
(SUB1 P)
Q)))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))).
This simplifies, rewriting with LENGTH-PARTITION, CAR-CONS,
NOT-MEMBER-CAR-WIT-CAR-PARTITION, and CDR-CONS, and opening up the functions
ZEROP, SETP, and WIT, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP DOMAIN))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))),
which simplifies, opening up the definitions of SETP, WIT, and CAR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
SETP-HOM-SET
(PROVE-LEMMA RAMSEY-THEOREM-2
(REWRITE)
(IMPLIES (LEQ (RAMSEY P Q) (LENGTH DOMAIN))
(AND (SUBSETP (CAR (WIT PAIRS DOMAIN P Q))
DOMAIN)
(GOOD-HOM-SET PAIRS DOMAIN P Q
(CDR (WIT PAIRS DOMAIN P Q)))
(IMPLIES (SETP DOMAIN)
(SETP (CAR (WIT PAIRS DOMAIN P Q))))))
((DISABLE GOOD-HOM-SET)))
WARNING: the previously added lemma, SUBSETP-HOM-SET-DOMAIN, could be applied
whenever the newly proposed RAMSEY-THEOREM-2 could!
WARNING: Note that the rewrite rule RAMSEY-THEOREM-2 will be stored so as to
apply only to terms with the nonrecursive function symbol GOOD-HOM-SET.
WARNING: the previously added lemma, WIT-YIELDS-GOOD-HOM-SET, could be
applied whenever the newly proposed RAMSEY-THEOREM-2 could!
WARNING: the previously added lemma, SETP-HOM-SET, could be applied whenever
the newly proposed RAMSEY-THEOREM-2 could!
WARNING: Note that the proposed lemma RAMSEY-THEOREM-2 is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This formula simplifies, applying the lemmas SUBSETP-HOM-SET-DOMAIN and
WIT-YIELDS-GOOD-HOM-SET, and unfolding the functions IMPLIES and AND, to:
(IMPLIES (AND (NOT (LESSP (LENGTH DOMAIN) (RAMSEY P Q)))
(SETP DOMAIN))
(SETP (CAR (WIT PAIRS DOMAIN P Q)))).
This again simplifies, appealing to the lemma SETP-HOM-SET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
RAMSEY-THEOREM-2