(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