(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(ADD-SHELL ST NIL STP
           ((PC (NONE-OF) ZERO)
            (STK (NONE-OF) ZERO)
            (MEM (NONE-OF) ZERO)
            (HALTEDP (NONE-OF) ZERO)
            (DEFS (NONE-OF) ZERO)))

[ 0.0 0.0 0.0 ]

ST


(DEFN ADD1-PC
      (PC)
      (CONS (CAR PC) (ADD1 (CDR PC))))

     From the definition we can conclude that (LISTP (ADD1-PC PC)) is a
theorem.




[ 0.0 0.0 0.0 ]

ADD1-PC


(DEFN GET
      (N LST)
      (IF (ZEROP N)
          (CAR LST)
          (GET (SUB1 N) (CDR LST))))

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




[ 0.0 0.0 0.0 ]

GET


(DEFN PUT
      (N V LST)
      (IF (ZEROP N)
          (CONS V (CDR LST))
          (CONS (CAR LST)
                (PUT (SUB1 N) V (CDR LST)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, PUT is accepted
under the definitional principle.  Observe that (LISTP (PUT N V LST)) is a
theorem.




[ 0.0 0.0 0.0 ]

PUT


(DEFN FETCH
      (PC DEFS)
      (GET (CDR PC)
           (CDR (ASSOC (CAR PC) DEFS))))

   




[ 0.0 0.0 0.0 ]

FETCH


(DEFN MOVE
      (ADDR1 ADDR2 S)
      (ST (ADD1-PC (PC S))
          (STK S)
          (PUT ADDR1
               (GET ADDR2 (MEM S))
               (MEM S))
          F
          (DEFS S)))

     From the definition we can conclude that (STP (MOVE ADDR1 ADDR2 S)) is a
theorem.




[ 0.0 0.0 0.0 ]

MOVE


(DEFN MOVI
      (ADDR VAL S)
      (ST (ADD1-PC (PC S))
          (STK S)
          (PUT ADDR VAL (MEM S))
          F
          (DEFS S)))

     Observe that (STP (MOVI ADDR VAL S)) is a theorem.




[ 0.0 0.0 0.0 ]

MOVI


(DEFN ADD
      (ADDR1 ADDR2 S)
      (ST (ADD1-PC (PC S))
          (STK S)
          (PUT ADDR1
               (PLUS (GET ADDR1 (MEM S))
                     (GET ADDR2 (MEM S)))
               (MEM S))
          F
          (DEFS S)))

     From the definition we can conclude that (STP (ADD ADDR1 ADDR2 S)) is a
theorem.




[ 0.0 0.0 0.0 ]

ADD


(DEFN SUBI
      (ADDR VAL S)
      (ST (ADD1-PC (PC S))
          (STK S)
          (PUT ADDR
               (DIFFERENCE (GET ADDR (MEM S)) VAL)
               (MEM S))
          F
          (DEFS S)))

     Observe that (STP (SUBI ADDR VAL S)) is a theorem.




[ 0.0 0.0 0.0 ]

SUBI


(DEFN JUMPZ
      (ADDR PC S)
      (ST (IF (ZEROP (GET ADDR (MEM S)))
              (CONS (CAR (PC S)) PC)
              (ADD1-PC (PC S)))
          (STK S)
          (MEM S)
          F
          (DEFS S)))

     Observe that (STP (JUMPZ ADDR PC S)) is a theorem.




[ 0.0 0.0 0.0 ]

JUMPZ


(DEFN JUMP
      (PC S)
      (ST (CONS (CAR (PC S)) PC)
          (STK S)
          (MEM S)
          F
          (DEFS S)))

     Note that (STP (JUMP PC S)) is a theorem.




[ 0.0 0.0 0.0 ]

JUMP


(DEFN CALL
      (SUBR S)
      (ST (CONS SUBR 0)
          (CONS (ADD1-PC (PC S)) (STK S))
          (MEM S)
          F
          (DEFS S)))

     Observe that (STP (CALL SUBR S)) is a theorem.




[ 0.0 0.0 0.0 ]

CALL


(DEFN RET
      (S)
      (IF (NLISTP (STK S))
          (ST (PC S) (STK S) (MEM S) T (DEFS S))
          (ST (CAR (STK S))
              (CDR (STK S))
              (MEM S)
              F
              (DEFS S))))

     Observe that (STP (RET S)) is a theorem.




[ 0.0 0.0 0.0 ]

RET


(DEFN EXECUTE
      (INS S)
      (IF (EQUAL (CAR INS) 'MOVE)
          (MOVE (CADR INS) (CADDR INS) S)
          (IF (EQUAL (CAR INS) 'MOVI)
              (MOVI (CADR INS) (CADDR INS) S)
              (IF (EQUAL (CAR INS) 'ADD)
                  (ADD (CADR INS) (CADDR INS) S)
                  (IF (EQUAL (CAR INS) 'SUBI)
                      (SUBI (CADR INS) (CADDR INS) S)
                      (IF (EQUAL (CAR INS) 'JUMPZ)
                          (JUMPZ (CADR INS) (CADDR INS) S)
                          (IF (EQUAL (CAR INS) 'JUMP)
                              (JUMP (CADR INS) S)
                              (IF (EQUAL (CAR INS) 'CALL)
                                  (CALL (CADR INS) S)
                                  (IF (EQUAL (CAR INS) 'RET)
                                      (RET S)
                                      S)))))))))

     Note that (OR (STP (EXECUTE INS S)) (EQUAL (EXECUTE INS S) S)) is a
theorem.




[ 0.0 0.0 0.0 ]

EXECUTE


(DEFN STEP
      (S)
      (IF (HALTEDP S)
          S
          (EXECUTE (FETCH (PC S) (DEFS S)) S)))

     Observe that (OR (STP (STEP S)) (EQUAL (STEP S) S)) is a theorem.




[ 0.0 0.0 0.0 ]

STEP


(DEFN SM
      (S N)
      (IF (ZEROP N)
          S
          (SM (STEP S) (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, SM is accepted under the
principle of definition.  From the definition we can conclude that:
      (OR (STP (SM S N)) (EQUAL (SM S N) S))
is a theorem.




[ 0.0 0.0 0.0 ]

SM


(PROVE-LEMMA STEP-OPENER
             (REWRITE)
             (AND (IMPLIES (HALTEDP S)
                           (EQUAL (STEP S) S))
                  (IMPLIES (LISTP (FETCH (PC S) (DEFS S)))
                           (EQUAL (STEP S)
                                  (IF (HALTEDP S)
                                      S
                                      (EXECUTE (FETCH (PC S) (DEFS S))
                                               S)))))
             ((DISABLE EXECUTE)))

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


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


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


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

Case 2. (IMPLIES (HALTEDP S)
                 (EQUAL (STEP S) S)),

  which simplifies, opening up the function STEP, to:

        T.

Case 1. (IMPLIES (LISTP (FETCH (PC S) (DEFS S)))
                 (EQUAL (STEP S)
                        (IF (HALTEDP S)
                            S
                            (EXECUTE (FETCH (PC S) (DEFS S))
                                     S)))),

  which simplifies, expanding FETCH and STEP, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

STEP-OPENER


(DISABLE STEP)

[ 0.0 0.0 0.0 ]

STEP-OFF


(PROVE-LEMMA SM-PLUS
             (REWRITE)
             (EQUAL (SM S (PLUS I J))
                    (SM (SM S I) J)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Three inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP I) (p S I J))
           (IMPLIES (AND (NOT (ZEROP I))
                         (p (STEP S) (SUB1 I) J))
                    (p S I J))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP can be used to prove that the measure (COUNT I) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for S.  The above induction scheme
leads to two new goals:

Case 2. (IMPLIES (ZEROP I)
                 (EQUAL (SM S (PLUS I J))
                        (SM (SM S I) J))),

  which simplifies, opening up the definitions of ZEROP, EQUAL, PLUS, and SM,
  to two new conjectures:

  Case 2.2.
          (IMPLIES (AND (EQUAL I 0) (NOT (NUMBERP J)))
                   (EQUAL (SM S 0) (SM S J))),

    which again simplifies, unfolding the functions EQUAL and SM, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (NUMBERP J)))
                   (EQUAL (SM S 0) (SM S J))),

    which again simplifies, opening up the functions EQUAL and SM, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (SM (STEP S) (PLUS (SUB1 I) J))
                             (SM (SM (STEP S) (SUB1 I)) J)))
                 (EQUAL (SM S (PLUS I J))
                        (SM (SM S I) J))),

  which simplifies, applying the lemma SUB1-ADD1, and opening up ZEROP, PLUS,
  and SM, to:

        T.


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


[ 0.0 0.0 0.0 ]

SM-PLUS


(PROVE-LEMMA SM-ADD1
             (REWRITE)
             (EQUAL (SM S (ADD1 I))
                    (SM (STEP S) I)))

This conjecture simplifies, applying SUB1-ADD1, and unfolding the function SM,
to the formula:

      (IMPLIES (NOT (NUMBERP I))
               (EQUAL (SM (STEP S) 0)
                      (SM (STEP S) I))).

This again simplifies, expanding EQUAL and SM, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SM-ADD1


(PROVE-LEMMA SM-0
             (REWRITE)
             (EQUAL (SM S 0) S))

This conjecture simplifies, unfolding the definitions of EQUAL and SM, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SM-0


(DISABLE SM)

[ 0.0 0.0 0.0 ]

SM-OFF


(DEFN TIMES-PROGRAM NIL
      '(TIMES (MOVI 2 0)
              (JUMPZ 0 5)
              (ADD 2 1)
              (SUBI 0 1)
              (JUMP 1)
              (RET)))

     From the definition we can conclude that (LISTP (TIMES-PROGRAM)) is a
theorem.




[ 0.0 0.0 0.0 ]

TIMES-PROGRAM


(DEFN TIMES-FN
      (I J ANS)
      (IF (ZEROP I)
          ANS
          (TIMES-FN (SUB1 I) J (PLUS ANS J))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT I) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, TIMES-FN is accepted under the
definitional principle.  From the definition we can conclude that:
      (OR (NUMBERP (TIMES-FN I J ANS))
          (EQUAL (TIMES-FN I J ANS) ANS))
is a theorem.




[ 0.0 0.0 0.0 ]

TIMES-FN


(PROVE-LEMMA TIMES-FN-IS-TIMES
             (REWRITE)
             (IMPLIES (NUMBERP ANS)
                      (EQUAL (TIMES-FN I J ANS)
                             (PLUS (TIMES I J) ANS))))


     Call the conjecture *1.


     We will try to prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP I) (p I J ANS))
           (IMPLIES (AND (NOT (ZEROP I))
                         (p (SUB1 I) J (PLUS ANS J)))
                    (p I J ANS))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT I) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  Note, however, the inductive
instance chosen for ANS.  The above induction scheme generates two new goals:

Case 2. (IMPLIES (AND (ZEROP I) (NUMBERP ANS))
                 (EQUAL (TIMES-FN I J ANS)
                        (PLUS (TIMES I J) ANS))),

  which simplifies, opening up the functions ZEROP, EQUAL, TIMES-FN, TIMES,
  and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (TIMES-FN (SUB1 I) J (PLUS ANS J))
                             (PLUS (TIMES (SUB1 I) J) ANS J))
                      (NUMBERP ANS))
                 (EQUAL (TIMES-FN I J ANS)
                        (PLUS (TIMES I J) ANS))),

  which simplifies, expanding ZEROP, TIMES-FN, and TIMES, to the conjecture:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL (TIMES-FN (SUB1 I) J (PLUS ANS J))
                             (PLUS (TIMES (SUB1 I) J) ANS J))
                      (NUMBERP ANS))
                 (EQUAL (TIMES-FN (SUB1 I) J (PLUS ANS J))
                        (PLUS (PLUS J (TIMES (SUB1 I) J))
                              ANS))).

  But this again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-FN-IS-TIMES


(PROVE-LEMMA PLUS-RIGHT-ID
             (REWRITE)
             (EQUAL (PLUS X 0) (FIX X)))

This simplifies, unfolding FIX, to two new formulas:

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

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

        T.

Case 1. (IMPLIES (NUMBERP X)
                 (EQUAL (PLUS X 0) X)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-RIGHT-ID


(DEFN TIMES-CLOCK
      (I)
      (PLUS 2 (TIMES I 4) 2))

     From the definition we can conclude that (NUMBERP (TIMES-CLOCK I)) is a
theorem.




[ 0.0 0.0 0.0 ]

TIMES-CLOCK


(PROVE-LEMMA TIMES-CORRECT-LEMMA
             (REWRITE)
             (IMPLIES (AND (NUMBERP I)
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM)))
                      (EQUAL (SM (ST '(TIMES . 1)
                                     STK1
                                     (LIST I J ANS R3 R4)
                                     F DEFS)
                                 (TIMES I 4))
                             (ST '(TIMES . 1)
                                 STK1
                                 (LIST 0 J (TIMES-FN I J ANS) R3 R4)
                                 F DEFS))))

This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
TIMES-PROGRAM, to:

      (IMPLIES (AND (NUMBERP I)
                    (EQUAL (ASSOC 'TIMES DEFS)
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET))))
               (EQUAL (SM (ST '(TIMES . 1)
                              STK1
                              (LIST I J ANS R3 R4)
                              F DEFS)
                          (TIMES I 4))
                      (ST '(TIMES . 1)
                          STK1
                          (LIST 0 J (TIMES-FN I J ANS) R3 R4)
                          F DEFS))).

This simplifies, applying TIMES-FN-IS-TIMES and PC-ST, and opening up TIMES-FN,
to two new goals:

Case 2. (IMPLIES (AND (NUMBERP I)
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL I 0)))
                 (EQUAL (SM (ST '(TIMES . 1)
                                STK1
                                (LIST I J ANS R3 R4)
                                F DEFS)
                            (TIMES I 4))
                        (ST '(TIMES . 1)
                            STK1
                            (LIST 0 J
                                  (PLUS (TIMES (SUB1 I) J) ANS J)
                                  R3 R4)
                            F DEFS))).

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

        (IMPLIES (AND (NUMBERP X)
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (ADD1 X) 0)))
                 (EQUAL (SM (ST '(TIMES . 1)
                                STK1
                                (LIST (ADD1 X) J ANS R3 R4)
                                F DEFS)
                            (TIMES (ADD1 X) 4))
                        (ST '(TIMES . 1)
                            STK1
                            (LIST 0 J
                                  (PLUS (TIMES X J) ANS J)
                                  R3 R4)
                            F DEFS))),

  which further simplifies, rewriting with SUB1-ADD1, DEFS-ST, PC-ST,
  HALTEDP-ST, MEM-ST, CAR-CONS, STK-ST, STEP-OPENER, CDR-CONS, SM-0, SM-ADD1,
  and SM-PLUS, and opening up the functions TIMES, LISTP, FETCH, CDR, CAR, GET,
  JUMPZ, ADD1-PC, EQUAL, EXECUTE, ADD, SUB1, NUMBERP, PUT, SUBI, DIFFERENCE,
  JUMP, and CONS, to the following two new formulas:

  Case 2.2.
          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (ASSOC 'TIMES DEFS)
                               '(TIMES (MOVI 2 0)
                                       (JUMPZ 0 5)
                                       (ADD 2 1)
                                       (SUBI 0 1)
                                       (JUMP 1)
                                       (RET)))
                        (NOT (EQUAL X 0)))
                   (EQUAL (SM (ST '(TIMES . 1)
                                  STK1
                                  (LIST X J (PLUS ANS J) R3 R4)
                                  F DEFS)
                              (TIMES X 4))
                          (ST '(TIMES . 1)
                              STK1
                              (LIST 0 J
                                    (PLUS (TIMES X J) ANS J)
                                    R3 R4)
                              F DEFS))),

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


     So now let us consider:

(IMPLIES (AND (NUMBERP I)
              (EQUAL (ASSOC 'TIMES DEFS)
                     (TIMES-PROGRAM)))
         (EQUAL (SM (ST '(TIMES . 1)
                        STK1
                        (LIST I J ANS R3 R4)
                        F DEFS)
                    (TIMES I 4))
                (ST '(TIMES . 1)
                    STK1
                    (LIST 0 J (TIMES-FN I J ANS) R3 R4)
                    F DEFS))),

which we named *1 above.  We will appeal to induction.  Three inductions are
suggested by terms in the conjecture.  They merge into two likely candidate
inductions, both of which are unflawed.  So we will choose the one suggested
by the largest number of nonprimitive recursive functions.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP I)
                    (p STK1 I J ANS R3 R4 DEFS))
           (IMPLIES (AND (NOT (ZEROP I))
                         (p STK1
                            (SUB1 I)
                            J
                            (PLUS ANS J)
                            R3 R4 DEFS))
                    (p STK1 I J ANS R3 R4 DEFS))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT I) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  Note, however, the inductive
instance chosen for ANS.  The above induction scheme leads to the following
two new goals:

Case 2. (IMPLIES (AND (ZEROP I)
                      (NUMBERP I)
                      (EQUAL (ASSOC 'TIMES DEFS)
                             (TIMES-PROGRAM)))
                 (EQUAL (SM (ST '(TIMES . 1)
                                STK1
                                (LIST I J ANS R3 R4)
                                F DEFS)
                            (TIMES I 4))
                        (ST '(TIMES . 1)
                            STK1
                            (LIST 0 J (TIMES-FN I J ANS) R3 R4)
                            F DEFS))).

  This simplifies, rewriting with SM-0, and expanding ZEROP, NUMBERP,
  TIMES-PROGRAM, TIMES, EQUAL, and TIMES-FN, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (SM (ST '(TIMES . 1)
                                     STK1
                                     (LIST (SUB1 I) J (PLUS ANS J) R3 R4)
                                     F DEFS)
                                 (TIMES (SUB1 I) 4))
                             (ST '(TIMES . 1)
                                 STK1
                                 (LIST 0 J
                                       (TIMES-FN (SUB1 I) J (PLUS ANS J))
                                       R3 R4)
                                 F DEFS))
                      (NUMBERP I)
                      (EQUAL (ASSOC 'TIMES DEFS)
                             (TIMES-PROGRAM)))
                 (EQUAL (SM (ST '(TIMES . 1)
                                STK1
                                (LIST I J ANS R3 R4)
                                F DEFS)
                            (TIMES I 4))
                        (ST '(TIMES . 1)
                            STK1
                            (LIST 0 J (TIMES-FN I J ANS) R3 R4)
                            F DEFS))),

  which simplifies, rewriting with the lemmas PC-ST, DEFS-ST, HALTEDP-ST,
  MEM-ST, CAR-CONS, STK-ST, STEP-OPENER, CDR-CONS, SM-0, SM-ADD1, and SM-PLUS,
  and expanding the functions ZEROP, TIMES-PROGRAM, TIMES, LISTP, FETCH, CDR,
  CAR, GET, JUMPZ, ADD1-PC, EQUAL, EXECUTE, ADD, SUB1, NUMBERP, PUT, SUBI,
  DIFFERENCE, JUMP, CONS, and TIMES-FN, to:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (EQUAL (SM (ST '(TIMES . 1)
                                     STK1
                                     (LIST (SUB1 I) J (PLUS ANS J) R3 R4)
                                     F DEFS)
                                 (TIMES (SUB1 I) 4))
                             (ST '(TIMES . 1)
                                 STK1
                                 (LIST 0 J
                                       (TIMES-FN (SUB1 I) J (PLUS ANS J))
                                       R3 R4)
                                 F DEFS))
                      (NUMBERP I)
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL (SUB1 I) 0))
                 (EQUAL (SM (ST '(TIMES . 1)
                                STK1
                                (LIST 0 J (PLUS ANS J) R3 R4)
                                F DEFS)
                            (TIMES (SUB1 I) 4))
                        (ST '(TIMES . 1)
                            STK1
                            (LIST 0 J
                                  (TIMES-FN (SUB1 I) J (PLUS ANS J))
                                  R3 R4)
                            F DEFS))).

  This again simplifies, clearly, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-CORRECT-LEMMA


(PROVE-LEMMA TIMES-CORRECT
             (REWRITE)
             (IMPLIES (AND (EQUAL (FETCH PC DEFS) '(CALL TIMES))
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM))
                           (NUMBERP I))
                      (EQUAL (SM (ST PC STK (LIST I J R2 R3 R4) F DEFS)
                                 (TIMES-CLOCK I))
                             (ST (ADD1-PC PC)
                                 STK
                                 (LIST 0 J (TIMES I J) R3 R4)
                                 F DEFS))))

This formula can be simplified, using the abbreviations AND, IMPLIES, SM-0,
SM-ADD1, SM-PLUS, TIMES-CLOCK, and TIMES-PROGRAM, to the new conjecture:

      (IMPLIES (AND (EQUAL (FETCH PC DEFS) '(CALL TIMES))
                    (EQUAL (ASSOC 'TIMES DEFS)
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET)))
                    (NUMBERP I))
               (EQUAL (STEP (STEP (SM (STEP (STEP (ST PC STK
                                                      (LIST I J R2 R3 R4)
                                                      F DEFS)))
                                      (TIMES I 4))))
                      (ST (ADD1-PC PC)
                          STK
                          (LIST 0 J (TIMES I J) R3 R4)
                          F DEFS))),

which simplifies, applying DEFS-ST, PC-ST, HALTEDP-ST, STK-ST, MEM-ST,
STEP-OPENER, CDR-CONS, CAR-CONS, PLUS-RIGHT-ID, TIMES-FN-IS-TIMES, and
TIMES-CORRECT-LEMMA, and expanding the definitions of FETCH, LISTP, CALL, CONS,
ADD1-PC, CDR, EQUAL, CAR, EXECUTE, GET, MOVI, SUB1, NUMBERP, PUT,
TIMES-PROGRAM, JUMPZ, and RET, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-CORRECT


(DISABLE TIMES-CLOCK)

[ 0.0 0.0 0.0 ]

TIMES-CLOCK-OFF


(DEFN EXP
      (I J)
      (IF (ZEROP J)
          1
          (TIMES (EXP I (SUB1 J)) I)))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT J) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, EXP is accepted under the
definitional principle.  From the definition we can conclude that
(NUMBERP (EXP I J)) is a theorem.




[ 0.0 0.0 0.0 ]

EXP


(DEFN EXP-PROGRAM NIL
      '(EXP (MOVE 3 0)
            (MOVE 4 1)
            (MOVI 1 1)
            (JUMPZ 4 9)
            (MOVE 0 3)
            (CALL TIMES)
            (MOVE 1 2)
            (SUBI 4 1)
            (JUMP 3)
            (RET)))

     Observe that (LISTP (EXP-PROGRAM)) is a theorem.




[ 0.0 0.0 0.0 ]

EXP-PROGRAM


(DEFN EXP-FN
      (R0 R1 R2 R3 R4)
      (IF (ZEROP R4)
          R1
          (EXP-FN 0
                  (TIMES R3 R1)
                  (TIMES R3 R1)
                  R3
                  (SUB1 R4))))

WARNING:  R0 and R2 are in the arglist but not in the body of the definition
of EXP-FN.


     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT R4) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, EXP-FN is accepted
under the definitional principle.  Observe that:
      (OR (NUMBERP (EXP-FN R0 R1 R2 R3 R4))
          (EQUAL (EXP-FN R0 R1 R2 R3 R4) R1))
is a theorem.




[ 0.0 0.0 0.0 ]

EXP-FN


(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES (TIMES I J) K)
                    (TIMES I (TIMES J K))))


     Call the conjecture *1.


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

Case 2. (IMPLIES (ZEROP I)
                 (EQUAL (TIMES (TIMES I J) K)
                        (TIMES I J K))),

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

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (TIMES (TIMES (SUB1 I) J) K)
                             (TIMES (SUB1 I) J K)))
                 (EQUAL (TIMES (TIMES I J) K)
                        (TIMES I J K))),

  which simplifies, expanding ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL (TIMES (TIMES (SUB1 I) J) K)
                             (TIMES (SUB1 I) J K)))
                 (EQUAL (TIMES (PLUS J (TIMES (SUB1 I) J)) K)
                        (PLUS (TIMES J K)
                              (TIMES (SUB1 I) J K)))).

  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:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ADD1 X) 0))
                      (EQUAL (TIMES (TIMES X J) K)
                             (TIMES X J K)))
                 (EQUAL (TIMES (PLUS J (TIMES X J)) K)
                        (PLUS (TIMES J K) (TIMES X J K)))).

  This further simplifies, trivially, to:

        (IMPLIES (AND (NUMBERP X)
                      (EQUAL (TIMES (TIMES X J) K)
                             (TIMES X J K)))
                 (EQUAL (TIMES (PLUS J (TIMES X J)) K)
                        (PLUS (TIMES J K) (TIMES X J K)))).

  We use the above equality hypothesis by substituting (TIMES (TIMES X J) K)
  for (TIMES X J K) and throwing away the equality.  This generates the goal:

        (IMPLIES (NUMBERP X)
                 (EQUAL (TIMES (PLUS J (TIMES X J)) K)
                        (PLUS (TIMES J K)
                              (TIMES (TIMES X J) K)))).

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

        (IMPLIES (AND (NUMBERP Y) (NUMBERP X))
                 (EQUAL (TIMES (PLUS J Y) K)
                        (PLUS (TIMES J K) (TIMES Y K)))),

  which has an irrelevant term in it.  By eliminating the term we get:

        (IMPLIES (NUMBERP Y)
                 (EQUAL (TIMES (PLUS J Y) K)
                        (PLUS (TIMES J K) (TIMES Y K)))),

  which we will finally name *1.1.


     Perhaps we can prove it by induction.  Three inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP J) (p J Y K))
           (IMPLIES (AND (NOT (ZEROP J)) (p (SUB1 J) Y K))
                    (p J Y K))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP establish that the measure (COUNT J) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme leads to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP J) (NUMBERP Y))
                 (EQUAL (TIMES (PLUS J Y) K)
                        (PLUS (TIMES J K) (TIMES Y K)))).

  This simplifies, unfolding ZEROP, EQUAL, PLUS, and TIMES, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP J))
                      (EQUAL (TIMES (PLUS (SUB1 J) Y) K)
                             (PLUS (TIMES (SUB1 J) K) (TIMES Y K)))
                      (NUMBERP Y))
                 (EQUAL (TIMES (PLUS J Y) K)
                        (PLUS (TIMES J K) (TIMES Y K)))).

  This simplifies, applying SUB1-ADD1, and opening up the functions ZEROP,
  PLUS, and TIMES, to the formula:

        (IMPLIES (AND (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (EQUAL (TIMES (PLUS (SUB1 J) Y) K)
                             (PLUS (TIMES (SUB1 J) K) (TIMES Y K)))
                      (NUMBERP Y))
                 (EQUAL (PLUS K (TIMES (PLUS (SUB1 J) Y) K))
                        (PLUS (PLUS K (TIMES (SUB1 J) K))
                              (TIMES Y K)))).

  This again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.1, which finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOCIATIVITY-OF-TIMES


(PROVE-LEMMA TIMES-RIGHT-ID
             (REWRITE)
             (EQUAL (TIMES I 1) (FIX I)))

This simplifies, unfolding FIX, to two new formulas:

Case 2. (IMPLIES (NOT (NUMBERP I))
                 (EQUAL (TIMES I 1) 0)),

  which again simplifies, unfolding TIMES and EQUAL, to:

        T.

Case 1. (IMPLIES (NUMBERP I)
                 (EQUAL (TIMES I 1) I)),

  which we will name *1.


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

Case 2. (IMPLIES (AND (ZEROP I) (NUMBERP I))
                 (EQUAL (TIMES I 1) I)).

  This simplifies, opening up the definitions of ZEROP, NUMBERP, TIMES, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (TIMES (SUB1 I) 1) (SUB1 I))
                      (NUMBERP I))
                 (EQUAL (TIMES I 1) I)).

  This simplifies, expanding the definitions of ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (EQUAL (TIMES (SUB1 I) 1) (SUB1 I))
                      (NUMBERP I))
                 (EQUAL (PLUS 1 (SUB1 I)) I)),

  which again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-RIGHT-ID


(PROVE-LEMMA EXP-FN-IS-EXP
             (REWRITE)
             (IMPLIES (NUMBERP R1)
                      (EQUAL (EXP-FN R0 R1 R2 R3 R4)
                             (TIMES (EXP R3 R4) R1))))


     Give the conjecture the name *1.


     Let us appeal to the induction principle.  The recursive terms in the
conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP R4)
                    (p R0 R1 R2 R3 R4))
           (IMPLIES (AND (NOT (ZEROP R4))
                         (p 0
                            (TIMES R3 R1)
                            (TIMES R3 R1)
                            R3
                            (SUB1 R4)))
                    (p R0 R1 R2 R3 R4))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT R4) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for R0, R1, and R2.  The above
induction scheme generates the following two new conjectures:

Case 2. (IMPLIES (AND (ZEROP R4) (NUMBERP R1))
                 (EQUAL (EXP-FN R0 R1 R2 R3 R4)
                        (TIMES (EXP R3 R4) R1))).

  This simplifies, opening up the functions ZEROP, EQUAL, EXP-FN, and EXP, to
  the following two new goals:

  Case 2.2.
          (IMPLIES (AND (EQUAL R4 0) (NUMBERP R1))
                   (EQUAL R1 (TIMES 1 R1))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP R4)) (NUMBERP R1))
                   (EQUAL R1 (TIMES 1 R1))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP R4))
                      (EQUAL (EXP-FN 0
                                     (TIMES R3 R1)
                                     (TIMES R3 R1)
                                     R3
                                     (SUB1 R4))
                             (TIMES (EXP R3 (SUB1 R4)) R3 R1))
                      (NUMBERP R1))
                 (EQUAL (EXP-FN R0 R1 R2 R3 R4)
                        (TIMES (EXP R3 R4) R1))),

  which simplifies, applying ASSOCIATIVITY-OF-TIMES, and opening up ZEROP,
  EXP-FN, and EXP, to:

        T.


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


[ 0.0 0.0 0.0 ]

EXP-FN-IS-EXP


(DEFN EXP-CLOCK
      (I J)
      (PLUS 4
            (TIMES J (PLUS 2 (TIMES-CLOCK I) 3))
            2))

     From the definition we can conclude that (NUMBERP (EXP-CLOCK I J)) is a
theorem.




[ 0.0 0.0 0.0 ]

EXP-CLOCK


(PROVE-LEMMA EXP-CORRECT-LEMMA
             (REWRITE)
             (IMPLIES (AND (NUMBERP R3)
                           (NUMBERP R4)
                           (EQUAL (ASSOC 'EXP DEFS)
                                  (EXP-PROGRAM))
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM)))
                      (EQUAL (SM (ST '(EXP . 3)
                                     STK
                                     (LIST R0 R1 R2 R3 R4)
                                     F DEFS)
                                 (TIMES R4
                                        (PLUS 2 (TIMES-CLOCK R3) 3)))
                             (ST '(EXP . 3)
                                 STK
                                 (IF (ZEROP R4)
                                     (LIST R0 R1 R2 R3 R4)
                                     (LIST 0
                                           (TIMES (EXP R3 R4) R1)
                                           (TIMES (EXP R3 R4) R1)
                                           R3 0))
                                 F DEFS)))
             ((INDUCT (EXP-FN R0 R1 R2 R3 R4))))

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

Case 2. (IMPLIES (AND (ZEROP R4)
                      (NUMBERP R3)
                      (NUMBERP R4)
                      (EQUAL (ASSOC 'EXP DEFS)
                             '(EXP (MOVE 3 0)
                                   (MOVE 4 1)
                                   (MOVI 1 1)
                                   (JUMPZ 4 9)
                                   (MOVE 0 3)
                                   (CALL TIMES)
                                   (MOVE 1 2)
                                   (SUBI 4 1)
                                   (JUMP 3)
                                   (RET)))
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET))))
                 (EQUAL (SM (ST '(EXP . 3)
                                STK
                                (LIST R0 R1 R2 R3 R4)
                                F DEFS)
                            (TIMES R4
                                   (PLUS 2 (TIMES-CLOCK R3) 3)))
                        (ST '(EXP . 3)
                            STK
                            (IF (ZEROP R4)
                                (LIST R0 R1 R2 R3 R4)
                                (CONS 0
                                      (CONS (TIMES (EXP R3 R4) R1)
                                            (CONS (TIMES (EXP R3 R4) R1)
                                                  (CONS R3 '(0))))))
                            F DEFS))),

  which simplifies, applying SM-0, and opening up ZEROP, NUMBERP, CONS, EQUAL,
  and TIMES, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (EQUAL R4 0))
          (NUMBERP R4)
          (IMPLIES
              (AND (NUMBERP R3)
                   (NUMBERP (SUB1 R4))
                   (EQUAL (ASSOC 'EXP DEFS)
                          '(EXP (MOVE 3 0)
                                (MOVE 4 1)
                                (MOVI 1 1)
                                (JUMPZ 4 9)
                                (MOVE 0 3)
                                (CALL TIMES)
                                (MOVE 1 2)
                                (SUBI 4 1)
                                (JUMP 3)
                                (RET)))
                   (EQUAL (ASSOC 'TIMES DEFS)
                          '(TIMES (MOVI 2 0)
                                  (JUMPZ 0 5)
                                  (ADD 2 1)
                                  (SUBI 0 1)
                                  (JUMP 1)
                                  (RET))))
              (EQUAL (SM (ST '(EXP . 3)
                             STK
                             (LIST 0
                                   (TIMES R3 R1)
                                   (TIMES R3 R1)
                                   R3
                                   (SUB1 R4))
                             F DEFS)
                         (TIMES (SUB1 R4)
                                (PLUS 2 (TIMES-CLOCK R3) 3)))
                     (ST '(EXP . 3)
                         STK
                         (IF (ZEROP (SUB1 R4))
                             (LIST 0
                                   (TIMES R3 R1)
                                   (TIMES R3 R1)
                                   R3
                                   (SUB1 R4))
                             (CONS 0
                                   (CONS (TIMES (EXP R3 (SUB1 R4)) R3 R1)
                                         (CONS (TIMES (EXP R3 (SUB1 R4)) R3 R1)
                                               (CONS R3 '(0))))))
                         F DEFS)))
          (NUMBERP R3)
          (EQUAL (ASSOC 'EXP DEFS)
                 '(EXP (MOVE 3 0)
                       (MOVE 4 1)
                       (MOVI 1 1)
                       (JUMPZ 4 9)
                       (MOVE 0 3)
                       (CALL TIMES)
                       (MOVE 1 2)
                       (SUBI 4 1)
                       (JUMP 3)
                       (RET)))
          (EQUAL (ASSOC 'TIMES DEFS)
                 '(TIMES (MOVI 2 0)
                         (JUMPZ 0 5)
                         (ADD 2 1)
                         (SUBI 0 1)
                         (JUMP 1)
                         (RET))))
         (EQUAL (SM (ST '(EXP . 3)
                        STK
                        (LIST R0 R1 R2 R3 R4)
                        F DEFS)
                    (TIMES R4
                           (PLUS 2 (TIMES-CLOCK R3) 3)))
                (ST '(EXP . 3)
                    STK
                    (IF (ZEROP R4)
                        (LIST R0 R1 R2 R3 R4)
                        (CONS 0
                              (CONS (TIMES (EXP R3 R4) R1)
                                    (CONS (TIMES (EXP R3 R4) R1)
                                          (CONS R3 '(0))))))
                    F DEFS))).

  This simplifies, rewriting with the lemmas PC-ST, DEFS-ST, HALTEDP-ST,
  MEM-ST, CDR-CONS, CAR-CONS, STK-ST, STEP-OPENER, SM-0, SM-ADD1,
  TIMES-CORRECT, SM-PLUS, ASSOCIATIVITY-OF-TIMES, and PLUS-RIGHT-ID, and
  opening up the functions EQUAL, AND, ZEROP, CONS, IMPLIES, TIMES, LISTP,
  FETCH, CDR, CAR, GET, JUMPZ, SUB1, NUMBERP, ADD1-PC, EXECUTE, MOVE, PUT,
  TIMES-PROGRAM, SUBI, DIFFERENCE, JUMP, and EXP, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

EXP-CORRECT-LEMMA


(PROVE-LEMMA EXP-CORRECT
             (REWRITE)
             (IMPLIES (AND (NUMBERP I)
                           (NUMBERP J)
                           (EQUAL (FETCH PC DEFS) '(CALL EXP))
                           (EQUAL (ASSOC 'EXP DEFS)
                                  (EXP-PROGRAM))
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM)))
                      (EQUAL (SM (ST PC STK (LIST I J R2 R3 R4) F DEFS)
                                 (EXP-CLOCK I J))
                             (ST (ADD1-PC PC)
                                 STK
                                 (IF (ZEROP J)
                                     (LIST I (EXP I J) R2 I 0)
                                     (LIST 0 (EXP I J) (EXP I J) I 0))
                                 F DEFS))))

This conjecture can be simplified, using the abbreviations AND, IMPLIES, SM-0,
SM-ADD1, SM-PLUS, EXP-CLOCK, TIMES-PROGRAM, and EXP-PROGRAM, to:

      (IMPLIES
         (AND (NUMBERP I)
              (NUMBERP J)
              (EQUAL (FETCH PC DEFS) '(CALL EXP))
              (EQUAL (ASSOC 'EXP DEFS)
                     '(EXP (MOVE 3 0)
                           (MOVE 4 1)
                           (MOVI 1 1)
                           (JUMPZ 4 9)
                           (MOVE 0 3)
                           (CALL TIMES)
                           (MOVE 1 2)
                           (SUBI 4 1)
                           (JUMP 3)
                           (RET)))
              (EQUAL (ASSOC 'TIMES DEFS)
                     '(TIMES (MOVI 2 0)
                             (JUMPZ 0 5)
                             (ADD 2 1)
                             (SUBI 0 1)
                             (JUMP 1)
                             (RET))))
         (EQUAL (STEP (STEP (SM (STEP (STEP (STEP (STEP (ST PC STK
                                                            (LIST I J R2 R3 R4)
                                                            F DEFS)))))
                                (TIMES J
                                       (PLUS 2 (TIMES-CLOCK I) 3)))))
                (ST (ADD1-PC PC)
                    STK
                    (IF (ZEROP J)
                        (CONS I
                              (CONS (EXP I J)
                                    (CONS R2 (CONS I '(0)))))
                        (CONS 0
                              (CONS (EXP I J)
                                    (CONS (EXP I J) (CONS I '(0))))))
                    F DEFS))).

This simplifies, rewriting with the lemmas DEFS-ST, PC-ST, HALTEDP-ST, STK-ST,
MEM-ST, STEP-OPENER, CAR-CONS, CDR-CONS, TIMES-RIGHT-ID, and EXP-CORRECT-LEMMA,
and unfolding the definitions of FETCH, LISTP, CALL, CONS, ADD1-PC, CDR, EQUAL,
CAR, EXECUTE, GET, MOVE, SUB1, NUMBERP, PUT, MOVI, TIMES-PROGRAM, EXP-PROGRAM,
ZEROP, and EXP, to the following two new conjectures:

Case 2. (IMPLIES
            (AND (NUMBERP I)
                 (NUMBERP J)
                 (EQUAL (GET (CDR PC)
                             (CDR (ASSOC (CAR PC) DEFS)))
                        '(CALL EXP))
                 (EQUAL (ASSOC 'EXP DEFS)
                        '(EXP (MOVE 3 0)
                              (MOVE 4 1)
                              (MOVI 1 1)
                              (JUMPZ 4 9)
                              (MOVE 0 3)
                              (CALL TIMES)
                              (MOVE 1 2)
                              (SUBI 4 1)
                              (JUMP 3)
                              (RET)))
                 (EQUAL (ASSOC 'TIMES DEFS)
                        '(TIMES (MOVI 2 0)
                                (JUMPZ 0 5)
                                (ADD 2 1)
                                (SUBI 0 1)
                                (JUMP 1)
                                (RET)))
                 (NOT (EQUAL J 0)))
            (EQUAL (STEP (STEP (ST '(EXP . 3)
                                   (CONS (CONS (CAR PC) (ADD1 (CDR PC)))
                                         STK)
                                   (CONS 0
                                         (CONS (EXP I J)
                                               (CONS (EXP I J) (CONS I '(0)))))
                                   F DEFS)))
                   (ST (CONS (CAR PC) (ADD1 (CDR PC)))
                       STK
                       (CONS 0
                             (CONS (EXP I J)
                                   (CONS (EXP I J) (CONS I '(0)))))
                       F DEFS))).

  This again simplifies, appealing to the lemmas DEFS-ST, PC-ST, HALTEDP-ST,
  MEM-ST, CDR-CONS, STK-ST, STEP-OPENER, and CAR-CONS, and unfolding the
  functions LISTP, FETCH, CDR, CAR, GET, JUMPZ, SUB1, NUMBERP, CONS, EQUAL,
  EXECUTE, and RET, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP I)
                      (NUMBERP J)
                      (EQUAL (GET (CDR PC)
                                  (CDR (ASSOC (CAR PC) DEFS)))
                             '(CALL EXP))
                      (EQUAL (ASSOC 'EXP DEFS)
                             '(EXP (MOVE 3 0)
                                   (MOVE 4 1)
                                   (MOVI 1 1)
                                   (JUMPZ 4 9)
                                   (MOVE 0 3)
                                   (CALL TIMES)
                                   (MOVE 1 2)
                                   (SUBI 4 1)
                                   (JUMP 3)
                                   (RET)))
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL J 0))
                 (EQUAL (STEP (STEP (ST '(EXP . 3)
                                        (CONS (CONS (CAR PC) (ADD1 (CDR PC)))
                                              STK)
                                        (CONS I
                                              (CONS 1 (CONS R2 (CONS I '(0)))))
                                        F DEFS)))
                        (ST (CONS (CAR PC) (ADD1 (CDR PC)))
                            STK
                            (CONS I
                                  (CONS 1 (CONS R2 (CONS I '(0)))))
                            F DEFS))),

  which again simplifies, rewriting with DEFS-ST, PC-ST, HALTEDP-ST, MEM-ST,
  CDR-CONS, STK-ST, STEP-OPENER, and CAR-CONS, and expanding the functions
  NUMBERP, LISTP, FETCH, CDR, CAR, GET, JUMPZ, SUB1, CONS, EQUAL, EXECUTE, and
  RET, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EXP-CORRECT


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

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




[ 0.0 0.0 0.0 ]

LENGTH


(PROVE-LEMMA PUT-PUT-0
             (REWRITE)
             (IMPLIES (AND (LESSP ADDR (LENGTH MEM))
                           (EQUAL (GET ADDR MEM) VAL))
                      (EQUAL (PUT ADDR VAL MEM) MEM)))


     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 (OR (EQUAL (LENGTH MEM) 0)
                        (NOT (NUMBERP (LENGTH MEM))))
                    (p ADDR MEM))
           (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                                  (NOT (NUMBERP (LENGTH MEM)))))
                         (OR (EQUAL ADDR 0)
                             (NOT (NUMBERP ADDR))))
                    (p ADDR MEM))
           (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                                  (NOT (NUMBERP (LENGTH MEM)))))
                         (NOT (OR (EQUAL ADDR 0)
                                  (NOT (NUMBERP ADDR))))
                         (p (SUB1 ADDR) (CDR MEM)))
                    (p ADDR MEM))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT ADDR) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for MEM.  The above induction scheme
produces four new formulas:

Case 4. (IMPLIES (AND (OR (EQUAL (LENGTH MEM) 0)
                          (NOT (NUMBERP (LENGTH MEM))))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (PUT ADDR (GET ADDR MEM) MEM)
                        MEM)),

  which simplifies, opening up the definitions of LENGTH, NOT, OR, EQUAL, and
  LESSP, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (OR (EQUAL ADDR 0)
                          (NOT (NUMBERP ADDR)))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (PUT ADDR (GET ADDR MEM) MEM)
                        MEM)),

  which simplifies, applying CONS-CAR-CDR, and expanding the definitions of
  LENGTH, NOT, OR, EQUAL, LESSP, GET, and PUT, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (NOT (OR (EQUAL ADDR 0)
                               (NOT (NUMBERP ADDR))))
                      (NOT (LESSP (SUB1 ADDR)
                                  (LENGTH (CDR MEM))))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (PUT ADDR (GET ADDR MEM) MEM)
                        MEM)).

  This simplifies, rewriting with SUB1-ADD1, and opening up LENGTH, NOT, OR,
  and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (NOT (OR (EQUAL ADDR 0)
                               (NOT (NUMBERP ADDR))))
                      (EQUAL (PUT (SUB1 ADDR)
                                  (GET (SUB1 ADDR) (CDR MEM))
                                  (CDR MEM))
                             (CDR MEM))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (PUT ADDR (GET ADDR MEM) MEM)
                        MEM)),

  which simplifies, applying SUB1-ADD1 and CONS-CAR-CDR, and unfolding LENGTH,
  NOT, OR, LESSP, GET, and PUT, to:

        T.


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


[ 0.0 0.0 0.0 ]

PUT-PUT-0


(PROVE-LEMMA PUT-PUT-1
             (REWRITE)
             (EQUAL (PUT ADDR V2 (PUT ADDR V1 MEM))
                    (PUT ADDR V2 MEM)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Three inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP ADDR)
                    (p ADDR V2 V1 MEM))
           (IMPLIES (AND (NOT (ZEROP ADDR))
                         (p (SUB1 ADDR) V2 V1 (CDR MEM)))
                    (p ADDR V2 V1 MEM))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT ADDR) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for MEM.  The above induction scheme
leads to two new goals:

Case 2. (IMPLIES (ZEROP ADDR)
                 (EQUAL (PUT ADDR V2 (PUT ADDR V1 MEM))
                        (PUT ADDR V2 MEM))),

  which simplifies, applying the lemma CDR-CONS, and opening up the
  definitions of ZEROP, EQUAL, and PUT, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP ADDR))
                      (EQUAL (PUT (SUB1 ADDR)
                                  V2
                                  (PUT (SUB1 ADDR) V1 (CDR MEM)))
                             (PUT (SUB1 ADDR) V2 (CDR MEM))))
                 (EQUAL (PUT ADDR V2 (PUT ADDR V1 MEM))
                        (PUT ADDR V2 MEM))),

  which simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
  functions ZEROP and PUT, to:

        T.


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


[ 0.0 0.0 0.0 ]

PUT-PUT-1


(PROVE-LEMMA PUT-PUT-2
             (REWRITE)
             (IMPLIES (AND (NUMBERP ADDR1)
                           (NUMBERP ADDR2)
                           (NOT (EQUAL ADDR1 ADDR2)))
                      (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                             (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))))


     Give the conjecture the name *1.


     We will appeal to induction.  There are four plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP ADDR2)
                    (p ADDR2 V2 ADDR1 V1 MEM))
           (IMPLIES (AND (NOT (ZEROP ADDR2))
                         (p (SUB1 ADDR2)
                            V2
                            (SUB1 ADDR1)
                            V1
                            (CDR MEM)))
                    (p ADDR2 V2 ADDR1 V1 MEM))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT ADDR2) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for ADDR1 and MEM.  The above
induction scheme generates the following three new formulas:

Case 3. (IMPLIES (AND (ZEROP ADDR2)
                      (NUMBERP ADDR1)
                      (NUMBERP ADDR2)
                      (NOT (EQUAL ADDR1 ADDR2)))
                 (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                        (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))).

  This simplifies, unfolding ZEROP, NUMBERP, PUT, and EQUAL, to:

        (IMPLIES (AND (EQUAL ADDR2 0)
                      (NUMBERP ADDR1)
                      (NOT (EQUAL ADDR1 0)))
                 (EQUAL (PUT 0 V2
                             (CONS (CAR MEM)
                                   (PUT (SUB1 ADDR1) V1 (CDR MEM))))
                        (PUT ADDR1 V1 (CONS V2 (CDR MEM))))),

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

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP ADDR2))
                      (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                      (NUMBERP ADDR1)
                      (NUMBERP ADDR2)
                      (NOT (EQUAL ADDR1 ADDR2)))
                 (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                        (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))).

  This simplifies, using linear arithmetic, to the following two new
  conjectures:

  Case 2.2.
          (IMPLIES (AND (EQUAL ADDR2 0)
                        (NOT (ZEROP ADDR2))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2)))
                   (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                          (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))).

    However this again simplifies, unfolding the definition of ZEROP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (EQUAL ADDR1 0)
                        (NOT (ZEROP ADDR2))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2)))
                   (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                          (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))),

    which again simplifies, applying CDR-CONS and CAR-CONS, and opening up
    ZEROP, SUB1, NUMBERP, EQUAL, and PUT, to:

          (IMPLIES (AND (EQUAL 0 (SUB1 ADDR2))
                        (NUMBERP ADDR2)
                        (NOT (EQUAL 0 ADDR2)))
                   (EQUAL (CONS V1 (CONS V2 (CDDR MEM)))
                          (PUT 0 V1
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) V2 (CDR MEM)))))),

    which again simplifies, applying CDR-CONS, and opening up the definitions
    of EQUAL and PUT, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP ADDR2))
                      (EQUAL (PUT (SUB1 ADDR2)
                                  V2
                                  (PUT (SUB1 ADDR1) V1 (CDR MEM)))
                             (PUT (SUB1 ADDR1)
                                  V1
                                  (PUT (SUB1 ADDR2) V2 (CDR MEM))))
                      (NUMBERP ADDR1)
                      (NUMBERP ADDR2)
                      (NOT (EQUAL ADDR1 ADDR2)))
                 (EQUAL (PUT ADDR2 V2 (PUT ADDR1 V1 MEM))
                        (PUT ADDR1 V1 (PUT ADDR2 V2 MEM)))).

  This simplifies, applying the lemmas CAR-CONS and CDR-CONS, and expanding
  the definitions of ZEROP and PUT, to the following two new formulas:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL ADDR2 0))
                        (EQUAL (PUT (SUB1 ADDR2)
                                    V2
                                    (PUT (SUB1 ADDR1) V1 (CDR MEM)))
                               (PUT (SUB1 ADDR1)
                                    V1
                                    (PUT (SUB1 ADDR2) V2 (CDR MEM))))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (NOT (EQUAL ADDR1 0)))
                   (EQUAL (PUT ADDR2 V2
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR1) V1 (CDR MEM))))
                          (CONS (CAR MEM)
                                (PUT (SUB1 ADDR1)
                                     V1
                                     (PUT (SUB1 ADDR2) V2 (CDR MEM)))))).

    But this again simplifies, rewriting with CDR-CONS and CAR-CONS, and
    opening up PUT, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL ADDR2 0))
                        (EQUAL (PUT (SUB1 ADDR2)
                                    V2
                                    (PUT (SUB1 ADDR1) V1 (CDR MEM)))
                               (PUT (SUB1 ADDR1)
                                    V1
                                    (PUT (SUB1 ADDR2) V2 (CDR MEM))))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (EQUAL ADDR1 0))
                   (EQUAL (PUT ADDR2 V2 (CONS V1 (CDR MEM)))
                          (CONS V1
                                (PUT (SUB1 ADDR2) V2 (CDR MEM))))).

    But this again simplifies, rewriting with CAR-CONS and CDR-CONS, and
    expanding the definitions of SUB1, EQUAL, PUT, and NUMBERP, to:

          T.


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


[ 0.0 0.1 0.0 ]

PUT-PUT-2


(PROVE-LEMMA GET-PUT
             (REWRITE)
             (IMPLIES (AND (NUMBERP ADDR1) (NUMBERP ADDR2))
                      (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                             (IF (EQUAL ADDR1 ADDR2)
                                 VAL
                                 (GET ADDR1 MEM)))))

This conjecture simplifies, trivially, to the following two new formulas:

Case 2. (IMPLIES (AND (NUMBERP ADDR1)
                      (NUMBERP ADDR2)
                      (NOT (EQUAL ADDR1 ADDR2)))
                 (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                        (GET ADDR1 MEM))).

  Name the above subgoal *1.

Case 1. (IMPLIES (AND (NUMBERP ADDR1)
                      (NUMBERP ADDR2)
                      (EQUAL ADDR1 ADDR2))
                 (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                        VAL)).

  This again simplifies, obviously, to:

        (IMPLIES (NUMBERP ADDR2)
                 (EQUAL (GET ADDR2 (PUT ADDR2 VAL MEM))
                        VAL)),

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


     So now let us return to:

(IMPLIES (AND (NUMBERP ADDR1) (NUMBERP ADDR2))
         (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                (IF (EQUAL ADDR1 ADDR2)
                    VAL
                    (GET ADDR1 MEM)))),

named *1.  Let us appeal to the induction principle.  There are three
plausible inductions.  However, they merge into one likely candidate induction.
We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP ADDR1)
                    (p ADDR1 ADDR2 VAL MEM))
           (IMPLIES (AND (NOT (ZEROP ADDR1))
                         (p (SUB1 ADDR1)
                            (SUB1 ADDR2)
                            VAL
                            (CDR MEM)))
                    (p ADDR1 ADDR2 VAL MEM))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT ADDR1) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for ADDR2 and MEM.  The above
induction scheme leads to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP ADDR1)
                      (NUMBERP ADDR1)
                      (NUMBERP ADDR2))
                 (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                        (IF (EQUAL ADDR1 ADDR2)
                            VAL
                            (GET ADDR1 MEM)))).

  This simplifies, opening up ZEROP, NUMBERP, PUT, EQUAL, and GET, to the
  following four new goals:

  Case 2.4.
          (IMPLIES (AND (EQUAL ADDR1 0)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL 0 ADDR2))
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (CAR (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          (CAR MEM))).

    But this again simplifies, applying CAR-CONS, to:

          T.

  Case 2.3.
          (IMPLIES (AND (EQUAL ADDR1 0)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL 0 ADDR2))
                        (EQUAL ADDR2 0))
                   (EQUAL (CAR (CONS VAL (CDR MEM)))
                          (CAR MEM))).

    This again simplifies, trivially, to:

          T.

  Case 2.2.
          (IMPLIES (AND (EQUAL ADDR1 0)
                        (NUMBERP ADDR2)
                        (EQUAL 0 ADDR2)
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (CAR (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          VAL)).

    This again simplifies, obviously, to:

          T.

  Case 2.1.
          (IMPLIES (AND (EQUAL ADDR1 0)
                        (NUMBERP ADDR2)
                        (EQUAL 0 ADDR2)
                        (EQUAL ADDR2 0))
                   (EQUAL (CAR (CONS VAL (CDR MEM)))
                          VAL)).

    But this again simplifies, applying CAR-CONS, and unfolding NUMBERP and
    EQUAL, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP ADDR1))
                      (EQUAL (GET (SUB1 ADDR1)
                                  (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                             (IF (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                                 VAL
                                 (GET (SUB1 ADDR1) (CDR MEM))))
                      (NUMBERP ADDR1)
                      (NUMBERP ADDR2))
                 (EQUAL (GET ADDR1 (PUT ADDR2 VAL MEM))
                        (IF (EQUAL ADDR1 ADDR2)
                            VAL
                            (GET ADDR1 MEM)))).

  This simplifies, unfolding the definitions of ZEROP, PUT, and GET, to the
  following eight new formulas:

  Case 1.8.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (NOT (EQUAL (SUB1 ADDR1) (SUB1 ADDR2)))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               (GET (SUB1 ADDR1) (CDR MEM)))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (GET ADDR1
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          (GET (SUB1 ADDR1) (CDR MEM)))).

    This again simplifies, applying CDR-CONS, and opening up the definition of
    GET, to:

          T.

  Case 1.7.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (NOT (EQUAL (SUB1 ADDR1) (SUB1 ADDR2)))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               (GET (SUB1 ADDR1) (CDR MEM)))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (EQUAL ADDR2 0))
                   (EQUAL (GET ADDR1 (CONS VAL (CDR MEM)))
                          (GET (SUB1 ADDR1) (CDR MEM)))).

    But this again simplifies, rewriting with CDR-CONS, and opening up the
    definitions of SUB1, EQUAL, PUT, NUMBERP, and GET, to:

          T.

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (NOT (EQUAL (SUB1 ADDR1) (SUB1 ADDR2)))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               (GET (SUB1 ADDR1) (CDR MEM)))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (EQUAL ADDR1 ADDR2)
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (GET ADDR1
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          VAL)).

    This again simplifies, clearly, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (NOT (EQUAL (SUB1 ADDR1) (SUB1 ADDR2)))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               (GET (SUB1 ADDR1) (CDR MEM)))
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (EQUAL ADDR1 ADDR2)
                        (EQUAL ADDR2 0))
                   (EQUAL (GET ADDR1 (CONS VAL (CDR MEM)))
                          VAL)).

    This again simplifies, trivially, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               VAL)
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (GET ADDR1
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          (GET (SUB1 ADDR1) (CDR MEM)))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               VAL)
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (NOT (EQUAL ADDR1 ADDR2))
                        (EQUAL ADDR2 0))
                   (EQUAL (GET ADDR1 (CONS VAL (CDR MEM)))
                          (GET (SUB1 ADDR1) (CDR MEM)))),

    which again simplifies, applying the lemmas CAR-CONS and CDR-CONS, and
    expanding the definitions of SUB1, EQUAL, PUT, GET, and NUMBERP, to:

          (IMPLIES (AND (EQUAL (SUB1 ADDR1) 0)
                        (NUMBERP ADDR1)
                        (NOT (EQUAL ADDR1 0)))
                   (EQUAL (CADR MEM)
                          (GET (SUB1 ADDR1) (CDR MEM)))).

    This again simplifies, unfolding the definitions of EQUAL and GET, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               VAL)
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (EQUAL ADDR1 ADDR2)
                        (NOT (EQUAL ADDR2 0)))
                   (EQUAL (GET ADDR1
                               (CONS (CAR MEM)
                                     (PUT (SUB1 ADDR2) VAL (CDR MEM))))
                          VAL)),

    which again simplifies, rewriting with the lemma CDR-CONS, and opening up
    GET, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL ADDR1 0))
                        (EQUAL (SUB1 ADDR1) (SUB1 ADDR2))
                        (EQUAL (GET (SUB1 ADDR1)
                                    (PUT (SUB1 ADDR2) VAL (CDR MEM)))
                               VAL)
                        (NUMBERP ADDR1)
                        (NUMBERP ADDR2)
                        (EQUAL ADDR1 ADDR2)
                        (EQUAL ADDR2 0))
                   (EQUAL (GET ADDR1 (CONS VAL (CDR MEM)))
                          VAL)),

    which again simplifies, clearly, to:

          T.


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


[ 0.0 0.0 0.0 ]

GET-PUT


(PROVE-LEMMA LENGTH-PUT
             (REWRITE)
             (IMPLIES (LESSP ADDR (LENGTH MEM))
                      (EQUAL (LENGTH (PUT ADDR VAL MEM))
                             (LENGTH MEM))))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  Four inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (OR (EQUAL (LENGTH MEM) 0)
                        (NOT (NUMBERP (LENGTH MEM))))
                    (p ADDR VAL MEM))
           (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                                  (NOT (NUMBERP (LENGTH MEM)))))
                         (OR (EQUAL ADDR 0)
                             (NOT (NUMBERP ADDR))))
                    (p ADDR VAL MEM))
           (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                                  (NOT (NUMBERP (LENGTH MEM)))))
                         (NOT (OR (EQUAL ADDR 0)
                                  (NOT (NUMBERP ADDR))))
                         (p (SUB1 ADDR) VAL (CDR MEM)))
                    (p ADDR VAL MEM))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT ADDR) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for MEM.  The above induction scheme
leads to the following four new conjectures:

Case 4. (IMPLIES (AND (OR (EQUAL (LENGTH MEM) 0)
                          (NOT (NUMBERP (LENGTH MEM))))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (LENGTH (PUT ADDR VAL MEM))
                        (LENGTH MEM))).

  This simplifies, opening up LENGTH, NOT, OR, EQUAL, and LESSP, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (OR (EQUAL ADDR 0)
                          (NOT (NUMBERP ADDR)))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (LENGTH (PUT ADDR VAL MEM))
                        (LENGTH MEM))).

  This simplifies, rewriting with CDR-CONS, and expanding the functions LENGTH,
  NOT, OR, EQUAL, LESSP, and PUT, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (NOT (OR (EQUAL ADDR 0)
                               (NOT (NUMBERP ADDR))))
                      (NOT (LESSP (SUB1 ADDR)
                                  (LENGTH (CDR MEM))))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (LENGTH (PUT ADDR VAL MEM))
                        (LENGTH MEM))),

  which simplifies, rewriting with SUB1-ADD1, and unfolding LENGTH, NOT, OR,
  and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL (LENGTH MEM) 0)
                               (NOT (NUMBERP (LENGTH MEM)))))
                      (NOT (OR (EQUAL ADDR 0)
                               (NOT (NUMBERP ADDR))))
                      (EQUAL (LENGTH (PUT (SUB1 ADDR) VAL (CDR MEM)))
                             (LENGTH (CDR MEM)))
                      (LESSP ADDR (LENGTH MEM)))
                 (EQUAL (LENGTH (PUT ADDR VAL MEM))
                        (LENGTH MEM))).

  This simplifies, applying SUB1-ADD1 and CDR-CONS, and expanding LENGTH, NOT,
  OR, LESSP, and PUT, to:

        T.


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


[ 0.0 0.0 0.0 ]

LENGTH-PUT


(DISABLE GET)

[ 0.0 0.0 0.0 ]

GET-OFF


(DISABLE PUT)

[ 0.0 0.0 0.0 ]

PUT-OFF


(PROVE-LEMMA DIFFERENCE-1
             (REWRITE)
             (EQUAL (DIFFERENCE X 1) (SUB1 X)))

This simplifies, using linear arithmetic, to:

      (IMPLIES (LESSP X 1)
               (EQUAL (DIFFERENCE X 1) (SUB1 X))).

Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
(SUB1 X).  We employ the type restriction lemma noted when SUB1 was introduced
to constrain the new variable.  We must thus prove three new formulas:

Case 3. (IMPLIES (AND (EQUAL X 0) (LESSP X 1))
                 (EQUAL (DIFFERENCE X 1) (SUB1 X))),

  which further simplifies, expanding the functions LESSP, DIFFERENCE, SUB1,
  and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 1))
                 (EQUAL (DIFFERENCE X 1) (SUB1 X))),

  which further simplifies, appealing to the lemma SUB1-NNUMBERP, and
  unfolding the functions NUMBERP, EQUAL, LESSP, and DIFFERENCE, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (LESSP (ADD1 Z) 1))
                 (EQUAL (DIFFERENCE (ADD1 Z) 1) Z)),

  which further simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-1


(PROVE-LEMMA DIFFERENCE-ELIM
             (ELIM)
             (IMPLIES (AND (NUMBERP I) (NOT (LESSP I J)))
                      (EQUAL (PLUS J (DIFFERENCE I J)) I)))

This conjecture simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-ELIM


(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS (PLUS I J) K)
                    (PLUS I (PLUS J K))))

This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOCIATIVITY-OF-PLUS


(PROVE-LEMMA COMMUTATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS I J) (PLUS J I)))

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




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




This formula simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-PLUS


(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS I (PLUS K J))
                    (PLUS K (PLUS I J))))

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


This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY2-OF-PLUS


(DEFN TIMES-MEM-FN-LOOP
      (MEM)
      (IF (ZEROP (GET 0 MEM))
          MEM
          (TIMES-MEM-FN-LOOP (PUT 0
                                  (SUB1 (GET 0 MEM))
                                  (PUT 2
                                       (PLUS (GET 2 MEM) (GET 1 MEM))
                                       MEM))))
      ((LESSP (GET 0 MEM))))

     Linear arithmetic, the lemmas GET-PUT and COMMUTATIVITY-OF-PLUS, and the
definitions of EQUAL and ZEROP inform us that the measure (GET 0 MEM)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, TIMES-MEM-FN-LOOP is accepted under the definitional principle.
Observe that:
      (OR (LISTP (TIMES-MEM-FN-LOOP MEM))
          (EQUAL (TIMES-MEM-FN-LOOP MEM) MEM))
is a theorem.




[ 0.0 0.0 0.0 ]

TIMES-MEM-FN-LOOP


(DEFN TIMES-MEM-FN
      (MEM)
      (TIMES-MEM-FN-LOOP (PUT 2 0 MEM)))

     Observe that (LISTP (TIMES-MEM-FN MEM)) is a theorem.




[ 0.0 0.0 0.0 ]

TIMES-MEM-FN


(PROVE-LEMMA TIMES-MEM-FN-LOOP-IS-TIMES
             (REWRITE)
             (IMPLIES (AND (NUMBERP (GET 0 MEM))
                           (NUMBERP (GET 2 MEM))
                           (LESSP 2 (LENGTH MEM)))
                      (EQUAL (TIMES-MEM-FN-LOOP MEM)
                             (PUT 0 0
                                  (PUT 2
                                       (PLUS (TIMES (GET 0 MEM) (GET 1 MEM))
                                             (GET 2 MEM))
                                       MEM)))))

This formula simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, to
the formula:

      (IMPLIES (AND (NUMBERP (GET 0 MEM))
                    (NUMBERP (GET 2 MEM))
                    (LESSP 2 (LENGTH MEM)))
               (EQUAL (TIMES-MEM-FN-LOOP MEM)
                      (PUT 0 0
                           (PUT 2
                                (PLUS (GET 2 MEM)
                                      (TIMES (GET 0 MEM) (GET 1 MEM)))
                                MEM)))).

Give the above formula the name *1.


     Perhaps we can prove it by induction.  There are two plausible inductions,
both of which are unflawed.  So we will choose the one suggested by the
largest number of nonprimitive recursive functions.  We will induct according
to the following scheme:
      (AND (IMPLIES (ZEROP (GET 0 MEM)) (p MEM))
           (IMPLIES (AND (NOT (ZEROP (GET 0 MEM)))
                         (p (PUT 0
                                 (SUB1 (GET 0 MEM))
                                 (PUT 2
                                      (PLUS (GET 2 MEM) (GET 1 MEM))
                                      MEM))))
                    (p MEM))).
Linear arithmetic, the lemmas GET-PUT and COMMUTATIVITY-OF-PLUS, and the
definitions of EQUAL and ZEROP can be used to establish that the measure
(GET 0 MEM) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  The above induction scheme generates five new
conjectures:

Case 5. (IMPLIES (AND (ZEROP (GET 0 MEM))
                      (NUMBERP (GET 0 MEM))
                      (NUMBERP (GET 2 MEM))
                      (LESSP 2 (LENGTH MEM)))
                 (EQUAL (TIMES-MEM-FN-LOOP MEM)
                        (PUT 0 0
                             (PUT 2
                                  (PLUS (GET 2 MEM)
                                        (TIMES (GET 0 MEM) (GET 1 MEM)))
                                  MEM)))),

  which simplifies, using linear arithmetic, rewriting with
  COMMUTATIVITY-OF-PLUS and PUT-PUT-0, and unfolding ZEROP, NUMBERP,
  TIMES-MEM-FN-LOOP, EQUAL, TIMES, and PLUS, to:

        T.

Case 4. (IMPLIES
               (AND (NOT (ZEROP (GET 0 MEM)))
                    (NOT (NUMBERP (GET 0
                                       (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))))
                    (NUMBERP (GET 0 MEM))
                    (NUMBERP (GET 2 MEM))
                    (LESSP 2 (LENGTH MEM)))
               (EQUAL (TIMES-MEM-FN-LOOP MEM)
                      (PUT 0 0
                           (PUT 2
                                (PLUS (GET 2 MEM)
                                      (TIMES (GET 0 MEM) (GET 1 MEM)))
                                MEM)))).

  This simplifies, applying COMMUTATIVITY-OF-PLUS and GET-PUT, and unfolding
  the functions ZEROP and EQUAL, to:

        T.

Case 3. (IMPLIES
               (AND (NOT (ZEROP (GET 0 MEM)))
                    (NOT (NUMBERP (GET 2
                                       (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))))
                    (NUMBERP (GET 0 MEM))
                    (NUMBERP (GET 2 MEM))
                    (LESSP 2 (LENGTH MEM)))
               (EQUAL (TIMES-MEM-FN-LOOP MEM)
                      (PUT 0 0
                           (PUT 2
                                (PLUS (GET 2 MEM)
                                      (TIMES (GET 0 MEM) (GET 1 MEM)))
                                MEM)))),

  which simplifies, applying COMMUTATIVITY-OF-PLUS and GET-PUT, and expanding
  the functions ZEROP and EQUAL, to:

        T.

Case 2. (IMPLIES
              (AND (NOT (ZEROP (GET 0 MEM)))
                   (NOT (LESSP 2
                               (LENGTH (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))))
                   (NUMBERP (GET 0 MEM))
                   (NUMBERP (GET 2 MEM))
                   (LESSP 2 (LENGTH MEM)))
              (EQUAL (TIMES-MEM-FN-LOOP MEM)
                     (PUT 0 0
                          (PUT 2
                               (PLUS (GET 2 MEM)
                                     (TIMES (GET 0 MEM) (GET 1 MEM)))
                               MEM)))).

  This simplifies, using linear arithmetic, applying COMMUTATIVITY-OF-PLUS and
  LENGTH-PUT, and expanding ZEROP, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (ZEROP (GET 0 MEM)))
          (EQUAL
           (TIMES-MEM-FN-LOOP (PUT 0
                                   (SUB1 (GET 0 MEM))
                                   (PUT 2
                                        (PLUS (GET 2 MEM) (GET 1 MEM))
                                        MEM)))
           (PUT 0 0
                (PUT 2
                     (PLUS (GET 2
                                (PUT 0
                                     (SUB1 (GET 0 MEM))
                                     (PUT 2
                                          (PLUS (GET 2 MEM) (GET 1 MEM))
                                          MEM)))
                           (TIMES (GET 0
                                       (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))
                                  (GET 1
                                       (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))))
                     (PUT 0
                          (SUB1 (GET 0 MEM))
                          (PUT 2
                               (PLUS (GET 2 MEM) (GET 1 MEM))
                               MEM)))))
          (NUMBERP (GET 0 MEM))
          (NUMBERP (GET 2 MEM))
          (LESSP 2 (LENGTH MEM)))
         (EQUAL (TIMES-MEM-FN-LOOP MEM)
                (PUT 0 0
                     (PUT 2
                          (PLUS (GET 2 MEM)
                                (TIMES (GET 0 MEM) (GET 1 MEM)))
                          MEM)))),

  which simplifies, rewriting with the lemmas COMMUTATIVITY-OF-PLUS, GET-PUT,
  COMMUTATIVITY2-OF-PLUS, PUT-PUT-1, and PUT-PUT-2, and unfolding the
  definitions of ZEROP, EQUAL, TIMES-MEM-FN-LOOP, and TIMES, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-MEM-FN-LOOP-IS-TIMES


(PROVE-LEMMA TIMES-MEM-FN-IS-CORRECT NIL
             (IMPLIES (AND (NUMBERP (GET 0 MEM))
                           (LESSP 2 (LENGTH MEM)))
                      (EQUAL (TIMES-MEM-FN MEM)
                             (PUT 0 0
                                  (PUT 2
                                       (TIMES (GET 0 MEM) (GET 1 MEM))
                                       MEM)))))

This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
TIMES-MEM-FN, to:

      (IMPLIES (AND (NUMBERP (GET 0 MEM))
                    (LESSP 2 (LENGTH MEM)))
               (EQUAL (TIMES-MEM-FN-LOOP (PUT 2 0 MEM))
                      (PUT 0 0
                           (PUT 2
                                (TIMES (GET 0 MEM) (GET 1 MEM))
                                MEM)))).

This simplifies, using linear arithmetic, applying LENGTH-PUT, GET-PUT,
COMMUTATIVITY-OF-PLUS, PUT-PUT-1, and TIMES-MEM-FN-LOOP-IS-TIMES, and
expanding NUMBERP, EQUAL, and PLUS, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-MEM-FN-IS-CORRECT


(DEFN TIMES-STEP
      (S)
      (ST (ADD1-PC (PC S))
          (STK S)
          (PUT 0 0
               (PUT 2
                    (TIMES (GET 0 (MEM S))
                           (GET 1 (MEM S)))
                    (MEM S)))
          F
          (DEFS S)))

     Observe that (STP (TIMES-STEP S)) is a theorem.




[ 0.0 0.0 0.0 ]

TIMES-STEP


(PROVE-LEMMA TIMES-CORRECT-LEMMA-REVISITED
             (REWRITE)
             (IMPLIES (AND (NUMBERP (GET 0 MEM))
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM)))
                      (EQUAL (SM (ST '(TIMES . 1) STK1 MEM F DEFS)
                                 (TIMES (GET 0 MEM) 4))
                             (ST '(TIMES . 1)
                                 STK1
                                 (TIMES-MEM-FN-LOOP MEM)
                                 F DEFS)))
             ((INDUCT (TIMES-MEM-FN-LOOP MEM))))

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

Case 2. (IMPLIES (AND (ZEROP (GET 0 MEM))
                      (NUMBERP (GET 0 MEM))
                      (EQUAL (ASSOC 'TIMES DEFS)
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET))))
                 (EQUAL (SM (ST '(TIMES . 1) STK1 MEM F DEFS)
                            (TIMES (GET 0 MEM) 4))
                        (ST '(TIMES . 1)
                            STK1
                            (TIMES-MEM-FN-LOOP MEM)
                            F DEFS))),

  which simplifies, rewriting with the lemma SM-0, and opening up the
  definitions of ZEROP, NUMBERP, TIMES, EQUAL, and TIMES-MEM-FN-LOOP, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (EQUAL (GET 0 MEM) 0))
          (NUMBERP (GET 0 MEM))
          (IMPLIES
           (AND (NUMBERP (GET 0
                              (PUT 0
                                   (SUB1 (GET 0 MEM))
                                   (PUT 2
                                        (PLUS (GET 2 MEM) (GET 1 MEM))
                                        MEM))))
                (EQUAL (ASSOC 'TIMES DEFS)
                       '(TIMES (MOVI 2 0)
                               (JUMPZ 0 5)
                               (ADD 2 1)
                               (SUBI 0 1)
                               (JUMP 1)
                               (RET))))
           (EQUAL
                (SM (ST '(TIMES . 1)
                        STK1
                        (PUT 0
                             (SUB1 (GET 0 MEM))
                             (PUT 2
                                  (PLUS (GET 2 MEM) (GET 1 MEM))
                                  MEM))
                        F DEFS)
                    (TIMES (GET 0
                                (PUT 0
                                     (SUB1 (GET 0 MEM))
                                     (PUT 2
                                          (PLUS (GET 2 MEM) (GET 1 MEM))
                                          MEM)))
                           4))
                (ST '(TIMES . 1)
                    STK1
                    (TIMES-MEM-FN-LOOP (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 2 MEM) (GET 1 MEM))
                                                 MEM)))
                    F DEFS)))
          (EQUAL (ASSOC 'TIMES DEFS)
                 '(TIMES (MOVI 2 0)
                         (JUMPZ 0 5)
                         (ADD 2 1)
                         (SUBI 0 1)
                         (JUMP 1)
                         (RET))))
         (EQUAL (SM (ST '(TIMES . 1) STK1 MEM F DEFS)
                    (TIMES (GET 0 MEM) 4))
                (ST '(TIMES . 1)
                    STK1
                    (TIMES-MEM-FN-LOOP MEM)
                    F DEFS))),

  which simplifies, applying COMMUTATIVITY-OF-PLUS, GET-PUT, PC-ST, DEFS-ST,
  HALTEDP-ST, MEM-ST, STK-ST, STEP-OPENER, DIFFERENCE-1, SM-0, SM-ADD1,
  SM-PLUS, and ST-EQUAL, and expanding the functions EQUAL, AND, IMPLIES,
  TIMES, LISTP, FETCH, CDR, CAR, GET, JUMPZ, ADD1-PC, EXECUTE, ADD, SUBI, JUMP,
  and CONS, to the new goal:

        (IMPLIES
         (AND
          (NOT (EQUAL (GET 0 MEM) 0))
          (NUMBERP (GET 0 MEM))
          (EQUAL
                (SM (ST '(TIMES . 1)
                        STK1
                        (PUT 0
                             (SUB1 (GET 0 MEM))
                             (PUT 2
                                  (PLUS (GET 1 MEM) (GET 2 MEM))
                                  MEM))
                        F DEFS)
                    (TIMES (SUB1 (GET 0 MEM)) 4))
                (ST '(TIMES . 1)
                    STK1
                    (TIMES-MEM-FN-LOOP (PUT 0
                                            (SUB1 (GET 0 MEM))
                                            (PUT 2
                                                 (PLUS (GET 1 MEM) (GET 2 MEM))
                                                 MEM)))
                    F DEFS))
          (EQUAL (ASSOC 'TIMES DEFS)
                 '(TIMES (MOVI 2 0)
                         (JUMPZ 0 5)
                         (ADD 2 1)
                         (SUBI 0 1)
                         (JUMP 1)
                         (RET))))
         (EQUAL (TIMES-MEM-FN-LOOP (PUT 0
                                        (SUB1 (GET 0 MEM))
                                        (PUT 2
                                             (PLUS (GET 1 MEM) (GET 2 MEM))
                                             MEM)))
                (TIMES-MEM-FN-LOOP MEM))),

  which again simplifies, rewriting with PC-ST and COMMUTATIVITY-OF-PLUS, and
  opening up the definition of TIMES-MEM-FN-LOOP, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

TIMES-CORRECT-LEMMA-REVISITED


(PROVE-LEMMA TIMES-CORRECT-LEMMA-REVISITED-AND-GENERALIZED
             (REWRITE)
             (IMPLIES (AND (EQUAL R0 (GET 0 MEM))
                           (NUMBERP (GET 0 MEM))
                           (EQUAL (ASSOC 'TIMES DEFS)
                                  (TIMES-PROGRAM)))
                      (EQUAL (SM (ST '(TIMES . 1) STK1 MEM F DEFS)
                                 (TIMES R0 4))
                             (ST '(TIMES . 1)
                                 STK1
                                 (TIMES-MEM-FN-LOOP MEM)
                                 F DEFS))))

This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
TIMES-PROGRAM, to:

      (IMPLIES (AND (EQUAL R0 (GET 0 MEM))
                    (NUMBERP (GET 0 MEM))
                    (EQUAL (ASSOC 'TIMES DEFS)
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET))))
               (EQUAL (SM (ST '(TIMES . 1) STK1 MEM F DEFS)
                          (TIMES R0 4))
                      (ST '(TIMES . 1)
                          STK1
                          (TIMES-MEM-FN-LOOP MEM)
                          F DEFS))).

This simplifies, appealing to the lemma TIMES-CORRECT-LEMMA-REVISITED, and
expanding EQUAL and TIMES-PROGRAM, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-CORRECT-LEMMA-REVISITED-AND-GENERALIZED


(PROVE-LEMMA TIMES-CORRECT-REVISITED NIL
             (IMPLIES (AND (EQUAL (FETCH (PC S) (DEFS S))
                                  '(CALL TIMES))
                           (EQUAL (ASSOC 'TIMES (DEFS S))
                                  (TIMES-PROGRAM))
                           (LESSP 2 (LENGTH (MEM S)))
                           (EQUAL R0 (GET 0 (MEM S)))
                           (NUMBERP R0)
                           (NOT (LESSP N (TIMES-CLOCK R0)))
                           (NOT (HALTEDP S)))
                      (EQUAL (SM S N)
                             (SM (TIMES-STEP S)
                                 (DIFFERENCE N (TIMES-CLOCK R0)))))
             ((DISABLE COMMUTATIVITY-OF-PLUS COMMUTATIVITY2-OF-PLUS)
              (ENABLE TIMES-CLOCK)))

This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
TIMES-CLOCK, and TIMES-PROGRAM, to the conjecture:

      (IMPLIES (AND (EQUAL (FETCH (PC S) (DEFS S))
                           '(CALL TIMES))
                    (EQUAL (ASSOC 'TIMES (DEFS S))
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET)))
                    (LESSP 2 (LENGTH (MEM S)))
                    (EQUAL R0 (GET 0 (MEM S)))
                    (NUMBERP R0)
                    (NOT (LESSP N (PLUS 2 (TIMES R0 4) 2)))
                    (NOT (HALTEDP S)))
               (EQUAL (SM S N)
                      (SM (TIMES-STEP S)
                          (DIFFERENCE N
                                      (PLUS 2 (TIMES R0 4) 2))))).

This simplifies, opening up the definitions of FETCH, ADD1-PC, and TIMES-STEP,
to:

      (IMPLIES (AND (EQUAL (GET (CDR (PC S))
                                (CDR (ASSOC (CAR (PC S)) (DEFS S))))
                           '(CALL TIMES))
                    (EQUAL (ASSOC 'TIMES (DEFS S))
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET)))
                    (LESSP 2 (LENGTH (MEM S)))
                    (NUMBERP (GET 0 (MEM S)))
                    (NOT (LESSP N
                                (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)))
                    (NOT (HALTEDP S)))
               (EQUAL (SM S N)
                      (SM (ST (CONS (CAR (PC S))
                                    (ADD1 (CDR (PC S))))
                              (STK S)
                              (PUT 0 0
                                   (PUT 2
                                        (TIMES (GET 0 (MEM S))
                                               (GET 1 (MEM S)))
                                        (MEM S)))
                              F
                              (DEFS S))
                          (DIFFERENCE N
                                      (PLUS 2
                                            (TIMES (GET 0 (MEM S)) 4)
                                            2))))).

Applying the lemma DIFFERENCE-ELIM, replace N by:
      (PLUS (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)
            X)
to eliminate (DIFFERENCE N (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)).  We use the
type restriction lemma noted when DIFFERENCE was introduced to restrict the
new variable.  We would thus like to prove the following two new conjectures:

Case 2. (IMPLIES (AND (NOT (NUMBERP N))
                      (EQUAL (GET (CDR (PC S))
                                  (CDR (ASSOC (CAR (PC S)) (DEFS S))))
                             '(CALL TIMES))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (LESSP 2 (LENGTH (MEM S)))
                      (NUMBERP (GET 0 (MEM S)))
                      (NOT (LESSP N
                                  (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)))
                      (NOT (HALTEDP S)))
                 (EQUAL (SM S N)
                        (SM (ST (CONS (CAR (PC S))
                                      (ADD1 (CDR (PC S))))
                                (STK S)
                                (PUT 0 0
                                     (PUT 2
                                          (TIMES (GET 0 (MEM S))
                                                 (GET 1 (MEM S)))
                                          (MEM S)))
                                F
                                (DEFS S))
                            (DIFFERENCE N
                                        (PLUS 2
                                              (TIMES (GET 0 (MEM S)) 4)
                                              2))))).

  However this further simplifies, applying SM-0, and unfolding the functions
  LESSP and DIFFERENCE, to the new formula:

        (IMPLIES (AND (NOT (NUMBERP N))
                      (EQUAL (GET (CDR (PC S))
                                  (CDR (ASSOC (CAR (PC S)) (DEFS S))))
                             '(CALL TIMES))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (LESSP 2 (LENGTH (MEM S)))
                      (NUMBERP (GET 0 (MEM S)))
                      (EQUAL (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)
                             0)
                      (NOT (HALTEDP S)))
                 (EQUAL (SM S N)
                        (ST (CONS (CAR (PC S))
                                  (ADD1 (CDR (PC S))))
                            (STK S)
                            (PUT 0 0
                                 (PUT 2
                                      (TIMES (GET 0 (MEM S))
                                             (GET 1 (MEM S)))
                                      (MEM S)))
                            F
                            (DEFS S)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (EQUAL (GET (CDR (PC S))
                                  (CDR (ASSOC (CAR (PC S)) (DEFS S))))
                             '(CALL TIMES))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (LESSP 2 (LENGTH (MEM S)))
                      (NUMBERP (GET 0 (MEM S)))
                      (NOT (LESSP (PLUS (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)
                                        X)
                                  (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)))
                      (NOT (HALTEDP S)))
                 (EQUAL (SM S
                            (PLUS (PLUS 2 (TIMES (GET 0 (MEM S)) 4) 2)
                                  X))
                        (SM (ST (CONS (CAR (PC S))
                                      (ADD1 (CDR (PC S))))
                                (STK S)
                                (PUT 0 0
                                     (PUT 2
                                          (TIMES (GET 0 (MEM S))
                                                 (GET 1 (MEM S)))
                                          (MEM S)))
                                F
                                (DEFS S))
                            X))),

  which further simplifies, using linear arithmetic, rewriting with
  ASSOCIATIVITY-OF-PLUS, STEP-OPENER, DEFS-ST, PC-ST, HALTEDP-ST, STK-ST,
  MEM-ST, SM-0, SM-ADD1, GET-PUT, LENGTH-PUT, PLUS-RIGHT-ID, PUT-PUT-1,
  TIMES-MEM-FN-LOOP-IS-TIMES, TIMES-CORRECT-LEMMA-REVISITED-AND-GENERALIZED,
  CAR-CONS, CDR-CONS, and SM-PLUS, and unfolding LISTP, FETCH, CALL, CONS,
  ADD1-PC, CDR, EQUAL, CAR, EXECUTE, GET, MOVI, TIMES-PROGRAM, NUMBERP, JUMPZ,
  and RET, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

TIMES-CORRECT-REVISITED


(PROVE-LEMMA VERIFICATION-CONDITIONS-FOR-TIMES NIL
             (AND (IMPLIES (AND (NUMBERP I0) (NUMBERP I1))
                           (AND (NUMBERP 0)
                                (EQUAL (TIMES I0 I1)
                                       (PLUS 0 (TIMES I0 I1)))))
                  (IMPLIES (AND (NUMBERP R2)
                                (EQUAL (TIMES I0 I1)
                                       (PLUS R2 (TIMES R0 R1)))
                                (NOT (ZEROP R0)))
                           (AND (NUMBERP (PLUS R2 R1))
                                (EQUAL (TIMES I0 I1)
                                       (PLUS (PLUS R2 R1)
                                             (TIMES (SUB1 R0) R1)))))
                  (IMPLIES (AND (NUMBERP R2)
                                (EQUAL (TIMES I0 I1)
                                       (PLUS R2 (TIMES R0 R1)))
                                (ZEROP R0))
                           (EQUAL R2 (TIMES I0 I1)))))

This conjecture can be simplified, using the abbreviations ZEROP, NOT, IMPLIES,
AND, and ASSOCIATIVITY-OF-PLUS, to three new formulas:

Case 3. (IMPLIES (AND (NUMBERP I0) (NUMBERP I1))
                 (AND (NUMBERP 0)
                      (EQUAL (TIMES I0 I1)
                             (PLUS 0 (TIMES I0 I1))))),

  which simplifies, expanding the definitions of NUMBERP, EQUAL, PLUS, and AND,
  to:

        T.

Case 2. (IMPLIES (AND (NUMBERP R2)
                      (EQUAL (TIMES I0 I1)
                             (PLUS R2 (TIMES R0 R1)))
                      (NOT (EQUAL R0 0))
                      (NUMBERP R0))
                 (AND (NUMBERP (PLUS R2 R1))
                      (EQUAL (TIMES I0 I1)
                             (PLUS R2 R1 (TIMES (SUB1 R0) R1))))),

  which simplifies, rewriting with COMMUTATIVITY2-OF-PLUS and
  COMMUTATIVITY-OF-PLUS, and unfolding the functions TIMES and AND, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP R2)
                      (EQUAL (TIMES I0 I1)
                             (PLUS R2 (TIMES R0 R1)))
                      (ZEROP R0))
                 (EQUAL R2 (TIMES I0 I1))).

  This simplifies, unfolding the function ZEROP, to the following two new
  goals:

  Case 1.2.
          (IMPLIES (AND (NUMBERP R2)
                        (EQUAL (TIMES I0 I1)
                               (PLUS R2 (TIMES R0 R1)))
                        (EQUAL R0 0))
                   (EQUAL R2 (TIMES I0 I1))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP R2)
                        (EQUAL (TIMES I0 I1)
                               (PLUS R2 (TIMES R0 R1)))
                        (NOT (NUMBERP R0)))
                   (EQUAL R2 (TIMES I0 I1))),

    which again simplifies, applying COMMUTATIVITY-OF-PLUS, and expanding
    TIMES, EQUAL, and PLUS, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

VERIFICATION-CONDITIONS-FOR-TIMES


(CONSTRAIN P-STEP
           (REWRITE)
           (IMPLIES (P S) (P (STEP S)))
           ((P (LAMBDA (S) T))))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (IMPLIES T T).

This simplifies, clearly, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-STEP


(PROVE-LEMMA P-INVARIANT
             (REWRITE)
             (IMPLIES (P S0) (P (SM S0 N)))
             ((ENABLE SM)))


     Call the conjecture *1.


     We will try to prove it by induction.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p S0 N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (p (STEP S0) (SUB1 N)))
                    (p S0 N))).
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 induction step of the scheme.  Note,
however, the inductive instance chosen for S0.  The above induction scheme
generates the following three new formulas:

Case 3. (IMPLIES (AND (ZEROP N) (P S0))
                 (P (SM S0 N))).

  This simplifies, applying SM-0, and expanding the functions ZEROP and SM, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (P (STEP S0)))
                      (P S0))
                 (P (SM S0 N))),

  which simplifies, appealing to the lemma P-STEP, and unfolding the function
  ZEROP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (P (SM (STEP S0) (SUB1 N)))
                      (P S0))
                 (P (SM S0 N))),

  which simplifies, unfolding the definitions of ZEROP and SM, to:

        T.


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


[ 0.0 0.0 0.0 ]

P-INVARIANT


(DEFN R0 (S) (GET 0 (MEM S)))

   




[ 0.0 0.0 0.0 ]

R0


(DEFN R1 (S) (GET 1 (MEM S)))

   




[ 0.0 0.0 0.0 ]

R1


(DEFN R2 (S) (GET 2 (MEM S)))

   




[ 0.0 0.0 0.0 ]

R2


(DEFN TIMESP
     (I0 I1 S)
     (AND (NUMBERP I0)
          (NUMBERP I1)
          (STP S)
          (NLISTP (STK S))
          (EQUAL (ASSOC 'TIMES (DEFS S))
                 (TIMES-PROGRAM))
          (EQUAL I1 (R1 S))
          (IF (EQUAL (PC S) '(TIMES . 0))
              (EQUAL I0 (R0 S))
              (IF (EQUAL (PC S) '(TIMES . 1))
                  (AND (NUMBERP (R2 S))
                       (EQUAL (TIMES I0 I1)
                              (PLUS (R2 S) (TIMES (R0 S) (R1 S)))))
                  (IF (EQUAL (PC S) '(TIMES . 2))
                      (AND (NOT (ZEROP (R0 S)))
                           (NUMBERP (R2 S))
                           (EQUAL (TIMES I0 I1)
                                  (PLUS (R2 S) (TIMES (R0 S) (R1 S)))))
                      (IF (EQUAL (PC S) '(TIMES . 3))
                          (AND (NOT (ZEROP (R0 S)))
                               (NUMBERP (R2 S))
                               (EQUAL (PLUS I1 (TIMES I0 I1))
                                      (PLUS (R2 S) (TIMES (R0 S) (R1 S)))))
                          (IF (EQUAL (PC S) '(TIMES . 4))
                              (AND (NUMBERP (R2 S))
                                   (EQUAL (TIMES I0 I1)
                                          (PLUS (R2 S) (TIMES (R0 S) (R1 S)))))
                              (IF (EQUAL (PC S) '(TIMES . 5))
                                  (EQUAL (R2 S) (TIMES I0 I1))
                                  F))))))))

     From the definition we can conclude that:
      (OR (FALSEP (TIMESP I0 I1 S))
          (TRUEP (TIMESP I0 I1 S)))
is a theorem.




[ 0.0 0.0 0.0 ]

TIMESP


(PROVE-LEMMA TIMESP-STEP
             (REWRITE)
             (IMPLIES (TIMESP I0 I1 S)
                      (TIMESP I0 I1 (STEP S))))

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


This formula can be simplified, using the abbreviations R2, R0, R1,
TIMES-PROGRAM, TIMESP, and IMPLIES, to:

      (IMPLIES (AND (NUMBERP I0)
                    (NUMBERP I1)
                    (STP S)
                    (NOT (LISTP (STK S)))
                    (EQUAL (ASSOC 'TIMES (DEFS S))
                           '(TIMES (MOVI 2 0)
                                   (JUMPZ 0 5)
                                   (ADD 2 1)
                                   (SUBI 0 1)
                                   (JUMP 1)
                                   (RET)))
                    (EQUAL I1 (GET 1 (MEM S)))
                    (CASE (PC S)
                          ((TIMES . 0)
                           (EQUAL I0 (GET 0 (MEM S))))
                          ((TIMES . 1)
                           (IF (NUMBERP (GET 2 (MEM S)))
                               (EQUAL (TIMES I0 I1)
                                      (PLUS (GET 2 (MEM S))
                                            (TIMES (GET 0 (MEM S))
                                                   (GET 1 (MEM S)))))
                               F))
                          ((TIMES . 2)
                           (COND ((EQUAL (GET 0 (MEM S)) 0) F)
                                 ((NUMBERP (GET 0 (MEM S)))
                                  (IF (NUMBERP (GET 2 (MEM S)))
                                      (EQUAL (TIMES I0 I1)
                                             (PLUS (GET 2 (MEM S))
                                                   (TIMES (GET 0 (MEM S))
                                                          (GET 1 (MEM S)))))
                                      F))
                                 (T F)))
                          ((TIMES . 3)
                           (COND ((EQUAL (GET 0 (MEM S)) 0) F)
                                 ((NUMBERP (GET 0 (MEM S)))
                                  (IF (NUMBERP (GET 2 (MEM S)))
                                      (EQUAL (PLUS I1 (TIMES I0 I1))
                                             (PLUS (GET 2 (MEM S))
                                                   (TIMES (GET 0 (MEM S))
                                                          (GET 1 (MEM S)))))
                                      F))
                                 (T F)))
                          ((TIMES . 4)
                           (IF (NUMBERP (GET 2 (MEM S)))
                               (EQUAL (TIMES I0 I1)
                                      (PLUS (GET 2 (MEM S))
                                            (TIMES (GET 0 (MEM S))
                                                   (GET 1 (MEM S)))))
                               F))
                          ((TIMES . 5)
                           (EQUAL (GET 2 (MEM S)) (TIMES I0 I1)))
                          (OTHERWISE F)))
               (TIMESP I0 I1 (STEP S))),

which simplifies, appealing to the lemmas STEP-OPENER, DIFFERENCE-1, and
COMMUTATIVITY-OF-PLUS, and unfolding LISTP, FETCH, CDR, CAR, GET, MOVI,
ADD1-PC, EQUAL, EXECUTE, RET, SUBI, ADD, JUMPZ, CONS, and JUMP, to 14 new
conjectures:

Case 14.(IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL (PC S) '(TIMES . 0))
                      (EQUAL I0 (GET 0 (MEM S)))
                      (NOT (HALTEDP S)))
                 (TIMESP I0
                         (GET 1 (MEM S))
                         (ST '(TIMES . 1)
                             (STK S)
                             (PUT 2 0 (MEM S))
                             F
                             (DEFS S)))),

  which again simplifies, applying PC-ST, MEM-ST, GET-PUT, DEFS-ST, and STK-ST,
  and expanding the definitions of PLUS, R0, NUMBERP, R2, R1, EQUAL,
  TIMES-PROGRAM, and TIMESP, to:

        T.

Case 13.(IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL (PC S) '(TIMES . 0))
                      (EQUAL I0 (GET 0 (MEM S)))
                      (HALTEDP S))
                 (TIMESP I0 (GET 1 (MEM S)) S)).

  But this again simplifies, opening up R0, R1, EQUAL, TIMES-PROGRAM, and
  TIMESP, to:

        T.

Case 12.(IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (NOT (EQUAL (PC S) '(TIMES . 1)))
                      (NOT (EQUAL (PC S) '(TIMES . 2)))
                      (NOT (EQUAL (PC S) '(TIMES . 3)))
                      (NOT (EQUAL (PC S) '(TIMES . 4)))
                      (EQUAL (PC S) '(TIMES . 5))
                      (EQUAL (GET 2 (MEM S))
                             (TIMES I0 (GET 1 (MEM S))))
                      (NOT (HALTEDP S)))
                 (TIMESP I0
                         (GET 1 (MEM S))
                         (ST '(TIMES . 5)
                             (STK S)
                             (MEM S)
                             T
                             (DEFS S)))),

  which again simplifies, applying the lemmas PC-ST, MEM-ST, DEFS-ST, and
  STK-ST, and opening up EQUAL, R2, R1, TIMES-PROGRAM, and TIMESP, to:

        T.

Case 11.(IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (NOT (EQUAL (PC S) '(TIMES . 1)))
                      (NOT (EQUAL (PC S) '(TIMES . 2)))
                      (NOT (EQUAL (PC S) '(TIMES . 3)))
                      (NOT (EQUAL (PC S) '(TIMES . 4)))
                      (EQUAL (PC S) '(TIMES . 5))
                      (EQUAL (GET 2 (MEM S))
                             (TIMES I0 (GET 1 (MEM S))))
                      (HALTEDP S))
                 (TIMESP I0 (GET 1 (MEM S)) S)),

  which again simplifies, unfolding the functions EQUAL, R2, R1, TIMES-PROGRAM,
  and TIMESP, to:

        T.

Case 10.(IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (NOT (EQUAL (PC S) '(TIMES . 1)))
                      (NOT (EQUAL (PC S) '(TIMES . 2)))
                      (EQUAL (PC S) '(TIMES . 3))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (PLUS (GET 1 (MEM S))
                                   (TIMES I0 (GET 1 (MEM S))))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (NOT (HALTEDP S)))
                 (TIMESP I0
                         (GET 1 (MEM S))
                         (ST '(TIMES . 4)
                             (STK S)
                             (PUT 0 (SUB1 (GET 0 (MEM S))) (MEM S))
                             F
                             (DEFS S)))),

  which again simplifies, rewriting with PC-ST, MEM-ST, GET-PUT, DEFS-ST, and
  STK-ST, and opening up the definitions of EQUAL, R0, R2, R1, TIMES-PROGRAM,
  and TIMESP, to:

        (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL (PC S) '(TIMES . 3))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (PLUS (GET 1 (MEM S))
                                   (TIMES I0 (GET 1 (MEM S))))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (NOT (HALTEDP S)))
                 (EQUAL (TIMES I0 (GET 1 (MEM S)))
                        (PLUS (GET 2 (MEM S))
                              (TIMES (SUB1 (GET 0 (MEM S)))
                                     (GET 1 (MEM S)))))),

  which again simplifies, applying COMMUTATIVITY2-OF-PLUS, and opening up
  TIMES, to the new formula:

        (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (EQUAL (PC S) '(TIMES . 3))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (PLUS (GET 1 (MEM S))
                                   (TIMES I0 (GET 1 (MEM S))))
                             (PLUS (GET 1 (MEM S))
                                   (GET 2 (MEM S))
                                   (TIMES (SUB1 (GET 0 (MEM S)))
                                          (GET 1 (MEM S)))))
                      (NOT (HALTEDP S)))
                 (EQUAL (TIMES I0 (GET 1 (MEM S)))
                        (PLUS (GET 2 (MEM S))
                              (TIMES (SUB1 (GET 0 (MEM S)))
                                     (GET 1 (MEM S)))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 9. (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (NOT (EQUAL (PC S) '(TIMES . 1)))
                      (NOT (EQUAL (PC S) '(TIMES . 2)))
                      (EQUAL (PC S) '(TIMES . 3))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (PLUS (GET 1 (MEM S))
                                   (TIMES I0 (GET 1 (MEM S))))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (HALTEDP S))
                 (TIMESP I0 (GET 1 (MEM S)) S)),

  which again simplifies, unfolding the functions EQUAL, R2, R0, R1,
  TIMES-PROGRAM, and TIMESP, to:

        T.

Case 8. (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (EQUAL (PC S) '(TIMES . 2))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (TIMES I0 (GET 1 (MEM S)))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (NOT (HALTEDP S)))
                 (TIMESP I0
                         (GET 1 (MEM S))
                         (ST '(TIMES . 3)
                             (STK S)
                             (PUT 2
                                  (PLUS (GET 1 (MEM S)) (GET 2 (MEM S)))
                                  (MEM S))
                             F
                             (DEFS S)))),

  which again simplifies, rewriting with the lemmas COMMUTATIVITY2-OF-PLUS,
  COMMUTATIVITY-OF-PLUS, PC-ST, MEM-ST, GET-PUT, DEFS-ST, and STK-ST, and
  opening up the functions EQUAL, R2, R0, R1, TIMES-PROGRAM, and TIMESP, to:

        T.

Case 7. (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (EQUAL (PC S) '(TIMES . 2))
                      (NOT (EQUAL (GET 0 (MEM S)) 0))
                      (NUMBERP (GET 0 (MEM S)))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (TIMES I0 (GET 1 (MEM S)))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (HALTEDP S))
                 (TIMESP I0 (GET 1 (MEM S)) S)),

  which again simplifies, opening up EQUAL, R2, R0, R1, TIMES-PROGRAM, and
  TIMESP, to:

        T.

Case 6. (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIMES . 0)))
                      (EQUAL (PC S) '(TIMES . 1))
                      (NUMBERP (GET 2 (MEM S)))
                      (EQUAL (TIMES I0 (GET 1 (MEM S)))
                             (PLUS (GET 2 (MEM S))
                                   (TIMES (GET 0 (MEM S))
                                          (GET 1 (MEM S)))))
                      (NOT (HALTEDP S))
                      (NOT (NUMBERP (GET 0 (MEM S)))))
                 (TIMESP I0
                         (GET 1 (MEM S))
                         (ST '(TIMES . 5)
                             (STK S)
                             (MEM S)
                             F
                             (DEFS S)))),

  which again simplifies, applying COMMUTATIVITY-OF-PLUS, PC-ST, MEM-ST,
  DEFS-ST, and STK-ST, and unfolding the functions EQUAL, TIMES, PLUS, R2, R1,
  TIMES-PROGRAM, and TIMESP, to:

        T.

Case 5. (IMPLIES (AND (NUMBERP I0)
                      (NUMBERP (GET 1 (MEM S)))
                      (STP S)
                      (NOT (LISTP (STK S)))
                      (EQUAL (ASSOC 'TIMES (DEFS S))
                             '(TIMES (MOVI 2 0)
                                     (JUMPZ 0 5)
                                     (ADD 2 1)
                                     (SUBI 0 1)
                                     (JUMP 1)
                                     (RET)))
                      (NOT (EQUAL (PC S) '(TIME