(BOOT-STRAP NQTHM)

[ 0.0 0.1 0.0 ]

GROUND-ZERO


(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading tmp.o
Finished loading tmp.o

/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp


(DEFN FROM-TO
      (I J)
      (IF (LESSP J I)
          NIL
          (IF (EQUAL (FIX I) (FIX J))
              (LIST (FIX J))
              (APPEND (FROM-TO I (SUB1 J))
                      (LIST J)))))

     Linear arithmetic, the lemmas COUNT-NUMBERP, SUB1-NNUMBERP, and
COUNT-NOT-LESSP, and the definitions of LESSP, EQUAL, COUNT, and FIX establish
that the measure (COUNT J) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, FROM-TO is accepted under the
definitional principle.  Note that:
      (OR (LITATOM (FROM-TO I J))
          (LISTP (FROM-TO I J)))
is a theorem.




[ 0.0 0.0 0.0 ]

FROM-TO


(PROVE-LEMMA PLUS-RIGHT-ID2
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (PLUS X Y) (FIX X))))

This simplifies, unfolding the definition of FIX, to the following two new
goals:

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

  This again simplifies, opening up the definitions of PLUS and EQUAL, to:

        T.

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

  which we will name *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates the following two new formulas:

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

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

        T.

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

  This simplifies, using linear arithmetic, to the new conjecture:

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

  which again simplifies, expanding the function ZEROP, to:

        T.


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


[ 0.0 0.0 0.0 ]

PLUS-RIGHT-ID2


(PROVE-LEMMA PLUS-ADD1
             (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X))))

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


(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X (PLUS Y Z))
                    (PLUS Y (PLUS X Z))))

This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY2-OF-PLUS


(PROVE-LEMMA COMMUTATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X Y) (PLUS Y X)))

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




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




WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the previously added lemma PLUS-RIGHT-ID2 could.




This formula simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-PLUS


(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS (PLUS X Y) Z)
                    (PLUS X (PLUS Y Z))))

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-EQUAL-0
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) 0)
                    (AND (ZEROP A) (ZEROP B))))

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, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and unfolding the functions NUMBERP and EQUAL, to:

        T.

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

  However this again simplifies, applying PLUS-RIGHT-ID2, and unfolding the
  function EQUAL, to:

        T.

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

  This 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, applying the lemma PLUS-RIGHT-ID2, and opening up
  the definitions of NUMBERP and EQUAL, 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 ]

PLUS-EQUAL-0


(PROVE-LEMMA DIFFERENCE-X-X
             (REWRITE)
             (EQUAL (DIFFERENCE X X) 0))

This conjecture simplifies, using linear arithmetic, to:

      (IMPLIES (LESSP X X)
               (EQUAL (DIFFERENCE X X) 0)).

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-X-X


(PROVE-LEMMA DIFFERENCE-PLUS
             (REWRITE)
             (AND (EQUAL (DIFFERENCE (PLUS X Y) X)
                         (FIX Y))
                  (EQUAL (DIFFERENCE (PLUS Y X) X)
                         (FIX Y))))

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


This formula can be simplified, using the abbreviation AND, to the following
two new conjectures:

Case 2. (EQUAL (DIFFERENCE (PLUS X Y) X)
               (FIX Y)).

  This simplifies, unfolding the function FIX, to the following two new
  formulas:

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

    However this again simplifies, applying PLUS-RIGHT-ID2, to the following
    two new goals:

    Case 2.2.2.
            (IMPLIES (AND (NOT (NUMBERP Y))
                          (NOT (NUMBERP X)))
                     (EQUAL (DIFFERENCE 0 X) 0)).

      But this again simplifies, expanding EQUAL and DIFFERENCE, to:

            T.

    Case 2.2.1.
            (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)),

      which again simplifies, using linear arithmetic, to:

            (IMPLIES (AND (LESSP X X)
                          (NOT (NUMBERP Y))
                          (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)).

      However this again simplifies, using linear arithmetic, to:

            T.

  Case 2.1.
          (IMPLIES (NUMBERP Y)
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)),

    which again simplifies, using linear arithmetic, to the conjecture:

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

    This again simplifies, using linear arithmetic, to:

          T.

Case 1. (EQUAL (DIFFERENCE (PLUS Y X) X)
               (FIX Y)),

  which simplifies, applying the lemma COMMUTATIVITY-OF-PLUS, and unfolding
  FIX, to two new conjectures:

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

    which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, to two
    new formulas:

    Case 1.2.2.
            (IMPLIES (AND (NOT (NUMBERP Y))
                          (NOT (NUMBERP X)))
                     (EQUAL (DIFFERENCE 0 X) 0)),

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

            T.

    Case 1.2.1.
            (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)),

      which again simplifies, using linear arithmetic, to:

            (IMPLIES (AND (LESSP X X)
                          (NOT (NUMBERP Y))
                          (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)).

      However this again simplifies, using linear arithmetic, to:

            T.

  Case 1.1.
          (IMPLIES (NUMBERP Y)
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)),

    which again simplifies, using linear arithmetic, to the formula:

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

    This again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS


(PROVE-LEMMA PLUS-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                    (EQUAL (FIX B) (FIX C))))

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 again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two
  new conjectures:

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

    This again simplifies, using linear arithmetic, to:

          T.

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

    which again simplifies, using linear arithmetic, to:

          T.

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

  which again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two
  new goals:

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

    This again simplifies, using linear arithmetic, to:

          T.

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

    which again simplifies, using linear arithmetic, to:

          T.

Case 4. (IMPLIES (AND (NOT (NUMBERP C))
                      (NOT (NUMBERP B)))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)),

  which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, and opening
  up EQUAL, to:

        T.

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

  which again simplifies, rewriting with COMMUTATIVITY-OF-PLUS and
  PLUS-RIGHT-ID2, and expanding the functions EQUAL and PLUS, to:

        T.

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

  This again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and opening up EQUAL and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP C)
                      (NUMBERP B)
                      (EQUAL B C))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)).

  But this again simplifies, expanding the function EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-CANCELLATION


(PROVE-LEMMA DIFFERENCE-0
             (REWRITE)
             (IMPLIES (NOT (LESSP Y X))
                      (EQUAL (DIFFERENCE X Y) 0)))


     Name the conjecture *1.


     Let us appeal to the induction principle.  The recursive terms in the
conjecture suggest four inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X)))
                    (p X Y))
           (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                         (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                    (p X Y))
           (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                         (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                         (p (SUB1 X) (SUB1 Y)))
                    (p X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to show that the measure (COUNT Y) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  Note, however, the inductive instance chosen for X.  The above
induction scheme leads to the following four new goals:

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

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

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)).

  This simplifies, unfolding NOT, OR, EQUAL, and LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                      (LESSP (SUB1 Y) (SUB1 X))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)).

  This simplifies, using linear arithmetic, to:

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

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

        T.

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

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

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

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

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

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

            T.

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

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

            T.

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

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

          T.

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

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

          T.


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


[ 0.0 0.0 0.0 ]

DIFFERENCE-0


(PROVE-LEMMA EQUAL-DIFFERENCE-0
             (REWRITE)
             (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                    (NOT (LESSP Y X))))

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

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

  which again simplifies, rewriting with the lemma DIFFERENCE-0, and opening
  up the definition of EQUAL, to:

        T.

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

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-DIFFERENCE-0


(PROVE-LEMMA DIFFERENCE-CANCELLATION-0
             (REWRITE)
             (EQUAL (EQUAL X (DIFFERENCE X Y))
                    (AND (NUMBERP X)
                         (OR (EQUAL X 0) (ZEROP Y)))))

This simplifies, opening up the functions ZEROP, OR, and AND, to five new
goals:

Case 5. (IMPLIES (EQUAL X (DIFFERENCE X Y))
                 (NUMBERP X)),

  which again simplifies, obviously, to:

        T.

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

  But this again simplifies, using linear arithmetic, to the conjecture:

        (IMPLIES (AND (LESSP X Y)
                      (EQUAL X (DIFFERENCE X Y))
                      (NOT (EQUAL X 0))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))).

  This again simplifies, using linear arithmetic and applying DIFFERENCE-0, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y)))
                      (NUMBERP X))
                 (NUMBERP Y)).

  But this again simplifies, expanding the definition of DIFFERENCE, to:

        T.

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

  which again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP X 0)
                      (NOT (EQUAL X (DIFFERENCE X 0))))
                 (NOT (NUMBERP X))).

  But this again simplifies, using linear arithmetic, to:

        T.

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

  which again simplifies, using linear arithmetic, applying the lemma
  DIFFERENCE-0, and expanding EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-CANCELLATION-0


(PROVE-LEMMA DIFFERENCE-CANCELLATION-1
             (REWRITE)
             (EQUAL (EQUAL (DIFFERENCE X Y)
                           (DIFFERENCE Z Y))
                    (IF (LESSP X Y)
                        (NOT (LESSP Y Z))
                        (IF (LESSP Z Y)
                            (NOT (LESSP Y X))
                            (EQUAL (FIX X) (FIX Z))))))

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, using linear arithmetic, applying DIFFERENCE-0 and
  EQUAL-DIFFERENCE-0, and expanding 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, using linear arithmetic, rewriting with DIFFERENCE-0
  and EQUAL-DIFFERENCE-0, and opening up the functions 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, using linear arithmetic, appealing to the lemma
  DIFFERENCE-0, and unfolding the function EQUAL, 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, using linear arithmetic, applying DIFFERENCE-0, and
  unfolding the function 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))).

  This again simplifies, clearly, to:

        T.

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

  However this again simplifies, using linear arithmetic, applying
  DIFFERENCE-0, and expanding the function EQUAL, to:

        T.

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)).

  However this again simplifies, using linear arithmetic, applying
  DIFFERENCE-0, and unfolding the definition of 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)).

  But this again simplifies, using linear arithmetic, to three new goals:

  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, appealing to the lemma DIFFERENCE-0, and expanding
    the definitions of 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, using linear arithmetic, applying DIFFERENCE-0,
    and unfolding the function 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)).

    However this again simplifies, using linear arithmetic, applying
    DIFFERENCE-0, and expanding the function EQUAL, to:

          T.

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

  However this again simplifies, using linear arithmetic and rewriting with
  the lemmas DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to:

        T.

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

  which again simplifies, using linear arithmetic and rewriting with
  DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-CANCELLATION-1


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

     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, DELETE is accepted under the principle of definition.




[ 0.0 0.0 0.0 ]

DELETE


(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


(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


(PROVE-LEMMA DELETE-NON-MEMBER
             (REWRITE)
             (IMPLIES (NOT (MEMBER X Y))
                      (EQUAL (DELETE X Y) Y)))


     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 MEMBER-DELETE
             (REWRITE)
             (IMPLIES (MEMBER X (DELETE U V))
                      (MEMBER X V)))

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



     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 V) (EQUAL U (CAR V)))
                    (p X V U))
           (IMPLIES (AND (LISTP V)
                         (NOT (EQUAL U (CAR V)))
                         (p X (CDR V) U))
                    (p X V U))
           (IMPLIES (NOT (LISTP V)) (p X V U))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT V)
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 V)
                      (EQUAL U (CAR V))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

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

        T.

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

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

        T.

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

  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 V))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

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

        T.


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


[ 0.0 0.0 0.0 ]

MEMBER-DELETE


(PROVE-LEMMA COMMUTATIVITY-OF-DELETE
             (REWRITE)
             (EQUAL (DELETE X (DELETE Y Z))
                    (DELETE Y (DELETE X Z))))


     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 Y (CAR Z)))
                    (p X Y Z))
           (IMPLIES (AND (LISTP Z)
                         (NOT (EQUAL Y (CAR Z)))
                         (p X Y (CDR Z)))
                    (p X Y Z))
           (IMPLIES (NOT (LISTP Z)) (p X Y 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 Y (CAR Z)))
                 (EQUAL (DELETE X (DELETE Y Z))
                        (DELETE Y (DELETE X Z)))),

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

  Case 3.2.
          (IMPLIES (AND (LISTP Z)
                        (NOT (EQUAL X (CAR Z))))
                   (EQUAL (DELETE X (CDR Z))
                          (DELETE (CAR Z)
                                  (CONS (CAR Z) (DELETE X (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 X (CAR Z)))
                   (EQUAL (DELETE X (CDR Z))
                          (DELETE (CAR Z) (CDR Z)))).

    This again simplifies, obviously, to:

          T.

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

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

        (IMPLIES (AND (LISTP Z)
                      (NOT (EQUAL Y (CAR Z)))
                      (EQUAL (DELETE X (DELETE Y (CDR Z)))
                             (DELETE Y (DELETE X (CDR Z))))
                      (NOT (EQUAL X (CAR Z))))
                 (EQUAL (CONS (CAR Z)
                              (DELETE X (DELETE Y (CDR Z))))
                        (DELETE Y
                                (CONS (CAR Z) (DELETE X (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 X (DELETE Y Z))
                        (DELETE Y (DELETE X 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 ]

COMMUTATIVITY-OF-DELETE


(PROVE-LEMMA SUBBAGP-DELETE
             (REWRITE)
             (IMPLIES (SUBBAGP X (DELETE U Y))
                      (SUBBAGP X Y)))

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 COMMUTATIVITY-OF-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 COMMUTATIVITY-OF-DELETE and
  MEMBER-DELETE, 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)))

.

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)))

.

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.1 0.0 ]

SUBBAGP-CDR2


(PROVE-LEMMA SUBBAGP-BAGINT1
             (REWRITE)
             (SUBBAGP (BAGINT X Y) X))


     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 CDR-NLISTP and SUBBAGP-CDR2, and
  unfolding BAGINT 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))


     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


(DEFN PLUS-FRINGE
      (X)
      (IF (AND (LISTP X) (EQUAL (CAR X) 'PLUS))
          (APPEND (PLUS-FRINGE (CADR X))
                  (PLUS-FRINGE (CADDR X)))
          (CONS X NIL)))

     Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, and CDR-LESSP,
and the definition of AND establish that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
PLUS-FRINGE is accepted under the principle of definition.  Note that
(LISTP (PLUS-FRINGE X)) is a theorem.




[ 0.0 0.0 0.0 ]

PLUS-FRINGE


(DEFN PLUS-TREE
      (L)
      (IF (NLISTP L)
          ''0
          (IF (NLISTP (CDR L))
              (LIST 'FIX (CAR L))
              (IF (NLISTP (CDDR L))
                  (LIST 'PLUS (CAR L) (CADR L))
                  (LIST 'PLUS
                        (CAR L)
                        (PLUS-TREE (CDR L)))))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, PLUS-TREE
is accepted under the principle of definition.  Note that
(LISTP (PLUS-TREE L)) is a theorem.




[ 0.0 0.0 0.0 ]

PLUS-TREE


(DEFN CANCEL
      (X)
      (IF (AND (LISTP X)
               (EQUAL (CAR X) 'EQUAL))
          (IF (AND (LISTP (CADR X))
                   (EQUAL (CAADR X) 'PLUS)
                   (LISTP (CADDR X))
                   (EQUAL (CAADDR X) 'PLUS))
              (LIST 'EQUAL
                    (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADR X))
                                        (BAGINT (PLUS-FRINGE (CADR X))
                                                (PLUS-FRINGE (CADDR X)))))
                    (PLUS-TREE (BAGDIFF (PLUS-FRINGE (CADDR X))
                                        (BAGINT (PLUS-FRINGE (CADR X))
                                                (PLUS-FRINGE (CADDR X))))))
              (IF (AND (LISTP (CADR X))
                       (EQUAL (CAADR X) 'PLUS)
                       (MEMBER (CADDR X)
                               (PLUS-FRINGE (CADR X))))
                  (LIST 'IF
                        (LIST 'NUMBERP (CADDR X))
                        (LIST 'EQUAL
                              (PLUS-TREE (DELETE (CADDR X)
                                                 (PLUS-FRINGE (CADR X))))
                              ''0)
                        (LIST 'QUOTE F))
                  (IF (AND (LISTP (CADDR X))
                           (EQUAL (CAADDR X) 'PLUS)
                           (MEMBER (CADR X)
                                   (PLUS-FRINGE (CADDR X))))
                      (LIST 'IF
                            (LIST 'NUMBERP (CADR X))
                            (LIST 'EQUAL
                                  ''0
                                  (PLUS-TREE (DELETE (CADR X)
                                                     (PLUS-FRINGE (CADDR X)))))
                            (LIST 'QUOTE F))
                      X)))
          X))

     From the definition we can conclude that:
      (OR (LISTP (CANCEL X))
          (EQUAL (CANCEL X) X))
is a theorem.




[ 0.0 0.0 0.0 ]

CANCEL


(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading tmp.o
Finished loading tmp.o

/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp


(PROVE-LEMMA NUMBERP-EVAL$-PLUS
             (REWRITE)
             (IMPLIES (AND (LISTP X) (EQUAL (CAR X) 'PLUS))
                      (NUMBERP (EVAL$ T X A))))

.

Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate (CAR X)
and (CDR X).  This produces:

      (IMPLIES (EQUAL Z 'PLUS)
               (NUMBERP (EVAL$ T (CONS Z V) A))),

which simplifies, applying REWRITE-EVAL$, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NUMBERP-EVAL$-PLUS


(PROVE-LEMMA NUMBERP-EVAL$-PLUS-TREE
             (REWRITE)
             (NUMBERP (EVAL$ T (PLUS-TREE L) A)))


     Call the conjecture *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 (NLISTP L) (p L A))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NLISTP (CDR L)))
                    (p L A))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NOT (NLISTP (CDR L)))
                         (NLISTP (CDDR L)))
                    (p L A))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NOT (NLISTP (CDR L)))
                         (NOT (NLISTP (CDDR L)))
                         (p (CDR L) A))
                    (p L A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to 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 the following four new formulas:

Case 4. (IMPLIES (NLISTP L)
                 (NUMBERP (EVAL$ T (PLUS-TREE L) A))).

  This simplifies, expanding the definitions of NLISTP, PLUS-TREE, CDR, CAR,
  LISTP, LITATOM, EQUAL, EVAL$, and NUMBERP, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NLISTP (CDR L)))
                 (NUMBERP (EVAL$ T (PLUS-TREE L) A))).

  This simplifies, appealing to the lemmas REWRITE-EVAL$ and CAR-CONS, and
  opening up NLISTP, PLUS-TREE, and FIX, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (NLISTP (CDR L)))
                      (NLISTP (CDDR L)))
                 (NUMBERP (EVAL$ T (PLUS-TREE L) A))).

  This simplifies, rewriting with REWRITE-EVAL$, CAR-CONS, and CDR-CONS, and
  unfolding the definitions of NLISTP and PLUS-TREE, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (NLISTP (CDR L)))
                      (NOT (NLISTP (CDDR L)))
                      (NUMBERP (EVAL$ T (PLUS-TREE (CDR L)) A)))
                 (NUMBERP (EVAL$ T (PLUS-TREE L) A))),

  which simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, and
  expanding the functions NLISTP and PLUS-TREE, to:

        T.


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


[ 0.0 0.0 0.0 ]

NUMBERP-EVAL$-PLUS-TREE


(PROVE-LEMMA MEMBER-IMPLIES-PLUS-TREE-GREATEREQP
             (REWRITE)
             (IMPLIES (MEMBER X Y)
                      (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A)
                                  (EVAL$ T X A)))))

WARNING:  When the linear lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP is stored
under (EVAL$ T (PLUS-TREE Y) A) it contains the free variable X which will be
chosen by instantiating the hypothesis (MEMBER X Y).


WARNING:  When the linear lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP is stored
under (EVAL$ T X A) it contains the free variable Y which will be chosen by
instantiating the hypothesis (MEMBER X Y).


WARNING:  Note that the proposed lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP is
to be stored as zero type prescription rules, zero compound recognizer rules,
two linear rules, and zero replacement rules.



     Give the conjecture the name *1.


     We will appeal to 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 (NLISTP Y) (p Y A X))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (EQUAL X (CAR Y)))
                    (p Y A X))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (NOT (EQUAL X (CAR Y)))
                         (p (CDR Y) A X))
                    (p Y A X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT Y) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to four new goals:

Case 4. (IMPLIES (AND (NLISTP Y) (MEMBER X Y))
                 (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A)
                             (EVAL$ T X A)))),

  which simplifies, unfolding the functions NLISTP and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP Y))
                      (EQUAL X (CAR Y))
                      (MEMBER X Y))
                 (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A)
                             (EVAL$ T X A)))),

  which simplifies, opening up NLISTP, MEMBER, and PLUS-TREE, to three new
  formulas:

  Case 3.3.
          (IMPLIES (AND (LISTP Y) (NOT (LISTP (CDR Y))))
                   (NOT (LESSP (EVAL$ T (LIST 'FIX (CAR Y)) A)
                               (EVAL$ T (CAR Y) A)))),

    which again simplifies, rewriting with the lemmas REWRITE-EVAL$ and
    CAR-CONS, and expanding FIX, to two new goals:

    Case 3.3.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (NOT (LESSP 0 (EVAL$ T (CAR Y) A)))),

      which again simplifies, opening up the function LESSP, to:

            T.

    Case 3.3.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (NOT (LESSP (EVAL$ T (CAR Y) A)
                                 (EVAL$ T (CAR Y) A)))),

      which again simplifies, using linear arithmetic, to:

            T.

  Case 3.2.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y)))
                   (NOT (LESSP (EVAL$ T
                                      (LIST 'PLUS
                                            (CAR Y)
                                            (PLUS-TREE (CDR Y)))
                                      A)
                               (EVAL$ T (CAR Y) A)))),

    which again simplifies, rewriting with REWRITE-EVAL$, CAR-CONS, and
    CDR-CONS, to the new conjecture:

          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y)))
                   (NOT (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                     (EVAL$ T (PLUS-TREE (CDR Y)) A))
                               (EVAL$ T (CAR Y) A)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y))))
                   (NOT (LESSP (EVAL$ T
                                      (LIST 'PLUS (CAR Y) (CADR Y))
                                      A)
                               (EVAL$ T (CAR Y) A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, to:

          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y))))
                   (NOT (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                     (EVAL$ T (CADR Y) A))
                               (EVAL$ T (CAR Y) A)))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 2. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (NOT (MEMBER X (CDR Y)))
                      (MEMBER X Y))
                 (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A)
                             (EVAL$ T X A)))),

  which simplifies, unfolding the functions NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A)))
                      (MEMBER X Y))
                 (NOT (LESSP (EVAL$ T (PLUS-TREE Y) A)
                             (EVAL$ T X A)))),

  which simplifies, opening up NLISTP, MEMBER, and PLUS-TREE, to three new
  formulas:

  Case 1.3.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                    (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (NOT (LISTP (CDR Y))))
                   (NOT (LESSP (EVAL$ T (LIST 'FIX (CAR Y)) A)
                               (EVAL$ T X A)))),

    which again simplifies, applying the lemmas REWRITE-EVAL$ and CAR-CONS,
    and opening up the definition of FIX, to two new conjectures:

    Case 1.3.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                      (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (NOT (LESSP 0 (EVAL$ T X A)))),

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

            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                      (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A)))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))).

      This further simplifies, expanding the definitions of PLUS-TREE, CDR,
      CAR, LISTP, LITATOM, EQUAL, EVAL$, and LESSP, to:

            T.

    Case 1.3.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                      (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (NOT (LESSP (EVAL$ T (CAR Y) A)
                                 (EVAL$ T X A)))),

      which further simplifies, expanding PLUS-TREE, CDR, CAR, LISTP, LITATOM,
      EQUAL, EVAL$, LESSP, and MEMBER, to:

            T.

  Case 1.2.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                    (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y)))
                   (NOT (LESSP (EVAL$ T
                                      (LIST 'PLUS
                                            (CAR Y)
                                            (PLUS-TREE (CDR Y)))
                                      A)
                               (EVAL$ T X A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, to:

          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                    (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y)))
                   (NOT (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                     (EVAL$ T (PLUS-TREE (CDR Y)) A))
                               (EVAL$ T X A)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                    (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y))))
                   (NOT (LESSP (EVAL$ T
                                      (LIST 'PLUS (CAR Y) (CADR Y))
                                      A)
                               (EVAL$ T X A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, to
    the new conjecture:

          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                    (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y))))
                   (NOT (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                     (EVAL$ T (CADR Y) A))
                               (EVAL$ T X A)))),

    which further simplifies, rewriting with the lemmas REWRITE-EVAL$,
    CAR-CONS, and PLUS-RIGHT-ID2, and opening up the functions PLUS-TREE and
    FIX, to two new conjectures:

    Case 1.1.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (NUMBERP (EVAL$ T (CADR Y) A)))
                          (NOT (LESSP 0 (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y)))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (NOT (LESSP (EVAL$ T (CAR Y) A)
                                 (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 1.1.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NUMBERP (EVAL$ T (CADR Y) A))
                          (NOT (LESSP (EVAL$ T (CADR Y) A)
                                      (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y))))
                     (NOT (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                       (EVAL$ T (CADR Y) A))
                                 (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic, to:

            T.


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


[ 0.0 0.1 0.0 ]

MEMBER-IMPLIES-PLUS-TREE-GREATEREQP


(PROVE-LEMMA PLUS-TREE-DELETE
             (REWRITE)
             (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                    (IF (MEMBER X Y)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A))
                        (EVAL$ T (PLUS-TREE Y) A))))

This simplifies, clearly, to the following two new formulas:

Case 2. (IMPLIES (NOT (MEMBER X Y))
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (EVAL$ T (PLUS-TREE Y) A))).

  But this again simplifies, rewriting with DELETE-NON-MEMBER, to:

        T.

Case 1. (IMPLIES (MEMBER X Y)
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A)))).

  Name the above subgoal *1.


     We will appeal to induction.  There are four plausible inductions.  They
merge into two likely candidate inductions.  However, only one is unflawed.
We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP Y) (p X Y A))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (EQUAL X (CAR Y)))
                    (p X Y A))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (NOT (EQUAL X (CAR Y)))
                         (p X (CDR Y) A))
                    (p X Y A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show 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 conjectures:

Case 4. (IMPLIES (AND (NLISTP Y) (MEMBER X Y))
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A)))),

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

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP Y))
                      (EQUAL X (CAR Y))
                      (MEMBER X Y))
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A)))),

  which simplifies, opening up the definitions of NLISTP, MEMBER, DELETE, and
  PLUS-TREE, to three new conjectures:

  Case 3.3.
          (IMPLIES (AND (LISTP Y) (NOT (LISTP (CDR Y))))
                   (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                          (DIFFERENCE (EVAL$ T (LIST 'FIX (CAR Y)) A)
                                      (EVAL$ T (CAR Y) A)))),

    which again simplifies, applying the lemmas REWRITE-EVAL$ and CAR-CONS,
    and opening up the definition of FIX, to two new formulas:

    Case 3.3.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            (DIFFERENCE 0 (EVAL$ T (CAR Y) A)))),

      which again simplifies, using linear arithmetic and applying
      DIFFERENCE-0, to the new formula:

            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            0)),

      which further simplifies, opening up the definitions of PLUS-TREE, CDR,
      CAR, LISTP, LITATOM, EQUAL, and EVAL$, to:

            T.

    Case 3.3.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            (DIFFERENCE (EVAL$ T (CAR Y) A)
                                        (EVAL$ T (CAR Y) A)))),

      which again simplifies, using linear arithmetic and rewriting with
      DIFFERENCE-0, to:

            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            0)),

      which further simplifies, expanding the functions PLUS-TREE, CDR, CAR,
      LISTP, LITATOM, EQUAL, and EVAL$, to:

            T.

  Case 3.2.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y)))
                   (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS
                                                   (CAR Y)
                                                   (PLUS-TREE (CDR Y)))
                                             A)
                                      (EVAL$ T (CAR Y) A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, CDR-CONS,
    NUMBERP-EVAL$-PLUS-TREE, and DIFFERENCE-PLUS, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y))))
                   (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS (CAR Y) (CADR Y))
                                             A)
                                      (EVAL$ T (CAR Y) A)))).

    However this again simplifies, appealing to the lemmas REWRITE-EVAL$,
    CAR-CONS, CDR-CONS, and DIFFERENCE-PLUS, to two new goals:

    Case 3.1.2.
            (IMPLIES (AND (LISTP Y)
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y)))
                          (NOT (NUMBERP (EVAL$ T (CADR Y) A))))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            0)),

      which further simplifies, applying REWRITE-EVAL$ and CAR-CONS, and
      opening up the functions PLUS-TREE, FIX, and EQUAL, to:

            T.

    Case 3.1.1.
            (IMPLIES (AND (LISTP Y)
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y)))
                          (NUMBERP (EVAL$ T (CADR Y) A)))
                     (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                            (EVAL$ T (CADR Y) A))).

      But this further simplifies, rewriting with REWRITE-EVAL$ and CAR-CONS,
      and unfolding PLUS-TREE and FIX, to:

            T.

Case 2. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (NOT (MEMBER X (CDR Y)))
                      (MEMBER X Y))
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A)))).

  This simplifies, unfolding NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (EQUAL (EVAL$ T
                                    (PLUS-TREE (DELETE X (CDR Y)))
                                    A)
                             (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                         (EVAL$ T X A)))
                      (MEMBER X Y))
                 (EQUAL (EVAL$ T (PLUS-TREE (DELETE X Y)) A)
                        (DIFFERENCE (EVAL$ T (PLUS-TREE Y) A)
                                    (EVAL$ T X A)))).

  This simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the
  functions NLISTP, MEMBER, DELETE, and PLUS-TREE, to nine new formulas:

  Case 1.9.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (NOT (LISTP (CDR Y)))
                        (NOT (LISTP (DELETE X (CDR Y)))))
                   (EQUAL (EVAL$ T (LIST 'FIX (CAR Y)) A)
                          (DIFFERENCE (EVAL$ T (LIST 'FIX (CAR Y)) A)
                                      (EVAL$ T X A)))),

    which again simplifies, rewriting with EQUAL-DIFFERENCE-0, REWRITE-EVAL$,
    CAR-CONS, and DIFFERENCE-CANCELLATION-0, and opening up the functions
    PLUS-TREE, CDR, CAR, LISTP, LITATOM, EQUAL, EVAL$, and FIX, to:

          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (NOT (LESSP (EVAL$ T X A)
                                    (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                        (MEMBER X (CDR Y))
                        (NOT (LISTP (CDR Y)))
                        (NOT (LISTP (DELETE X (CDR Y))))
                        (NUMBERP (EVAL$ T (CAR Y) A))
                        (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                        (NOT (EQUAL (EVAL$ T X A) 0)))
                   (NOT (NUMBERP (EVAL$ T X A)))),

    which again simplifies, using linear arithmetic and rewriting with
    MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to the following two new conjectures:

    Case 1.9.2.
            (IMPLIES (AND (NOT (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A))
                          (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))).

      However this again simplifies, using linear arithmetic and rewriting
      with the lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

            T.

    Case 1.9.1.
            (IMPLIES (AND (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A))
                          (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A))
                          (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))),

      which again simplifies, clearly, to:

            (IMPLIES (AND (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A))
                          (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))),

      which further simplifies, using linear arithmetic, applying the lemma
      MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, and unfolding EVAL$, EQUAL, LITATOM,
      LISTP, CAR, CDR, and PLUS-TREE, to:

            T.

  Case 1.8.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (NOT (LISTP (CDR Y)))
                        (LISTP (DELETE X (CDR Y)))
                        (LISTP (CDR (DELETE X (CDR Y)))))
                   (EQUAL (EVAL$ T
                                 (LIST 'PLUS
                                       (CAR Y)
                                       (PLUS-TREE (DELETE X (CDR Y))))
                                 A)
                          (DIFFERENCE (EVAL$ T (LIST 'FIX (CAR Y)) A)
                                      (EVAL$ T X A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS,
    and unfolding FIX, to the following two new formulas:

    Case 1.8.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T
                                         (PLUS-TREE (DELETE X (CDR Y)))
                                         A))
                            (DIFFERENCE 0 (EVAL$ T X A)))).

      But this again simplifies, using linear arithmetic, applying the lemma
      DIFFERENCE-0, and opening up the function PLUS, to the goal:

            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (EVAL$ T
                                   (PLUS-TREE (DELETE X (CDR Y)))
                                   A)
                            0)).

      But this further simplifies, using linear arithmetic, rewriting with
      DIFFERENCE-0, and opening up the functions DELETE, PLUS-TREE, CDR, CAR,
      LISTP, LITATOM, EQUAL, EVAL$, and MEMBER, to:

            T.

    Case 1.8.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T
                                         (PLUS-TREE (DELETE X (CDR Y)))
                                         A))
                            (DIFFERENCE (EVAL$ T (CAR Y) A)
                                        (EVAL$ T X A)))).

      This further simplifies, using linear arithmetic, rewriting with the
      lemma DIFFERENCE-0, and opening up the functions DELETE, PLUS-TREE, CDR,
      CAR, LISTP, LITATOM, EQUAL, EVAL$, and MEMBER, to:

            T.

  Case 1.7.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (NOT (LISTP (CDR Y)))
                        (LISTP (DELETE X (CDR Y)))
                        (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                   (EQUAL (EVAL$ T
                                 (LIST 'PLUS
                                       (CAR Y)
                                       (CAR (DELETE X (CDR Y))))
                                 A)
                          (DIFFERENCE (EVAL$ T (LIST 'FIX (CAR Y)) A)
                                      (EVAL$ T X A)))),

    which again simplifies, appealing to the lemmas REWRITE-EVAL$, CAR-CONS,
    CDR-CONS, PLUS-RIGHT-ID2, and DIFFERENCE-CANCELLATION-0, and opening up
    PLUS-TREE and FIX, to three new conjectures:

    Case 1.7.3.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                          (EQUAL 0
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NUMBERP (EVAL$ T (CAR Y) A))
                          (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))),

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

            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NUMBERP (EVAL$ T (CAR Y) A))
                          (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                          (NOT (EQUAL (EVAL$ T X A) 0)))
                     (NOT (NUMBERP (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic and appealing to the
      lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to two new goals:

      Case 1.7.3.2.
              (IMPLIES
                      (AND (NOT (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (NOT (LESSP (EVAL$ T X A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                           (MEMBER X (CDR Y))
                           (NOT (LISTP (CDR Y)))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A))
                           (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                           (NOT (EQUAL (EVAL$ T X A) 0)))
                      (NOT (NUMBERP (EVAL$ T X A)))),

        which again simplifies, using linear arithmetic and applying
        MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

              T.

      Case 1.7.3.1.
              (IMPLIES
                      (AND (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A))
                           (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (NOT (LISTP (CDR Y)))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A))
                           (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                           (NOT (EQUAL (EVAL$ T X A) 0)))
                      (NOT (NUMBERP (EVAL$ T X A)))).

        This again simplifies, trivially, to:

              (IMPLIES
                      (AND (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (NOT (LISTP (CDR Y)))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A))
                           (NOT (EQUAL (EVAL$ T (CAR Y) A) 0))
                           (NOT (EQUAL (EVAL$ T X A) 0)))
                      (NOT (NUMBERP (EVAL$ T X A)))),

        which finally simplifies, using linear arithmetic, rewriting with the
        lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, and opening up the
        functions EVAL$, EQUAL, LITATOM, LISTP, CAR, CDR, and PLUS-TREE, to:

              T.

    Case 1.7.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                          (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                            (DIFFERENCE 0 (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic, applying the lemma
      DIFFERENCE-0, and opening up the definition of PLUS, to:

            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                            0)).

      But this further simplifies, using linear arithmetic, applying
      CAR-NLISTP and DIFFERENCE-0, and expanding DELETE, LISTP, LITATOM, EQUAL,
      EVAL$, PLUS-TREE, CDR, CAR, and MEMBER, to:

            T.

    Case 1.7.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                          (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                            (DIFFERENCE (EVAL$ T (CAR Y) A)
                                        (EVAL$ T X A)))).

      This again simplifies, trivially, to:

            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (NOT (LISTP (CDR Y)))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                            (DIFFERENCE (EVAL$ T (CAR Y) A)
                                        (EVAL$ T X A)))),

      which further simplifies, using linear arithmetic, applying the lemmas
      CAR-NLISTP and DIFFERENCE-0, and opening up the definitions of DELETE,
      LISTP, LITATOM, EQUAL, EVAL$, PLUS-TREE, CDR, CAR, and MEMBER, to:

            T.

  Case 1.6.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y))
                        (NOT (LISTP (DELETE X (CDR Y)))))
                   (EQUAL (EVAL$ T (LIST 'FIX (CAR Y)) A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS
                                                   (CAR Y)
                                                   (PLUS-TREE (CDR Y)))
                                             A)
                                      (EVAL$ T X A)))),

    which again simplifies, applying EQUAL-DIFFERENCE-0, REWRITE-EVAL$,
    CAR-CONS, and CDR-CONS, and unfolding the functions PLUS-TREE, CDR, CAR,
    LISTP, LITATOM, EQUAL, EVAL$, and FIX, to the following two new goals:

    Case 1.6.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL 0
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))).

      This again simplifies, using linear arithmetic and appealing to the
      lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to three new goals:

      Case 1.6.2.3.
              (IMPLIES
                      (AND (NOT (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (LESSP (EVAL$ T X A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (NOT (LISTP (DELETE X (CDR Y))))
                           (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                      (EQUAL 0
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))),

        which again simplifies, applying NUMBERP-EVAL$-PLUS-TREE, to:

              T.

      Case 1.6.2.2.
              (IMPLIES
                      (AND (NOT (NUMBERP (EVAL$ T X A)))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (LESSP (EVAL$ T X A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (NOT (LISTP (DELETE X (CDR Y))))
                           (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                      (EQUAL 0
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))).

        However this again simplifies, using linear arithmetic, applying
        NUMBERP-EVAL$-PLUS-TREE, PLUS-RIGHT-ID2, COMMUTATIVITY-OF-PLUS, and
        DIFFERENCE-0, and expanding LESSP, NUMBERP, and EQUAL, to:

              T.

      Case 1.6.2.1.
              (IMPLIES (AND (NUMBERP (EVAL$ T X A))
                            (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A))
                            (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                   (EVAL$ T X A))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (LISTP (CDDR Y))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                       (EQUAL 0
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T X A))
                                          (EVAL$ T X A)))).

        However this again simplifies, applying PLUS-RIGHT-ID2,
        COMMUTATIVITY-OF-PLUS, and DIFFERENCE-0, and expanding EQUAL, to:

              T.

    Case 1.6.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (CAR Y) A)
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))).

      However this again simplifies, using linear arithmetic and rewriting
      with MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

            (IMPLIES (AND (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (CAR Y) A)
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic and rewriting with the
      lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

            T.

  Case 1.5.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y))
                        (LISTP (DELETE X (CDR Y)))
                        (LISTP (CDR (DELETE X (CDR Y)))))
                   (EQUAL (EVAL$ T
                                 (LIST 'PLUS
                                       (CAR Y)
                                       (PLUS-TREE (DELETE X (CDR Y))))
                                 A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS
                                                   (CAR Y)
                                                   (PLUS-TREE (CDR Y)))
                                             A)
                                      (EVAL$ T X A)))),

    which again simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, to:

          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y))
                        (LISTP (DELETE X (CDR Y)))
                        (LISTP (CDR (DELETE X (CDR Y)))))
                   (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                (EVAL$ T
                                       (PLUS-TREE (DELETE X (CDR Y)))
                                       A))
                          (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                            (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                      (EVAL$ T X A)))),

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

    Case 1.5.2.
            (IMPLIES (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y)))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T
                                         (PLUS-TREE (DELETE X (CDR Y)))
                                         A))
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic and rewriting with
      MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

            T.

    Case 1.5.1.
            (IMPLIES (AND (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y)))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T
                                         (PLUS-TREE (DELETE X (CDR Y)))
                                         A))
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))).

      However this again simplifies, using linear arithmetic, to:

            (IMPLIES (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                 (EVAL$ T X A))
                          (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                       (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                 (EVAL$ T X A))
                          (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (EQUAL (EVAL$ T
                                        (PLUS-TREE (DELETE X (CDR Y)))
                                        A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (LISTP (CDR (DELETE X (CDR Y)))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T
                                         (PLUS-TREE (DELETE X (CDR Y)))
                                         A))
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))).

      But this again simplifies, using linear arithmetic and applying
      MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

            T.

  Case 1.4.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (LISTP (CDDR Y))
                        (LISTP (DELETE X (CDR Y)))
                        (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                   (EQUAL (EVAL$ T
                                 (LIST 'PLUS
                                       (CAR Y)
                                       (CAR (DELETE X (CDR Y))))
                                 A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS
                                                   (CAR Y)
                                                   (PLUS-TREE (CDR Y)))
                                             A)
                                      (EVAL$ T X A)))).

    However this again simplifies, rewriting with REWRITE-EVAL$, CAR-CONS,
    CDR-CONS, and PLUS-RIGHT-ID2, and opening up the definitions of PLUS-TREE
    and FIX, to the following three new formulas:

    Case 1.4.3.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                          (EQUAL 0
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL 0
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))).

      However this again simplifies, applying the lemmas EQUAL-DIFFERENCE-0,
      NUMBERP-EVAL$-PLUS-TREE, and DIFFERENCE-0, and unfolding the definitions
      of PLUS and EQUAL, to:

            T.

    Case 1.4.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                          (EQUAL 0
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (CAR Y) A)
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))),

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

      Case 1.4.2.2.
              (IMPLIES
                      (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (EQUAL 0
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A)))
                      (EQUAL (EVAL$ T (CAR Y) A)
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))),

        which again simplifies, using linear arithmetic and applying the lemma
        MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

              T.

      Case 1.4.2.1.
              (IMPLIES
                      (AND (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (EQUAL 0
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A)))
                      (EQUAL (EVAL$ T (CAR Y) A)
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))),

        which again simplifies, using linear arithmetic, to the conjecture:

              (IMPLIES
                      (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NOT (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A)))
                           (EQUAL 0
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y)))))
                           (NUMBERP (EVAL$ T (CAR Y) A)))
                      (EQUAL (EVAL$ T (CAR Y) A)
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))).

        This again simplifies, using linear arithmetic and appealing to the
        lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

              T.

    Case 1.4.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                          (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                 (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                             (EVAL$ T X A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (LISTP (CDDR Y))
                          (LISTP (DELETE X (CDR Y)))
                          (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                     (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                  (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                        (EVAL$ T X A)))),

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

      Case 1.4.1.2.
              (IMPLIES
                      (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                           (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                      (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                   (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))),

        which again simplifies, using linear arithmetic and applying
        MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

              T.

      Case 1.4.1.1.
              (IMPLIES
                      (AND (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                           (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                      (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                   (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))).

        This again simplifies, using linear arithmetic, to:

              (IMPLIES
                      (AND (LESSP (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                  (EVAL$ T X A))
                           (LESSP (PLUS (EVAL$ T (CAR Y) A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                  (EVAL$ T X A))
                           (LISTP Y)
                           (NOT (EQUAL X (CAR Y)))
                           (NUMBERP (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                           (EQUAL (EVAL$ T (CAR (DELETE X (CDR Y))) A)
                                  (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                              (EVAL$ T X A)))
                           (MEMBER X (CDR Y))
                           (LISTP (CDR Y))
                           (LISTP (CDDR Y))
                           (LISTP (DELETE X (CDR Y)))
                           (NOT (LISTP (CDR (DELETE X (CDR Y))))))
                      (EQUAL (PLUS (EVAL$ T (CAR Y) A)
                                   (EVAL$ T (CAR (DELETE X (CDR Y))) A))
                             (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                               (EVAL$ T (PLUS-TREE (CDR Y)) A))
                                         (EVAL$ T X A)))).

        This again simplifies, using linear arithmetic and rewriting with
        MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to:

              T.

  Case 1.3.
          (IMPLIES (AND (LISTP Y)
                        (NOT (EQUAL X (CAR Y)))
                        (EQUAL (EVAL$ T
                                      (PLUS-TREE (DELETE X (CDR Y)))
                                      A)
                               (DIFFERENCE (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                           (EVAL$ T X A)))
                        (MEMBER X (CDR Y))
                        (LISTP (CDR Y))
                        (NOT (LISTP (CDDR Y)))
                        (NOT (LISTP (DELETE X (CDR Y)))))
                   (EQUAL (EVAL$ T (LIST 'FIX (CAR Y)) A)
                          (DIFFERENCE (EVAL$ T
                                             (LIST 'PLUS (CAR Y) (CADR Y))
                                             A)
                                      (EVAL$ T X A)))).

    However this again simplifies, applying the lemmas EQUAL-DIFFERENCE-0,
    REWRITE-EVAL$, CAR-CONS, and CDR-CONS, and opening up the functions
    PLUS-TREE, CDR, CAR, LISTP, LITATOM, EQUAL, EVAL$, and FIX, to two new
    conjectures:

    Case 1.3.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y)))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                     (EQUAL 0
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (CADR Y) A))
                                        (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic and rewriting with
      MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to the following three new formulas:

      Case 1.3.2.3.
              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                       (EQUAL 0
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T (CADR Y) A))
                                          (EVAL$ T X A)))).

        However this again simplifies, rewriting with NUMBERP-EVAL$-PLUS-TREE,
        to:

              T.

      Case 1.3.2.2.
              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T X A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                       (EQUAL 0
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T (CADR Y) A))
                                          (EVAL$ T X A)))).

        But this again simplifies, applying NUMBERP-EVAL$-PLUS-TREE, and
        opening up the definitions of LESSP, PLUS, and DIFFERENCE, to:

              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T X A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                   0)
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A)))
                            (NUMBERP (EVAL$ T (CADR Y) A))
                            (NOT (EQUAL (EVAL$ T (CADR Y) A) 0)))
                       (EQUAL 0 (EVAL$ T (CADR Y) A))),

        which again simplifies, obviously, to:

              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T X A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                   0)
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A)))
                            (NUMBERP (EVAL$ T (CADR Y) A)))
                       (EQUAL 0 (EVAL$ T (CADR Y) A))),

        which finally simplifies, rewriting with REWRITE-EVAL$ and CAR-CONS,
        and expanding PLUS-TREE and FIX, to:

              T.

      Case 1.3.2.1.
              (IMPLIES (AND (NUMBERP (EVAL$ T X A))
                            (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A))
                            (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                   (EVAL$ T X A))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NOT (NUMBERP (EVAL$ T (CAR Y) A))))
                       (EQUAL 0
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T (CADR Y) A))
                                          (EVAL$ T X A)))).

        This again simplifies, applying the lemma EQUAL-DIFFERENCE-0, and
        unfolding PLUS, to two new conjectures:

        Case 1.3.2.1.2.
                (IMPLIES (AND (NUMBERP (EVAL$ T X A))
                              (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                     (EVAL$ T X A))
                              (LISTP Y)
                              (NOT (EQUAL X (CAR Y)))
                              (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                              (MEMBER X (CDR Y))
                              (LISTP (CDR Y))
                              (NOT (LISTP (CDDR Y)))
                              (NOT (LISTP (DELETE X (CDR Y))))
                              (NOT (NUMBERP (EVAL$ T (CAR Y) A)))
                              (NOT (NUMBERP (EVAL$ T (CADR Y) A))))
                         (NOT (LESSP (EVAL$ T X A) 0))),

          which again simplifies, using linear arithmetic, to:

                T.

        Case 1.3.2.1.1.
                (IMPLIES (AND (NUMBERP (EVAL$ T X A))
                              (EQUAL (EVAL$ T (PLUS-TREE (CDR Y)) A)
                                     (EVAL$ T X A))
                              (LISTP Y)
                              (NOT (EQUAL X (CAR Y)))
                              (NOT (LESSP (EVAL$ T X A) (EVAL$ T X A)))
                              (MEMBER X (CDR Y))
                              (LISTP (CDR Y))
                              (NOT (LISTP (CDDR Y)))
                              (NOT (LISTP (DELETE X (CDR Y))))
                              (NOT (NUMBERP (EVAL$ T (CAR Y) A)))
                              (NUMBERP (EVAL$ T (CADR Y) A)))
                         (NOT (LESSP (EVAL$ T X A)
                                     (EVAL$ T (CADR Y) A)))),

          which further simplifies, applying the lemmas REWRITE-EVAL$,
          CAR-CONS, CONS-CAR-CDR, and DELETE-NON-MEMBER, and opening up the
          definitions of PLUS-TREE, FIX, MEMBER, and DELETE, to:

                T.

    Case 1.3.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (EQUAL X (CAR Y)))
                          (NOT (LESSP (EVAL$ T X A)
                                      (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                          (MEMBER X (CDR Y))
                          (LISTP (CDR Y))
                          (NOT (LISTP (CDDR Y)))
                          (NOT (LISTP (DELETE X (CDR Y))))
                          (NUMBERP (EVAL$ T (CAR Y) A)))
                     (EQUAL (EVAL$ T (CAR Y) A)
                            (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                              (EVAL$ T (CADR Y) A))
                                        (EVAL$ T X A)))),

      which again simplifies, using linear arithmetic and rewriting with the
      lemma MEMBER-IMPLIES-PLUS-TREE-GREATEREQP, to three new conjectures:

      Case 1.3.1.3.
              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NUMBERP (EVAL$ T (CAR Y) A)))
                       (EQUAL (EVAL$ T (CAR Y) A)
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T (CADR Y) A))
                                          (EVAL$ T X A)))),

        which again simplifies, rewriting with NUMBERP-EVAL$-PLUS-TREE, to:

              T.

      Case 1.3.1.2.
              (IMPLIES (AND (NOT (NUMBERP (EVAL$ T X A)))
                            (LISTP Y)
                            (NOT (EQUAL X (CAR Y)))
                            (NOT (LESSP (EVAL$ T X A)
                                        (EVAL$ T (PLUS-TREE (CDR Y)) A)))
                            (MEMBER X (CDR Y))
                            (LISTP (CDR Y))
                            (NOT (LISTP (CDDR Y)))
                            (NOT (LISTP (DELETE X (CDR Y))))
                            (NUMBERP (EVAL$ T (CAR Y) A)))
                       (EQUAL (EVAL$ T (CAR Y) A)
                              (DIFFERENCE (PLUS (EVAL$ T (CAR Y) A)
                                                (EVAL$ T (CADR Y) A))
                                          (EVAL$ T X A)))).

        But this again simplifies, rewriting with NUMBERP-EVAL$-PLUS-TREE and
        PLUS