(BOOT-STRAP NQTHM)

[ 0.0 0.1 0.0 ]

GROUND-ZERO


(DEFN DOUBLE-LIST
      (L)
      (IF (NLISTP L)
          NIL
          (CONS (TIMES 2 (CAR L))
                (DOUBLE-LIST (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, DOUBLE-LIST
is accepted under the principle of definition.  Note that:
      (OR (LITATOM (DOUBLE-LIST L))
          (LISTP (DOUBLE-LIST L)))
is a theorem.




[ 0.0 0.0 0.0 ]

DOUBLE-LIST


(PROVE-LEMMA DOUBLE-LIST-APPEND NIL
             (EQUAL (DOUBLE-LIST (APPEND A B))
                    (APPEND (DOUBLE-LIST A)
                            (DOUBLE-LIST B))))


     Call the conjecture *1.


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

Case 2. (IMPLIES (AND (LISTP A)
                      (EQUAL (DOUBLE-LIST (APPEND (CDR A) B))
                             (APPEND (DOUBLE-LIST (CDR A))
                                     (DOUBLE-LIST B))))
                 (EQUAL (DOUBLE-LIST (APPEND A B))
                        (APPEND (DOUBLE-LIST A)
                                (DOUBLE-LIST B)))),

  which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
  the definitions of APPEND and DOUBLE-LIST, to:

        T.

Case 1. (IMPLIES (NOT (LISTP A))
                 (EQUAL (DOUBLE-LIST (APPEND A B))
                        (APPEND (DOUBLE-LIST A)
                                (DOUBLE-LIST B)))),

  which simplifies, unfolding the functions APPEND, DOUBLE-LIST, and LISTP, to:

        T.


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


[ 0.0 0.0 0.0 ]

DOUBLE-LIST-APPEND


(PROVE-LEMMA SUM-DISTRIBUTES-OVER-PLUS NIL
             (EQUAL (FOR I L COND 'SUM
                         (LIST 'PLUS G H)
                         A)
                    (PLUS (FOR I L COND 'SUM G A)
                          (FOR I L COND 'SUM H A))))


     Call the conjecture *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 (NLISTP L)
                    (p I L COND G H A))
           (IMPLIES (AND (NOT (NLISTP L))
                         (EVAL$ T COND
                                (CONS (CONS I (CAR L)) A))
                         (p I (CDR L) COND G H A))
                    (p I L COND G H A))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NOT (EVAL$ T COND
                                     (CONS (CONS I (CAR L)) A)))
                         (p I (CDR L) COND G H A))
                    (p I L COND G H 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 produces the following three new formulas:

Case 3. (IMPLIES (NLISTP L)
                 (EQUAL (FOR I L COND 'SUM
                             (LIST 'PLUS G H)
                             A)
                        (PLUS (FOR I L COND 'SUM G A)
                              (FOR I L COND 'SUM H A)))).

  This simplifies, unfolding the functions NLISTP, FOR,
  QUANTIFIER-INITIAL-VALUE, PLUS, and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (EVAL$ T COND
                             (CONS (CONS I (CAR L)) A))
                      (EQUAL (FOR I
                                  (CDR L)
                                  COND 'SUM
                                  (LIST 'PLUS G H)
                                  A)
                             (PLUS (FOR I (CDR L) COND 'SUM G A)
                                   (FOR I (CDR L) COND 'SUM H A))))
                 (EQUAL (FOR I L COND 'SUM
                             (LIST 'PLUS G H)
                             A)
                        (PLUS (FOR I L COND 'SUM G A)
                              (FOR I L COND 'SUM H A)))).

  This simplifies, applying REWRITE-EVAL$, CAR-CONS, and CDR-CONS, and
  unfolding the definitions of NLISTP, FOR, EQUAL, and QUANTIFIER-OPERATION,
  to:

        (IMPLIES (AND (LISTP L)
                      (EVAL$ T COND
                             (CONS (CONS I (CAR L)) A))
                      (EQUAL (FOR I
                                  (CDR L)
                                  COND 'SUM
                                  (LIST 'PLUS G H)
                                  A)
                             (PLUS (FOR I (CDR L) COND 'SUM G A)
                                   (FOR I (CDR L) COND 'SUM H A))))
                 (EQUAL (PLUS (PLUS (EVAL$ T G (CONS (CONS I (CAR L)) A))
                                    (EVAL$ T H (CONS (CONS I (CAR L)) A)))
                              (FOR I
                                   (CDR L)
                                   COND 'SUM
                                   (LIST 'PLUS G H)
                                   A))
                        (PLUS (PLUS (EVAL$ T G (CONS (CONS I (CAR L)) A))
                                    (FOR I (CDR L) COND 'SUM G A))
                              (EVAL$ T H (CONS (CONS I (CAR L)) A))
                              (FOR I (CDR L) COND 'SUM H A)))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (EVAL$ T COND
                                  (CONS (CONS I (CAR L)) A)))
                      (EQUAL (FOR I
                                  (CDR L)
                                  COND 'SUM
                                  (LIST 'PLUS G H)
                                  A)
                             (PLUS (FOR I (CDR L) COND 'SUM G A)
                                   (FOR I (CDR L) COND 'SUM H A))))
                 (EQUAL (FOR I L COND 'SUM
                             (LIST 'PLUS G H)
                             A)
                        (PLUS (FOR I L COND 'SUM G A)
                              (FOR I L COND 'SUM H A)))),

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

        T.


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


[ 0.0 0.1 0.0 ]

SUM-DISTRIBUTES-OVER-PLUS


(PROVE-LEMMA EVAL$-DISTRIBUTES-OVER-PLUS NIL
             (EQUAL (EVAL$ T (LIST 'PLUS X Y) A)
                    (PLUS (EVAL$ T X A) (EVAL$ T Y A))))

This formula simplifies, appealing to the lemmas REWRITE-EVAL$, CAR-CONS, and
CDR-CONS, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EVAL$-DISTRIBUTES-OVER-PLUS


(PROVE-LEMMA V&C$-LIST-DEFN NIL
             (EQUAL (V&C$ 'LIST L VA)
                    (IF (NLISTP L)
                        NIL
                        (CONS (V&C$ T (CAR L) VA)
                              (V&C$ 'LIST (CDR L) VA)))))

This conjecture simplifies, opening up NLISTP, EQUAL, and V&C$, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

V&C$-LIST-DEFN


(PROVE-LEMMA V&C$-DEFN NIL
             (EQUAL (V&C$ T X VA)
                    (IF (LITATOM X)
                        (CONS (CDR (ASSOC X VA)) 0)
                        (IF (NLISTP X)
                            (CONS X 0)
                            (IF (EQUAL (CAR X) 'QUOTE)
                                (CONS (CADR X) 0)
                                (V&C-APPLY$ (CAR X)
                                            (V&C$ 'LIST (CDR X) VA)))))))

This conjecture simplifies, opening up the definitions of NLISTP, EQUAL, and
V&C$, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

V&C$-DEFN


(PROVE-LEMMA EQ-ARGS-GIVE-EQ-VALUES--APPLY-VERSION NIL
             (IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                           (EQUAL (STRIP-CARS ARGS1)
                                  (STRIP-CARS ARGS2))
                           (NOT (MEMBER F ARGS1))
                           (NOT (MEMBER F ARGS2)))
                      (AND (IFF (V&C-APPLY$ FN ARGS1)
                                (V&C-APPLY$ FN ARGS2))
                           (EQUAL (CAR (V&C-APPLY$ FN ARGS1))
                                  (CAR (V&C-APPLY$ FN ARGS2)))))
             ((ENABLE V&C-APPLY$)))

This simplifies, applying SUB1-ADD1, and expanding the functions FIX-COST,
PLUS, V&C-APPLY$, and AND, to 94 new conjectures:

Case 94.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (NOT (EQUAL FN 'IF))
                      (SUBRP FN))
                 (IFF (CONS (APPLY-SUBR FN (STRIP-CARS ARGS1))
                            (ADD1 (SUM-CDRS ARGS1)))
                      (CONS (APPLY-SUBR FN (STRIP-CARS ARGS1))
                            (ADD1 (SUM-CDRS ARGS2))))),

  which again simplifies, expanding the function IFF, to:

        T.

Case 93.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (NOT (CAR ARGS1)))
                 (IFF F F)),

  which again simplifies, applying CAR-NLISTP, and opening up the functions
  EQUAL and MEMBER, to:

        T.

Case 92.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (CAAR ARGS1)
                      (NOT (CADR ARGS1)))
                 (IFF F F)).

  But this again simplifies, applying CAR-NLISTP, and unfolding the
  definitions of EQUAL and MEMBER, to:

        T.

Case 91.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (NOT (CAAR ARGS1))
                      (NOT (CADDR ARGS1)))
                 (IFF F F)).

  But this again simplifies, rewriting with CAR-NLISTP, and unfolding the
  definitions of EQUAL and MEMBER, to:

        T.

Case 90.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (NOT (CAR ARGS1)))
                 (IFF F F)).

  But this again simplifies, applying CAR-NLISTP, and unfolding the
  definitions of EQUAL and MEMBER, to:

        T.

Case 89.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (CAAR ARGS1)
                      (NOT (CADR ARGS1)))
                 (IFF F F)).

  But this again simplifies, opening up the functions EQUAL and IFF, to:

        T.

Case 88.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (NOT (CAAR ARGS1))
                      (NOT (CADDR ARGS1)))
                 (IFF F F)),

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

        T.

Case 87.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (NOT (CAR ARGS1)))
                 (IFF F F)),

  which again simplifies, appealing to the lemma CAR-NLISTP, and opening up
  EQUAL and MEMBER, to:

        T.

Case 86.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (CAAR ARGS1)
                      (NOT (CADR ARGS1)))
                 (IFF F F)),

  which again simplifies, unfolding the definitions of EQUAL and IFF, to:

        T.

Case 85.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (NOT (CAAR ARGS1))
                      (NOT (CADDR ARGS1)))
                 (IFF F F)),

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

        T.

Case 84.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (NOT (EQUAL FN 'IF))
                      (NOT (SUBRP FN))
                      (NOT (V&C$ T
                                 (BODY FN)
                                 (PAIRLIST (FORMALS FN)
                                           (STRIP-CARS ARGS1)))))
                 (IFF F F)),

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

        T.

Case 83.(IMPLIES
         (AND (NOT (EQUAL FN 'QUOTE))
              (EQUAL (STRIP-CARS ARGS1)
                     (STRIP-CARS ARGS2))
              (NOT (MEMBER F ARGS1))
              (NOT (MEMBER F ARGS2))
              (NOT (EQUAL FN 'IF))
              (NOT (SUBRP FN))
              (V&C$ T
                    (BODY FN)
                    (PAIRLIST (FORMALS FN)
                              (STRIP-CARS ARGS1))))
         (IFF
             (CONS (CAR (V&C$ T
                              (BODY FN)
                              (PAIRLIST (FORMALS FN)
                                        (STRIP-CARS ARGS1))))
                   (ADD1 (PLUS (SUM-CDRS ARGS1)
                               (CDR (V&C$ T
                                          (BODY FN)
                                          (PAIRLIST (FORMALS FN)
                                                    (STRIP-CARS ARGS1)))))))
             (CONS (CAR (V&C$ T
                              (BODY FN)
                              (PAIRLIST (FORMALS FN)
                                        (STRIP-CARS ARGS1))))
                   (ADD1 (PLUS (SUM-CDRS ARGS2)
                               (CDR (V&C$ T
                                          (BODY FN)
                                          (PAIRLIST (FORMALS FN)
                                                    (STRIP-CARS ARGS1))))))))),

  which again simplifies, opening up the definition of IFF, to:

        T.

Case 82.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS 0 (CDADDR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))),

  which again simplifies, unfolding EQUAL, PLUS, and IFF, to:

        T.

Case 81.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADDR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))),

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

        T.

Case 80.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (NOT (CAR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))),

  which again simplifies, rewriting with the lemma CAR-NLISTP, and opening up
  the definitions of EQUAL and MEMBER, to:

        T.

Case 79.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAAR ARGS1)
                      (NOT (CADR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))),

  which again simplifies, unfolding the functions EQUAL, PLUS, and IFF, to the
  conjecture:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAAR ARGS1))
                 (CADR ARGS1)).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  We must thus prove seven new formulas:

  Case 79.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAR ARGS2)
                        (NOT (CAAR ARGS2))
                        (CADDR ARGS2)
                        (NOT (NUMBERP (CDAR ARGS2)))
                        (CAAR ARGS1))
                   (CADR ARGS1)),

    which further simplifies, rewriting with CAR-NLISTP, and opening up
    STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 79.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        X
                        (NOT (CAR X))
                        (CADR Z)
                        (NOT (NUMBERP (CDR X)))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    But this further simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
    and opening up the functions STRIP-CARS, CONS, and MEMBER, to:

          T.

  Case 79.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        X
                        (NOT (CAR X))
                        (CAR V)
                        (NOT (NUMBERP (CDR X)))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    But this further simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
    and expanding the functions STRIP-CARS and MEMBER, to:

          T.

  Case 79.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        X
                        (NOT (CAR X))
                        Z
                        (NOT (NUMBERP (CDR X)))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    However this further simplifies, applying CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up STRIP-CARS and MEMBER, to:

          T.

  Case 79.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (CADR Z)
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    But this further simplifies, applying CDR-CONS, CAR-CONS, and CDR-NLISTP,
    and unfolding the functions STRIP-CARS, CONS, MEMBER, and CAR, to:

          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1) (LIST F))
                        (NOT (MEMBER F ARGS1))
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS D C) to eliminate (CAR X) and
    (CDR X), V by (CONS X X1) to eliminate (CAR V) and (CDR V), and V by
    (CONS D C) to eliminate (CAR V) and (CDR V).  We thus obtain the following
    five new goals:

    Case 79.3.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS ARGS1) (LIST F))
                          (NOT (MEMBER F ARGS1))
                          (NOT (NUMBERP W))
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      This finally simplifies, expanding the definitions of STRIP-CARS and
      EQUAL, to:

            T.

    Case 79.3.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X V)))
                          (NOT (NUMBERP W))
                          (CAR X))
                     (CAR V)),

      which finally simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and unfolding the functions STRIP-CARS, CONS, and EQUAL, to:

            T.

    Case 79.3.3.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS D C)))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X (CONS D C))))
                          (NOT (NUMBERP W))
                          (CAR X))
                     D).

      But this finally simplifies, appealing to the lemmas CDR-CONS,
      CAR-NLISTP, and CAR-CONS, and expanding the definitions of STRIP-CARS,
      CAR, and EQUAL, to:

            T.

    Case 79.3.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS (CONS D C) V)))
                          (NOT (NUMBERP W))
                          D)
                     (CAR V)),

      which finally simplifies, rewriting with CDR-CONS and CAR-CONS, and
      expanding the definitions of STRIP-CARS and CAR, to:

            T.

    Case 79.3.1.
            (IMPLIES (AND (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) (CONS X X1)))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C) (CONS X X1))))
                          (NOT (NUMBERP W))
                          D)
                     X).

      This finally simplifies, applying CDR-CONS and CAR-CONS, and unfolding
      the definitions of STRIP-CARS and CAR, to:

            T.

  Case 79.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (CAR X)
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    This further simplifies, applying CDR-CONS, CAR-CONS, and CAR-NLISTP, and
    expanding STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (LIST F (CAR D)))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS V Z) to eliminate
    (CDR ARGS1) and (CAR ARGS1), V by (CONS C X1) to eliminate (CAR V) and
    (CDR V), Z by (CONS V Z1) to eliminate (CAR Z) and (CDR Z), and Z by
    (CONS C X1) to eliminate (CAR Z) and (CDR Z).  We thus obtain the
    following five new conjectures:

    Case 79.2.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (NUMBERP W))
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      However this finally simplifies, unfolding STRIP-CARS, to:

            T.

    Case 79.2.4.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V Z)))
                          D
                          (NOT (NUMBERP W))
                          (CAR V))
                     (CAR Z)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and unfolding the definitions of STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 79.2.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS C X1)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V (CONS C X1))))
                          D
                          (NOT (NUMBERP W))
                          (CAR V))
                     C).

      This finally simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and unfolding the definitions of STRIP-CARS, CAR, and EQUAL,
      to:

            T.

    Case 79.2.2.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS (CONS C X1) Z)))
                          D
                          (NOT (NUMBERP W))
                          C)
                     (CAR Z)).

      However this finally simplifies, applying CDR-CONS and CAR-CONS, and
      unfolding STRIP-CARS, to:

            T.

    Case 79.2.1.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) (CONS V Z1)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1) (CONS V Z1))))
                          D
                          (NOT (NUMBERP W))
                          C)
                     V).

      However this finally simplifies, applying CDR-CONS and CAR-CONS, and
      opening up the definitions of STRIP-CARS and CAR, to:

            T.

  Case 79.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        Z
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    However this further simplifies, rewriting with CDR-CONS and CAR-CONS, and
    expanding STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (CONS F
                                     (CONS (CAR D)
                                           (CONS (CAR Z) (STRIP-CARS C)))))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (MEMBER F C))
                        Z
                        (NOT (NUMBERP W))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS X1 Z1) to eliminate (CAR X) and
    (CDR X), V by (CONS X V1) to eliminate (CAR V) and (CDR V), and V by
    (CONS X1 Z1) to eliminate (CAR V) and (CDR V).  We thus obtain the
    following five new goals:

    Case 79.1.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      However this finally simplifies, expanding the function STRIP-CARS, to:

            T.

    Case 79.1.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (CAR X))
                     (CAR V)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and unfolding the functions STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 79.1.3.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS X1 Z1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X (CONS X1 Z1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (CAR X))
                     X1).

      However this finally simplifies, applying CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and expanding the functions STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 79.1.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS (CONS X1 Z1) V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          X1)
                     (CAR V)).

      But this finally simplifies, rewriting with CDR-CONS and CAR-CONS, and
      expanding the definition of STRIP-CARS, to:

            T.

    Case 79.1.1.
            (IMPLIES (AND (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) (CONS X V1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1) (CONS X V1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          X1)
                     X).

      This finally simplifies, rewriting with CDR-CONS and CAR-CONS, and
      opening up the functions STRIP-CARS and CAR, to:

            T.

Case 78.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (NOT (CAAR ARGS1))
                      (NOT (CADDR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))).

  But this again simplifies, opening up the functions EQUAL, PLUS, and IFF, to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (NOT (CAAR ARGS1)))
                 (CADDR ARGS1)).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  We must thus prove seven new conjectures:

  Case 78.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAR ARGS2)
                        (NOT (CAAR ARGS2))
                        (CADDR ARGS2)
                        (NOT (NUMBERP (CDAR ARGS2)))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)),

    which further simplifies, applying CAR-NLISTP, and opening up STRIP-CARS,
    MEMBER, and CAR, to:

          T.

  Case 78.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        X
                        (NOT (CAR X))
                        (CADR Z)
                        (NOT (NUMBERP (CDR X)))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, applying the lemmas CDR-CONS, CAR-NLISTP,
    and CAR-CONS, and unfolding the definitions of STRIP-CARS, CONS, and
    MEMBER, to:

          T.

  Case 78.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        X
                        (NOT (CAR X))
                        (CAR V)
                        (NOT (NUMBERP (CDR X)))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)),

    which further simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
    and CAR-CONS, and opening up the definitions of STRIP-CARS and MEMBER, to:

          T.

  Case 78.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        X
                        (NOT (CAR X))
                        Z
                        (NOT (NUMBERP (CDR X)))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)),

    which further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up the functions STRIP-CARS and MEMBER, to:

          T.

  Case 78.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (CADR Z)
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, rewriting with CDR-CONS, CAR-CONS, and
    CDR-NLISTP, and opening up the definitions of STRIP-CARS, CONS, MEMBER,
    and CAR, to:

          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1) (LIST F))
                        (NOT (MEMBER F ARGS1))
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS D C) to eliminate (CAR X) and
    (CDR X), V by (CONS X1 X) to eliminate (CDR V) and (CAR V), X by
    (CONS V Z1) to eliminate (CAR X) and (CDR X), V by (CONS C D) to eliminate
    (CDR V) and (CAR V), and D by (CONS V X1) to eliminate (CAR D) and (CDR D).
    This produces the following seven new formulas:

    Case 78.3.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS ARGS1) (LIST F))
                          (NOT (MEMBER F ARGS1))
                          (NOT (NUMBERP W))
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)).

      However this finally simplifies, expanding the definitions of STRIP-CARS
      and EQUAL, to:

            T.

    Case 78.3.6.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X V)))
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     (CADR V)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and opening up STRIP-CARS, CONS, and EQUAL, to:

            T.

    Case 78.3.5.
            (IMPLIES (AND (NOT (LISTP D))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS C D)))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X (CONS C D))))
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     (CAR D)).

      However this finally simplifies, applying CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and opening up the definitions of STRIP-CARS, CAR, and EQUAL,
      to:

            T.

    Case 78.3.4.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS C (CONS V X1))))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS X (CONS C (CONS V X1)))))
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     V).

      This finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and expanding the functions STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 78.3.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS (CONS D C) V)))
                          (NOT (NUMBERP W))
                          (NOT D))
                     (CADR V)),

      which further simplifies, applying the lemmas CDR-CONS, CAR-CONS, and
      CDR-NLISTP, and expanding the functions STRIP-CARS, CONS, EQUAL, MEMBER,
      and CAR, to:

            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (NOT (NUMBERP W)))
                     0).

      This finally simplifies, trivially, to:

            T.

    Case 78.3.2.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) (CONS X1 X)))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C) (CONS X1 X))))
                          (NOT (NUMBERP W))
                          (NOT D))
                     (CAR X)).

      However this finally simplifies, rewriting with CDR-CONS and CAR-CONS,
      and unfolding STRIP-CARS, CAR, EQUAL, and CDR, to:

            T.

    Case 78.3.1.
            (IMPLIES (AND (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C)
                                                   (CONS X1 (CONS V Z1))))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C)
                                             (CONS X1 (CONS V Z1)))))
                          (NOT (NUMBERP W))
                          (NOT D))
                     V).

      But this finally simplifies, applying CDR-CONS and CAR-CONS, and
      expanding the functions STRIP-CARS, CAR, EQUAL, and CDR, to:

            T.

  Case 78.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (CAR X)
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    But this further simplifies, appealing to the lemmas CDR-CONS, CAR-CONS,
    and CAR-NLISTP, and unfolding the definitions of STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (LIST F (CAR D)))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS1 by (CONS V Z) to
    eliminate (CDR ARGS1) and (CAR ARGS1), V by (CONS C X1) to eliminate
    (CAR V) and (CDR V), Z by (CONS Z1 V) to eliminate (CDR Z) and (CAR Z), V
    by (CONS Z V1) to eliminate (CAR V) and (CDR V), Z by (CONS X1 C) to
    eliminate (CDR Z) and (CAR Z), and C by (CONS Z Z1) to eliminate (CAR C)
    and (CDR C).  We must thus prove seven new goals:

    Case 78.2.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (NUMBERP W))
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)),

      which finally simplifies, unfolding the definition of STRIP-CARS, to:

            T.

    Case 78.2.6.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V Z)))
                          D
                          (NOT (NUMBERP W))
                          (NOT (CAR V)))
                     (CADR Z)),

      which finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and expanding the definitions of STRIP-CARS, CONS, CAR,
      and EQUAL, to:

            T.

    Case 78.2.5.
            (IMPLIES (AND (NOT (LISTP C))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS X1 C)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V (CONS X1 C))))
                          D
                          (NOT (NUMBERP W))
                          (NOT (CAR V)))
                     (CAR C)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and expanding the definitions of STRIP-CARS and EQUAL, to:

            T.

    Case 78.2.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS X1 (CONS Z Z1))))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS V (CONS X1 (CONS Z Z1)))))
                          D
                          (NOT (NUMBERP W))
                          (NOT (CAR V)))
                     Z).

      This finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and opening up the functions STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 78.2.3.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS (CONS C X1) Z)))
                          D
                          (NOT (NUMBERP W))
                          (NOT C))
                     (CADR Z)).

      However this finally simplifies, rewriting with CDR-CONS and CAR-CONS,
      and opening up the functions STRIP-CARS, CONS, CAR, EQUAL, and CDR, to:

            T.

    Case 78.2.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) (CONS Z1 V)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1) (CONS Z1 V))))
                          D
                          (NOT (NUMBERP W))
                          (NOT C))
                     (CAR V)).

      But this further simplifies, rewriting with the lemmas CDR-CONS,
      CAR-CONS, CONS-EQUAL, and CAR-NLISTP, and opening up STRIP-CARS, EQUAL,
      and MEMBER, to:

            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (CAR Z1) (CAR D))
                          Z1 D
                          (NOT (NUMBERP W)))
                     0).

      This finally simplifies, clearly, to:

            T.

    Case 78.2.1.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1)
                                                   (CONS Z1 (CONS Z V1))))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1)
                                             (CONS Z1 (CONS Z V1)))))
                          D
                          (NOT (NUMBERP W))
                          (NOT C))
                     Z).

      However this finally simplifies, applying CDR-CONS, CAR-CONS, and
      CONS-EQUAL, and opening up the functions STRIP-CARS, CAR, and EQUAL, to:

            T.

  Case 78.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        Z
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, appealing to the lemmas CDR-CONS and
    CAR-CONS, and opening up STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (CONS F
                                     (CONS (CAR D)
                                           (CONS (CAR Z) (STRIP-CARS C)))))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (MEMBER F C))
                        Z
                        (NOT (NUMBERP W))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS1 by (CONS X V) to
    eliminate (CAR ARGS1) and (CDR ARGS1), X by (CONS X1 Z1) to eliminate
    (CAR X) and (CDR X), V by (CONS V1 X) to eliminate (CDR V) and (CAR V), X
    by (CONS V W1) to eliminate (CAR X) and (CDR X), V by (CONS Z1 X1) to
    eliminate (CDR V) and (CAR V), and X1 by (CONS V V1) to eliminate (CAR X1)
    and (CDR X1).  This generates seven new conjectures:

    Case 78.1.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)),

      which finally simplifies, opening up the function STRIP-CARS, to:

            T.

    Case 78.1.6.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     (CADR V)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and expanding STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 78.1.5.
            (IMPLIES (AND (NOT (LISTP X1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS Z1 X1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X (CONS Z1 X1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     (CAR X1)).

      But this finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and unfolding the functions STRIP-CARS and EQUAL, to:

            T.

    Case 78.1.4.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS Z1 (CONS V V1))))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS X (CONS Z1 (CONS V V1)))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT (CAR X)))
                     V).

      However this finally simplifies, rewriting with CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and opening up the definitions of STRIP-CARS, CAR, and
      EQUAL, to:

            T.

    Case 78.1.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS (CONS X1 Z1) V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT X1))
                     (CADR V)).

      However this finally simplifies, rewriting with CDR-CONS and CAR-CONS,
      and unfolding STRIP-CARS, CONS, CAR, EQUAL, and CDR, to:

            T.

    Case 78.1.2.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) (CONS V1 X)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1) (CONS V1 X))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT X1))
                     (CAR X)).

      But this finally simplifies, rewriting with CDR-CONS, CAR-CONS, and
      CONS-EQUAL, and opening up STRIP-CARS and EQUAL, to:

            T.

    Case 78.1.1.
            (IMPLIES (AND (EQUAL (STRIP-CARS (CONS (CONS X1 Z1)
                                                   (CONS V1 (CONS V W1))))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1)
                                             (CONS V1 (CONS V W1)))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NOT (NUMBERP W))
                          (NOT X1))
                     V).

      This finally simplifies, rewriting with CDR-CONS, CAR-CONS, and
      CONS-EQUAL, and expanding the definitions of STRIP-CARS, CAR, EQUAL, and
      MEMBER, to:

            T.

Case 77.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAR ARGS1)
                      (CAAR ARGS1)
                      (CADR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADR ARGS1)
                            (ADD1 (PLUS 0 (CDADR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))).

  However this again simplifies, expanding EQUAL, PLUS, and IFF, to:

        T.

Case 76.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NOT (NUMBERP (CDAR ARGS2)))
                      (CAR ARGS1)
                      (CAAR ARGS1)
                      (CADR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS 0 (CDADDR ARGS2)))))),

  which again simplifies, unfolding EQUAL, PLUS, and IFF, to:

        T.

Case 75.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS 0 (CDADDR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

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

        T.

Case 74.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADDR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

  which again simplifies, expanding EQUAL and IFF, to:

        T.

Case 73.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (NOT (CAR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

  which again simplifies, applying CAR-NLISTP, and unfolding EQUAL and MEMBER,
  to:

        T.

Case 72.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAAR ARGS1)
                      (NOT (CADR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))).

  However this again simplifies, expanding EQUAL and IFF, to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAAR ARGS1))
                 (CADR ARGS1)).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  This generates seven new goals:

  Case 72.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAR ARGS2)
                        (NOT (CAAR ARGS2))
                        (CADDR ARGS2)
                        (NUMBERP (CDAR ARGS2))
                        (CAAR ARGS1))
                   (CADR ARGS1)),

    which further simplifies, rewriting with CAR-NLISTP, and opening up
    STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 72.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        X
                        (NOT (CAR X))
                        (CADR Z)
                        (NUMBERP (CDR X))
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    But this further simplifies, rewriting with the lemmas CDR-CONS,
    CAR-NLISTP, and CAR-CONS, and unfolding the definitions of STRIP-CARS,
    CONS, and MEMBER, to:

          T.

  Case 72.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        X
                        (NOT (CAR X))
                        (CAR V)
                        (NUMBERP (CDR X))
                        (CAAR ARGS1))
                   (CADR ARGS1)),

    which further simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
    and CAR-CONS, and unfolding the definitions of STRIP-CARS and MEMBER, to:

          T.

  Case 72.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        X
                        (NOT (CAR X))
                        Z
                        (NUMBERP (CDR X))
                        (CAAR ARGS1))
                   (CADR ARGS1)),

    which further simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS, and
    unfolding STRIP-CARS and MEMBER, to:

          T.

  Case 72.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (CADR Z)
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    This further simplifies, applying CDR-CONS, CAR-CONS, and CDR-NLISTP, and
    expanding STRIP-CARS, CONS, MEMBER, and CAR, to:

          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1) (LIST F))
                        (NOT (MEMBER F ARGS1))
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS D C) to eliminate (CAR X) and
    (CDR X), V by (CONS X X1) to eliminate (CAR V) and (CDR V), and V by
    (CONS D C) to eliminate (CAR V) and (CDR V).  This produces the following
    five new goals:

    Case 72.3.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS ARGS1) (LIST F))
                          (NOT (MEMBER F ARGS1))
                          (NUMBERP W)
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      But this finally simplifies, unfolding the functions STRIP-CARS and
      EQUAL, to:

            T.

    Case 72.3.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X V)))
                          (NUMBERP W)
                          (CAR X))
                     (CAR V)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and opening up the definitions of STRIP-CARS, CONS, and EQUAL, to:

            T.

    Case 72.3.3.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS D C)))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X (CONS D C))))
                          (NUMBERP W)
                          (CAR X))
                     D).

      But this finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and expanding the definitions of STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 72.3.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS (CONS D C) V)))
                          (NUMBERP W)
                          D)
                     (CAR V)).

      But this finally simplifies, rewriting with CDR-CONS and CAR-CONS, and
      unfolding the functions STRIP-CARS and CAR, to:

            T.

    Case 72.3.1.
            (IMPLIES (AND (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) (CONS X X1)))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C) (CONS X X1))))
                          (NUMBERP W)
                          D)
                     X).

      However this finally simplifies, rewriting with CDR-CONS and CAR-CONS,
      and expanding the functions STRIP-CARS and CAR, to:

            T.

  Case 72.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (CAR X)
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    However this further simplifies, applying CDR-CONS, CAR-CONS, and
    CAR-NLISTP, and opening up the functions STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (LIST F (CAR D)))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS V Z) to eliminate
    (CDR ARGS1) and (CAR ARGS1), V by (CONS C X1) to eliminate (CAR V) and
    (CDR V), Z by (CONS V Z1) to eliminate (CAR Z) and (CDR Z), and Z by
    (CONS C X1) to eliminate (CAR Z) and (CDR Z).  This produces the following
    five new goals:

    Case 72.2.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NUMBERP W)
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      But this finally simplifies, unfolding the definition of STRIP-CARS, to:

            T.

    Case 72.2.4.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V Z)))
                          D
                          (NUMBERP W)
                          (CAR V))
                     (CAR Z)),

      which finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and unfolding STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 72.2.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS C X1)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V (CONS C X1))))
                          D
                          (NUMBERP W)
                          (CAR V))
                     C),

      which finally simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and expanding STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 72.2.2.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS (CONS C X1) Z)))
                          D
                          (NUMBERP W)
                          C)
                     (CAR Z)).

      This finally simplifies, applying CDR-CONS and CAR-CONS, and expanding
      the function STRIP-CARS, to:

            T.

    Case 72.2.1.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) (CONS V Z1)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1) (CONS V Z1))))
                          D
                          (NUMBERP W)
                          C)
                     V).

      But this finally simplifies, applying CDR-CONS and CAR-CONS, and
      unfolding STRIP-CARS and CAR, to:

            T.

  Case 72.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        Z
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    But this further simplifies, rewriting with CDR-CONS and CAR-CONS, and
    expanding the definitions of STRIP-CARS and MEMBER, to the new formula:

          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (CONS F
                                     (CONS (CAR D)
                                           (CONS (CAR Z) (STRIP-CARS C)))))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (MEMBER F C))
                        Z
                        (NUMBERP W)
                        (CAAR ARGS1))
                   (CADR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS X1 Z1) to eliminate (CAR X) and
    (CDR X), V by (CONS X V1) to eliminate (CAR V) and (CDR V), and V by
    (CONS X1 Z1) to eliminate (CAR V) and (CDR V).  We thus obtain the
    following five new conjectures:

    Case 72.1.5.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (CAAR ARGS1))
                     (CADR ARGS1)).

      However this finally simplifies, unfolding the definition of STRIP-CARS,
      to:

            T.

    Case 72.1.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (CAR X))
                     (CAR V)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and opening up STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 72.1.3.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS X1 Z1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X (CONS X1 Z1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (CAR X))
                     X1).

      But this finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and opening up the definitions of STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 72.1.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS (CONS X1 Z1) V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          X1)
                     (CAR V)).

      But this finally simplifies, applying CDR-CONS and CAR-CONS, and
      expanding the definition of STRIP-CARS, to:

            T.

    Case 72.1.1.
            (IMPLIES (AND (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) (CONS X V1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1) (CONS X V1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          X1)
                     X).

      However this finally simplifies, appealing to the lemmas CDR-CONS and
      CAR-CONS, and unfolding the functions STRIP-CARS and CAR, to:

            T.

Case 71.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (NOT (CAAR ARGS1))
                      (NOT (CADDR ARGS1)))
                 (IFF F
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

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

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (NOT (CAAR ARGS1)))
                 (CADDR ARGS1)).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  The result is seven new conjectures:

  Case 71.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAR ARGS2)
                        (NOT (CAAR ARGS2))
                        (CADDR ARGS2)
                        (NUMBERP (CDAR ARGS2))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)),

    which further simplifies, rewriting with CAR-NLISTP, and opening up the
    functions STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 71.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        X
                        (NOT (CAR X))
                        (CADR Z)
                        (NUMBERP (CDR X))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and unfolding the definitions of STRIP-CARS, CONS, and MEMBER,
    to:

          T.

  Case 71.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        X
                        (NOT (CAR X))
                        (CAR V)
                        (NUMBERP (CDR X))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and unfolding the functions STRIP-CARS and MEMBER, to:

          T.

  Case 71.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        X
                        (NOT (CAR X))
                        Z
                        (NUMBERP (CDR X))
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, applying CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up STRIP-CARS and MEMBER, to:

          T.

  Case 71.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (CADR Z)
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, rewriting with CDR-CONS, CAR-CONS, and
    CDR-NLISTP, and opening up the functions STRIP-CARS, CONS, MEMBER, and CAR,
    to:

          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1) (LIST F))
                        (NOT (MEMBER F ARGS1))
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS D C) to eliminate (CAR X) and
    (CDR X), V by (CONS X1 X) to eliminate (CDR V) and (CAR V), X by
    (CONS V Z1) to eliminate (CAR X) and (CDR X), V by (CONS C D) to eliminate
    (CDR V) and (CAR V), and D by (CONS V X1) to eliminate (CAR D) and (CDR D).
    We thus obtain the following seven new goals:

    Case 71.3.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS ARGS1) (LIST F))
                          (NOT (MEMBER F ARGS1))
                          (NUMBERP W)
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)).

      But this finally simplifies, opening up STRIP-CARS and EQUAL, to:

            T.

    Case 71.3.6.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X V)))
                          (NUMBERP W)
                          (NOT (CAR X)))
                     (CADR V)),

      which finally simplifies, applying the lemmas CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and opening up STRIP-CARS, CONS, and EQUAL, to:

            T.

    Case 71.3.5.
            (IMPLIES (AND (NOT (LISTP D))
                          (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS C D)))
                                 (LIST F))
                          (NOT (MEMBER F (CONS X (CONS C D))))
                          (NUMBERP W)
                          (NOT (CAR X)))
                     (CAR D)),

      which finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and unfolding the definitions of STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 71.3.4.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS X (CONS C (CONS V X1))))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS X (CONS C (CONS V X1)))))
                          (NUMBERP W)
                          (NOT (CAR X)))
                     V).

      But this finally simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
      and expanding the definitions of STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 71.3.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) V))
                                 (LIST F))
                          (NOT (MEMBER F (CONS (CONS D C) V)))
                          (NUMBERP W)
                          (NOT D))
                     (CADR V)).

      However this further simplifies, rewriting with the lemmas CDR-CONS,
      CAR-CONS, and CDR-NLISTP, and opening up STRIP-CARS, CONS, EQUAL, MEMBER,
      and CAR, to the conjecture:

            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP Z))
                          (NUMBERP W))
                     0).

      This finally simplifies, clearly, to:

            T.

    Case 71.3.2.
            (IMPLIES (AND (NOT (LISTP X))
                          (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C) (CONS X1 X)))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C) (CONS X1 X))))
                          (NUMBERP W)
                          (NOT D))
                     (CAR X)).

      But this finally simplifies, applying CDR-CONS and CAR-CONS, and
      expanding the definitions of STRIP-CARS, CAR, EQUAL, and CDR, to:

            T.

    Case 71.3.1.
            (IMPLIES (AND (NOT (LISTP Z))
                          (EQUAL (STRIP-CARS (CONS (CONS D C)
                                                   (CONS X1 (CONS V Z1))))
                                 (LIST F))
                          (NOT (MEMBER F
                                       (CONS (CONS D C)
                                             (CONS X1 (CONS V Z1)))))
                          (NUMBERP W)
                          (NOT D))
                     V).

      But this finally simplifies, appealing to the lemmas CDR-CONS and
      CAR-CONS, and expanding the functions STRIP-CARS, CAR, EQUAL, and CDR,
      to:

            T.

  Case 71.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (CAR X)
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)),

    which further simplifies, applying CDR-CONS, CAR-CONS, and CAR-NLISTP, and
    expanding the functions STRIP-CARS and MEMBER, to the new conjecture:

          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (LIST F (CAR D)))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS V Z) to eliminate
    (CDR ARGS1) and (CAR ARGS1), V by (CONS C X1) to eliminate (CAR V) and
    (CDR V), Z by (CONS Z1 V) to eliminate (CDR Z) and (CAR Z), V by
    (CONS Z V1) to eliminate (CAR V) and (CDR V), Z by (CONS X1 C) to
    eliminate (CDR Z) and (CAR Z), and C by (CONS Z Z1) to eliminate (CAR C)
    and (CDR C).  We would thus like to prove the following seven new goals:

    Case 71.2.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NUMBERP W)
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)).

      This finally simplifies, opening up the function STRIP-CARS, to:

            T.

    Case 71.2.6.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V Z)))
                          D
                          (NUMBERP W)
                          (NOT (CAR V)))
                     (CADR Z)),

      which finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and opening up the definitions of STRIP-CARS, CONS, CAR,
      and EQUAL, to:

            T.

    Case 71.2.5.
            (IMPLIES (AND (NOT (LISTP C))
                          (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS X1 C)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS V (CONS X1 C))))
                          D
                          (NUMBERP W)
                          (NOT (CAR V)))
                     (CAR C)),

      which finally simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and unfolding the definitions of STRIP-CARS and EQUAL, to:

            T.

    Case 71.2.4.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS V (CONS X1 (CONS Z Z1))))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS V (CONS X1 (CONS Z Z1)))))
                          D
                          (NUMBERP W)
                          (NOT (CAR V)))
                     Z).

      But this finally simplifies, applying the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and opening up the definitions of STRIP-CARS, CAR, and
      EQUAL, to:

            T.

    Case 71.2.3.
            (IMPLIES (AND (NOT (LISTP Z))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) Z))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F (CONS (CONS C X1) Z)))
                          D
                          (NUMBERP W)
                          (NOT C))
                     (CADR Z)),

      which finally simplifies, rewriting with CDR-CONS and CAR-CONS, and
      unfolding the definitions of STRIP-CARS, CONS, CAR, EQUAL, and CDR, to:

            T.

    Case 71.2.2.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1) (CONS Z1 V)))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1) (CONS Z1 V))))
                          D
                          (NUMBERP W)
                          (NOT C))
                     (CAR V)).

      This further simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS,
      CONS-EQUAL, and CAR-NLISTP, and unfolding the definitions of STRIP-CARS,
      EQUAL, and MEMBER, to the goal:

            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (CAR Z1) (CAR D))
                          Z1 D
                          (NUMBERP W))
                     0).

      This finally simplifies, clearly, to:

            T.

    Case 71.2.1.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS C X1)
                                                   (CONS Z1 (CONS Z V1))))
                                 (LIST F (CAR D)))
                          (NOT (MEMBER F
                                       (CONS (CONS C X1)
                                             (CONS Z1 (CONS Z V1)))))
                          D
                          (NUMBERP W)
                          (NOT C))
                     Z).

      However this finally simplifies, applying CDR-CONS, CAR-CONS, and
      CONS-EQUAL, and unfolding STRIP-CARS, CAR, and EQUAL, to:

            T.

  Case 71.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        Z
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    However this further simplifies, applying CDR-CONS and CAR-CONS, and
    expanding the functions STRIP-CARS and MEMBER, to:

          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (CONS F
                                     (CONS (CAR D)
                                           (CONS (CAR Z) (STRIP-CARS C)))))
                        (NOT (MEMBER F ARGS1))
                        D
                        (NOT (MEMBER F C))
                        Z
                        (NUMBERP W)
                        (NOT (CAAR ARGS1)))
                   (CADDR ARGS1)).

    Applying the lemma CAR-CDR-ELIM, replace ARGS1 by (CONS X V) to eliminate
    (CAR ARGS1) and (CDR ARGS1), X by (CONS X1 Z1) to eliminate (CAR X) and
    (CDR X), V by (CONS V1 X) to eliminate (CDR V) and (CAR V), X by
    (CONS V W1) to eliminate (CAR X) and (CDR X), V by (CONS Z1 X1) to
    eliminate (CDR V) and (CAR V), and X1 by (CONS V V1) to eliminate (CAR X1)
    and (CDR X1).  We would thus like to prove the following seven new
    conjectures:

    Case 71.1.7.
            (IMPLIES (AND (NOT (LISTP ARGS1))
                          (EQUAL (STRIP-CARS ARGS1)
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F ARGS1))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT (CAAR ARGS1)))
                     (CADDR ARGS1)).

      This finally simplifies, unfolding STRIP-CARS, to:

            T.

    Case 71.1.6.
            (IMPLIES (AND (NOT (LISTP V))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT (CAR X)))
                     (CADR V)),

      which finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and expanding STRIP-CARS, CONS, CAR, and EQUAL, to:

            T.

    Case 71.1.5.
            (IMPLIES (AND (NOT (LISTP X1))
                          (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS Z1 X1)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS X (CONS Z1 X1))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT (CAR X)))
                     (CAR X1)),

      which finally simplifies, applying the lemmas CDR-CONS, CAR-NLISTP, and
      CAR-CONS, and opening up the functions STRIP-CARS and EQUAL, to:

            T.

    Case 71.1.4.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS X (CONS Z1 (CONS V V1))))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS X (CONS Z1 (CONS V V1)))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT (CAR X)))
                     V),

      which finally simplifies, rewriting with the lemmas CDR-CONS, CAR-NLISTP,
      and CAR-CONS, and expanding the functions STRIP-CARS, CAR, and EQUAL, to:

            T.

    Case 71.1.3.
            (IMPLIES (AND (NOT (LISTP V))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) V))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F (CONS (CONS X1 Z1) V)))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT X1))
                     (CADR V)),

      which finally simplifies, appealing to the lemmas CDR-CONS and CAR-CONS,
      and opening up STRIP-CARS, CONS, CAR, EQUAL, and CDR, to:

            T.

    Case 71.1.2.
            (IMPLIES (AND (NOT (LISTP X))
                          (EQUAL (STRIP-CARS (CONS (CONS X1 Z1) (CONS V1 X)))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1) (CONS V1 X))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT X1))
                     (CAR X)),

      which finally simplifies, applying the lemmas CDR-CONS, CAR-CONS, and
      CONS-EQUAL, and expanding the definitions of STRIP-CARS and EQUAL, to:

            T.

    Case 71.1.1.
            (IMPLIES (AND (EQUAL (STRIP-CARS (CONS (CONS X1 Z1)
                                                   (CONS V1 (CONS V W1))))
                                 (CONS F
                                       (CONS (CAR D)
                                             (CONS (CAR Z) (STRIP-CARS C)))))
                          (NOT (MEMBER F
                                       (CONS (CONS X1 Z1)
                                             (CONS V1 (CONS V W1)))))
                          D
                          (NOT (MEMBER F C))
                          Z
                          (NUMBERP W)
                          (NOT X1))
                     V),

      which finally simplifies, appealing to the lemmas CDR-CONS, CAR-CONS,
      and CONS-EQUAL, and expanding the functions STRIP-CARS, CAR, EQUAL, and
      MEMBER, to:

            T.

Case 70.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAR ARGS1)
                      (CAAR ARGS1)
                      (CADR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADR ARGS1)
                            (ADD1 (PLUS 0 (CDADR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

  which again simplifies, unfolding EQUAL, PLUS, and IFF, to:

        T.

Case 69.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAR ARGS2)
                      (NOT (CAAR ARGS2))
                      (CADDR ARGS2)
                      (NUMBERP (CDAR ARGS2))
                      (CAR ARGS1)
                      (CAAR ARGS1)
                      (CADR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADR ARGS1))))
                      (CONS (CAADDR ARGS2)
                            (ADD1 (PLUS (CDAR ARGS2)
                                        (CDADDR ARGS2)))))),

  which again simplifies, expanding EQUAL and IFF, to:

        T.

Case 68.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS 0 (CDADDR ARGS1))))
                      F)),

  which again simplifies, rewriting with CAR-NLISTP, and opening up the
  functions EQUAL and MEMBER, to:

        T.

Case 67.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS 0 (CDADDR ARGS1))))
                      F)).

  However this again simplifies, unfolding the functions EQUAL, PLUS, and IFF,
  to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1))
                 (NUMBERP (CDAR ARGS1))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS X D) to eliminate (CAR Z) and (CDR Z), and Z by
  (CONS V W) to eliminate (CAR Z) and (CDR Z).  The result is five new
  conjectures:

  Case 67.5.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAAR ARGS2)
                        (NOT (CADR ARGS2))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))),

    which further simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
    opening up the definitions of STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 67.4.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        (CAR X)
                        (NOT (CAR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    This further simplifies, applying the lemmas CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and unfolding STRIP-CARS, CONS, and MEMBER, to:

          T.

  Case 67.3.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS V W))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS V W))))
                        (CAR X)
                        (NOT V)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))),

    which further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and expanding the functions STRIP-CARS, CAR, MEMBER, and EQUAL,
    to:

          T.

  Case 67.2.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        V
                        (NOT (CAR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    But this further simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS,
    and CAR-NLISTP, and opening up the functions STRIP-CARS and MEMBER, to:

          T.

  Case 67.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS X D))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS X D))))
                        V
                        (NOT X)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))),

    which further simplifies, applying CDR-CONS and CAR-CONS, and unfolding
    the definitions of STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

Case 66.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS 0 (CDADDR ARGS1))))
                      F)).

  However this again simplifies, unfolding EQUAL, PLUS, and IFF, to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1))
                 (NUMBERP (CDAR ARGS1))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  We must thus prove seven new goals:

  Case 66.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (NOT (CAAR ARGS2))
                        (NOT (CADDR ARGS2))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))),

    which further simplifies, rewriting with the lemma CAR-NLISTP, and
    expanding STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 66.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        (NOT (CAR X))
                        (NOT (CADR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))),

    which further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and expanding the definitions of STRIP-CARS, CONS, and MEMBER,
    to:

          T.

  Case 66.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        (NOT (CAR X))
                        (NOT (CAR V))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    However this further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up the definitions of STRIP-CARS and MEMBER, to:

          T.

  Case 66.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        (NOT (CAR X))
                        (NOT Z)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    But this further simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS,
    and unfolding the definitions of STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

  Case 66.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (NOT (CADR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    However this further simplifies, applying CDR-CONS, CAR-CONS, and
    CDR-NLISTP, and unfolding STRIP-CARS, CONS, MEMBER, and CAR, to:

          T.

  Case 66.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (NOT (CAR X))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    This further simplifies, rewriting with CDR-CONS, CAR-CONS, and CAR-NLISTP,
    and expanding the functions STRIP-CARS and MEMBER, to:

          T.

  Case 66.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        (NOT Z)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NUMBERP (CDAR ARGS1))).

    However this further simplifies, applying CDR-CONS and CAR-CONS, and
    unfolding the definitions of STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

Case 65.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADDR ARGS1))))
                      F)).

  However this again simplifies, applying CAR-NLISTP, and expanding the
  definitions of EQUAL and MEMBER, to:

        T.

Case 64.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADDR ARGS1))))
                      F)).

  This again simplifies, unfolding EQUAL and IFF, to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (CAAR ARGS2)
                      (NOT (CADR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1))
                 (NOT (NUMBERP (CDAR ARGS1)))).

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

  Case 64.5.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (CAAR ARGS2)
                        (NOT (CADR ARGS2))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))),

    which further simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP,
    and expanding STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 64.4.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        (CAR X)
                        (NOT (CAR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))),

    which further simplifies, applying CDR-CONS, CAR-NLISTP, and CAR-CONS, and
    unfolding the definitions of STRIP-CARS, CONS, and MEMBER, to:

          T.

  Case 64.3.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS V W))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS V W))))
                        (CAR X)
                        (NOT V)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    This further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and CAR-CONS,
    and unfolding the definitions of STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

  Case 64.2.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        V
                        (NOT (CAR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    But this further simplifies, rewriting with CDR-CONS, CAR-CONS, and
    CAR-NLISTP, and unfolding the functions STRIP-CARS and MEMBER, to:

          T.

  Case 64.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS X D))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS X D))))
                        V
                        (NOT X)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    This further simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
    functions STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

Case 63.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1)
                      (NUMBERP (CDAR ARGS1)))
                 (IFF (CONS (CAADDR ARGS1)
                            (ADD1 (PLUS (CDAR ARGS1) (CDADDR ARGS1))))
                      F)).

  But this again simplifies, expanding the functions EQUAL and IFF, to:

        (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (NOT (CAAR ARGS2))
                      (NOT (CADDR ARGS2))
                      (CAR ARGS1)
                      (NOT (CAAR ARGS1))
                      (CADDR ARGS1))
                 (NOT (NUMBERP (CDAR ARGS1)))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace ARGS2 by (CONS X Z) to
  eliminate (CAR ARGS2) and (CDR ARGS2), X by (CONS V W) to eliminate (CAR X)
  and (CDR X), Z by (CONS D X) to eliminate (CDR Z) and (CAR Z), X by
  (CONS Z C) to eliminate (CAR X) and (CDR X), Z by (CONS W V) to eliminate
  (CDR Z) and (CAR Z), and V by (CONS Z D) to eliminate (CAR V) and (CDR V).
  This generates seven new conjectures:

  Case 63.7.
          (IMPLIES (AND (NOT (LISTP ARGS2))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS ARGS2))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F ARGS2))
                        (NOT (CAAR ARGS2))
                        (NOT (CADDR ARGS2))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))),

    which further simplifies, rewriting with CAR-NLISTP, and opening up
    STRIP-CARS, MEMBER, and CAR, to:

          T.

  Case 63.6.
          (IMPLIES (AND (NOT (LISTP Z))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X Z)))
                        (NOT (CAR X))
                        (NOT (CADR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    This further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and CAR-CONS,
    and expanding STRIP-CARS, CONS, and MEMBER, to:

          T.

  Case 63.5.
          (IMPLIES (AND (NOT (LISTP V))
                        (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W V))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS X (CONS W V))))
                        (NOT (CAR X))
                        (NOT (CAR V))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    This further simplifies, appealing to the lemmas CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up STRIP-CARS and MEMBER, to:

          T.

  Case 63.4.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS X (CONS W (CONS Z D)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS X (CONS W (CONS Z D)))))
                        (NOT (CAR X))
                        (NOT Z)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))),

    which further simplifies, rewriting with CDR-CONS, CAR-NLISTP, and
    CAR-CONS, and opening up the functions STRIP-CARS, CAR, MEMBER, and EQUAL,
    to:

          T.

  Case 63.3.
          (IMPLIES (AND (NOT (LISTP Z))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) Z)))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F (CONS (CONS V W) Z)))
                        (NOT V)
                        (NOT (CADR Z))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    This further simplifies, applying CDR-CONS, CAR-CONS, and CDR-NLISTP, and
    opening up the definitions of STRIP-CARS, CONS, MEMBER, and CAR, to:

          T.

  Case 63.2.
          (IMPLIES (AND (NOT (LISTP X))
                        (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W) (CONS D X))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W) (CONS D X))))
                        (NOT V)
                        (NOT (CAR X))
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    However this further simplifies, rewriting with CDR-CONS, CAR-CONS, and
    CAR-NLISTP, and unfolding the definitions of STRIP-CARS and MEMBER, to:

          T.

  Case 63.1.
          (IMPLIES (AND (EQUAL (STRIP-CARS ARGS1)
                               (STRIP-CARS (CONS (CONS V W)
                                                 (CONS D (CONS Z C)))))
                        (NOT (MEMBER F ARGS1))
                        (NOT (MEMBER F
                                     (CONS (CONS V W)
                                           (CONS D (CONS Z C)))))
                        (NOT V)
                        (NOT Z)
                        (CAR ARGS1)
                        (NOT (CAAR ARGS1))
                        (CADDR ARGS1))
                   (NOT (NUMBERP (CDAR ARGS1)))).

    But this further simplifies, appealing to the lemmas CDR-CONS and CAR-CONS,
    and opening up STRIP-CARS, CAR, MEMBER, and EQUAL, to:

          T.

Case 62.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))
                      (NOT (MEMBER F ARGS1))
                      (NOT (MEMBER F ARGS2))
                      (EQUAL FN 'IF)
                      (NOT (CAR ARGS2))
                      (CAR ARGS1)
                      (CAAR ARGS1)
                      (CADR ARGS1)
                      (NOT (NUMBERP (CDAR ARGS1))))
                 (IFF (CONS (CAADR ARGS1)
                            (ADD1 (PLUS 0 (CDADR ARGS1))))
                      F)),

  which again simplifies, rewriting with CAR-NLISTP, and expanding EQUAL and
  MEMBER, to:

        T.

Case 61.(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
                      (EQUAL (STRIP-CARS ARGS1)
                             (STRIP-CARS ARGS2))