(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(DEFN ONES
(N)
(IF (ZEROP N)
NIL
(CONS 1 (ONES (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, ONES is accepted under the
definitional principle. From the definition we can conclude that:
(OR (LITATOM (ONES N))
(LISTP (ONES N)))
is a theorem.
[ 0.0 0.0 0.0 ]
ONES
(DEFN ALL-ONES
(S)
(IF (LISTP S)
(AND (EQUAL (CAR S) 1)
(ALL-ONES (CDR S)))
(EQUAL S NIL)))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT S) decreases according to the well-founded relation LESSP in each
recursive call. Hence, ALL-ONES is accepted under the definitional principle.
Note that (OR (FALSEP (ALL-ONES S)) (TRUEP (ALL-ONES S))) is a theorem.
[ 0.0 0.0 0.0 ]
ALL-ONES
(DEFN LENGTH
(S)
(IF (LISTP S)
(ADD1 (LENGTH (CDR S)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT S) 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 S)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN SUBSEQ
(S1 S2)
(IF (EQUAL S1 S2)
T
(IF (NLISTP S2)
F
(SUBSEQ S1 (CDR S2)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure (COUNT S2)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, SUBSEQ is accepted under the principle of definition. Note that:
(OR (FALSEP (SUBSEQ S1 S2))
(TRUEP (SUBSEQ S1 S2)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBSEQ
(PROVE-LEMMA SUBSEQ-ALL-ONES
(REWRITE)
(IMPLIES (AND (ALL-ONES S1) (SUBSEQ S2 S1))
(ALL-ONES S2)))
WARNING: Note that SUBSEQ-ALL-ONES contains the free variable S1 which will
be chosen by instantiating the hypothesis (ALL-ONES S1).
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest three inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP S1) (p S2 (CDR S1)))
(p S2 S1))
(IMPLIES (NOT (LISTP S1)) (p S2 S1))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT S1) 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 S1)
(NOT (ALL-ONES (CDR S1)))
(ALL-ONES S1)
(SUBSEQ S2 S1))
(ALL-ONES S2)).
This simplifies, expanding the definition of ALL-ONES, to:
T.
Case 2. (IMPLIES (AND (LISTP S1)
(NOT (SUBSEQ S2 (CDR S1)))
(ALL-ONES S1)
(SUBSEQ S2 S1))
(ALL-ONES S2)).
This simplifies, expanding the definitions of ALL-ONES, SUBSEQ, and EQUAL,
to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP S1))
(ALL-ONES S1)
(SUBSEQ S2 S1))
(ALL-ONES S2)).
This simplifies, opening up the functions ALL-ONES, LISTP, and SUBSEQ, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSEQ-ALL-ONES
(DEFN PLISTP
(S)
(IF (LISTP S)
(PLISTP (CDR S))
(EQUAL S NIL)))
Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT S) decreases according to the well-founded relation LESSP
in each recursive call. Hence, PLISTP is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (PLISTP S))
(TRUEP (PLISTP S)))
is a theorem.
[ 0.0 0.0 0.0 ]
PLISTP
(PROVE-LEMMA PLISTP-ALL-ONES
(REWRITE)
(IMPLIES (ALL-ONES S) (PLISTP S)))
Call the conjecture *1.
Perhaps we can 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 S) (p (CDR S)))
(p S))
(IMPLIES (NOT (LISTP S)) (p S))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
goals:
Case 3. (IMPLIES (AND (LISTP S)
(NOT (ALL-ONES (CDR S)))
(ALL-ONES S))
(PLISTP S)).
This simplifies, expanding the definition of ALL-ONES, to:
T.
Case 2. (IMPLIES (AND (LISTP S)
(PLISTP (CDR S))
(ALL-ONES S))
(PLISTP S)).
This simplifies, expanding ALL-ONES and PLISTP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP S)) (ALL-ONES S))
(PLISTP S)).
This simplifies, unfolding the functions ALL-ONES and PLISTP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PLISTP-ALL-ONES
(PROVE-LEMMA ALL-ONES-ONES
(REWRITE)
(ALL-ONES (ONES N)))
Call the conjecture *1.
Let us appeal to the induction principle. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to two new goals:
Case 2. (IMPLIES (ZEROP N)
(ALL-ONES (ONES N))),
which simplifies, expanding the definitions of ZEROP, ONES, and ALL-ONES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-ONES (ONES (SUB1 N))))
(ALL-ONES (ONES N))),
which simplifies, applying SUBSEQ-ALL-ONES, CDR-CONS, and CAR-CONS, and
expanding ZEROP, ONES, SUBSEQ, EQUAL, and ALL-ONES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-ONES-ONES
(PROVE-LEMMA ONES-IS-INJECTIVE
(REWRITE)
(IMPLIES (AND (NUMBERP I)
(NUMBERP J)
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J))))
((INDUCT (LESSP I J))))
This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
and AND, to three new formulas:
Case 3. (IMPLIES (AND (OR (EQUAL J 0) (NOT (NUMBERP J)))
(NUMBERP I)
(NUMBERP J)
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J)))),
which simplifies, opening up the definitions of NOT, OR, NUMBERP, and ONES,
to:
(IMPLIES (AND (EQUAL J 0)
(NUMBERP I)
(NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))).
This again simplifies, trivially, to the new conjecture:
(IMPLIES (AND (NUMBERP I) (NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))),
which we will name *1.
Case 2. (IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(OR (EQUAL I 0) (NOT (NUMBERP I)))
(NUMBERP I)
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J)))).
This simplifies, expanding NOT, OR, NUMBERP, and ONES, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(EQUAL I 0))
(NOT (EQUAL NIL (ONES J)))),
which again simplifies, obviously, to:
(IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J))
(NOT (EQUAL NIL (ONES J)))),
which we will name *2.
Case 1. (IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL I 0))
(NUMBERP I)
(IMPLIES (AND (NUMBERP (SUB1 I))
(NUMBERP (SUB1 J))
(NOT (EQUAL (SUB1 I) (SUB1 J))))
(NOT (EQUAL (ONES (SUB1 I))
(ONES (SUB1 J)))))
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J)))).
This simplifies, appealing to the lemmas CAR-CONS and CDR-CONS, and opening
up the definitions of NOT, AND, IMPLIES, ONES, and EQUAL, to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (SUB1 I) (SUB1 J)))
(EQUAL I J)),
which again simplifies, using linear arithmetic, to:
T.
So we now return to:
(IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J))
(NOT (EQUAL NIL (ONES J)))),
which is formula *2 above. What luck! This conjecture is subsumed by
formula *1 above.
So let us turn our attention to:
(IMPLIES (AND (NUMBERP I) (NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))),
which we named *1 above. Let us appeal to the induction principle. There is
only one suggested induction. We will induct according to the following
scheme:
(AND (IMPLIES (ZEROP I) (p I))
(IMPLIES (AND (NOT (ZEROP I)) (p (SUB1 I)))
(p I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT I) 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 (ZEROP I)
(NUMBERP I)
(NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))),
which simplifies, opening up the definition of ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP I))
(EQUAL (SUB1 I) 0)
(NUMBERP I)
(NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))),
which simplifies, opening up ZEROP and ONES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP I))
(NOT (EQUAL (ONES (SUB1 I)) NIL))
(NUMBERP I)
(NOT (EQUAL I 0)))
(NOT (EQUAL (ONES I) NIL))),
which simplifies, unfolding the functions ZEROP and ONES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ONES-IS-INJECTIVE
(CONSTRAIN KOENIG-INTRO
(REWRITE)
(AND (NODE-P NIL)
(OR (TRUEP (NODE-P S))
(FALSEP (NODE-P S)))
(IMPLIES (NODE-P S)
(EQUAL (NODE-P (CONS N S))
(AND (LESSP 0 N)
(NOT (LESSP (SUCCARD S) N)))))
(IMPLIES (AND (NODE-P S1) (SUBSEQ S S1))
(NODE-P S))
(NODE-P (S-N N))
(IMPLIES (AND (NUMBERP I)
(NUMBERP J)
(NOT (EQUAL I J)))
(NOT (EQUAL (S-N I) (S-N J))))
(IMPLIES (NOT (PLISTP S))
(NOT (NODE-P S))))
((NODE-P ALL-ONES)
(SUCCARD (LAMBDA (S) 1))
(S-N ONES))
((DISABLE SUBSEQ)))
WARNING: Note that KOENIG-INTRO contains the free variable S1 which will be
chosen by instantiating the hypothesis (NODE-P S1).
WARNING: Note that the proposed lemma KOENIG-INTRO is to be stored as one
type prescription rule, zero compound recognizer rules, zero linear rules, and
six replacement rules.
We will verify the consistency and the conservative nature of this constraint
by attempting to prove:
(AND (ALL-ONES NIL)
(OR (TRUEP (ALL-ONES S))
(FALSEP (ALL-ONES S)))
(IMPLIES (ALL-ONES S)
(EQUAL (ALL-ONES (CONS N S))
(AND (LESSP 0 N) (NOT (LESSP 1 N)))))
(IMPLIES (AND (ALL-ONES S1) (SUBSEQ S S1))
(ALL-ONES S))
(ALL-ONES (ONES N))
(IMPLIES (AND (NUMBERP I)
(NUMBERP J)
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J))))
(IMPLIES (NOT (PLISTP S))
(NOT (ALL-ONES S)))).
This conjecture can be simplified, using the abbreviations NOT, IMPLIES, OR,
and AND, to seven new conjectures:
Case 7. (ALL-ONES NIL),
which simplifies, unfolding the definition of ALL-ONES, to:
T.
Case 6. (IMPLIES (NOT (TRUEP (ALL-ONES S)))
(FALSEP (ALL-ONES S))),
which simplifies, obviously, to:
T.
Case 5. (IMPLIES (ALL-ONES S)
(EQUAL (ALL-ONES (CONS N S))
(AND (LESSP 0 N) (NOT (LESSP 1 N))))).
This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
functions ALL-ONES, EQUAL, LESSP, NOT, and AND, to four new conjectures:
Case 5.4.
(IMPLIES (AND (ALL-ONES S)
(NOT (EQUAL N 1))
(NOT (EQUAL N 0))
(NUMBERP N))
(LESSP 1 N)),
which again simplifies, using linear arithmetic, to:
T.
Case 5.3.
(IMPLIES (AND (ALL-ONES S) (EQUAL N 1))
(NOT (LESSP 1 N))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.2.
(IMPLIES (AND (ALL-ONES S) (EQUAL N 1))
(NUMBERP N)),
which again simplifies, trivially, to:
T.
Case 5.1.
(IMPLIES (AND (ALL-ONES S) (EQUAL N 1))
(NOT (EQUAL N 0))).
This again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (ALL-ONES S1) (SUBSEQ S S1))
(ALL-ONES S)),
which simplifies, rewriting with SUBSEQ-ALL-ONES, to:
T.
Case 3. (ALL-ONES (ONES N)).
This simplifies, rewriting with ALL-ONES-ONES, to:
T.
Case 2. (IMPLIES (AND (NUMBERP I)
(NUMBERP J)
(NOT (EQUAL I J)))
(NOT (EQUAL (ONES I) (ONES J)))),
which simplifies, applying the lemma ONES-IS-INJECTIVE, to:
T.
Case 1. (IMPLIES (NOT (PLISTP S))
(NOT (ALL-ONES S))),
which simplifies, applying PLISTP-ALL-ONES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KOENIG-INTRO
(DEFN SUCC-AUX
(S N)
(IF (ZEROP N)
NIL
(CONS (CONS N S)
(SUCC-AUX S (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, SUCC-AUX is
accepted under the definitional principle. From the definition we can
conclude that (OR (LITATOM (SUCC-AUX S N)) (LISTP (SUCC-AUX S N))) is a
theorem.
[ 0.0 0.0 0.0 ]
SUCC-AUX
(DEFN SUCCESSORS
(S)
(SUCC-AUX S (SUCCARD S)))
Observe that (OR (LITATOM (SUCCESSORS S)) (LISTP (SUCCESSORS S))) is a
theorem.
[ 0.0 0.0 0.0 ]
SUCCESSORS
(DEFN SUCCESSORS-LIST
(SS)
(IF (LISTP SS)
(APPEND (SUCCESSORS (CAR SS))
(SUCCESSORS-LIST (CDR SS)))
NIL))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT SS) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SUCCESSORS-LIST is accepted under the definitional
principle. Observe that:
(OR (LITATOM (SUCCESSORS-LIST SS))
(LISTP (SUCCESSORS-LIST SS)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUCCESSORS-LIST
(DEFN LEVEL
(N)
(IF (ZEROP N)
(LIST NIL)
(SUCCESSORS-LIST (LEVEL (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, LEVEL is accepted
under the principle of definition. From the definition we can conclude that:
(OR (LITATOM (LEVEL N))
(LISTP (LEVEL N)))
is a theorem.
[ 0.0 0.0 0.0 ]
LEVEL
(DEFN INIT-TREE
(N)
(IF (ZEROP N)
(LIST NIL)
(APPEND (LEVEL N)
(INIT-TREE (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, INIT-TREE is
accepted under the definitional principle. Note that (LISTP (INIT-TREE N)) is
a theorem.
[ 0.0 0.0 0.0 ]
INIT-TREE
(DEFN REMOVE1
(A X)
(IF (LISTP X)
(IF (EQUAL A (CAR X))
(CDR X)
(CONS (CAR X) (REMOVE1 A (CDR X))))
X))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, REMOVE1 is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
REMOVE1
(PROVE-LEMMA LENGTH-REMOVE1
(REWRITE)
(IMPLIES (MEMBER A X)
(LESSP (LENGTH (REMOVE1 A X))
(LENGTH X))))
WARNING: Note that the proposed lemma LENGTH-REMOVE1 is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP X) (p A X))
(IMPLIES (AND (NOT (NLISTP X))
(EQUAL A (CAR X)))
(p A X))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL A (CAR X)))
(p A (CDR X)))
(p A X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP 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 leads to the following four new goals:
Case 4. (IMPLIES (AND (NLISTP X) (MEMBER A X))
(LESSP (LENGTH (REMOVE1 A X))
(LENGTH X))).
This simplifies, expanding the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(EQUAL A (CAR X))
(MEMBER A X))
(LESSP (LENGTH (REMOVE1 A X))
(LENGTH X))).
This simplifies, rewriting with SUB1-ADD1, and unfolding the functions
NLISTP, MEMBER, REMOVE1, LENGTH, and LESSP, to the conjecture:
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (LENGTH (CDR X)) 0)))
(LESSP (SUB1 (LENGTH (CDR X)))
(LENGTH (CDR X)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL A (CAR X)))
(NOT (MEMBER A (CDR X)))
(MEMBER A X))
(LESSP (LENGTH (REMOVE1 A X))
(LENGTH X))),
which simplifies, unfolding the definitions of NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL A (CAR X)))
(LESSP (LENGTH (REMOVE1 A (CDR X)))
(LENGTH (CDR X)))
(MEMBER A X))
(LESSP (LENGTH (REMOVE1 A X))
(LENGTH X))),
which simplifies, applying the lemmas CDR-CONS and SUB1-ADD1, and opening up
the functions NLISTP, MEMBER, REMOVE1, LENGTH, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-REMOVE1
(DEFN FIRST-NON-MEMBER-INDEX
(I X)
(IF (MEMBER (S-N I) X)
(FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X))
I)
((LESSP (LENGTH X))))
Linear arithmetic and the lemma LENGTH-REMOVE1 inform us that the measure
(LENGTH X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, FIRST-NON-MEMBER-INDEX is accepted under the
definitional principle. Note that:
(OR (NUMBERP (FIRST-NON-MEMBER-INDEX I X))
(EQUAL (FIRST-NON-MEMBER-INDEX I X)
I))
is a theorem.
[ 0.0 0.0 0.0 ]
FIRST-NON-MEMBER-INDEX
(DEFN NTHCDR
(N S)
(IF (ZEROP N)
S
(NTHCDR (SUB1 N) (CDR S))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, NTHCDR is accepted under the
principle of definition.
[ 0.0 0.0 0.0 ]
NTHCDR
(DEFN S-HEIGHT
(N)
(NTHCDR (DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N)
(S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N)))))
[ 0.0 0.0 0.0 ]
S-HEIGHT
(PROVE-LEMMA NTHCDR-SUBSEQ
(REWRITE)
(IMPLIES (NOT (LESSP (LENGTH S) N))
(SUBSEQ (NTHCDR N S) S)))
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest four inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N)))
(p N S))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH S) 0)
(NOT (NUMBERP (LENGTH S)))))
(p N S))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH S) 0)
(NOT (NUMBERP (LENGTH S)))))
(p (SUB1 N) (CDR S)))
(p N S))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to show that the measure (COUNT N) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. Note, however, the inductive instance chosen for S. The above
induction scheme leads to the following four new goals:
Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(NOT (LESSP (LENGTH S) N)))
(SUBSEQ (NTHCDR N S) S)).
This simplifies, expanding the definitions of NOT, OR, LENGTH, EQUAL, LESSP,
NTHCDR, and SUBSEQ, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH S) 0)
(NOT (NUMBERP (LENGTH S))))
(NOT (LESSP (LENGTH S) N)))
(SUBSEQ (NTHCDR N S) S)).
This simplifies, unfolding NOT, OR, LENGTH, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH S) 0)
(NOT (NUMBERP (LENGTH S)))))
(LESSP (LENGTH (CDR S)) (SUB1 N))
(NOT (LESSP (LENGTH S) N)))
(SUBSEQ (NTHCDR N S) S)).
This simplifies, rewriting with SUB1-ADD1, and expanding the definitions of
NOT, OR, LENGTH, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH S) 0)
(NOT (NUMBERP (LENGTH S)))))
(SUBSEQ (NTHCDR (SUB1 N) (CDR S))
(CDR S))
(NOT (LESSP (LENGTH S) N)))
(SUBSEQ (NTHCDR N S) S)),
which simplifies, applying SUB1-ADD1, and opening up NOT, OR, LENGTH, LESSP,
NTHCDR, and SUBSEQ, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
NTHCDR-SUBSEQ
(PROVE-LEMMA NODE-P-NTHCDR
(REWRITE)
(IMPLIES (AND (NODE-P S)
(NOT (LESSP (LENGTH S) N)))
(NODE-P (NTHCDR N S))))
This formula simplifies, applying NTHCDR-SUBSEQ and KOENIG-INTRO, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NODE-P-NTHCDR
(PROVE-LEMMA LESSP-DIFFERENCE-1
(REWRITE)
(EQUAL (LESSP X (DIFFERENCE X N)) F))
This conjecture simplifies, using linear arithmetic, to the new conjecture:
(IMPLIES (LESSP X N)
(NOT (LESSP X (DIFFERENCE X N)))),
which we will name *1.
Perhaps we can prove it by induction. There are five plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N)))
(p X N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X))))
(p X N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(p (SUB1 X) (SUB1 N)))
(p X N))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT 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. Note, however, the inductive instance chosen for N. The above
induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(LESSP X N))
(NOT (LESSP X (DIFFERENCE X N)))),
which simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X)))
(LESSP X N))
(NOT (LESSP X (DIFFERENCE X N)))),
which simplifies, unfolding the definitions of NOT, OR, EQUAL, LESSP, and
DIFFERENCE, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 N)))
(LESSP X N))
(NOT (LESSP X (DIFFERENCE X N)))),
which simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP X 1)
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 N)))
(LESSP X N))
(NOT (LESSP X (DIFFERENCE X N)))).
This again simplifies, opening up the functions SUB1, NUMBERP, EQUAL, LESSP,
NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X)
(DIFFERENCE (SUB1 X) (SUB1 N))))
(LESSP X N))
(NOT (LESSP X (DIFFERENCE X N)))),
which simplifies, unfolding the functions NOT, OR, LESSP, and DIFFERENCE, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (LESSP (SUB1 X)
(DIFFERENCE (SUB1 X) (SUB1 N))))
(LESSP (SUB1 X) (SUB1 N)))
(NOT (LESSP X
(DIFFERENCE (SUB1 X) (SUB1 N))))).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
(SUB1 X). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. This generates:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (LESSP Z (DIFFERENCE Z (SUB1 N))))
(LESSP Z (SUB1 N)))
(NOT (LESSP (ADD1 Z)
(DIFFERENCE Z (SUB1 N))))).
This further simplifies, rewriting with SUB1-ADD1, and unfolding the
definition of LESSP, to:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP Z (DIFFERENCE Z (SUB1 N))))
(LESSP Z (SUB1 N))
(NOT (EQUAL (DIFFERENCE Z (SUB1 N)) 0)))
(NOT (LESSP Z
(SUB1 (DIFFERENCE Z (SUB1 N)))))).
Applying the lemma SUB1-ELIM, replace N by (ADD1 V) to eliminate (SUB1 N).
We rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove the new conjecture:
(IMPLIES (AND (NUMBERP V)
(NUMBERP Z)
(NOT (EQUAL (ADD1 V) 0))
(NOT (LESSP Z (DIFFERENCE Z V)))
(LESSP Z V)
(NOT (EQUAL (DIFFERENCE Z V) 0)))
(NOT (LESSP Z (SUB1 (DIFFERENCE Z V))))),
which further simplifies, clearly, to the new formula:
(IMPLIES (AND (NUMBERP V)
(NUMBERP Z)
(NOT (LESSP Z (DIFFERENCE Z V)))
(LESSP Z V)
(NOT (EQUAL (DIFFERENCE Z V) 0)))
(NOT (LESSP Z (SUB1 (DIFFERENCE Z V))))),
which we generalize by replacing (DIFFERENCE Z V) by Y. We restrict the new
variable by recalling the type restriction lemma noted when DIFFERENCE was
introduced. We thus obtain the new formula:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP V)
(NUMBERP Z)
(NOT (LESSP Z Y))
(LESSP Z V)
(NOT (EQUAL Y 0)))
(NOT (LESSP Z (SUB1 Y)))),
which finally simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-DIFFERENCE-1
(PROVE-LEMMA NODE-P-S-HEIGHT
(REWRITE)
(NODE-P (S-HEIGHT N)))
This simplifies, using linear arithmetic, appealing to the lemmas KOENIG-INTRO
and NODE-P-NTHCDR, and opening up S-HEIGHT, to:
(IMPLIES (LESSP (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N)
(NODE-P (S-HEIGHT N))).
But this again simplifies, applying LESSP-DIFFERENCE-1, KOENIG-INTRO, and
NODE-P-NTHCDR, and expanding the function S-HEIGHT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NODE-P-S-HEIGHT
(PROVE-LEMMA LENGTH-NTHCDR
(REWRITE)
(EQUAL (LENGTH (NTHCDR N S))
(DIFFERENCE (LENGTH S) N)))
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest three inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N S))
(IMPLIES (AND (NOT (ZEROP N))
(p (SUB1 N) (CDR S)))
(p N S))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. Note, however, the inductive
instance chosen for S. The above induction scheme produces the following two
new formulas:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (LENGTH (NTHCDR N S))
(DIFFERENCE (LENGTH S) N))).
This simplifies, expanding the definitions of ZEROP, EQUAL, NTHCDR, LENGTH,
and DIFFERENCE, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N))))
(EQUAL (LENGTH (NTHCDR N S))
(DIFFERENCE (LENGTH S) N))).
This simplifies, expanding the definitions of ZEROP, NTHCDR, and LENGTH, to
the following two new goals:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(NOT (LISTP S)))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
(DIFFERENCE 0 N))).
But this again simplifies, opening up the functions EQUAL and DIFFERENCE,
to the goal:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(NOT (LISTP S)))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
0)).
However this further simplifies, rewriting with CDR-NLISTP, and opening up
LENGTH, EQUAL, and DIFFERENCE, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(LISTP S))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
(DIFFERENCE (ADD1 (LENGTH (CDR S)))
N))).
However this again simplifies, using linear arithmetic, to two new
formulas:
Case 1.1.2.
(IMPLIES (AND (LESSP (LENGTH (CDR S)) (SUB1 N))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(LISTP S))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
(DIFFERENCE (ADD1 (LENGTH (CDR S)))
N))),
which again simplifies, applying SUB1-ADD1, and opening up DIFFERENCE,
to:
T.
Case 1.1.1.
(IMPLIES (AND (LESSP (ADD1 (LENGTH (CDR S))) N)
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(LISTP S))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
(DIFFERENCE (ADD1 (LENGTH (CDR S)))
N))).
This again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP (LENGTH (CDR S)) (SUB1 N))
(LESSP (ADD1 (LENGTH (CDR S))) N)
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (NTHCDR (SUB1 N) (CDR S)))
(DIFFERENCE (LENGTH (CDR S))
(SUB1 N)))
(LISTP S))
(EQUAL (DIFFERENCE (LENGTH (CDR S)) (SUB1 N))
(DIFFERENCE (ADD1 (LENGTH (CDR S)))
N))).
However this again simplifies, appealing to the lemma SUB1-ADD1, and
opening up LESSP and DIFFERENCE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-NTHCDR
(PROVE-LEMMA FIRST-NON-MEMBER-INDEX-LESSP
(REWRITE)
(NOT (LESSP (FIRST-NON-MEMBER-INDEX I X)
I)))
WARNING: Note that the proposed lemma FIRST-NON-MEMBER-INDEX-LESSP is to be
stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.
Name the conjecture *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (AND (MEMBER (S-N I) X)
(p (ADD1 I) (REMOVE1 (S-N I) X)))
(p I X))
(IMPLIES (NOT (MEMBER (S-N I) X))
(p I X))).
Linear arithmetic and the lemma LENGTH-REMOVE1 inform us that the measure
(LENGTH X) decreases according to the well-founded relation LESSP in each
induction step of the scheme. Note, however, the inductive instance chosen
for I. The above induction scheme leads to two new conjectures:
Case 2. (IMPLIES (AND (MEMBER (S-N I) X)
(NOT (LESSP (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X))
(ADD1 I))))
(NOT (LESSP (FIRST-NON-MEMBER-INDEX I X)
I))),
which simplifies, applying SUB1-ADD1, and unfolding the functions LESSP and
FIRST-NON-MEMBER-INDEX, to:
(IMPLIES
(AND (MEMBER (S-N I) X)
(NOT (EQUAL (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X))
0))
(NUMBERP I)
(NOT (LESSP (SUB1 (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X)))
I)))
(NOT (LESSP (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X))
I))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (NOT (MEMBER (S-N I) X))
(NOT (LESSP (FIRST-NON-MEMBER-INDEX I X)
I))),
which simplifies, unfolding FIRST-NON-MEMBER-INDEX, to:
(IMPLIES (NOT (MEMBER (S-N I) X))
(NOT (LESSP I I))).
However this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FIRST-NON-MEMBER-INDEX-LESSP
(PROVE-LEMMA S-N-FIRST-NON-MEMBER-INDEX-NOT-EQUAL
(REWRITE)
(IMPLIES (NUMBERP I)
(NOT (EQUAL (S-N (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X)))
(S-N I)))))
This simplifies, using linear arithmetic and appealing to the lemmas
FIRST-NON-MEMBER-INDEX-LESSP and KOENIG-INTRO, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
S-N-FIRST-NON-MEMBER-INDEX-NOT-EQUAL
(PROVE-LEMMA MEMBER-REMOVE1
(REWRITE)
(IMPLIES (NOT (EQUAL A B))
(EQUAL (MEMBER A (REMOVE1 B X))
(MEMBER A X))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X) (EQUAL B (CAR X)))
(p A B X))
(IMPLIES (AND (LISTP X)
(NOT (EQUAL B (CAR X)))
(p A B (CDR X)))
(p A B X))
(IMPLIES (NOT (LISTP X)) (p A B X))).
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 the
following three new conjectures:
Case 3. (IMPLIES (AND (LISTP X)
(EQUAL B (CAR X))
(NOT (EQUAL A B)))
(EQUAL (MEMBER A (REMOVE1 B X))
(MEMBER A X))).
This simplifies, opening up the functions REMOVE1 and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (EQUAL B (CAR X)))
(EQUAL (MEMBER A (REMOVE1 B (CDR X)))
(MEMBER A (CDR X)))
(NOT (EQUAL A B)))
(EQUAL (MEMBER A (REMOVE1 B X))
(MEMBER A X))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
definitions of REMOVE1 and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X))
(NOT (EQUAL A B)))
(EQUAL (MEMBER A (REMOVE1 B X))
(MEMBER A X))),
which simplifies, unfolding the functions REMOVE1, MEMBER, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-REMOVE1
(PROVE-LEMMA S-N-FIRST-NON-MEMBER-INDEX
(REWRITE)
(IMPLIES (NUMBERP I)
(NOT (MEMBER (S-N (FIRST-NON-MEMBER-INDEX I X))
X))))
Call the conjecture *1.
Perhaps we can prove it by induction. Two inductions are suggested by
terms in the conjecture, both of which are unflawed. So we will choose the
one suggested by the largest number of nonprimitive recursive functions. We
will induct according to the following scheme:
(AND (IMPLIES (AND (MEMBER (S-N I) X)
(p (ADD1 I) (REMOVE1 (S-N I) X)))
(p I X))
(IMPLIES (NOT (MEMBER (S-N I) X))
(p I X))).
Linear arithmetic and the lemma LENGTH-REMOVE1 can be used to prove that the
measure (LENGTH X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive instance
chosen for I. The above induction scheme leads to two new goals:
Case 2. (IMPLIES
(AND (MEMBER (S-N I) X)
(NOT (MEMBER (S-N (FIRST-NON-MEMBER-INDEX (ADD1 I)
(REMOVE1 (S-N I) X)))
(REMOVE1 (S-N I) X)))
(NUMBERP I))
(NOT (MEMBER (S-N (FIRST-NON-MEMBER-INDEX I X))
X))),
which simplifies, applying the lemmas S-N-FIRST-NON-MEMBER-INDEX-NOT-EQUAL
and MEMBER-REMOVE1, and opening up the definition of FIRST-NON-MEMBER-INDEX,
to:
T.
Case 1. (IMPLIES (AND (NOT (MEMBER (S-N I) X))
(NUMBERP I))
(NOT (MEMBER (S-N (FIRST-NON-MEMBER-INDEX I X))
X))),
which simplifies, unfolding the function FIRST-NON-MEMBER-INDEX, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
S-N-FIRST-NON-MEMBER-INDEX
(PROVE-LEMMA MEMBER-APPEND
(REWRITE)
(EQUAL (MEMBER A (APPEND X Y))
(OR (MEMBER A X) (MEMBER A Y))))
This simplifies, opening up the function OR, to two new conjectures:
Case 2. (IMPLIES (NOT (MEMBER A X))
(EQUAL (MEMBER A (APPEND X Y))
(MEMBER A Y))),
which we will name *1.
Case 1. (IMPLIES (MEMBER A X)
(EQUAL (MEMBER A (APPEND X Y)) T)).
This again simplifies, trivially, to the new formula:
(IMPLIES (MEMBER A X)
(MEMBER A (APPEND X Y))),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(EQUAL (MEMBER A (APPEND X Y))
(OR (MEMBER A X) (MEMBER A Y))).
We named this *1. We will try to prove it by induction. There are three
plausible inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP X) (p A (CDR X) Y))
(p A X Y))
(IMPLIES (NOT (LISTP X)) (p A X Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates two new conjectures:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (MEMBER A (APPEND (CDR X) Y))
(OR (MEMBER A (CDR X)) (MEMBER A Y))))
(EQUAL (MEMBER A (APPEND X Y))
(OR (MEMBER A X) (MEMBER A Y)))),
which simplifies, applying CDR-CONS and CAR-CONS, and unfolding OR, APPEND,
MEMBER, and EQUAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (MEMBER A (APPEND X Y))
(OR (MEMBER A X) (MEMBER A Y)))).
This simplifies, expanding the functions APPEND, MEMBER, and OR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-APPEND
(PROVE-LEMMA MEMBER-CONS-SUCC-AUX
(REWRITE)
(EQUAL (MEMBER (CONS Z V) (SUCC-AUX V N))
(AND (LESSP 0 Z) (NOT (LESSP N Z))))
((INDUCT (SUCC-AUX V N))))
This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new conjectures:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (MEMBER (CONS Z V) (SUCC-AUX V N))
(AND (LESSP 0 Z) (NOT (LESSP N Z))))).
This simplifies, opening up the definitions of ZEROP, EQUAL, SUCC-AUX, LISTP,
MEMBER, LESSP, NOT, and AND, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
(AND (LESSP 0 Z)
(NOT (LESSP (SUB1 N) Z)))))
(EQUAL (MEMBER (CONS Z V) (SUCC-AUX V N))
(AND (LESSP 0 Z) (NOT (LESSP N Z))))).
This simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, and
CONS-EQUAL, and opening up the definitions of EQUAL, LESSP, NOT, AND,
SUCC-AUX, and MEMBER, to the following six new conjectures:
Case 1.6.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL Z 0)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
F))
(NOT (MEMBER (CONS 0 V)
(SUCC-AUX V (SUB1 N))))).
This again simplifies, obviously, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) Z)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
F)
(NOT (EQUAL Z N))
(NOT (EQUAL Z 0))
(NUMBERP Z))
(LESSP N Z)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) Z)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
F)
(EQUAL Z N))
(NOT (LESSP N Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) Z)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
F)
(EQUAL Z N))
(NUMBERP Z)),
which again simplifies, trivially, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) Z)
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
F)
(EQUAL Z N))
(NOT (EQUAL Z 0))).
This again simplifies, clearly, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(NOT (LESSP (SUB1 N) Z))
(EQUAL (MEMBER (CONS Z V)
(SUCC-AUX V (SUB1 N)))
T))
(NOT (LESSP N Z))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-CONS-SUCC-AUX
(PROVE-LEMMA NODE-P-CONS-LEMMA NIL
(IMPLIES (NOT (NODE-P S))
(NOT (NODE-P (CONS N S)))))
This formula simplifies, applying CDR-CONS and KOENIG-INTRO, and opening up
the function SUBSEQ, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NODE-P-CONS-LEMMA
(PROVE-LEMMA NODE-P-CONS
(REWRITE)
(EQUAL (NODE-P (CONS N S))
(AND (NODE-P S)
(LESSP 0 N)
(NOT (LESSP (SUCCARD S) N))))
((USE (NODE-P-CONS-LEMMA))))
WARNING: the newly proposed lemma, NODE-P-CONS, could be applied whenever the
previously added lemma KOENIG-INTRO could.
This formula simplifies, rewriting with KOENIG-INTRO, and opening up the
definitions of NOT, IMPLIES, EQUAL, LESSP, SUBSEQ, and AND, to:
(IMPLIES (AND (NOT (NODE-P (CONS N S)))
(NODE-P S)
(NOT (EQUAL N 0))
(NUMBERP N))
(LESSP (SUCCARD S) N)),
which again simplifies, rewriting with the lemma KOENIG-INTRO, and expanding
the definitions of EQUAL and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NODE-P-CONS
(DEFN ALL-LENGTH-N
(SS N)
(IF (LISTP SS)
(AND (EQUAL (LENGTH (CAR SS)) N)
(ALL-LENGTH-N (CDR SS) N))
T))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT SS) decreases according to the well-founded relation LESSP in each
recursive call. Hence, ALL-LENGTH-N is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (ALL-LENGTH-N SS N))
(TRUEP (ALL-LENGTH-N SS N)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-LENGTH-N
(PROVE-LEMMA ALL-LENGTH-N-APPEND
(REWRITE)
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
(AND (ALL-LENGTH-N SS1 N)
(ALL-LENGTH-N SS2 N))))
This simplifies, opening up the function AND, to two new conjectures:
Case 2. (IMPLIES (NOT (ALL-LENGTH-N SS1 N))
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
F)),
which again simplifies, clearly, to:
(IMPLIES (NOT (ALL-LENGTH-N SS1 N))
(NOT (ALL-LENGTH-N (APPEND SS1 SS2) N))),
which we will name *1.
Case 1. (IMPLIES (ALL-LENGTH-N SS1 N)
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
(ALL-LENGTH-N SS2 N))),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
(AND (ALL-LENGTH-N SS1 N)
(ALL-LENGTH-N SS2 N))),
which we named *1 above. We will appeal to induction. There are three
plausible inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP SS1) (p (CDR SS1) SS2 N))
(p SS1 SS2 N))
(IMPLIES (NOT (LISTP SS1))
(p SS1 SS2 N))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT SS1) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme produces two new
conjectures:
Case 2. (IMPLIES (AND (LISTP SS1)
(EQUAL (ALL-LENGTH-N (APPEND (CDR SS1) SS2)
N)
(AND (ALL-LENGTH-N (CDR SS1) N)
(ALL-LENGTH-N SS2 N))))
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
(AND (ALL-LENGTH-N SS1 N)
(ALL-LENGTH-N SS2 N)))),
which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and expanding
AND, APPEND, ALL-LENGTH-N, and EQUAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP SS1))
(EQUAL (ALL-LENGTH-N (APPEND SS1 SS2) N)
(AND (ALL-LENGTH-N SS1 N)
(ALL-LENGTH-N SS2 N)))),
which simplifies, opening up the definitions of APPEND, ALL-LENGTH-N, and
AND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-LENGTH-N-APPEND
(PROVE-LEMMA ALL-LENGTH-N-SUCC-AUX
(REWRITE)
(IMPLIES (EQUAL (LENGTH S) N)
(ALL-LENGTH-N (SUCC-AUX S K)
(ADD1 N))))
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (ZEROP K) (p S K))
(IMPLIES (AND (NOT (ZEROP K)) (p S (SUB1 K)))
(p S K))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT K) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following two new goals:
Case 2. (IMPLIES (ZEROP K)
(ALL-LENGTH-N (SUCC-AUX S K)
(ADD1 (LENGTH S)))).
This simplifies, expanding the definitions of ZEROP, EQUAL, SUCC-AUX, LISTP,
and ALL-LENGTH-N, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP K))
(ALL-LENGTH-N (SUCC-AUX S (SUB1 K))
(ADD1 (LENGTH S))))
(ALL-LENGTH-N (SUCC-AUX S K)
(ADD1 (LENGTH S)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding the
functions ZEROP, SUCC-AUX, LENGTH, and ALL-LENGTH-N, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-LENGTH-N-SUCC-AUX
(PROVE-LEMMA ALL-LENGTH-N-SUCCESSORS-LIST
(REWRITE)
(IMPLIES (ALL-LENGTH-N SS N)
(ALL-LENGTH-N (SUCCESSORS-LIST SS)
(ADD1 N))))
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest two inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP SS) (p (CDR SS) N))
(p SS N))
(IMPLIES (NOT (LISTP SS)) (p SS N))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT SS) 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 SS)
(NOT (ALL-LENGTH-N (CDR SS) N))
(ALL-LENGTH-N SS N))
(ALL-LENGTH-N (SUCCESSORS-LIST SS)
(ADD1 N))).
This simplifies, expanding the definition of ALL-LENGTH-N, to:
T.
Case 2. (IMPLIES (AND (LISTP SS)
(ALL-LENGTH-N (SUCCESSORS-LIST (CDR SS))
(ADD1 N))
(ALL-LENGTH-N SS N))
(ALL-LENGTH-N (SUCCESSORS-LIST SS)
(ADD1 N))).
This simplifies, applying ALL-LENGTH-N-SUCC-AUX and ALL-LENGTH-N-APPEND, and
expanding the definitions of ALL-LENGTH-N, SUCCESSORS-LIST, and SUCCESSORS,
to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP SS))
(ALL-LENGTH-N SS N))
(ALL-LENGTH-N (SUCCESSORS-LIST SS)
(ADD1 N))),
which simplifies, opening up ALL-LENGTH-N, SUCCESSORS-LIST, and LISTP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-LENGTH-N-SUCCESSORS-LIST
(PROVE-LEMMA LENGTH-0
(REWRITE)
(EQUAL (EQUAL (LENGTH S) 0)
(NLISTP S)))
This formula simplifies, opening up the definition of NLISTP, to two new
conjectures:
Case 2. (IMPLIES (NOT (EQUAL (LENGTH S) 0))
(LISTP S)),
which again simplifies, unfolding the definitions of LENGTH and EQUAL, to:
T.
Case 1. (IMPLIES (EQUAL (LENGTH S) 0)
(NOT (LISTP S))),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP S) (p (CDR S)))
(p S))
(IMPLIES (NOT (LISTP S)) (p S))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT S) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme produces two
new formulas:
Case 2. (IMPLIES (AND (NOT (EQUAL (LENGTH (CDR S)) 0))
(EQUAL (LENGTH S) 0))
(NOT (LISTP S))),
which simplifies, opening up LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP (CDR S)))
(EQUAL (LENGTH S) 0))
(NOT (LISTP S))),
which simplifies, opening up LENGTH, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-0
(DEFN MEMBER-LEVEL-INDUCTION
(S N)
(IF (ZEROP N)
T
(MEMBER-LEVEL-INDUCTION (CDR S)
(SUB1 N))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MEMBER-LEVEL-INDUCTION is
accepted under the principle of definition. Observe that:
(TRUEP (MEMBER-LEVEL-INDUCTION S N))
is a theorem.
[ 0.0 0.0 0.0 ]
MEMBER-LEVEL-INDUCTION
(PROVE-LEMMA SUCC-AUX-LISTP
(REWRITE)
(IMPLIES (NOT (LISTP S))
(NOT (MEMBER S (SUCC-AUX Z N)))))
Call the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p S Z N))
(IMPLIES (AND (NOT (ZEROP N)) (p S Z (SUB1 N)))
(p S Z N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to two new goals:
Case 2. (IMPLIES (AND (ZEROP N) (NOT (LISTP S)))
(NOT (MEMBER S (SUCC-AUX Z N)))),
which simplifies, opening up the definitions of ZEROP, EQUAL, SUCC-AUX,
LISTP, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (MEMBER S (SUCC-AUX Z (SUB1 N))))
(NOT (LISTP S)))
(NOT (MEMBER S (SUCC-AUX Z N)))),
which simplifies, applying CDR-CONS and CAR-CONS, and unfolding ZEROP,
SUCC-AUX, and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUCC-AUX-LISTP
(PROVE-LEMMA SUCCESSORS-LIST-LISTP
(REWRITE)
(IMPLIES (NOT (LISTP S))
(NOT (MEMBER S (SUCCESSORS-LIST SS)))))
Give the conjecture the name *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 SS) (p S (CDR SS)))
(p S SS))
(IMPLIES (NOT (LISTP SS)) (p S SS))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT SS) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates two new
goals:
Case 2. (IMPLIES (AND (LISTP SS)
(NOT (MEMBER S (SUCCESSORS-LIST (CDR SS))))
(NOT (LISTP S)))
(NOT (MEMBER S (SUCCESSORS-LIST SS)))),
which simplifies, applying SUCC-AUX-LISTP and MEMBER-APPEND, and unfolding
the functions SUCCESSORS-LIST and SUCCESSORS, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP SS)) (NOT (LISTP S)))
(NOT (MEMBER S (SUCCESSORS-LIST SS)))).
This simplifies, opening up SUCCESSORS-LIST, LISTP, and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUCCESSORS-LIST-LISTP
(PROVE-LEMMA MEMBER-SUCC-AUX NIL
(IMPLIES (MEMBER S (SUCC-AUX X N))
(EQUAL (CDR S) X)))
.
Appealing to the lemma CAR-CDR-ELIM, we now replace S by (CONS V Z) to
eliminate (CDR S) and (CAR S). This generates two new conjectures:
Case 2. (IMPLIES (AND (NOT (LISTP S))
(MEMBER S (SUCC-AUX X N)))
(EQUAL (CDR S) X)),
which simplifies, appealing to the lemma SUCC-AUX-LISTP, to:
T.
Case 1. (IMPLIES (MEMBER (CONS V Z) (SUCC-AUX X N))
(EQUAL Z X)),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(IMPLIES (MEMBER S (SUCC-AUX X N))
(EQUAL (CDR S) X)).
We named this *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 (ZEROP N) (p S X N))
(IMPLIES (AND (NOT (ZEROP N)) (p S X (SUB1 N)))
(p S X N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP N)
(MEMBER S (SUCC-AUX X N)))
(EQUAL (CDR S) X)).
This simplifies, unfolding ZEROP, EQUAL, SUCC-AUX, LISTP, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (MEMBER S (SUCC-AUX X (SUB1 N))))
(MEMBER S (SUCC-AUX X N)))
(EQUAL (CDR S) X)).
This simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and opening
up the functions ZEROP, SUCC-AUX, and MEMBER, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (MEMBER S (SUCC-AUX X (SUB1 N))))
(EQUAL S (CONS N X)))
(EQUAL (CDR S) X)),
which again simplifies, applying the lemmas MEMBER-CONS-SUCC-AUX and
CDR-CONS, and unfolding EQUAL and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-SUCC-AUX
(PROVE-LEMMA MEMBER-SUCCESSORS-LIST-SUCCESSORS-LIST-WITNESS
(REWRITE)
(EQUAL (MEMBER S (SUCCESSORS-LIST SS))
(AND (MEMBER (CDR S) SS)
(MEMBER S (SUCCESSORS (CDR S)))))
((USE (MEMBER-SUCC-AUX (X (CAR SS))
(N (SUCCARD (CAR SS)))))
(INDUCT (SUCCESSORS-LIST SS))))
This simplifies, opening up the functions IMPLIES, NOT, SUCCESSORS, AND,
SUCCESSORS-LIST, MEMBER, and OR, to the following seven new goals:
Case 7. (IMPLIES (AND (NOT (MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))
(LISTP SS)
(NOT (MEMBER (CDR S) (CDR SS)))
(EQUAL (MEMBER S (SUCCESSORS-LIST (CDR SS)))
F)
(NOT (EQUAL (CDR S) (CAR SS))))
(EQUAL (MEMBER S
(APPEND (SUCC-AUX (CAR SS) (SUCCARD (CAR SS)))
(SUCCESSORS-LIST (CDR SS))))
F)).
However this again simplifies, rewriting with the lemma MEMBER-APPEND, and
opening up the definition of EQUAL, to:
T.
Case 6. (IMPLIES (AND (NOT (MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))
(LISTP SS)
(NOT (MEMBER (CDR S) (CDR SS)))
(EQUAL (MEMBER S (SUCCESSORS-LIST (CDR SS)))
F)
(EQUAL (CDR S) (CAR SS)))
(EQUAL (MEMBER S
(APPEND (SUCC-AUX (CAR SS) (SUCCARD (CAR SS)))
(SUCCESSORS-LIST (CDR SS))))
(MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))),
which again simplifies, applying MEMBER-APPEND, and opening up the function
EQUAL, to:
T.
Case 5. (IMPLIES (AND (NOT (MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))
(LISTP SS)
(MEMBER (CDR S) (CDR SS))
(EQUAL (MEMBER S (SUCCESSORS-LIST (CDR SS)))
(MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S))))))
(EQUAL (MEMBER S
(APPEND (SUCC-AUX (CAR SS) (SUCCARD (CAR SS)))
(SUCCESSORS-LIST (CDR SS))))
(MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))).
However this again simplifies, applying the lemma MEMBER-APPEND, to:
T.
Case 4. (IMPLIES (AND (NOT (MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))
(NOT (LISTP SS)))
(EQUAL (MEMBER S NIL) F)),
which again simplifies, applying CAR-NLISTP, and opening up LISTP, MEMBER,
and EQUAL, to:
T.
Case 3. (IMPLIES (AND (EQUAL (CDR S) (CAR SS))
(LISTP SS)
(NOT (MEMBER (CAR SS) (CDR SS)))
(EQUAL (MEMBER S (SUCCESSORS-LIST (CDR SS)))
F))
(EQUAL (MEMBER S
(APPEND (SUCC-AUX (CAR SS) (SUCCARD (CAR SS)))
(SUCCESSORS-LIST (CDR SS))))
(MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))).
However this again simplifies, appealing to the lemma MEMBER-APPEND, to:
T.
Case 2. (IMPLIES (AND (EQUAL (CDR S) (CAR SS))
(LISTP SS)
(MEMBER (CAR SS) (CDR SS))
(EQUAL (MEMBER S (SUCCESSORS-LIST (CDR SS)))
(MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS))))))
(EQUAL (MEMBER S
(APPEND (SUCC-AUX (CAR SS) (SUCCARD (CAR SS)))
(SUCCESSORS-LIST (CDR SS))))
(MEMBER S
(SUCC-AUX (CAR SS)
(SUCCARD (CAR SS)))))),
which again simplifies, applying MEMBER-APPEND, to:
T.
Case 1. (IMPLIES (AND (EQUAL (CDR S) (CAR SS))
(NOT (LISTP SS)))
(EQUAL (MEMBER S NIL) F)).
This again simplifies, applying CAR-NLISTP, and expanding the definitions of
LISTP, MEMBER, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
MEMBER-SUCCESSORS-LIST-SUCCESSORS-LIST-WITNESS
(PROVE-LEMMA MEMBER-LEVEL
(REWRITE)
(IMPLIES (AND (NUMBERP N) (NODE-P S))
(EQUAL (MEMBER S (LEVEL N))
(EQUAL (LENGTH S) N)))
((INDUCT (MEMBER-LEVEL-INDUCTION S N))))
This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to the following two new goals:
Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N) (NODE-P S))
(EQUAL (MEMBER S (LEVEL N))
(EQUAL (LENGTH S) N))).
This simplifies, appealing to the lemma LENGTH-0, and unfolding ZEROP,
NUMBERP, LEVEL, CDR, CAR, LISTP, and MEMBER, to the following two new
conjectures:
Case 2.2.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(NOT (EQUAL S NIL)))
(LISTP S)).
But this again simplifies, applying KOENIG-INTRO, and opening up the
definition of PLISTP, to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(EQUAL S NIL))
(NOT (LISTP S))).
This again simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (NUMBERP (SUB1 N))
(NODE-P (CDR S)))
(EQUAL (MEMBER (CDR S) (LEVEL (SUB1 N)))
(EQUAL (LENGTH (CDR S)) (SUB1 N))))
(NODE-P S))
(EQUAL (MEMBER S (LEVEL N))
(EQUAL (LENGTH S) N))).
This simplifies, rewriting with
MEMBER-SUCCESSORS-LIST-SUCCESSORS-LIST-WITNESS and ADD1-SUB1, and opening up
AND, IMPLIES, LEVEL, SUCCESSORS, and LENGTH, to seven new goals:
Case 1.7.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P (CDR S)))
(NODE-P S)
(LISTP S)
(EQUAL (ADD1 (LENGTH (CDR S))) N))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
T)),
which again simplifies, applying KOENIG-INTRO, and unfolding the function
SUBSEQ, to:
T.
Case 1.6.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P (CDR S)))
(NODE-P S)
(NOT (EQUAL (ADD1 (LENGTH (CDR S))) N))
(MEMBER (CDR S) (LEVEL (SUB1 N))))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace S by (CONS Z X) to
eliminate (CDR S) and (CAR S). The result is two new goals:
Case 1.6.2.
(IMPLIES (AND (NOT (LISTP S))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P (CDR S)))
(NODE-P S)
(NOT (EQUAL (ADD1 (LENGTH (CDR S))) N))
(MEMBER (CDR S) (LEVEL (SUB1 N))))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))),
which further simplifies, rewriting with CDR-NLISTP, KOENIG-INTRO, and
SUCC-AUX-LISTP, and unfolding PLISTP, LENGTH, and ADD1, to:
T.
Case 1.6.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P X))
(NODE-P (CONS Z X))
(NOT (EQUAL (ADD1 (LENGTH X)) N))
(MEMBER X (LEVEL (SUB1 N))))
(NOT (MEMBER (CONS Z X)
(SUCC-AUX X (SUCCARD X))))).
This further simplifies, applying the lemmas CDR-CONS and KOENIG-INTRO,
and unfolding the function SUBSEQ, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P (CDR S)))
(NODE-P S)
(NOT (LISTP S))
(MEMBER (CDR S) (LEVEL (SUB1 N))))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))),
which again simplifies, applying CDR-NLISTP, KOENIG-INTRO, and
SUCC-AUX-LISTP, and unfolding the function PLISTP, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (NODE-P (CDR S)))
(NODE-P S)
(LISTP S)
(EQUAL (ADD1 (LENGTH (CDR S))) N))
(MEMBER (CDR S) (LEVEL (SUB1 N)))).
But this again simplifies, rewriting with KOENIG-INTRO, and expanding the
function SUBSEQ, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (LENGTH (CDR S)) (SUB1 N)))
(NOT (MEMBER (CDR S) (LEVEL (SUB1 N))))
(NODE-P S)
(LISTP S))
(NOT (EQUAL (ADD1 (LENGTH (CDR S))) N))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (CDR S)) (SUB1 N))
(EQUAL (MEMBER (CDR S) (LEVEL (SUB1 N)))
T)
(NODE-P S)
(LISTP S))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
T)),
which again simplifies, obviously, to the new goal:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (CDR S)) (SUB1 N))
(MEMBER (CDR S) (LEVEL (SUB1 N)))
(NODE-P S)
(LISTP S))
(MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S))))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS Z X) to eliminate
(CDR S) and (CAR S). We thus obtain:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH X) (SUB1 N))
(MEMBER X (LEVEL (SUB1 N)))
(NODE-P (CONS Z X)))
(MEMBER (CONS Z X)
(SUCC-AUX X (SUCCARD X)))),
which further simplifies, applying the lemmas NODE-P-CONS and
MEMBER-CONS-SUCC-AUX, and unfolding EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (LENGTH (CDR S)) (SUB1 N))
(EQUAL (MEMBER (CDR S) (LEVEL (SUB1 N)))
T)
(NODE-P S)
(NOT (LISTP S)))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))),
which again simplifies, rewriting with CDR-NLISTP, and opening up the
functions LENGTH, LEVEL, MEMBER, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
MEMBER-LEVEL
(PROVE-LEMMA MEMBER-INIT-TREE
(REWRITE)
(IMPLIES (NODE-P S)
(EQUAL (MEMBER S (INIT-TREE N))
(NOT (LESSP N (LENGTH S))))))
This formula simplifies, expanding NOT, to two new conjectures:
Case 2. (IMPLIES (AND (NODE-P S)
(NOT (LESSP N (LENGTH S))))
(EQUAL (MEMBER S (INIT-TREE N)) T)),
which again simplifies, clearly, to:
(IMPLIES (AND (NODE-P S)
(NOT (LESSP N (LENGTH S))))
(MEMBER S (INIT-TREE N))),
which we will name *1.
Case 1. (IMPLIES (AND (NODE-P S) (LESSP N (LENGTH S)))
(EQUAL (MEMBER S (INIT-TREE N)) F)).
This again simplifies, trivially, to:
(IMPLIES (AND (NODE-P S) (LESSP N (LENGTH S)))
(NOT (MEMBER S (INIT-TREE N)))),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(IMPLIES (NODE-P S)
(EQUAL (MEMBER S (INIT-TREE N))
(NOT (LESSP N (LENGTH S))))).
We named this *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 (ZEROP N) (p S N))
(IMPLIES (AND (NOT (ZEROP N)) (p S (SUB1 N)))
(p S N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme produces two new conjectures:
Case 2. (IMPLIES (AND (ZEROP N) (NODE-P S))
(EQUAL (MEMBER S (INIT-TREE N))
(NOT (LESSP N (LENGTH S))))),
which simplifies, rewriting with the lemma LENGTH-0, and opening up ZEROP,
INIT-TREE, CDR, CAR, LISTP, MEMBER, EQUAL, LESSP, and NOT, to four new goals:
Case 2.4.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(NOT (EQUAL S NIL)))
(LISTP S)),
which again simplifies, rewriting with KOENIG-INTRO, and opening up the
definition of PLISTP, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(EQUAL S NIL))
(NOT (LISTP S))).
This again simplifies, clearly, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NODE-P S)
(NOT (EQUAL S NIL)))
(LISTP S)).
This again simplifies, applying KOENIG-INTRO, and unfolding the definition
of PLISTP, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(NODE-P S)
(EQUAL S NIL))
(NOT (LISTP S))).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
(NOT (LESSP (SUB1 N) (LENGTH S))))
(NODE-P S))
(EQUAL (MEMBER S (INIT-TREE N))
(NOT (LESSP N (LENGTH S))))).
This simplifies, applying MEMBER-SUCCESSORS-LIST-SUCCESSORS-LIST-WITNESS,
MEMBER-APPEND, and LENGTH-0, and expanding the definitions of ZEROP, NOT,
INIT-TREE, LEVEL, SUCCESSORS, and LESSP, to six new goals:
Case 1.6.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP (SUB1 N) (LENGTH S)))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
T)
(NODE-P S)
(LISTP S))
(NOT (LESSP (SUB1 N) (SUB1 (LENGTH S))))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (EQUAL (LENGTH S) 0)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP (SUB1 N) (LENGTH S)))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
T)
(NODE-P S)
(LISTP S))
(NOT (LESSP (SUB1 N) (SUB1 (LENGTH S))))).
However this again simplifies, rewriting with LENGTH-0, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
F)
(NODE-P S)
(LISTP S)
(LESSP (SUB1 N) (SUB1 (LENGTH S)))
(MEMBER (CDR S) (LEVEL (SUB1 N))))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
F)).
This again simplifies, obviously, to the new formula:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(NOT (MEMBER S (INIT-TREE (SUB1 N))))
(NODE-P S)
(LISTP S)
(LESSP (SUB1 N) (SUB1 (LENGTH S)))
(MEMBER (CDR S) (LEVEL (SUB1 N))))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))).
Applying the lemma SUB1-ELIM, replace N by (ADD1 X) to eliminate (SUB1 N).
We use the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. This produces:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(LESSP X (LENGTH S))
(NOT (MEMBER S (INIT-TREE X)))
(NODE-P S)
(LISTP S)
(LESSP X (SUB1 (LENGTH S)))
(MEMBER (CDR S) (LEVEL X)))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))),
which further simplifies, clearly, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X (LENGTH S))
(NOT (MEMBER S (INIT-TREE X)))
(NODE-P S)
(LISTP S)
(LESSP X (SUB1 (LENGTH S)))
(MEMBER (CDR S) (LEVEL X)))
(NOT (MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S)))))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS V Z) to eliminate
(CDR S) and (CAR S). We thus obtain the new formula:
(IMPLIES (AND (NUMBERP X)
(LESSP X (LENGTH (CONS V Z)))
(NOT (MEMBER (CONS V Z) (INIT-TREE X)))
(NODE-P (CONS V Z))
(LESSP X (SUB1 (LENGTH (CONS V Z))))
(MEMBER Z (LEVEL X)))
(NOT (MEMBER (CONS V Z)
(SUCC-AUX Z (SUCCARD Z))))),
which further simplifies, rewriting with the lemmas CDR-CONS, SUB1-ADD1,
NODE-P-CONS, LENGTH-0, MEMBER-LEVEL, and MEMBER-CONS-SUCC-AUX, and
expanding the definitions of LENGTH, LESSP, INIT-TREE, CDR, CAR, LISTP,
MEMBER, EQUAL, and LEVEL, to:
(IMPLIES (AND (NUMBERP X)
(LESSP (SUB1 X) (LENGTH Z))
(NOT (MEMBER (CONS V Z) (INIT-TREE X)))
(NODE-P Z)
(NOT (EQUAL V 0))
(NUMBERP V)
(NOT (LESSP (SUCCARD Z) V))
(LESSP X (LENGTH Z)))
(NOT (EQUAL (LENGTH Z) X))).
This finally simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
F)
(NODE-P S)
(NOT (LESSP (SUB1 N) (SUB1 (LENGTH S)))))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
T)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL (LENGTH S) 0))
(NUMBERP (LENGTH S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))
(EQUAL (MEMBER S
(INIT-TREE (SUB1 (LENGTH S))))
F)
(NODE-P S)
(NOT (LESSP (SUB1 (LENGTH S))
(SUB1 (LENGTH S)))))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
T)).
But this again simplifies, rewriting with LENGTH-0, to:
(IMPLIES (AND (LISTP S)
(LESSP (SUB1 (LENGTH S)) (LENGTH S))
(NOT (MEMBER S
(INIT-TREE (SUB1 (LENGTH S)))))
(NODE-P S)
(NOT (LESSP (SUB1 (LENGTH S))
(SUB1 (LENGTH S)))))
(MEMBER S
(SUCC-AUX (CDR S)
(SUCCARD (CDR S))))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS Z X) to eliminate
(CDR S) and (CAR S). We thus obtain:
(IMPLIES (AND (LESSP (SUB1 (LENGTH (CONS Z X)))
(LENGTH (CONS Z X)))
(NOT (MEMBER (CONS Z X)
(INIT-TREE (SUB1 (LENGTH (CONS Z X))))))
(NODE-P (CONS Z X))
(NOT (LESSP (SUB1 (LENGTH (CONS Z X)))
(SUB1 (LENGTH (CONS Z X))))))
(MEMBER (CONS Z X)
(SUCC-AUX X (SUCCARD X)))),
which further simplifies, rewriting with CDR-CONS, SUB1-ADD1, LENGTH-0,
NODE-P-CONS, and MEMBER-CONS-SUCC-AUX, and unfolding the definitions of
LENGTH, LESSP, ADD1, SUB1, INIT-TREE, CDR, CAR, LISTP, MEMBER, and EQUAL,
to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
F)
(NODE-P S)
(NOT (LISTP S)))
(EQUAL (MEMBER S
(SUCC-AUX (CDR S) (SUCCARD (CDR S))))
T)).
This again simplifies, rewriting with CDR-NLISTP and SUCC-AUX-LISTP, and
unfolding the function EQUAL, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(NOT (MEMBER S (INIT-TREE (SUB1 N))))
(NODE-P S))
(LISTP S)),
which further simplifies, unfolding LENGTH, EQUAL, and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
F)
(NODE-P S)
(NOT (LISTP S)))
(MEMBER (CDR S) (LEVEL (SUB1 N)))),
which again simplifies, applying CDR-NLISTP, to the new formula:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(NOT (MEMBER S (INIT-TREE (SUB1 N))))
(NODE-P S)
(NOT (LISTP S)))
(MEMBER 0 (LEVEL (SUB1 N)))),
which further simplifies, unfolding the definitions of LENGTH, EQUAL, and
LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) (LENGTH S))
(EQUAL (MEMBER S (INIT-TREE (SUB1 N)))
F)
(NODE-P S)
(NOT (LESSP (SUB1 N) (SUB1 (LENGTH S)))))
(MEMBER (CDR S) (LEVEL (SUB1 N)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL (LENGTH S) 0))
(NUMBERP (LENGTH S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))
(EQUAL (MEMBER S
(INIT-TREE (SUB1 (LENGTH S))))
F)
(NODE-P S)
(NOT (LESSP (SUB1 (LENGTH S))
(SUB1 (LENGTH S)))))
(MEMBER (CDR S)
(LEVEL (SUB1 (LENGTH S))))).
However this again simplifies, applying LENGTH-0, to the new conjecture:
(IMPLIES (AND (LISTP S)
(LESSP (SUB1 (LENGTH S)) (LENGTH S))
(NOT (MEMBER S
(INIT-TREE (SUB1 (LENGTH S)))))
(NODE-P S)
(NOT (LESSP (SUB1 (LENGTH S))
(SUB1 (LENGTH S)))))
(MEMBER (CDR S)
(LEVEL (SUB1 (LENGTH S))))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS Z X) to eliminate
(CDR S) and (CAR S). This produces:
(IMPLIES (AND (LESSP (SUB1 (LENGTH (CONS Z X)))
(LENGTH (CONS Z X)))
(NOT (MEMBER (CONS Z X)
(INIT-TREE (SUB1 (LENGTH (CONS Z X))))))
(NODE-P (CONS Z X))
(NOT (LESSP (SUB1 (LENGTH (CONS Z X)))
(SUB1 (LENGTH (CONS Z X))))))
(MEMBER X
(LEVEL (SUB1 (LENGTH (CONS Z X)))))),
which further simplifies, rewriting with the lemmas CDR-CONS, SUB1-ADD1,
LENGTH-0, NODE-P-CONS, and MEMBER-LEVEL, and unfolding LENGTH, LESSP, ADD1,
SUB1, INIT-TREE, CDR, CAR, LISTP, MEMBER, EQUAL, and LEVEL, to the
conjecture:
(IMPLIES (AND (NOT (LISTP X))
(NODE-P X)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(NOT (LESSP (SUCCARD X) Z)))
(EQUAL X NIL)).
This finally simplifies, rewriting with KOENIG-INTRO, and expanding PLISTP,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
MEMBER-INIT-TREE
(PROVE-LEMMA LENGTH-S-NON-MEMBER-INDEX
(REWRITE)
(IMPLIES (NUMBERP I)
(LESSP N
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX I
(INIT-TREE N))))))
((USE (S-N-FIRST-NON-MEMBER-INDEX (X (INIT-TREE N))))
(DISABLE S-N-FIRST-NON-MEMBER-INDEX)))
WARNING: Note that the proposed lemma LENGTH-S-NON-MEMBER-INDEX is to be
stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.
This formula simplifies, rewriting with KOENIG-INTRO and MEMBER-INIT-TREE, and
expanding the definitions of NOT and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-S-NON-MEMBER-INDEX
(PROVE-LEMMA LENGTH-S-HEIGHT
(REWRITE)
(EQUAL (LENGTH (S-HEIGHT N)) (FIX N)))
This formula simplifies, rewriting with LENGTH-NTHCDR, and expanding the
functions S-HEIGHT and FIX, to two new conjectures:
Case 2. (IMPLIES
(NOT (NUMBERP N))
(EQUAL
(DIFFERENCE
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
0)),
which again simplifies, rewriting with LENGTH-0, and expanding the functions
INIT-TREE, REMOVE1, ADD1, MEMBER, LISTP, CAR, CDR, FIRST-NON-MEMBER-INDEX,
and DIFFERENCE, to the following four new conjectures:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP N))
(EQUAL (S-N 0) NIL)
(NOT (LISTP (S-N 1))))
(EQUAL (DIFFERENCE (LENGTH (S-N 1)) 0)
0)).
However this again simplifies, unfolding LENGTH, DIFFERENCE, and EQUAL, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (NUMBERP N))
(EQUAL (S-N 0) NIL)
(LISTP (S-N 1)))
(EQUAL (DIFFERENCE (LENGTH (S-N 1))
(LENGTH (S-N 1)))
0)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (LENGTH (S-N 1))
(LENGTH (S-N 1)))
(NOT (NUMBERP N))
(EQUAL (S-N 0) NIL)
(LISTP (S-N 1)))
(EQUAL (DIFFERENCE (LENGTH (S-N 1))
(LENGTH (S-N 1)))
0)).
This again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (EQUAL (S-N 0) NIL))
(NOT (LISTP (S-N 0))))
(EQUAL (DIFFERENCE (LENGTH (S-N 0)) 0)
0)),
which again simplifies, opening up the definitions of LENGTH, DIFFERENCE,
and EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (EQUAL (S-N 0) NIL))
(LISTP (S-N 0)))
(EQUAL (DIFFERENCE (LENGTH (S-N 0))
(LENGTH (S-N 0)))
0)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (LENGTH (S-N 0))
(LENGTH (S-N 0)))
(NOT (NUMBERP N))
(NOT (EQUAL (S-N 0) NIL))
(LISTP (S-N 0)))
(EQUAL (DIFFERENCE (LENGTH (S-N 0))
(LENGTH (S-N 0)))
0)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(NUMBERP N)
(EQUAL
(DIFFERENCE
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
N)),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 1.2.
(IMPLIES
(AND
(LESSP
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
(NUMBERP N))
(EQUAL
(DIFFERENCE
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
N)),
which again simplifies, using linear arithmetic, to:
(IMPLIES
(AND
(LESSP (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N)
(LESSP
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
(NUMBERP N))
(EQUAL
(DIFFERENCE
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
N)).
This again simplifies, using linear arithmetic and applying
LENGTH-S-NON-MEMBER-INDEX, to:
T.
Case 1.1.
(IMPLIES
(AND (LESSP (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N)
(NUMBERP N))
(EQUAL
(DIFFERENCE
(LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
(DIFFERENCE (LENGTH (S-N (FIRST-NON-MEMBER-INDEX 0
(INIT-TREE N))))
N))
N)).
But this again simplifies, using linear arithmetic and rewriting with
LENGTH-S-NON-MEMBER-INDEX, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-S-HEIGHT
(DISABLE S-HEIGHT)
[ 0.0 0.0 0.0 ]
S-HEIGHT-OFF
(DCL INF (S))
[ 0.0 0.0 0.0 ]
INF
(DCL BIG-H (S))
[ 0.0 0.0 0.0 ]
BIG-H
(DCL BIG-S (BIG-H S))
[ 0.0 0.0 0.0 ]
BIG-S
(ADD-AXIOM INF-INTRO
(REWRITE)
(AND (IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(LESSP (BIG-H S) (LENGTH BIG-S)))
(INF S))
(IMPLIES (NOT (AND (SUBSEQ S (BIG-S BIG-H S))
(NODE-P (BIG-S BIG-H S))
(LESSP BIG-H
(LENGTH (BIG-S BIG-H S)))))
(NOT (INF S)))))
WARNING: Note that INF-INTRO contains the free variable BIG-S which will be
chosen by instantiating the hypothesis (SUBSEQ S BIG-S).
WARNING: Note that INF-INTRO contains the free variable BIG-H which will be
chosen by instantiating the hypothesis:
(NOT (AND (SUBSEQ S (BIG-S BIG-H S))
(NODE-P (BIG-S BIG-H S))
(LESSP BIG-H
(LENGTH (BIG-S BIG-H S))))).
WARNING: Note that the proposed lemma INF-INTRO is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and two
replacement rules.
[ 0.0 0.0 0.0 ]
INF-INTRO
(ADD-AXIOM INF-BOOLEAN
(REWRITE)
(OR (TRUEP (INF S)) (FALSEP (INF S))))
WARNING: Note that the proposed lemma INF-BOOLEAN is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and zero
replacement rules.
[ 0.0 0.0 0.0 ]
INF-BOOLEAN
(DISABLE INF-INTRO)
[ 0.0 0.0 0.0 ]
INF-INTRO-OFF
(PROVE-LEMMA INF-SUFF
(REWRITE)
(IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(LESSP (BIG-H S) (LENGTH BIG-S)))
(INF S))
((USE (INF-INTRO))))
WARNING: Note that INF-SUFF contains the free variable BIG-S which will be
chosen by instantiating the hypothesis (SUBSEQ S BIG-S).
This conjecture simplifies, applying the lemma KOENIG-INTRO, and expanding the
functions SUBSEQ, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INF-SUFF
(PROVE-LEMMA INF-NECC
(REWRITE)
(IMPLIES (NOT (AND (SUBSEQ S (BIG-S BIG-H S))
(NODE-P (BIG-S BIG-H S))
(LESSP BIG-H
(LENGTH (BIG-S BIG-H S)))))
(NOT (INF S)))
((USE (INF-INTRO))))
WARNING: Note that INF-NECC contains the free variable BIG-H which will be
chosen by instantiating the hypothesis:
(NOT (AND (SUBSEQ S (BIG-S BIG-H S))
(NODE-P (BIG-S BIG-H S))
(LESSP BIG-H
(LENGTH (BIG-S BIG-H S))))).
This conjecture simplifies, rewriting with KOENIG-INTRO, and unfolding the
definitions of AND, IMPLIES, NOT, and SUBSEQ, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INF-NECC
(DEFN NEXT
(S MAX)
(IF (ZEROP MAX)
(CONS 0 S)
(IF (INF (CONS MAX S))
(CONS MAX S)
(NEXT S (SUB1 MAX)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT MAX) decreases according to
the well-founded relation LESSP in each recursive call. Hence, NEXT is
accepted under the principle of definition. Note that (LISTP (NEXT S MAX)) is
a theorem.
[ 0.0 0.0 0.0 ]
NEXT
(PROVE-LEMMA INF-IMPLIES-NODE-P
(REWRITE)
(IMPLIES (INF S) (NODE-P S))
((USE (INF-NECC))))
This conjecture simplifies, rewriting with KOENIG-INTRO, and opening up AND,
NOT, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INF-IMPLIES-NODE-P
(PROVE-LEMMA NOT-INF-ZEROP
(REWRITE)
(IMPLIES (ZEROP I)
(NOT (INF (CONS I S))))
((USE (INF-IMPLIES-NODE-P (S (CONS I S))))
(DISABLE INF-IMPLIES-NODE-P)))
This formula simplifies, appealing to the lemma NODE-P-CONS, and unfolding the
definitions of EQUAL, LESSP, IMPLIES, and ZEROP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NOT-INF-ZEROP
(PROVE-LEMMA INF-CONS-IMPLIES-INF-NEXT
(REWRITE)
(IMPLIES (AND (NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S N)))
((INDUCT (NEXT S N))))
WARNING: Note that INF-CONS-IMPLIES-INF-NEXT contains the free variable I
which will be chosen by instantiating the hypothesis (INF (CONS I S)).
This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to three new goals:
Case 3. (IMPLIES (AND (ZEROP N)
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S N))),
which simplifies, appealing to the lemma NOT-INF-ZEROP, and unfolding ZEROP,
EQUAL, LESSP, and NEXT, to four new goals:
Case 3.4.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(INF (CONS I S)))
(NOT (EQUAL I 0))),
which again simplifies, rewriting with NOT-INF-ZEROP, and opening up the
definition of ZEROP, to:
T.
Case 3.3.
(IMPLIES (AND (EQUAL N 0)
(NODE-P S)
(INF (CONS I S)))
(NUMBERP I)).
This again simplifies, rewriting with NOT-INF-ZEROP, and opening up the
function ZEROP, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NODE-P S)
(INF (CONS I S)))
(NOT (EQUAL I 0))).
However this again simplifies, applying NOT-INF-ZEROP, and expanding the
definition of ZEROP, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (NUMBERP N))
(NODE-P S)
(INF (CONS I S)))
(NUMBERP I)).
This again simplifies, applying NOT-INF-ZEROP, and expanding the function
ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(INF (CONS N S))
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S N))).
This simplifies, unfolding the function NEXT, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (INF (CONS N S)))
(IMPLIES (AND (NODE-P S)
(INF (CONS I S))
(NOT (LESSP (SUB1 N) I)))
(INF (NEXT S (SUB1 N))))
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S N))).
This simplifies, applying KOENIG-INTRO, and opening up SUBSEQ, NOT, AND,
IMPLIES, and NEXT, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (INF (CONS N S)))
(LESSP (SUB1 N) I)
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S (SUB1 N)))).
However this again simplifies, using linear arithmetic, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (INF (CONS N S)))
(LESSP (SUB1 N) I)
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP N I)))
(INF (NEXT S (SUB1 N)))),
which again simplifies, expanding LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP I)
(NOT (EQUAL I 0))
(NOT (INF (CONS I S)))
(LESSP (SUB1 I) I)
(NODE-P S)
(INF (CONS I S))
(NOT (LESSP I I)))
(INF (NEXT S (SUB1 I)))),
which again simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INF-CONS-IMPLIES-INF-NEXT
(DEFN ALL-BIG-H
(S N)
(IF (ZEROP N)
(ADD1 (LENGTH S))
(PLUS (BIG-H (CONS N S))
(ALL-BIG-H S (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, ALL-BIG-H is accepted under the
principle of definition. From the definition we can conclude that:
(NUMBERP (ALL-BIG-H S N))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-BIG-H
(PROVE-LEMMA ALL-BIG-H-LENGTH
(REWRITE)
(LESSP (LENGTH S) (ALL-BIG-H S N)))
WARNING: Note that the proposed lemma ALL-BIG-H-LENGTH is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and zero replacement rules.
Name the conjecture *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP N) (p S N))
(IMPLIES (AND (NOT (ZEROP N)) (p S (SUB1 N)))
(p S N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to two new conjectures:
Case 2. (IMPLIES (ZEROP N)
(LESSP (LENGTH S) (ALL-BIG-H S N))),
which simplifies, applying SUB1-ADD1 and LENGTH-0, and unfolding the
functions ZEROP, EQUAL, ALL-BIG-H, and LESSP, to the following two new
formulas:
Case 2.2.
(IMPLIES (AND (EQUAL N 0) (LISTP S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))).
But this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (LENGTH S) 0) (LISTP S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))).
However this again simplifies, rewriting with LENGTH-0, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N)) (LISTP S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (LENGTH S) 0)
(NOT (NUMBERP N))
(LISTP S))
(LESSP (SUB1 (LENGTH S)) (LENGTH S))).
However this again simplifies, applying the lemma LENGTH-0, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(LESSP (LENGTH S)
(ALL-BIG-H S (SUB1 N))))
(LESSP (LENGTH S) (ALL-BIG-H S N))),
which simplifies, expanding the definitions of ZEROP and ALL-BIG-H, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (LENGTH S)
(ALL-BIG-H S (SUB1 N))))
(LESSP (LENGTH S)
(PLUS (BIG-H (CONS N S))
(ALL-BIG-H S (SUB1 N))))).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-BIG-H-LENGTH
(PROVE-LEMMA ALL-BIG-H-LESSP
(REWRITE)
(IMPLIES (AND (LESSP 0 I) (NOT (LESSP N I)))
(EQUAL (LESSP (BIG-H (CONS I S))
(ALL-BIG-H S N))
T))
((INDUCT (ALL-BIG-H S N))))
This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to two new formulas:
Case 2. (IMPLIES (AND (ZEROP N)
(LESSP 0 I)
(NOT (LESSP N I)))
(EQUAL (LESSP (BIG-H (CONS I S))
(ALL-BIG-H S N))
T)),
which simplifies, expanding the definitions of ZEROP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (LESSP 0 I)
(NOT (LESSP (SUB1 N) I)))
(EQUAL (LESSP (BIG-H (CONS I S))
(ALL-BIG-H S (SUB1 N)))
T))
(LESSP 0 I)
(NOT (LESSP N I)))
(EQUAL (LESSP (BIG-H (CONS I S))
(ALL-BIG-H S N))
T)),
which simplifies, unfolding EQUAL, LESSP, NOT, AND, IMPLIES, and ALL-BIG-H,
to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (SUB1 N) I)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP N I)))
(LESSP (BIG-H (CONS I S))
(PLUS (BIG-H (CONS N S))
(ALL-BIG-H S (SUB1 N))))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(LESSP (SUB1 I) I)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP I I)))
(LESSP (BIG-H (CONS I S))
(PLUS (BIG-H (CONS I S))
(ALL-BIG-H S (SUB1 I))))).
However this again simplifies, using linear arithmetic and applying
ALL-BIG-H-LENGTH, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (BIG-H (CONS I S))
(ALL-BIG-H S (SUB1 N)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (LESSP N I)))
(LESSP (BIG-H (CONS I S))
(PLUS (BIG-H (CONS N S))
(ALL-BIG-H S (SUB1 N))))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-BIG-H-LESSP
(DEFN FIRST-BRANCH
(S S1)
(IF (EQUAL S (CDR S1))
(CAR S1)
(IF (NLISTP S1)
0
(FIRST-BRANCH S (CDR S1)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT S1) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
FIRST-BRANCH is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
FIRST-BRANCH
(PROVE-LEMMA SUBSEQ-CONS-FIRST-BRANCH
(REWRITE)
(IMPLIES (AND (SUBSEQ S X) (NOT (EQUAL S X)))
(SUBSEQ (CONS (FIRST-BRANCH S X) S)
X)))
Give the conjecture the name *1.
Perhaps we can prove it by induction. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (EQUAL S X) (p S X))
(IMPLIES (AND (NOT (EQUAL S X)) (NLISTP X))
(p S X))
(IMPLIES (AND (NOT (EQUAL S X))
(NOT (NLISTP X))
(p S (CDR X)))
(p S X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP X)
(SUBSEQ S X)
(NOT (EQUAL S X)))
(SUBSEQ (CONS (FIRST-BRANCH S X) S)
X)).
This simplifies, opening up the functions NLISTP and SUBSEQ, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(NOT (SUBSEQ S (CDR X)))
(SUBSEQ S X)
(NOT (EQUAL S X)))
(SUBSEQ (CONS (FIRST-BRANCH S X) S)
X)).
This simplifies, opening up the functions NLISTP and SUBSEQ, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(EQUAL S (CDR X))
(SUBSEQ S X)
(NOT (EQUAL S X)))
(SUBSEQ (CONS (FIRST-BRANCH S X) S)
X)).
This simplifies, applying CONS-CAR-CDR, and opening up the functions NLISTP,
SUBSEQ, and FIRST-BRANCH, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(SUBSEQ (CONS (FIRST-BRANCH S (CDR X)) S)
(CDR X))
(SUBSEQ S X)
(NOT (EQUAL S X)))
(SUBSEQ (CONS (FIRST-BRANCH S X) S)
X)),
which simplifies, unfolding the functions NLISTP, SUBSEQ, and FIRST-BRANCH,
to two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP X)
(SUBSEQ (CONS (FIRST-BRANCH S (CDR X)) S)
(CDR X))
(SUBSEQ S (CDR X))
(NOT (EQUAL S X))
(NOT (EQUAL S (CDR X))))
(SUBSEQ (CONS (FIRST-BRANCH S (CDR X)) S)
X)),
which again simplifies, applying CAR-CONS, and opening up the function
SUBSEQ, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP X)
(SUBSEQ (CONS (FIRST-BRANCH S (CDR X)) S)
(CDR X))
(SUBSEQ S (CDR X))
(NOT (EQUAL S X))
(EQUAL S (CDR X)))
(SUBSEQ (CONS (CAR X) S) X)).
This again simplifies, rewriting with CONS-CAR-CDR, and expanding the
function SUBSEQ, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSEQ-CONS-FIRST-BRANCH
(PROVE-LEMMA LENGTH-NON-EQUAL
(REWRITE)
(IMPLIES (LESSP (LENGTH X) (LENGTH Y))
(EQUAL (EQUAL X Y) F)))
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-NON-EQUAL
(PROVE-LEMMA FIRST-BRANCH-OK-FOR-SUCCARD
(REWRITE)
(IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(AND (NUMBERP (FIRST-BRANCH S BIG-S))
(LESSP 0 (FIRST-BRANCH S BIG-S))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S))))))
WARNING: When the linear lemma FIRST-BRANCH-OK-FOR-SUCCARD is stored under
(SUCCARD S) it contains the free variable BIG-S which will be chosen by
instantiating the hypothesis (SUBSEQ S BIG-S).
WARNING: Note that the proposed lemma FIRST-BRANCH-OK-FOR-SUCCARD is to be
stored as zero type prescription rules, zero compound recognizer rules, three
linear rules, and one replacement rule.
This formula simplifies, unfolding the functions EQUAL, LESSP, NOT, and AND,
to three new formulas:
Case 3. (IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))),
which we will name *1.
Case 2. (IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (EQUAL (FIRST-BRANCH S BIG-S) 0))),
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 (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S)))
(IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S)))
(IMPLIES (AND (SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S))))).
We gave this the name *1 above. Perhaps we can prove it by induction. Six
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 (EQUAL S BIG-S) (p S BIG-S))
(IMPLIES (AND (NOT (EQUAL S BIG-S))
(NLISTP BIG-S))
(p S BIG-S))
(IMPLIES (AND (NOT (EQUAL S BIG-S))
(NOT (NLISTP BIG-S))
(p S (CDR BIG-S)))
(p S BIG-S))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT BIG-S) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following 15 new goals:
Case 15.(IMPLIES (AND (NLISTP BIG-S)
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))).
This simplifies, unfolding NLISTP and SUBSEQ, to:
T.
Case 14.(IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (SUBSEQ S (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))).
This simplifies, opening up NLISTP and SUBSEQ, to:
T.
Case 13.(IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (NODE-P (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))).
This simplifies, using linear arithmetic, rewriting with LENGTH-NON-EQUAL
and KOENIG-INTRO, and unfolding the definitions of NLISTP, SUBSEQ, and
LENGTH, to:
T.
Case 12.(IMPLIES (AND (NOT (NLISTP BIG-S))
(EQUAL S (CDR BIG-S))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))),
which simplifies, using linear arithmetic, rewriting with LENGTH-NON-EQUAL,
and expanding NLISTP, LENGTH, SUBSEQ, and FIRST-BRANCH, to:
(IMPLIES (AND (LISTP BIG-S) (NODE-P BIG-S))
(NUMBERP (CAR BIG-S))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS X Z) to eliminate
(CAR BIG-S) and (CDR BIG-S). This produces the new conjecture:
(IMPLIES (NODE-P (CONS X Z))
(NUMBERP X)),
which further simplifies, applying NODE-P-CONS, and unfolding the definition
of LESSP, to:
T.
Case 11.(IMPLIES (AND (NOT (NLISTP BIG-S))
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(LESSP 0 (FIRST-BRANCH S (CDR BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NUMBERP (FIRST-BRANCH S BIG-S))).
This simplifies, opening up the functions NLISTP, EQUAL, LESSP, SUBSEQ, and
FIRST-BRANCH, to the new formula:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH S (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S (CDR BIG-S))
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S))
(EQUAL S (CDR BIG-S)))
(NUMBERP (CAR BIG-S))),
which again simplifies, using linear arithmetic, applying LENGTH-NON-EQUAL,
and unfolding the functions SUBSEQ and LENGTH, to the new conjecture:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH (CDR BIG-S) (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S))))
(NODE-P BIG-S))
(NUMBERP (CAR BIG-S))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS Z X) to eliminate
(CDR BIG-S) and (CAR BIG-S). We would thus like to prove the new conjecture:
(IMPLIES (AND (NUMBERP (FIRST-BRANCH X X))
(NOT (EQUAL (FIRST-BRANCH X X) 0))
(NOT (LESSP (SUCCARD X)
(FIRST-BRANCH X X)))
(NODE-P (CONS Z X)))
(NUMBERP Z)),
which further simplifies, appealing to the lemma NODE-P-CONS, and unfolding
the function LESSP, to:
T.
Case 10.(IMPLIES (AND (NLISTP BIG-S)
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S))),
which simplifies, expanding the functions NLISTP and SUBSEQ, to:
T.
Case 9. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (SUBSEQ S (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S))),
which simplifies, expanding the functions NLISTP and SUBSEQ, to:
T.
Case 8. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (NODE-P (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S))),
which simplifies, using linear arithmetic, applying the lemmas
LENGTH-NON-EQUAL and KOENIG-INTRO, and opening up NLISTP, SUBSEQ, and LENGTH,
to:
T.
Case 7. (IMPLIES (AND (NOT (NLISTP BIG-S))
(EQUAL S (CDR BIG-S))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S))),
which simplifies, using linear arithmetic, rewriting with LENGTH-NON-EQUAL,
and expanding the functions NLISTP, LENGTH, SUBSEQ, FIRST-BRANCH, EQUAL, and
LESSP, to the following two new formulas:
Case 7.2.
(IMPLIES (AND (LISTP BIG-S) (NODE-P BIG-S))
(NOT (EQUAL (CAR BIG-S) 0))).
Appealing to the lemma CAR-CDR-ELIM, we now replace BIG-S by (CONS X Z) to
eliminate (CAR BIG-S) and (CDR BIG-S). The result is:
(IMPLIES (NODE-P (CONS X Z))
(NOT (EQUAL X 0))).
However this further simplifies, applying the lemma NODE-P-CONS, and
unfolding the function LESSP, to:
T.
Case 7.1.
(IMPLIES (AND (LISTP BIG-S) (NODE-P BIG-S))
(NUMBERP (CAR BIG-S))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS X Z) to eliminate
(CAR BIG-S) and (CDR BIG-S). This produces:
(IMPLIES (NODE-P (CONS X Z))
(NUMBERP X)),
which further simplifies, applying NODE-P-CONS, and opening up the
function LESSP, to:
T.
Case 6. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(LESSP 0 (FIRST-BRANCH S (CDR BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(LESSP 0 (FIRST-BRANCH S BIG-S))).
This simplifies, opening up the definitions of NLISTP, EQUAL, LESSP, SUBSEQ,
and FIRST-BRANCH, to the following two new goals:
Case 6.2.
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH S (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S (CDR BIG-S))
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S))
(EQUAL S (CDR BIG-S)))
(NOT (EQUAL (CAR BIG-S) 0))).
However this again simplifies, using linear arithmetic, applying
LENGTH-NON-EQUAL, and opening up SUBSEQ and LENGTH, to:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH (CDR BIG-S) (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S))))
(NODE-P BIG-S))
(NOT (EQUAL (CAR BIG-S) 0))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS Z X) to eliminate
(CDR BIG-S) and (CAR BIG-S). This produces:
(IMPLIES (AND (NUMBERP (FIRST-BRANCH X X))
(NOT (EQUAL (FIRST-BRANCH X X) 0))
(NOT (LESSP (SUCCARD X)
(FIRST-BRANCH X X)))
(NODE-P (CONS Z X)))
(NOT (EQUAL Z 0))),
which further simplifies, applying the lemma NODE-P-CONS, and unfolding
LESSP, to:
T.
Case 6.1.
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH S (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S (CDR BIG-S))
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S))
(EQUAL S (CDR BIG-S)))
(NUMBERP (CAR BIG-S))),
which again simplifies, using linear arithmetic, rewriting with
LENGTH-NON-EQUAL, and opening up the definitions of SUBSEQ and LENGTH, to
the new goal:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH (CDR BIG-S) (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S))))
(NODE-P BIG-S))
(NUMBERP (CAR BIG-S))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS Z X) to eliminate
(CDR BIG-S) and (CAR BIG-S). This produces:
(IMPLIES (AND (NUMBERP (FIRST-BRANCH X X))
(NOT (EQUAL (FIRST-BRANCH X X) 0))
(NOT (LESSP (SUCCARD X)
(FIRST-BRANCH X X)))
(NODE-P (CONS Z X)))
(NUMBERP Z)),
which further simplifies, applying NODE-P-CONS, and expanding the
definition of LESSP, to:
T.
Case 5. (IMPLIES (AND (NLISTP BIG-S)
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S)))).
This simplifies, opening up the definitions of NLISTP and SUBSEQ, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (SUBSEQ S (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S)))).
This simplifies, expanding NLISTP and SUBSEQ, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NOT (NODE-P (CDR BIG-S)))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S)))).
This simplifies, using linear arithmetic, applying LENGTH-NON-EQUAL and
KOENIG-INTRO, and expanding NLISTP, SUBSEQ, and LENGTH, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP BIG-S))
(EQUAL S (CDR BIG-S))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S)))),
which simplifies, using linear arithmetic, rewriting with LENGTH-NON-EQUAL,
and expanding NLISTP, LENGTH, SUBSEQ, and FIRST-BRANCH, to:
(IMPLIES (AND (LISTP BIG-S) (NODE-P BIG-S))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(CAR BIG-S)))).
Applying the lemma CAR-CDR-ELIM, replace BIG-S by (CONS Z X) to eliminate
(CDR BIG-S) and (CAR BIG-S). This produces the new goal:
(IMPLIES (NODE-P (CONS Z X))
(NOT (LESSP (SUCCARD X) Z))),
which further simplifies, rewriting with NODE-P-CONS, and unfolding the
functions EQUAL and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP BIG-S))
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(LESSP 0 (FIRST-BRANCH S (CDR BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S BIG-S)
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S)))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S BIG-S)))).
This simplifies, expanding NLISTP, EQUAL, LESSP, SUBSEQ, and FIRST-BRANCH,
to:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH S (CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH S (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD S)
(FIRST-BRANCH S (CDR BIG-S))))
(SUBSEQ S (CDR BIG-S))
(NODE-P BIG-S)
(NOT (EQUAL S BIG-S))
(EQUAL S (CDR BIG-S)))
(NOT (LESSP (SUCCARD S) (CAR BIG-S)))),
which again simplifies, using linear arithmetic, appealing to the lemma
LENGTH-NON-EQUAL, and unfolding SUBSEQ and LENGTH, to the conjecture:
(IMPLIES (AND (LISTP BIG-S)
(NUMBERP (FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S)))
(NOT (EQUAL (FIRST-BRANCH (CDR BIG-S) (CDR BIG-S))
0))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(FIRST-BRANCH (CDR BIG-S)
(CDR BIG-S))))
(NODE-P BIG-S))
(NOT (LESSP (SUCCARD (CDR BIG-S))
(CAR BIG-S)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace BIG-S by (CONS Z X) to
eliminate (CDR BIG-S) and (CAR BIG-S). This generates:
(IMPLIES (AND (NUMBERP (FIRST-BRANCH X X))
(NOT (EQUAL (FIRST-BRANCH X X) 0))
(NOT (LESSP (SUCCARD X)
(FIRST-BRANCH X X)))
(NODE-P (CONS Z X)))
(NOT (LESSP (SUCCARD X) Z))).
However this further simplifies, appealing to the lemma NODE-P-CONS, and
opening up the functions EQUAL and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
FIRST-BRANCH-OK-FOR-SUCCARD
(PROVE-LEMMA ALL-BIG-H-LESSP-LINEAR
(REWRITE)
(IMPLIES (AND (LESSP 0 I)
(NOT (LESSP (SUCCARD S) I)))
(LESSP (BIG-H (CONS I S))
(ALL-BIG-H S (SUCCARD S)))))
WARNING: When the linear lemma ALL-BIG-H-LESSP-LINEAR is stored under:
(ALL-BIG-H S (SUCCARD S))
it contains the free variable I which will be chosen by instantiating the
hypothesis (LESSP 0 I).
WARNING: Note that the proposed lemma ALL-BIG-H-LESSP-LINEAR is to be stored
as zero type prescription rules, zero compound recognizer rules, two linear
rules, and zero replacement rules.
This formula simplifies, using linear arithmetic, appealing to the lemma
ALL-BIG-H-LESSP, and unfolding the definitions of EQUAL and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-BIG-H-LESSP-LINEAR
(DISABLE ALL-BIG-H-LESSP)
[ 0.0 0.0 0.0 ]
ALL-BIG-H-LESSP-OFF
(PROVE-LEMMA INF-IMPLIES-INF-NEXT
(REWRITE)
(IMPLIES (AND (NODE-P S) (INF S))
(INF (NEXT S (SUCCARD S))))
((USE
(INF-SUFF (BIG-S (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(S (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S)))
(INF-NECC (BIG-H (ALL-BIG-H S (SUCCARD S)))
(S S))
(ALL-BIG-H-LESSP-LINEAR (I (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S))
S)))))
(DISABLE ALL-BIG-H-LESSP-LINEAR)))
This conjecture simplifies, using linear arithmetic, applying the lemmas
INF-IMPLIES-NODE-P and INF-CONS-IMPLIES-INF-NEXT, and unfolding the
definitions of AND, IMPLIES, NOT, EQUAL, and LESSP, to ten new formulas:
Case 10.(IMPLIES
(AND
(NOT (SUBSEQ (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S)
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(EQUAL (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
0)
(INF S))
(INF (NEXT S (SUCCARD S)))),
which again simplifies, using linear arithmetic and rewriting with
FIRST-BRANCH-OK-FOR-SUCCARD, ALL-BIG-H-LENGTH, and LENGTH-NON-EQUAL, to:
T.
Case 9. (IMPLIES
(AND
(NOT (SUBSEQ (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S)
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(NOT (NUMBERP (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(INF S))
(INF (NEXT S (SUCCARD S)))).
But this again simplifies, using linear arithmetic and rewriting with
LENGTH-NON-EQUAL, ALL-BIG-H-LENGTH, and SUBSEQ-CONS-FIRST-BRANCH, to:
T.
Case 8. (IMPLIES
(AND
(NOT (SUBSEQ (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S)
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP (SUCCARD S)
(FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(INF S))
(INF (NEXT S (SUCCARD S)))).
This again simplifies, using linear arithmetic and applying
FIRST-BRANCH-OK-FOR-SUCCARD, ALL-BIG-H-LENGTH, and LENGTH-NON-EQUAL, to:
T.
Case 7. (IMPLIES
(AND
(NOT (SUBSEQ (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S)
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(ALL-BIG-H S (SUCCARD S)))
(INF S))
(INF (NEXT S (SUCCARD S)))).
But this again simplifies, using linear arithmetic and appealing to the
lemmas LENGTH-NON-EQUAL, ALL-BIG-H-LENGTH, and SUBSEQ-CONS-FIRST-BRANCH, to:
T.
Case 6. (IMPLIES
(AND
(NOT
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(EQUAL (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
0)
(INF S))
(INF (NEXT S (SUCCARD S)))),
which again simplifies, using linear arithmetic and applying
FIRST-BRANCH-OK-FOR-SUCCARD, ALL-BIG-H-LENGTH, and LENGTH-NON-EQUAL, to:
T.
Case 5. (IMPLIES
(AND
(NOT
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(NOT (NUMBERP (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(INF S))
(INF (NEXT S (SUCCARD S)))).
This again simplifies, using linear arithmetic and appealing to the lemmas
LENGTH-NON-EQUAL, ALL-BIG-H-LENGTH, and FIRST-BRANCH-OK-FOR-SUCCARD, to:
T.
Case 4. (IMPLIES
(AND
(NOT
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP (SUCCARD S)
(FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(INF S))
(INF (NEXT S (SUCCARD S)))),
which again simplifies, using linear arithmetic and rewriting with
FIRST-BRANCH-OK-FOR-SUCCARD, ALL-BIG-H-LENGTH, and LENGTH-NON-EQUAL, to:
T.
Case 3. (IMPLIES
(AND
(NOT
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S))))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(ALL-BIG-H S (SUCCARD S)))
(INF S))
(INF (NEXT S (SUCCARD S)))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (INF (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP (SUCCARD S)
(FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(INF S))
(INF (NEXT S (SUCCARD S)))),
which again simplifies, using linear arithmetic and rewriting with the
lemmas FIRST-BRANCH-OK-FOR-SUCCARD, ALL-BIG-H-LENGTH, and LENGTH-NON-EQUAL,
to:
T.
Case 1. (IMPLIES
(AND
(INF (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(SUBSEQ S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(NODE-P (BIG-S (ALL-BIG-H S (SUCCARD S)) S))
(LESSP (ALL-BIG-H S (SUCCARD S))
(LENGTH (BIG-S (ALL-BIG-H S (SUCCARD S)) S)))
(LESSP
(BIG-H (CONS (FIRST-BRANCH S
(BIG-S (ALL-BIG-H S (SUCCARD S)) S))
S))
(ALL-BIG-H S (SUCCARD S)))
(INF S))
(INF (NEXT S (SUCCARD S)))),
which again simplifies, using linear arithmetic and rewriting with
LENGTH-NON-EQUAL, ALL-BIG-H-LENGTH, FIRST-BRANCH-OK-FOR-SUCCARD,
INF-IMPLIES-NODE-P, and INF-CONS-IMPLIES-INF-NEXT, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
INF-IMPLIES-INF-NEXT
(DEFN K
(N)
(IF (ZEROP N)
NIL
(NEXT (K (SUB1 N))
(SUCCARD (K (SUB1 N))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, K is accepted under the
definitional principle. Note that (OR (LITATOM (K N)) (LISTP (K N))) is a
theorem.
[ 0.0 0.0 0.0 ]
K
(PROVE-LEMMA SUBSEQ-NIL
(REWRITE)
(EQUAL (SUBSEQ NIL X) (PLISTP X))
((ENABLE SUBSEQ)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (EQUAL NIL X) (p X))
(IMPLIES (AND (NOT (EQUAL NIL X)) (NLISTP X))
(p X))
(IMPLIES (AND (NOT (EQUAL NIL X))
(NOT (NLISTP X))
(p (CDR X)))
(p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates the following three new formulas:
Case 3. (IMPLIES (EQUAL NIL X)
(EQUAL (SUBSEQ NIL X) (PLISTP X))).
This simplifies, expanding the definitions of SUBSEQ, PLISTP, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL NIL X)) (NLISTP X))
(EQUAL (SUBSEQ NIL X) (PLISTP X))).
This simplifies, opening up the functions NLISTP, SUBSEQ, PLISTP, and EQUAL,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL NIL X))
(NOT (NLISTP X))
(EQUAL (SUBSEQ NIL (CDR X))
(PLISTP (CDR X))))
(EQUAL (SUBSEQ NIL X) (PLISTP X))).
This simplifies, opening up the definitions of NLISTP, SUBSEQ, and PLISTP,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSEQ-NIL
(PROVE-LEMMA NODE-P-IMPLIES-PLISTP
(REWRITE)
(IMPLIES (NODE-P S) (PLISTP S)))
This simplifies, applying KOENIG-INTRO, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NODE-P-IMPLIES-PLISTP
(PROVE-LEMMA INF-NIL
(REWRITE)
(INF NIL)
((USE (INF-SUFF (BIG-S (S-HEIGHT (ADD1 (BIG-H NIL))))
(S NIL)))))
This formula can be simplified, using the abbreviation SUBSEQ-NIL, to the new
conjecture:
(IMPLIES (IMPLIES (AND (PLISTP (S-HEIGHT (ADD1 (BIG-H NIL))))
(NODE-P (S-HEIGHT (ADD1 (BIG-H NIL))))
(LESSP (BIG-H NIL)
(LENGTH (S-HEIGHT (ADD1 (BIG-H NIL))))))
(INF NIL))
(INF NIL)),
which simplifies, applying the lemmas NODE-P-S-HEIGHT, NODE-P-IMPLIES-PLISTP,
LENGTH-S-HEIGHT, and SUB1-ADD1, and unfolding the functions LESSP, AND, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL (BIG-H NIL) 0))
(NUMBERP (BIG-H NIL))
(NOT (LESSP (SUB1 (BIG-H NIL))
(BIG-H NIL))))
(INF NIL)).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INF-NIL
(DISABLE NODE-P-IMPLIES-PLISTP)
[ 0.0 0.0 0.0 ]
NODE-P-IMPLIES-PLISTP-OFF
(PROVE-LEMMA KONIG-TREE-LEMMA-1
(REWRITE)
(INF (K N)))
Call the conjecture *1.
Let us appeal to the induction principle. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to two new goals:
Case 2. (IMPLIES (ZEROP N) (INF (K N))),
which simplifies, applying INF-NIL, and expanding the functions ZEROP and K,
to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(INF (K (SUB1 N))))
(INF (K N))).
This simplifies, applying INF-IMPLIES-NODE-P and INF-IMPLIES-INF-NEXT, and
unfolding the functions ZEROP and K, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
KONIG-TREE-LEMMA-1
(PROVE-LEMMA LENGTH-NEXT
(REWRITE)
(IMPLIES (INF X)
(EQUAL (LENGTH (NEXT S N))
(ADD1 (LENGTH S)))))
WARNING: Note that LENGTH-NEXT contains the free variable X which will be
chosen by instantiating the hypothesis (INF X).
Give the conjecture the name *1.
We will appeal to induction. There are two plausible inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (ZEROP N) (p S N X))
(IMPLIES (AND (NOT (ZEROP N)) (INF (CONS N S)))
(p S N X))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (INF (CONS N S)))
(p S (SUB1 N) X))
(p S N X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme produces the following three new formulas:
Case 3. (IMPLIES (AND (ZEROP N) (INF X))
(EQUAL (LENGTH (NEXT S N))
(ADD1 (LENGTH S)))).
This simplifies, rewriting with the lemma CDR-CONS, and unfolding ZEROP,
EQUAL, NEXT, and LENGTH, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(INF (CONS N S))
(INF X))
(EQUAL (LENGTH (NEXT S N))
(ADD1 (LENGTH S)))).
This simplifies, rewriting with CDR-CONS, and expanding the functions ZEROP,
NEXT, and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (INF (CONS N S)))
(EQUAL (LENGTH (NEXT S (SUB1 N)))
(ADD1 (LENGTH S)))
(INF X))
(EQUAL (LENGTH (NEXT S N))
(ADD1 (LENGTH S)))),
which simplifies, unfolding the functions ZEROP and NEXT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-NEXT
(PROVE-LEMMA KONIG-TREE-LEMMA-2
(REWRITE)
(EQUAL (LENGTH (K N)) (FIX N)))
This formula simplifies, unfolding the definition of FIX, to the following two
new goals:
Case 2. (IMPLIES (NOT (NUMBERP N))
(EQUAL (LENGTH (K N)) 0)).
This again simplifies, unfolding the definitions of K, LENGTH, and EQUAL, to:
T.
Case 1. (IMPLIES (NUMBERP N)
(EQUAL (LENGTH (K N)) N)),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N))
(EQUAL (LENGTH (K N)) N)).
This simplifies, unfolding the definitions of ZEROP, NUMBERP, K, LENGTH, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (LENGTH (K (SUB1 N))) (SUB1 N))
(NUMBERP N))
(EQUAL (LENGTH (K N)) N)).
This simplifies, rewriting with the lemmas INF-NIL, ADD1-SUB1, and
LENGTH-NEXT, and opening up the functions ZEROP and K, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
KONIG-TREE-LEMMA-2
(PROVE-LEMMA SUBSEQ-NEXT
(REWRITE)
(IMPLIES (SUBSEQ S1 S2)
(SUBSEQ S1 (NEXT S2 N))))
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP N) (p S1 S2 N))
(IMPLIES (AND (NOT (ZEROP N))
(INF (CONS N S2)))
(p S1 S2 N))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (INF (CONS N S2)))
(p S1 S2 (SUB1 N)))
(p S1 S2 N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme generates three new conjectures:
Case 3. (IMPLIES (AND (ZEROP N) (SUBSEQ S1 S2))
(SUBSEQ S1 (NEXT S2 N))),
which simplifies, applying CDR-CONS, and opening up ZEROP, EQUAL, NEXT, and
SUBSEQ, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(INF (CONS N S2))
(SUBSEQ S1 S2))
(SUBSEQ S1 (NEXT S2 N))).
This simplifies, applying the lemma CDR-CONS, and unfolding the functions
ZEROP, NEXT, and SUBSEQ, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (INF (CONS N S2)))
(SUBSEQ S1 (NEXT S2 (SUB1 N)))
(SUBSEQ S1 S2))
(SUBSEQ S1 (NEXT S2 N))).
This simplifies, unfolding the functions ZEROP and NEXT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSEQ-NEXT
(PROVE-LEMMA KONIG-TREE-LEMMA-3
(REWRITE)
(IMPLIES (NOT (LESSP J I))
(SUBSEQ (K I) (K J)))
((INDUCT (K J))))
This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to the following two new conjectures:
Case 2. (IMPLIES (AND (ZEROP J) (NOT (LESSP J I)))
(SUBSEQ (K I) (K J))).
This simplifies, unfolding ZEROP, EQUAL, LESSP, K, and SUBSEQ, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(IMPLIES (NOT (LESSP (SUB1 J) I))
(SUBSEQ (K I) (K (SUB1 J))))
(NOT (LESSP J I)))
(SUBSEQ (K I) (K J))).
This simplifies, applying the lemma SUBSEQ-NEXT, and expanding NOT, IMPLIES,
and K, to:
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(LESSP (SUB1 J) I)
(NOT (LESSP J I)))
(SUBSEQ (K I)
(NEXT (K (SUB1 J))
(SUCCARD (K (SUB1 J)))))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP I))
(NOT (EQUAL J 0))
(NUMBERP J)
(LESSP (SUB1 J) I)
(NOT (LESSP J I)))
(SUBSEQ (K I)
(NEXT (K (SUB1 J))
(SUCCARD (K (SUB1 J)))))),
which again simplifies, opening up LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP I)
(NOT (EQUAL I 0))
(LESSP (SUB1 I) I)
(NOT (LESSP I I)))
(SUBSEQ (K I)
(NEXT (K (SUB1 I))
(SUCCARD (K (SUB1 I)))))),
which again simplifies, unfolding the functions K and SUBSEQ, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KONIG-TREE-LEMMA-3
(PROVE-LEMMA KONIG-TREE-LEMMA NIL
(AND (NODE-P (K N))
(IMPLIES (NOT (LESSP J I))
(SUBSEQ (K I) (K J)))
(EQUAL (LENGTH (K N)) (FIX N))))
This conjecture can be simplified, using the abbreviations NOT, IMPLIES, and
AND, to three new goals:
Case 3. (NODE-P (K N)),
which simplifies, rewriting with the lemmas KONIG-TREE-LEMMA-1 and
INF-IMPLIES-NODE-P, to:
T.
Case 2. (IMPLIES (NOT (LESSP J I))
(SUBSEQ (K I) (K J))),
which simplifies, rewriting with KONIG-TREE-LEMMA-3, to:
T.
Case 1. (EQUAL (LENGTH (K N)) (FIX N)).
This simplifies, rewriting with KONIG-TREE-LEMMA-2, and opening up the
function FIX, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KONIG-TREE-LEMMA
(PROVE-LEMMA KONIG-TREE-LEMMA-AGAIN NIL
(IMPLIES (NUMBERP N)
(AND (NODE-P (K N))
(IMPLIES (NOT (LESSP J I))
(SUBSEQ (K I) (K J)))
(EQUAL (LENGTH (K N)) N))))
This formula simplifies, appealing to the lemmas KONIG-TREE-LEMMA-1,
INF-IMPLIES-NODE-P, and KONIG-TREE-LEMMA-2, and expanding the definitions of
NOT, IMPLIES, and AND, to:
(IMPLIES (AND (NUMBERP N) (NOT (LESSP J I)))
(SUBSEQ (K I) (K J))),
which again simplifies, rewriting with the lemma KONIG-TREE-LEMMA-3, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KONIG-TREE-LEMMA-AGAIN