(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(DEFN LENGTH
(X)
(IF (LISTP X)
(ADD1 (LENGTH (CDR X)))
0))
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, LENGTH is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (LENGTH X)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN MERGE
(L M)
(IF (NOT (LISTP L))
M
(IF (NOT (LISTP M))
L
(IF (LESSP (CAR L) (CAR M))
(CONS (CAR L) (MERGE (CDR L) M))
(CONS (CAR M) (MERGE L (CDR M))))))
((LESSP (PLUS (LENGTH L) (LENGTH M)))))
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP,
PLUS, and LENGTH inform us that the measure (PLUS (LENGTH L) (LENGTH M))
decreases according to the well-founded relation LESSP in each recursive call.
Hence, MERGE is accepted under the principle of definition. Note that:
(OR (LISTP (MERGE L M))
(EQUAL (MERGE L M) M))
is a theorem.
[ 0.0 0.0 0.0 ]
MERGE
(DEFN ODDS
(L)
(IF (NOT (LISTP L))
NIL
(CONS (CAR L) (ODDS (CDDR L)))))
Linear arithmetic and the lemmas CDR-LESSEQP and CDR-LESSP establish that
the measure (COUNT L) decreases according to the well-founded relation LESSP
in each recursive call. Hence, ODDS is accepted under the definitional
principle. Note that (OR (LITATOM (ODDS L)) (LISTP (ODDS L))) is a theorem.
[ 0.0 0.0 0.0 ]
ODDS
(PROVE-LEMMA MERGESORT-HELPER
(REWRITE)
(IMPLIES (AND (LISTP L) (LISTP (CDR L)))
(AND (EQUAL (LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))
T)
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDR L))))
(LENGTH (CDR L)))
T))))
WARNING: Note that the proposed lemma MERGESORT-HELPER is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.
This formula simplifies, expanding AND, to the following two new goals:
Case 2. (IMPLIES (AND (LISTP L) (LISTP (CDR L)))
(LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS Z X) to
eliminate (CDR L) and (CAR L). The result is the goal:
(IMPLIES (LISTP X)
(LESSP (SUB1 (LENGTH (ODDS (CONS Z X))))
(LENGTH X))),
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 (LISTP L) (LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))
T))
(IMPLIES (AND (LISTP L) (LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDR L))))
(LENGTH (CDR L)))
T))).
We gave this the name *1 above. Perhaps we can prove it by induction. There
is only one plausible induction. We will induct according to the following
scheme:
(AND (IMPLIES (NOT (LISTP L)) (p L))
(IMPLIES (AND (LISTP L) (p (CDDR L)))
(p L))).
Linear arithmetic and the lemmas CDR-LESSEQP and CDR-LESSP can be used to
prove 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 six new goals:
Case 6. (IMPLIES (AND (NOT (LISTP (CDDR L)))
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))
T)),
which simplifies, rewriting with CDR-CONS and SUB1-ADD1, and expanding the
definitions of ODDS, LENGTH, and ADD1, to:
(IMPLIES (AND (NOT (LISTP (CDDR L)))
(LISTP L)
(LISTP (CDR L)))
(LESSP (LENGTH (ODDS (CDDR L))) 1)),
which further simplifies, opening up the functions ODDS, LENGTH, and LESSP,
to:
T.
Case 5. (IMPLIES (AND (NOT (LISTP (CDDDR L)))
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))
T)),
which simplifies, applying CDR-CONS and SUB1-ADD1, and expanding ODDS,
LENGTH, ADD1, and LESSP, to the following two new goals:
Case 5.2.
(IMPLIES (AND (NOT (LISTP (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDR L))) 0))
(LISTP (CDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
1)).
However this further simplifies, rewriting with the lemmas CDR-NLISTP and
CDR-CONS, and expanding the definitions of ODDS, ADD1, LENGTH, EQUAL, SUB1,
and LESSP, to:
T.
Case 5.1.
(IMPLIES (AND (NOT (LISTP (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDR L))) 0))
(NOT (LISTP (CDDR L))))
(LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
0)),
which again simplifies, rewriting with CDR-NLISTP, and expanding the
definitions of LISTP, EQUAL, and LESSP, to the new goal:
(IMPLIES (AND (LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDR L))) 0)))
(LISTP (CDDR L))),
which further simplifies, opening up ODDS, LENGTH, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
T)
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
T)
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS L)))
(LENGTH (CDR L)))
T)),
which simplifies, applying CDR-CONS and SUB1-ADD1, and expanding ODDS,
LENGTH, and LESSP, to the following two new conjectures:
Case 4.2.
(IMPLIES (AND (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDR L))) 0))
(LISTP (CDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(ADD1 (LENGTH (CDDDR L))))).
This again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDR L))) 0))
(NOT (LISTP (CDDR L))))
(LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
0)),
which again simplifies, rewriting with the lemma CDR-NLISTP, and expanding
LENGTH, EQUAL, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (LISTP (CDDR L)))
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDR L))))
(LENGTH (CDR L)))
T)),
which simplifies, applying CDR-NLISTP and CDR-CONS, and expanding the
functions ODDS, ADD1, LENGTH, SUB1, LESSP, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP (CDDDR L)))
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDR L))))
(LENGTH (CDR L)))
T)).
This simplifies, rewriting with CDR-CONS, and unfolding ODDS, ADD1, LENGTH,
SUB1, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
T)
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
T)
(LISTP L)
(LISTP (CDR L)))
(EQUAL (LESSP (SUB1 (LENGTH (ODDS (CDR L))))
(LENGTH (CDR L)))
T)),
which simplifies, applying CDR-CONS and SUB1-ADD1, and unfolding the
definitions of ODDS, LENGTH, and LESSP, to the following two new formulas:
Case 1.2.
(IMPLIES (AND (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDDR L))) 0))
(LISTP (CDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(ADD1 (LENGTH (CDDDR L))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (LESSP (SUB1 (LENGTH (ODDS (CDDR L))))
(LENGTH (CDDDR L)))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
(LENGTH (CDDDR L)))
(LISTP L)
(LISTP (CDR L))
(NOT (EQUAL (LENGTH (ODDS (CDDDR L))) 0))
(NOT (LISTP (CDDR L))))
(LESSP (SUB1 (LENGTH (ODDS (CDDDR L))))
0)),
which again simplifies, rewriting with CDR-NLISTP, and opening up the
definitions of LENGTH, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MERGESORT-HELPER
(DEFN MERGESORT
(L)
(IF (NOT (LISTP L))
NIL
(IF (NOT (LISTP (CDR L)))
L
(MERGE (MERGESORT (ODDS (CDR L)))
(MERGESORT (ODDS L)))))
((LESSP (LENGTH L))))
The lemmas SUB1-ADD1 and MERGESORT-HELPER and the definitions of LESSP
and LENGTH establish that the measure (LENGTH L) decreases according to the
well-founded relation LESSP in each recursive call. Hence, MERGESORT is
accepted under the principle of definition. Note that:
(OR (LITATOM (MERGESORT L))
(LISTP (MERGESORT L)))
is a theorem.
[ 0.0 0.0 0.0 ]
MERGESORT
(DEFN SORTEDP
(X)
(IF (LISTP X)
(IF (LISTP (CDR X))
(AND (NOT (LESSP (CAR (CDR X)) (CAR X)))
(SORTEDP (CDR X)))
T)
T))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SORTEDP is accepted under the principle of definition.
Observe that (OR (FALSEP (SORTEDP X)) (TRUEP (SORTEDP X))) is a theorem.
[ 0.0 0.0 0.0 ]
SORTEDP
(PROVE-LEMMA SORTEDP-MERGESORT
(REWRITE)
(SORTEDP (MERGESORT X)))
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 (NOT (LISTP X)) (p X))
(IMPLIES (AND (LISTP X) (NOT (LISTP (CDR X))))
(p X))
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(p (ODDS X))
(p (ODDS (CDR X))))
(p X))).
The lemmas SUB1-ADD1 and MERGESORT-HELPER and the definitions of LESSP and
LENGTH inform us that the measure (LENGTH X) 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 (NOT (LISTP X))
(SORTEDP (MERGESORT X))),
which simplifies, expanding the definitions of MERGESORT and SORTEDP, to:
T.
Case 2. (IMPLIES (AND (LISTP X) (NOT (LISTP (CDR X))))
(SORTEDP (MERGESORT X))),
which simplifies, expanding the definitions of MERGESORT and SORTEDP, to:
T.
Case 1. (IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(SORTEDP (MERGESORT (ODDS X)))
(SORTEDP (MERGESORT (ODDS (CDR X)))))
(SORTEDP (MERGESORT X))),
which simplifies, unfolding the definition of MERGESORT, to:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(SORTEDP (MERGESORT (ODDS X)))
(SORTEDP (MERGESORT (ODDS (CDR X)))))
(SORTEDP (MERGE (MERGESORT (ODDS (CDR X)))
(MERGESORT (ODDS X))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to
eliminate (CDR X) and (CAR X). This generates the conjecture:
(IMPLIES (AND (LISTP Z)
(SORTEDP (MERGESORT (ODDS (CONS V Z))))
(SORTEDP (MERGESORT (ODDS Z))))
(SORTEDP (MERGE (MERGESORT (ODDS Z))
(MERGESORT (ODDS (CONS V Z)))))).
We will try to prove the above formula by generalizing it, replacing
(ODDS Z) by Y and (ODDS (CONS V Z)) by A. The result is the formula:
(IMPLIES (AND (LISTP Z)
(SORTEDP (MERGESORT A))
(SORTEDP (MERGESORT Y)))
(SORTEDP (MERGE (MERGESORT Y) (MERGESORT A)))).
We will try to prove the above formula by generalizing it, replacing
(MERGESORT Y) by U and (MERGESORT A) by B. We must thus prove:
(IMPLIES (AND (LISTP Z)
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))).
Eliminate the irrelevant term. We would thus like to prove:
(IMPLIES (AND (SORTEDP B) (SORTEDP U))
(SORTEDP (MERGE U B))),
which we will finally name *1.1.
We will appeal to induction. Three inductions are suggested by terms in
the conjecture. However, they merge into one likely candidate induction. We
will induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP U)) (p U B))
(IMPLIES (AND (LISTP U) (NOT (LISTP B)))
(p U B))
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(p (CDR U) B))
(p U B))
(IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(p U (CDR B)))
(p U B))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and LENGTH establish that the measure (PLUS (LENGTH U) (LENGTH B)) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following six new conjectures:
Case 6. (IMPLIES (AND (NOT (LISTP U))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))).
This simplifies, opening up MERGE and SORTEDP, to the following two new
conjectures:
Case 6.2.
(IMPLIES (AND (NOT (LISTP U))
(SORTEDP B)
(SORTEDP U)
(LISTP B)
(LISTP (CDR B)))
(NOT (LESSP (CADR B) (CAR B)))).
However this further simplifies, opening up SORTEDP, to:
T.
Case 6.1.
(IMPLIES (AND (NOT (LISTP U))
(SORTEDP B)
(SORTEDP U)
(LISTP B)
(LISTP (CDR B)))
(SORTEDP (CDR B))),
which further simplifies, opening up the definition of SORTEDP, to:
T.
Case 5. (IMPLIES (AND (LISTP U)
(NOT (LISTP B))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))),
which simplifies, opening up the functions MERGE and SORTEDP, to two new
conjectures:
Case 5.2.
(IMPLIES (AND (LISTP U)
(NOT (LISTP B))
(SORTEDP B)
(SORTEDP U)
(LISTP (CDR U)))
(SORTEDP (CDR U))),
which further simplifies, opening up SORTEDP, to:
T.
Case 5.1.
(IMPLIES (AND (LISTP U)
(NOT (LISTP B))
(SORTEDP B)
(SORTEDP U)
(LISTP (CDR U)))
(NOT (LESSP (CADR U) (CAR U)))),
which further simplifies, opening up the definition of SORTEDP, to:
T.
Case 4. (IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(NOT (SORTEDP (CDR U)))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))),
which simplifies, applying CAR-CONS and CDR-CONS, and unfolding the
functions MERGE and SORTEDP, to the following two new formulas:
Case 4.2.
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(NOT (SORTEDP (CDR U)))
(SORTEDP B)
(SORTEDP U))
(NOT (LESSP (CAR (MERGE (CDR U) B))
(CAR U)))).
This further simplifies, opening up SORTEDP and MERGE, to:
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(NOT (SORTEDP (CDR U)))
(SORTEDP B)
(NOT (LISTP (CDR U))))
(NOT (LESSP (CAR B) (CAR U)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(NOT (SORTEDP (CDR U)))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE (CDR U) B))),
which further simplifies, opening up the definitions of SORTEDP and MERGE,
to:
T.
Case 3. (IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(SORTEDP (MERGE (CDR U) B))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))),
which simplifies, rewriting with CAR-CONS and CDR-CONS, and opening up the
functions MERGE and SORTEDP, to:
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(SORTEDP (MERGE (CDR U) B))
(SORTEDP B)
(SORTEDP U))
(NOT (LESSP (CAR (MERGE (CDR U) B))
(CAR U)))),
which further simplifies, unfolding the functions SORTEDP and MERGE, to two
new conjectures:
Case 3.2.
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(SORTEDP (MERGE (CDR U) B))
(SORTEDP B)
(NOT (LISTP (CDR U))))
(NOT (LESSP (CAR B) (CAR U)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP U)
(LISTP B)
(LESSP (CAR U) (CAR B))
(SORTEDP (MERGE (CDR U) B))
(SORTEDP B)
(NOT (LESSP (CADR U) (CAR U)))
(SORTEDP (CDR U)))
(NOT (LESSP (CAR (MERGE (CDR U) B))
(CAR U)))).
Applying the lemma CAR-CDR-ELIM, replace U by (CONS X Z) to eliminate
(CAR U) and (CDR U) and Z by (CONS V W) to eliminate (CAR Z) and (CDR Z).
We thus obtain the following two new goals:
Case 3.1.2.
(IMPLIES (AND (NOT (LISTP Z))
(LISTP B)
(LESSP X (CAR B))
(SORTEDP (MERGE Z B))
(SORTEDP B)
(NOT (LESSP (CAR Z) X))
(SORTEDP Z))
(NOT (LESSP (CAR (MERGE Z B)) X))).
This further simplifies, rewriting with the lemma CAR-NLISTP, and
expanding the definitions of MERGE, EQUAL, LESSP, and SORTEDP, to:
T.
Case 3.1.1.
(IMPLIES (AND (LISTP B)
(LESSP X (CAR B))
(SORTEDP (MERGE (CONS V W) B))
(SORTEDP B)
(NOT (LESSP V X))
(SORTEDP (CONS V W)))
(NOT (LESSP (CAR (MERGE (CONS V W) B))
X))),
which further simplifies, applying CAR-CONS and CDR-CONS, and expanding
SORTEDP, to the following two new formulas:
Case 3.1.1.2.
(IMPLIES (AND (LISTP B)
(LESSP X (CAR B))
(SORTEDP (MERGE (CONS V W) B))
(SORTEDP B)
(NOT (LESSP V X))
(NOT (LISTP W)))
(NOT (LESSP (CAR (MERGE (CONS V W) B))
X))).
Appealing to the lemma CAR-CDR-ELIM, we now replace B by (CONS Z D) to
eliminate (CAR B) and (CDR B). We must thus prove:
(IMPLIES (AND (LESSP X Z)
(SORTEDP (MERGE (CONS V W) (CONS Z D)))
(SORTEDP (CONS Z D))
(NOT (LESSP V X))
(NOT (LISTP W)))
(NOT (LESSP (CAR (MERGE (CONS V W) (CONS Z D)))
X))).
However this further simplifies, appealing to the lemmas CDR-CONS and
CAR-CONS, and opening up the definitions of MERGE and SORTEDP, to two
new goals:
Case 3.1.1.2.2.
(IMPLIES (AND (LESSP X Z)
(NOT (LESSP V Z))
(SORTEDP (CONS Z (MERGE (CONS V W) D)))
(NOT (LISTP D))
(NOT (LESSP V X))
(NOT (LISTP W)))
(NOT (LESSP Z X))),
which finally simplifies, using linear arithmetic, to:
T.
Case 3.1.1.2.1.
(IMPLIES (AND (LESSP X Z)
(NOT (LESSP V Z))
(SORTEDP (CONS Z (MERGE (CONS V W) D)))
(NOT (LESSP (CAR D) Z))
(SORTEDP D)
(NOT (LESSP V X))
(NOT (LISTP W)))
(NOT (LESSP Z X))),
which finally simplifies, using linear arithmetic, to:
T.
Case 3.1.1.1.
(IMPLIES (AND (LISTP B)
(LESSP X (CAR B))
(SORTEDP (MERGE (CONS V W) B))
(SORTEDP B)
(NOT (LESSP V X))
(NOT (LESSP (CAR W) V))
(SORTEDP W))
(NOT (LESSP (CAR (MERGE (CONS V W) B))
X))).
Applying the lemma CAR-CDR-ELIM, replace B by (CONS Z D) to eliminate
(CAR B) and (CDR B). We thus obtain:
(IMPLIES (AND (LESSP X Z)
(SORTEDP (MERGE (CONS V W) (CONS Z D)))
(SORTEDP (CONS Z D))
(NOT (LESSP V X))
(NOT (LESSP (CAR W) V))
(SORTEDP W))
(NOT (LESSP (CAR (MERGE (CONS V W) (CONS Z D)))
X))),
which further simplifies, applying CDR-CONS and CAR-CONS, and
unfolding MERGE and SORTEDP, to the following two new conjectures:
Case 3.1.1.1.2.
(IMPLIES (AND (LESSP X Z)
(NOT (LESSP V Z))
(SORTEDP (CONS Z (MERGE (CONS V W) D)))
(NOT (LISTP D))
(NOT (LESSP V X))
(NOT (LESSP (CAR W) V))
(SORTEDP W))
(NOT (LESSP Z X))).
But this finally simplifies, using linear arithmetic, to:
T.
Case 3.1.1.1.1.
(IMPLIES (AND (LESSP X Z)
(NOT (LESSP V Z))
(SORTEDP (CONS Z (MERGE (CONS V W) D)))
(NOT (LESSP (CAR D) Z))
(SORTEDP D)
(NOT (LESSP V X))
(NOT (LESSP (CAR W) V))
(SORTEDP W))
(NOT (LESSP Z X))),
which finally simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(NOT (SORTEDP (CDR B)))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))),
which simplifies, appealing to the lemmas CAR-CONS and CDR-CONS, and
expanding MERGE and SORTEDP, to two new formulas:
Case 2.2.
(IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(NOT (SORTEDP (CDR B)))
(SORTEDP B)
(SORTEDP U)
(LISTP (MERGE U (CDR B))))
(SORTEDP (MERGE U (CDR B)))),
which further simplifies, expanding SORTEDP and MERGE, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(NOT (SORTEDP (CDR B)))
(SORTEDP B)
(SORTEDP U)
(LISTP (MERGE U (CDR B))))
(NOT (LESSP (CAR (MERGE U (CDR B)))
(CAR B)))),
which further simplifies, expanding SORTEDP and MERGE, to:
T.
Case 1. (IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(SORTEDP (MERGE U (CDR B)))
(SORTEDP B)
(SORTEDP U))
(SORTEDP (MERGE U B))),
which simplifies, appealing to the lemmas CAR-CONS and CDR-CONS, and
unfolding the definitions of MERGE and SORTEDP, to:
(IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(SORTEDP (MERGE U (CDR B)))
(SORTEDP B)
(SORTEDP U)
(LISTP (MERGE U (CDR B))))
(NOT (LESSP (CAR (MERGE U (CDR B)))
(CAR B)))).
But this further simplifies, unfolding the definitions of SORTEDP and MERGE,
to:
(IMPLIES (AND (LISTP U)
(LISTP B)
(NOT (LESSP (CAR U) (CAR B)))
(SORTEDP (MERGE U (CDR B)))
(NOT (LESSP (CADR B) (CAR B)))
(SORTEDP (CDR B))
(SORTEDP U)
(LISTP (MERGE U (CDR B))))
(NOT (LESSP (CAR (MERGE U (CDR B)))
(CAR B)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace U by (CONS X Z) to
eliminate (CAR U) and (CDR U). We must thus prove:
(IMPLIES (AND (LISTP B)
(NOT (LESSP X (CAR B)))
(SORTEDP (MERGE (CONS X Z) (CDR B)))
(NOT (LESSP (CADR B) (CAR B)))
(SORTEDP (CDR B))
(SORTEDP (CONS X Z))
(LISTP (MERGE (CONS X Z) (CDR B))))
(NOT (LESSP (CAR (MERGE (CONS X Z) (CDR B)))
(CAR B)))).
This further simplifies, appealing to the lemmas CAR-CONS and CDR-CONS, and
expanding SORTEDP, to two new goals:
Case 1.2.
(IMPLIES (AND (LISTP B)
(NOT (LESSP X (CAR B)))
(SORTEDP (MERGE (CONS X Z) (CDR B)))
(NOT (LESSP (CADR B) (CAR B)))
(SORTEDP (CDR B))
(NOT (LISTP Z))
(LISTP (MERGE (CONS X Z) (CDR B))))
(NOT (LESSP (CAR (MERGE (CONS X Z) (CDR B)))
(CAR B)))).
Applying the lemma CAR-CDR-ELIM, replace B by (CONS V W) to eliminate
(CAR B) and (CDR B) and W by (CONS D C) to eliminate (CAR W) and (CDR W).
We thus obtain the following two new conjectures:
Case 1.2.2.
(IMPLIES (AND (NOT (LISTP W))
(NOT (LESSP X V))
(SORTEDP (MERGE (CONS X Z) W))
(NOT (LESSP (CAR W) V))
(SORTEDP W)
(NOT (LISTP Z))
(LISTP (MERGE (CONS X Z) W)))
(NOT (LESSP (CAR (MERGE (CONS X Z) W))
V))).
But this finally simplifies, rewriting with the lemmas CDR-CONS,
CAR-NLISTP, and CAR-CONS, and unfolding the functions MERGE, SORTEDP,
EQUAL, and LESSP, to:
T.
Case 1.2.1.
(IMPLIES (AND (NOT (LESSP X V))
(SORTEDP (MERGE (CONS X Z) (CONS D C)))
(NOT (LESSP D V))
(SORTEDP (CONS D C))
(NOT (LISTP Z)))
(NOT (LESSP (CAR (MERGE (CONS X Z) (CONS D C)))
V))),
which finally simplifies, applying CDR-CONS and CAR-CONS, and opening up
MERGE and SORTEDP, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP B)
(NOT (LESSP X (CAR B)))
(SORTEDP (MERGE (CONS X Z) (CDR B)))
(NOT (LESSP (CADR B) (CAR B)))
(SORTEDP (CDR B))
(NOT (LESSP (CAR Z) X))
(SORTEDP Z)
(LISTP (MERGE (CONS X Z) (CDR B))))
(NOT (LESSP (CAR (MERGE (CONS X Z) (CDR B)))
(CAR B)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace B by (CONS V W) to
eliminate (CAR B) and (CDR B) and W by (CONS D C) to eliminate (CAR W) and
(CDR W). The result is two new goals:
Case 1.1.2.
(IMPLIES (AND (NOT (LISTP W))
(NOT (LESSP X V))
(SORTEDP (MERGE (CONS X Z) W))
(NOT (LESSP (CAR W) V))
(SORTEDP W)
(NOT (LESSP (CAR Z) X))
(SORTEDP Z)
(LISTP (MERGE (CONS X Z) W)))
(NOT (LESSP (CAR (MERGE (CONS X Z) W))
V))),
which finally simplifies, rewriting with CAR-CONS, CDR-CONS, and
CAR-NLISTP, and unfolding MERGE, SORTEDP, EQUAL, and LESSP, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (LESSP X V))
(SORTEDP (MERGE (CONS X Z) (CONS D C)))
(NOT (LESSP D V))
(SORTEDP (CONS D C))
(NOT (LESSP (CAR Z) X))
(SORTEDP Z))
(NOT (LESSP (CAR (MERGE (CONS X Z) (CONS D C)))
V))).
However this finally simplifies, applying CDR-CONS and CAR-CONS, and
opening up MERGE and SORTEDP, to:
T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 0.2 0.0 ]
SORTEDP-MERGESORT
(DEFN OCCUR
(A X)
(IF (LISTP X)
(IF (EQUAL A (CAR X))
(ADD1 (OCCUR A (CDR X)))
(OCCUR A (CDR X)))
0))
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, OCCUR is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (OCCUR A X)) is a theorem.
[ 0.0 0.0 0.0 ]
OCCUR
(PROVE-LEMMA OCCUR-MERGE
(REWRITE)
(EQUAL (OCCUR A (MERGE X Y))
(PLUS (OCCUR A X) (OCCUR A Y))))
Call the conjecture *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 (NOT (LISTP X)) (p A X Y))
(IMPLIES (AND (LISTP X) (NOT (LISTP Y)))
(p A X Y))
(IMPLIES (AND (LISTP X)
(LISTP Y)
(LESSP (CAR X) (CAR Y))
(p A (CDR X) Y))
(p A X Y))
(IMPLIES (AND (LISTP X)
(LISTP Y)
(NOT (LESSP (CAR X) (CAR Y)))
(p A X (CDR Y)))
(p A X Y))).
Linear arithmetic, the lemma SUB1-ADD1, and the definitions of LESSP, PLUS,
and LENGTH inform us that the measure (PLUS (LENGTH X) (LENGTH 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 (NOT (LISTP X))
(EQUAL (OCCUR A (MERGE X Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which simplifies, opening up the functions MERGE and OCCUR, to three new
formulas:
Case 4.3.
(IMPLIES (AND (NOT (LISTP X)) (NOT (LISTP Y)))
(EQUAL 0
(PLUS (OCCUR A X) (OCCUR A Y)))),
which further simplifies, opening up OCCUR, PLUS, and EQUAL, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (LISTP X))
(LISTP Y)
(EQUAL A (CAR Y)))
(EQUAL (ADD1 (OCCUR A (CDR Y)))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which again simplifies, opening up the definitions of OCCUR, EQUAL, and
PLUS, to the goal:
(IMPLIES (AND (NOT (LISTP X)) (LISTP Y))
(EQUAL (ADD1 (OCCUR (CAR Y) (CDR Y)))
(OCCUR (CAR Y) Y))).
This again simplifies, unfolding the function OCCUR, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (LISTP X))
(LISTP Y)
(NOT (EQUAL A (CAR Y))))
(EQUAL (OCCUR A (CDR Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which further simplifies, opening up the functions OCCUR, EQUAL, and PLUS,
to:
T.
Case 3. (IMPLIES (AND (LISTP X) (NOT (LISTP Y)))
(EQUAL (OCCUR A (MERGE X Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which simplifies, opening up the definitions of MERGE and OCCUR, to two new
formulas:
Case 3.2.
(IMPLIES (AND (LISTP X)
(NOT (LISTP Y))
(NOT (EQUAL A (CAR X))))
(EQUAL (OCCUR A (CDR X))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which further simplifies, opening up the definition of OCCUR, to the
conjecture:
(IMPLIES (AND (LISTP X)
(NOT (LISTP Y))
(NOT (EQUAL A (CAR X))))
(EQUAL (OCCUR A (CDR X))
(PLUS (OCCUR A (CDR X)) 0))).
But this again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP X)
(NOT (LISTP Y))
(EQUAL A (CAR X)))
(EQUAL (ADD1 (OCCUR A (CDR X)))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which again simplifies, expanding OCCUR, to:
(IMPLIES (AND (LISTP X) (NOT (LISTP Y)))
(EQUAL (ADD1 (OCCUR (CAR X) (CDR X)))
(PLUS (OCCUR (CAR X) X) 0))).
However this again simplifies, rewriting with SUB1-ADD1 and ADD1-EQUAL,
and expanding the definitions of OCCUR and PLUS, to:
(IMPLIES (AND (LISTP X) (NOT (LISTP Y)))
(EQUAL (OCCUR (CAR X) (CDR X))
(PLUS (OCCUR (CAR X) (CDR X)) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(LISTP Y)
(LESSP (CAR X) (CAR Y))
(EQUAL (OCCUR A (MERGE (CDR X) Y))
(PLUS (OCCUR A (CDR X)) (OCCUR A Y))))
(EQUAL (OCCUR A (MERGE X Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and opening
up the definitions of MERGE and OCCUR, to two new goals:
Case 2.2.
(IMPLIES (AND (LISTP X)
(LISTP Y)
(LESSP (CAR X) (CAR Y))
(EQUAL (OCCUR A (MERGE (CDR X) Y))
(PLUS (OCCUR A (CDR X)) (OCCUR A Y)))
(NOT (EQUAL A (CAR X))))
(EQUAL (OCCUR A (MERGE (CDR X) Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which further simplifies, unfolding the definition of OCCUR, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP X)
(LISTP Y)
(LESSP (CAR X) (CAR Y))
(EQUAL (OCCUR A (MERGE (CDR X) Y))
(PLUS (OCCUR A (CDR X)) (OCCUR A Y)))
(EQUAL A (CAR X)))
(EQUAL (ADD1 (OCCUR A (MERGE (CDR X) Y)))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which again simplifies, applying the lemma SUB1-ADD1, and expanding the
definitions of OCCUR and PLUS, to:
T.
Case 1. (IMPLIES (AND (LISTP X)
(LISTP Y)
(NOT (LESSP (CAR X) (CAR Y)))
(EQUAL (OCCUR A (MERGE X (CDR Y)))
(PLUS (OCCUR A X) (OCCUR A (CDR Y)))))
(EQUAL (OCCUR A (MERGE X Y))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
definitions of MERGE and OCCUR, to the following two new goals:
Case 1.2.
(IMPLIES (AND (LISTP X)
(LISTP Y)
(NOT (LESSP (CAR X) (CAR Y)))
(EQUAL (OCCUR A (MERGE X (CDR Y)))
(PLUS (OCCUR A X) (OCCUR A (CDR Y))))
(NOT (EQUAL A (CAR Y))))
(EQUAL (OCCUR A (MERGE X (CDR Y)))
(PLUS (OCCUR A X) (OCCUR A Y)))).
But this further simplifies, opening up the definition of OCCUR, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP X)
(LISTP Y)
(NOT (LESSP (CAR X) (CAR Y)))
(EQUAL (OCCUR A (MERGE X (CDR Y)))
(PLUS (OCCUR A X) (OCCUR A (CDR Y))))
(EQUAL A (CAR Y)))
(EQUAL (ADD1 (OCCUR A (MERGE X (CDR Y))))
(PLUS (OCCUR A X) (OCCUR A Y)))),
which again simplifies, expanding OCCUR, to:
(IMPLIES (AND (LISTP X)
(LISTP Y)
(NOT (LESSP (CAR X) (CAR Y)))
(EQUAL (OCCUR (CAR Y) (MERGE X (CDR Y)))
(PLUS (OCCUR (CAR Y) X)
(OCCUR (CAR Y) (CDR Y)))))
(EQUAL (ADD1 (OCCUR (CAR Y) (MERGE X (CDR Y))))
(PLUS (OCCUR (CAR Y) X)
(ADD1 (OCCUR (CAR Y) (CDR Y)))))).
However this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
OCCUR-MERGE
(PROVE-LEMMA PLUS-OCCUR-ODDS
(REWRITE)
(IMPLIES (AND (LISTP X) (LISTP (CDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A X))))
This conjecture simplifies, expanding OCCUR, to the following two new
conjectures:
Case 2. (IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X))))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A (CDR X)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to
eliminate (CDR X) and (CAR X). We must thus prove:
(IMPLIES (AND (LISTP Z) (NOT (EQUAL A V)))
(EQUAL (PLUS (OCCUR A (ODDS Z))
(OCCUR A (ODDS (CONS V Z))))
(OCCUR A 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 (AND (LISTP X) (LISTP (CDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A X))),
which we named *1 above. We will appeal to induction. Two inductions are
suggested by terms in the conjecture, both of which are unflawed. Since both
of these are equally likely, we will choose arbitrarily. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP X)) (p A X))
(IMPLIES (AND (LISTP X) (p A (CDDR X)))
(p A X))).
Linear arithmetic and the lemmas CDR-LESSEQP and CDR-LESSP 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 produces the
following three new conjectures:
Case 3. (IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A X))).
This simplifies, applying the lemmas CDR-NLISTP, CDR-CONS, and CAR-CONS, and
expanding the definitions of ODDS, OCCUR, LISTP, and ADD1, to the following
four new goals:
Case 3.4.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X)))
(EQUAL (PLUS 1 (OCCUR A (ODDS (CDDR X))))
1)).
This again simplifies, clearly, to the new formula:
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X))))
(EQUAL (PLUS 1
(OCCUR (CADR X) (ODDS (CDDR X))))
1)),
which further simplifies, opening up the functions ODDS, LISTP, OCCUR,
PLUS, and EQUAL, to:
T.
Case 3.3.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS 0 (OCCUR A (ODDS (CDDR X))))
0)),
which again simplifies, expanding the definitions of EQUAL and PLUS, to:
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X))))
(EQUAL (OCCUR A (ODDS (CDDR X))) 0)).
However this further simplifies, unfolding ODDS, LISTP, OCCUR, and EQUAL,
to:
T.
Case 3.2.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR A (ODDS (CDDR X)))))
2)),
which again simplifies, obviously, to the new conjecture:
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR (CAR X) (ODDS (CDDR X)))))
2)),
which further simplifies, expanding the functions ODDS, LISTP, OCCUR, ADD1,
PLUS, and EQUAL, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS 0
(ADD1 (OCCUR A (ODDS (CDDR X)))))
1)),
which again simplifies, rewriting with ADD1-EQUAL, and unfolding the
functions EQUAL, PLUS, and NUMBERP, to:
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X))))
(EQUAL (OCCUR (CAR X) (ODDS (CDDR X)))
0)),
which further simplifies, opening up the functions ODDS, LISTP, OCCUR, and
EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A X))),
which simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
opening up ODDS, OCCUR, LISTP, and ADD1, to 12 new formulas:
Case 2.12.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X))
(NOT (EQUAL A (CADDR X))))
(EQUAL (PLUS 1 (OCCUR A (ODDS (CDDR X))))
1)),
which again simplifies, obviously, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X)))
(NOT (EQUAL (CADR X) (CADDR X))))
(EQUAL (PLUS 1
(OCCUR (CADR X) (ODDS (CDDR X))))
1)),
which further simplifies, appealing to the lemma CDR-NLISTP, and unfolding
ODDS, to two new conjectures:
Case 2.12.2.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X)))
(NOT (EQUAL (CADR X) (CADDR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1 (OCCUR (CADR X) NIL))
1)),
which again simplifies, applying the lemmas CDR-NLISTP and CAR-NLISTP,
and unfolding the definitions of LISTP, OCCUR, PLUS, and EQUAL, to:
T.
Case 2.12.1.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X)))
(NOT (EQUAL (CADR X) (CADDR X)))
(LISTP (CDDR X)))
(EQUAL (PLUS 1
(OCCUR (CADR X) (LIST (CADDR X))))
1)),
which again simplifies, rewriting with CDR-CONS and CAR-CONS, and
opening up OCCUR, LISTP, PLUS, and EQUAL, to:
T.
Case 2.11.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1 (OCCUR A (ODDS (CDDR X))))
1)).
But this again simplifies, applying the lemma CDR-NLISTP, and unfolding
the definition of LISTP, to:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1
(OCCUR (CADR X) (ODDS (CDDR X))))
1)).
This further simplifies, unfolding the functions ODDS, LISTP, OCCUR, PLUS,
and EQUAL, to:
T.
Case 2.10.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X))
(LISTP (CDDR X))
(EQUAL A (CADDR X)))
(EQUAL (PLUS 1 (OCCUR A (ODDS (CDDR X))))
2)),
which again simplifies, trivially, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADR X) (CAR X)))
(LISTP (CDDR X))
(EQUAL (CADR X) (CADDR X)))
(EQUAL (PLUS 1
(OCCUR (CADR X) (ODDS (CDDR X))))
2)),
which further simplifies, applying CDR-NLISTP, CDR-CONS, and CAR-CONS, and
unfolding ODDS, OCCUR, LISTP, ADD1, PLUS, and EQUAL, to:
T.
Case 2.9.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (EQUAL A (CADDR X))))
(EQUAL (PLUS 0 (OCCUR A (ODDS (CDDR X))))
0)).
However this again simplifies, opening up the functions EQUAL and PLUS, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (EQUAL A (CADDR X))))
(EQUAL (OCCUR A (ODDS (CDDR X))) 0)).
But this further simplifies, rewriting with CDR-NLISTP, and unfolding ODDS,
to the following two new formulas:
Case 2.9.2.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (EQUAL A (CADDR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (OCCUR A NIL) 0)).
This again simplifies, appealing to the lemmas CDR-NLISTP and CAR-NLISTP,
and opening up the functions LISTP, OCCUR, and EQUAL, to:
T.
Case 2.9.1.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (EQUAL A (CADDR X)))
(LISTP (CDDR X)))
(EQUAL (OCCUR A (LIST (CADDR X))) 0)),
which again simplifies, rewriting with CDR-CONS and CAR-CONS, and
opening up the definitions of OCCUR, LISTP, and EQUAL, to:
T.
Case 2.8.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 0 (OCCUR A (ODDS (CDDR X))))
0)).
However this again simplifies, rewriting with CDR-NLISTP, and expanding
the functions LISTP, EQUAL, and PLUS, to the new formula:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (OCCUR A (ODDS (CDDR X))) 0)),
which further simplifies, unfolding ODDS, LISTP, OCCUR, and EQUAL, to:
T.
Case 2.7.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X)))
(LISTP (CDDR X))
(EQUAL A (CADDR X)))
(EQUAL (PLUS 0 (OCCUR A (ODDS (CDDR X))))
1)),
which again simplifies, expanding EQUAL and PLUS, to the formula:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CADDR X) (CAR X)))
(NOT (EQUAL (CADDR X) (CADR X)))
(LISTP (CDDR X)))
(EQUAL (OCCUR (CADDR X) (ODDS (CDDR X)))
1)).
But this further simplifies, applying the lemmas CDR-NLISTP, CDR-CONS, and
CAR-CONS, and opening up the definitions of ODDS, OCCUR, LISTP, ADD1, and
EQUAL, to:
T.
Case 2.6.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X))
(NOT (EQUAL A (CADDR X))))
(EQUAL (PLUS 1
(ADD1 (OCCUR A (ODDS (CDDR X)))))
2)),
which again simplifies, clearly, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X))
(NOT (EQUAL (CAR X) (CADDR X))))
(EQUAL (PLUS 1
(ADD1 (OCCUR (CAR X) (ODDS (CDDR X)))))
2)),
which further simplifies, rewriting with CDR-NLISTP, and unfolding the
function ODDS, to the following two new goals:
Case 2.6.2.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X))
(NOT (EQUAL (CAR X) (CADDR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1 (ADD1 (OCCUR (CAR X) NIL)))
2)).
This again simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
expanding the definitions of LISTP, OCCUR, ADD1, PLUS, and EQUAL, to:
T.
Case 2.6.1.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X))
(NOT (EQUAL (CAR X) (CADDR X)))
(LISTP (CDDR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR (CAR X) (LIST (CADDR X)))))
2)).
However this again simplifies, appealing to the lemmas CDR-CONS and
CAR-CONS, and unfolding the definitions of OCCUR, LISTP, ADD1, PLUS, and
EQUAL, to:
T.
Case 2.5.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1
(ADD1 (OCCUR A (ODDS (CDDR X)))))
2)),
which again simplifies, rewriting with CDR-NLISTP, and unfolding the
function LISTP, to the new conjecture:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 1
(ADD1 (OCCUR (CAR X) (ODDS (CDDR X)))))
2)),
which further simplifies, expanding the definitions of ODDS, LISTP, OCCUR,
ADD1, PLUS, and EQUAL, to:
T.
Case 2.4.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X))
(LISTP (CDDR X))
(EQUAL A (CADDR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR A (ODDS (CDDR X)))))
3)),
which again simplifies, obviously, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL (CAR X) (CADR X))
(LISTP (CDDR X))
(EQUAL (CAR X) (CADDR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR (CAR X) (ODDS (CDDR X)))))
3)),
which further simplifies, applying CDR-NLISTP, CDR-CONS, and CAR-CONS, and
opening up the functions ODDS, OCCUR, LISTP, ADD1, PLUS, and EQUAL, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X)))
(NOT (EQUAL A (CADDR X))))
(EQUAL (PLUS 0
(ADD1 (OCCUR A (ODDS (CDDR X)))))
1)).
But this again simplifies, appealing to the lemma ADD1-EQUAL, and
expanding the definitions of EQUAL, PLUS, and NUMBERP, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X)))
(NOT (EQUAL (CAR X) (CADDR X))))
(EQUAL (OCCUR (CAR X) (ODDS (CDDR X)))
0)).
This further simplifies, applying CDR-NLISTP, and expanding the definition
of ODDS, to the following two new goals:
Case 2.3.2.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X)))
(NOT (EQUAL (CAR X) (CADDR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (OCCUR (CAR X) NIL) 0)).
This again simplifies, applying CDR-NLISTP and CAR-NLISTP, and unfolding
the definitions of LISTP, OCCUR, and EQUAL, to:
T.
Case 2.3.1.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X)))
(NOT (EQUAL (CAR X) (CADDR X)))
(LISTP (CDDR X)))
(EQUAL (OCCUR (CAR X) (LIST (CADDR X)))
0)).
But this again simplifies, rewriting with the lemmas CDR-CONS and
CAR-CONS, and unfolding OCCUR, LISTP, and EQUAL, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (PLUS 0
(ADD1 (OCCUR A (ODDS (CDDR X)))))
1)),
which again simplifies, applying CDR-NLISTP and ADD1-EQUAL, and unfolding
the definitions of LISTP, EQUAL, PLUS, and NUMBERP, to:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X)))
(NOT (LISTP (CDDR X))))
(EQUAL (OCCUR (CAR X) (ODDS (CDDR X)))
0)),
which further simplifies, unfolding the definitions of ODDS, LISTP, OCCUR,
and EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X)))
(LISTP (CDDR X))
(EQUAL A (CADDR X)))
(EQUAL (PLUS 0
(ADD1 (OCCUR A (ODDS (CDDR X)))))
2)),
which again simplifies, rewriting with ADD1-EQUAL, and opening up the
definitions of EQUAL, PLUS, and NUMBERP, to:
(IMPLIES (AND (NOT (LISTP (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL (CAR X) (CADR X)))
(LISTP (CDDR X))
(EQUAL (CAR X) (CADDR X)))
(EQUAL (OCCUR (CAR X) (ODDS (CDDR X)))
1)),
which further simplifies, appealing to the lemmas CDR-NLISTP, CDR-CONS,
and CAR-CONS, and expanding ODDS, OCCUR, LISTP, ADD1, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(OCCUR A (CDDR X)))
(LISTP X)
(LISTP (CDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDR X)))
(OCCUR A (ODDS X)))
(OCCUR A X))),
which simplifies, applying CDR-NLISTP, CDR-CONS, and CAR-CONS, and opening
up the definitions of OCCUR, ODDS, LISTP, and ADD1, to the following ten new
goals:
Case 1.10.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
0)
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X)))
(EQUAL (PLUS 1 (OCCUR A (ODDS (CDDR X))))
1)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.9.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
0)
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS 0 (OCCUR A (ODDS (CDDR X))))
0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.8.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
0)
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X)))
(EQUAL (PLUS 1
(ADD1 (OCCUR A (ODDS (CDDR X)))))
2)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.7.
(IMPLIES (AND (NOT (LISTP (CDDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
0)
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS 0
(ADD1 (OCCUR A (ODDS (CDDR X)))))
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.6.
(IMPLIES (AND (LISTP (CDDR X))
(EQUAL A (CADDR X))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(ADD1 (OCCUR A (CDDDR X))))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X)))
(EQUAL (PLUS (ADD1 (OCCUR A (ODDS (CDDDR X))))
(OCCUR A (ODDS (CDDR X))))
(ADD1 (ADD1 (OCCUR A (CDDDR X)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.5.
(IMPLIES (AND (LISTP (CDDR X))
(EQUAL A (CADDR X))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(ADD1 (OCCUR A (CDDDR X))))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X)))
(EQUAL (PLUS (ADD1 (OCCUR A (ODDS (CDDDR X))))
(ADD1 (OCCUR A (ODDS (CDDR X)))))
(ADD1 (ADD1 (ADD1 (OCCUR A (CDDDR X))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (LISTP (CDDR X))
(EQUAL A (CADDR X))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(ADD1 (OCCUR A (CDDDR X))))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(ADD1 (OCCUR A (ODDS (CDDR X)))))
(ADD1 (ADD1 (OCCUR A (CDDDR X)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (LISTP (CDDR X))
(NOT (EQUAL A (CADDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(OCCUR A (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(NOT (EQUAL A (CAR X)))
(EQUAL A (CADR X)))
(EQUAL (PLUS (ADD1 (OCCUR A (ODDS (CDDDR X))))
(OCCUR A (ODDS (CDDR X))))
(ADD1 (OCCUR A (CDDDR X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP (CDDR X))
(NOT (EQUAL A (CADDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(OCCUR A (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(EQUAL A (CADR X)))
(EQUAL (PLUS (ADD1 (OCCUR A (ODDS (CDDDR X))))
(ADD1 (OCCUR A (ODDS (CDDR X)))))
(ADD1 (ADD1 (OCCUR A (CDDDR X)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP (CDDR X))
(NOT (EQUAL A (CADDR X)))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(OCCUR A (ODDS (CDDR X))))
(OCCUR A (CDDDR X)))
(LISTP X)
(LISTP (CDR X))
(EQUAL A (CAR X))
(NOT (EQUAL A (CADR X))))
(EQUAL (PLUS (OCCUR A (ODDS (CDDDR X)))
(ADD1 (OCCUR A (ODDS (CDDR X)))))
(ADD1 (OCCUR A (CDDDR X))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.1 ]
PLUS-OCCUR-ODDS
(PROVE-LEMMA OCCUR-MERGESORT
(REWRITE)
(EQUAL (OCCUR A (MERGESORT X))
(OCCUR A X)))
Name the conjecture *1.
Perhaps we can prove it by induction. There are two plausible inductions,
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 (NOT (LISTP X)) (p A X))
(IMPLIES (AND (LISTP X) (NOT (LISTP (CDR X))))
(p A X))
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(p A (ODDS X))
(p A (ODDS (CDR X))))
(p A X))).
The lemmas SUB1-ADD1 and MERGESORT-HELPER and the definitions of LESSP and
LENGTH establish that the measure (LENGTH X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following three new goals:
Case 3. (IMPLIES (NOT (LISTP X))
(EQUAL (OCCUR A (MERGESORT X))
(OCCUR A X))).
This simplifies, expanding MERGESORT, LISTP, OCCUR, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (LISTP X) (NOT (LISTP (CDR X))))
(EQUAL (OCCUR A (MERGESORT X))
(OCCUR A X))).
This simplifies, unfolding MERGESORT, OCCUR, and ADD1, to:
T.
Case 1. (IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(EQUAL (OCCUR A (MERGESORT (ODDS X)))
(OCCUR A (ODDS X)))
(EQUAL (OCCUR A (MERGESORT (ODDS (CDR X))))
(OCCUR A (ODDS (CDR X)))))
(EQUAL (OCCUR A (MERGESORT X))
(OCCUR A X))).
This simplifies, rewriting with the lemmas PLUS-OCCUR-ODDS and OCCUR-MERGE,
and expanding the definitions of MERGESORT and OCCUR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
OCCUR-MERGESORT
(DEFN REMOVE1
(A X)
(IF (LISTP X)
(IF (EQUAL (CAR X) A)
(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
(DEFN BADGUY
(X Y)
(IF (LISTP X)
(IF (MEMBER (CAR X) Y)
(BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CAR X))
0))
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, BADGUY is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
BADGUY
(DEFN SUBBAGP
(X Y)
(IF (LISTP X)
(AND (MEMBER (CAR X) Y)
(SUBBAGP (CDR X) (REMOVE1 (CAR X) Y)))
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 definitional principle.
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
(PROVE-LEMMA MEMBER-OCCUR
(REWRITE)
(EQUAL (MEMBER A X)
(LESSP 0 (OCCUR A X))))
This formula simplifies, expanding the functions EQUAL and LESSP, to two new
conjectures:
Case 2. (IMPLIES (NOT (EQUAL (OCCUR A X) 0))
(EQUAL (MEMBER A X) T)),
which again simplifies, trivially, to the new formula:
(IMPLIES (NOT (EQUAL (OCCUR A X) 0))
(MEMBER A X)),
which we will name *1.
Case 1. (IMPLIES (EQUAL (OCCUR A X) 0)
(EQUAL (MEMBER A X) F)).
This again simplifies, obviously, to:
(IMPLIES (EQUAL (OCCUR A X) 0)
(NOT (MEMBER A 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:
(EQUAL (MEMBER A X)
(LESSP 0 (OCCUR A X))).
We named this *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 (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 prove that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme produces the following three new goals:
Case 3. (IMPLIES (NLISTP X)
(EQUAL (MEMBER A X)
(LESSP 0 (OCCUR A X)))).
This simplifies, expanding the definitions of NLISTP, MEMBER, OCCUR, LESSP,
and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(EQUAL A (CAR X)))
(EQUAL (MEMBER A X)
(LESSP 0 (OCCUR A X)))).
This simplifies, expanding NLISTP, MEMBER, EQUAL, and LESSP, to:
(IMPLIES (LISTP X)
(NOT (EQUAL (OCCUR (CAR X) X) 0))).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate
(CAR X) and (CDR X). This produces the new conjecture:
(NOT (EQUAL (OCCUR Z (CONS Z V)) 0)),
which further simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
up OCCUR, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL A (CAR X)))
(EQUAL (MEMBER A (CDR X))
(LESSP 0 (OCCUR A (CDR X)))))
(EQUAL (MEMBER A X)
(LESSP 0 (OCCUR A X)))).
This simplifies, expanding the functions NLISTP, EQUAL, LESSP, MEMBER, and
OCCUR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MEMBER-OCCUR
(PROVE-LEMMA OCCUR-REMOVE1
(REWRITE)
(EQUAL (OCCUR A (REMOVE1 B X))
(IF (EQUAL A B)
(SUB1 (OCCUR A X))
(OCCUR A X))))
This simplifies, trivially, to the following two new goals:
Case 2. (IMPLIES (NOT (EQUAL A B))
(EQUAL (OCCUR A (REMOVE1 B X))
(OCCUR A X))).
Give the above formula the name *1.
Case 1. (IMPLIES (EQUAL A B)
(EQUAL (OCCUR A (REMOVE1 B X))
(SUB1 (OCCUR A X)))).
This again simplifies, trivially, to:
(EQUAL (OCCUR B (REMOVE1 B X))
(SUB1 (OCCUR B 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:
(EQUAL (OCCUR A (REMOVE1 B X))
(IF (EQUAL A B)
(SUB1 (OCCUR A X))
(OCCUR A X))).
We named this *1. We will try to 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 (AND (LISTP X) (EQUAL (CAR X) B))
(p A B X))
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(p A B (CDR X)))
(p A B X))
(IMPLIES (NOT (LISTP X)) (p A B X))).
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. The above induction scheme leads to three new formulas:
Case 3. (IMPLIES (AND (LISTP X) (EQUAL (CAR X) B))
(EQUAL (OCCUR A (REMOVE1 B X))
(IF (EQUAL A B)
(SUB1 (OCCUR A X))
(OCCUR A X)))),
which simplifies, applying SUB1-ADD1, and unfolding REMOVE1 and OCCUR, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(EQUAL (OCCUR A (REMOVE1 B (CDR X)))
(IF (EQUAL A B)
(SUB1 (OCCUR A (CDR X)))
(OCCUR A (CDR X)))))
(EQUAL (OCCUR A (REMOVE1 B X))
(IF (EQUAL A B)
(SUB1 (OCCUR A X))
(OCCUR A X)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up
REMOVE1 and OCCUR, to four new conjectures:
Case 2.4.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(EQUAL A B)
(EQUAL (OCCUR A (REMOVE1 B (CDR X)))
(SUB1 (OCCUR A (CDR X))))
(NOT (EQUAL A (CAR X)))
(NOT (EQUAL (CAR X) A)))
(EQUAL (OCCUR A
(CONS (CAR X) (REMOVE1 A (CDR X))))
(SUB1 (OCCUR A (CDR X))))),
which again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
and expanding the definition of OCCUR, to:
T.
Case 2.3.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(EQUAL A B)
(EQUAL (OCCUR A (REMOVE1 B (CDR X)))
(SUB1 (OCCUR A (CDR X))))
(NOT (EQUAL A (CAR X)))
(EQUAL (CAR X) A))
(EQUAL (OCCUR A (CDR X))
(SUB1 (OCCUR A (CDR X))))),
which again simplifies, clearly, to:
T.
Case 2.2.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(EQUAL A B)
(EQUAL (OCCUR A (REMOVE1 B (CDR X)))
(SUB1 (OCCUR A (CDR X))))
(EQUAL A (CAR X))
(NOT (EQUAL (CAR X) A)))
(EQUAL (OCCUR A
(CONS (CAR X) (REMOVE1 A (CDR X))))
(SUB1 (ADD1 (OCCUR A (CDR X)))))).
This again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (CAR X) B))
(EQUAL A B)
(EQUAL (OCCUR A (REMOVE1 B (CDR X)))
(SUB1 (OCCUR A (CDR X))))
(EQUAL A (CAR X))
(EQUAL (CAR X) A))
(EQUAL (OCCUR A (CDR X))
(SUB1 (ADD1 (OCCUR A (CDR X)))))).
This again simplifies, clearly, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (OCCUR A (REMOVE1 B X))
(IF (EQUAL A B)
(SUB1 (OCCUR A X))
(OCCUR A X)))).
This simplifies, unfolding the definitions of REMOVE1, OCCUR, SUB1, and
EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
OCCUR-REMOVE1
(PROVE-LEMMA SUBBAGP-WIT-LEMMA
(REWRITE)
(EQUAL (SUBBAGP X Y)
(NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X)))))
This formula simplifies, opening up NOT, to the following two new formulas:
Case 2. (IMPLIES (NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X)))
(EQUAL (SUBBAGP X Y) T)).
This again simplifies, trivially, to the new formula:
(IMPLIES (NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X)))
(SUBBAGP X Y)),
which we will name *1.
Case 1. (IMPLIES (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X))
(EQUAL (SUBBAGP X Y) F)).
This again simplifies, clearly, to:
(IMPLIES (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X))
(NOT (SUBBAGP 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 (SUBBAGP X Y)
(NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X)))).
We named this *1. We will try to prove it by induction. There are five
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)
(MEMBER (CAR X) Y)
(p (CDR X) (REMOVE1 (CAR X) Y)))
(p X Y))
(IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y)))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p X Y))).
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. Note, however, the inductive instance chosen
for Y. The above induction scheme generates the following three new
conjectures:
Case 3. (IMPLIES
(AND (LISTP X)
(MEMBER (CAR X) Y)
(EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
(NOT (LESSP (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(REMOVE1 (CAR X) Y))
(OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CDR X))))))
(EQUAL (SUBBAGP X Y)
(NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X))))).
This simplifies, applying MEMBER-OCCUR, OCCUR-REMOVE1, and SUB1-ADD1, and
expanding the definitions of EQUAL, LESSP, NOT, SUBBAGP, BADGUY, and OCCUR,
to two new conjectures:
Case 3.2.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (OCCUR (CAR X) Y) 0))
(EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CAR X))
(NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CDR X))))
(EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
T))
(NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (CAR X) (CDR X))))),
which again simplifies, obviously, to:
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (OCCUR (CAR X) Y) 0))
(EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CAR X))
(NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CDR X))))
(SUBBAGP (CDR X) (REMOVE1 (CAR X) Y)))
(NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (CAR X) (CDR X))))),
which further simplifies, clearly, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (OCCUR (CAR X) Y) 0))
(EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CAR X))
(LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CDR X)))
(EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
F))
(LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (CAR X) (CDR X)))).
This again simplifies, obviously, to:
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (OCCUR (CAR X) Y) 0))
(EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CAR X))
(LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
(CDR X)))
(NOT (SUBBAGP (CDR X)
(REMOVE1 (CAR X) Y))))
(LESSP (SUB1 (OCCUR (CAR X) Y))
(OCCUR (CAR X) (CDR X)))),
which further simplifies, obviously, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (MEMBER (CAR X) Y)))
(EQUAL (SUBBAGP X Y)
(NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X))))).
This simplifies, applying the lemma MEMBER-OCCUR, and opening up EQUAL,
LESSP, SUBBAGP, BADGUY, and NOT, to:
(IMPLIES (AND (LISTP X)
(EQUAL (OCCUR (CAR X) Y) 0))
(NOT (EQUAL (OCCUR (CAR X) X) 0))).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate
(CAR X) and (CDR X). This produces the new formula:
(IMPLIES (EQUAL (OCCUR Z Y) 0)
(NOT (EQUAL (OCCUR Z (CONS Z V)) 0))),
which further simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
unfolding the function OCCUR, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (SUBBAGP X Y)
(NOT (LESSP (OCCUR (BADGUY X Y) Y)
(OCCUR (BADGUY X Y) X))))),
which simplifies, opening up the definitions of SUBBAGP, BADGUY, OCCUR,
EQUAL, LESSP, and NOT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
SUBBAGP-WIT-LEMMA
(DEFN PERMUTATIONP
(X Y)
(AND (SUBBAGP X Y) (SUBBAGP Y X)))
Observe that (OR (FALSEP (PERMUTATIONP X Y)) (TRUEP (PERMUTATIONP X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
PERMUTATIONP
(PROVE-LEMMA PERMUTATIONP-MERGESORT
(REWRITE)
(PERMUTATIONP (MERGESORT X) X))
WARNING: Note that the rewrite rule PERMUTATIONP-MERGESORT will be stored so
as to apply only to terms with the nonrecursive function symbol PERMUTATIONP.
This formula can be simplified, using the abbreviations NOT, OCCUR-MERGESORT,
SUBBAGP-WIT-LEMMA, and PERMUTATIONP, to the following two new conjectures:
Case 2. (NOT (LESSP (OCCUR (BADGUY (MERGESORT X) X) X)
(OCCUR (BADGUY (MERGESORT X) X) X))).
This simplifies, using linear arithmetic, to:
T.
Case 1. (NOT (LESSP (OCCUR (BADGUY X (MERGESORT X)) X)
(OCCUR (BADGUY X (MERGESORT X)) X))).
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PERMUTATIONP-MERGESORT