(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


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

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

(ADD-SHELL BTM NIL BTMP NIL)

[ 0.0 0.0 0.0 ]

BTM


(DEFN GET
      (X ALIST)
      (IF (NLISTP ALIST)
          (BTM)
          (IF (EQUAL X (CAAR ALIST))
              (CDAR ALIST)
              (GET X (CDR ALIST)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT ALIST) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
GET is accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

GET


(DEFN UNSOLV-SUBRP
      (FN)
      (MEMBER FN
              '(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS CAR CDR LISTP PACK
                     UNPACK LITATOM EQUAL LIST)))

     From the definition we can conclude that:
      (OR (FALSEP (UNSOLV-SUBRP FN))
          (TRUEP (UNSOLV-SUBRP FN)))
is a theorem.




[ 0.0 0.0 0.0 ]

UNSOLV-SUBRP


(DEFN UNSOLV-APPLY-SUBR
 (FN LST)
 (IF
  (EQUAL FN 'ZERO)
  (ZERO)
  (IF
   (EQUAL FN 'TRUE)
   (TRUE)
   (IF
    (EQUAL FN 'FALSE)
    (FALSE)
    (IF
       (EQUAL FN 'ADD1)
       (ADD1 (CAR LST))
       (IF (EQUAL FN 'SUB1)
           (SUB1 (CAR LST))
           (IF (EQUAL FN 'NUMBERP)
               (NUMBERP (CAR LST))
               (IF (EQUAL FN 'CONS)
                   (CONS (CAR LST) (CADR LST))
                   (IF (EQUAL FN 'LIST)
                       LST
                       (IF (EQUAL FN 'CAR)
                           (CAR (CAR LST))
                           (IF (EQUAL FN 'CDR)
                               (CDR (CAR LST))
                               (IF (EQUAL FN 'LISTP)
                                   (LISTP (CAR LST))
                                   (IF (EQUAL FN 'PACK)
                                       (PACK (CAR LST))
                                       (IF (EQUAL FN 'UNPACK)
                                           (UNPACK (CAR LST))
                                           (IF (EQUAL FN 'LITATOM)
                                               (LITATOM (CAR LST))
                                               (IF (EQUAL FN 'EQUAL)
                                                   (EQUAL (CAR LST) (CADR LST))
                                                   0))))))))))))))))

   




[ 0.0 0.0 0.0 ]

UNSOLV-APPLY-SUBR


(DEFN EV
     (FLG X VA FA N)
     (IF (EQUAL FLG 'AL)
         (IF (NLISTP X)
             (IF (NUMBERP X)
                 X
                 (IF (EQUAL X 'T)
                     T
                     (IF (EQUAL X 'F)
                         F
                         (IF (EQUAL X NIL) NIL (GET X VA)))))
             (IF (EQUAL (CAR X) 'QUOTE)
                 (CADR X)
                 (IF (EQUAL (CAR X) 'IF)
                     (IF (BTMP (EV 'AL (CADR X) VA FA N))
                         (BTM)
                         (IF (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADDR X) VA FA N)
                             (EV 'AL (CADDDR X) VA FA N)))
                     (IF (BTMP (EV 'LIST (CDR X) VA FA N))
                         (BTM)
                         (IF (UNSOLV-SUBRP (CAR X))
                             (UNSOLV-APPLY-SUBR (CAR X)
                                                (EV 'LIST (CDR X) VA FA N))
                             (IF (BTMP (GET (CAR X) FA))
                                 (BTM)
                                 (IF (ZEROP N)
                                     (BTM)
                                     (EV 'AL
                                         (CADR (GET (CAR X) FA))
                                         (PAIRLIST (CAR (GET (CAR X) FA))
                                                   (EV 'LIST (CDR X) VA FA N))
                                         FA
                                         (SUB1 N)))))))))
         (IF (LISTP X)
             (IF (BTMP (EV 'AL (CAR X) VA FA N))
                 (BTM)
                 (IF (BTMP (EV 'LIST (CDR X) VA FA N))
                     (BTM)
                     (CONS (EV 'AL (CAR X) VA FA N)
                           (EV 'LIST (CDR X) VA FA N))))
             NIL))
     ((ORD-LESSP (CONS (ADD1 N) (COUNT X)))))

     Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, CAR-LESSEQP,
CDR-LESSP, CDR-LESSEQP, ADD1-SUB1, and CAR-LESSP, and the definitions of
ORDINALP, LESSP, ORD-LESSP, EQUAL, NLISTP, BTMP, UNSOLV-SUBRP, CDR, CAR, LISTP,
MEMBER, and ZEROP can be used to establish that the measure:
      (CONS (ADD1 N) (COUNT X))
decreases according to the well-founded relation ORD-LESSP in each recursive
call.  Hence, EV is accepted under the principle of definition.




[ 0.0 0.1 0.0 ]

EV


(DEFN PR-EVAL
      (X VA FA N)
      (EV 'AL X VA FA N))

   




[ 0.0 0.0 0.0 ]

PR-EVAL


(DEFN EVLIST
      (X VA FA N)
      (EV 'LIST X VA FA N))

   




[ 0.0 0.0 0.0 ]

EVLIST


(DEFN SUBLIS
      (ALIST X)
      (IF (NLISTP X)
          (IF (ASSOC X ALIST)
              (CDR (ASSOC X ALIST))
              X)
          (CONS (SUBLIS ALIST (CAR X))
                (SUBLIS ALIST (CDR X)))))

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




[ 0.0 0.0 0.0 ]

SUBLIS


(DEFN X
      (FA)
      (SUBLIS (LIST (CONS 'CIRC (CONS FA 0)))
              '(CIRC A)))

   




[ 0.0 0.0 0.0 ]

X


(DEFN FA
      (FA)
      (APPEND (SUBLIS (LIST (CONS 'CIRC (CONS FA 0))
                            (CONS 'LOOP (CONS FA 1)))
                      '((CIRC (A)
                              (IF (HALTS '(CIRC A)
                                         (LIST (CONS 'A A))
                                         A)
                                  (LOOP)
                                  T))
                        (LOOP NIL (LOOP))))
              FA))

     Observe that (OR (LISTP (FA FA)) (EQUAL (FA FA) FA)) is a theorem.




[ 0.0 0.0 0.0 ]

FA


(DEFN VA
      (FA)
      (LIST (CONS 'A (FA FA))))

     From the definition we can conclude that (LISTP (VA FA)) is a theorem.




[ 0.0 0.0 0.0 ]

VA


(DEFN K (N) (ADD1 N))

     Observe that (NUMBERP (K N)) is a theorem.




[ 0.0 0.0 0.0 ]

K


(DEFN OCCUR
      (X Y)
      (IF (EQUAL X Y)
          T
          (IF (NLISTP Y)
              F
              (OR (OCCUR X (CAR Y))
                  (OCCUR X (CDR Y))))))

     Linear arithmetic, the lemmas CDR-LESSEQP, CDR-LESSP, CAR-LESSEQP, and
CAR-LESSP, and the definition of NLISTP inform us that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, OCCUR is accepted under the definitional principle.  Note that:
      (OR (FALSEP (OCCUR X Y))
          (TRUEP (OCCUR X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

OCCUR


(DEFN OCCUR-IN-DEFNS
      (X LST)
      (IF (NLISTP LST)
          F
          (OR (OCCUR X (CADDR (CAR LST)))
              (OCCUR-IN-DEFNS X (CDR LST))))
      NIL)

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
OCCUR-IN-DEFNS is accepted under the principle of definition.  Note that:
      (OR (FALSEP (OCCUR-IN-DEFNS X LST))
          (TRUEP (OCCUR-IN-DEFNS X LST)))
is a theorem.




[ 0.0 0.0 0.0 ]

OCCUR-IN-DEFNS


(PROVE-LEMMA OCCUR-OCCUR-IN-DEFNS
             (REWRITE)
             (IMPLIES (AND (NOT (OCCUR-IN-DEFNS FN FA))
                           (NOT (BTMP (GET X FA))))
                      (NOT (OCCUR FN (CADR (GET X FA))))))


     Name 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 FA) (p FN X FA))
           (IMPLIES (AND (NOT (NLISTP FA))
                         (p FN X (CDR FA)))
                    (p FN X FA))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT FA) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme generates the following four new conjectures:

Case 4. (IMPLIES (AND (NLISTP FA)
                      (NOT (OCCUR-IN-DEFNS FN FA))
                      (NOT (BTMP (GET X FA))))
                 (NOT (OCCUR FN (CADR (GET X FA))))).

  This simplifies, expanding the functions NLISTP, OCCUR-IN-DEFNS, GET, and
  BTMP, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP FA))
                      (OCCUR-IN-DEFNS FN (CDR FA))
                      (NOT (OCCUR-IN-DEFNS FN FA))
                      (NOT (BTMP (GET X FA))))
                 (NOT (OCCUR FN (CADR (GET X FA))))).

  This simplifies, opening up the functions NLISTP and OCCUR-IN-DEFNS, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP FA))
                      (BTMP (GET X (CDR FA)))
                      (NOT (OCCUR-IN-DEFNS FN FA))
                      (NOT (BTMP (GET X FA))))
                 (NOT (OCCUR FN (CADR (GET X FA))))).

  This simplifies, unfolding NLISTP, OCCUR-IN-DEFNS, and GET, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP FA))
                      (NOT (OCCUR FN (CADR (GET X (CDR FA)))))
                      (NOT (OCCUR-IN-DEFNS FN FA))
                      (NOT (BTMP (GET X FA))))
                 (NOT (OCCUR FN (CADR (GET X FA))))).

  This simplifies, unfolding the definitions of NLISTP, OCCUR-IN-DEFNS, and
  GET, to:

        T.


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


[ 0.0 0.0 0.0 ]

OCCUR-OCCUR-IN-DEFNS


(PROVE-LEMMA LEMMA1
             (REWRITE)
             (IMPLIES (AND (NOT (OCCUR FN X))
                           (NOT (OCCUR-IN-DEFNS FN FA)))
                      (EQUAL (EV FLG X VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV FLG X VA FA N)))
             NIL)


     Give the conjecture the name *1.


     We will appeal to induction.  There are four plausible inductions.  They
merge into three likely candidate inductions, two of which are unflawed.
However, one of these is more likely than the other.  We will induct according
to the following scheme:
      (AND
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NLISTP X)
                       (NUMBERP X))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NLISTP X)
                       (NOT (NUMBERP X))
                       (EQUAL X 'T))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NLISTP X)
                       (NOT (NUMBERP X))
                       (NOT (EQUAL X 'T))
                       (EQUAL X 'F))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NLISTP X)
                       (NOT (NUMBERP X))
                       (NOT (EQUAL X 'T))
                       (NOT (EQUAL X 'F))
                       (EQUAL X NIL))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NLISTP X)
                       (NOT (NUMBERP X))
                       (NOT (EQUAL X 'T))
                       (NOT (EQUAL X 'F))
                       (NOT (EQUAL X NIL)))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (EQUAL (CAR X) 'QUOTE))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (EQUAL (CAR X) 'IF)
                       (BTMP (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                       (p 'AL (CADR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (EQUAL (CAR X) 'IF)
                       (NOT (BTMP (EV 'AL
                                      (CADR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (EV 'AL
                           (CADR X)
                           VA
                           (CONS (CONS FN DEF) FA)
                           N)
                       (p 'AL (CADDR X) VA FN DEF FA N)
                       (p 'AL (CADR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (EQUAL (CAR X) 'IF)
                       (NOT (BTMP (EV 'AL
                                      (CADR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (NOT (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                       (p 'AL (CADDDR X) VA FN DEF FA N)
                       (p 'AL (CADR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (NOT (EQUAL (CAR X) 'IF))
                       (BTMP (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (NOT (EQUAL (CAR X) 'IF))
                       (NOT (BTMP (EV 'LIST
                                      (CDR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (UNSOLV-SUBRP (CAR X))
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (NOT (EQUAL (CAR X) 'IF))
                       (NOT (BTMP (EV 'LIST
                                      (CDR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (NOT (UNSOLV-SUBRP (CAR X)))
                       (BTMP (GET (CAR X) (CONS (CONS FN DEF) FA)))
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (NOT (EQUAL (CAR X) 'IF))
                       (NOT (BTMP (EV 'LIST
                                      (CDR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (NOT (UNSOLV-SUBRP (CAR X)))
                       (NOT (BTMP (GET (CAR X)
                                       (CONS (CONS FN DEF) FA))))
                       (ZEROP N)
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (EQUAL FLG 'AL)
                       (NOT (NLISTP X))
                       (NOT (EQUAL (CAR X) 'QUOTE))
                       (NOT (EQUAL (CAR X) 'IF))
                       (NOT (BTMP (EV 'LIST
                                      (CDR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (NOT (UNSOLV-SUBRP (CAR X)))
                       (NOT (BTMP (GET (CAR X)
                                       (CONS (CONS FN DEF) FA))))
                       (NOT (ZEROP N))
                       (p 'LIST (CDR X) VA FN DEF FA N)
                       (p 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          FN DEF FA
                          (SUB1 N)))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                       (LISTP X)
                       (BTMP (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                       (p 'AL (CAR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                       (LISTP X)
                       (NOT (BTMP (EV 'AL
                                      (CAR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (BTMP (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                       (p 'AL (CAR X) VA FN DEF FA N)
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                       (LISTP X)
                       (NOT (BTMP (EV 'AL
                                      (CAR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (NOT (BTMP (EV 'LIST
                                      (CDR X)
                                      VA
                                      (CONS (CONS FN DEF) FA)
                                      N)))
                       (p 'AL (CAR X) VA FN DEF FA N)
                       (p 'LIST (CDR X) VA FN DEF FA N))
                  (p FLG X VA FN DEF FA N))
         (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                       (NOT (LISTP X)))
                  (p FLG X VA FN DEF FA N))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, CAR-LESSEQP,
CDR-LESSP, CDR-LESSEQP, ADD1-SUB1, and CAR-LESSP, and the definitions of
ORDINALP, LESSP, ORD-LESSP, EQUAL, NLISTP, BTMP, UNSOLV-SUBRP, CDR, CAR, LISTP,
MEMBER, and ZEROP establish that the measure (CONS (ADD1 N) (COUNT X))
decreases according to the well-founded relation ORD-LESSP in each induction
step of the scheme.  Note, however, the inductive instances chosen for FLG and
VA.  The above induction scheme generates the following 39 new formulas:

Case 39.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NUMBERP X)
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, unfolding NLISTP, OCCUR, EQUAL, and EV, to:

        T.

Case 38.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (EQUAL X 'T)
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the definitions of NLISTP, NUMBERP, LISTP, OCCUR,
  EQUAL, and EV, to:

        T.

Case 37.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (EQUAL X 'F)
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the functions NLISTP, NUMBERP, EQUAL, LISTP,
  OCCUR, and EV, to:

        T.

Case 36.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (NOT (EQUAL X 'F))
                      (EQUAL X NIL)
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up NLISTP, NUMBERP, EQUAL, LISTP, OCCUR, and EV, to:

        T.

Case 35.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (NOT (EQUAL X 'F))
                      (NOT (EQUAL X NIL))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding NLISTP, OCCUR, EQUAL, and EV, to:

        T.

Case 34.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (EQUAL (CAR X) 'QUOTE)
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up NLISTP, OCCUR, EQUAL, and EV, to:

        T.

Case 33.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CADR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the definitions of NLISTP, EQUAL, OCCUR, and EV,
  to the new formula:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (BTM) (EV 'AL X VA FA N))),

  which again simplifies, expanding the definitions of LISTP and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (BTM) (EV 'AL X VA FA N))).

  However this further simplifies, opening up the function OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (BTM) (EV 'AL X VA FA N))).

  However this again simplifies, rewriting with the lemma CAR-NLISTP, and
  unfolding the definitions of NUMBERP, LISTP, EQUAL, EV, and BTMP, to:

        T.

Case 32.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL
                                (CADR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, opening up the definitions of NLISTP, EQUAL, OCCUR, and EV,
  to:

        T.

Case 31.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (OCCUR FN (CADDR X))
                      (OCCUR FN (CADR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, unfolding the functions NLISTP, EQUAL, OCCUR, and EV, to
  the formula:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (OCCUR FN (CADDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL X VA FA N))).

  However this again simplifies, expanding the functions LISTP and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (OCCUR FN (CADDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL X VA FA N))).

  However this further simplifies, rewriting with the lemma CDR-NLISTP, and
  unfolding the definitions of OCCUR, CAR, NUMBERP, LISTP, EQUAL, and EV, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (OCCUR FN (CADDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))).

  However this again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
  opening up NUMBERP, LISTP, EQUAL, EV, BTMP, CAR, and OCCUR, to the new
  formula:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (EQUAL FN 0)
                      (NOT (EQUAL 0 (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))),

  which again simplifies, trivially, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EQUAL 0 (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))).

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

        (IMPLIES (AND (EQUAL Z 'IF)
                      (NOT (EQUAL 0 V))
                      (NOT (LISTP V))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0
                        (EV 'AL (CONS Z V) VA FA N))),

  which finally simplifies, applying the lemmas CDR-NLISTP, CAR-NLISTP,
  CDR-CONS, and CAR-CONS, and opening up CDR, CAR, EQUAL, EV, NUMBERP, LISTP,
  and BTMP, to:

        T.

Case 30.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EQUAL (EV 'AL
                                 (CADDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, expanding NLISTP, EQUAL, OCCUR, and EV, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EQUAL (EV 'AL
                                 (CADDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL (CADDR X) VA FA N)
                        (EV 'AL X VA FA N))).

  But this again simplifies, expanding the definitions of LISTP and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EQUAL (EV 'AL
                                 (CADDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL (CADDR X) VA FA N)
                        (EV 'AL X VA FA N))).

  However this further simplifies, rewriting with the lemma CDR-NLISTP, and
  opening up OCCUR, CAR, NUMBERP, LISTP, EQUAL, and EV, to the conjecture:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EQUAL (EV 'AL
                                 (CADDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))).

  But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and expanding
  the functions NUMBERP, LISTP, EQUAL, EV, BTMP, CAR, and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (EQUAL FN 0)
                      (NOT (EQUAL 0 (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))),

  which again simplifies, clearly, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EQUAL 0 (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))).

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

        (IMPLIES (AND (EQUAL Z 'IF)
                      (NOT (EQUAL 0 V))
                      (NOT (LISTP V))
                      (NOT (OCCUR-IN-DEFNS 0 FA)))
                 (EQUAL 0
                        (EV 'AL (CONS Z V) VA FA N))),

  which finally simplifies, applying CDR-NLISTP, CAR-NLISTP, CDR-CONS, and
  CAR-CONS, and expanding the functions CDR, CAR, EQUAL, EV, NUMBERP, LISTP,
  and BTMP, to:

        T.

Case 29.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (OCCUR FN (CADDR X))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding NLISTP, EQUAL, OCCUR, and EV, to the new goal:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (OCCUR FN (CADDR X))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL (CADDR X) VA FA N))),

  which again simplifies, expanding LISTP and OCCUR, to the formula:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (OCCUR FN (CADDR X))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL (CADDR X) VA FA N))).

  But this further simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP,
  and expanding OCCUR, NUMBERP, LISTP, EQUAL, EV, and CAR, to:

        T.

Case 28.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EV 'AL
                          (CADR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EQUAL (EV 'AL
                                 (CADDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDR X) VA FA N))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, expanding the definitions of NLISTP, EQUAL, OCCUR, and EV,
  to:

        T.

Case 27.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (OCCUR FN (CADDDR X))
                      (OCCUR FN (CADR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, opening up the definitions of NLISTP, EQUAL, BTMP, OCCUR,
  and EV, to the formula:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (OCCUR FN (CADDDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL X VA FA N))).

  However this again simplifies, expanding the functions LISTP and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (OCCUR FN (CADDDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL X VA FA N))).

  But this further simplifies, rewriting with CDR-NLISTP, and expanding the
  functions OCCUR, CDR, CAR, NUMBERP, LISTP, EQUAL, and EV, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (OCCUR FN (CADDDR X))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))),

  which again simplifies, applying CAR-NLISTP, and unfolding the definitions
  of NUMBERP, LISTP, EQUAL, and EV, to:

        T.

Case 26.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (EQUAL (EV 'AL
                                 (CADDDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the definitions of NLISTP, EQUAL, BTMP, OCCUR,
  and EV, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (EQUAL (EV 'AL
                                 (CADDDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL (CADDDR X) VA FA N)
                        (EV 'AL X VA FA N))),

  which again simplifies, unfolding LISTP and OCCUR, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (EQUAL (EV 'AL
                                 (CADDDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL (CADDDR X) VA FA N)
                        (EV 'AL X VA FA N))).

  But this further simplifies, applying CDR-NLISTP, and opening up the
  definitions of OCCUR, CDR, CAR, NUMBERP, LISTP, EQUAL, and EV, to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (EQUAL (EV 'AL
                                 (CADDDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDDR X) VA FA N))
                      (OCCUR FN (CADR X))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (LISTP (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL 0 (EV 'AL X VA FA N))),

  which again simplifies, applying CAR-NLISTP, and expanding NUMBERP, LISTP,
  EQUAL, and EV, to:

        T.

Case 25.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (OCCUR FN (CADDDR X))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the functions NLISTP, EQUAL, OCCUR, BTMP, and EV,
  to:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (OCCUR FN (CADDDR X))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL (CADDDR X) VA FA N))),

  which again simplifies, expanding LISTP and OCCUR, to the goal:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (OCCUR FN (CADDDR X))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL (CADDDR X) VA FA N))).

  However this further simplifies, rewriting with the lemma CDR-NLISTP, and
  expanding the functions OCCUR, CDR, CAR, NUMBERP, LISTP, EQUAL, and EV, to
  the goal:

        (IMPLIES (AND (LISTP X)
                      (EQUAL (CAR X) 'IF)
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (OCCUR FN (CADDDR X))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (NOT (EQUAL FN X))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN (CDR X)))
                      (NOT (OCCUR FN (CADR X)))
                      (NOT (OCCUR FN (CDDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            (CADDDR X)
                            VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL (CADDDR X) VA FA N))).

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

  Case 25.4.
          (IMPLIES (AND (NOT (LISTP V))
                        (EQUAL Z 'IF)
                        (NOT (EV 'AL (CAR V) VA FA N))
                        (OCCUR FN (CADDR V))
                        (NOT (EV 'AL
                                 (CAR V)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                        (NOT (EQUAL FN (CONS Z V)))
                        (NOT (EQUAL FN 'IF))
                        (NOT (EQUAL FN V))
                        (NOT (OCCUR FN (CAR V)))
                        (NOT (OCCUR FN (CDR V)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              (CADDR V)
                              VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL (CADDR V) VA FA N))),

    which further simplifies, applying CAR-NLISTP, and expanding NUMBERP,
    LISTP, EQUAL, and EV, to:

          T.

  Case 25.3.
          (IMPLIES (AND (NOT (LISTP D))
                        (EQUAL Z 'IF)
                        (NOT (EV 'AL W VA FA N))
                        (OCCUR FN (CADR D))
                        (NOT (EV 'AL
                                 W VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                        (NOT (EQUAL FN (CONS Z (CONS W D))))
                        (NOT (EQUAL FN 'IF))
                        (NOT (EQUAL FN (CONS W D)))
                        (NOT (OCCUR FN W))
                        (NOT (OCCUR FN D))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              (CADR D)
                              VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL (CADR D) VA FA N))).

    But this further simplifies, applying CDR-NLISTP, and opening up CAR,
    LISTP, OCCUR, EQUAL, NUMBERP, and EV, to:

          T.

  Case 25.2.
          (IMPLIES (AND (NOT (LISTP V))
                        (EQUAL Z 'IF)
                        (NOT (EV 'AL W VA FA N))
                        (OCCUR FN (CAR V))
                        (NOT (EV 'AL
                                 W VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                        (NOT (EQUAL FN
                                    (CONS Z (CONS W (CONS C V)))))
                        (NOT (EQUAL FN 'IF))
                        (NOT (EQUAL FN (CONS W (CONS C V))))
                        (NOT (OCCUR FN W))
                        (NOT (OCCUR FN (CONS C V)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              (CAR V)
                              VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL (CAR V) VA FA N))).

    However this further simplifies, applying CAR-NLISTP, CDR-CONS, and
    CAR-CONS, and unfolding the definitions of LISTP, OCCUR, EQUAL, NUMBERP,
    and EV, to:

          T.

  Case 25.1.
          (IMPLIES (AND (EQUAL Z 'IF)
                        (NOT (EV 'AL W VA FA N))
                        (OCCUR FN D)
                        (NOT (EV 'AL
                                 W VA
                                 (CONS (CONS FN DEF) FA)
                                 N))
                        (NOT (EQUAL FN
                                    (CONS Z
                                          (CONS W (CONS C (CONS D X1))))))
                        (NOT (EQUAL FN 'IF))
                        (NOT (EQUAL FN
                                    (CONS W (CONS C (CONS D X1)))))
                        (NOT (OCCUR FN W))
                        (NOT (OCCUR FN (CONS C (CONS D X1))))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              D VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL D VA FA N))).

    This further simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
    up the function OCCUR, to:

          T.

Case 24.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL
                                     (CADR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (EV 'AL
                               (CADR X)
                               VA
                               (CONS (CONS FN DEF) FA)
                               N))
                      (EQUAL (EV 'AL
                                 (CADDDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADDDR X) VA FA N))
                      (EQUAL (EV 'AL
                                 (CADR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CADR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up NLISTP, EQUAL, OCCUR, BTMP, and EV, to:

        T.

Case 23.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the definitions of NLISTP and OCCUR, to:

        T.

Case 22.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding NLISTP, OCCUR, EQUAL, and EV, to:

        T.

Case 21.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (UNSOLV-SUBRP (CAR X))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the definitions of NLISTP, MEMBER, LISTP, CAR,
  CDR, UNSOLV-SUBRP, and OCCUR, to:

        T.

Case 20.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (UNSOLV-SUBRP (CAR X))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the functions NLISTP, MEMBER, LISTP, CAR, CDR,
  UNSOLV-SUBRP, OCCUR, UNSOLV-APPLY-SUBR, EQUAL, and EV, to:

        T.

Case 19.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (BTMP (GET (CAR X) (CONS (CONS FN DEF) FA)))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, and OCCUR, to:

        T.

Case 18.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (BTMP (GET (CAR X) (CONS (CONS FN DEF) FA)))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
  opening up the definitions of NLISTP, MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP,
  GET, OCCUR, EQUAL, and EV, to the goal:

        (IMPLIES (AND (LISTP X)
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                      (NOT (EQUAL (CAR X) 'ZERO))
                      (NOT (EQUAL (CAR X) 'TRUE))
                      (NOT (EQUAL (CAR X) 'FALSE))
                      (NOT (EQUAL (CAR X) 'ADD1))
                      (NOT (EQUAL (CAR X) 'SUB1))
                      (NOT (EQUAL (CAR X) 'NUMBERP))
                      (NOT (EQUAL (CAR X) 'CONS))
                      (NOT (EQUAL (CAR X) 'CAR))
                      (NOT (EQUAL (CAR X) 'CDR))
                      (NOT (EQUAL (CAR X) 'LISTP))
                      (NOT (EQUAL (CAR X) 'PACK))
                      (NOT (EQUAL (CAR X) 'UNPACK))
                      (NOT (EQUAL (CAR X) 'LITATOM))
                      (NOT (EQUAL (CAR X) 'EQUAL))
                      (NOT (EQUAL (CAR X) 'LIST))
                      (EQUAL (CAR X) FN)
                      (BTMP DEF)
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (EQUAL FN X))
                      (NOT (OCCUR FN (CAR X)))
                      (NOT (OCCUR FN (CDR X)))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV 'AL
                            X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV 'AL X VA FA N))).

  However this again simplifies, expanding OCCUR, to:

        T.

Case 17.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (NOT (BTMP (GET (CAR X)
                                      (CONS (CONS FN DEF) FA))))
                      (ZEROP N)
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, and OCCUR, to:

        T.

Case 16.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (NOT (BTMP (GET (CAR X)
                                      (CONS (CONS FN DEF) FA))))
                      (ZEROP N)
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, OCCUR, EQUAL, and EV, to
  two new goals:

  Case 16.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) 'QUOTE))
                        (NOT (EQUAL (CAR X) 'IF))
                        (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                        (NOT (EQUAL (CAR X) 'ZERO))
                        (NOT (EQUAL (CAR X) 'TRUE))
                        (NOT (EQUAL (CAR X) 'FALSE))
                        (NOT (EQUAL (CAR X) 'ADD1))
                        (NOT (EQUAL (CAR X) 'SUB1))
                        (NOT (EQUAL (CAR X) 'NUMBERP))
                        (NOT (EQUAL (CAR X) 'CONS))
                        (NOT (EQUAL (CAR X) 'CAR))
                        (NOT (EQUAL (CAR X) 'CDR))
                        (NOT (EQUAL (CAR X) 'LISTP))
                        (NOT (EQUAL (CAR X) 'PACK))
                        (NOT (EQUAL (CAR X) 'UNPACK))
                        (NOT (EQUAL (CAR X) 'LITATOM))
                        (NOT (EQUAL (CAR X) 'EQUAL))
                        (NOT (EQUAL (CAR X) 'LIST))
                        (EQUAL (CAR X) FN)
                        (NOT (BTMP DEF))
                        (EQUAL N 0)
                        (EQUAL (EV 'LIST
                                   (CDR X)
                                   VA
                                   (CONS (CONS FN DEF) FA)
                                   N)
                               (EV 'LIST (CDR X) VA FA 0))
                        (NOT (EQUAL FN X))
                        (NOT (OCCUR FN (CAR X)))
                        (NOT (OCCUR FN (CDR X)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              X VA
                              (CONS (CONS FN DEF) FA)
                              0)
                          (EV 'AL X VA FA 0))),

    which again simplifies, opening up OCCUR, to:

          T.

  Case 16.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) 'QUOTE))
                        (NOT (EQUAL (CAR X) 'IF))
                        (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                        (NOT (EQUAL (CAR X) 'ZERO))
                        (NOT (EQUAL (CAR X) 'TRUE))
                        (NOT (EQUAL (CAR X) 'FALSE))
                        (NOT (EQUAL (CAR X) 'ADD1))
                        (NOT (EQUAL (CAR X) 'SUB1))
                        (NOT (EQUAL (CAR X) 'NUMBERP))
                        (NOT (EQUAL (CAR X) 'CONS))
                        (NOT (EQUAL (CAR X) 'CAR))
                        (NOT (EQUAL (CAR X) 'CDR))
                        (NOT (EQUAL (CAR X) 'LISTP))
                        (NOT (EQUAL (CAR X) 'PACK))
                        (NOT (EQUAL (CAR X) 'UNPACK))
                        (NOT (EQUAL (CAR X) 'LITATOM))
                        (NOT (EQUAL (CAR X) 'EQUAL))
                        (NOT (EQUAL (CAR X) 'LIST))
                        (EQUAL (CAR X) FN)
                        (NOT (BTMP DEF))
                        (NOT (NUMBERP N))
                        (EQUAL (EV 'LIST
                                   (CDR X)
                                   VA
                                   (CONS (CONS FN DEF) FA)
                                   N)
                               (EV 'LIST (CDR X) VA FA N))
                        (NOT (EQUAL FN X))
                        (NOT (OCCUR FN (CAR X)))
                        (NOT (OCCUR FN (CDR X)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              X VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL X VA FA N))),

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

          T.

Case 15.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (NOT (BTMP (GET (CAR X)
                                      (CONS (CONS FN DEF) FA))))
                      (NOT (ZEROP N))
                      (OCCUR FN (CDR X))
                      (OCCUR FN
                             (CADR (GET (CAR X)
                                        (CONS (CONS FN DEF) FA))))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))),

  which simplifies, applying CDR-CONS and CAR-CONS, and unfolding NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, and OCCUR, to:

        T.

Case 14.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (UNSOLV-SUBRP (CAR X)))
                      (NOT (BTMP (GET (CAR X)
                                      (CONS (CONS FN DEF) FA))))
                      (NOT (ZEROP N))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (OCCUR FN
                             (CADR (GET (CAR X)
                                        (CONS (CONS FN DEF) FA))))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
  the functions NLISTP, MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, and
  OCCUR, to the following two new conjectures:

  Case 14.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) 'QUOTE))
                        (NOT (EQUAL (CAR X) 'IF))
                        (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                        (NOT (EQUAL (CAR X) 'ZERO))
                        (NOT (EQUAL (CAR X) 'TRUE))
                        (NOT (EQUAL (CAR X) 'FALSE))
                        (NOT (EQUAL (CAR X) 'ADD1))
                        (NOT (EQUAL (CAR X) 'SUB1))
                        (NOT (EQUAL (CAR X) 'NUMBERP))
                        (NOT (EQUAL (CAR X) 'CONS))
                        (NOT (EQUAL (CAR X) 'CAR))
                        (NOT (EQUAL (CAR X) 'CDR))
                        (NOT (EQUAL (CAR X) 'LISTP))
                        (NOT (EQUAL (CAR X) 'PACK))
                        (NOT (EQUAL (CAR X) 'UNPACK))
                        (NOT (EQUAL (CAR X) 'LITATOM))
                        (NOT (EQUAL (CAR X) 'EQUAL))
                        (NOT (EQUAL (CAR X) 'LIST))
                        (NOT (EQUAL (CAR X) FN))
                        (NOT (BTMP (GET (CAR X) FA)))
                        (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (EQUAL (EV 'LIST
                                   (CDR X)
                                   VA
                                   (CONS (CONS FN DEF) FA)
                                   N)
                               (EV 'LIST (CDR X) VA FA N))
                        (OCCUR FN
                               (CADR (GET (CAR X)
                                          (CONS (CONS FN DEF) FA))))
                        (NOT (EQUAL FN X))
                        (NOT (OCCUR FN (CAR X)))
                        (NOT (OCCUR FN (CDR X)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              X VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL X VA FA N))).

    This further simplifies, rewriting with CDR-CONS, CAR-CONS, and
    OCCUR-OCCUR-IN-DEFNS, and opening up the definition of GET, to:

          T.

  Case 14.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (CAR X) 'QUOTE))
                        (NOT (EQUAL (CAR X) 'IF))
                        (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                        (NOT (EQUAL (CAR X) 'ZERO))
                        (NOT (EQUAL (CAR X) 'TRUE))
                        (NOT (EQUAL (CAR X) 'FALSE))
                        (NOT (EQUAL (CAR X) 'ADD1))
                        (NOT (EQUAL (CAR X) 'SUB1))
                        (NOT (EQUAL (CAR X) 'NUMBERP))
                        (NOT (EQUAL (CAR X) 'CONS))
                        (NOT (EQUAL (CAR X) 'CAR))
                        (NOT (EQUAL (CAR X) 'CDR))
                        (NOT (EQUAL (CAR X) 'LISTP))
                        (NOT (EQUAL (CAR X) 'PACK))
                        (NOT (EQUAL (CAR X) 'UNPACK))
                        (NOT (EQUAL (CAR X) 'LITATOM))
                        (NOT (EQUAL (CAR X) 'EQUAL))
                        (NOT (EQUAL (CAR X) 'LIST))
                        (EQUAL (CAR X) FN)
                        (NOT (BTMP DEF))
                        (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (EQUAL (EV 'LIST
                                   (CDR X)
                                   VA
                                   (CONS (CONS FN DEF) FA)
                                   N)
                               (EV 'LIST (CDR X) VA FA N))
                        (OCCUR FN
                               (CADR (GET (CAR X)
                                          (CONS (CONS FN DEF) FA))))
                        (NOT (EQUAL FN X))
                        (NOT (OCCUR FN (CAR X)))
                        (NOT (OCCUR FN (CDR X)))
                        (NOT (OCCUR-IN-DEFNS FN FA)))
                   (EQUAL (EV 'AL
                              X VA
                              (CONS (CONS FN DEF) FA)
                              N)
                          (EV 'AL X VA FA N))).

    However this again simplifies, applying CDR-CONS and CAR-CONS, and
    expanding GET and OCCUR, to:

          T.

Case 13.(IMPLIES
          (AND (EQUAL FLG 'AL)
               (NOT (NLISTP X))
               (NOT (EQUAL (CAR X) 'QUOTE))
               (NOT (EQUAL (CAR X) 'IF))
               (NOT (BTMP (EV 'LIST
                              (CDR X)
                              VA
                              (CONS (CONS FN DEF) FA)
                              N)))
               (NOT (UNSOLV-SUBRP (CAR X)))
               (NOT (BTMP (GET (CAR X)
                               (CONS (CONS FN DEF) FA))))
               (NOT (ZEROP N))
               (OCCUR FN (CDR X))
               (EQUAL (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          (CONS (CONS FN DEF) FA)
                          (SUB1 N))
                      (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          FA
                          (SUB1 N)))
               (NOT (OCCUR FN X))
               (NOT (OCCUR-IN-DEFNS FN FA)))
          (EQUAL (EV FLG X VA
                     (CONS (CONS FN DEF) FA)
                     N)
                 (EV FLG X VA FA N))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, and OCCUR, to:

        T.

Case 12.(IMPLIES
          (AND (EQUAL FLG 'AL)
               (NOT (NLISTP X))
               (NOT (EQUAL (CAR X) 'QUOTE))
               (NOT (EQUAL (CAR X) 'IF))
               (NOT (BTMP (EV 'LIST
                              (CDR X)
                              VA
                              (CONS (CONS FN DEF) FA)
                              N)))
               (NOT (UNSOLV-SUBRP (CAR X)))
               (NOT (BTMP (GET (CAR X)
                               (CONS (CONS FN DEF) FA))))
               (NOT (ZEROP N))
               (EQUAL (EV 'LIST
                          (CDR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EV 'LIST (CDR X) VA FA N))
               (EQUAL (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          (CONS (CONS FN DEF) FA)
                          (SUB1 N))
                      (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          FA
                          (SUB1 N)))
               (NOT (OCCUR FN X))
               (NOT (OCCUR-IN-DEFNS FN FA)))
          (EQUAL (EV FLG X VA
                     (CONS (CONS FN DEF) FA)
                     N)
                 (EV FLG X VA FA N))),

  which simplifies, applying CDR-CONS and CAR-CONS, and opening up NLISTP,
  MEMBER, LISTP, CAR, CDR, UNSOLV-SUBRP, GET, ZEROP, and OCCUR, to the
  following two new conjectures:

  Case 12.2.
          (IMPLIES
           (AND
               (LISTP X)
               (NOT (EQUAL (CAR X) 'QUOTE))
               (NOT (EQUAL (CAR X) 'IF))
               (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
               (NOT (EQUAL (CAR X) 'ZERO))
               (NOT (EQUAL (CAR X) 'TRUE))
               (NOT (EQUAL (CAR X) 'FALSE))
               (NOT (EQUAL (CAR X) 'ADD1))
               (NOT (EQUAL (CAR X) 'SUB1))
               (NOT (EQUAL (CAR X) 'NUMBERP))
               (NOT (EQUAL (CAR X) 'CONS))
               (NOT (EQUAL (CAR X) 'CAR))
               (NOT (EQUAL (CAR X) 'CDR))
               (NOT (EQUAL (CAR X) 'LISTP))
               (NOT (EQUAL (CAR X) 'PACK))
               (NOT (EQUAL (CAR X) 'UNPACK))
               (NOT (EQUAL (CAR X) 'LITATOM))
               (NOT (EQUAL (CAR X) 'EQUAL))
               (NOT (EQUAL (CAR X) 'LIST))
               (NOT (EQUAL (CAR X) FN))
               (NOT (BTMP (GET (CAR X) FA)))
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (EQUAL (EV 'LIST
                          (CDR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EV 'LIST (CDR X) VA FA N))
               (EQUAL (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          (CONS (CONS FN DEF) FA)
                          (SUB1 N))
                      (EV 'AL
                          (CADR (GET (CAR X) FA))
                          (PAIRLIST (CAR (GET (CAR X) FA))
                                    (EV 'LIST (CDR X) VA FA N))
                          FA
                          (SUB1 N)))
               (NOT (EQUAL FN X))
               (NOT (OCCUR FN (CAR X)))
               (NOT (OCCUR FN (CDR X)))
               (NOT (OCCUR-IN-DEFNS FN FA)))
           (EQUAL (EV 'AL
                      X VA
                      (CONS (CONS FN DEF) FA)
                      N)
                  (EV 'AL X VA FA N))).

    This again simplifies, applying CAR-CONS and CDR-CONS, and opening up GET,
    UNSOLV-SUBRP, CDR, CAR, LISTP, MEMBER, EQUAL, and EV, to:

          T.

  Case 12.1.
          (IMPLIES
           (AND
               (LISTP X)
               (NOT (EQUAL (CAR X) 'QUOTE))
               (NOT (EQUAL (CAR X) 'IF))
               (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
               (NOT (EQUAL (CAR X) 'ZERO))
               (NOT (EQUAL (CAR X) 'TRUE))
               (NOT (EQUAL (CAR X) 'FALSE))
               (NOT (EQUAL (CAR X) 'ADD1))
               (NOT (EQUAL (CAR X) 'SUB1))
               (NOT (EQUAL (CAR X) 'NUMBERP))
               (NOT (EQUAL (CAR X) 'CONS))
               (NOT (EQUAL (CAR X) 'CAR))
               (NOT (EQUAL (CAR X) 'CDR))
               (NOT (EQUAL (CAR X) 'LISTP))
               (NOT (EQUAL (CAR X) 'PACK))
               (NOT (EQUAL (CAR X) 'UNPACK))
               (NOT (EQUAL (CAR X) 'LITATOM))
               (NOT (EQUAL (CAR X) 'EQUAL))
               (NOT (EQUAL (CAR X) 'LIST))
               (EQUAL (CAR X) FN)
               (NOT (BTMP DEF))
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (EQUAL (EV 'LIST
                          (CDR X)
                          VA
                          (CONS (CONS FN DEF) FA)
                          N)
                      (EV 'LIST (CDR X) VA FA N))
               (EQUAL (EV 'AL
                          (CADR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                          (PAIRLIST (CAR (GET (CAR X) (CONS (CONS FN DEF) FA)))
                                    (EV 'LIST
                                        (CDR X)
                                        VA
                                        (CONS (CONS FN DEF) FA)
                                        N))
                          (CONS (CONS FN DEF) FA)
                          (SUB1 N))
                      (EV 'AL
                          (CADR DEF)
                          (PAIRLIST (CAR DEF)
                                    (EV 'LIST (CDR X) VA FA N))
                          FA
                          (SUB1 N)))
               (NOT (EQUAL FN X))
               (NOT (OCCUR FN (CAR X)))
               (NOT (OCCUR FN (CDR X)))
               (NOT (OCCUR-IN-DEFNS FN FA)))
           (EQUAL (EV 'AL
                      X VA
                      (CONS (CONS FN DEF) FA)
                      N)
                  (EV 'AL X VA FA N))).

    This again simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
    functions GET and OCCUR, to:

          T.

Case 11.(IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (BTMP (EV 'AL
                                (CAR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CAR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the function OCCUR, to:

        T.

Case 10.(IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (BTMP (EV 'AL
                                (CAR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (EQUAL (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CAR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, unfolding the functions OCCUR, EV, and EQUAL, to:

        T.

Case 9. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CAR X))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, unfolding the definition of OCCUR, to:

        T.

Case 8. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (EQUAL (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CAR X) VA FA N))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding OCCUR, to:

        T.

Case 7. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (OCCUR FN (CAR X))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the function OCCUR, to:

        T.

Case 6. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (BTMP (EV 'LIST
                                (CDR X)
                                VA
                                (CONS (CONS FN DEF) FA)
                                N))
                      (EQUAL (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CAR X) VA FA N))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, unfolding the functions OCCUR, EV, and EQUAL, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (OCCUR FN (CAR X))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, expanding the definition of OCCUR, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EQUAL (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CAR X) VA FA N))
                      (OCCUR FN (CDR X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the function OCCUR, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (OCCUR FN (CAR X))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the definition of OCCUR, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (LISTP X)
                      (NOT (BTMP (EV 'AL
                                     (CAR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (NOT (BTMP (EV 'LIST
                                     (CDR X)
                                     VA
                                     (CONS (CONS FN DEF) FA)
                                     N)))
                      (EQUAL (EV 'AL
                                 (CAR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'AL (CAR X) VA FA N))
                      (EQUAL (EV 'LIST
                                 (CDR X)
                                 VA
                                 (CONS (CONS FN DEF) FA)
                                 N)
                             (EV 'LIST (CDR X) VA FA N))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, opening up the definitions of OCCUR and EV, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                      (NOT (LISTP X))
                      (NOT (OCCUR FN X))
                      (NOT (OCCUR-IN-DEFNS FN FA)))
                 (EQUAL (EV FLG X VA
                            (CONS (CONS FN DEF) FA)
                            N)
                        (EV FLG X VA FA N))).

  This simplifies, unfolding OCCUR, EV, and EQUAL, to:

        T.


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


[ 0.0 1.1 0.1 ]

LEMMA1


(PROVE-LEMMA COUNT-OCCUR
             (REWRITE)
             (IMPLIES (LESSP (COUNT Y) (COUNT X))
                      (NOT (OCCUR X Y)))
             NIL)


     Call the conjecture *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (EQUAL X Y) (p X Y))
           (IMPLIES (AND (NOT (EQUAL X Y)) (NLISTP Y))
                    (p X Y))
           (IMPLIES (AND (NOT (EQUAL X Y))
                         (NOT (NLISTP Y))
                         (p X (CDR Y))
                         (p X (CAR Y)))
                    (p X Y))).
Linear arithmetic, the lemmas CDR-LESSEQP, CDR-LESSP, CAR-LESSEQP, and
CAR-LESSP, and the definition of NLISTP can be used to prove that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  The above induction scheme leads to six new
goals:

Case 6. (IMPLIES (AND (EQUAL X Y)
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))),

  which simplifies, using linear arithmetic, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL X Y))
                      (NLISTP Y)
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))),

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

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL X Y))
                      (NOT (NLISTP Y))
                      (NOT (LESSP (COUNT (CDR Y)) (COUNT X)))
                      (NOT (LESSP (COUNT (CAR Y)) (COUNT X)))
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))),

  which simplifies, using linear arithmetic and rewriting with CAR-LESSEQP, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL X Y))
                      (NOT (NLISTP Y))
                      (NOT (OCCUR X (CDR Y)))
                      (NOT (LESSP (COUNT (CAR Y)) (COUNT X)))
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))).

  This simplifies, using linear arithmetic and applying CAR-LESSEQP, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL X Y))
                      (NOT (NLISTP Y))
                      (NOT (LESSP (COUNT (CDR Y)) (COUNT X)))
                      (NOT (OCCUR X (CAR Y)))
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))),

  which simplifies, using linear arithmetic and rewriting with CDR-LESSEQP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL X Y))
                      (NOT (NLISTP Y))
                      (NOT (OCCUR X (CDR Y)))
                      (NOT (OCCUR X (CAR Y)))
                      (LESSP (COUNT Y) (COUNT X)))
                 (NOT (OCCUR X Y))).

  This simplifies, expanding the functions NLISTP and OCCUR, to:

        T.


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


[ 0.0 0.0 0.0 ]

COUNT-OCCUR


(PROVE-LEMMA COUNT-GET
             (REWRITE)
             (LESSP (COUNT (CADR (GET FN FA)))
                    (ADD1 (COUNT FA)))
             NIL)

WARNING:  Note that the proposed lemma COUNT-GET is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.


This conjecture simplifies, rewriting with SUB1-ADD1, and unfolding LESSP, to:

      (IMPLIES (NOT (EQUAL (COUNT (CADR (GET FN FA))) 0))
               (LESSP (SUB1 (COUNT (CADR (GET FN FA))))
                      (COUNT FA))),

which we will name *1.


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

Case 4. (IMPLIES (AND (NLISTP FA)
                      (NOT (EQUAL (COUNT (CADR (GET FN FA))) 0)))
                 (LESSP (SUB1 (COUNT (CADR (GET FN FA))))
                        (COUNT FA))),

  which simplifies, unfolding the functions NLISTP, GET, CDR, CAR, COUNT, and
  EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP FA))
                      (EQUAL FN (CAAR FA))
                      (NOT (EQUAL (COUNT (CADR (GET FN FA))) 0)))
                 (LESSP (SUB1 (COUNT (CADR (GET FN FA))))
                        (COUNT FA))),

  which simplifies, expanding the definitions of NLISTP and GET, to the
  conjecture:

        (IMPLIES (AND (LISTP FA)
                      (NOT (EQUAL (COUNT (CADDAR FA)) 0)))
                 (LESSP (SUB1 (COUNT (CADDAR FA)))
                        (COUNT FA))).

  However this again simplifies, using linear arithmetic and applying
  CDR-LESSEQP and CAR-LESSEQP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP FA))
                      (NOT (EQUAL FN (CAAR FA)))
                      (EQUAL (COUNT (CADR (GET FN (CDR FA))))
                             0)
                      (NOT (EQUAL (COUNT (CADR (GET FN FA))) 0)))
                 (LESSP (SUB1 (COUNT (CADR (GET FN FA))))
                        (COUNT FA))).

  This simplifies, expanding the functions NLISTP, GET, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP FA))
                      (NOT (EQUAL FN (CAAR FA)))
                      (LESSP (SUB1 (COUNT (CADR (GET FN (CDR FA)))))
                             (COUNT (CDR FA)))
                      (NOT (EQUAL (COUNT (CADR (GET FN FA))) 0)))
                 (LESSP (SUB1 (COUNT (CADR (GET FN FA))))
                        (COUNT FA))).

  This simplifies, opening up the definitions of NLISTP and GET, to:

        (IMPLIES (AND (LISTP FA)
                      (NOT (EQUAL FN (CAAR FA)))
                      (LESSP (SUB1 (COUNT (CADR (GET FN (CDR FA)))))
                             (COUNT (CDR FA)))
                      (NOT (EQUAL (COUNT (CADR (GET FN (CDR FA))))
                                  0)))
                 (LESSP (SUB1 (COUNT (CADR (GET FN (CDR FA)))))
                        (COUNT FA))),

  which again simplifies, using linear arithmetic and rewriting with the lemma
  CDR-LESSEQP, to:

        T.


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


[ 0.0 0.0 0.0 ]

COUNT-GET


(PROVE-LEMMA COUNT-OCCUR-IN-DEFNS
             (REWRITE)
             (IMPLIES (LESSP (COUNT FA) (COUNT X))
                      (NOT (OCCUR-IN-DEFNS X FA)))
             NIL)


     Call the conjecture *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP FA) (p X FA))
           (IMPLIES (AND (NOT (NLISTP FA)) (p X (CDR FA)))
                    (p X FA))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT FA) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to three new goals:

Case 3. (IMPLIES (AND (NLISTP FA)
                      (LESSP (COUNT FA) (COUNT X)))
                 (NOT (OCCUR-IN-DEFNS X FA))),

  which simplifies, opening up the definitions of NLISTP and OCCUR-IN-DEFNS,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP FA))
                      (NOT (LESSP (COUNT (CDR FA)) (COUNT X)))
                      (LESSP (COUNT FA) (COUNT X)))
                 (NOT (OCCUR-IN-DEFNS X FA))),

  which simplifies, using linear arithmetic and applying CDR-LESSEQP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP FA))
                      (NOT (OCCUR-IN-DEFNS X (CDR FA)))
                      (LESSP (COUNT FA) (COUNT X)))
                 (NOT (OCCUR-IN-DEFNS X FA))).

  This simplifies, using linear arithmetic, appealing to the lemmas
  CAR-LESSEQP, CDR-LESSEQP, and COUNT-OCCUR, and expanding the functions
  NLISTP and OCCUR-IN-DEFNS, to:

        T.


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


[ 0.0 0.0 0.0 ]

COUNT-OCCUR-IN-DEFNS


(PROVE-LEMMA COROLLARY1
             (REWRITE)
             (EQUAL (EV 'AL
                        (CADR (GET 'HALTS FA))
                        VA
                        (CONS (CONS (CONS FA 0) DEF0)
                              (CONS (LIST (CONS FA 1)
                                          NIL
                                          (LIST (CONS FA 1)))
                                    FA))
                        N)
                    (EV 'AL
                        (CADR (GET 'HALTS FA))
                        VA FA N))
             NIL)

This simplifies, using linear arithmetic, rewriting with CAR-CONS, CDR-CONS,
COUNT-OCCUR-IN-DEFNS, COUNT-OCCUR, COUNT-CONS, COUNT-GET, and LEMMA1, and
expanding the definitions of OCCUR-IN-DEFNS, OCCUR, EQUAL, LISTP, and COUNT,
to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

COROLLARY1


(DISABLE LEMMA1)

[ 0.0 0.0 0.0 ]

LEMMA1-OFF


(PROVE-LEMMA LEMMA2 NIL
             (IMPLIES (AND (NOT (BTMP (EV FLG X VA FA N)))
                           (NOT (BTMP (EV FLG X VA FA K))))
                      (EQUAL (EV FLG X VA FA N)
                             (EV FLG X VA FA K)))
             NIL)


     Name the conjecture *1.


     We will appeal to induction.  There are four plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (AND (EQUAL FLG 'AL)
                         (NLISTP X)
                         (NUMBERP X))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NLISTP X)
                         (NOT (NUMBERP X))
                         (EQUAL X 'T))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NLISTP X)
                         (NOT (NUMBERP X))
                         (NOT (EQUAL X 'T))
                         (EQUAL X 'F))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NLISTP X)
                         (NOT (NUMBERP X))
                         (NOT (EQUAL X 'T))
                         (NOT (EQUAL X 'F))
                         (EQUAL X NIL))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NLISTP X)
                         (NOT (NUMBERP X))
                         (NOT (EQUAL X 'T))
                         (NOT (EQUAL X 'F))
                         (NOT (EQUAL X NIL)))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (EQUAL (CAR X) 'QUOTE))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (EQUAL (CAR X) 'IF)
                         (BTMP (EV 'AL (CADR X) VA FA N))
                         (p 'AL (CADR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (EQUAL (CAR X) 'IF)
                         (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                         (EV 'AL (CADR X) VA FA N)
                         (p 'AL (CADR X) VA FA N K)
                         (p 'AL (CADDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (EQUAL (CAR X) 'IF)
                         (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                         (NOT (EV 'AL (CADR X) VA FA N))
                         (p 'AL (CADR X) VA FA N K)
                         (p 'AL (CADDDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (NOT (EQUAL (CAR X) 'IF))
                         (BTMP (EV 'LIST (CDR X) VA FA N))
                         (p 'LIST (CDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (NOT (EQUAL (CAR X) 'IF))
                         (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                         (UNSOLV-SUBRP (CAR X))
                         (p 'LIST (CDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (NOT (EQUAL (CAR X) 'IF))
                         (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                         (NOT (UNSOLV-SUBRP (CAR X)))
                         (BTMP (GET (CAR X) FA))
                         (p 'LIST (CDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (NOT (EQUAL (CAR X) 'IF))
                         (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                         (NOT (UNSOLV-SUBRP (CAR X)))
                         (NOT (BTMP (GET (CAR X) FA)))
                         (ZEROP N)
                         (p 'LIST (CDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (EQUAL FLG 'AL)
                         (NOT (NLISTP X))
                         (NOT (EQUAL (CAR X) 'QUOTE))
                         (NOT (EQUAL (CAR X) 'IF))
                         (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                         (NOT (UNSOLV-SUBRP (CAR X)))
                         (NOT (BTMP (GET (CAR X) FA)))
                         (NOT (ZEROP N))
                         (p 'AL
                            (CADR (GET (CAR X) FA))
                            (PAIRLIST (CAR (GET (CAR X) FA))
                                      (EV 'LIST (CDR X) VA FA N))
                            FA
                            (SUB1 N)
                            (SUB1 K))
                         (p 'LIST (CDR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                         (LISTP X)
                         (BTMP (EV 'AL (CAR X) VA FA N))
                         (p 'AL (CAR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                         (LISTP X)
                         (NOT (BTMP (EV 'AL (CAR X) VA FA N)))
                         (BTMP (EV 'LIST (CDR X) VA FA N))
                         (p 'LIST (CDR X) VA FA N K)
                         (p 'AL (CAR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                         (LISTP X)
                         (NOT (BTMP (EV 'AL (CAR X) VA FA N)))
                         (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                         (p 'LIST (CDR X) VA FA N K)
                         (p 'AL (CAR X) VA FA N K))
                    (p FLG X VA FA N K))
           (IMPLIES (AND (NOT (EQUAL FLG 'AL))
                         (NOT (LISTP X)))
                    (p FLG X VA FA N K))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, CAR-LESSEQP,
CDR-LESSP, CDR-LESSEQP, ADD1-SUB1, and CAR-LESSP, and the definitions of
ORDINALP, LESSP, ORD-LESSP, EQUAL, NLISTP, BTMP, UNSOLV-SUBRP, CDR, CAR, LISTP,
MEMBER, and ZEROP can be used to show that the measure:
      (CONS (ADD1 N) (COUNT X))
decreases according to the well-founded relation ORD-LESSP in each induction
step of the scheme.  Note, however, the inductive instances chosen for K, FLG,
and VA.  The above induction scheme generates 40 new conjectures:

Case 40.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NUMBERP X)
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up the functions NLISTP, EQUAL, and EV, to:

        T.

Case 39.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (EQUAL X 'T)
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up the definitions of NLISTP, NUMBERP, LISTP,
  EQUAL, EV, and BTMP, to:

        T.

Case 38.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (EQUAL X 'F)
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding the functions NLISTP, NUMBERP, EQUAL, LISTP, EV,
  and BTMP, to:

        T.

Case 37.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (NOT (EQUAL X 'F))
                      (EQUAL X NIL)
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up the definitions of NLISTP, NUMBERP, EQUAL,
  LISTP, EV, and BTMP, to:

        T.

Case 36.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NLISTP X)
                      (NOT (NUMBERP X))
                      (NOT (EQUAL X 'T))
                      (NOT (EQUAL X 'F))
                      (NOT (EQUAL X NIL))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding the functions NLISTP, EQUAL, and EV, to:

        T.

Case 35.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (EQUAL (CAR X) 'QUOTE)
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, unfolding NLISTP, EQUAL, and EV, to:

        T.

Case 34.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDR X) VA FA N))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

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

        T.

Case 33.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDR X) VA FA N))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, unfolding NLISTP, EQUAL, and EV, to:

        T.

Case 32.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding the functions NLISTP, EQUAL, EV, and BTMP, to:

        T.

Case 31.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding NLISTP, EQUAL, and EV, to:

        T.

Case 30.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (EQUAL (EV 'AL (CADDR X) VA FA N)
                             (EV 'AL (CADDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up the functions NLISTP, EQUAL, EV, and BTMP, to:

        T.

Case 29.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (EV 'AL (CADR X) VA FA N)
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (EQUAL (EV 'AL (CADDR X) VA FA N)
                             (EV 'AL (CADDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, unfolding the functions NLISTP, EQUAL, and EV, to:

        T.

Case 28.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDDR X) VA FA N))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up the definitions of NLISTP, EQUAL, BTMP, and EV,
  to:

        T.

Case 27.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDDR X) VA FA N))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, unfolding NLISTP, EQUAL, BTMP, and EV, to:

        T.

Case 26.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up NLISTP, EQUAL, BTMP, and EV, to:

        T.

Case 25.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (BTMP (EV 'AL (CADDDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, opening up NLISTP, EQUAL, BTMP, and EV, to:

        T.

Case 24.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (BTMP (EV 'AL (CADR X) VA FA N))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding NLISTP, EQUAL, EV, and BTMP, to:

        T.

Case 23.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (BTMP (EV 'AL (CADR X) VA FA K))
                      (EQUAL (EV 'AL (CADDDR X) VA FA N)
                             (EV 'AL (CADDDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, unfolding the functions NLISTP, EQUAL, BTMP, and EV, to:

        T.

Case 22.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (EQUAL (CAR X) 'IF)
                      (NOT (BTMP (EV 'AL (CADR X) VA FA N)))
                      (NOT (EV 'AL (CADR X) VA FA N))
                      (EQUAL (EV 'AL (CADR X) VA FA N)
                             (EV 'AL (CADR X) VA FA K))
                      (EQUAL (EV 'AL (CADDDR X) VA FA N)
                             (EV 'AL (CADDDR X) VA FA K))
                      (NOT (BTMP (EV FLG X VA FA N)))
                      (NOT (BTMP (EV FLG X VA FA K))))
                 (EQUAL (EV FLG X VA FA N)
                        (EV FLG X VA FA K))),

  which simplifies, expanding the functions NLISTP, EQUAL, BTMP, and EV, to:

        T.

Case 21.(IMPLIES (AND (EQUAL FLG 'AL)
                      (NOT (NLISTP X))
                      (NOT (EQUAL (CAR X) 'QUOTE))
                      (NOT (EQUAL (CAR X) 'IF))
                      (NOT (BTMP (EV 'LIST (CDR X) VA FA N)))
                      (UNSOLV-SUBRP (CAR X))
                      (BTMP (EV 'LIST (CDR X) VA FA K))