(NOTE-LIB "unsolv" T)
Loading ./basic/unsolv.lib
Finished loading ./basic/unsolv.lib
Loading ./basic/unsolv.o
Finished loading ./basic/unsolv.o

(#./basic/unsolv.lib #./basic/unsolv)


(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


(DEFN SYMBOL (X) (MEMBER X '(0 1)))

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




[ 0.0 0.0 0.0 ]

SYMBOL


(DEFN HALF-TAPE
      (X)
      (IF (NLISTP X)
          (EQUAL X 0)
          (AND (SYMBOL (CAR X))
               (HALF-TAPE (CDR X)))))

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




[ 0.0 0.0 0.0 ]

HALF-TAPE


(DEFN TAPE
      (X)
      (AND (LISTP X)
           (HALF-TAPE (CAR X))
           (HALF-TAPE (CDR X))))

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




[ 0.0 0.0 0.0 ]

TAPE


(DEFN OPERATION
      (X)
      (MEMBER X '(L R 0 1)))

     From the definition we can conclude that:
      (OR (FALSEP (OPERATION X))
          (TRUEP (OPERATION X)))
is a theorem.




[ 0.0 0.0 0.0 ]

OPERATION


(DEFN STATE (X) (LITATOM X))

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




[ 0.0 0.0 0.0 ]

STATE


(DEFN TURING-4TUPLE
      (X)
      (AND (LISTP X)
           (STATE (CAR X))
           (SYMBOL (CADR X))
           (OPERATION (CADDR X))
           (STATE (CADDDR X))
           (EQUAL (CDDDDR X) NIL)))

     Note that (OR (FALSEP (TURING-4TUPLE X)) (TRUEP (TURING-4TUPLE X))) is a
theorem.




[ 0.0 0.0 0.0 ]

TURING-4TUPLE


(DEFN TURING-MACHINE
      (X)
      (IF (NLISTP X)
          (EQUAL X NIL)
          (AND (TURING-4TUPLE (CAR X))
               (TURING-MACHINE (CDR X)))))

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




[ 0.0 0.0 0.0 ]

TURING-MACHINE


(DEFN INSTR
      (ST SYM TM)
      (IF (LISTP TM)
          (IF (EQUAL ST (CAR (CAR TM)))
              (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                  (CDR (CDR (CAR TM)))
                  (INSTR ST SYM (CDR TM)))
              (INSTR ST SYM (CDR TM)))
          F))

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




[ 0.0 0.0 0.0 ]

INSTR


(DEFN NEW-TAPE
      (OP TAPE)
      (IF (EQUAL OP 'L)
          (CONS (CDR (CAR TAPE))
                (CONS (CAR (CAR TAPE)) (CDR TAPE)))
          (IF (EQUAL OP 'R)
              (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                    (CDR (CDR TAPE)))
              (CONS (CAR TAPE)
                    (CONS OP (CDR (CDR TAPE)))))))

     Observe that (LISTP (NEW-TAPE OP TAPE)) is a theorem.




[ 0.0 0.0 0.0 ]

NEW-TAPE


(DEFN TMI
      (ST TAPE TM N)
      (IF (ZEROP N)
          (BTM)
          (IF (INSTR ST (CAR (CDR TAPE)) TM)
              (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                   (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                             TAPE)
                   TM
                   (SUB1 N))
              TAPE)))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, TMI is accepted
under the principle of definition.  Observe that:
      (OR (OR (LISTP (TMI ST TAPE TM N))
              (BTMP (TMI ST TAPE TM N)))
          (EQUAL (TMI ST TAPE TM N) TAPE))
is a theorem.




[ 0.0 0.1 0.0 ]

TMI


(DEFN INSTR-DEFN NIL
      '((ST SYM TM)
        (IF (LISTP TM)
            (IF (EQUAL ST (CAR (CAR TM)))
                (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                    (CDR (CDR (CAR TM)))
                    (INSTR ST SYM (CDR TM)))
                (INSTR ST SYM (CDR TM)))
            F)))

     From the definition we can conclude that (LISTP (INSTR-DEFN)) is a
theorem.




[ 0.0 0.0 0.0 ]

INSTR-DEFN


(DEFN NEW-TAPE-DEFN NIL
      '((OP TAPE)
        (IF (EQUAL OP 'L)
            (CONS (CDR (CAR TAPE))
                  (CONS (CAR (CAR TAPE)) (CDR TAPE)))
            (IF (EQUAL OP 'R)
                (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                      (CDR (CDR TAPE)))
                (CONS (CAR TAPE)
                      (CONS OP (CDR (CDR TAPE))))))))

     Note that (LISTP (NEW-TAPE-DEFN)) is a theorem.




[ 0.0 0.0 0.0 ]

NEW-TAPE-DEFN


(DEFN TMI-DEFN NIL
      '((ST TAPE TM)
        (IF (INSTR ST (CAR (CDR TAPE)) TM)
            (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                 (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                           TAPE)
                 TM)
            TAPE)))

     Note that (LISTP (TMI-DEFN)) is a theorem.




[ 0.0 0.0 0.0 ]

TMI-DEFN


(DEFN KWOTE (X) (LIST 'QUOTE X))

     Observe that (LISTP (KWOTE X)) is a theorem.




[ 0.0 0.0 0.0 ]

KWOTE


(DEFN TMI-FA
      (TM)
      (LIST (LIST 'TM NIL (KWOTE TM))
            (CONS 'INSTR (INSTR-DEFN))
            (CONS 'NEW-TAPE (NEW-TAPE-DEFN))
            (CONS 'TMI (TMI-DEFN))))

     Observe that (LISTP (TMI-FA TM)) is a theorem.




[ 0.0 0.0 0.0 ]

TMI-FA


(DEFN TMI-X
      (ST TAPE)
      (LIST 'TMI
            (KWOTE ST)
            (KWOTE TAPE)
            '(TM)))

     From the definition we can conclude that (LISTP (TMI-X ST TAPE)) is a
theorem.




[ 0.0 0.0 0.0 ]

TMI-X


(DEFN LENGTH
      (X)
      (IF (NLISTP X)
          0
          (ADD1 (LENGTH (CDR X)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, LENGTH is
accepted under the principle of definition.  From the definition we can
conclude that (NUMBERP (LENGTH X)) is a theorem.




[ 0.0 0.0 0.0 ]

LENGTH


(DEFN TMI-K
      (ST TAPE TM N)
      (DIFFERENCE N (ADD1 (LENGTH TM))))

WARNING:  ST and TAPE are in the arglist but not in the body of the definition
of TMI-K.


     Observe that (NUMBERP (TMI-K ST TAPE TM N)) is a theorem.




[ 0.0 0.0 0.0 ]

TMI-K


(DEFN TMI-N
      (ST TAPE TM K)
      (PLUS K (ADD1 (LENGTH TM))))

WARNING:  ST and TAPE are in the arglist but not in the body of the definition
of TMI-N.


     Observe that (NUMBERP (TMI-N ST TAPE TM K)) is a theorem.




[ 0.0 0.0 0.0 ]

TMI-N


(PROVE-LEMMA LENGTH-0
             (REWRITE)
             (EQUAL (EQUAL (LENGTH X) 0)
                    (NLISTP X)))

This formula simplifies, opening up the definition of NLISTP, to two new
conjectures:

Case 2. (IMPLIES (NOT (EQUAL (LENGTH X) 0))
                 (LISTP X)),

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

        T.

Case 1. (IMPLIES (EQUAL (LENGTH X) 0)
                 (NOT (LISTP X))),

  which we will name *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 X) (p X))
           (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X)))
                    (p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces three new formulas:

Case 3. (IMPLIES (AND (NLISTP X) (EQUAL (LENGTH X) 0))
                 (NOT (LISTP X))),

  which simplifies, opening up NLISTP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (EQUAL (LENGTH (CDR X)) 0))
                      (EQUAL (LENGTH X) 0))
                 (NOT (LISTP X))),

  which simplifies, opening up NLISTP and LENGTH, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (LISTP (CDR X)))
                      (EQUAL (LENGTH X) 0))
                 (NOT (LISTP X))),

  which simplifies, expanding the definitions of NLISTP and LENGTH, to:

        T.


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


[ 0.0 0.0 0.0 ]

LENGTH-0


(PROVE-LEMMA PLUS-EQUAL-0
             (REWRITE)
             (EQUAL (EQUAL (PLUS I J) 0)
                    (AND (ZEROP I) (ZEROP J))))

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

Case 6. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
                      (NOT (NUMBERP I)))
                 (NOT (EQUAL J 0))),

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

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
                      (NOT (NUMBERP I)))
                 (NUMBERP J)),

  which again simplifies, unfolding PLUS and EQUAL, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
                      (EQUAL I 0))
                 (NOT (EQUAL J 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
                      (EQUAL I 0))
                 (NUMBERP J)),

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

        T.

Case 2. (IMPLIES (AND (EQUAL (PLUS I J) 0)
                      (NOT (EQUAL I 0)))
                 (NOT (NUMBERP I))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (PLUS I J) 0)
                      (NOT (EQUAL J 0)))
                 (NOT (NUMBERP J))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-EQUAL-0


(PROVE-LEMMA PLUS-DIFFERENCE
             (REWRITE)
             (EQUAL (PLUS (DIFFERENCE I J) J)
                    (IF (LEQ I J) (FIX J) I)))

This simplifies, expanding FIX, to three new goals:

Case 3. (IMPLIES (AND (NOT (LESSP J I)) (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)),

  which we will name *1.

Case 2. (IMPLIES (AND (NOT (LESSP J I))
                      (NOT (NUMBERP J)))
                 (EQUAL (PLUS (DIFFERENCE I J) J) 0)).

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

        T.

Case 1. (IMPLIES (LESSP J I)
                 (EQUAL (PLUS (DIFFERENCE I J) J) I)),

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

  Case 1.2.
          (IMPLIES (AND (LESSP I J) (LESSP J I))
                   (EQUAL (PLUS (DIFFERENCE I J) J) I)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (NUMBERP I)) (LESSP J I))
                   (EQUAL (PLUS (DIFFERENCE I J) J) I)),

    which again simplifies, unfolding LESSP, to:

          T.


     So we now return to:

      (IMPLIES (AND (NOT (LESSP J I)) (NUMBERP J))
               (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

Case 4. (IMPLIES (AND (OR (EQUAL I 0) (NOT (NUMBERP I)))
                      (NOT (LESSP J I))
                      (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (OR (EQUAL J 0) (NOT (NUMBERP J)))
                      (NOT (LESSP J I))
                      (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                      (LESSP (SUB1 J) (SUB1 I))
                      (NOT (LESSP J I))
                      (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)),

  which simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP I 1)
                      (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                      (LESSP (SUB1 J) (SUB1 I))
                      (NOT (LESSP J I))
                      (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)).

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

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                      (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                   (SUB1 J))
                             (SUB1 J))
                      (NOT (LESSP J I))
                      (NUMBERP J))
                 (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

  Case 1.4.
          (IMPLIES (AND (LESSP I J)
                        (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                        (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP J I))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

    Case 1.4.3.
            (IMPLIES (AND (EQUAL J 0)
                          (LESSP I J)
                          (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                          (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                          (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                       (SUB1 J))
                                 (SUB1 J))
                          (NOT (LESSP J I))
                          (NUMBERP J))
                     (EQUAL (PLUS (DIFFERENCE I J) J) J)),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 1.4.2.
            (IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
                          (LESSP I J)
                          (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                          (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                          (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                       (SUB1 J))
                                 (SUB1 J))
                          (NOT (LESSP J I))
                          (NUMBERP J))
                     (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

            (IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
                          (NOT (EQUAL J 0))
                          (NOT (EQUAL I 0))
                          (NUMBERP I)
                          (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                       (SUB1 J))
                                 (SUB1 J))
                          (NOT (LESSP (SUB1 J) (SUB1 I)))
                          (NUMBERP J))
                     (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                  J)
                            J)).

      Appealing to the lemma SUB1-ELIM, we now replace I by (ADD1 X) to
      eliminate (SUB1 I).  We rely upon the type restriction lemma noted when
      SUB1 was introduced to constrain the new variable.  This generates the
      formula:

            (IMPLIES (AND (NUMBERP X)
                          (LESSP X (SUB1 J))
                          (NOT (EQUAL J 0))
                          (NOT (EQUAL (ADD1 X) 0))
                          (EQUAL (PLUS (DIFFERENCE X (SUB1 J))
                                       (SUB1 J))
                                 (SUB1 J))
                          (NOT (LESSP (SUB1 J) X))
                          (NUMBERP J))
                     (EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
                            J)).

      This further simplifies, clearly, to the new formula:

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

      Applying the lemma SUB1-ELIM, replace J by (ADD1 Z) to eliminate
      (SUB1 J).  We rely upon the type restriction lemma noted when SUB1 was
      introduced to restrict the new variable.  This produces:

            (IMPLIES (AND (NUMBERP Z)
                          (NUMBERP X)
                          (LESSP X Z)
                          (NOT (EQUAL (ADD1 Z) 0))
                          (EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
                          (NOT (LESSP Z X)))
                     (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                            (ADD1 Z))),

      which further simplifies, obviously, to the new formula:

            (IMPLIES (AND (NUMBERP X)
                          (LESSP X Z)
                          (EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
                          (NOT (LESSP Z X)))
                     (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                            (ADD1 Z))).

      We use the above equality hypothesis by cross-fertilizing:
            (PLUS (DIFFERENCE X Z) Z)
      for Z and throwing away the equality.  The result is:

            (IMPLIES (AND (NUMBERP X)
                          (LESSP X Z)
                          (NOT (LESSP Z X)))
                     (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                            (ADD1 (PLUS (DIFFERENCE X Z) Z)))).

      We will try to prove the above formula by generalizing it, replacing
      (DIFFERENCE X Z) by Y.  We restrict the new variable by recalling the
      type restriction lemma noted when DIFFERENCE was introduced.  We would
      thus like to prove:

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

      which finally simplifies, using linear arithmetic, to:

            T.

    Case 1.4.1.
            (IMPLIES (AND (LESSP I 1)
                          (LESSP I J)
                          (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                          (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                          (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                       (SUB1 J))
                                 (SUB1 J))
                          (NOT (LESSP J I))
                          (NUMBERP J))
                     (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

            T.

  Case 1.3.
          (IMPLIES (AND (EQUAL J 0)
                        (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                        (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP J I))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE I J) J) J)),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (LESSP I 0)
                        (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                        (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0))))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 0))
                                     (SUB1 0))
                               (SUB1 0))
                        (NOT (LESSP 0 I))
                        (NUMBERP 0))
                   (EQUAL (PLUS (DIFFERENCE I 0) 0) 0)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
                        (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                        (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP J I))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE I J) J) J)),

    which again simplifies, unfolding the definitions of NOT, OR, LESSP, and
    DIFFERENCE, to the conjecture:

          (IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL J 0))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP (SUB1 J) (SUB1 I)))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                J)
                          J)).

    Appealing to the lemma SUB1-ELIM, we now replace I by (ADD1 X) to
    eliminate (SUB1 I).  We employ the type restriction lemma noted when SUB1
    was introduced to constrain the new variable.  This generates the goal:

          (IMPLIES (AND (NUMBERP X)
                        (LESSP X (SUB1 J))
                        (NOT (EQUAL (ADD1 X) 0))
                        (NOT (EQUAL J 0))
                        (EQUAL (PLUS (DIFFERENCE X (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP (SUB1 J) X))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
                          J)).

    This further simplifies, trivially, to:

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

    Applying the lemma SUB1-ELIM, replace J by (ADD1 Z) to eliminate (SUB1 J).
    We rely upon the type restriction lemma noted when SUB1 was introduced to
    restrict the new variable.  We thus obtain the new conjecture:

          (IMPLIES (AND (NUMBERP Z)
                        (NUMBERP X)
                        (LESSP X Z)
                        (NOT (EQUAL (ADD1 Z) 0))
                        (EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
                        (NOT (LESSP Z X)))
                   (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                          (ADD1 Z))),

    which further simplifies, trivially, to:

          (IMPLIES (AND (NUMBERP X)
                        (LESSP X Z)
                        (EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
                        (NOT (LESSP Z X)))
                   (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                          (ADD1 Z))).

    We now use the above equality hypothesis by cross-fertilizing:
          (PLUS (DIFFERENCE X Z) Z)
    for Z and throwing away the equality.  This generates:

          (IMPLIES (AND (NUMBERP X)
                        (LESSP X Z)
                        (NOT (LESSP Z X)))
                   (EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
                          (ADD1 (PLUS (DIFFERENCE X Z) Z)))).

    We will try to prove the above formula by generalizing it, replacing
    (DIFFERENCE X Z) by Y.  We restrict the new variable by recalling the type
    restriction lemma noted when DIFFERENCE was introduced.  This produces:

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

    which finally simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LESSP I 1)
                        (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                        (NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
                        (EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
                                     (SUB1 J))
                               (SUB1 J))
                        (NOT (LESSP J I))
                        (NUMBERP J))
                   (EQUAL (PLUS (DIFFERENCE I J) J) J)),

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

          T.


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


[ 0.0 0.0 0.1 ]

PLUS-DIFFERENCE


(TOGGLE DIFFERENCE-OFF DIFFERENCE T)

[ 0.0 0.0 0.0 ]

DIFFERENCE-OFF


(PROVE-LEMMA PR-EVAL-FN-0
             (REWRITE)
             (IMPLIES (AND (ZEROP N)
                           (NOT (EQUAL FN 'QUOTE))
                           (NOT (EQUAL FN 'IF))
                           (NOT (UNSOLV-SUBRP FN))
                           (EQUAL VARGS
                                  (EV 'LIST ARGS VA FA N)))
                      (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                             (BTM))))

WARNING:  Note that PR-EVAL-FN-0 contains the free variable VARGS which will
be chosen by instantiating the hypothesis:
      (EQUAL VARGS
             (EV 'LIST ARGS VA FA N)).



This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
and UNSOLV-SUBRP, to:

      (IMPLIES (AND (ZEROP N)
                    (NOT (EQUAL FN 'QUOTE))
                    (NOT (EQUAL FN 'IF))
                    (NOT (MEMBER FN
                                 '(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS
                                        CAR CDR LISTP PACK UNPACK LITATOM
                                        EQUAL LIST)))
                    (EQUAL VARGS
                           (EV 'LIST ARGS VA FA N)))
               (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                      (BTM))).

This simplifies, applying the lemmas CDR-CONS and CAR-CONS, and expanding the
definitions of ZEROP, CDR, CAR, LISTP, MEMBER, UNSOLV-SUBRP, EQUAL, and EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-FN-0


(PROVE-LEMMA PR-EVAL-FN-1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (NOT (EQUAL FN 'QUOTE))
                           (NOT (EQUAL FN 'IF))
                           (NOT (UNSOLV-SUBRP FN))
                           (EQUAL VARGS
                                  (EV 'LIST ARGS VA FA N)))
                      (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                             (IF (BTMP VARGS)
                                 (BTM)
                                 (IF (BTMP (GET FN FA))
                                     (BTM)
                                     (EV 'AL
                                         (CADR (GET FN FA))
                                         (PAIRLIST (CAR (GET FN FA)) VARGS)
                                         FA
                                         (SUB1 N)))))))

WARNING:  Note that PR-EVAL-FN-1 contains the free variable VARGS which will
be chosen by instantiating the hypothesis:
      (EQUAL VARGS
             (EV 'LIST ARGS VA FA N)).



This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
IMPLIES, and UNSOLV-SUBRP, to:

      (IMPLIES (AND (NOT (EQUAL N 0))
                    (NUMBERP N)
                    (NOT (EQUAL FN 'QUOTE))
                    (NOT (EQUAL FN 'IF))
                    (NOT (MEMBER FN
                                 '(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS
                                        CAR CDR LISTP PACK UNPACK LITATOM
                                        EQUAL LIST)))
                    (EQUAL VARGS
                           (EV 'LIST ARGS VA FA N)))
               (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                      (COND ((BTMP VARGS) (BTM))
                            ((BTMP (GET FN FA)) (BTM))
                            (T (EV 'AL
                                   (CADR (GET FN FA))
                                   (PAIRLIST (CAR (GET FN FA)) VARGS)
                                   FA
                                   (SUB1 N)))))).

This simplifies, unfolding the functions CDR, CAR, LISTP, and MEMBER, to the
following three new formulas:

Case 3. (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (EQUAL FN 'QUOTE))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN 'ZERO))
                      (NOT (EQUAL FN 'TRUE))
                      (NOT (EQUAL FN 'FALSE))
                      (NOT (EQUAL FN 'ADD1))
                      (NOT (EQUAL FN 'SUB1))
                      (NOT (EQUAL FN 'NUMBERP))
                      (NOT (EQUAL FN 'CONS))
                      (NOT (EQUAL FN 'CAR))
                      (NOT (EQUAL FN 'CDR))
                      (NOT (EQUAL FN 'LISTP))
                      (NOT (EQUAL FN 'PACK))
                      (NOT (EQUAL FN 'UNPACK))
                      (NOT (EQUAL FN 'LITATOM))
                      (NOT (EQUAL FN 'EQUAL))
                      (NOT (EQUAL FN 'LIST))
                      (BTMP (EV 'LIST ARGS VA FA N)))
                 (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                        (BTM))).

  But this again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
  opening up the definitions of EQUAL and EV, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (EQUAL FN 'QUOTE))
                      (NOT (EQUAL FN 'IF))
                      (NOT (EQUAL FN 'ZERO))
                      (NOT (EQUAL FN 'TRUE))
                      (NOT (EQUAL FN 'FALSE))
                      (NOT (EQUAL FN 'ADD1))
                      (NOT (EQUAL FN 'SUB1))
                      (NOT (EQUAL FN 'NUMBERP))
                      (NOT (EQUAL FN 'CONS))
                      (NOT (EQUAL FN 'CAR))
                      (NOT (EQUAL FN 'CDR))
                      (NOT (EQUAL FN 'LISTP))
                      (NOT (EQUAL FN 'PACK))
                      (NOT (EQUAL FN 'UNPACK))
                      (NOT (EQUAL FN 'LITATOM))
                      (NOT (EQUAL FN 'EQUAL))
                      (NOT (EQUAL FN 'LIST))
                      (BTMP (GET FN FA)))
                 (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                        (BTM))),

  which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding
  UNSOLV-SUBRP, CDR, CAR, LISTP, MEMBER, EQUAL, and EV, to:

        T.

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

  However this again simplifies, rewriting with the lemmas CDR-CONS and
  CAR-CONS, and opening up the functions UNSOLV-SUBRP, CDR, CAR, LISTP, MEMBER,
  EQUAL, and EV, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PR-EVAL-FN-1


(PROVE-LEMMA PR-EVAL-UNSOLV-SUBRP
             (REWRITE)
             (IMPLIES (AND (UNSOLV-SUBRP FN)
                           (EQUAL VARGS
                                  (EV 'LIST ARGS VA FA N)))
                      (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                             (IF (BTMP VARGS)
                                 (BTM)
                                 (UNSOLV-APPLY-SUBR FN VARGS)))))

WARNING:  Note that PR-EVAL-UNSOLV-SUBRP contains the free variable VARGS
which will be chosen by instantiating the hypothesis:
      (EQUAL VARGS
             (EV 'LIST ARGS VA FA N)).



This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
UNSOLV-SUBRP, to:

      (IMPLIES (AND (MEMBER FN
                            '(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS CAR CDR
                                   LISTP PACK UNPACK LITATOM EQUAL LIST))
                    (EQUAL VARGS
                           (EV 'LIST ARGS VA FA N)))
               (EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
                      (IF (BTMP VARGS)
                          (BTM)
                          (UNSOLV-APPLY-SUBR FN VARGS)))).

This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
functions CDR, CAR, LISTP, MEMBER, UNSOLV-APPLY-SUBR, UNSOLV-SUBRP, EQUAL, and
EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-UNSOLV-SUBRP


(PROVE-LEMMA PR-EVAL-IF
             (REWRITE)
             (IMPLIES (EQUAL VX1 (EV 'AL X1 VA FA N))
                      (EQUAL (EV 'AL (LIST 'IF X1 X2 X3) VA FA N)
                             (IF (BTMP VX1)
                                 (BTM)
                                 (IF VX1
                                     (EV 'AL X2 VA FA N)
                                     (EV 'AL X3 VA FA N))))))

WARNING:  Note that PR-EVAL-IF contains the free variable VX1 which will be
chosen by instantiating the hypothesis (EQUAL VX1 (EV (QUOTE AL) X1 VA FA N)).


This simplifies, applying CDR-CONS and CAR-CONS, and opening up the functions
EQUAL and EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-IF


(PROVE-LEMMA PR-EVAL-QUOTE
             (REWRITE)
             (EQUAL (EV 'AL (LIST 'QUOTE X) VA FA N)
                    X))

This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up EQUAL
and EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-QUOTE


(PROVE-LEMMA PR-EVAL-NLISTP
             (REWRITE)
             (AND (EQUAL (EV 'AL 0 VA FA N) 0)
                  (EQUAL (EV 'AL (ADD1 N) VA FA N)
                         (ADD1 N))
                  (EQUAL (EV 'AL (PACK X) VA FA N)
                         (IF (EQUAL (PACK X) 'T)
                             T
                             (IF (EQUAL (PACK X) 'F)
                                 F
                                 (IF (EQUAL (PACK X) 'NIL)
                                     NIL
                                     (GET (PACK X) VA)))))))

WARNING:  Note that the proposed lemma PR-EVAL-NLISTP is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and three replacement rules.


This formula can be simplified, using the abbreviations AND and PACK-EQUAL, to
the following three new formulas:

Case 3. (EQUAL (EV 'AL 0 VA FA N) 0).

  This simplifies, unfolding NUMBERP, LISTP, EQUAL, and EV, to:

        T.

Case 2. (EQUAL (EV 'AL (ADD1 N) VA FA N)
               (ADD1 N)).

  This simplifies, expanding EQUAL and EV, to:

        T.

Case 1. (EQUAL (EV 'AL (PACK X) VA FA N)
               (CASE X
                     ((84 . 0) T)
                     ((70 . 0) F)
                     ((78 73 76 . 0) NIL)
                     (OTHERWISE (GET (PACK X) VA)))).

  This simplifies, rewriting with the lemmas PACK-EQUAL and UNPACK-PACK, and
  expanding UNPACK, EQUAL, and EV, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-NLISTP


(PROVE-LEMMA EVLIST-NIL
             (REWRITE)
             (EQUAL (EV 'LIST NIL VA FA N) NIL))

This simplifies, unfolding the definitions of LISTP, EQUAL, and EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EVLIST-NIL


(PROVE-LEMMA EVLIST-CONS
             (REWRITE)
             (IMPLIES (AND (EQUAL VX (EV 'AL X VA FA N))
                           (EQUAL VL (EV 'LIST L VA FA N)))
                      (EQUAL (EV 'LIST (CONS X L) VA FA N)
                             (IF (BTMP VX)
                                 (BTM)
                                 (IF (BTMP VL) (BTM) (CONS VX VL))))))

WARNING:  Note that EVLIST-CONS contains the free variables VL and VX which
will be chosen by instantiating the hypotheses:
      (EQUAL VX (EV 'AL X VA FA N))
and (EQUAL VL (EV (QUOTE LIST) L VA FA N)).


This simplifies, applying CDR-CONS and CAR-CONS, and expanding the functions
EQUAL and EV, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EVLIST-CONS


(TOGGLE UNSOLV-SUBRP-OFF UNSOLV-SUBRP T)

[ 0.0 0.0 0.0 ]

UNSOLV-SUBRP-OFF


(TOGGLE EV-OFF EV T)

[ 0.0 0.0 0.0 ]

EV-OFF


(DEFN CNB
      (X)
      (IF (LISTP X)
          (AND (CNB (CAR X)) (CNB (CDR X)))
          (NOT (BTMP X))))

     Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call.  Hence, CNB is accepted under the definitional
principle.  Note that (OR (FALSEP (CNB X)) (TRUEP (CNB X))) is a theorem.




[ 0.0 0.0 0.0 ]

CNB


(PROVE-LEMMA CNB-NBTM
             (REWRITE)
             (IMPLIES (CNB X) (EQUAL (BTMP X) F)))

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

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CNB-NBTM


(PROVE-LEMMA CNB-CONS
             (REWRITE)
             (AND (EQUAL (CNB (CONS A B))
                         (AND (CNB A) (CNB B)))
                  (IMPLIES (CNB X) (CNB (CAR X)))
                  (IMPLIES (CNB X) (CNB (CDR X)))))

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


This formula can be simplified, using the abbreviations IMPLIES and AND, to
the following three new conjectures:

Case 3. (EQUAL (CNB (CONS A B))
               (AND (CNB A) (CNB B))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
  functions CNB and AND, to:

        T.

Case 2. (IMPLIES (CNB X) (CNB (CAR X))),

  which simplifies, applying CAR-NLISTP, and unfolding the function CNB, to:

        T.

Case 1. (IMPLIES (CNB X) (CNB (CDR X))).

  This simplifies, appealing to the lemma CDR-NLISTP, and expanding the
  function CNB, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CNB-CONS


(PROVE-LEMMA CNB-LITATOM
             (REWRITE)
             (IMPLIES (LITATOM X) (CNB X)))

This simplifies, expanding the function CNB, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CNB-LITATOM


(PROVE-LEMMA CNB-NUMBERP
             (REWRITE)
             (IMPLIES (NUMBERP X) (CNB X)))

This simplifies, expanding the function CNB, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CNB-NUMBERP


(TOGGLE CNB-OFF CNB T)

[ 0.0 0.0 0.0 ]

CNB-OFF


(PROVE-LEMMA GET-TMI-FA
             (REWRITE)
             (AND (EQUAL (GET 'TM (TMI-FA TM))
                         (LIST NIL (KWOTE TM)))
                  (EQUAL (GET 'INSTR (TMI-FA TM))
                         (INSTR-DEFN))
                  (EQUAL (GET 'NEW-TAPE (TMI-FA TM))
                         (NEW-TAPE-DEFN))
                  (EQUAL (GET 'TMI (TMI-FA TM))
                         (TMI-DEFN))))

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


This conjecture can be simplified, using the abbreviations AND, TMI-DEFN,
NEW-TAPE-DEFN, INSTR-DEFN, KWOTE, and TMI-FA, to four new goals:

Case 4. (EQUAL
         (GET 'TM
           (CONS (LIST 'TM NIL (LIST 'QUOTE TM))
                 '((INSTR (ST SYM TM)
                          (IF (LISTP TM)
                              (IF (EQUAL ST (CAR (CAR TM)))
                                  (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                                      (CDR (CDR (CAR TM)))
                                      (INSTR ST SYM (CDR TM)))
                                  (INSTR ST SYM (CDR TM)))
                              F))
                   (NEW-TAPE (OP TAPE)
                             (IF (EQUAL OP 'L)
                                 (CONS (CDR (CAR TAPE))
                                       (CONS (CAR (CAR TAPE)) (CDR TAPE)))
                                 (IF (EQUAL OP 'R)
                                     (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                                           (CDR (CDR TAPE)))
                                     (CONS (CAR TAPE)
                                           (CONS OP (CDR (CDR TAPE)))))))
                   (TMI (ST TAPE TM)
                        (IF (INSTR ST (CAR (CDR TAPE)) TM)
                            (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                 (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                 TM)
                            TAPE)))))
         (LIST NIL (LIST 'QUOTE TM))),

  which simplifies, applying CDR-CONS and CAR-CONS, and expanding the
  definitions of EQUAL and GET, to:

        T.

Case 3. (EQUAL
         (GET 'INSTR
           (CONS (LIST 'TM NIL (LIST 'QUOTE TM))
                 '((INSTR (ST SYM TM)
                          (IF (LISTP TM)
                              (IF (EQUAL ST (CAR (CAR TM)))
                                  (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                                      (CDR (CDR (CAR TM)))
                                      (INSTR ST SYM (CDR TM)))
                                  (INSTR ST SYM (CDR TM)))
                              F))
                   (NEW-TAPE (OP TAPE)
                             (IF (EQUAL OP 'L)
                                 (CONS (CDR (CAR TAPE))
                                       (CONS (CAR (CAR TAPE)) (CDR TAPE)))
                                 (IF (EQUAL OP 'R)
                                     (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                                           (CDR (CDR TAPE)))
                                     (CONS (CAR TAPE)
                                           (CONS OP (CDR (CDR TAPE)))))))
                   (TMI (ST TAPE TM)
                        (IF (INSTR ST (CAR (CDR TAPE)) TM)
                            (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                 (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                 TM)
                            TAPE)))))
         '((ST SYM TM)
           (IF (LISTP TM)
               (IF (EQUAL ST (CAR (CAR TM)))
                   (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                       (CDR (CDR (CAR TM)))
                       (INSTR ST SYM (CDR TM)))
                   (INSTR ST SYM (CDR TM)))
               F))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding GET and
  EQUAL, to:

        T.

Case 2. (EQUAL
         (GET 'NEW-TAPE
           (CONS (LIST 'TM NIL (LIST 'QUOTE TM))
                 '((INSTR (ST SYM TM)
                          (IF (LISTP TM)
                              (IF (EQUAL ST (CAR (CAR TM)))
                                  (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                                      (CDR (CDR (CAR TM)))
                                      (INSTR ST SYM (CDR TM)))
                                  (INSTR ST SYM (CDR TM)))
                              F))
                   (NEW-TAPE (OP TAPE)
                             (IF (EQUAL OP 'L)
                                 (CONS (CDR (CAR TAPE))
                                       (CONS (CAR (CAR TAPE)) (CDR TAPE)))
                                 (IF (EQUAL OP 'R)
                                     (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                                           (CDR (CDR TAPE)))
                                     (CONS (CAR TAPE)
                                           (CONS OP (CDR (CDR TAPE)))))))
                   (TMI (ST TAPE TM)
                        (IF (INSTR ST (CAR (CDR TAPE)) TM)
                            (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                 (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                 TM)
                            TAPE)))))
         '((OP TAPE)
           (IF (EQUAL OP 'L)
               (CONS (CDR (CAR TAPE))
                     (CONS (CAR (CAR TAPE)) (CDR TAPE)))
               (IF (EQUAL OP 'R)
                   (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                         (CDR (CDR TAPE)))
                   (CONS (CAR TAPE)
                         (CONS OP (CDR (CDR TAPE)))))))),

  which simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
  definitions of GET and EQUAL, to:

        T.

Case 1. (EQUAL
         (GET 'TMI
           (CONS (LIST 'TM NIL (LIST 'QUOTE TM))
                 '((INSTR (ST SYM TM)
                          (IF (LISTP TM)
                              (IF (EQUAL ST (CAR (CAR TM)))
                                  (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                                      (CDR (CDR (CAR TM)))
                                      (INSTR ST SYM (CDR TM)))
                                  (INSTR ST SYM (CDR TM)))
                              F))
                   (NEW-TAPE (OP TAPE)
                             (IF (EQUAL OP 'L)
                                 (CONS (CDR (CAR TAPE))
                                       (CONS (CAR (CAR TAPE)) (CDR TAPE)))
                                 (IF (EQUAL OP 'R)
                                     (CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
                                           (CDR (CDR TAPE)))
                                     (CONS (CAR TAPE)
                                           (CONS OP (CDR (CDR TAPE)))))))
                   (TMI (ST TAPE TM)
                        (IF (INSTR ST (CAR (CDR TAPE)) TM)
                            (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                 (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                 TM)
                            TAPE)))))
         '((ST TAPE TM)
           (IF (INSTR ST (CAR (CDR TAPE)) TM)
               (TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                    (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                              TAPE)
                    TM)
               TAPE))).

  This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
  functions GET and EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

GET-TMI-FA


(TOGGLE TMI-FA-OFF TMI-FA T)

[ 0.0 0.0 0.0 ]

TMI-FA-OFF


(DEFN INSTRN
      (ST SYM TM N)
      (IF (ZEROP N)
          (BTM)
          (IF (LISTP TM)
              (IF (EQUAL ST (CAR (CAR TM)))
                  (IF (EQUAL SYM (CAR (CDR (CAR TM))))
                      (CDR (CDR (CAR TM)))
                      (INSTRN ST SYM (CDR TM) (SUB1 N)))
                  (INSTRN ST SYM (CDR TM) (SUB1 N)))
              F)))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TM) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, INSTRN is accepted under the definitional principle.
The definition of INSTRN can be justified in another way.  Linear arithmetic,
the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the
measure (COUNT N) decreases according to the well-founded relation LESSP in
each recursive call.




[ 0.0 0.0 0.0 ]

INSTRN


(DEFN PR-EVAL-INSTR-INDUCTION-SCHEME
 (ST SYM TM-- VA TM N)
 (IF
  (ZEROP N)
  T
  (PR-EVAL-INSTR-INDUCTION-SCHEME 'ST
                                  'SYM
                                  '(CDR TM)
                                  (LIST (CONS 'ST
                                              (PR-EVAL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (PR-EVAL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (PR-EVAL TM-- VA (TMI-FA TM) N)))
                                  TM
                                  (SUB1 N))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, PR-EVAL-INSTR-INDUCTION-SCHEME
is accepted under the definitional principle.  From the definition we can
conclude that (TRUEP (PR-EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N)) is
a theorem.




[ 0.0 0.0 0.0 ]

PR-EVAL-INSTR-INDUCTION-SCHEME


(PROVE-LEMMA PR-EVAL-INSTR
             (REWRITE)
             (IMPLIES (AND (CNB (EV 'AL ST VA (TMI-FA TM) N))
                           (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                           (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (EQUAL (EV 'AL
                                 (LIST 'INSTR ST SYM TM--)
                                 VA
                                 (TMI-FA TM)
                                 N)
                             (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                     (EV 'AL SYM VA (TMI-FA TM) N)
                                     (EV 'AL TM-- VA (TMI-FA TM) N)
                                     N)))
             ((INDUCT (PR-EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N))))

This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, AND, and PR-EVAL, to two new goals:

Case 2. (IMPLIES (AND (ZEROP N)
                      (CNB (EV 'AL ST VA (TMI-FA TM) N))
                      (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                      (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (EQUAL (EV 'AL
                            (LIST 'INSTR ST SYM TM--)
                            VA
                            (TMI-FA TM)
                            N)
                        (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                (EV 'AL SYM VA (TMI-FA TM) N)
                                (EV 'AL TM-- VA (TMI-FA TM) N)
                                N))),

  which simplifies, rewriting with EVLIST-CONS, CNB-NBTM, EVLIST-NIL, and
  PR-EVAL-FN-0, and opening up the definitions of ZEROP, BTMP, UNSOLV-SUBRP,
  EQUAL, and INSTRN, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (EQUAL N 0))
          (NUMBERP N)
          (IMPLIES
               (AND (CNB (EV 'AL
                             'ST
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'SYM
                                         (EV 'AL SYM VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N)))
                    (CNB (EV 'AL
                             'SYM
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'SYM
                                         (EV 'AL SYM VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N)))
                    (CNB (EV 'AL
                             '(CDR TM)
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'SYM
                                         (EV 'AL SYM VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N))))
               (EQUAL (EV 'AL
                          '(INSTR ST SYM (CDR TM))
                          (LIST (CONS 'ST
                                      (EV 'AL ST VA (TMI-FA TM) N))
                                (CONS 'SYM
                                      (EV 'AL SYM VA (TMI-FA TM) N))
                                (CONS 'TM
                                      (EV 'AL TM-- VA (TMI-FA TM) N)))
                          (TMI-FA TM)
                          (SUB1 N))
                      (INSTRN (EV 'AL
                                  'ST
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (EV 'AL
                                  'SYM
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (EV 'AL
                                  '(CDR TM)
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (SUB1 N))))
          (CNB (EV 'AL ST VA (TMI-FA TM) N))
          (CNB (EV 'AL SYM VA (TMI-FA TM) N))
          (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
         (EQUAL (EV 'AL
                    (LIST 'INSTR ST SYM TM--)
                    VA
                    (TMI-FA TM)
                    N)
                (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL SYM VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))).

  This simplifies, rewriting with CDR-CONS, CAR-CONS, PR-EVAL-NLISTP,
  EVLIST-CONS, CNB-NBTM, EVLIST-NIL, PR-EVAL-UNSOLV-SUBRP, CNB-CONS,
  GET-TMI-FA, PR-EVAL-IF, and PR-EVAL-FN-1, and expanding the functions PACK,
  EQUAL, GET, BTMP, UNSOLV-SUBRP, UNSOLV-APPLY-SUBR, AND, IMPLIES, INSTR-DEFN,
  CDR, CAR, LISTP, and PAIRLIST, to four new formulas:

  Case 1.4.
          (IMPLIES
                  (AND (NOT (EQUAL N 0))
                       (NUMBERP N)
                       (EQUAL (EV 'AL
                                  '(INSTR ST SYM (CDR TM))
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (EV 'AL SYM VA (TMI-FA TM) N)
                                      (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                      (SUB1 N)))
                       (CNB (EV 'AL ST VA (TMI-FA TM) N))
                       (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                       (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                       (NOT (LISTP (EV 'AL TM-- VA (TMI-FA TM) N))))
                  (EQUAL F
                         (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 N))),

    which again simplifies, rewriting with CDR-NLISTP, and unfolding the
    definitions of LISTP, INSTRN, and EQUAL, to:

          T.

  Case 1.3.
          (IMPLIES
                  (AND (NOT (EQUAL N 0))
                       (NUMBERP N)
                       (EQUAL (EV 'AL
                                  '(INSTR ST SYM (CDR TM))
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (EV 'AL SYM VA (TMI-FA TM) N)
                                      (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                      (SUB1 N)))
                       (CNB (EV 'AL ST VA (TMI-FA TM) N))
                       (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                       (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                       (LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
                       (NOT (EQUAL (EV 'AL ST VA (TMI-FA TM) N)
                                   (CAAR (EV 'AL TM-- VA (TMI-FA TM) N)))))
                  (EQUAL (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                 (SUB1 N))
                         (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 N))).

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

          T.

  Case 1.2.
          (IMPLIES
                  (AND (NOT (EQUAL N 0))
                       (NUMBERP N)
                       (EQUAL (EV 'AL
                                  '(INSTR ST SYM (CDR TM))
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (EV 'AL SYM VA (TMI-FA TM) N)
                                      (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                      (SUB1 N)))
                       (CNB (EV 'AL ST VA (TMI-FA TM) N))
                       (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                       (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                       (LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
                       (NOT (EQUAL (EV 'AL SYM VA (TMI-FA TM) N)
                                   (CADAR (EV 'AL TM-- VA (TMI-FA TM) N)))))
                  (EQUAL (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                 (SUB1 N))
                         (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 N))),

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

          T.

  Case 1.1.
          (IMPLIES
                  (AND (NOT (EQUAL N 0))
                       (NUMBERP N)
                       (EQUAL (EV 'AL
                                  '(INSTR ST SYM (CDR TM))
                                  (LIST (CONS 'ST
                                              (EV 'AL ST VA (TMI-FA TM) N))
                                        (CONS 'SYM
                                              (EV 'AL SYM VA (TMI-FA TM) N))
                                        (CONS 'TM
                                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                                  (TMI-FA TM)
                                  (SUB1 N))
                              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (EV 'AL SYM VA (TMI-FA TM) N)
                                      (CDR (EV 'AL TM-- VA (TMI-FA TM) N))
                                      (SUB1 N)))
                       (CNB (EV 'AL ST VA (TMI-FA TM) N))
                       (CNB (EV 'AL SYM VA (TMI-FA TM) N))
                       (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                       (LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
                       (EQUAL (EV 'AL ST VA (TMI-FA TM) N)
                              (CAAR (EV 'AL TM-- VA (TMI-FA TM) N)))
                       (EQUAL (EV 'AL SYM VA (TMI-FA TM) N)
                              (CADAR (EV 'AL TM-- VA (TMI-FA TM) N))))
                  (EQUAL (CDDAR (EV 'AL TM-- VA (TMI-FA TM) N))
                         (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (EV 'AL SYM VA (TMI-FA TM) N)
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 N))),

    which again simplifies, expanding the function INSTRN, to:

          T.

Q.E.D.


[ 0.0 0.1 0.1 ]

PR-EVAL-INSTR


(PROVE-LEMMA PR-EVAL-NEW-TAPE
             (REWRITE)
             (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                           (CNB (EV 'AL TAPE VA (TMI-FA TM) N)))
                      (EQUAL (EV 'AL
                                 (LIST 'NEW-TAPE OP TAPE)
                                 VA
                                 (TMI-FA TM)
                                 N)
                             (IF (ZEROP N)
                                 (BTM)
                                 (NEW-TAPE (EV 'AL OP VA (TMI-FA TM) N)
                                           (EV 'AL TAPE VA (TMI-FA TM) N))))))

This conjecture simplifies, opening up the definitions of ZEROP and NEW-TAPE,
to the following five new goals:

Case 5. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (NOT (NUMBERP N)))
                 (EQUAL (EV 'AL
                            (LIST 'NEW-TAPE OP TAPE)
                            VA
                            (TMI-FA TM)
                            N)
                        (BTM))).

  This again simplifies, applying the lemmas EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
  and PR-EVAL-FN-0, and expanding the functions BTMP, UNSOLV-SUBRP, EQUAL, and
  ZEROP, to:

        T.

Case 4. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (EQUAL N 0))
                 (EQUAL (EV 'AL
                            (LIST 'NEW-TAPE OP TAPE)
                            VA
                            (TMI-FA TM)
                            N)
                        (BTM))),

  which again simplifies, rewriting with EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
  and PR-EVAL-FN-0, and opening up the functions BTMP, UNSOLV-SUBRP, EQUAL,
  and ZEROP, to:

        T.

Case 3. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
                             'L))
                 (EQUAL (EV 'AL
                            (LIST 'NEW-TAPE OP TAPE)
                            VA
                            (TMI-FA TM)
                            N)
                        (CONS (CDAR (EV 'AL TAPE VA (TMI-FA TM) N))
                              (CONS (CAAR (EV 'AL TAPE VA (TMI-FA TM) N))
                                    (CDR (EV 'AL TAPE VA (TMI-FA TM) N)))))).

  However this again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
  GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
  PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and unfolding CNB,
  BTMP, UNSOLV-SUBRP, EQUAL, NEW-TAPE-DEFN, CDR, CAR, CONS, LISTP, PAIRLIST,
  UNSOLV-APPLY-SUBR, GET, and PACK, to:

        T.

Case 2. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
                                  'L))
                      (NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
                                  'R)))
                 (EQUAL (EV 'AL
                            (LIST 'NEW-TAPE OP TAPE)
                            VA
                            (TMI-FA TM)
                            N)
                        (CONS (CAR (EV 'AL TAPE VA (TMI-FA TM) N))
                              (CONS (EV 'AL OP VA (TMI-FA TM) N)
                                    (CDDR (EV 'AL TAPE VA (TMI-FA TM) N)))))).

  This again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
  GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
  PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and unfolding BTMP,
  UNSOLV-SUBRP, EQUAL, NEW-TAPE-DEFN, CDR, CAR, LISTP, PAIRLIST,
  UNSOLV-APPLY-SUBR, CONS, GET, and PACK, to:

        T.

Case 1. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
                                  'L))
                      (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
                             'R))
                 (EQUAL (EV 'AL
                            (LIST 'NEW-TAPE OP TAPE)
                            VA
                            (TMI-FA TM)
                            N)
                        (CONS (CONS (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                    (CAR (EV 'AL TAPE VA (TMI-FA TM) N)))
                              (CDDR (EV 'AL TAPE VA (TMI-FA TM) N))))).

  But this again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
  GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
  PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and opening up the
  functions CNB, EQUAL, BTMP, UNSOLV-SUBRP, NEW-TAPE-DEFN, CDR, CAR, CONS,
  LISTP, PAIRLIST, UNSOLV-APPLY-SUBR, GET, and PACK, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PR-EVAL-NEW-TAPE


(PROVE-LEMMA CNB-INSTRN
             (REWRITE)
             (IMPLIES (AND (NOT (BTMP (INSTRN ST SYM TM N)))
                           (CNB TM))
                      (CNB (INSTRN ST SYM TM N))))


     Call the conjecture *1.


     Let us appeal to the induction principle.  There are four plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p ST SYM TM N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (LISTP TM)
                         (EQUAL ST (CAAR TM))
                         (EQUAL SYM (CADAR TM)))
                    (p ST SYM TM N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (LISTP TM)
                         (EQUAL ST (CAAR TM))
                         (NOT (EQUAL SYM (CADAR TM)))
                         (p ST SYM (CDR TM) (SUB1 N)))
                    (p ST SYM TM N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (LISTP TM)
                         (NOT (EQUAL ST (CAAR TM)))
                         (p ST SYM (CDR TM) (SUB1 N)))
                    (p ST SYM TM N))
           (IMPLIES (AND (NOT (ZEROP N)) (NOT (LISTP TM)))
                    (p ST SYM TM N))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT TM) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  Note, however, the inductive instances chosen
for N.  The above induction scheme produces nine new formulas:

Case 9. (IMPLIES (AND (ZEROP N)
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, opening up the definitions of ZEROP, EQUAL, INSTRN, and
  BTMP, to:

        T.

Case 8. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (EQUAL ST (CAAR TM))
                      (EQUAL SYM (CADAR TM))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, applying CNB-CONS and CNB-NBTM, and expanding the
  definitions of ZEROP and INSTRN, to:

        T.

Case 7. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (EQUAL ST (CAAR TM))
                      (NOT (EQUAL SYM (CADAR TM)))
                      (BTMP (INSTRN ST SYM (CDR TM) (SUB1 N)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))).

  This simplifies, unfolding the functions ZEROP and INSTRN, to:

        T.

Case 6. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (EQUAL ST (CAAR TM))
                      (NOT (EQUAL SYM (CADAR TM)))
                      (NOT (CNB (CDR TM)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))).

  This simplifies, applying CNB-CONS, and expanding ZEROP, to:

        T.

Case 5. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (EQUAL ST (CAAR TM))
                      (NOT (EQUAL SYM (CADAR TM)))
                      (CNB (INSTRN ST SYM (CDR TM) (SUB1 N)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, rewriting with the lemma CNB-NBTM, and opening up ZEROP
  and INSTRN, to:

        T.

Case 4. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (NOT (EQUAL ST (CAAR TM)))
                      (BTMP (INSTRN ST SYM (CDR TM) (SUB1 N)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, expanding ZEROP and INSTRN, to:

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (NOT (EQUAL ST (CAAR TM)))
                      (NOT (CNB (CDR TM)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, applying CNB-CONS, and expanding the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP TM)
                      (NOT (EQUAL ST (CAAR TM)))
                      (CNB (INSTRN ST SYM (CDR TM) (SUB1 N)))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))).

  This simplifies, applying CNB-NBTM, and expanding the definitions of ZEROP
  and INSTRN, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (LISTP TM))
                      (NOT (BTMP (INSTRN ST SYM TM N)))
                      (CNB TM))
                 (CNB (INSTRN ST SYM TM N))),

  which simplifies, opening up the functions ZEROP, INSTRN, BTMP, and CNB, to:

        T.


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


[ 0.0 0.0 0.0 ]

CNB-INSTRN


(PROVE-LEMMA CNB-NEW-TAPE
             (REWRITE)
             (IMPLIES (AND (CNB OP) (CNB TAPE))
                      (CNB (NEW-TAPE OP TAPE))))

This simplifies, unfolding the definition of NEW-TAPE, to the following three
new goals:

Case 3. (IMPLIES (AND (CNB OP)
                      (CNB TAPE)
                      (NOT (EQUAL OP 'L))
                      (EQUAL OP 'R))
                 (CNB (CONS (CONS (CADR TAPE) (CAR TAPE))
                            (CDDR TAPE)))).

  This again simplifies, applying the lemma CNB-CONS, and opening up the
  definitions of CNB and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (CNB OP)
                      (CNB TAPE)
                      (NOT (EQUAL OP 'L))
                      (NOT (EQUAL OP 'R)))
                 (CNB (CONS (CAR TAPE)
                            (CONS OP (CDDR TAPE))))),

  which again simplifies, applying CNB-CONS, to:

        T.

Case 1. (IMPLIES (AND (CNB OP)
                      (CNB TAPE)
                      (EQUAL OP 'L))
                 (CNB (CONS (CDAR TAPE)
                            (CONS (CAAR TAPE) (CDR TAPE))))).

  However this again simplifies, applying the lemma CNB-CONS, and opening up
  the function CNB, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CNB-NEW-TAPE


(TOGGLE NEW-TAPE-OFF NEW-TAPE T)

[ 0.0 0.0 0.0 ]

NEW-TAPE-OFF


(DEFN TMIN
      (ST TAPE TM N)
      (IF (ZEROP N)
          (BTM)
          (IF (BTMP (INSTRN ST
                            (CAR (CDR TAPE))
                            TM
                            (SUB1 N)))
              (BTM)
              (IF (INSTRN ST
                          (CAR (CDR TAPE))
                          TM
                          (SUB1 N))
                  (TMIN (CAR (CDR (INSTRN ST
                                          (CAR (CDR TAPE))
                                          TM
                                          (SUB1 N))))
                        (NEW-TAPE (CAR (INSTRN ST
                                               (CAR (CDR TAPE))
                                               TM
                                               (SUB1 N)))
                                  TAPE)
                        TM
                        (SUB1 N))
                  TAPE))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, TMIN is accepted
under the principle of definition.  From the definition we can conclude that:
      (OR (OR (LISTP (TMIN ST TAPE TM N))
              (BTMP (TMIN ST TAPE TM N)))
          (EQUAL (TMIN ST TAPE TM N) TAPE))
is a theorem.




[ 0.0 0.0 0.0 ]

TMIN


(DEFN PR-EVAL-TMI-INDUCTION-SCHEME
 (ST TAPE TM-- VA TM N)
 (IF
  (ZEROP N)
  T
  (PR-EVAL-TMI-INDUCTION-SCHEME '(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                'TM
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                TM
                                (SUB1 N))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, PR-EVAL-TMI-INDUCTION-SCHEME is
accepted under the definitional principle.  Observe that:
      (TRUEP (PR-EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N))
is a theorem.




[ 0.0 0.0 0.0 ]

PR-EVAL-TMI-INDUCTION-SCHEME


(PROVE-LEMMA PR-EVAL-TMI
             (REWRITE)
             (IMPLIES (AND (CNB (EV 'AL ST VA (TMI-FA TM) N))
                           (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                           (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (EQUAL (EV 'AL
                                 (LIST 'TMI ST TAPE TM--)
                                 VA
                                 (TMI-FA TM)
                                 N)
                             (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                                   (EV 'AL TAPE VA (TMI-FA TM) N)
                                   (EV 'AL TM-- VA (TMI-FA TM) N)
                                   N)))
             ((INDUCT (PR-EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N))))

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

Case 2. (IMPLIES (AND (ZEROP N)
                      (CNB (EV 'AL ST VA (TMI-FA TM) N))
                      (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                      (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (EQUAL (EV 'AL
                            (LIST 'TMI ST TAPE TM--)
                            VA
                            (TMI-FA TM)
                            N)
                        (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                              (EV 'AL TAPE VA (TMI-FA TM) N)
                              (EV 'AL TM-- VA (TMI-FA TM) N)
                              N))),

  which simplifies, rewriting with EVLIST-CONS, CNB-NBTM, EVLIST-NIL, and
  PR-EVAL-FN-0, and opening up the definitions of ZEROP, BTMP, UNSOLV-SUBRP,
  EQUAL, and TMIN, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (EQUAL N 0))
          (NUMBERP N)
          (IMPLIES
               (AND (CNB (EV 'AL
                             '(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'TAPE
                                         (EV 'AL TAPE VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N)))
                    (CNB (EV 'AL
                             '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                        TAPE)
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'TAPE
                                         (EV 'AL TAPE VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N)))
                    (CNB (EV 'AL
                             'TM
                             (LIST (CONS 'ST
                                         (EV 'AL ST VA (TMI-FA TM) N))
                                   (CONS 'TAPE
                                         (EV 'AL TAPE VA (TMI-FA TM) N))
                                   (CONS 'TM
                                         (EV 'AL TM-- VA (TMI-FA TM) N)))
                             (TMI-FA TM)
                             (SUB1 N))))
               (EQUAL (EV 'AL
                          '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                          TAPE)
                                TM)
                          (LIST (CONS 'ST
                                      (EV 'AL ST VA (TMI-FA TM) N))
                                (CONS 'TAPE
                                      (EV 'AL TAPE VA (TMI-FA TM) N))
                                (CONS 'TM
                                      (EV 'AL TM-- VA (TMI-FA TM) N)))
                          (TMI-FA TM)
                          (SUB1 N))
                      (TMIN (EV 'AL
                                '(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (EV 'AL
                                'TM
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (SUB1 N))))
          (CNB (EV 'AL ST VA (TMI-FA TM) N))
          (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
          (CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
         (EQUAL (EV 'AL
                    (LIST 'TMI ST TAPE TM--)
                    VA
                    (TMI-FA TM)
                    N)
                (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                      (EV 'AL TAPE VA (TMI-FA TM) N)
                      (EV 'AL TM-- VA (TMI-FA TM) N)
                      N))).

  This simplifies, applying PR-EVAL-UNSOLV-SUBRP, EVLIST-NIL, CNB-NBTM,
  EVLIST-CONS, CNB-CONS, PR-EVAL-NLISTP, CAR-CONS, CDR-CONS, PR-EVAL-INSTR,
  GET-TMI-FA, PR-EVAL-IF, and PR-EVAL-FN-1, and expanding UNSOLV-APPLY-SUBR,
  BTMP, GET, EQUAL, PACK, UNSOLV-SUBRP, AND, IMPLIES, TMI-DEFN, CDR, CAR,
  LISTP, PAIRLIST, and TMIN, to 13 new conjectures:

  Case 1.13.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (NOT (CNB (BTM)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                  (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                  (EV 'AL TM-- VA (TMI-FA TM) N)
                                  (SUB1 N))))
               (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                       (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                       (EV 'AL TM-- VA (TMI-FA TM) N)
                       (SUB1 N)))
           (EQUAL (EV 'AL
                      '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                            (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                      TAPE)
                            TM)
                      (LIST (CONS 'ST
                                  (EV 'AL ST VA (TMI-FA TM) N))
                            (CONS 'TAPE
                                  (EV 'AL TAPE VA (TMI-FA TM) N))
                            (CONS 'TM
                                  (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (TMI-FA TM)
                      (SUB1 N))
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

    which again simplifies, rewriting with CAR-CONS, CNB-CONS, CNB-INSTRN, and
    CNB-NBTM, to:

          T.

  Case 1.12.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (NOT (CNB (BTM)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                  (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                  (EV 'AL TM-- VA (TMI-FA TM) N)
                                  (SUB1 N))))
               (NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                            (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                            (EV 'AL TM-- VA (TMI-FA TM) N)
                            (SUB1 N))))
           (EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))).

    However this again simplifies, opening up CONS, CAR, CDR, and BTMP, to:

          T.

  Case 1.11.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (NOT (CNB (BTM)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                             (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                             (EV 'AL TM-- VA (TMI-FA TM) N)
                             (SUB1 N))))
           (EQUAL (BTM)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

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

          T.

  Case 1.10.
          (IMPLIES
           (AND
            (NOT (EQUAL N 0))
            (NUMBERP N)
            (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N))))
            (NOT
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
            (NOT
             (CNB
              (CAAR
               (LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))))
            (CNB (EV 'AL ST VA (TMI-FA TM) N))
            (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
            (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
            (NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                         (EV 'AL TM-- VA (TMI-FA TM) N)
                         (SUB1 N))))
           (EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))).

    This again simplifies, unfolding the definitions of BTMP, CONS, CAR, CDR,
    and CNB, to:

          T.

  Case 1.9.
          (IMPLIES
           (AND
            (NOT (EQUAL N 0))
            (NUMBERP N)
            (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N))))
            (NOT
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
            (NOT
             (CNB
              (CAAR
               (LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))))
            (CNB (EV 'AL ST VA (TMI-FA TM) N))
            (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
            (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
            (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                    (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                    (EV 'AL TM-- VA (TMI-FA TM) N)
                    (SUB1 N)))
           (EQUAL (EV 'AL
                      '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                            (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                      TAPE)
                            TM)
                      (LIST (CONS 'ST
                                  (EV 'AL ST VA (TMI-FA TM) N))
                            (CONS 'TAPE
                                  (EV 'AL TAPE VA (TMI-FA TM) N))
                            (CONS 'TM
                                  (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (TMI-FA TM)
                      (SUB1 N))
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

    which again simplifies, applying CAR-CONS, CNB-CONS, CNB-INSTRN, and
    CNB-NBTM, to:

          T.

  Case 1.8.
          (IMPLIES
             (AND (NOT (EQUAL N 0))
                  (NUMBERP N)
                  (NOT (CNB (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))))
                  (CNB (EV 'AL ST VA (TMI-FA TM) N))
                  (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                  (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                  (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                     (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                     (EV 'AL TM-- VA (TMI-FA TM) N)
                                     (SUB1 N))))
                  (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                          (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                          (EV 'AL TM-- VA (TMI-FA TM) N)
                          (SUB1 N)))
             (EQUAL (EV 'AL
                        '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                              (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                        TAPE)
                              TM)
                        (LIST (CONS 'ST
                                    (EV 'AL ST VA (TMI-FA TM) N))
                              (CONS 'TAPE
                                    (EV 'AL TAPE VA (TMI-FA TM) N))
                              (CONS 'TM
                                    (EV 'AL TM-- VA (TMI-FA TM) N)))
                        (TMI-FA TM)
                        (SUB1 N))
                    (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                          (EV 'AL TAPE VA (TMI-FA TM) N)
                          (EV 'AL TM-- VA (TMI-FA TM) N)
                          N))).

    This again simplifies, rewriting with CNB-INSTRN, PR-EVAL-INSTR, CDR-CONS,
    CAR-CONS, PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
    PR-EVAL-UNSOLV-SUBRP, PR-EVAL-NEW-TAPE, GET-TMI-FA, PR-EVAL-IF, and
    PR-EVAL-FN-1, and opening up the functions UNSOLV-SUBRP, PACK, EQUAL, GET,
    BTMP, UNSOLV-APPLY-SUBR, TMI-DEFN, CDR, CAR, LISTP, PAIRLIST, and INSTRN,
    to the following three new goals:

    Case 1.8.3.
            (IMPLIES
             (AND
              (NOT (EQUAL N 0))
              (NUMBERP N)
              (NOT (EQUAL (SUB1 N) 0))
              (NOT
               (CNB
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N))))
              (CNB (EV 'AL ST VA (TMI-FA TM) N))
              (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
              (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
              (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 (SUB1 N))))
              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                      (EV 'AL TM-- VA (TMI-FA TM) N)
                      (SUB1 N))
              (NOT
               (BTMP
                (EV 'AL
                 '(INSTR ST (CAR (CDR TAPE)) TM)
                 (LIST
                  (CONS 'ST
                        (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (EV 'AL TM-- VA (TMI-FA TM) N)
                                      (SUB1 N))))
                  (CONS 'TAPE
                   (NEW-TAPE
                            (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                  (CONS 'TM
                        (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (TMI-FA TM)
                 (SUB1 (SUB1 N)))))
              (EV 'AL
               '(INSTR ST (CAR (CDR TAPE)) TM)
               (LIST
                (CONS 'ST
                      (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                    (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                    (EV 'AL TM-- VA (TMI-FA TM) N)
                                    (SUB1 N))))
                (CONS 'TAPE
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                (CONS 'TM
                      (EV 'AL TM-- VA (TMI-FA TM) N)))
               (TMI-FA TM)
               (SUB1 (SUB1 N))))
             (EQUAL
              (EV 'AL
               '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                     (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                               TAPE)
                     TM)
               (LIST
                (CONS 'ST
                      (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                    (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                    (EV 'AL TM-- VA (TMI-FA TM) N)
                                    (SUB1 N))))
                (CONS 'TAPE
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                (CONS 'TM
                      (EV 'AL TM-- VA (TMI-FA TM) N)))
               (TMI-FA TM)
               (SUB1 (SUB1 N)))
              (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                    (EV 'AL TAPE VA (TMI-FA TM) N)
                    (EV 'AL TM-- VA (TMI-FA TM) N)
                    N))).

      But this again simplifies, applying the lemmas CNB-CONS, CNB-INSTRN, and
      CNB-NEW-TAPE, to:

            T.

    Case 1.8.2.
            (IMPLIES
             (AND
              (NOT (EQUAL N 0))
              (NUMBERP N)
              (NOT (EQUAL (SUB1 N) 0))
              (NOT
               (CNB
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N))))
              (CNB (EV 'AL ST VA (TMI-FA TM) N))
              (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
              (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
              (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 (SUB1 N))))
              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                      (EV 'AL TM-- VA (TMI-FA TM) N)
                      (SUB1 N))
              (NOT
               (BTMP
                (EV 'AL
                 '(INSTR ST (CAR (CDR TAPE)) TM)
                 (LIST
                  (CONS 'ST
                        (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (EV 'AL TM-- VA (TMI-FA TM) N)
                                      (SUB1 N))))
                  (CONS 'TAPE
                   (NEW-TAPE
                            (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                  (CONS 'TM
                        (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (TMI-FA TM)
                 (SUB1 (SUB1 N)))))
              (NOT
               (EV 'AL
                '(INSTR ST (CAR (CDR TAPE)) TM)
                (LIST
                 (CONS 'ST
                       (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                     (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                     (EV 'AL TM-- VA (TMI-FA TM) N)
                                     (SUB1 N))))
                 (CONS 'TAPE
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                 (CONS 'TM
                       (EV 'AL TM-- VA (TMI-FA TM) N)))
                (TMI-FA TM)
                (SUB1 (SUB1 N)))))
             (EQUAL
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N))
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

      which again simplifies, applying CNB-CONS, CNB-INSTRN, and CNB-NEW-TAPE,
      to:

            T.

    Case 1.8.1.
            (IMPLIES
             (AND
              (NOT (EQUAL N 0))
              (NUMBERP N)
              (NOT (EQUAL (SUB1 N) 0))
              (NOT
               (CNB
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N))))
              (CNB (EV 'AL ST VA (TMI-FA TM) N))
              (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
              (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
              (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 (SUB1 N))))
              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                      (EV 'AL TM-- VA (TMI-FA TM) N)
                      (SUB1 N))
              (BTMP
               (EV 'AL
                '(INSTR ST (CAR (CDR TAPE)) TM)
                (LIST
                 (CONS 'ST
                       (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                     (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                     (EV 'AL TM-- VA (TMI-FA TM) N)
                                     (SUB1 N))))
                 (CONS 'TAPE
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                 (CONS 'TM
                       (EV 'AL TM-- VA (TMI-FA TM) N)))
                (TMI-FA TM)
                (SUB1 (SUB1 N)))))
             (EQUAL (BTM)
                    (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                          (EV 'AL TAPE VA (TMI-FA TM) N)
                          (EV 'AL TM-- VA (TMI-FA TM) N)
                          N))).

      But this again simplifies, applying CNB-CONS, CNB-INSTRN, and
      CNB-NEW-TAPE, to:

            T.

  Case 1.7.
          (IMPLIES
             (AND (NOT (EQUAL N 0))
                  (NUMBERP N)
                  (NOT (CNB (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))))
                  (CNB (EV 'AL ST VA (TMI-FA TM) N))
                  (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                  (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                  (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                     (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                     (EV 'AL TM-- VA (TMI-FA TM) N)
                                     (SUB1 N))))
                  (NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N))))
             (EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
                    (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                          (EV 'AL TAPE VA (TMI-FA TM) N)
                          (EV 'AL TM-- VA (TMI-FA TM) N)
                          N))).

    But this again simplifies, applying the lemmas PR-EVAL-INSTR, CDR-CONS,
    CAR-CONS, PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
    PR-EVAL-UNSOLV-SUBRP, and PR-EVAL-NEW-TAPE, and unfolding the functions
    CNB, UNSOLV-SUBRP, PACK, EQUAL, GET, BTMP, UNSOLV-APPLY-SUBR, CONS, TMIN,
    and INSTRN, to:

          T.

  Case 1.6.
          (IMPLIES
             (AND (NOT (EQUAL N 0))
                  (NUMBERP N)
                  (NOT (CNB (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))))
                  (CNB (EV 'AL ST VA (TMI-FA TM) N))
                  (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
                  (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
                  (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                (EV 'AL TM-- VA (TMI-FA TM) N)
                                (SUB1 N))))
             (EQUAL (BTM)
                    (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                          (EV 'AL TAPE VA (TMI-FA TM) N)
                          (EV 'AL TM-- VA (TMI-FA TM) N)
                          N))),

    which again simplifies, unfolding TMIN and EQUAL, to:

          T.

  Case 1.5.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (EQUAL (EV 'AL
                          '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                          TAPE)
                                TM)
                          (LIST (CONS 'ST
                                      (EV 'AL ST VA (TMI-FA TM) N))
                                (CONS 'TAPE
                                      (EV 'AL TAPE VA (TMI-FA TM) N))
                                (CONS 'TM
                                      (EV 'AL TM-- VA (TMI-FA TM) N)))
                          (TMI-FA TM)
                          (SUB1 N))
                      (TMIN (BTM)
                            (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (EV 'AL TM-- VA (TMI-FA TM) N)
                            (SUB1 N)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                  (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                  (EV 'AL TM-- VA (TMI-FA TM) N)
                                  (SUB1 N))))
               (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                       (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                       (EV 'AL TM-- VA (TMI-FA TM) N)
                       (SUB1 N)))
           (EQUAL (EV 'AL
                      '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                            (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                      TAPE)
                            TM)
                      (LIST (CONS 'ST
                                  (EV 'AL ST VA (TMI-FA TM) N))
                            (CONS 'TAPE
                                  (EV 'AL TAPE VA (TMI-FA TM) N))
                            (CONS 'TM
                                  (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (TMI-FA TM)
                      (SUB1 N))
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

    which again simplifies, applying the lemmas CAR-CONS, CNB-CONS, CNB-INSTRN,
    and CNB-NBTM, to:

          T.

  Case 1.4.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (EQUAL (EV 'AL
                          '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                          TAPE)
                                TM)
                          (LIST (CONS 'ST
                                      (EV 'AL ST VA (TMI-FA TM) N))
                                (CONS 'TAPE
                                      (EV 'AL TAPE VA (TMI-FA TM) N))
                                (CONS 'TM
                                      (EV 'AL TM-- VA (TMI-FA TM) N)))
                          (TMI-FA TM)
                          (SUB1 N))
                      (TMIN (BTM)
                            (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (EV 'AL TM-- VA (TMI-FA TM) N)
                            (SUB1 N)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                  (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                  (EV 'AL TM-- VA (TMI-FA TM) N)
                                  (SUB1 N))))
               (NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                            (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                            (EV 'AL TM-- VA (TMI-FA TM) N)
                            (SUB1 N))))
           (EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

    which again simplifies, opening up the functions CONS, CAR, CDR, and BTMP,
    to:

          T.

  Case 1.3.
          (IMPLIES
           (AND
               (NOT (EQUAL N 0))
               (NUMBERP N)
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))))
               (EQUAL (EV 'AL
                          '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                                (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                          TAPE)
                                TM)
                          (LIST (CONS 'ST
                                      (EV 'AL ST VA (TMI-FA TM) N))
                                (CONS 'TAPE
                                      (EV 'AL TAPE VA (TMI-FA TM) N))
                                (CONS 'TM
                                      (EV 'AL TM-- VA (TMI-FA TM) N)))
                          (TMI-FA TM)
                          (SUB1 N))
                      (TMIN (BTM)
                            (EV 'AL
                                '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                           TAPE)
                                (LIST (CONS 'ST
                                            (EV 'AL ST VA (TMI-FA TM) N))
                                      (CONS 'TAPE
                                            (EV 'AL TAPE VA (TMI-FA TM) N))
                                      (CONS 'TM
                                            (EV 'AL TM-- VA (TMI-FA TM) N)))
                                (TMI-FA TM)
                                (SUB1 N))
                            (EV 'AL TM-- VA (TMI-FA TM) N)
                            (SUB1 N)))
               (CNB (EV 'AL ST VA (TMI-FA TM) N))
               (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
               (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
               (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                             (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                             (EV 'AL TM-- VA (TMI-FA TM) N)
                             (SUB1 N))))
           (EQUAL (BTM)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))),

    which again simplifies, rewriting with CAR-CONS and CDR-NLISTP, and
    opening up BTMP, to:

          T.

  Case 1.2.
          (IMPLIES
           (AND
            (NOT (EQUAL N 0))
            (NUMBERP N)
            (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N))))
            (NOT
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
            (EQUAL
             (EV 'AL
                 '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                       (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                 TAPE)
                       TM)
                 (LIST (CONS 'ST
                             (EV 'AL ST VA (TMI-FA TM) N))
                       (CONS 'TAPE
                             (EV 'AL TAPE VA (TMI-FA TM) N))
                       (CONS 'TM
                             (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (TMI-FA TM)
                 (SUB1 N))
             (TMIN
              (CAAR
               (LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
              (EV 'AL
                  '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                             TAPE)
                  (LIST (CONS 'ST
                              (EV 'AL ST VA (TMI-FA TM) N))
                        (CONS 'TAPE
                              (EV 'AL TAPE VA (TMI-FA TM) N))
                        (CONS 'TM
                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                  (TMI-FA TM)
                  (SUB1 N))
              (EV 'AL TM-- VA (TMI-FA TM) N)
              (SUB1 N)))
            (CNB (EV 'AL ST VA (TMI-FA TM) N))
            (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
            (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
            (NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                         (EV 'AL TM-- VA (TMI-FA TM) N)
                         (SUB1 N))))
           (EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))).

    However this again simplifies, applying PR-EVAL-INSTR, CDR-CONS, CAR-CONS,
    PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
    PR-EVAL-UNSOLV-SUBRP, and PR-EVAL-NEW-TAPE, and expanding the functions
    BTMP, CONS, CAR, CDR, CNB, UNSOLV-SUBRP, PACK, EQUAL, GET,
    UNSOLV-APPLY-SUBR, TMIN, and INSTRN, to:

          T.

  Case 1.1.
          (IMPLIES
           (AND
            (NOT (EQUAL N 0))
            (NUMBERP N)
            (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N))))
            (NOT
               (BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
            (EQUAL
             (EV 'AL
                 '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                       (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                 TAPE)
                       TM)
                 (LIST (CONS 'ST
                             (EV 'AL ST VA (TMI-FA TM) N))
                       (CONS 'TAPE
                             (EV 'AL TAPE VA (TMI-FA TM) N))
                       (CONS 'TM
                             (EV 'AL TM-- VA (TMI-FA TM) N)))
                 (TMI-FA TM)
                 (SUB1 N))
             (TMIN
              (CAAR
               (LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N))))))
              (EV 'AL
                  '(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                             TAPE)
                  (LIST (CONS 'ST
                              (EV 'AL ST VA (TMI-FA TM) N))
                        (CONS 'TAPE
                              (EV 'AL TAPE VA (TMI-FA TM) N))
                        (CONS 'TM
                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                  (TMI-FA TM)
                  (SUB1 N))
              (EV 'AL TM-- VA (TMI-FA TM) N)
              (SUB1 N)))
            (CNB (EV 'AL ST VA (TMI-FA TM) N))
            (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
            (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
            (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                    (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                    (EV 'AL TM-- VA (TMI-FA TM) N)
                    (SUB1 N)))
           (EQUAL (EV 'AL
                      '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                            (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                      TAPE)
                            TM)
                      (LIST (CONS 'ST
                                  (EV 'AL ST VA (TMI-FA TM) N))
                            (CONS 'TAPE
                                  (EV 'AL TAPE VA (TMI-FA TM) N))
                            (CONS 'TM
                                  (EV 'AL TM-- VA (TMI-FA TM) N)))
                      (TMI-FA TM)
                      (SUB1 N))
                  (TMIN (EV 'AL ST VA (TMI-FA TM) N)
                        (EV 'AL TAPE VA (TMI-FA TM) N)
                        (EV 'AL TM-- VA (TMI-FA TM) N)
                        N))).

    This again simplifies, rewriting with the lemmas CAR-CONS, CNB-CONS,
    CNB-INSTRN, CNB-NBTM, PR-EVAL-INSTR, CDR-CONS, PR-EVAL-NLISTP, EVLIST-CONS,
    EVLIST-NIL, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-NEW-TAPE, GET-TMI-FA,
    CNB-NEW-TAPE, PR-EVAL-IF, PR-EVAL-FN-1, and PR-EVAL-FN-0, and opening up
    UNSOLV-SUBRP, PACK, EQUAL, GET, BTMP, UNSOLV-APPLY-SUBR, TMI-DEFN, CDR,
    CAR, LISTP, PAIRLIST, TMIN, INSTRN, and ZEROP, to three new conjectures:

    Case 1.1.3.
            (IMPLIES
             (AND
              (NOT (EQUAL N 0))
              (NUMBERP N)
              (NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                 (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                 (EV 'AL TM-- VA (TMI-FA TM) N)
                                 (SUB1 N))))
              (NOT (EQUAL (SUB1 N) 0))
              (EQUAL
               (EV 'AL
                   '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                         (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                   TAPE)
                         TM)
                   (LIST (CONS 'ST
                               (EV 'AL ST VA (TMI-FA TM) N))
                         (CONS 'TAPE
                               (EV 'AL TAPE VA (TMI-FA TM) N))
                         (CONS 'TM
                               (EV 'AL TM-- VA (TMI-FA TM) N)))
                   (TMI-FA TM)
                   (SUB1 N))
               (TMIN
                  (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                (EV 'AL TM-- VA (TMI-FA TM) N)
                                (SUB1 N)))
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N))
                  (EV 'AL TM-- VA (TMI-FA TM) N)
                  (SUB1 N)))
              (CNB (EV 'AL ST VA (TMI-FA TM) N))
              (CNB (EV 'AL TAPE VA (TMI-FA TM) N))
              (CNB (EV 'AL TM-- VA (TMI-FA TM) N))
              (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                      (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                      (EV 'AL TM-- VA (TMI-FA TM) N)
                      (SUB1 N))
              (NOT
               (BTMP
                (INSTRN
                 (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                               (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                               (EV 'AL TM-- VA (TMI-FA TM) N)
                               (SUB1 N)))
                 (CADR
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                 (EV 'AL TM-- VA (TMI-FA TM) N)
                 (SUB1 (SUB1 N)))))
              (INSTRN
               (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                             (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                             (EV 'AL TM-- VA (TMI-FA TM) N)
                             (SUB1 N)))
               (CADR
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
               (EV 'AL TM-- VA (TMI-FA TM) N)
               (SUB1 (SUB1 N))))
             (EQUAL
              (EV 'AL
               '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                     (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                               TAPE)
                     TM)
               (LIST
                (CONS 'ST
                      (CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                    (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                    (EV 'AL TM-- VA (TMI-FA TM) N)
                                    (SUB1 N))))
                (CONS 'TAPE
                  (NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
                                         (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
                                         (EV 'AL TM-- VA (TMI-FA TM) N)
                                         (SUB1 N)))
                            (EV 'AL TAPE VA (TMI-FA TM) N)))
                (CONS 'TM
                      (EV 'AL TM-- VA (TMI-FA TM) N)))
               (TMI-FA TM)
               (SUB1 (SUB1 N)))
              (EV 'AL
                  '(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
                        (NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
                                  TAPE)
                        TM)
                  (LIST (CONS 'ST
                              (EV 'AL ST VA (TMI-FA TM) N))
                        (CONS 'TAPE
                              (EV 'AL TAPE VA (TMI-FA TM) N))
                        (CONS 'TM
                              (EV 'AL TM-- VA (TMI-FA TM) N)))
                  (TMI-FA TM)
                  (SUB1 N)))),

      which again simplifies, rewriting with the lemmas CNB-INSTRN,
      PR-EVAL-UNSOLV-SUBR