(BOOT-STRAP NQTHM)

[ 0.0 0.1 0.0 ]

GROUND-ZERO


(DEFN REMOVE1
      (A X)
      (IF (LISTP X)
          (IF (EQUAL (CAR X) A)
              (CDR X)
              (CONS (CAR X) (REMOVE1 A (CDR X))))
          X))

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




[ 0.0 0.0 0.0 ]

REMOVE1


(DEFN BADGUY
      (X Y)
      (IF (LISTP X)
          (IF (MEMBER (CAR X) Y)
              (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
              (CAR X))
          0))

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




[ 0.0 0.0 0.0 ]

BADGUY


(DEFN SUBBAGP
      (X Y)
      (IF (LISTP X)
          (AND (MEMBER (CAR X) Y)
               (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y)))
          T))

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




[ 0.0 0.0 0.0 ]

SUBBAGP


(DEFN OCCUR
      (A X)
      (IF (LISTP X)
          (IF (EQUAL (CAR X) A)
              (ADD1 (OCCUR A (CDR X)))
              (OCCUR A (CDR X)))
          0))

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




[ 0.0 0.0 0.0 ]

OCCUR


(PROVE-LEMMA MEMBER-OCCUR
             (REWRITE)
             (EQUAL (MEMBER A X)
                    (LESSP 0 (OCCUR A X))))

This formula simplifies, expanding the functions EQUAL and LESSP, to two new
conjectures:

Case 2. (IMPLIES (NOT (EQUAL (OCCUR A X) 0))
                 (EQUAL (MEMBER A X) T)),

  which again simplifies, trivially, to the new formula:

        (IMPLIES (NOT (EQUAL (OCCUR A X) 0))
                 (MEMBER A X)),

  which we will name *1.

Case 1. (IMPLIES (EQUAL (OCCUR A X) 0)
                 (EQUAL (MEMBER A X) F)).

  This again simplifies, obviously, to:

        (IMPLIES (EQUAL (OCCUR A X) 0)
                 (NOT (MEMBER A X))),

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


     So now let us return to:

(EQUAL (MEMBER A X)
       (LESSP 0 (OCCUR A X))).

We named this *1.  We will try to prove it by induction.  The recursive terms
in the conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP X) (p A X))
           (IMPLIES (AND (NOT (NLISTP X))
                         (EQUAL A (CAR X)))
                    (p A X))
           (IMPLIES (AND (NOT (NLISTP X))
                         (NOT (EQUAL A (CAR X)))
                         (p A (CDR X)))
                    (p A X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces the following three new goals:

Case 3. (IMPLIES (NLISTP X)
                 (EQUAL (MEMBER A X)
                        (LESSP 0 (OCCUR A X)))).

  This simplifies, expanding the definitions of NLISTP, MEMBER, OCCUR, LESSP,
  and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP X))
                      (EQUAL A (CAR X)))
                 (EQUAL (MEMBER A X)
                        (LESSP 0 (OCCUR A X)))).

  This simplifies, expanding NLISTP, MEMBER, EQUAL, and LESSP, to:

        (IMPLIES (LISTP X)
                 (NOT (EQUAL (OCCUR (CAR X) X) 0))).

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

        (NOT (EQUAL (OCCUR Z (CONS Z V)) 0)),

  which further simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
  up OCCUR, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (EQUAL A (CAR X)))
                      (EQUAL (MEMBER A (CDR X))
                             (LESSP 0 (OCCUR A (CDR X)))))
                 (EQUAL (MEMBER A X)
                        (LESSP 0 (OCCUR A X)))).

  This simplifies, expanding the functions NLISTP, EQUAL, LESSP, MEMBER, and
  OCCUR, to:

        T.


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


[ 0.0 0.0 0.0 ]

MEMBER-OCCUR


(PROVE-LEMMA OCCUR-REMOVE1
             (REWRITE)
             (EQUAL (OCCUR A (REMOVE1 B X))
                    (IF (EQUAL A B)
                        (SUB1 (OCCUR A X))
                        (OCCUR A X))))

This simplifies, trivially, to the following two new goals:

Case 2. (IMPLIES (NOT (EQUAL A B))
                 (EQUAL (OCCUR A (REMOVE1 B X))
                        (OCCUR A X))).

  Give the above formula the name *1.

Case 1. (IMPLIES (EQUAL A B)
                 (EQUAL (OCCUR A (REMOVE1 B X))
                        (SUB1 (OCCUR A X)))).

  This again simplifies, trivially, to:

        (EQUAL (OCCUR B (REMOVE1 B X))
               (SUB1 (OCCUR B X))),

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


     So now let us return to:

(EQUAL (OCCUR A (REMOVE1 B X))
       (IF (EQUAL A B)
           (SUB1 (OCCUR A X))
           (OCCUR A X))).

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

Case 3. (IMPLIES (AND (LISTP X) (EQUAL (CAR X) B))
                 (EQUAL (OCCUR A (REMOVE1 B X))
                        (IF (EQUAL A B)
                            (SUB1 (OCCUR A X))
                            (OCCUR A X)))),

  which simplifies, applying SUB1-ADD1, and unfolding REMOVE1 and OCCUR, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (EQUAL (CAR X) B))
                      (EQUAL (OCCUR A (REMOVE1 B (CDR X)))
                             (IF (EQUAL A B)
                                 (SUB1 (OCCUR A (CDR X)))
                                 (OCCUR A (CDR X)))))
                 (EQUAL (OCCUR A (REMOVE1 B X))
                        (IF (EQUAL A B)
                            (SUB1 (OCCUR A X))
                            (OCCUR A X)))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up
  REMOVE1 and OCCUR, to two new conjectures:

  Case 2.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) B))
                        (EQUAL A B)
                        (EQUAL (OCCUR A (REMOVE1 B (CDR X)))
                               (SUB1 (OCCUR A (CDR X))))
                        (NOT (EQUAL (CAR X) A)))
                   (EQUAL (OCCUR A
                                 (CONS (CAR X) (REMOVE1 A (CDR X))))
                          (SUB1 (OCCUR A (CDR X))))),

    which again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
    and expanding the definition of OCCUR, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) B))
                        (EQUAL A B)
                        (EQUAL (OCCUR A (REMOVE1 B (CDR X)))
                               (SUB1 (OCCUR A (CDR X))))
                        (EQUAL (CAR X) A))
                   (EQUAL (OCCUR A (CDR X))
                          (SUB1 (ADD1 (OCCUR A (CDR X)))))),

    which again simplifies, clearly, to:

          T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (EQUAL (OCCUR A (REMOVE1 B X))
                        (IF (EQUAL A B)
                            (SUB1 (OCCUR A X))
                            (OCCUR A X)))).

  This simplifies, expanding the functions REMOVE1, OCCUR, SUB1, and EQUAL, to:

        T.


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


[ 0.0 0.0 0.0 ]

OCCUR-REMOVE1


(PROVE-LEMMA SUBBAGP-WIT-LEMMA
             (REWRITE)
             (EQUAL (SUBBAGP X Y)
                    (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                (OCCUR (BADGUY X Y) X)))))

This formula simplifies, opening up NOT, to the following two new formulas:

Case 2. (IMPLIES (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                             (OCCUR (BADGUY X Y) X)))
                 (EQUAL (SUBBAGP X Y) T)).

  This again simplifies, trivially, to the new formula:

        (IMPLIES (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                             (OCCUR (BADGUY X Y) X)))
                 (SUBBAGP X Y)),

  which we will name *1.

Case 1. (IMPLIES (LESSP (OCCUR (BADGUY X Y) Y)
                        (OCCUR (BADGUY X Y) X))
                 (EQUAL (SUBBAGP X Y) F)).

  This again simplifies, clearly, to:

        (IMPLIES (LESSP (OCCUR (BADGUY X Y) Y)
                        (OCCUR (BADGUY X Y) X))
                 (NOT (SUBBAGP X Y))),

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


     So now let us return to:

(EQUAL (SUBBAGP X Y)
       (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                   (OCCUR (BADGUY X Y) X)))).

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

Case 3. (IMPLIES
            (AND (LISTP X)
                 (MEMBER (CAR X) Y)
                 (EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
                        (NOT (LESSP (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                           (REMOVE1 (CAR X) Y))
                                    (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                           (CDR X))))))
            (EQUAL (SUBBAGP X Y)
                   (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                               (OCCUR (BADGUY X Y) X))))).

  This simplifies, applying MEMBER-OCCUR, OCCUR-REMOVE1, and SUB1-ADD1, and
  expanding the definitions of EQUAL, LESSP, NOT, SUBBAGP, BADGUY, and OCCUR,
  to two new conjectures:

  Case 3.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                                    (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                           (CDR X))))
                        (EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
                               T))
                   (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (CAR X) (CDR X))))),

    which again simplifies, obviously, to:

          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                                    (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                           (CDR X))))
                        (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y)))
                   (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (CAR X) (CDR X))))),

    which further simplifies, clearly, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                      (CDR X)))
                        (EQUAL (SUBBAGP (CDR X) (REMOVE1 (CAR X) Y))
                               F))
                   (LESSP (SUB1 (OCCUR (CAR X) Y))
                          (OCCUR (CAR X) (CDR X)))).

    This again simplifies, obviously, to:

          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                      (CDR X)))
                        (NOT (SUBBAGP (CDR X)
                                      (REMOVE1 (CAR X) Y))))
                   (LESSP (SUB1 (OCCUR (CAR X) Y))
                          (OCCUR (CAR X) (CDR X)))),

    which further simplifies, obviously, to:

          T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) Y)))
                 (EQUAL (SUBBAGP X Y)
                        (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                    (OCCUR (BADGUY X Y) X))))).

  This simplifies, applying the lemma MEMBER-OCCUR, and opening up EQUAL,
  LESSP, SUBBAGP, BADGUY, and NOT, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (OCCUR (CAR X) Y) 0))
                 (NOT (EQUAL (OCCUR (CAR X) X) 0))).

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

        (IMPLIES (EQUAL (OCCUR Z Y) 0)
                 (NOT (EQUAL (OCCUR Z (CONS Z V)) 0))),

  which further simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
  unfolding the function OCCUR, to:

        T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (EQUAL (SUBBAGP X Y)
                        (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                    (OCCUR (BADGUY X Y) X))))),

  which simplifies, opening up the definitions of SUBBAGP, BADGUY, OCCUR,
  EQUAL, LESSP, and NOT, to:

        T.


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


[ 0.0 0.0 0.0 ]

SUBBAGP-WIT-LEMMA


(PROVE-LEMMA OCCUR-APPEND
             (REWRITE)
             (EQUAL (OCCUR A (APPEND X Y))
                    (PLUS (OCCUR A X) (OCCUR A Y))))


     Call the conjecture *1.


     We will try to prove it by induction.  There are three plausible
inductions.  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) (p A (CDR X) Y))
                    (p A X Y))
           (IMPLIES (NOT (LISTP X)) (p A 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.  The above induction scheme generates two new goals:

Case 2. (IMPLIES (AND (LISTP X)
                      (EQUAL (OCCUR A (APPEND (CDR X) Y))
                             (PLUS (OCCUR A (CDR X)) (OCCUR A Y))))
                 (EQUAL (OCCUR A (APPEND X Y))
                        (PLUS (OCCUR A X) (OCCUR A Y)))),

  which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
  unfolding APPEND and OCCUR, to two new formulas:

  Case 2.2.
          (IMPLIES (AND (LISTP X)
                        (EQUAL (OCCUR A (APPEND (CDR X) Y))
                               (PLUS (OCCUR A (CDR X)) (OCCUR A Y)))
                        (NOT (EQUAL (CAR X) A)))
                   (EQUAL (OCCUR A (APPEND (CDR X) Y))
                          (PLUS (OCCUR A (CDR X))
                                (OCCUR A Y)))),

    which again simplifies, clearly, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP X)
                        (EQUAL (OCCUR A (APPEND (CDR X) Y))
                               (PLUS (OCCUR A (CDR X)) (OCCUR A Y)))
                        (EQUAL (CAR X) A))
                   (EQUAL (ADD1 (OCCUR A (APPEND (CDR X) Y)))
                          (PLUS (ADD1 (OCCUR A (CDR X)))
                                (OCCUR A Y)))).

    But this again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (EQUAL (OCCUR A (APPEND X Y))
                        (PLUS (OCCUR A X) (OCCUR A Y)))),

  which simplifies, opening up the definitions of APPEND, OCCUR, EQUAL, and
  PLUS, to:

        T.


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


[ 0.0 0.0 0.0 ]

OCCUR-APPEND


(PROVE-LEMMA SUBBAGP-APPEND
             (REWRITE)
             (SUBBAGP (APPEND X Y) (APPEND Y X)))

This formula can be simplified, using the abbreviations NOT and
SUBBAGP-WIT-LEMMA, to:

      (NOT (LESSP (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                         (APPEND Y X))
                  (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                         (APPEND X Y)))),

which simplifies, applying the lemma OCCUR-APPEND, to:

      (NOT (LESSP (PLUS (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                               Y)
                        (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                               X))
                  (PLUS (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                               X)
                        (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                               Y)))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-APPEND


(DEFN PERMUTATIONP
      (X Y)
      (AND (SUBBAGP X Y) (SUBBAGP Y X)))

     Observe that (OR (FALSEP (PERMUTATIONP X Y)) (TRUEP (PERMUTATIONP X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

PERMUTATIONP


(PROVE-LEMMA PERMUTATIONP-APPEND
             (REWRITE)
             (PERMUTATIONP (APPEND X Y)
                           (APPEND Y X)))

WARNING:  Note that the rewrite rule PERMUTATIONP-APPEND will be stored so as
to apply only to terms with the nonrecursive function symbol PERMUTATIONP.


This formula can be simplified, using the abbreviations NOT, SUBBAGP-WIT-LEMMA,
and PERMUTATIONP, to the following two new conjectures:

Case 2. (NOT (LESSP (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                           (APPEND Y X))
                    (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                           (APPEND X Y)))).

  This simplifies, applying OCCUR-APPEND, to:

        (NOT (LESSP (PLUS (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                                 Y)
                          (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                                 X))
                    (PLUS (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                                 X)
                          (OCCUR (BADGUY (APPEND X Y) (APPEND Y X))
                                 Y)))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 1. (NOT (LESSP (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                           (APPEND X Y))
                    (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                           (APPEND Y X)))),

  which simplifies, applying OCCUR-APPEND, to the new goal:

        (NOT (LESSP (PLUS (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                                 X)
                          (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                                 Y))
                    (PLUS (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                                 Y)
                          (OCCUR (BADGUY (APPEND Y X) (APPEND X Y))
                                 X)))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PERMUTATIONP-APPEND


(PROVE-LEMMA SUBBAGP-NECC
             (REWRITE)
             (IMPLIES (SUBBAGP X Y)
                      (NOT (LESSP (OCCUR A Y) (OCCUR A X)))))

WARNING:  When the linear lemma SUBBAGP-NECC is stored under (OCCUR A Y) it
contains the free variable X which will be chosen by instantiating the
hypothesis (SUBBAGP X Y).


WARNING:  When the linear lemma SUBBAGP-NECC is stored under (OCCUR A X) it
contains the free variable Y which will be chosen by instantiating the
hypothesis (SUBBAGP X Y).


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


This formula can be simplified, using the abbreviations NOT, SUBBAGP-WIT-LEMMA,
and IMPLIES, to the new conjecture:

      (IMPLIES (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                           (OCCUR (BADGUY X Y) X)))
               (NOT (LESSP (OCCUR A Y) (OCCUR A X)))),

which we will name *1.


     We will appeal to induction.  The recursive terms in the conjecture
suggest six inductions.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP X)
                         (MEMBER (CAR X) Y)
                         (p A (REMOVE1 (CAR X) Y) (CDR X)))
                    (p A Y X))
           (IMPLIES (AND (LISTP X)
                         (NOT (MEMBER (CAR X) Y)))
                    (p A Y X))
           (IMPLIES (NOT (LISTP X)) (p A Y X))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for Y.  The above
induction scheme leads to the following four new formulas:

Case 4. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) Y)
                      (LESSP (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                    (REMOVE1 (CAR X) Y))
                             (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                    (CDR X)))
                      (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                  (OCCUR (BADGUY X Y) X))))
                 (NOT (LESSP (OCCUR A Y) (OCCUR A X)))).

  This simplifies, applying the lemmas MEMBER-OCCUR, OCCUR-REMOVE1, and
  SUB1-ADD1, and unfolding the definitions of EQUAL, LESSP, BADGUY, and OCCUR,
  to the following two new conjectures:

  Case 4.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                      (CDR X)))
                        (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                                    (OCCUR (CAR X) (CDR X))))
                        (NOT (EQUAL (CAR X) A)))
                   (NOT (LESSP (OCCUR A Y)
                               (OCCUR A (CDR X))))).

    This further simplifies, clearly, to:

          T.

  Case 4.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (OCCUR (CAR X) Y) 0))
                        (EQUAL (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                               (CAR X))
                        (LESSP (SUB1 (OCCUR (CAR X) Y))
                               (OCCUR (BADGUY (CDR X) (REMOVE1 (CAR X) Y))
                                      (CDR X)))
                        (NOT (LESSP (SUB1 (OCCUR (CAR X) Y))
                                    (OCCUR (CAR X) (CDR X))))
                        (EQUAL (CAR X) A))
                   (NOT (LESSP (OCCUR A Y)
                               (ADD1 (OCCUR A (CDR X)))))).

    But this again simplifies, using linear arithmetic, to:

          T.

Case 3. (IMPLIES (AND (LISTP X)
                      (MEMBER (CAR X) Y)
                      (NOT (LESSP (OCCUR A (REMOVE1 (CAR X) Y))
                                  (OCCUR A (CDR X))))
                      (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                  (OCCUR (BADGUY X Y) X))))
                 (NOT (LESSP (OCCUR A Y) (OCCUR A X)))),

  which simplifies, rewriting with MEMBER-OCCUR, OCCUR-REMOVE1, and SUB1-ADD1,
  and opening up the functions EQUAL, LESSP, BADGUY, and OCCUR, to:

        T.

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (MEMBER (CAR X) Y))
                      (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                  (OCCUR (BADGUY X Y) X))))
                 (NOT (LESSP (OCCUR A Y) (OCCUR A X)))).

  This simplifies, rewriting with MEMBER-OCCUR, and opening up the functions
  EQUAL, LESSP, BADGUY, and OCCUR, to two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP X)
                        (EQUAL (OCCUR (CAR X) Y) 0)
                        (EQUAL (OCCUR (CAR X) X) 0)
                        (NOT (EQUAL (CAR X) A)))
                   (NOT (LESSP (OCCUR A Y)
                               (OCCUR A (CDR X))))).

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

          (IMPLIES (AND (EQUAL (OCCUR Z Y) 0)
                        (EQUAL (OCCUR Z (CONS Z V)) 0)
                        (NOT (EQUAL Z A)))
                   (NOT (LESSP (OCCUR A Y) (OCCUR A V)))),

    which further simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
    unfolding the definition of OCCUR, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP X)
                        (EQUAL (OCCUR (CAR X) Y) 0)
                        (EQUAL (OCCUR (CAR X) X) 0)
                        (EQUAL (CAR X) A))
                   (NOT (LESSP (OCCUR A Y)
                               (ADD1 (OCCUR A (CDR X)))))),

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

          (IMPLIES (AND (LISTP X)
                        (EQUAL (OCCUR (CAR X) Y) 0))
                   (NOT (EQUAL (OCCUR (CAR X) X) 0))).

    Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to
    eliminate (CAR X) and (CDR X).  We must thus prove:

          (IMPLIES (EQUAL (OCCUR Z Y) 0)
                   (NOT (EQUAL (OCCUR Z (CONS Z V)) 0))).

    However this further simplifies, applying the lemmas CDR-CONS and CAR-CONS,
    and opening up the definition of OCCUR, to:

          T.

Case 1. (IMPLIES (AND (NOT (LISTP X))
                      (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                  (OCCUR (BADGUY X Y) X))))
                 (NOT (LESSP (OCCUR A Y) (OCCUR A X)))),

  which simplifies, opening up the definitions of BADGUY, OCCUR, EQUAL, and
  LESSP, to:

        T.


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


[ 0.0 0.0 0.0 ]

SUBBAGP-NECC


(PROVE-LEMMA SUBBAGP-TRANSITIVE
             (REWRITE)
             (IMPLIES (AND (SUBBAGP X Y) (SUBBAGP Y Z))
                      (SUBBAGP X Z))
             ((USE (SUBBAGP-NECC (A (BADGUY X Z))
                                 (Y Z)
                                 (X Y))
                   (SUBBAGP-NECC (A (BADGUY X Z))))
              (DISABLE SUBBAGP-NECC)))

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


This conjecture can be simplified, using the abbreviations SUBBAGP-WIT-LEMMA,
IMPLIES, and AND, to the goal:

      (IMPLIES (AND (IMPLIES (SUBBAGP Y Z)
                             (NOT (LESSP (OCCUR (BADGUY X Z) Z)
                                         (OCCUR (BADGUY X Z) Y))))
                    (IMPLIES (SUBBAGP X Y)
                             (NOT (LESSP (OCCUR (BADGUY X Z) Y)
                                         (OCCUR (BADGUY X Z) X))))
                    (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                (OCCUR (BADGUY X Y) X)))
                    (NOT (LESSP (OCCUR (BADGUY Y Z) Z)
                                (OCCUR (BADGUY Y Z) Y))))
               (NOT (LESSP (OCCUR (BADGUY X Z) Z)
                           (OCCUR (BADGUY X Z) X)))).

This simplifies, appealing to the lemma SUBBAGP-WIT-LEMMA, and unfolding the
functions NOT and IMPLIES, to:

      (IMPLIES (AND (NOT (LESSP (OCCUR (BADGUY X Z) Z)
                                (OCCUR (BADGUY X Z) Y)))
                    (NOT (LESSP (OCCUR (BADGUY X Z) Y)
                                (OCCUR (BADGUY X Z) X)))
                    (NOT (LESSP (OCCUR (BADGUY X Y) Y)
                                (OCCUR (BADGUY X Y) X)))
                    (NOT (LESSP (OCCUR (BADGUY Y Z) Z)
                                (OCCUR (BADGUY Y Z) Y))))
               (NOT (LESSP (OCCUR (BADGUY X Z) Z)
                           (OCCUR (BADGUY X Z) X)))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUBBAGP-TRANSITIVE


(PROVE-LEMMA PERMUTATIONP-TRANSITIVE
             (REWRITE)
             (IMPLIES (AND (PERMUTATIONP X Y)
                           (PERMUTATIONP Y Z))
                      (PERMUTATIONP X Z))
             ((DISABLE SUBBAGP-WIT-LEMMA)))

WARNING:  Note that the rewrite rule PERMUTATIONP-TRANSITIVE will be stored so
as to apply only to terms with the nonrecursive function symbol PERMUTATIONP.


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


This formula can be simplified, using the abbreviations PERMUTATIONP, AND, and
IMPLIES, to:

      (IMPLIES (AND (SUBBAGP X Y)
                    (SUBBAGP Y X)
                    (SUBBAGP Y Z)
                    (SUBBAGP Z Y))
               (PERMUTATIONP X Z)),

which simplifies, rewriting with the lemma SUBBAGP-TRANSITIVE, and expanding
the function PERMUTATIONP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PERMUTATIONP-TRANSITIVE