(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(SETQ REDUCE-TERM-CLOCK 2000)

2000


(DEFN DELETE
      (X L)
      (IF (LISTP L)
          (IF (EQUAL X (CAR L))
              (CDR L)
              (CONS (CAR L) (DELETE X (CDR L))))
          L))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, DELETE is accepted under the principle of definition.




[ 0.0 0.0 0.0 ]

DELETE


(DEFN BAGDIFF
      (X Y)
      (IF (LISTP Y)
          (IF (MEMBER (CAR Y) X)
              (BAGDIFF (DELETE (CAR Y) X) (CDR Y))
              (BAGDIFF X (CDR Y)))
          X))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, BAGDIFF is accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

BAGDIFF


(DEFN BAGINT
      (X Y)
      (IF (LISTP X)
          (IF (MEMBER (CAR X) Y)
              (CONS (CAR X)
                    (BAGINT (CDR X) (DELETE (CAR X) Y)))
              (BAGINT (CDR X) Y))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, BAGINT is accepted under the principle of definition.
Note that (OR (LITATOM (BAGINT X Y)) (LISTP (BAGINT X Y))) is a theorem.




[ 0.0 0.0 0.0 ]

BAGINT


(DEFN OCCURRENCES
      (X L)
      (IF (LISTP L)
          (IF (EQUAL X (CAR L))
              (ADD1 (OCCURRENCES X (CDR L)))
              (OCCURRENCES X (CDR L)))
          0))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, OCCURRENCES is accepted under the principle of
definition.  From the definition we can conclude that:
      (NUMBERP (OCCURRENCES X L))
is a theorem.




[ 0.0 0.0 0.0 ]

OCCURRENCES


(DEFN SUBBAGP
      (X Y)
      (IF (LISTP X)
          (IF (MEMBER (CAR X) Y)
              (SUBBAGP (CDR X) (DELETE (CAR X) Y))
              F)
          T))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, SUBBAGP is accepted under the principle of definition.
From the definition we can conclude that:
      (OR (FALSEP (SUBBAGP X Y))
          (TRUEP (SUBBAGP X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

SUBBAGP


(PROVE-LEMMA LISTP-DELETE
             (REWRITE)
             (EQUAL (LISTP (DELETE X L))
                    (IF (LISTP L)
                        (OR (NOT (EQUAL X (CAR L)))
                            (LISTP (CDR L)))
                        F))
             ((ENABLE DELETE)
              (INDUCT (DELETE X L))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This conjecture can be simplified, using the abbreviations NOT, OR, and AND,
to three new conjectures:

Case 3. (IMPLIES (AND (LISTP L) (EQUAL X (CAR L)))
                 (EQUAL (LISTP (DELETE X L))
                        (IF (LISTP L)
                            (OR (NOT (EQUAL X (CAR L)))
                                (LISTP (CDR L)))
                            F))),

  which simplifies, opening up the definitions of DELETE, NOT, and OR, to:

        T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL X (CAR L)))
                      (EQUAL (LISTP (DELETE X (CDR L)))
                             (IF (LISTP (CDR L))
                                 (OR (NOT (EQUAL X (CADR L)))
                                     (LISTP (CDDR L)))
                                 F)))
                 (EQUAL (LISTP (DELETE X L))
                        (IF (LISTP L)
                            (OR (NOT (EQUAL X (CAR L)))
                                (LISTP (CDR L)))
                            F))),

  which simplifies, applying CONS-CAR-CDR, and unfolding DELETE, NOT, OR, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (NOT (LISTP L))
                 (EQUAL (LISTP (DELETE X L))
                        (IF (LISTP L)
                            (OR (NOT (EQUAL X (CAR L)))
                                (LISTP (CDR L)))
                            F))).

  This simplifies, opening up DELETE and EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LISTP-DELETE


(TOGGLE LISTP-DELETE-OFF LISTP-DELETE T)

[ 0.0 0.0 0.0 ]

LISTP-DELETE-OFF


(PROVE-LEMMA DELETE-NON-MEMBER
             (REWRITE)
             (IMPLIES (NOT (MEMBER X Y))
                      (EQUAL (DELETE X Y) Y))
             ((ENABLE DELETE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Give the conjecture the name *1.


     We will try to prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (NLISTP Y) (p X Y))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (EQUAL X (CAR Y)))
                    (p X Y))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (NOT (EQUAL X (CAR Y)))
                         (p X (CDR Y)))
                    (p X Y))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates four new goals:

Case 4. (IMPLIES (AND (NLISTP Y) (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, expanding NLISTP, MEMBER, and DELETE, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP Y))
                      (EQUAL X (CAR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, opening up the functions NLISTP and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (MEMBER X (CDR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, opening up the definitions of NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (EQUAL (DELETE X (CDR Y)) (CDR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, rewriting with the lemma CONS-CAR-CDR, and unfolding the
  functions NLISTP, MEMBER, and DELETE, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DELETE-NON-MEMBER


(PROVE-LEMMA DELETE-DELETE
             (REWRITE)
             (EQUAL (DELETE Y (DELETE X Z))
                    (DELETE X (DELETE Y Z)))
             ((ENABLE DELETE DELETE-NON-MEMBER)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Two inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP Z) (EQUAL X (CAR Z)))
                    (p Y X Z))
           (IMPLIES (AND (LISTP Z)
                         (NOT (EQUAL X (CAR Z)))
                         (p Y X (CDR Z)))
                    (p Y X Z))
           (IMPLIES (NOT (LISTP Z)) (p Y X Z))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT Z) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme leads to three
new goals:

Case 3. (IMPLIES (AND (LISTP Z) (EQUAL X (CAR Z)))
                 (EQUAL (DELETE Y (DELETE X Z))
                        (DELETE X (DELETE Y Z)))),

  which simplifies, opening up the definition of DELETE, to two new
  conjectures:

  Case 3.2.
          (IMPLIES (AND (LISTP Z)
                        (NOT (EQUAL Y (CAR Z))))
                   (EQUAL (DELETE Y (CDR Z))
                          (DELETE (CAR Z)
                                  (CONS (CAR Z) (DELETE Y (CDR Z)))))),

    which again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
    up the function DELETE, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP Z) (EQUAL Y (CAR Z)))
                   (EQUAL (DELETE Y (CDR Z))
                          (DELETE (CAR Z) (CDR Z)))).

    This again simplifies, obviously, to:

          T.

Case 2. (IMPLIES (AND (LISTP Z)
                      (NOT (EQUAL X (CAR Z)))
                      (EQUAL (DELETE Y (DELETE X (CDR Z)))
                             (DELETE X (DELETE Y (CDR Z)))))
                 (EQUAL (DELETE Y (DELETE X Z))
                        (DELETE X (DELETE Y Z)))).

  This simplifies, applying CDR-CONS and CAR-CONS, and opening up DELETE, to:

        (IMPLIES (AND (LISTP Z)
                      (NOT (EQUAL X (CAR Z)))
                      (EQUAL (DELETE Y (DELETE X (CDR Z)))
                             (DELETE X (DELETE Y (CDR Z))))
                      (NOT (EQUAL Y (CAR Z))))
                 (EQUAL (CONS (CAR Z)
                              (DELETE X (DELETE Y (CDR Z))))
                        (DELETE X
                                (CONS (CAR Z) (DELETE Y (CDR Z)))))).

  But this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
  and expanding the definition of DELETE, to:

        T.

Case 1. (IMPLIES (NOT (LISTP Z))
                 (EQUAL (DELETE Y (DELETE X Z))
                        (DELETE X (DELETE Y Z)))),

  which simplifies, applying DELETE-NON-MEMBER, and expanding the definition
  of MEMBER, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DELETE-DELETE


(PROVE-LEMMA EQUAL-OCCURRENCES-ZERO
             (REWRITE)
             (EQUAL (EQUAL (OCCURRENCES X L) 0)
                    (NOT (MEMBER X L)))
             ((ENABLE OCCURRENCES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This conjecture simplifies, unfolding NOT, to two new conjectures:

Case 2. (IMPLIES (NOT (EQUAL (OCCURRENCES X L) 0))
                 (MEMBER X L)),

  which we will name *1.

Case 1. (IMPLIES (EQUAL (OCCURRENCES X L) 0)
                 (NOT (MEMBER X L))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (EQUAL (OCCURRENCES X L) 0)
       (NOT (MEMBER X L))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  Two
inductions are suggested by terms in the conjecture.  However, they merge into
one likely candidate induction.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP L)
                         (EQUAL X (CAR L))
                         (p X (CDR L)))
                    (p X L))
           (IMPLIES (AND (LISTP L)
                         (NOT (EQUAL X (CAR L)))
                         (p X (CDR L)))
                    (p X L))
           (IMPLIES (NOT (LISTP L)) (p X L))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme leads to the following three new
formulas:

Case 3. (IMPLIES (AND (LISTP L)
                      (EQUAL X (CAR L))
                      (EQUAL (EQUAL (OCCURRENCES X (CDR L)) 0)
                             (NOT (MEMBER X (CDR L)))))
                 (EQUAL (EQUAL (OCCURRENCES X L) 0)
                        (NOT (MEMBER X L)))).

  This simplifies, unfolding the definitions of NOT, OCCURRENCES, MEMBER,
  EQUAL, and ADD1, to:

        T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL X (CAR L)))
                      (EQUAL (EQUAL (OCCURRENCES X (CDR L)) 0)
                             (NOT (MEMBER X (CDR L)))))
                 (EQUAL (EQUAL (OCCURRENCES X L) 0)
                        (NOT (MEMBER X L)))).

  This simplifies, expanding the definitions of NOT, OCCURRENCES, MEMBER, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (NOT (LISTP L))
                 (EQUAL (EQUAL (OCCURRENCES X L) 0)
                        (NOT (MEMBER X L)))).

  This simplifies, expanding the definitions of OCCURRENCES, EQUAL, MEMBER,
  and NOT, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-OCCURRENCES-ZERO


(PROVE-LEMMA MEMBER-NON-LIST
             (REWRITE)
             (IMPLIES (NOT (LISTP L))
                      (NOT (MEMBER X L)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This formula simplifies, opening up the definition of MEMBER, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-NON-LIST


(PROVE-LEMMA MEMBER-DELETE
             (REWRITE)
             (EQUAL (MEMBER X (DELETE Y L))
                    (IF (MEMBER X L)
                        (IF (EQUAL X Y)
                            (LESSP 1 (OCCURRENCES X L))
                            T)
                        F))
             ((ENABLE DELETE OCCURRENCES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This simplifies, obviously, to three new goals:

Case 3. (IMPLIES (NOT (MEMBER X L))
                 (EQUAL (MEMBER X (DELETE Y L)) F)),

  which again simplifies, trivially, to:

        (IMPLIES (NOT (MEMBER X L))
                 (NOT (MEMBER X (DELETE Y L)))),

  which we will name *1.

Case 2. (IMPLIES (AND (MEMBER X L) (EQUAL X Y))
                 (EQUAL (MEMBER X (DELETE Y L))
                        (LESSP 1 (OCCURRENCES X L)))).

  This again simplifies, obviously, to:

        (IMPLIES (MEMBER Y L)
                 (EQUAL (MEMBER Y (DELETE Y L))
                        (LESSP 1 (OCCURRENCES Y L)))),

  which we would normally push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(EQUAL (MEMBER X (DELETE Y L))
       (IF (MEMBER X L)
           (IF (EQUAL X Y)
               (LESSP 1 (OCCURRENCES X L))
               T)
           F)).

We named this *1.  We will try to prove it by induction.  There are three
plausible inductions.  However, they merge into one likely candidate induction.
We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
                    (p X Y L))
           (IMPLIES (AND (LISTP L)
                         (NOT (EQUAL Y (CAR L)))
                         (p X Y (CDR L)))
                    (p X Y L))
           (IMPLIES (NOT (LISTP L)) (p X Y L))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
                 (EQUAL (MEMBER X (DELETE Y L))
                        (IF (MEMBER X L)
                            (IF (EQUAL X Y)
                                (LESSP 1 (OCCURRENCES X L))
                                T)
                            F))),

  which simplifies, applying SUB1-ADD1, and unfolding DELETE, MEMBER,
  OCCURRENCES, SUB1, NUMBERP, EQUAL, and LESSP, to the following four new
  conjectures:

  Case 3.4.
          (IMPLIES (AND (LISTP L)
                        (EQUAL X (CAR L))
                        (NOT (EQUAL (OCCURRENCES X (CDR L)) 0)))
                   (EQUAL (MEMBER X (CDR L)) T)).

    This again simplifies, clearly, to:

          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL (OCCURRENCES (CAR L) (CDR L))
                                    0)))
                   (MEMBER (CAR L) (CDR L))).

    Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z V) to eliminate
    (CAR L) and (CDR L).  We thus obtain:

          (IMPLIES (NOT (EQUAL (OCCURRENCES Z V) 0))
                   (MEMBER Z V)),

    which we will name *1.1.

  Case 3.3.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL X (CAR L)))
                        (MEMBER X (CDR L)))
                   (EQUAL (MEMBER X (CDR L)) T)).

    This again simplifies, clearly, to:

          T.

  Case 3.2.
          (IMPLIES (AND (LISTP L)
                        (EQUAL X (CAR L))
                        (EQUAL (OCCURRENCES X (CDR L)) 0))
                   (EQUAL (MEMBER X (CDR L)) F)).

    This again simplifies, clearly, to:

          (IMPLIES (AND (LISTP L)
                        (EQUAL (OCCURRENCES (CAR L) (CDR L))
                               0))
                   (NOT (MEMBER (CAR L) (CDR L)))).

    Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z V) to eliminate
    (CAR L) and (CDR L).  We would thus like to prove the new formula:

          (IMPLIES (EQUAL (OCCURRENCES Z V) 0)
                   (NOT (MEMBER Z V))),

    which we will name *1.2.

  Case 3.1.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL X (CAR L)))
                        (NOT (MEMBER X (CDR L))))
                   (EQUAL (MEMBER X (CDR L)) F)).

    This again simplifies, trivially, to:

          T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL Y (CAR L)))
                      (EQUAL (MEMBER X (DELETE Y (CDR L)))
                             (IF (MEMBER X (CDR L))
                                 (IF (EQUAL X Y)
                                     (LESSP 1 (OCCURRENCES X (CDR L)))
                                     T)
                                 F)))
                 (EQUAL (MEMBER X (DELETE Y L))
                        (IF (MEMBER X L)
                            (IF (EQUAL X Y)
                                (LESSP 1 (OCCURRENCES X L))
                                T)
                            F))).

  This simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and opening up
  the definitions of DELETE, MEMBER, OCCURRENCES, SUB1, NUMBERP, EQUAL, and
  LESSP, to three new formulas:

  Case 2.3.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (NOT (MEMBER X (CDR L)))
                        (EQUAL (MEMBER X (DELETE Y (CDR L)))
                               F)
                        (EQUAL X (CAR L))
                        (EQUAL X Y))
                   (NOT (EQUAL (OCCURRENCES X (CDR L)) 0))),

    which again simplifies, clearly, to:

          T.

  Case 2.2.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (MEMBER X (CDR L))
                        (EQUAL X Y)
                        (EQUAL (MEMBER X (DELETE Y (CDR L)))
                               (LESSP 1 (OCCURRENCES X (CDR L))))
                        (NOT (EQUAL X (CAR L))))
                   (EQUAL (MEMBER X
                                  (CONS (CAR L) (DELETE X (CDR L))))
                          (LESSP 1 (OCCURRENCES X (CDR L))))).

    This again simplifies, applying CDR-CONS and CAR-CONS, and expanding
    MEMBER, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (MEMBER X (CDR L))
                        (EQUAL X Y)
                        (EQUAL (MEMBER X (DELETE Y (CDR L)))
                               (LESSP 1 (OCCURRENCES X (CDR L))))
                        (EQUAL X (CAR L)))
                   (EQUAL (MEMBER X (CDR L))
                          (LESSP 1
                                 (ADD1 (OCCURRENCES X (CDR L)))))).

    This again simplifies, trivially, to:

          T.

Case 1. (IMPLIES (NOT (LISTP L))
                 (EQUAL (MEMBER X (DELETE Y L))
                        (IF (MEMBER X L)
                            (IF (EQUAL X Y)
                                (LESSP 1 (OCCURRENCES X L))
                                T)
                            F))).

  This simplifies, unfolding the functions DELETE, MEMBER, and EQUAL, to:

        T.


     So next consider:

      (IMPLIES (EQUAL (OCCURRENCES Z V) 0)
               (NOT (MEMBER Z V))),

which we named *1.2 above.  We will appeal to induction.  Two inductions are
suggested by terms in the conjecture.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP V)
                         (EQUAL Z (CAR V))
                         (p Z (CDR V)))
                    (p Z V))
           (IMPLIES (AND (LISTP V)
                         (NOT (EQUAL Z (CAR V)))
                         (p Z (CDR V)))
                    (p Z V))
           (IMPLIES (NOT (LISTP V)) (p Z V))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT V) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme produces five
new conjectures:

Case 5. (IMPLIES (AND (LISTP V)
                      (EQUAL Z (CAR V))
                      (NOT (EQUAL (OCCURRENCES Z (CDR V)) 0))
                      (EQUAL (OCCURRENCES Z V) 0))
                 (NOT (MEMBER Z V))),

  which simplifies, expanding the function OCCURRENCES, to:

        T.

Case 4. (IMPLIES (AND (LISTP V)
                      (EQUAL Z (CAR V))
                      (NOT (MEMBER Z (CDR V)))
                      (EQUAL (OCCURRENCES Z V) 0))
                 (NOT (MEMBER Z V))),

  which simplifies, expanding the definition of OCCURRENCES, to:

        T.

Case 3. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL Z (CAR V)))
                      (NOT (EQUAL (OCCURRENCES Z (CDR V)) 0))
                      (EQUAL (OCCURRENCES Z V) 0))
                 (NOT (MEMBER Z V))),

  which simplifies, unfolding the function OCCURRENCES, to:

        T.

Case 2. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL Z (CAR V)))
                      (NOT (MEMBER Z (CDR V)))
                      (EQUAL (OCCURRENCES Z V) 0))
                 (NOT (MEMBER Z V))),

  which simplifies, expanding the definitions of OCCURRENCES and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP V))
                      (EQUAL (OCCURRENCES Z V) 0))
                 (NOT (MEMBER Z V))),

  which simplifies, unfolding the functions OCCURRENCES, EQUAL, and MEMBER, to:

        T.


     That finishes the proof of *1.2.


     So let us turn our attention to:

      (IMPLIES (NOT (EQUAL (OCCURRENCES Z V) 0))
               (MEMBER Z V)),

which is formula *1.1 above.  Let us appeal to the induction principle.  There
are two plausible inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP V)
                         (EQUAL Z (CAR V))
                         (p Z (CDR V)))
                    (p Z V))
           (IMPLIES (AND (LISTP V)
                         (NOT (EQUAL Z (CAR V)))
                         (p Z (CDR V)))
                    (p Z V))
           (IMPLIES (NOT (LISTP V)) (p Z V))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT V)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme leads to five new conjectures:

Case 5. (IMPLIES (AND (LISTP V)
                      (EQUAL Z (CAR V))
                      (EQUAL (OCCURRENCES Z (CDR V)) 0)
                      (NOT (EQUAL (OCCURRENCES Z V) 0)))
                 (MEMBER Z V)),

  which simplifies, opening up ADD1, OCCURRENCES, EQUAL, and MEMBER, to:

        T.

Case 4. (IMPLIES (AND (LISTP V)
                      (EQUAL Z (CAR V))
                      (MEMBER Z (CDR V))
                      (NOT (EQUAL (OCCURRENCES Z V) 0)))
                 (MEMBER Z V)),

  which simplifies, expanding the functions OCCURRENCES and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL Z (CAR V)))
                      (EQUAL (OCCURRENCES Z (CDR V)) 0)
                      (NOT (EQUAL (OCCURRENCES Z V) 0)))
                 (MEMBER Z V)),

  which simplifies, unfolding OCCURRENCES and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL Z (CAR V)))
                      (MEMBER Z (CDR V))
                      (NOT (EQUAL (OCCURRENCES Z V) 0)))
                 (MEMBER Z V)),

  which simplifies, expanding the functions OCCURRENCES and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP V))
                      (NOT (EQUAL (OCCURRENCES Z V) 0)))
                 (MEMBER Z V)),

  which simplifies, opening up the functions OCCURRENCES and EQUAL, to:

        T.


     That finishes the proof of *1.1, which, in turn, finishes the proof of *1.
Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-DELETE


(PROVE-LEMMA MEMBER-DELETE-IMPLIES-MEMBERSHIP
             (REWRITE)
             (IMPLIES (MEMBER X (DELETE Y L))
                      (MEMBER X L))
             ((ENABLE DELETE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  Note that MEMBER-DELETE-IMPLIES-MEMBERSHIP contains the free
variable Y which will be chosen by instantiating the hypothesis
(MEMBER X (DELETE Y L)).



     Give the conjecture the name *1.


     Let us appeal to the induction principle.  Two inductions are suggested
by terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
                    (p X L Y))
           (IMPLIES (AND (LISTP L)
                         (NOT (EQUAL Y (CAR L)))
                         (p X (CDR L) Y))
                    (p X L Y))
           (IMPLIES (NOT (LISTP L)) (p X L Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme generates four new conjectures:

Case 4. (IMPLIES (AND (LISTP L)
                      (EQUAL Y (CAR L))
                      (MEMBER X (DELETE Y L)))
                 (MEMBER X L)),

  which simplifies, expanding the functions DELETE and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL Y (CAR L)))
                      (NOT (MEMBER X (DELETE Y (CDR L))))
                      (MEMBER X (DELETE Y L)))
                 (MEMBER X L)),

  which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
  expanding DELETE and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL Y (CAR L)))
                      (MEMBER X (CDR L))
                      (MEMBER X (DELETE Y L)))
                 (MEMBER X L)),

  which simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
  opening up the functions DELETE and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP L))
                      (MEMBER X (DELETE Y L)))
                 (MEMBER X L)),

  which simplifies, expanding DELETE and MEMBER, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-DELETE-IMPLIES-MEMBERSHIP


(PROVE-LEMMA OCCURRENCES-DELETE
             (REWRITE)
             (EQUAL (OCCURRENCES X (DELETE Y L))
                    (IF (EQUAL X Y)
                        (IF (MEMBER X L)
                            (SUB1 (OCCURRENCES X L))
                            0)
                        (OCCURRENCES X L)))
             ((ENABLE OCCURRENCES DELETE EQUAL-OCCURRENCES-ZERO)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This conjecture simplifies, clearly, to three new conjectures:

Case 3. (IMPLIES (NOT (EQUAL X Y))
                 (EQUAL (OCCURRENCES X (DELETE Y L))
                        (OCCURRENCES X L))),

  which we will name *1.

Case 2. (IMPLIES (AND (EQUAL X Y) (MEMBER X L))
                 (EQUAL (OCCURRENCES X (DELETE Y L))
                        (SUB1 (OCCURRENCES X L)))).

  This again simplifies, obviously, to:

        (IMPLIES (MEMBER Y L)
                 (EQUAL (OCCURRENCES Y (DELETE Y L))
                        (SUB1 (OCCURRENCES Y L)))),

  which we would normally push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(EQUAL (OCCURRENCES X (DELETE Y L))
       (IF (EQUAL X Y)
           (IF (MEMBER X L)
               (SUB1 (OCCURRENCES X L))
               0)
           (OCCURRENCES X L))),

named *1.  Let us appeal to the induction principle.  Four inductions are
suggested by terms in the conjecture.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
                    (p X Y L))
           (IMPLIES (AND (LISTP L)
                         (NOT (EQUAL Y (CAR L)))
                         (p X Y (CDR L)))
                    (p X Y L))
           (IMPLIES (NOT (LISTP L)) (p X Y L))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (LISTP L) (EQUAL Y (CAR L)))
                 (EQUAL (OCCURRENCES X (DELETE Y L))
                        (IF (EQUAL X Y)
                            (IF (MEMBER X L)
                                (SUB1 (OCCURRENCES X L))
                                0)
                            (OCCURRENCES X L)))),

  which simplifies, applying SUB1-ADD1, and expanding the definitions of
  DELETE, MEMBER, and OCCURRENCES, to:

        T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL Y (CAR L)))
                      (EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
                             (IF (EQUAL X Y)
                                 (IF (MEMBER X (CDR L))
                                     (SUB1 (OCCURRENCES X (CDR L)))
                                     0)
                                 (OCCURRENCES X (CDR L)))))
                 (EQUAL (OCCURRENCES X (DELETE Y L))
                        (IF (EQUAL X Y)
                            (IF (MEMBER X L)
                                (SUB1 (OCCURRENCES X L))
                                0)
                            (OCCURRENCES X L)))).

  This simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and expanding
  the functions DELETE, OCCURRENCES, and MEMBER, to three new goals:

  Case 2.3.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (EQUAL X Y)
                        (MEMBER X (CDR L))
                        (EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
                               (SUB1 (OCCURRENCES X (CDR L))))
                        (NOT (EQUAL X (CAR L))))
                   (EQUAL (OCCURRENCES X
                                       (CONS (CAR L) (DELETE X (CDR L))))
                          (SUB1 (OCCURRENCES X (CDR L))))),

    which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
    function OCCURRENCES, to:

          T.

  Case 2.2.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (EQUAL X Y)
                        (MEMBER X (CDR L))
                        (EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
                               (SUB1 (OCCURRENCES X (CDR L))))
                        (EQUAL X (CAR L)))
                   (EQUAL (OCCURRENCES X (CDR L))
                          (SUB1 (ADD1 (OCCURRENCES X (CDR L)))))).

    This again simplifies, clearly, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL Y (CAR L)))
                        (EQUAL X Y)
                        (NOT (MEMBER X (CDR L)))
                        (EQUAL (OCCURRENCES X (DELETE Y (CDR L)))
                               0)
                        (NOT (EQUAL X (CAR L))))
                   (EQUAL (OCCURRENCES X
                                       (CONS (CAR L) (DELETE X (CDR L))))
                          0)).

    This again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, CDR-CONS,
    and CAR-CONS, and unfolding OCCURRENCES, to:

          T.

Case 1. (IMPLIES (NOT (LISTP L))
                 (EQUAL (OCCURRENCES X (DELETE Y L))
                        (IF (EQUAL X Y)
                            (IF (MEMBER X L)
                                (SUB1 (OCCURRENCES X L))
                                0)
                            (OCCURRENCES X L)))).

  This simplifies, unfolding DELETE, OCCURRENCES, MEMBER, and EQUAL, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

OCCURRENCES-DELETE


(PROVE-LEMMA MEMBER-BAGDIFF
             (REWRITE)
             (EQUAL (MEMBER X (BAGDIFF A B))
                    (LESSP (OCCURRENCES X B)
                           (OCCURRENCES X A)))
             ((ENABLE BAGDIFF OCCURRENCES EQUAL-OCCURRENCES-ZERO
                      OCCURRENCES-DELETE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Call the conjecture *1.


     We will try to prove it by induction.  There are three plausible
inductions.  They merge into two likely candidate inductions.  However, only
one is unflawed.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP B)
                         (MEMBER (CAR B) A)
                         (p X (DELETE (CAR B) A) (CDR B)))
                    (p X A B))
           (IMPLIES (AND (LISTP B)
                         (NOT (MEMBER (CAR B) A))
                         (p X A (CDR B)))
                    (p X A B))
           (IMPLIES (NOT (LISTP B)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT B)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instances chosen for A.  The
above induction scheme generates three new goals:

Case 3. (IMPLIES (AND (LISTP B)
                      (MEMBER (CAR B) A)
                      (EQUAL (MEMBER X
                                     (BAGDIFF (DELETE (CAR B) A) (CDR B)))
                             (LESSP (OCCURRENCES X (CDR B))
                                    (OCCURRENCES X (DELETE (CAR B) A)))))
                 (EQUAL (MEMBER X (BAGDIFF A B))
                        (LESSP (OCCURRENCES X B)
                               (OCCURRENCES X A)))),

  which simplifies, appealing to the lemmas OCCURRENCES-DELETE, SUB1-ADD1, and
  EQUAL-OCCURRENCES-ZERO, and unfolding BAGDIFF, OCCURRENCES, and LESSP, to:

        (IMPLIES (AND (LISTP B)
                      (MEMBER (CAR B) A)
                      (EQUAL X (CAR B))
                      (NOT (MEMBER X A))
                      (EQUAL (MEMBER X
                                     (BAGDIFF (DELETE (CAR B) A) (CDR B)))
                             (LESSP (OCCURRENCES X (CDR B)) 0)))
                 (NOT (MEMBER X (BAGDIFF A (CDR B))))).

  This again simplifies, clearly, to:

        T.

Case 2. (IMPLIES (AND (LISTP B)
                      (NOT (MEMBER (CAR B) A))
                      (EQUAL (MEMBER X (BAGDIFF A (CDR B)))
                             (LESSP (OCCURRENCES X (CDR B))
                                    (OCCURRENCES X A))))
                 (EQUAL (MEMBER X (BAGDIFF A B))
                        (LESSP (OCCURRENCES X B)
                               (OCCURRENCES X A)))).

  This simplifies, expanding the functions BAGDIFF and OCCURRENCES, to the
  following two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP B)
                        (NOT (MEMBER (CAR B) A))
                        (EQUAL (MEMBER X (BAGDIFF A (CDR B)))
                               (LESSP (OCCURRENCES X (CDR B))
                                      (OCCURRENCES X A)))
                        (NOT (EQUAL X (CAR B))))
                   (EQUAL (MEMBER X (BAGDIFF A (CDR B)))
                          (LESSP (OCCURRENCES X (CDR B))
                                 (OCCURRENCES X A)))).

    This again simplifies, obviously, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP B)
                        (NOT (MEMBER (CAR B) A))
                        (EQUAL (MEMBER X (BAGDIFF A (CDR B)))
                               (LESSP (OCCURRENCES X (CDR B))
                                      (OCCURRENCES X A)))
                        (EQUAL X (CAR B)))
                   (EQUAL (MEMBER X (BAGDIFF A (CDR B)))
                          (LESSP (ADD1 (OCCURRENCES X (CDR B)))
                                 (OCCURRENCES X A)))).

    But this again simplifies, appealing to the lemma EQUAL-OCCURRENCES-ZERO,
    and unfolding the functions LESSP and EQUAL, to:

          T.

Case 1. (IMPLIES (NOT (LISTP B))
                 (EQUAL (MEMBER X (BAGDIFF A B))
                        (LESSP (OCCURRENCES X B)
                               (OCCURRENCES X A)))),

  which simplifies, rewriting with the lemma EQUAL-OCCURRENCES-ZERO, and
  expanding the functions BAGDIFF, OCCURRENCES, EQUAL, and LESSP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-BAGDIFF


(PROVE-LEMMA BAGDIFF-DELETE
             (REWRITE)
             (EQUAL (BAGDIFF (DELETE E X) Y)
                    (DELETE E (BAGDIFF X Y)))
             ((ENABLE BAGDIFF DELETE DELETE-DELETE DELETE-NON-MEMBER
                      MEMBER-BAGDIFF MEMBER-DELETE OCCURRENCES-DELETE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Three inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP Y)
                         (MEMBER (CAR Y) (DELETE E X))
                         (p E X (CDR Y))
                         (p E (DELETE (CAR Y) X) (CDR Y)))
                    (p E X Y))
           (IMPLIES (AND (LISTP Y)
                         (NOT (MEMBER (CAR Y) (DELETE E X)))
                         (p E X (CDR Y))
                         (p E (DELETE (CAR Y) X) (CDR Y)))
                    (p E X Y))
           (IMPLIES (NOT (LISTP Y)) (p E X Y))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  Note, however, the inductive instances
chosen for X.  The above induction scheme leads to three new goals:

Case 3. (IMPLIES (AND (LISTP Y)
                      (MEMBER (CAR Y) (DELETE E X))
                      (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                             (DELETE E (BAGDIFF X (CDR Y))))
                      (EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
                                      (CDR Y))
                             (DELETE E
                                     (BAGDIFF (DELETE (CAR Y) X)
                                              (CDR Y)))))
                 (EQUAL (BAGDIFF (DELETE E X) Y)
                        (DELETE E (BAGDIFF X Y)))),

  which simplifies, applying the lemmas MEMBER-DELETE and DELETE-DELETE, and
  opening up the definition of BAGDIFF, to:

        T.

Case 2. (IMPLIES (AND (LISTP Y)
                      (NOT (MEMBER (CAR Y) (DELETE E X)))
                      (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                             (DELETE E (BAGDIFF X (CDR Y))))
                      (EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
                                      (CDR Y))
                             (DELETE E
                                     (BAGDIFF (DELETE (CAR Y) X)
                                              (CDR Y)))))
                 (EQUAL (BAGDIFF (DELETE E X) Y)
                        (DELETE E (BAGDIFF X Y)))),

  which simplifies, rewriting with MEMBER-DELETE, and opening up the function
  BAGDIFF, to the following two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP Y)
                        (EQUAL (CAR Y) E)
                        (NOT (LESSP 1 (OCCURRENCES E X)))
                        (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                               (DELETE E (BAGDIFF X (CDR Y))))
                        (EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
                                        (CDR Y))
                               (DELETE E
                                       (BAGDIFF (DELETE (CAR Y) X) (CDR Y))))
                        (NOT (MEMBER E X)))
                   (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                          (DELETE E (BAGDIFF X (CDR Y))))).

    This again simplifies, trivially, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP Y)
                        (EQUAL (CAR Y) E)
                        (NOT (LESSP 1 (OCCURRENCES E X)))
                        (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                               (DELETE E (BAGDIFF X (CDR Y))))
                        (EQUAL (BAGDIFF (DELETE E (DELETE (CAR Y) X))
                                        (CDR Y))
                               (DELETE E
                                       (BAGDIFF (DELETE (CAR Y) X) (CDR Y))))
                        (MEMBER E X))
                   (EQUAL (BAGDIFF (DELETE E X) (CDR Y))
                          (DELETE E
                                  (BAGDIFF (DELETE (CAR Y) X)
                                           (CDR Y))))).

    But this again simplifies, using linear arithmetic, applying MEMBER-DELETE,
    DELETE-NON-MEMBER, MEMBER-BAGDIFF, and OCCURRENCES-DELETE, and opening up
    the function SUB1, to:

          T.

Case 1. (IMPLIES (NOT (LISTP Y))
                 (EQUAL (BAGDIFF (DELETE E X) Y)
                        (DELETE E (BAGDIFF X Y)))).

  This simplifies, unfolding the definition of BAGDIFF, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

BAGDIFF-DELETE


(PROVE-LEMMA SUBBAGP-DELETE
             (REWRITE)
             (IMPLIES (SUBBAGP X (DELETE U Y))
                      (SUBBAGP X Y))
             ((ENABLE DELETE SUBBAGP DELETE-DELETE
                      MEMBER-DELETE-IMPLIES-MEMBERSHIP)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  Note that SUBBAGP-DELETE contains the free variable U which will be
chosen by instantiating the hypothesis (SUBBAGP X (DELETE U Y)).



     Give the conjecture the name *1.


     Let us appeal to the induction principle.  Three inductions are suggested
by terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP X)
                         (MEMBER (CAR X) (DELETE U Y))
                         (p (CDR X) (DELETE (CAR X) Y) U))
                    (p X Y U))
           (IMPLIES (AND (LISTP X)
                         (NOT (MEMBER (CAR X) (DELETE U Y))))
                    (p X Y U))
           (IMPLIES (NOT (LISTP X)) (p X Y U))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for Y.  The above
induction scheme generates four new conjectures:

Case 4. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) (DELETE U Y))
                      (NOT (SUBBAGP (CDR X)
                                    (DELETE U (DELETE (CAR X) Y))))
                      (SUBBAGP X (DELETE U Y)))
                 (SUBBAGP X Y)),

  which simplifies, applying DELETE-DELETE, and opening up SUBBAGP, to:

        T.

Case 3. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) (DELETE U Y))
                      (SUBBAGP (CDR X) (DELETE (CAR X) Y))
                      (SUBBAGP X (DELETE U Y)))
                 (SUBBAGP X Y)).

  This simplifies, applying the lemmas DELETE-DELETE and
  MEMBER-DELETE-IMPLIES-MEMBERSHIP, and unfolding the function SUBBAGP, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) (DELETE U Y)))
                      (SUBBAGP X (DELETE U Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding the function SUBBAGP, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP X))
                      (SUBBAGP X (DELETE U Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding the definition of SUBBAGP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-DELETE


(PROVE-LEMMA SUBBAGP-CDR1
             (REWRITE)
             (IMPLIES (SUBBAGP X Y)
                      (SUBBAGP (CDR X) Y))
             ((ENABLE SUBBAGP SUBBAGP-DELETE)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

.

Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X)
and (CAR X).  We thus obtain the following two new goals:

Case 2. (IMPLIES (AND (NOT (LISTP X)) (SUBBAGP X Y))
                 (SUBBAGP (CDR X) Y)).

  But this simplifies, applying CDR-NLISTP, and expanding SUBBAGP and LISTP,
  to:

        T.

Case 1. (IMPLIES (SUBBAGP (CONS V Z) Y)
                 (SUBBAGP Z Y)).

  However this simplifies, rewriting with CDR-CONS, CAR-CONS, and
  SUBBAGP-DELETE, and expanding the definition of SUBBAGP, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-CDR1


(PROVE-LEMMA SUBBAGP-CDR2
             (REWRITE)
             (IMPLIES (SUBBAGP X (CDR Y))
                      (SUBBAGP X Y))
             ((ENABLE DELETE SUBBAGP DELETE-NON-MEMBER SUBBAGP-CDR1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

.

Applying the lemma CAR-CDR-ELIM, replace Y by (CONS V Z) to eliminate (CDR Y)
and (CAR Y).  We thus obtain the following two new goals:

Case 2. (IMPLIES (AND (NOT (LISTP Y))
                      (SUBBAGP X (CDR Y)))
                 (SUBBAGP X Y)).

  But this simplifies, applying CDR-NLISTP, and expanding MEMBER, LISTP, and
  SUBBAGP, to:

        T.

Case 1. (IMPLIES (SUBBAGP X Z)
                 (SUBBAGP X (CONS V Z))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(IMPLIES (SUBBAGP X (CDR Y))
         (SUBBAGP X Y)),

which we named *1 above.  We will appeal to induction.  Two inductions are
suggested by terms in the conjecture.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP X)
                         (MEMBER (CAR X) (CDR Y))
                         (p (CDR X) (DELETE (CAR X) Y)))
                    (p X Y))
           (IMPLIES (AND (LISTP X)
                         (NOT (MEMBER (CAR X) (CDR Y))))
                    (p X Y))
           (IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for Y.  The above
induction scheme leads to the following four new conjectures:

Case 4. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) (CDR Y))
                      (NOT (SUBBAGP (CDR X)
                                    (CDR (DELETE (CAR X) Y))))
                      (SUBBAGP X (CDR Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding SUBBAGP and MEMBER, to the following two new
  conjectures:

  Case 4.2.
          (IMPLIES (AND (LISTP X)
                        (MEMBER (CAR X) (CDR Y))
                        (NOT (SUBBAGP (CDR X)
                                      (CDR (DELETE (CAR X) Y))))
                        (SUBBAGP (CDR X)
                                 (DELETE (CAR X) (CDR Y))))
                   (LISTP Y)).

    But this again simplifies, rewriting with CDR-NLISTP, and opening up LISTP
    and MEMBER, to:

          T.

  Case 4.1.
          (IMPLIES (AND (LISTP X)
                        (MEMBER (CAR X) (CDR Y))
                        (NOT (SUBBAGP (CDR X)
                                      (CDR (DELETE (CAR X) Y))))
                        (SUBBAGP (CDR X)
                                 (DELETE (CAR X) (CDR Y))))
                   (SUBBAGP (CDR X) (DELETE (CAR X) Y))).

    This further simplifies, rewriting with CDR-NLISTP, DELETE-NON-MEMBER, and
    SUBBAGP-CDR1, and unfolding the definitions of DELETE, MEMBER, LISTP, and
    SUBBAGP, to the new formula:

          (IMPLIES (AND (LISTP X)
                        (MEMBER (CAR X) (CDR Y))
                        (LISTP Y)
                        (NOT (EQUAL (CAR X) (CAR Y)))
                        (NOT (SUBBAGP (CDR X)
                                      (CDR (CONS (CAR Y)
                                                 (DELETE (CAR X) (CDR Y))))))
                        (SUBBAGP (CDR X)
                                 (DELETE (CAR X) (CDR Y))))
                   (SUBBAGP (CDR X)
                            (CONS (CAR Y)
                                  (DELETE (CAR X) (CDR Y))))),

    which again simplifies, rewriting with CDR-CONS, to:

          T.

Case 3. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) (CDR Y))
                      (SUBBAGP (CDR X) (DELETE (CAR X) Y))
                      (SUBBAGP X (CDR Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding the definitions of SUBBAGP and MEMBER, to:

        (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) (CDR Y))
                      (SUBBAGP (CDR X) (DELETE (CAR X) Y))
                      (SUBBAGP (CDR X)
                               (DELETE (CAR X) (CDR Y))))
                 (LISTP Y)),

  which again simplifies, applying CDR-NLISTP, and opening up the functions
  LISTP and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) (CDR Y)))
                      (SUBBAGP X (CDR Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding the definition of SUBBAGP, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP X))
                      (SUBBAGP X (CDR Y)))
                 (SUBBAGP X Y)).

  This simplifies, unfolding the function SUBBAGP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-CDR2


(PROVE-LEMMA SUBBAGP-BAGINT1
             (REWRITE)
             (SUBBAGP (BAGINT X Y) X)
             ((ENABLE DELETE SUBBAGP BAGINT SUBBAGP-CDR2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Give the conjecture the name *1.


     We will try to prove it by induction.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP X)
                         (MEMBER (CAR X) Y)
                         (p (CDR X) (DELETE (CAR X) Y)))
                    (p X Y))
           (IMPLIES (AND (LISTP X)
                         (NOT (MEMBER (CAR X) Y))
                         (p (CDR X) Y))
                    (p X Y))
           (IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instances chosen for Y.  The
above induction scheme leads to three new formulas:

Case 3. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) Y)
                      (SUBBAGP (BAGINT (CDR X) (DELETE (CAR X) Y))
                               (CDR X)))
                 (SUBBAGP (BAGINT X Y) X)),

  which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  definitions of BAGINT, DELETE, MEMBER, and SUBBAGP, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) Y))
                      (SUBBAGP (BAGINT (CDR X) Y) (CDR X)))
                 (SUBBAGP (BAGINT X Y) X)).

  This simplifies, applying SUBBAGP-CDR2, and unfolding BAGINT, to:

        T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (SUBBAGP (BAGINT X Y) X)),

  which simplifies, appealing to the lemmas SUBBAGP-CDR2 and CDR-NLISTP, and
  unfolding BAGINT, CDR, LISTP, and SUBBAGP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-BAGINT1


(PROVE-LEMMA SUBBAGP-BAGINT2
             (REWRITE)
             (SUBBAGP (BAGINT X Y) Y)
             ((ENABLE SUBBAGP BAGINT SUBBAGP-CDR2)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))


     Give the conjecture the name *1.


     We will try to prove it by induction.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP X)
                         (MEMBER (CAR X) Y)
                         (p (CDR X) (DELETE (CAR X) Y)))
                    (p X Y))
           (IMPLIES (AND (LISTP X)
                         (NOT (MEMBER (CAR X) Y))
                         (p (CDR X) Y))
                    (p X Y))
           (IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instances chosen for Y.  The
above induction scheme leads to three new formulas:

Case 3. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) Y)
                      (SUBBAGP (BAGINT (CDR X) (DELETE (CAR X) Y))
                               (DELETE (CAR X) Y)))
                 (SUBBAGP (BAGINT X Y) Y)),

  which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  definitions of BAGINT and SUBBAGP, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) Y))
                      (SUBBAGP (BAGINT (CDR X) Y) Y))
                 (SUBBAGP (BAGINT X Y) Y)).

  This simplifies, expanding BAGINT, to:

        T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (SUBBAGP (BAGINT X Y) Y)).

  This simplifies, applying SUBBAGP-CDR2, and opening up the functions BAGINT,
  SUBBAGP, and LISTP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-BAGINT2


(PROVE-LEMMA OCCURRENCES-BAGINT
             (REWRITE)
             (EQUAL (OCCURRENCES X (BAGINT A B))
                    (IF (LESSP (OCCURRENCES X A)
                               (OCCURRENCES X B))
                        (OCCURRENCES X A)
                        (OCCURRENCES X B)))
             ((ENABLE OCCURRENCES BAGINT EQUAL-OCCURRENCES-ZERO
                      OCCURRENCES-DELETE)))

This formula simplifies, obviously, to the following two new conjectures:

Case 2. (IMPLIES (NOT (LESSP (OCCURRENCES X A)
                             (OCCURRENCES X B)))
                 (EQUAL (OCCURRENCES X (BAGINT A B))
                        (OCCURRENCES X B))).

  Call the above conjecture *1.

Case 1. (IMPLIES (LESSP (OCCURRENCES X A)
                        (OCCURRENCES X B))
                 (EQUAL (OCCURRENCES X (BAGINT A B))
                        (OCCURRENCES X A))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (OCCURRENCES X (BAGINT A B))
       (IF (LESSP (OCCURRENCES X A)
                  (OCCURRENCES X B))
           (OCCURRENCES X A)
           (OCCURRENCES X B))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  The
recursive terms in the conjecture suggest five inductions.  They merge into
two likely candidate inductions.  However, only one is unflawed.  We will
induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP A)
                         (MEMBER (CAR A) B)
                         (p X (CDR A) (DELETE (CAR A) B)))
                    (p X A B))
           (IMPLIES (AND (LISTP A)
                         (NOT (MEMBER (CAR A) B))
                         (p X (CDR A) B))
                    (p X A B))
           (IMPLIES (NOT (LISTP A)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instances chosen for B.  The
above induction scheme leads to the following three new goals:

Case 3. (IMPLIES (AND (LISTP A)
                      (MEMBER (CAR A) B)
                      (EQUAL (OCCURRENCES X
                                          (BAGINT (CDR A) (DELETE (CAR A) B)))
                             (IF (LESSP (OCCURRENCES X (CDR A))
                                        (OCCURRENCES X (DELETE (CAR A) B)))
                                 (OCCURRENCES X (CDR A))
                                 (OCCURRENCES X (DELETE (CAR A) B)))))
                 (EQUAL (OCCURRENCES X (BAGINT A B))
                        (IF (LESSP (OCCURRENCES X A)
                                   (OCCURRENCES X B))
                            (OCCURRENCES X A)
                            (OCCURRENCES X B)))).

  This simplifies, applying OCCURRENCES-DELETE, EQUAL-OCCURRENCES-ZERO,
  CDR-CONS, CAR-CONS, SUB1-ADD1, and ADD1-SUB1, and opening up the definitions
  of BAGINT, OCCURRENCES, and LESSP, to two new goals:

  Case 3.2.
          (IMPLIES
                  (AND (LISTP A)
                       (MEMBER (CAR A) B)
                       (EQUAL X (CAR A))
                       (NOT (MEMBER X B))
                       (NOT (LESSP (OCCURRENCES X (CDR A)) 0))
                       (EQUAL (OCCURRENCES X
                                           (BAGINT (CDR A) (DELETE (CAR A) B)))
                              0))
                  (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                         (OCCURRENCES X B))),

    which again simplifies, trivially, to:

          T.

  Case 3.1.
          (IMPLIES
                  (AND (LISTP A)
                       (MEMBER (CAR A) B)
                       (EQUAL X (CAR A))
                       (NOT (MEMBER X B))
                       (LESSP (OCCURRENCES X (CDR A)) 0)
                       (EQUAL (OCCURRENCES X
                                           (BAGINT (CDR A) (DELETE (CAR A) B)))
                              (OCCURRENCES X (CDR A))))
                  (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                         (OCCURRENCES X B))).

    This again simplifies, trivially, to:

          T.

Case 2. (IMPLIES (AND (LISTP A)
                      (NOT (MEMBER (CAR A) B))
                      (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                             (IF (LESSP (OCCURRENCES X (CDR A))
                                        (OCCURRENCES X B))
                                 (OCCURRENCES X (CDR A))
                                 (OCCURRENCES X B))))
                 (EQUAL (OCCURRENCES X (BAGINT A B))
                        (IF (LESSP (OCCURRENCES X A)
                                   (OCCURRENCES X B))
                            (OCCURRENCES X A)
                            (OCCURRENCES X B)))).

  This simplifies, expanding the functions BAGINT and OCCURRENCES, to the
  following three new conjectures:

  Case 2.3.
          (IMPLIES (AND (LISTP A)
                        (NOT (MEMBER (CAR A) B))
                        (NOT (LESSP (OCCURRENCES X (CDR A))
                                    (OCCURRENCES X B)))
                        (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                               (OCCURRENCES X B))
                        (EQUAL X (CAR A))
                        (LESSP (ADD1 (OCCURRENCES X (CDR A)))
                               (OCCURRENCES X B)))
                   (EQUAL (OCCURRENCES X B)
                          (ADD1 (OCCURRENCES X (CDR A))))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.2.
          (IMPLIES (AND (LISTP A)
                        (NOT (MEMBER (CAR A) B))
                        (LESSP (OCCURRENCES X (CDR A))
                               (OCCURRENCES X B))
                        (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                               (OCCURRENCES X (CDR A)))
                        (EQUAL X (CAR A))
                        (NOT (LESSP (ADD1 (OCCURRENCES X (CDR A)))
                                    (OCCURRENCES X B))))
                   (EQUAL (OCCURRENCES X (CDR A))
                          (OCCURRENCES X B))),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (EQUAL (OCCURRENCES (CAR A) B)
                               (PLUS 1
                                     (OCCURRENCES (CAR A) (CDR A))))
                        (LISTP A)
                        (NOT (MEMBER (CAR A) B))
                        (LESSP (OCCURRENCES (CAR A) (CDR A))
                               (PLUS 1
                                     (OCCURRENCES (CAR A) (CDR A))))
                        (EQUAL (OCCURRENCES (CAR A)
                                            (BAGINT (CDR A) B))
                               (OCCURRENCES (CAR A) (CDR A)))
                        (NOT (LESSP (ADD1 (OCCURRENCES (CAR A) (CDR A)))
                                    (PLUS 1
                                          (OCCURRENCES (CAR A) (CDR A))))))
                   (EQUAL (OCCURRENCES (CAR A) (CDR A))
                          (PLUS 1
                                (OCCURRENCES (CAR A) (CDR A))))).

    But this again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, and
    unfolding the definition of LESSP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP A)
                        (NOT (MEMBER (CAR A) B))
                        (LESSP (OCCURRENCES X (CDR A))
                               (OCCURRENCES X B))
                        (EQUAL (OCCURRENCES X (BAGINT (CDR A) B))
                               (OCCURRENCES X (CDR A)))
                        (EQUAL X (CAR A))
                        (LESSP (ADD1 (OCCURRENCES X (CDR A)))
                               (OCCURRENCES X B)))
                   (EQUAL (OCCURRENCES X (CDR A))
                          (ADD1 (OCCURRENCES X (CDR A))))).

    However this again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, and
    opening up LESSP, to:

          T.

Case 1. (IMPLIES (NOT (LISTP A))
                 (EQUAL (OCCURRENCES X (BAGINT A B))
                        (IF (LESSP (OCCURRENCES X A)
                                   (OCCURRENCES X B))
                            (OCCURRENCES X A)
                            (OCCURRENCES X B)))).

  This simplifies, appealing to the lemma EQUAL-OCCURRENCES-ZERO, and
  expanding BAGINT, LISTP, OCCURRENCES, EQUAL, and LESSP, to:

        (IMPLIES (AND (NOT (LISTP A))
                      (NOT (MEMBER X B)))
                 (EQUAL 0 (OCCURRENCES X B))),

  which again simplifies, rewriting with EQUAL-OCCURRENCES-ZERO, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

OCCURRENCES-BAGINT


(PROVE-LEMMA OCCURRENCES-BAGDIFF
             (REWRITE)
             (EQUAL (OCCURRENCES X (BAGDIFF A B))
                    (DIFFERENCE (OCCURRENCES X A)
                                (OCCURRENCES X B)))
             ((ENABLE OCCURRENCES BAGDIFF EQUAL-OCCURRENCES-ZERO
                      OCCURRENCES-DELETE)))


     Call the conjecture *1.


     We will try to prove it by induction.  There are three plausible
inductions.  They merge into two likely candidate inductions.  However, only
one is unflawed.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP B)
                         (MEMBER (CAR B) A)
                         (p X (DELETE (CAR B) A) (CDR B)))
                    (p X A B))
           (IMPLIES (AND (LISTP B)
                         (NOT (MEMBER (CAR B) A))
                         (p X A (CDR B)))
                    (p X A B))
           (IMPLIES (NOT (LISTP B)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT B)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instances chosen for A.  The
above induction scheme generates three new goals:

Case 3. (IMPLIES (AND (LISTP B)
                      (MEMBER (CAR B) A)
                      (EQUAL (OCCURRENCES X
                                          (BAGDIFF (DELETE (CAR B) A) (CDR B)))
                             (DIFFERENCE (OCCURRENCES X (DELETE (CAR B) A))
                                         (OCCURRENCES X (CDR B)))))
                 (EQUAL (OCCURRENCES X (BAGDIFF A B))
                        (DIFFERENCE (OCCURRENCES X A)
                                    (OCCURRENCES X B)))),

  which simplifies, appealing to the lemmas OCCURRENCES-DELETE, SUB1-ADD1,
  EQUAL-OCCURRENCES-ZERO, and MEMBER-BAGDIFF, and unfolding BAGDIFF,
  OCCURRENCES, DIFFERENCE, and LESSP, to:

        T.

Case 2. (IMPLIES (AND (LISTP B)
                      (NOT (MEMBER (CAR B) A))
                      (EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
                             (DIFFERENCE (OCCURRENCES X A)
                                         (OCCURRENCES X (CDR B)))))
                 (EQUAL (OCCURRENCES X (BAGDIFF A B))
                        (DIFFERENCE (OCCURRENCES X A)
                                    (OCCURRENCES X B)))),

  which simplifies, opening up BAGDIFF and OCCURRENCES, to two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP B)
                        (NOT (MEMBER (CAR B) A))
                        (EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
                               (DIFFERENCE (OCCURRENCES X A)
                                           (OCCURRENCES X (CDR B))))
                        (NOT (EQUAL X (CAR B))))
                   (EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
                          (DIFFERENCE (OCCURRENCES X A)
                                      (OCCURRENCES X (CDR B))))),

    which again simplifies, trivially, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP B)
                        (NOT (MEMBER (CAR B) A))
                        (EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
                               (DIFFERENCE (OCCURRENCES X A)
                                           (OCCURRENCES X (CDR B))))
                        (EQUAL X (CAR B)))
                   (EQUAL (OCCURRENCES X (BAGDIFF A (CDR B)))
                          (DIFFERENCE (OCCURRENCES X A)
                                      (ADD1 (OCCURRENCES X (CDR B)))))).

    But this again simplifies, applying EQUAL-OCCURRENCES-ZERO and
    MEMBER-BAGDIFF, and unfolding DIFFERENCE and LESSP, to:

          T.

Case 1. (IMPLIES (NOT (LISTP B))
                 (EQUAL (OCCURRENCES X (BAGDIFF A B))
                        (DIFFERENCE (OCCURRENCES X A)
                                    (OCCURRENCES X B)))).

  This simplifies, applying EQUAL-OCCURRENCES-ZERO, and opening up the
  functions BAGDIFF, OCCURRENCES, EQUAL, and DIFFERENCE, to:

        (IMPLIES (AND (NOT (LISTP B))
                      (NOT (MEMBER X A)))
                 (EQUAL (OCCURRENCES X A) 0)).

  But this again simplifies, rewriting with the lemma EQUAL-OCCURRENCES-ZERO,
  to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

OCCURRENCES-BAGDIFF


(PROVE-LEMMA MEMBER-BAGINT
             (REWRITE)
             (EQUAL (MEMBER X (BAGINT A B))
                    (AND (MEMBER X A) (MEMBER X B)))
             ((ENABLE BAGINT MEMBER-DELETE)))

This simplifies, opening up the function AND, to two new conjectures:

Case 2. (IMPLIES (NOT (MEMBER X A))
                 (EQUAL (MEMBER X (BAGINT A B)) F)),

  which again simplifies, clearly, to:

        (IMPLIES (NOT (MEMBER X A))
                 (NOT (MEMBER X (BAGINT A B)))),

  which we will name *1.

Case 1. (IMPLIES (MEMBER X A)
                 (EQUAL (MEMBER X (BAGINT A B))
                        (MEMBER X B))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (MEMBER X (BAGINT A B))
       (AND (MEMBER X A) (MEMBER X B))),

which we named *1 above.  We will appeal to induction.  There are three
plausible inductions.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP A)
                         (MEMBER (CAR A) B)
                         (p X (CDR A) (DELETE (CAR A) B)))
                    (p X A B))
           (IMPLIES (AND (LISTP A)
                         (NOT (MEMBER (CAR A) B))
                         (p X (CDR A) B))
                    (p X A B))
           (IMPLIES (NOT (LISTP A)) (p X A B))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT A) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  Note, however, the inductive instances chosen
for B.  The above induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (LISTP A)
                      (MEMBER (CAR A) B)
                      (EQUAL (MEMBER X
                                     (BAGINT (CDR A) (DELETE (CAR A) B)))
                             (AND (MEMBER X (CDR A))
                                  (MEMBER X (DELETE (CAR A) B)))))
                 (EQUAL (MEMBER X (BAGINT A B))
                        (AND (MEMBER X A) (MEMBER X B)))),

  which simplifies, applying the lemmas MEMBER-DELETE, CDR-CONS, and CAR-CONS,
  and expanding AND, BAGINT, MEMBER, and EQUAL, to two new goals:

  Case 3.2.
          (IMPLIES (AND (LISTP A)
                        (MEMBER (CAR A) B)
                        (NOT (MEMBER X B))
                        (EQUAL (MEMBER X
                                       (BAGINT (CDR A) (DELETE (CAR A) B)))
                               F))
                   (NOT (EQUAL X (CAR A)))),

    which again simplifies, trivially, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP A)
                        (MEMBER (CAR A) B)
                        (NOT (MEMBER X (CDR A)))
                        (EQUAL (MEMBER X
                                       (BAGINT (CDR A) (DELETE (CAR A) B)))
                               F)
                        (EQUAL X (CAR A)))
                   (EQUAL (MEMBER X B) T)).

    This again simplifies, trivially, to:

          T.

Case 2. (IMPLIES (AND (LISTP A)
                      (NOT (MEMBER (CAR A) B))
                      (EQUAL (MEMBER X (BAGINT (CDR A) B))
                             (AND (MEMBER X (CDR A))
                                  (MEMBER X B))))
                 (EQUAL (MEMBER X (BAGINT A B))
                        (AND (MEMBER X A) (MEMBER X B)))).

  This simplifies, unfolding the definitions of AND, BAGINT, and MEMBER, to
  the new conjecture:

        (IMPLIES (AND (LISTP A)
                      (NOT (MEMBER (CAR A) B))
                      (NOT (MEMBER X (CDR A)))
                      (EQUAL (MEMBER X (BAGINT (CDR A) B))
                             F)
                      (EQUAL X (CAR A)))
                 (NOT (MEMBER X B))),

  which again simplifies, clearly, to:

        T.

Case 1. (IMPLIES (NOT (LISTP A))
                 (EQUAL (MEMBER X (BAGINT A B))
                        (AND (MEMBER X A) (MEMBER X B)))).

  This simplifies, rewriting with MEMBER-NON-LIST, and expanding the
  definitions of BAGINT, AND, and EQUAL, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-BAGINT


(DEFTHEORY BAGS
           (OCCURRENCES-BAGINT BAGDIFF-DELETE OCCURRENCES-BAGDIFF
                               MEMBER-BAGINT MEMBER-BAGDIFF SUBBAGP-BAGINT2
                               SUBBAGP-BAGINT1 SUBBAGP-CDR2 SUBBAGP-CDR1
                               SUBBAGP-DELETE))

[ 0.0 0.0 0.0 ]

BAGS


(PROVE-LEMMA EQUAL-PLUS-0
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) 0)
                    (AND (ZEROP A) (ZEROP B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This simplifies, opening up the functions ZEROP and AND, to six new
conjectures:

Case 6. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (NOT (NUMBERP A)))
                 (NOT (EQUAL B 0))),

  which again simplifies, expanding NUMBERP, PLUS, and EQUAL, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (NOT (NUMBERP A)))
                 (NUMBERP B)),

  which again simplifies, unfolding PLUS and EQUAL, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (EQUAL A 0))
                 (NOT (EQUAL B 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (EQUAL A 0))
                 (NUMBERP B)),

  which again simplifies, expanding the functions EQUAL and PLUS, to:

        T.

Case 2. (IMPLIES (AND (EQUAL (PLUS A B) 0)
                      (NOT (EQUAL A 0)))
                 (NOT (NUMBERP A))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (PLUS A B) 0)
                      (NOT (EQUAL B 0)))
                 (NOT (NUMBERP B))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-PLUS-0


(PROVE-LEMMA PLUS-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                    (EQUAL (FIX B) (FIX C)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This conjecture simplifies, expanding the definition of FIX, to the following
seven new formulas:

Case 7. (IMPLIES (AND (NUMBERP C)
                      (NUMBERP B)
                      (NOT (EQUAL B C)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 6. (IMPLIES (AND (NUMBERP C)
                      (NOT (NUMBERP B))
                      (NOT (EQUAL 0 C)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))),

  which we will name *1.

Case 5. (IMPLIES (AND (NOT (NUMBERP C))
                      (NUMBERP B)
                      (NOT (EQUAL B 0)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (EQUAL (PLUS A B) (PLUS A C))
       (EQUAL (FIX B) (FIX C))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  Two
inductions are suggested by terms in the conjecture.  However, they merge into
one likely candidate induction.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP A) (p A B C))
           (IMPLIES (AND (NOT (ZEROP A)) (p (SUB1 A) B C))
                    (p A B C))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP inform us that the measure (COUNT A) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces the following two new formulas:

Case 2. (IMPLIES (ZEROP A)
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        (EQUAL (FIX B) (FIX C)))).

  This simplifies, expanding the functions ZEROP, EQUAL, PLUS, and FIX, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP A))
                      (EQUAL (EQUAL (PLUS (SUB1 A) B)
                                    (PLUS (SUB1 A) C))
                             (EQUAL (FIX B) (FIX C))))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        (EQUAL (FIX B) (FIX C)))).

  This simplifies, rewriting with ADD1-EQUAL, and unfolding the definitions of
  ZEROP, FIX, PLUS, and EQUAL, to two new goals:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (NUMBERP C))
                        (EQUAL B 0)
                        (EQUAL (EQUAL (PLUS (SUB1 A) B)
                                      (PLUS (SUB1 A) C))
                               T))
                   (EQUAL (PLUS A 0)
                          (ADD1 (PLUS (SUB1 A) C)))),

    which again simplifies, trivially, to:

          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (NUMBERP C))
                        (EQUAL (PLUS (SUB1 A) 0)
                               (PLUS (SUB1 A) C)))
                   (EQUAL (PLUS A 0)
                          (ADD1 (PLUS (SUB1 A) 0)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (NUMBERP B))
                        (EQUAL 0 C)
                        (EQUAL (EQUAL (PLUS (SUB1 A) B)
                                      (PLUS (SUB1 A) C))
                               T))
                   (EQUAL (ADD1 (PLUS (SUB1 A) B))
                          (PLUS A 0))),

    which again simplifies, trivially, to the new formula:

          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (NUMBERP B))
                        (EQUAL (PLUS (SUB1 A) B)
                               (PLUS (SUB1 A) 0)))
                   (EQUAL (ADD1 (PLUS (SUB1 A) 0))
                          (PLUS A 0))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-CANCELLATION


(TOGGLE PLUS-CANCELLATION-OFF PLUS-CANCELLATION T)

[ 0.0 0.0 0.0 ]

PLUS-CANCELLATION-OFF


(PROVE-LEMMA EQUAL-DIFFERENCE-0
             (REWRITE)
             (AND (EQUAL (EQUAL (DIFFERENCE X Y) 0)
                         (NOT (LESSP Y X)))
                  (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                         (NOT (LESSP Y X))))
             ((INDUCT (DIFFERENCE X Y))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  Note that the proposed lemma EQUAL-DIFFERENCE-0 is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.


This conjecture can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to three new conjectures:

Case 3. (IMPLIES (ZEROP X)
                 (AND (EQUAL (EQUAL (DIFFERENCE X Y) 0)
                             (NOT (LESSP Y X)))
                      (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                             (NOT (LESSP Y X))))),

  which simplifies, expanding the definitions of ZEROP, EQUAL, DIFFERENCE,
  LESSP, NOT, and AND, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (ZEROP Y))
                 (AND (EQUAL (EQUAL (DIFFERENCE X Y) 0)
                             (NOT (LESSP Y X)))
                      (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                             (NOT (LESSP Y X))))),

  which simplifies, unfolding the definitions of ZEROP, EQUAL, DIFFERENCE,
  LESSP, NOT, and AND, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (EQUAL (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    0)
                             (NOT (LESSP (SUB1 Y) (SUB1 X))))
                      (EQUAL (EQUAL 0
                                    (DIFFERENCE (SUB1 X) (SUB1 Y)))
                             (NOT (LESSP (SUB1 Y) (SUB1 X)))))
                 (AND (EQUAL (EQUAL (DIFFERENCE X Y) 0)
                             (NOT (LESSP Y X)))
                      (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                             (NOT (LESSP Y X))))),

  which simplifies, expanding the functions NOT, EQUAL, DIFFERENCE, LESSP, and
  AND, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-DIFFERENCE-0


(PROVE-LEMMA DIFFERENCE-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (DIFFERENCE X Y)
                           (DIFFERENCE Z Y))
                    (COND ((LESSP X Y) (NOT (LESSP Y Z)))
                          ((LESSP Z Y) (NOT (LESSP Y X)))
                          (T (EQUAL (FIX X) (FIX Z)))))
             ((ENABLE EQUAL-DIFFERENCE-0)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This simplifies, opening up NOT and FIX, to the following 11 new goals:

Case 11.(IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z))
                      (NUMBERP X))
                 (EQUAL (EQUAL X 0) T)).

  This again simplifies, applying EQUAL-DIFFERENCE-0, and expanding DIFFERENCE
  and LESSP, to the following two new conjectures:

  Case 11.2.
          (IMPLIES (AND (NOT (LESSP Y X))
                        (NOT (LESSP X Y))
                        (EQUAL Y 0)
                        (NOT (NUMBERP Z))
                        (NUMBERP X))
                   (EQUAL X 0)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 11.1.
          (IMPLIES (AND (NOT (LESSP Y X))
                        (NOT (LESSP X Y))
                        (NOT (NUMBERP Y))
                        (NOT (NUMBERP Z))
                        (NUMBERP X))
                   (EQUAL X 0)),

    which again simplifies, unfolding the definition of LESSP, to:

          T.

Case 10.(IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NOT (NUMBERP X)))
                 (EQUAL (EQUAL 0 Z) T)),

  which again simplifies, rewriting with EQUAL-DIFFERENCE-0, and opening up
  the functions DIFFERENCE, LESSP, and EQUAL, to the following two new
  formulas:

  Case 10.2.
          (IMPLIES (AND (NOT (LESSP Y Z))
                        (EQUAL Y 0)
                        (NUMBERP Z)
                        (NOT (NUMBERP X)))
                   (EQUAL 0 Z)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 10.1.
          (IMPLIES (AND (NOT (LESSP Y Z))
                        (NOT (NUMBERP Y))
                        (NUMBERP Z)
                        (NOT (NUMBERP X)))
                   (EQUAL 0 Z)),

    which again simplifies, expanding the function LESSP, to:

          T.

Case 9. (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (EQUAL (EQUAL X Z) T)),

  which again simplifies, obviously, to the new formula:

        (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (EQUAL X Z)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 8. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z)))
                 (NOT (EQUAL X 0))),

  which again simplifies, opening up the functions EQUAL and DIFFERENCE, to:

        T.

Case 7. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP X)))
                 (NOT (EQUAL 0 Z))),

  which again simplifies, expanding the functions DIFFERENCE and EQUAL, to:

        T.

Case 6. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (NOT (EQUAL X Z))),

  which again simplifies, trivially, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (LESSP X Y))
                 (LESSP Y Z)).

  Call the above conjecture *1.

Case 4. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z)))
                 (NUMBERP X)).

  This again simplifies, unfolding DIFFERENCE and EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (LESSP Z Y))
                 (LESSP Y X)),

  which again simplifies, using linear arithmetic, to three new formulas:

  Case 3.3.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NOT (EQUAL (DIFFERENCE X Y)
                                    (DIFFERENCE Z Y)))
                        (NOT (LESSP X Y))
                        (LESSP Z Y))
                   (LESSP Y X)),

    which again simplifies, expanding DIFFERENCE and LESSP, to:

          T.

  Case 3.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL (DIFFERENCE X Y)
                                    (DIFFERENCE Z Y)))
                        (NOT (LESSP X Y))
                        (LESSP Z Y))
                   (LESSP Y X)),

    which again simplifies, appealing to the lemma EQUAL-DIFFERENCE-0, and
    unfolding the functions DIFFERENCE, LESSP, and EQUAL, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE X X)
                                    (DIFFERENCE Z X)))
                        (NOT (LESSP X X))
                        (LESSP Z X))
                   (LESSP X X)),

    which again simplifies, trivially, to the new conjecture:

          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE X X)
                                    (DIFFERENCE Z X)))
                        (LESSP Z X))
                   (LESSP X 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 (EQUAL (DIFFERENCE X Y)
              (DIFFERENCE Z Y))
       (COND ((LESSP X Y) (NOT (LESSP Y Z)))
             ((LESSP Z Y) (NOT (LESSP Y X)))
             (T (EQUAL (FIX X) (FIX Z))))),

named *1.  Let us appeal to the induction principle.  The recursive terms in
the conjecture suggest 12 inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP X)) (ZEROP Y))
                    (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP X))
                         (NOT (ZEROP Y))
                         (p (SUB1 X) (SUB1 Y) (SUB1 Z)))
                    (p X Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for Z and Y.  The above induction
scheme generates the following three new goals:

Case 3. (IMPLIES (ZEROP X)
                 (EQUAL (EQUAL (DIFFERENCE X Y)
                               (DIFFERENCE Z Y))
                        (COND ((LESSP X Y) (NOT (LESSP Y Z)))
                              ((LESSP Z Y) (NOT (LESSP Y X)))
                              (T (EQUAL (FIX X) (FIX Z)))))).

  This simplifies, opening up the functions ZEROP, EQUAL, DIFFERENCE, LESSP,
  NOT, and FIX, to the following 12 new goals:

  Case 3.12.
          (IMPLIES (AND (EQUAL X 0)
                        (NUMBERP Z)
                        (EQUAL Y 0)
                        (EQUAL 0 Z))
                   (EQUAL (EQUAL 0 Z) T)).

    However this again simplifies, opening up the definitions of NUMBERP and
    EQUAL, to:

          T.

  Case 3.11.
          (IMPLIES (AND (EQUAL X 0)
                        (NUMBERP Z)
                        (NOT (NUMBERP Y))
                        (EQUAL 0 Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, expanding the definitions of NUMBERP and EQUAL, to:

          T.

  Case 3.10.
          (IMPLIES (AND (EQUAL X 0)
                        (EQUAL Z 0)
                        (NOT (NUMBERP Y))
                        (NUMBERP Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, unfolding the functions NUMBERP and EQUAL, to:

          T.

  Case 3.9.
          (IMPLIES (AND (EQUAL X 0)
                        (EQUAL Z 0)
                        (EQUAL Y 0)
                        (NUMBERP Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, expanding the functions NUMBERP and EQUAL, to:

          T.

  Case 3.8.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL 0
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y)))))
                   (LESSP (SUB1 Y) (SUB1 Z))),

    which again simplifies, appealing to the lemma EQUAL-DIFFERENCE-0, to:

          T.

  Case 3.7.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL 0
                               (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                   (NOT (LESSP (SUB1 Y) (SUB1 Z)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 3.6.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NUMBERP Z)
                        (EQUAL Y 0)
                        (EQUAL 0 Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, opening up the definitions of NUMBERP and EQUAL,
    to:

          T.

  Case 3.5.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NUMBERP Z)
                        (NOT (NUMBERP Y))
                        (EQUAL 0 Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, expanding NUMBERP and EQUAL, to:

          T.

  Case 3.4.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (EQUAL Z 0)
                        (NOT (NUMBERP Y))
                        (NUMBERP Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, unfolding NUMBERP and EQUAL, to:

          T.

  Case 3.3.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (EQUAL Z 0)
                        (EQUAL Y 0)
                        (NUMBERP Z))
                   (EQUAL (EQUAL 0 Z) T)),

    which again simplifies, opening up NUMBERP and EQUAL, to:

          T.

  Case 3.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL 0
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y)))))
                   (LESSP (SUB1 Y) (SUB1 Z))),

    which again simplifies, rewriting with EQUAL-DIFFERENCE-0, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL 0
                               (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                   (NOT (LESSP (SUB1 Y) (SUB1 Z)))).

    However this again simplifies, using linear arithmetic, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP X)) (ZEROP Y))
                 (EQUAL (EQUAL (DIFFERENCE X Y)
                               (DIFFERENCE Z Y))
                        (COND ((LESSP X Y) (NOT (LESSP Y Z)))
                              ((LESSP Z Y) (NOT (LESSP Y X)))
                              (T (EQUAL (FIX X) (FIX Z)))))),

  which simplifies, expanding ZEROP, EQUAL, DIFFERENCE, LESSP, and FIX, to
  four new goals:

  Case 2.4.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL Y 0)
                        (NUMBERP Z)
                        (EQUAL X Z))
                   (EQUAL (EQUAL X Z) T)),

    which again simplifies, expanding the function EQUAL, to:

          T.

  Case 2.3.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL Y 0)
                        (NUMBERP Z)
                        (EQUAL X Z))
                   (NOT (EQUAL Z 0))),

    which again simplifies, trivially, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (NUMBERP Y))
                        (NUMBERP Z)
                        (EQUAL X Z))
                   (EQUAL (EQUAL X Z) T)).

    This again simplifies, expanding EQUAL, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (NUMBERP Y))
                        (NUMBERP Z)
                        (EQUAL X Z))
                   (NOT (EQUAL Z 0))),

    which again simplifies, trivially, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (ZEROP Y))
                      (EQUAL (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                             (COND ((LESSP (SUB1 X) (SUB1 Y))
                                    (NOT (LESSP (SUB1 Y) (SUB1 Z))))
                                   ((LESSP (SUB1 Z) (SUB1 Y))
                                    (NOT (LESSP (SUB1 Y) (SUB1 X))))
                                   (T (EQUAL (FIX (SUB1 X))
                                             (FIX (SUB1 Z)))))))
                 (EQUAL (EQUAL (DIFFERENCE X Y)
                               (DIFFERENCE Z Y))
                        (COND ((LESSP X Y) (NOT (LESSP Y Z)))
                              ((LESSP Z Y) (NOT (LESSP Y X)))
                              (T (EQUAL (FIX X) (FIX Z)))))).

  This simplifies, unfolding the definitions of ZEROP, NOT, FIX, DIFFERENCE,
  and LESSP, to the following 18 new goals:

  Case 1.18.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (LESSP (SUB1 Z) (SUB1 Y))
                        (NOT (LESSP (SUB1 Y) (SUB1 X)))
                        (NOT (NUMBERP Z)))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 1.17.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (LESSP (SUB1 Z) (SUB1 Y))
                        (NOT (LESSP (SUB1 Y) (SUB1 X)))
                        (EQUAL Z 0))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.16.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (LESSP (SUB1 Y) (SUB1 Z)))
                        (NOT (NUMBERP Z)))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)),

    which again simplifies, applying EQUAL-DIFFERENCE-0, to:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (LESSP (SUB1 Y) (SUB1 Z)))
                        (NOT (NUMBERP Z)))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.15.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (LESSP (SUB1 Y) (SUB1 Z)))
                        (EQUAL Z 0))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)),

    which again simplifies, applying EQUAL-DIFFERENCE-0, and unfolding the
    functions SUB1, EQUAL, DIFFERENCE, and LESSP, to:

          T.

  Case 1.14.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (LESSP (SUB1 Z) (SUB1 Y))
                        (LESSP (SUB1 Y) (SUB1 X))
                        (NOT (NUMBERP Z)))
                   (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.13.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (LESSP (SUB1 Z) (SUB1 Y))
                        (LESSP (SUB1 Y) (SUB1 X))
                        (EQUAL Z 0))
                   (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.12.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (LESSP (SUB1 Y) (SUB1 Z))
                        (EQUAL Z 0))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)),

    which again simplifies, rewriting with EQUAL-DIFFERENCE-0, and expanding
    the definitions of SUB1, EQUAL, DIFFERENCE, and LESSP, to:

          T.

  Case 1.11.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (LESSP (SUB1 Y) (SUB1 Z))
                        (NOT (NUMBERP Z)))
                   (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                          0)).

    However this again simplifies, rewriting with EQUAL-DIFFERENCE-0, to the
    new conjecture:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (LESSP (SUB1 X) (SUB1 Y))
                        (LESSP (SUB1 Y) (SUB1 Z))
                        (NOT (NUMBERP Z)))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.10.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (NOT (EQUAL (SUB1 X) (SUB1 Z)))
                        (EQUAL Z 0)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    0)))
                   (LESSP (SUB1 Y) (SUB1 X))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.9.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (NOT (EQUAL (SUB1 X) (SUB1 Z)))
                        (EQUAL Z 0)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.8.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (NOT (EQUAL (SUB1 X) (SUB1 Z)))
                        (NOT (NUMBERP Z))
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    0)))
                   (LESSP (SUB1 Y) (SUB1 X))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.7.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (NOT (EQUAL (SUB1 X) (SUB1 Z)))
                        (NOT (NUMBERP Z))
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    (DIFFERENCE (SUB1 Z) (SUB1 Y))))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (NOT (EQUAL (SUB1 X) (SUB1 Z)))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z))
                   (NOT (EQUAL X Z))),

    which again simplifies, clearly, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (EQUAL (SUB1 X) (SUB1 Z)) T)
                        (EQUAL Z 0)
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    0)))
                   (LESSP (SUB1 Y) (SUB1 X))).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (EQUAL (SUB1 X) (SUB1 Z)) T)
                        (EQUAL Z 0)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (EQUAL (SUB1 X) (SUB1 Z)) T)
                        (NOT (NUMBERP Z))
                        (NOT (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                    0)))
                   (LESSP (SUB1 Y) (SUB1 X))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (EQUAL (SUB1 X) (SUB1 Z)) T)
                        (NOT (NUMBERP Z))
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0))
                   (NOT (LESSP (SUB1 Y) (SUB1 X)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (EQUAL (SUB1 X) (SUB1 Z)) T)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z))
                   (EQUAL (EQUAL X Z) T)),

    which again simplifies, obviously, to:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               (DIFFERENCE (SUB1 Z) (SUB1 Y)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (LESSP (SUB1 Z) (SUB1 Y)))
                        (EQUAL (SUB1 X) (SUB1 Z))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z))
                   (EQUAL X Z)),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.1 ]

DIFFERENCE-CANCELLATION


(TOGGLE DIFFERENCE-CANCELLATION-OFF DIFFERENCE-CANCELLATION T)

[ 0.0 0.0 0.0 ]

DIFFERENCE-CANCELLATION-OFF


(PROVE-LEMMA COMMUTATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X Y) (PLUS Y X))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This formula simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-PLUS


(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X Y Z) (PLUS Y X Z))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed COMMUTATIVITY2-OF-PLUS could!


This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY2-OF-PLUS


(PROVE-LEMMA PLUS-ZERO-ARG2
             (REWRITE)
             (IMPLIES (ZEROP Y)
                      (EQUAL (PLUS X Y) (FIX X)))
             ((INDUCT (PLUS X Y))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-ZERO-ARG2 could!


This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP X) (ZEROP Y))
                 (EQUAL (PLUS X Y) (FIX X))).

  This simplifies, expanding the functions ZEROP, PLUS, FIX, EQUAL, and
  NUMBERP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (IMPLIES (ZEROP Y)
                               (EQUAL (PLUS (SUB1 X) Y)
                                      (FIX (SUB1 X))))
                      (ZEROP Y))
                 (EQUAL (PLUS X Y) (FIX X))).

  This simplifies, applying the lemma ADD1-SUB1, and expanding ZEROP, FIX,
  IMPLIES, and PLUS, to:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (EQUAL (PLUS (SUB1 X) Y) (SUB1 X))
                      (EQUAL Y 0))
                 (EQUAL (ADD1 (PLUS (SUB1 X) 0)) X)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-ZERO-ARG2


(PROVE-LEMMA PLUS-ADD1-ARG1
             (REWRITE)
             (EQUAL (PLUS (ADD1 A) B)
                    (ADD1 (PLUS A B)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-ADD1-ARG1 could!


This conjecture simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-ADD1-ARG1


(PROVE-LEMMA PLUS-ADD1-ARG2
             (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X)))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-ADD1-ARG2 could!


This simplifies, obviously, to two new formulas:

Case 2. (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (PLUS X (ADD1 Y)) (ADD1 X))),

  which again simplifies, rewriting with the lemma SUB1-TYPE-RESTRICTION, to
  the conjecture:

        (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (PLUS X 1) (ADD1 X))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (NUMBERP Y)
                 (EQUAL (PLUS X (ADD1 Y))
                        (ADD1 (PLUS X Y)))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-ADD1-ARG2


(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS (PLUS X Y) Z)
                    (PLUS X Y Z))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed ASSOCIATIVITY-OF-PLUS could!


This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOCIATIVITY-OF-PLUS


(PROVE-LEMMA PLUS-DIFFERENCE-ARG1
             (REWRITE)
             (EQUAL (PLUS (DIFFERENCE A B) C)
                    (IF (LESSP B A)
                        (DIFFERENCE (PLUS A C) B)
                        (PLUS 0 C)))
             ((INDUCT (DIFFERENCE A B))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-DIFFERENCE-ARG1 could!


This conjecture can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to three new formulas:

Case 3. (IMPLIES (ZEROP A)
                 (EQUAL (PLUS (DIFFERENCE A B) C)
                        (IF (LESSP B A)
                            (DIFFERENCE (PLUS A C) B)
                            (PLUS 0 C)))),

  which simplifies, unfolding the functions ZEROP, EQUAL, DIFFERENCE, PLUS,
  and LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (ZEROP B))
                 (EQUAL (PLUS (DIFFERENCE A B) C)
                        (IF (LESSP B A)
                            (DIFFERENCE (PLUS A C) B)
                            (PLUS 0 C)))),

  which simplifies, unfolding the definitions of ZEROP, EQUAL, DIFFERENCE, and
  LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (EQUAL (PLUS (DIFFERENCE (SUB1 A) (SUB1 B))
                                   C)
                             (IF (LESSP (SUB1 B) (SUB1 A))
                                 (DIFFERENCE (PLUS (SUB1 A) C)
                                             (SUB1 B))
                                 (PLUS 0 C))))
                 (EQUAL (PLUS (DIFFERENCE A B) C)
                        (IF (LESSP B A)
                            (DIFFERENCE (PLUS A C) B)
                            (PLUS 0 C)))),

  which simplifies, rewriting with SUB1-ADD1, and unfolding the functions
  EQUAL, PLUS, DIFFERENCE, and LESSP, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-DIFFERENCE-ARG1


(PROVE-LEMMA PLUS-DIFFERENCE-ARG2
             (REWRITE)
             (EQUAL (PLUS A (DIFFERENCE B C))
                    (IF (LESSP C B)
                        (DIFFERENCE (PLUS A B) C)
                        (PLUS A 0)))
             ((INDUCT (PLUS A B))
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-DIFFERENCE-ARG2 could!


This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new formulas:

Case 2. (IMPLIES (ZEROP A)
                 (EQUAL (PLUS A (DIFFERENCE B C))
                        (IF (LESSP C B)
                            (DIFFERENCE (PLUS A B) C)
                            (PLUS A 0)))).

  This simplifies, expanding ZEROP, EQUAL, PLUS, and NUMBERP, to the following
  four new formulas:

  Case 2.4.
          (IMPLIES (AND (EQUAL A 0) (NOT (LESSP C B)))
                   (EQUAL (DIFFERENCE B C) 0)).

    This again simplifies, trivially, to the new formula:

          (IMPLIES (NOT (LESSP C B))
                   (EQUAL (DIFFERENCE B C) 0)),

    which we will name *1.

  Case 2.3.
          (IMPLIES (AND (EQUAL A 0)
                        (LESSP C B)
                        (NOT (NUMBERP B)))
                   (EQUAL (DIFFERENCE B C)
                          (DIFFERENCE 0 C))).

    However this again simplifies, opening up LESSP, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (NOT (LESSP C B)))
                   (EQUAL (DIFFERENCE B C) 0)),

    which we will name *2.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (LESSP C B)
                        (NOT (NUMBERP B)))
                   (EQUAL (DIFFERENCE B C)
                          (DIFFERENCE 0 C))).

    This again simplifies, expanding the definition of LESSP, to:

          T.

Case 1. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                             (IF (LESSP C B)
                                 (DIFFERENCE (PLUS (SUB1 A) B) C)
                                 (PLUS (SUB1 A) 0))))
                 (EQUAL (PLUS A (DIFFERENCE B C))
                        (IF (LESSP C B)
                            (DIFFERENCE (PLUS A B) C)
                            (PLUS A 0)))),

  which simplifies, rewriting with SUB1-ADD1, and unfolding the definitions of
  PLUS and DIFFERENCE, to the following three new goals:

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (LESSP C B)
                        (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                               (DIFFERENCE (PLUS (SUB1 A) B) C))
                        (NOT (EQUAL C 0))
                        (NUMBERP C))
                   (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) C))
                          (DIFFERENCE (PLUS (SUB1 A) B)
                                      (SUB1 C)))).

    But this again simplifies, using linear arithmetic, to two new formulas:

    Case 1.3.2.
            (IMPLIES (AND (LESSP (PLUS (SUB1 A) B) C)
                          (NOT (EQUAL A 0))
                          (NUMBERP A)
                          (LESSP C B)
                          (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                                 (DIFFERENCE (PLUS (SUB1 A) B) C))
                          (NOT (EQUAL C 0))
                          (NUMBERP C))
                     (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) C))
                            (DIFFERENCE (PLUS (SUB1 A) B)
                                        (SUB1 C)))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 1.3.1.
            (IMPLIES (AND (LESSP (PLUS (SUB1 A) B) (SUB1 C))
                          (NOT (EQUAL A 0))
                          (NUMBERP A)
                          (LESSP C B)
                          (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                                 (DIFFERENCE (PLUS (SUB1 A) B) C))
                          (NOT (EQUAL C 0))
                          (NUMBERP C))
                     (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) C))
                            (DIFFERENCE (PLUS (SUB1 A) B)
                                        (SUB1 C)))),

      which again simplifies, using linear arithmetic, to:

            T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (LESSP C B)
                        (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                               (DIFFERENCE (PLUS (SUB1 A) B) C))
                        (EQUAL C 0))
                   (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) C))
                          (ADD1 (PLUS (SUB1 A) B)))),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (LESSP (PLUS (SUB1 A) B) 0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (LESSP 0 B)
                        (EQUAL (PLUS (SUB1 A) (DIFFERENCE B 0))
                               (DIFFERENCE (PLUS (SUB1 A) B) 0)))
                   (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) 0))
                          (ADD1 (PLUS (SUB1 A) B)))).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (LESSP C B)
                        (EQUAL (PLUS (SUB1 A) (DIFFERENCE B C))
                               (DIFFERENCE (PLUS (SUB1 A) B) C))
                        (NOT (NUMBERP C)))
                   (EQUAL (ADD1 (DIFFERENCE (PLUS (SUB1 A) B) C))
                          (ADD1 (PLUS (SUB1 A) B)))),

    which again simplifies, applying ADD1-EQUAL, and unfolding the functions
    LESSP and DIFFERENCE, to:

          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (NOT (NUMBERP C))
                        (EQUAL (PLUS (SUB1 A) B) 0))
                   (EQUAL 0 (PLUS (SUB1 A) B))),

    which again simplifies, clearly, to:

          T.


     So we now return to:

      (IMPLIES (AND (NOT (NUMBERP A))
                    (NOT (LESSP C B)))
               (EQUAL (DIFFERENCE B C) 0)),

named *2 above.  What luck!  This conjecture is subsumed by formula *1 above.


     So next consider:

      (IMPLIES (NOT (LESSP C B))
               (EQUAL (DIFFERENCE B C) 0)),

which is formula *1 above.  Perhaps we can prove it by induction.  Four
inductions are suggested by terms in the conjecture.  However, they merge into
one likely candidate induction.  We will induct according to the following
scheme:
      (AND (IMPLIES (OR (EQUAL B 0) (NOT (NUMBERP B)))
                    (p B C))
           (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                         (OR (EQUAL C 0) (NOT (NUMBERP C))))
                    (p B C))
           (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                         (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                         (p (SUB1 B) (SUB1 C)))
                    (p B C))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT C) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for B.  The above induction scheme
leads to the following four new conjectures:

Case 4. (IMPLIES (AND (OR (EQUAL B 0) (NOT (NUMBERP B)))
                      (NOT (LESSP C B)))
                 (EQUAL (DIFFERENCE B C) 0)).

  This simplifies, unfolding the definitions of NOT, OR, EQUAL, LESSP, and
  DIFFERENCE, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                      (OR (EQUAL C 0) (NOT (NUMBERP C)))
                      (NOT (LESSP C B)))
                 (EQUAL (DIFFERENCE B C) 0)).

  This simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                      (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (LESSP (SUB1 C) (SUB1 B))
                      (NOT (LESSP C B)))
                 (EQUAL (DIFFERENCE B C) 0)).

  This simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP B 1)
                      (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                      (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (LESSP (SUB1 C) (SUB1 B))
                      (NOT (LESSP C B)))
                 (EQUAL (DIFFERENCE B C) 0)),

  which again simplifies, expanding the functions SUB1, NUMBERP, EQUAL, LESSP,
  NOT, and OR, to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                      (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                             0)
                      (NOT (LESSP C B)))
                 (EQUAL (DIFFERENCE B C) 0)),

  which simplifies, using linear arithmetic, to three new formulas:

  Case 1.3.
          (IMPLIES (AND (LESSP B C)
                        (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                        (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                        (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                               0)
                        (NOT (LESSP C B)))
                   (EQUAL (DIFFERENCE B C) 0)),

    which again simplifies, using linear arithmetic, to two new formulas:

    Case 1.3.2.
            (IMPLIES (AND (LESSP (SUB1 B) (SUB1 C))
                          (LESSP B C)
                          (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                          (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                          (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                                 0)
                          (NOT (LESSP C B)))
                     (EQUAL (DIFFERENCE B C) 0)),

      which again simplifies, opening up the functions LESSP, NOT, OR,
      DIFFERENCE, and EQUAL, to:

            T.

    Case 1.3.1.
            (IMPLIES (AND (LESSP B 1)
                          (LESSP B C)
                          (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                          (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                          (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                                 0)
                          (NOT (LESSP C B)))
                     (EQUAL (DIFFERENCE B C) 0)),

      which again simplifies, expanding the definitions of SUB1, NUMBERP,
      EQUAL, LESSP, NOT, and OR, to:

            T.

  Case 1.2.
          (IMPLIES (AND (LESSP (SUB1 B) (SUB1 C))
                        (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                        (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                        (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                               0)
                        (NOT (LESSP C B)))
                   (EQUAL (DIFFERENCE B C) 0)),

    which again simplifies, opening up the functions NOT, OR, LESSP,
    DIFFERENCE, and EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LESSP B 1)
                        (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
                        (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                        (EQUAL (DIFFERENCE (SUB1 B) (SUB1 C))
                               0)
                        (NOT (LESSP C B)))
                   (EQUAL (DIFFERENCE B C) 0)),

    which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR,
    to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-DIFFERENCE-ARG2


(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION-PROOF NIL
             (EQUAL (DIFFERENCE (PLUS X Y) X)
                    (FIX Y))
             ((ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

This conjecture simplifies, opening up the function FIX, to the following two
new goals:

Case 2. (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (DIFFERENCE (PLUS X Y) X) 0)).

  Give the above formula the name *1.

Case 1. (IMPLIES (NUMBERP Y)
                 (EQUAL (DIFFERENCE (PLUS X Y) X) Y)).

  This again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP (PLUS X Y) X) (NUMBERP Y))
                 (EQUAL (DIFFERENCE (PLUS X Y) X) Y)).

  However this again simplifies, using linear arithmetic, to:

        T.


     So we now return to:

      (IMPLIES (NOT (NUMBERP Y))
               (EQUAL (DIFFERENCE (PLUS X Y) X) 0)),

which we named *1 above.  Let us appeal to the induction principle.  There are
two plausible inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP (PLUS X Y)) (p X Y))
           (IMPLIES (AND (NOT (ZEROP (PLUS X Y)))