(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(DEFN DELETE
(X L)
(IF (LISTP L)
(IF (EQUAL X (CAR L))
(CDR L)
(CONS (CAR L) (DELETE X (CDR L))))
L))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, DELETE is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
DELETE
(DEFN BAGDIFF
(X Y)
(IF (LISTP Y)
(IF (MEMBER (CAR Y) X)
(BAGDIFF (DELETE (CAR Y) X) (CDR Y))
(BAGDIFF X (CDR Y)))
X))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in each
recursive call. Hence, BAGDIFF is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
BAGDIFF
(DEFN BAGINT
(X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X) Y)
(CONS (CAR X)
(BAGINT (CDR X) (DELETE (CAR X) Y)))
(BAGINT (CDR X) Y))
NIL))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, BAGINT is accepted under the principle of definition.
Note that (OR (LITATOM (BAGINT X Y)) (LISTP (BAGINT X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
BAGINT
(DEFN OCCURRENCES
(X L)
(IF (LISTP L)
(IF (EQUAL X (CAR L))
(ADD1 (OCCURRENCES X (CDR L)))
(OCCURRENCES X (CDR L)))
0))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, OCCURRENCES is accepted under the principle of
definition. From the definition we can conclude that:
(NUMBERP (OCCURRENCES X L))
is a theorem.
[ 0.0 0.0 0.0 ]
OCCURRENCES
(DEFN SUBBAGP
(X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X) Y)
(SUBBAGP (CDR X) (DELETE (CAR X) Y))
F)
T))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SUBBAGP is accepted under the principle of definition.
From the definition we can conclude that:
(OR (FALSEP (SUBBAGP X Y))
(TRUEP (SUBBAGP X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBBAGP
(LEMMA LISTP-DELETE
(REWRITE)
(EQUAL (LISTP (DELETE X L))
(IF (LISTP L)
(OR (NOT (EQUAL X (CAR L)))
(LISTP (CDR L)))
F))
((ENABLE DELETE)
(INDUCT (DELETE X L))))
This conjecture can be simplified, using the abbreviations NOT, OR, and AND,
to three new conjectures:
Case 3. (IMPLIES (AND (LISTP L) (EQUAL X (CAR L)))
(EQUAL (LISTP (DELETE X L))
(IF (LISTP L)
(OR (NOT (EQUAL X (CAR L)))
(LISTP (CDR L)))
F))),
which simplifies, opening up the definitions of DELETE, NOT, and OR, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (EQUAL X (CAR L)))
(EQUAL (LISTP (DELETE X (CDR L)))
(IF (LISTP (CDR L))
(OR (NOT (EQUAL X (CADR L)))
(LISTP (CDDR L)))
F)))
(EQUAL (LISTP (DELETE X L))
(IF (LISTP L)
(OR (NOT (EQUAL X (CAR L)))
(LISTP (CDR L)))
F))),
which simplifies, applying CONS-CAR-CDR, and unfolding DELETE, NOT, OR, and
EQUAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP L))
(EQUAL (LISTP (DELETE X L))
(IF (LISTP L)
(OR (NOT (EQUAL X (CAR L)))
(LISTP (CDR L)))
F))).
This simplifies, opening up DELETE and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LISTP-DELETE
(DISABLE LISTP-DELETE)
[ 0.0 0.0 0.0 ]
LISTP-DELETE-OFF
(LEMMA DELETE-NON-MEMBER
(REWRITE)
(IMPLIES (NOT (MEMBER X Y))
(EQUAL (DELETE X Y) Y))
((ENABLE DELETE)))
Give the conjecture the name *1.
We will try to prove it by induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP Y) (p X Y))
(IMPLIES (AND (NOT (NLISTP Y))
(EQUAL X (CAR Y)))
(p X Y))
(IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(p X (CDR Y)))
(p X Y))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates four new goals:
Case 4. (IMPLIES (AND (NLISTP Y) (NOT (MEMBER X Y)))
(EQUAL (DELETE X Y) Y)),
which simplifies, expanding NLISTP, MEMBER, and DELETE, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP Y))
(EQUAL X (CAR Y))
(NOT (MEMBER X Y)))
(EQUAL (DELETE X Y) Y)),
which simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(MEMBER X (CDR Y))
(NOT (MEMBER X Y)))
(EQUAL (DELETE X Y) Y)),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP Y))
(NOT (EQUAL X (CAR Y)))
(EQUAL (DELETE X (CDR Y)) (CDR Y))
(NOT (MEMBER X Y)))
(EQUAL (DELETE X Y) Y)),
which simplifies, rewriting with the lemma CONS-CAR-CDR, and unfolding the
functions NLISTP, MEMBER, and DELETE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-NON-MEMBER
(LEMMA DELETE-DELETE
(REWRITE)
(EQUAL (DELETE Y (DELETE X Z))
(DELETE X (DELETE Y Z)))
((ENABLE DELETE DELETE-NON-MEMBER)))
Call the conjecture *1.
Perhaps we can prove it by induction. Two inductions are suggested by
terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Z) (EQUAL X (CAR Z)))
(p Y X Z))
(IMPLIES (AND (LISTP Z)
(NOT (EQUAL X (CAR Z)))
(p Y X (CDR Z)))
(p Y X Z))
(IMPLIES (NOT (LISTP Z)) (p Y X Z))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT Z) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to three
new goals:
Case 3. (IMPLIES (AND (LISTP Z) (EQUAL X (CAR Z)))
(EQUAL (DELETE Y (DELETE X Z))
(DELETE X (DELETE Y Z)))),
which simplifies, opening up the definition of DELETE, to two new
conjectures:
Case 3.2.
(IMPLIES (AND (LISTP Z)
(NOT (EQUAL Y (CAR Z))))
(EQUAL (DELETE Y (CDR Z))
(DELETE (CAR Z)
(CONS (CAR Z) (DELETE Y (CDR Z)))))),
which again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
up the function DELETE, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP Z) (EQUAL Y (CAR Z)))
(EQUAL (DELETE Y (CDR Z))
(DELETE (CAR Z) (CDR Z)))).
This again simplifies, obviously, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(NOT (EQUAL X (CAR Z)))
(EQUAL (DELETE Y (DELETE X (CDR Z)))
(DELETE X (DELETE Y (CDR Z)))))
(EQUAL (DELETE Y (DELETE X Z))
(DELETE X (DELETE Y Z)))).
This simplifies, applying CDR-CONS and CAR-CONS, and opening up DELETE, to:
(IMPLIES (AND (LISTP Z)
(NOT (EQUAL X (CAR Z)))
(EQUAL (DELETE Y (DELETE X (CDR Z)))
(DELETE X (DELETE Y (CDR Z))))
(NOT (EQUAL Y (CAR Z))))
(EQUAL (CONS (CAR Z)
(DELETE X (DELETE Y (CDR Z))))
(DELETE X
(CONS (CAR Z) (DELETE Y (CDR Z)))))).
But this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
and expanding the definition of DELETE, to:
T.
Case 1. (IMPLIES (NOT (LISTP Z))
(EQUAL (DELETE Y (DELETE X Z))
(DELETE X (DELETE Y Z)))),
which simplifies, applying DELETE-NON-MEMBER, and expanding the definition
of MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-DELETE
(LEMMA EQUAL-OCCURRENCES-ZERO
(REWRITE)
(EQUAL (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L)))
((ENABLE OCCURRENCES)))
This conjecture simplifies, unfolding NOT, to two new conjectures:
Case 2. (IMPLIES (NOT (EQUAL (OCCURRENCES X L) 0))
(MEMBER X L)),
which we will name *1.
Case 1. (IMPLIES (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L))),
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 (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L))).
We gave this the name *1 above. Perhaps we can prove it by induction. Two
inductions are suggested by terms in the conjecture. However, they merge into
one likely candidate induction. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP L)
(EQUAL X (CAR L))
(p X (CDR L)))
(p X L))
(IMPLIES (AND (LISTP L)
(NOT (EQUAL X (CAR L)))
(p X (CDR L)))
(p X L))
(IMPLIES (NOT (LISTP L)) (p X L))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to the following three new
formulas:
Case 3. (IMPLIES (AND (LISTP L)
(EQUAL X (CAR L))
(EQUAL (EQUAL (OCCURRENCES X (CDR L)) 0)
(NOT (MEMBER X (CDR L)))))
(EQUAL (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L)))).
This simplifies, unfolding the definitions of NOT, OCCURRENCES, MEMBER,
EQUAL, and ADD1, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (EQUAL X (CAR L)))
(EQUAL (EQUAL (OCCURRENCES X (CDR L)) 0)
(NOT (MEMBER X (CDR L)))))
(EQUAL (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L)))).
This simplifies, expanding the definitions of NOT, OCCURRENCES, MEMBER, and
EQUAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP L))
(EQUAL (EQUAL (OCCURRENCES X L) 0)
(NOT (MEMBER X L)))).
This simplifies, expanding the definitions of OCCURRENCES, EQUAL, MEMBER,
and NOT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
EQUAL-OCCURRENCES-ZERO
(LEMMA MEMBER-NON-LIST
(REWRITE)
(IMPLIES (NOT (LISTP L))
(NOT (MEMBER X L))))
This formula simplifies, opening up the definition of MEMBER, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-NON-LIST
(LEMMA MEMBER-DELETE
(REWRITE)
(EQUAL (MEMBER X (DELETE Y L))
(IF (MEMBER X L)
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X L))
T)
F))
((ENABLE DELETE OCCURRENCES)))
This simplifies, obviously, to three new goals:
Case 3. (IMPLIES (NOT (MEMBER X L))
(EQUAL (MEMBER X (DELETE Y L)) F)),
which again simplifies, trivially, to:
(IMPLIES (NOT (MEMBER X L))
(NOT (MEMBER X (DELETE Y L)))),
which we will name *1.
Case 2. (IMPLIES (AND (MEMBER X L) (EQUAL X Y))
(EQUAL (MEMBER X (DELETE Y L))
(LESSP 1 (OCCURRENCES X L)))).
This again simplifies, obviously, to:
(IMPLIES (MEMBER Y L)
(EQUAL (MEMBER Y (DELETE Y L))
(LESSP 1 (OCCURRENCES Y L)))),
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 X (DELETE Y L))
(IF (MEMBER X L)
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X L))
T)
F)).
We named this *1. We will try to prove it by induction. There are three
plausible inductions. However, they merge into one likely candidate induction.
We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
(p X Y L))
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(p X Y (CDR L)))
(p X Y L))
(IMPLIES (NOT (LISTP L)) (p X Y L))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces three new conjectures:
Case 3. (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
(EQUAL (MEMBER X (DELETE Y L))
(IF (MEMBER X L)
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X L))
T)
F))),
which simplifies, applying SUB1-ADD1, and unfolding DELETE, MEMBER,
OCCURRENCES, SUB1, NUMBERP, EQUAL, and LESSP, to the following four new
conjectures:
Case 3.4.
(IMPLIES (AND (LISTP L)
(EQUAL X (CAR L))
(NOT (EQUAL (OCCURRENCES X (CDR L)) 0)))
(EQUAL (MEMBER X (CDR L)) T)).
This again simplifies, clearly, to:
(IMPLIES (AND (LISTP L)
(NOT (EQUAL (OCCURRENCES (CAR L) (CDR L))
0)))
(MEMBER (CAR L) (CDR L))).
Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z V) to eliminate
(CAR L) and (CDR L). We thus obtain:
(IMPLIES (NOT (EQUAL (OCCURRENCES Z V) 0))
(MEMBER Z V)),
which we will name *1.1.
Case 3.3.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL X (CAR L)))
(MEMBER X (CDR L)))
(EQUAL (MEMBER X (CDR L)) T)).
This again simplifies, clearly, to:
T.
Case 3.2.
(IMPLIES (AND (LISTP L)
(EQUAL X (CAR L))
(EQUAL (OCCURRENCES X (CDR L)) 0))
(EQUAL (MEMBER X (CDR L)) F)).
This again simplifies, clearly, to:
(IMPLIES (AND (LISTP L)
(EQUAL (OCCURRENCES (CAR L) (CDR L))
0))
(NOT (MEMBER (CAR L) (CDR L)))).
Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z V) to eliminate
(CAR L) and (CDR L). We would thus like to prove the new formula:
(IMPLIES (EQUAL (OCCURRENCES Z V) 0)
(NOT (MEMBER Z V))),
which we will name *1.2.
Case 3.1.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL X (CAR L)))
(NOT (MEMBER X (CDR L))))
(EQUAL (MEMBER X (CDR L)) F)).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(EQUAL (MEMBER X (DELETE Y (CDR L)))
(IF (MEMBER X (CDR L))
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X (CDR L)))
T)
F)))
(EQUAL (MEMBER X (DELETE Y L))
(IF (MEMBER X L)
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X L))
T)
F))).
This simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and opening up
the definitions of DELETE, MEMBER, OCCURRENCES, SUB1, NUMBERP, EQUAL, and
LESSP, to three new formulas:
Case 2.3.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(NOT (MEMBER X (CDR L)))
(EQUAL (MEMBER X (DELETE Y (CDR L)))
F)
(EQUAL X (CAR L))
(EQUAL X Y))
(NOT (EQUAL (OCCURRENCES X (CDR L)) 0))),
which again simplifies, clearly, to:
T.
Case 2.2.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(MEMBER X (CDR L))
(EQUAL X Y)
(EQUAL (MEMBER X (DELETE Y (CDR L)))
(LESSP 1 (OCCURRENCES X (CDR L))))
(NOT (EQUAL X (CAR L))))
(EQUAL (MEMBER X
(CONS (CAR L) (DELETE X (CDR L))))
(LESSP 1 (OCCURRENCES X (CDR L))))).
This again simplifies, applying CDR-CONS and CAR-CONS, and expanding
MEMBER, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(MEMBER X (CDR L))
(EQUAL X Y)
(EQUAL (MEMBER X (DELETE Y (CDR L)))
(LESSP 1 (OCCURRENCES X (CDR L))))
(EQUAL X (CAR L)))
(EQUAL (MEMBER X (CDR L))
(LESSP 1
(ADD1 (OCCURRENCES X (CDR L)))))).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (NOT (LISTP L))
(EQUAL (MEMBER X (DELETE Y L))
(IF (MEMBER X L)
(IF (EQUAL X Y)
(LESSP 1 (OCCURRENCES X L))
T)
F))).
This simplifies, unfolding the functions DELETE, MEMBER, and EQUAL, to:
T.
So next consider:
(IMPLIES (EQUAL (OCCURRENCES Z V) 0)
(NOT (MEMBER Z V))),
which we named *1.2 above. We will appeal to induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP V)
(EQUAL Z (CAR V))
(p Z (CDR V)))
(p Z V))
(IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(p Z (CDR V)))
(p Z V))
(IMPLIES (NOT (LISTP V)) (p Z V))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT V) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme produces five
new conjectures:
Case 5. (IMPLIES (AND (LISTP V)
(EQUAL Z (CAR V))
(NOT (EQUAL (OCCURRENCES Z (CDR V)) 0))
(EQUAL (OCCURRENCES Z V) 0))
(NOT (MEMBER Z V))),
which simplifies, expanding the function OCCURRENCES, to:
T.
Case 4. (IMPLIES (AND (LISTP V)
(EQUAL Z (CAR V))
(NOT (MEMBER Z (CDR V)))
(EQUAL (OCCURRENCES Z V) 0))
(NOT (MEMBER Z V))),
which simplifies, expanding the definition of OCCURRENCES, to:
T.
Case 3. (IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(NOT (EQUAL (OCCURRENCES Z (CDR V)) 0))
(EQUAL (OCCURRENCES Z V) 0))
(NOT (MEMBER Z V))),
which simplifies, unfolding the function OCCURRENCES, to:
T.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(NOT (MEMBER Z (CDR V)))
(EQUAL (OCCURRENCES Z V) 0))
(NOT (MEMBER Z V))),
which simplifies, expanding the definitions of OCCURRENCES and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP V))
(EQUAL (OCCURRENCES Z V) 0))
(NOT (MEMBER Z V))),
which simplifies, unfolding the functions OCCURRENCES, EQUAL, and MEMBER, to:
T.
That finishes the proof of *1.2.
So let us turn our attention to:
(IMPLIES (NOT (EQUAL (OCCURRENCES Z V) 0))
(MEMBER Z V)),
which is formula *1.1 above. Let us appeal to the induction principle. 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 V)
(EQUAL Z (CAR V))
(p Z (CDR V)))
(p Z V))
(IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(p Z (CDR V)))
(p Z V))
(IMPLIES (NOT (LISTP V)) (p Z V))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT V)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to five new conjectures:
Case 5. (IMPLIES (AND (LISTP V)
(EQUAL Z (CAR V))
(EQUAL (OCCURRENCES Z (CDR V)) 0)
(NOT (EQUAL (OCCURRENCES Z V) 0)))
(MEMBER Z V)),
which simplifies, opening up ADD1, OCCURRENCES, EQUAL, and MEMBER, to:
T.
Case 4. (IMPLIES (AND (LISTP V)
(EQUAL Z (CAR V))
(MEMBER Z (CDR V))
(NOT (EQUAL (OCCURRENCES Z V) 0)))
(MEMBER Z V)),
which simplifies, expanding the functions OCCURRENCES and MEMBER, to:
T.
Case 3. (IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(EQUAL (OCCURRENCES Z (CDR V)) 0)
(NOT (EQUAL (OCCURRENCES Z V) 0)))
(MEMBER Z V)),
which simplifies, unfolding OCCURRENCES and EQUAL, to:
T.
Case 2. (IMPLIES (AND (LISTP V)
(NOT (EQUAL Z (CAR V)))
(MEMBER Z (CDR V))
(NOT (EQUAL (OCCURRENCES Z V) 0)))
(MEMBER Z V)),
which simplifies, expanding the functions OCCURRENCES and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP V))
(NOT (EQUAL (OCCURRENCES Z V) 0)))
(MEMBER Z V)),
which simplifies, opening up the functions OCCURRENCES and EQUAL, to:
T.
That finishes the proof of *1.1, which, in turn, finishes the proof of *1.
Q.E.D.
[ 0.0 0.1 0.3 ]
MEMBER-DELETE
(LEMMA MEMBER-DELETE-IMPLIES-MEMBERSHIP
(REWRITE)
(IMPLIES (MEMBER X (DELETE Y L))
(MEMBER X L))
((ENABLE DELETE)))
WARNING: Note that MEMBER-DELETE-IMPLIES-MEMBERSHIP contains the free
variable Y which will be chosen by instantiating the hypothesis
(MEMBER X (DELETE Y L)).
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
(p X L Y))
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(p X (CDR L) Y))
(p X L Y))
(IMPLIES (NOT (LISTP L)) (p X L Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (LISTP L)
(EQUAL Y (CAR L))
(MEMBER X (DELETE Y L)))
(MEMBER X L)),
which simplifies, expanding the functions DELETE and MEMBER, to:
T.
Case 3. (IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(NOT (MEMBER X (DELETE Y (CDR L))))
(MEMBER X (DELETE Y L)))
(MEMBER X L)),
which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
expanding DELETE and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(MEMBER X (CDR L))
(MEMBER X (DELETE Y L)))
(MEMBER X L)),
which simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
opening up the functions DELETE and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP L))
(MEMBER X (DELETE Y L)))
(MEMBER X L)),
which simplifies, expanding DELETE and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-DELETE-IMPLIES-MEMBERSHIP
(LEMMA OCCURRENCES-DELETE
(REWRITE)
(EQUAL (OCCURRENCES X (DELETE Y L))
(IF (EQUAL X Y)
(IF (MEMBER X L)
(SUB1 (OCCURRENCES X L))
0)
(OCCURRENCES X L)))
((ENABLE OCCURRENCES DELETE EQUAL-OCCURRENCES-ZERO)))
This conjecture simplifies, clearly, to three new conjectures:
Case 3. (IMPLIES (NOT (EQUAL X Y))
(EQUAL (OCCURRENCES X (DELETE Y L))
(OCCURRENCES X L))),
which we will name *1.
Case 2. (IMPLIES (AND (EQUAL X Y) (MEMBER X L))
(EQUAL (OCCURRENCES X (DELETE Y L))
(SUB1 (OCCURRENCES X L)))).
This again simplifies, obviously, to:
(IMPLIES (MEMBER Y L)
(EQUAL (OCCURRENCES Y (DELETE Y L))
(SUB1 (OCCURRENCES Y L)))),
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 (OCCURRENCES X (DELETE Y L))
(IF (EQUAL X Y)
(IF (MEMBER X L)
(SUB1 (OCCURRENCES X L))
0)
(OCCURRENCES X L))),
named *1. Let us appeal to the induction principle. Four inductions are
suggested by terms in the conjecture. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
(p X Y L))
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(p X Y (CDR L)))
(p X Y L))
(IMPLIES (NOT (LISTP L)) (p X Y L))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces three new conjectures:
Case 3. (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
(EQUAL (OCCURRENCES X (DELETE Y L))
(IF (EQUAL X Y)
(IF (MEMBER X L)
(SUB1 (OCCURRENCES X L))
0)
(OCCURRENCES X L)))),
which simplifies, applying SUB1-ADD1, and expanding the definitions of
DELETE, MEMBER, and OCCURRENCES, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
(IF (EQUAL X Y)
(IF (MEMBER X (CDR L))
(SUB1 (OCCURRENCES X (CDR L)))
0)
(OCCURRENCES X (CDR L)))))
(EQUAL (OCCURRENCES X (DELETE Y L))
(IF (EQUAL X Y)
(IF (MEMBER X L)
(SUB1 (OCCURRENCES X L))
0)
(OCCURRENCES X L)))).
This simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and expanding
the functions DELETE, OCCURRENCES, and MEMBER, to three new goals:
Case 2.3.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(EQUAL X Y)
(MEMBER X (CDR L))
(EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
(SUB1 (OCCURRENCES X (CDR L))))
(NOT (EQUAL X (CAR L))))
(EQUAL (OCCURRENCES X
(CONS (CAR L) (DELETE X (CDR L))))
(SUB1 (OCCURRENCES X (CDR L))))),
which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
function OCCURRENCES, to:
T.
Case 2.2.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(EQUAL X Y)
(MEMBER X (CDR L))
(EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
(SUB1 (OCCURRENCES X (CDR L))))
(EQUAL X (CAR L)))
(EQUAL (OCCURRENCES X (CDR L))
(SUB1 (ADD1 (OCCURRENCES X (CDR L)))))).
This again simplifies, clearly, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP L)
(NOT (EQUAL Y (CAR L)))
(EQUAL X Y)
(NOT (MEMBER X (CDR L)))
(EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
0)
(NOT (EQUAL X (CAR L))))
(EQUAL (OCCURRENCES X
(CONS (CAR L) (DELETE X (CDR L))))
0)).
This again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, CDR-CONS,
and CAR-CONS, and unfolding OCCURRENCES, to:
T.
Case 1. (IMPLIES (NOT (LISTP L))
(EQUAL (OCCURRENCES X (DELETE Y L))
(IF (EQUAL X Y)
(IF (MEMBER X L)
(SUB1 (OCCURRENCES X L))
0)
(OCCURRENCES X L)))).
This simplifies, unfolding DELETE, OCCURRENCES, MEMBER, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
OCCURRENCES-DELETE
(LEMMA MEMBER-BAGDIFF
(REWRITE)
(EQUAL (MEMBER X (BAGDIFF A B))
(LESSP (OCCURRENCES X B)
(OCCURRENCES X A)))
((ENABLE BAGDIFF OCCURRENCES EQUAL-OCCURRENCES-ZERO OCCURRENCES-DELETE)))
Call the conjecture *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 B)
(MEMBER (CAR B) A)
(p X (DELETE (CAR B) A) (CDR B)))
(p X A B))
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(p X A (CDR B)))
(p X A B))
(IMPLIES (NOT (LISTP B)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT B)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instances chosen for A. The
above induction scheme generates three new goals:
Case 3. (IMPLIES (AND (LISTP B)
(MEMBER (CAR B) A)
(EQUAL (MEMBER X
(BAGDIFF (DELETE (CAR B) A) (CDR B)))
(LESSP (OCCURRENCES X (CDR B))
(OCCURRENCES X (DELETE (CAR B) A)))))
(EQUAL (MEMBER X (BAGDIFF A B))
(LESSP (OCCURRENCES X B)
(OCCURRENCES X A)))),
which simplifies, appealing to the lemmas OCCURRENCES-DELETE, SUB1-ADD1, and
EQUAL-OCCURRENCES-ZERO, and unfolding BAGDIFF, OCCURRENCES, and LESSP, to:
(IMPLIES (AND (LISTP B)
(MEMBER (CAR B) A)
(EQUAL X (CAR B))
(NOT (MEMBER X A))
(EQUAL (MEMBER X
(BAGDIFF (DELETE (CAR B) A) (CDR B)))
(LESSP (OCCURRENCES X (CDR B)) 0)))
(NOT (MEMBER X (BAGDIFF A (CDR B))))).
This again simplifies, clearly, to:
T.
Case 2. (IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (MEMBER X (BAGDIFF A (CDR B)))
(LESSP (OCCURRENCES X (CDR B))
(OCCURRENCES X A))))
(EQUAL (MEMBER X (BAGDIFF A B))
(LESSP (OCCURRENCES X B)
(OCCURRENCES X A)))).
This simplifies, expanding the functions BAGDIFF and OCCURRENCES, to the
following two new goals:
Case 2.2.
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (MEMBER X (BAGDIFF A (CDR B)))
(LESSP (OCCURRENCES X (CDR B))
(OCCURRENCES X A)))
(NOT (EQUAL X (CAR B))))
(EQUAL (MEMBER X (BAGDIFF A (CDR B)))
(LESSP (OCCURRENCES X (CDR B))
(OCCURRENCES X A)))).
This again simplifies, obviously, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (MEMBER X (BAGDIFF A (CDR B)))
(LESSP (OCCURRENCES X (CDR B))
(OCCURRENCES X A)))
(EQUAL X (CAR B)))
(EQUAL (MEMBER X (BAGDIFF A (CDR B)))
(LESSP (ADD1 (OCCURRENCES X (CDR B)))
(OCCURRENCES X A)))).
But this again simplifies, appealing to the lemma EQUAL-OCCURRENCES-ZERO,
and unfolding the functions LESSP and EQUAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP B))
(EQUAL (MEMBER X (BAGDIFF A B))
(LESSP (OCCURRENCES X B)
(OCCURRENCES X A)))),
which simplifies, rewriting with the lemma EQUAL-OCCURRENCES-ZERO, and
expanding the functions BAGDIFF, OCCURRENCES, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-BAGDIFF
(LEMMA BAGDIFF-DELETE
(REWRITE)
(EQUAL (BAGDIFF (DELETE E X) Y)
(DELETE E (BAGDIFF X Y)))
((ENABLE BAGDIFF DELETE DELETE-DELETE DELETE-NON-MEMBER MEMBER-BAGDIFF
MEMBER-DELETE OCCURRENCES-DELETE)))
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP Y)
(MEMBER (CAR Y) (DELETE E X))
(p E X (CDR Y))
(p E (DELETE (CAR Y) X) (CDR Y)))
(p E X Y))
(IMPLIES (AND (LISTP Y)
(NOT (MEMBER (CAR Y) (DELETE E X)))
(p E X (CDR Y))
(p E (DELETE (CAR Y) X) (CDR Y)))
(p E X Y))
(IMPLIES (NOT (LISTP Y)) (p E X Y))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive instances
chosen for X. The above induction scheme leads to three new goals:
Case 3. (IMPLIES (AND (LISTP Y)
(MEMBER (CAR Y) (DELETE E X))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E (BAGDIFF X (CDR Y))))
(EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
(CDR Y))
(DELETE E
(BAGDIFF (DELETE (CAR Y) X)
(CDR Y)))))
(EQUAL (BAGDIFF (DELETE E X) Y)
(DELETE E (BAGDIFF X Y)))),
which simplifies, applying the lemmas MEMBER-DELETE and DELETE-DELETE, and
opening up the definition of BAGDIFF, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(NOT (MEMBER (CAR Y) (DELETE E X)))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E (BAGDIFF X (CDR Y))))
(EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
(CDR Y))
(DELETE E
(BAGDIFF (DELETE (CAR Y) X)
(CDR Y)))))
(EQUAL (BAGDIFF (DELETE E X) Y)
(DELETE E (BAGDIFF X Y)))),
which simplifies, rewriting with MEMBER-DELETE, and opening up the function
BAGDIFF, to the following two new goals:
Case 2.2.
(IMPLIES (AND (LISTP Y)
(EQUAL (CAR Y) E)
(NOT (LESSP 1 (OCCURRENCES E X)))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E (BAGDIFF X (CDR Y))))
(EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
(CDR Y))
(DELETE E
(BAGDIFF (DELETE (CAR Y) X) (CDR Y))))
(NOT (MEMBER E X)))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E (BAGDIFF X (CDR Y))))).
This again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP Y)
(EQUAL (CAR Y) E)
(NOT (LESSP 1 (OCCURRENCES E X)))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E (BAGDIFF X (CDR Y))))
(EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
(CDR Y))
(DELETE E
(BAGDIFF (DELETE (CAR Y) X) (CDR Y))))
(MEMBER E X))
(EQUAL (BAGDIFF (DELETE E X) (CDR Y))
(DELETE E
(BAGDIFF (DELETE (CAR Y) X)
(CDR Y))))).
But this again simplifies, using linear arithmetic, applying MEMBER-DELETE,
DELETE-NON-MEMBER, MEMBER-BAGDIFF, and OCCURRENCES-DELETE, and opening up
the function SUB1, to:
T.
Case 1. (IMPLIES (NOT (LISTP Y))
(EQUAL (BAGDIFF (DELETE E X) Y)
(DELETE E (BAGDIFF X Y)))).
This simplifies, unfolding the definition of BAGDIFF, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
BAGDIFF-DELETE
(LEMMA SUBBAGP-DELETE
(REWRITE)
(IMPLIES (SUBBAGP X (DELETE U Y))
(SUBBAGP X Y))
((ENABLE DELETE SUBBAGP DELETE-DELETE MEMBER-DELETE-IMPLIES-MEMBERSHIP)))
WARNING: Note that SUBBAGP-DELETE contains the free variable U which will be
chosen by instantiating the hypothesis (SUBBAGP X (DELETE U Y)).
Give the conjecture the name *1.
Let us appeal to the induction principle. Three inductions are suggested
by terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (DELETE U Y))
(p (CDR X) (DELETE (CAR X) Y) U))
(p X Y U))
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) (DELETE U Y))))
(p X Y U))
(IMPLIES (NOT (LISTP X)) (p X Y U))).
Linear arithmetic and the lemma CDR-LESSP establish 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 Y. The above
induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (DELETE U Y))
(NOT (SUBBAGP (CDR X)
(DELETE U (DELETE (CAR X) Y))))
(SUBBAGP X (DELETE U Y)))
(SUBBAGP X Y)),
which simplifies, applying DELETE-DELETE, and opening up SUBBAGP, to:
T.
Case 3. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (DELETE U Y))
(SUBBAGP (CDR X) (DELETE (CAR X) Y))
(SUBBAGP X (DELETE U Y)))
(SUBBAGP X Y)).
This simplifies, applying the lemmas DELETE-DELETE and
MEMBER-DELETE-IMPLIES-MEMBERSHIP, and unfolding the function SUBBAGP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) (DELETE U Y)))
(SUBBAGP X (DELETE U Y)))
(SUBBAGP X Y)).
This simplifies, unfolding the function SUBBAGP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X))
(SUBBAGP X (DELETE U Y)))
(SUBBAGP X Y)).
This simplifies, unfolding the definition of SUBBAGP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBBAGP-DELETE
(LEMMA SUBBAGP-CDR1
(REWRITE)
(IMPLIES (SUBBAGP X Y)
(SUBBAGP (CDR X) Y))
((ENABLE SUBBAGP SUBBAGP-DELETE)))
.
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X)
and (CAR X). We thus obtain the following two new goals:
Case 2. (IMPLIES (AND (NOT (LISTP X)) (SUBBAGP X Y))
(SUBBAGP (CDR X) Y)).
But this simplifies, applying CDR-NLISTP, and expanding SUBBAGP and LISTP,
to:
T.
Case 1. (IMPLIES (SUBBAGP (CONS V Z) Y)
(SUBBAGP Z Y)).
However this simplifies, rewriting with CDR-CONS, CAR-CONS, and
SUBBAGP-DELETE, and expanding the definition of SUBBAGP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUBBAGP-CDR1
(LEMMA SUBBAGP-CDR2
(REWRITE)
(IMPLIES (SUBBAGP X (CDR Y))
(SUBBAGP X Y))
((ENABLE DELETE SUBBAGP DELETE-NON-MEMBER SUBBAGP-CDR1)))
.
Applying the lemma CAR-CDR-ELIM, replace Y by (CONS V Z) to eliminate (CDR Y)
and (CAR Y). We thus obtain the following two new goals:
Case 2. (IMPLIES (AND (NOT (LISTP Y))
(SUBBAGP X (CDR Y)))
(SUBBAGP X Y)).
But this simplifies, applying CDR-NLISTP, and expanding MEMBER, LISTP, and
SUBBAGP, to:
T.
Case 1. (IMPLIES (SUBBAGP X Z)
(SUBBAGP X (CONS V Z))),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (SUBBAGP X (CDR Y))
(SUBBAGP X Y)),
which we named *1 above. We will appeal to induction. Two inductions are
suggested by terms in the conjecture. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(p (CDR X) (DELETE (CAR X) Y)))
(p X Y))
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) (CDR Y))))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p 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. Note, however, the inductive instance chosen for Y. The above
induction scheme leads to the following four new conjectures:
Case 4. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(NOT (SUBBAGP (CDR X)
(CDR (DELETE (CAR X) Y))))
(SUBBAGP X (CDR Y)))
(SUBBAGP X Y)).
This simplifies, unfolding SUBBAGP and MEMBER, to the following two new
conjectures:
Case 4.2.
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(NOT (SUBBAGP (CDR X)
(CDR (DELETE (CAR X) Y))))
(SUBBAGP (CDR X)
(DELETE (CAR X) (CDR Y))))
(LISTP Y)).
But this again simplifies, rewriting with CDR-NLISTP, and opening up LISTP
and MEMBER, to:
T.
Case 4.1.
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(NOT (SUBBAGP (CDR X)
(CDR (DELETE (CAR X) Y))))
(SUBBAGP (CDR X)
(DELETE (CAR X) (CDR Y))))
(SUBBAGP (CDR X) (DELETE (CAR X) Y))).
This further simplifies, rewriting with CDR-NLISTP, DELETE-NON-MEMBER, and
SUBBAGP-CDR1, and unfolding the definitions of DELETE, MEMBER, LISTP, and
SUBBAGP, to the new formula:
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(LISTP Y)
(NOT (EQUAL (CAR X) (CAR Y)))
(NOT (SUBBAGP (CDR X)
(CDR (CONS (CAR Y)
(DELETE (CAR X) (CDR Y))))))
(SUBBAGP (CDR X)
(DELETE (CAR X) (CDR Y))))
(SUBBAGP (CDR X)
(CONS (CAR Y)
(DELETE (CAR X) (CDR Y))))),
which again simplifies, rewriting with CDR-CONS, to:
T.
Case 3. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(SUBBAGP (CDR X) (DELETE (CAR X) Y))
(SUBBAGP X (CDR Y)))
(SUBBAGP X Y)).
This simplifies, unfolding the definitions of SUBBAGP and MEMBER, to:
(IMPLIES (AND (LISTP X)
(MEMBER (CAR X) (CDR Y))
(SUBBAGP (CDR X) (DELETE (CAR X) Y))
(SUBBAGP (CDR X)
(DELETE (CAR X) (CDR Y))))
(LISTP Y)),
which again simplifies, applying CDR-NLISTP, and opening up the functions
LISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) (CDR Y)))
(SUBBAGP X (CDR Y)))
(SUBBAGP X Y)).
This simplifies, unfolding the definition of SUBBAGP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X))
(SUBBAGP X (CDR Y)))
(SUBBAGP X Y)).
This simplifies, unfolding the function SUBBAGP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBBAGP-CDR2
(LEMMA SUBBAGP-BAGINT1
(REWRITE)
(SUBBAGP (BAGINT X Y) X)
((ENABLE DELETE SUBBAGP BAGINT SUBBAGP-CDR2)))
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 X)
(MEMBER (CAR X) Y)
(p (CDR X) (DELETE (CAR X) Y)))
(p X Y))
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y))
(p (CDR X) Y))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instances chosen for Y. The
above induction scheme leads to three new formulas:
Case 3. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) Y)
(SUBBAGP (BAGINT (CDR X) (DELETE (CAR X) Y))
(CDR X)))
(SUBBAGP (BAGINT X Y) X)),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
definitions of BAGINT, DELETE, MEMBER, and SUBBAGP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y))
(SUBBAGP (BAGINT (CDR X) Y) (CDR X)))
(SUBBAGP (BAGINT X Y) X)).
This simplifies, applying SUBBAGP-CDR2, and unfolding BAGINT, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(SUBBAGP (BAGINT X Y) X)),
which simplifies, appealing to the lemmas SUBBAGP-CDR2 and CDR-NLISTP, and
unfolding BAGINT, CDR, LISTP, and SUBBAGP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBBAGP-BAGINT1
(LEMMA SUBBAGP-BAGINT2
(REWRITE)
(SUBBAGP (BAGINT X Y) Y)
((ENABLE SUBBAGP BAGINT SUBBAGP-CDR2)))
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 X)
(MEMBER (CAR X) Y)
(p (CDR X) (DELETE (CAR X) Y)))
(p X Y))
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y))
(p (CDR X) Y))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instances chosen for Y. The
above induction scheme leads to three new formulas:
Case 3. (IMPLIES (AND (LISTP X)
(MEMBER (CAR X) Y)
(SUBBAGP (BAGINT (CDR X) (DELETE (CAR X) Y))
(DELETE (CAR X) Y)))
(SUBBAGP (BAGINT X Y) Y)),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
definitions of BAGINT and SUBBAGP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y))
(SUBBAGP (BAGINT (CDR X) Y) Y))
(SUBBAGP (BAGINT X Y) Y)).
This simplifies, expanding BAGINT, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(SUBBAGP (BAGINT X Y) Y)).
This simplifies, applying SUBBAGP-CDR2, and opening up the functions BAGINT,
SUBBAGP, and LISTP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBBAGP-BAGINT2
(PROVE-LEMMA OCCURRENCES-BAGINT
(REWRITE)
(EQUAL (OCCURRENCES X (BAGINT A B))
(IF (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(OCCURRENCES X A)
(OCCURRENCES X B)))
((ENABLE OCCURRENCES BAGINT EQUAL-OCCURRENCES-ZERO
OCCURRENCES-DELETE)))
This formula simplifies, obviously, to the following two new conjectures:
Case 2. (IMPLIES (NOT (LESSP (OCCURRENCES X A)
(OCCURRENCES X B)))
(EQUAL (OCCURRENCES X (BAGINT A B))
(OCCURRENCES X B))).
Call the above conjecture *1.
Case 1. (IMPLIES (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(EQUAL (OCCURRENCES X (BAGINT A B))
(OCCURRENCES X A))),
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 (OCCURRENCES X (BAGINT A B))
(IF (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(OCCURRENCES X A)
(OCCURRENCES X B))).
We gave this the name *1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest five 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 A)
(MEMBER (CAR A) B)
(p X (CDR A) (DELETE (CAR A) B)))
(p X A B))
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(p X (CDR A) B))
(p X A B))
(IMPLIES (NOT (LISTP A)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instances chosen for B. The
above induction scheme leads to the following three new goals:
Case 3. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(EQUAL (OCCURRENCES X
(BAGINT (CDR A) (DELETE (CAR A) B)))
(IF (LESSP (OCCURRENCES X (CDR A))
(OCCURRENCES X (DELETE (CAR A) B)))
(OCCURRENCES X (CDR A))
(OCCURRENCES X (DELETE (CAR A) B)))))
(EQUAL (OCCURRENCES X (BAGINT A B))
(IF (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(OCCURRENCES X A)
(OCCURRENCES X B)))).
This simplifies, applying OCCURRENCES-DELETE, EQUAL-OCCURRENCES-ZERO,
CDR-CONS, CAR-CONS, SUB1-ADD1, and ADD1-SUB1, and opening up the definitions
of BAGINT, OCCURRENCES, and LESSP, to two new goals:
Case 3.2.
(IMPLIES
(AND (LISTP A)
(MEMBER (CAR A) B)
(EQUAL X (CAR A))
(NOT (MEMBER X B))
(NOT (LESSP (OCCURRENCES X (CDR A)) 0))
(EQUAL (OCCURRENCES X
(BAGINT (CDR A) (DELETE (CAR A) B)))
0))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(OCCURRENCES X B))),
which again simplifies, trivially, to:
T.
Case 3.1.
(IMPLIES
(AND (LISTP A)
(MEMBER (CAR A) B)
(EQUAL X (CAR A))
(NOT (MEMBER X B))
(LESSP (OCCURRENCES X (CDR A)) 0)
(EQUAL (OCCURRENCES X
(BAGINT (CDR A) (DELETE (CAR A) B)))
(OCCURRENCES X (CDR A))))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(OCCURRENCES X B))).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(IF (LESSP (OCCURRENCES X (CDR A))
(OCCURRENCES X B))
(OCCURRENCES X (CDR A))
(OCCURRENCES X B))))
(EQUAL (OCCURRENCES X (BAGINT A B))
(IF (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(OCCURRENCES X A)
(OCCURRENCES X B)))).
This simplifies, expanding the functions BAGINT and OCCURRENCES, to the
following three new conjectures:
Case 2.3.
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(NOT (LESSP (OCCURRENCES X (CDR A))
(OCCURRENCES X B)))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(OCCURRENCES X B))
(EQUAL X (CAR A))
(LESSP (ADD1 (OCCURRENCES X (CDR A)))
(OCCURRENCES X B)))
(EQUAL (OCCURRENCES X B)
(ADD1 (OCCURRENCES X (CDR A))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(LESSP (OCCURRENCES X (CDR A))
(OCCURRENCES X B))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(OCCURRENCES X (CDR A)))
(EQUAL X (CAR A))
(NOT (LESSP (ADD1 (OCCURRENCES X (CDR A)))
(OCCURRENCES X B))))
(EQUAL (OCCURRENCES X (CDR A))
(OCCURRENCES X B))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (OCCURRENCES (CAR A) B)
(PLUS 1
(OCCURRENCES (CAR A) (CDR A))))
(LISTP A)
(NOT (MEMBER (CAR A) B))
(LESSP (OCCURRENCES (CAR A) (CDR A))
(PLUS 1
(OCCURRENCES (CAR A) (CDR A))))
(EQUAL (OCCURRENCES (CAR A)
(BAGINT (CDR A) B))
(OCCURRENCES (CAR A) (CDR A)))
(NOT (LESSP (ADD1 (OCCURRENCES (CAR A) (CDR A)))
(PLUS 1
(OCCURRENCES (CAR A) (CDR A))))))
(EQUAL (OCCURRENCES (CAR A) (CDR A))
(PLUS 1
(OCCURRENCES (CAR A) (CDR A))))).
But this again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, and
unfolding the definition of LESSP, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(LESSP (OCCURRENCES X (CDR A))
(OCCURRENCES X B))
(EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
(OCCURRENCES X (CDR A)))
(EQUAL X (CAR A))
(LESSP (ADD1 (OCCURRENCES X (CDR A)))
(OCCURRENCES X B)))
(EQUAL (OCCURRENCES X (CDR A))
(ADD1 (OCCURRENCES X (CDR A))))).
However this again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, and
opening up LESSP, to:
T.
Case 1. (IMPLIES (NOT (LISTP A))
(EQUAL (OCCURRENCES X (BAGINT A B))
(IF (LESSP (OCCURRENCES X A)
(OCCURRENCES X B))
(OCCURRENCES X A)
(OCCURRENCES X B)))).
This simplifies, appealing to the lemma EQUAL-OCCURRENCES-ZERO, and
expanding BAGINT, LISTP, OCCURRENCES, EQUAL, and LESSP, to:
(IMPLIES (AND (NOT (LISTP A))
(NOT (MEMBER X B)))
(EQUAL 0 (OCCURRENCES X B))),
which again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
OCCURRENCES-BAGINT
(PROVE-LEMMA OCCURRENCES-BAGDIFF
(REWRITE)
(EQUAL (OCCURRENCES X (BAGDIFF A B))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X B)))
((ENABLE OCCURRENCES BAGDIFF EQUAL-OCCURRENCES-ZERO
OCCURRENCES-DELETE)))
Call the conjecture *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 B)
(MEMBER (CAR B) A)
(p X (DELETE (CAR B) A) (CDR B)))
(p X A B))
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(p X A (CDR B)))
(p X A B))
(IMPLIES (NOT (LISTP B)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT B)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. Note, however, the inductive instances chosen for A. The
above induction scheme generates three new goals:
Case 3. (IMPLIES (AND (LISTP B)
(MEMBER (CAR B) A)
(EQUAL (OCCURRENCES X
(BAGDIFF (DELETE (CAR B) A) (CDR B)))
(DIFFERENCE (OCCURRENCES X (DELETE (CAR B) A))
(OCCURRENCES X (CDR B)))))
(EQUAL (OCCURRENCES X (BAGDIFF A B))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X B)))),
which simplifies, appealing to the lemmas OCCURRENCES-DELETE, SUB1-ADD1,
EQUAL-OCCURRENCES-ZERO, and MEMBER-BAGDIFF, and unfolding BAGDIFF,
OCCURRENCES, DIFFERENCE, and LESSP, to:
T.
Case 2. (IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X (CDR B)))))
(EQUAL (OCCURRENCES X (BAGDIFF A B))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X B)))),
which simplifies, opening up BAGDIFF and OCCURRENCES, to two new goals:
Case 2.2.
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X (CDR B))))
(NOT (EQUAL X (CAR B))))
(EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X (CDR B))))),
which again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP B)
(NOT (MEMBER (CAR B) A))
(EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X (CDR B))))
(EQUAL X (CAR B)))
(EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
(DIFFERENCE (OCCURRENCES X A)
(ADD1 (OCCURRENCES X (CDR B)))))).
But this again simplifies, applying EQUAL-OCCURRENCES-ZERO and
MEMBER-BAGDIFF, and unfolding DIFFERENCE and LESSP, to:
T.
Case 1. (IMPLIES (NOT (LISTP B))
(EQUAL (OCCURRENCES X (BAGDIFF A B))
(DIFFERENCE (OCCURRENCES X A)
(OCCURRENCES X B)))).
This simplifies, applying EQUAL-OCCURRENCES-ZERO, and opening up the
functions BAGDIFF, OCCURRENCES, EQUAL, and DIFFERENCE, to:
(IMPLIES (AND (NOT (LISTP B))
(NOT (MEMBER X A)))
(EQUAL (OCCURRENCES X A) 0)).
But this again simplifies, rewriting with the lemma EQUAL-OCCURRENCES-ZERO,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
OCCURRENCES-BAGDIFF
(PROVE-LEMMA MEMBER-BAGINT
(REWRITE)
(EQUAL (MEMBER X (BAGINT A B))
(AND (MEMBER X A) (MEMBER X B)))
((ENABLE BAGINT MEMBER-DELETE)))
This simplifies, opening up the function AND, to two new conjectures:
Case 2. (IMPLIES (NOT (MEMBER X A))
(EQUAL (MEMBER X (BAGINT A B)) F)),
which again simplifies, clearly, to:
(IMPLIES (NOT (MEMBER X A))
(NOT (MEMBER X (BAGINT A B)))),
which we will name *1.
Case 1. (IMPLIES (MEMBER X A)
(EQUAL (MEMBER X (BAGINT A B))
(MEMBER X B))),
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 (MEMBER X (BAGINT A B))
(AND (MEMBER X A) (MEMBER X B))),
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 A)
(MEMBER (CAR A) B)
(p X (CDR A) (DELETE (CAR A) B)))
(p X A B))
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(p X (CDR A) B))
(p X A B))
(IMPLIES (NOT (LISTP A)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT A) decreases according to the well-founded relation LESSP in each
induction step of the scheme. Note, however, the inductive instances chosen
for B. The above induction scheme produces three new conjectures:
Case 3. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(EQUAL (MEMBER X
(BAGINT (CDR A) (DELETE (CAR A) B)))
(AND (MEMBER X (CDR A))
(MEMBER X (DELETE (CAR A) B)))))
(EQUAL (MEMBER X (BAGINT A B))
(AND (MEMBER X A) (MEMBER X B)))),
which simplifies, applying the lemmas MEMBER-DELETE, CDR-CONS, and CAR-CONS,
and expanding AND, BAGINT, MEMBER, and EQUAL, to two new goals:
Case 3.2.
(IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(NOT (MEMBER X B))
(EQUAL (MEMBER X
(BAGINT (CDR A) (DELETE (CAR A) B)))
F))
(NOT (EQUAL X (CAR A)))),
which again simplifies, trivially, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(NOT (MEMBER X (CDR A)))
(EQUAL (MEMBER X
(BAGINT (CDR A) (DELETE (CAR A) B)))
F)
(EQUAL X (CAR A)))
(EQUAL (MEMBER X B) T)).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(EQUAL (MEMBER X (BAGINT (CDR A) B))
(AND (MEMBER X (CDR A))
(MEMBER X B))))
(EQUAL (MEMBER X (BAGINT A B))
(AND (MEMBER X A) (MEMBER X B)))).
This simplifies, unfolding the definitions of AND, BAGINT, and MEMBER, to
the new conjecture:
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(NOT (MEMBER X (CDR A)))
(EQUAL (MEMBER X (BAGINT (CDR A) B))
F)
(EQUAL X (CAR A)))
(NOT (MEMBER X B))),
which again simplifies, clearly, to:
T.
Case 1. (IMPLIES (NOT (LISTP A))
(EQUAL (MEMBER X (BAGINT A B))
(AND (MEMBER X A) (MEMBER X B)))).
This simplifies, rewriting with MEMBER-NON-LIST, and expanding the
definitions of BAGINT, AND, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-BAGINT
(DEFTHEORY BAGS
(OCCURRENCES-BAGINT BAGDIFF-DELETE OCCURRENCES-BAGDIFF
MEMBER-BAGINT MEMBER-BAGDIFF SUBBAGP-BAGINT2
SUBBAGP-BAGINT1 SUBBAGP-CDR2 SUBBAGP-CDR1
SUBBAGP-DELETE))
[ 0.0 0.0 0.0 ]
BAGS
(MAKE-LIB "bags" T)
Making the lib for "bags".
Compiling the lib for "bags".
Loading ./numbers/bags.o
Finished loading ./numbers/bags.o
Finished compiling the lib for "bags".
Finished making the lib for "bags".
(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/numbers/bags.lib
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/numbers/bags.lisp)