(NOTE-LIB "app-c-d-e" T)
Loading ./flatau/app-c-d-e.lib
Finished loading ./flatau/app-c-d-e.lib
Loading ./flatau/app-c-d-e.o
Loading ./flatau/0app-c-d-e.o
Finished loading ./flatau/0app-c-d-e.o
Loading ./flatau/1app-c-d-e.o
Finished loading ./flatau/1app-c-d-e.o
Finished loading ./flatau/app-c-d-e.o

(#./flatau/app-c-d-e.lib #./flatau/app-c-d-e)


(PROVE-LEMMA AXIOM-53
             (REWRITE)
             (IMPLIES (SUBRP FN)
                      (EQUAL (FORMALS FN) F)))

WARNING:  the previously added lemma, SUBRP-FORMALS, could be applied whenever
the newly proposed AXIOM-53 could!


This formula simplifies, applying the lemma SUBRP-FORMALS, and expanding the
definition of EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

AXIOM-53


(DISABLE PROPER-P-STATEP-RESTRUCTURING)

[ 0.0 0.0 0.0 ]

PROPER-P-STATEP-RESTRUCTURING-OFF


(DEFN CHANGE-ELEMENTS
      (LIST)
      (IF (LISTP LIST)
          (IF (TRUEP (CAR LIST))
              (CONS (FALSE)
                    (CHANGE-ELEMENTS (CDR LIST)))
              (CONS (TRUE)
                    (CHANGE-ELEMENTS (CDR LIST))))
          (IF (TRUEP LIST) (FALSE) (TRUE))))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LIST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, CHANGE-ELEMENTS is accepted under the principle of
definition.  Note that:
      (OR (FALSEP (CHANGE-ELEMENTS LIST))
          (TRUEP (CHANGE-ELEMENTS LIST))
          (LISTP (CHANGE-ELEMENTS LIST)))
is a theorem.




[ 0.0 0.0 0.0 ]

CHANGE-ELEMENTS


(DISABLE DEPOSIT)

[ 0.0 0.0 0.0 ]

DEPOSIT-OFF


(DISABLE FETCH)

[ 0.0 0.0 0.0 ]

FETCH-OFF


(DISABLE ADD-ADDR)

[ 0.0 0.0 0.0 ]

ADD-ADDR-OFF


(DISABLE SUB-ADDR)

[ 0.0 0.0 0.0 ]

SUB-ADDR-OFF


(DISABLE OFFSET)

[ 0.0 0.0 0.0 ]

OFFSET-OFF


(DISABLE AREA-NAME)

[ 0.0 0.0 0.0 ]

AREA-NAME-OFF


(DISABLE ERRORP)

[ 0.0 0.0 0.0 ]

ERRORP-OFF


(DISABLE P-CURRENT-PROGRAM)

[ 0.0 0.0 0.0 ]

P-CURRENT-PROGRAM-OFF


(PROVE-LEMMA MY-GET-PUT
             (REWRITE)
             (IMPLIES (AND (NUMBERP K) (NUMBERP N))
                      (EQUAL (GET K (PUT VAL N LST))
                             (IF (EQUAL K N) VAL (GET K LST))))
             ((ENABLE GET-CONS GET PUT GET-ANYTHING-NIL)))

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

Case 2. (IMPLIES (AND (NUMBERP K)
                      (NUMBERP N)
                      (NOT (EQUAL K N)))
                 (EQUAL (GET K (PUT VAL N LST))
                        (GET K LST))).

  Name the above subgoal *1.

Case 1. (IMPLIES (AND (NUMBERP K)
                      (NUMBERP N)
                      (EQUAL K N))
                 (EQUAL (GET K (PUT VAL N LST)) VAL)).

  This again simplifies, obviously, to:

        (IMPLIES (NUMBERP N)
                 (EQUAL (GET N (PUT VAL N LST)) 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 K) (NUMBERP N))
         (EQUAL (GET K (PUT VAL N LST))
                (IF (EQUAL K N) VAL (GET K LST)))),

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 K) (p K VAL N LST))
           (IMPLIES (AND (NOT (ZEROP K))
                         (p (SUB1 K) VAL (SUB1 N) (CDR LST)))
                    (p K VAL N LST))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT K) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for N and LST.  The above induction
scheme leads to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP K)
                      (NUMBERP K)
                      (NUMBERP N))
                 (EQUAL (GET K (PUT VAL N LST))
                        (IF (EQUAL K N) VAL (GET K LST)))).

  This simplifies, rewriting with the lemma GET-ZEROP, and unfolding the
  functions ZEROP, NUMBERP, and PUT, to the following six new goals:

  Case 2.6.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (NOT (EQUAL 0 N))
                        (NOT (EQUAL N 0)))
                   (EQUAL (CAR (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          (CAR LST))).

    This again simplifies, rewriting with the lemma CAR-CONS, to:

          T.

  Case 2.5.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (NOT (EQUAL 0 N))
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (CAR (CONS VAL (CDR LST)))
                          (CAR LST))),

    which again simplifies, clearly, to:

          T.

  Case 2.4.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (NOT (EQUAL 0 N))
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (CAR (LIST VAL)) (CAR LST))).

    This again simplifies, trivially, to:

          T.

  Case 2.3.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (EQUAL 0 N)
                        (NOT (EQUAL N 0)))
                   (EQUAL (CAR (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          VAL)).

    This again simplifies, obviously, to:

          T.

  Case 2.2.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (EQUAL 0 N)
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (CAR (CONS VAL (CDR LST)))
                          VAL)).

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

          T.

  Case 2.1.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP N)
                        (EQUAL 0 N)
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (CAR (LIST VAL)) VAL)).

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

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP K))
                      (EQUAL (GET (SUB1 K)
                                  (PUT VAL (SUB1 N) (CDR LST)))
                             (IF (EQUAL (SUB1 K) (SUB1 N))
                                 VAL
                                 (GET (SUB1 K) (CDR LST))))
                      (NUMBERP K)
                      (NUMBERP N))
                 (EQUAL (GET K (PUT VAL N LST))
                        (IF (EQUAL K N) VAL (GET K LST)))).

  This simplifies, opening up ZEROP, PUT, and GET, to the following 12 new
  conjectures:

  Case 1.12.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (NOT (EQUAL N 0)))
                   (EQUAL (GET K
                               (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          (GET (SUB1 K) (CDR LST)))).

    However this again simplifies, applying GET-CONS, to:

          T.

  Case 1.11.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (GET K (CONS VAL (CDR LST)))
                          (GET (SUB1 K) (CDR LST)))).

    This again simplifies, appealing to the lemmas EQUAL-SUB1-0 and GET-CONS,
    and opening up the definitions of SUB1, EQUAL, PUT, and NUMBERP, to:

          T.

  Case 1.10.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (GET K (LIST VAL))
                          (GET (SUB1 K) (CDR LST)))),

    which again simplifies, applying the lemmas EQUAL-SUB1-0, CDR-NLISTP,
    GET-ANYTHING-NIL, and GET-CONS, and expanding the definitions of SUB1,
    LISTP, EQUAL, PUT, and NUMBERP, to:

          T.

  Case 1.9.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (NOT (EQUAL N 0)))
                   (EQUAL (GET K
                               (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          VAL)),

    which again simplifies, clearly, to:

          T.

  Case 1.8.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (GET K (CONS VAL (CDR LST)))
                          VAL)).

    This again simplifies, trivially, to:

          T.

  Case 1.7.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (NOT (EQUAL (SUB1 K) (SUB1 N)))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               (GET (SUB1 K) (CDR LST)))
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (GET K (LIST VAL)) VAL)).

    This again simplifies, trivially, to:

          T.

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (NOT (EQUAL N 0)))
                   (EQUAL (GET K
                               (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          (GET (SUB1 K) (CDR LST)))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (GET K (CONS VAL (CDR LST)))
                          (GET (SUB1 K) (CDR LST)))),

    which again simplifies, rewriting with EQUAL-SUB1-0, GET-ZEROP, CDR-CONS,
    CAR-NLISTP, and GET-ADD1-OPENER, and opening up the definitions of SUB1,
    EQUAL, PUT, ZEROP, and NUMBERP, to the following two new conjectures:

    Case 1.5.2.
            (IMPLIES (AND (EQUAL K 1)
                          (NOT (LISTP (CDR LST)))
                          (EQUAL (CAR (LIST VAL)) VAL)
                          (LISTP LST))
                     (EQUAL 0 (GET (SUB1 K) (CDR LST)))).

      This again simplifies, applying CAR-CONS, CAR-NLISTP, and GET-ZEROP, and
      expanding the definitions of SUB1, ZEROP, and EQUAL, to:

            T.

    Case 1.5.1.
            (IMPLIES (AND (EQUAL K 1)
                          (LISTP (CDR LST))
                          (EQUAL (CAR (CONS VAL (CDDR LST)))
                                 VAL)
                          (LISTP LST))
                     (EQUAL (CADR LST)
                            (GET (SUB1 K) (CDR LST)))).

      This again simplifies, appealing to the lemmas CAR-CONS and GET-ZEROP,
      and opening up the definitions of SUB1 and ZEROP, to:

            T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (NOT (EQUAL K N))
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (GET K (LIST VAL))
                          (GET (SUB1 K) (CDR LST)))),

    which again simplifies, applying EQUAL-SUB1-0, CDR-NLISTP, CAR-CONS,
    GET-ZEROP, CDR-CONS, and GET-ADD1-OPENER, and expanding the functions SUB1,
    LISTP, EQUAL, PUT, ZEROP, NUMBERP, and GET, to the new goal:

          (IMPLIES (AND (EQUAL K 1) (NOT (LISTP LST)))
                   (EQUAL 0 (GET (SUB1 K) (CDR LST)))),

    which again simplifies, applying CDR-NLISTP, and expanding SUB1, GET, and
    EQUAL, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (NOT (EQUAL N 0)))
                   (EQUAL (GET K
                               (CONS (CAR LST)
                                     (PUT VAL (SUB1 N) (CDR LST))))
                          VAL)).

    However this again simplifies, rewriting with GET-CONS, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (EQUAL N 0)
                        (LISTP LST))
                   (EQUAL (GET K (CONS VAL (CDR LST)))
                          VAL)).

    This again simplifies, obviously, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL K 0))
                        (EQUAL (SUB1 K) (SUB1 N))
                        (EQUAL (GET (SUB1 K)
                                    (PUT VAL (SUB1 N) (CDR LST)))
                               VAL)
                        (NUMBERP K)
                        (NUMBERP N)
                        (EQUAL K N)
                        (EQUAL N 0)
                        (NOT (LISTP LST)))
                   (EQUAL (GET K (LIST VAL)) VAL)).

    This again simplifies, trivially, to:

          T.


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


[ 0.0 0.0 0.1 ]

MY-GET-PUT


(DISABLE MY-GET-PUT)

[ 0.0 0.0 0.0 ]

MY-GET-PUT-OFF


(PROVE-LEMMA LISTP-CDR-P-FRAME
             (REWRITE)
             (LISTP (CDR (P-FRAME BINDINGS RET-PC)))
             ((ENABLE P-FRAME)))

This formula can be simplified, using the abbreviations CDR-CONS and P-FRAME,
to:

      (LISTP (LIST RET-PC)),

which simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LISTP-CDR-P-FRAME


(PROVE-LEMMA EQUAL-CDDR-P-FRAME-NIL
             (REWRITE)
             (EQUAL (CDDR (P-FRAME BINDINGS RET-PC))
                    NIL)
             ((ENABLE P-FRAME)))

This conjecture can be simplified, using the abbreviations CDR-CONS and
P-FRAME, to the conjecture:

      (EQUAL NIL NIL).

This simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-CDDR-P-FRAME-NIL


(DEFN S-L-EVAL-EQUIV-HYPS
      (FLAG S C)
      (AND (S-GOOD-STATEP S C)
           (GOOD-POSP FLAG
                      (S-POS S)
                      (S-BODY (S-PROG S)))
           (EQUAL (S-ERR-FLAG (S-EVAL FLAG S C))
                  'RUN)))

     Observe that:
      (OR (FALSEP (S-L-EVAL-EQUIV-HYPS FLAG S C))
          (TRUEP (S-L-EVAL-EQUIV-HYPS FLAG S C)))
is a theorem.




[ 0.0 0.0 0.0 ]

S-L-EVAL-EQUIV-HYPS


(DEFN S-L-EVAL-FLAG-RUN-HYPS
      (FLAG S C)
      (AND (S-GOOD-STATEP S C)
           (S-ALL-TEMPS-SETP FLAG
                             (IF (EQUAL FLAG 'LIST)
                                 (S-EXPR-LIST S)
                                 (S-EXPR S))
                             (TEMP-ALIST-TO-SET (S-TEMPS S)))
           (S-ALL-PROGS-TEMPS-SETP (S-PROGS S))
           (IF (EQUAL FLAG 'LIST)
               (NOT (MEMBER F
                            (L-EVAL FLAG
                                    (S-EXPAND-TEMPS FLAG (S-EXPR-LIST S))
                                    (S-PARAMS S)
                                    C)))
               (L-EVAL FLAG
                       (S-EXPAND-TEMPS FLAG (S-EXPR S))
                       (S-PARAMS S)
                       C))
           (S-CHECK-TEMPS-SETP (S-TEMPS S))))

     Note that:
      (OR (FALSEP (S-L-EVAL-FLAG-RUN-HYPS FLAG S C))
          (TRUEP (S-L-EVAL-FLAG-RUN-HYPS FLAG S C)))
is a theorem.




[ 0.0 0.0 0.0 ]

S-L-EVAL-FLAG-RUN-HYPS


(DEFN LR-UNDEFINED-TAG NIL 0)

     From the definition we can conclude that (NUMBERP (LR-UNDEFINED-TAG)) is
a theorem.




[ 0.0 0.0 0.0 ]

LR-UNDEFINED-TAG


(DEFN LR-INIT-TAG NIL 1)

     From the definition we can conclude that (NUMBERP (LR-INIT-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-INIT-TAG


(DEFN LR-FALSE-TAG NIL 2)

     From the definition we can conclude that (NUMBERP (LR-FALSE-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-FALSE-TAG


(DEFN LR-TRUE-TAG NIL 3)

     From the definition we can conclude that (NUMBERP (LR-TRUE-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-TRUE-TAG


(DEFN LR-ADD1-TAG NIL 4)

     From the definition we can conclude that (NUMBERP (LR-ADD1-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-ADD1-TAG


(DEFN LR-CONS-TAG NIL 5)

     From the definition we can conclude that (NUMBERP (LR-CONS-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-CONS-TAG


(DEFN LR-PACK-TAG NIL 6)

     From the definition we can conclude that (NUMBERP (LR-PACK-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-PACK-TAG


(DEFN LR-MINUS-TAG NIL 7)

     From the definition we can conclude that (NUMBERP (LR-MINUS-TAG)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-MINUS-TAG


(DEFN LR-HEAP-NAME NIL 'HEAP)

     From the definition we can conclude that (LITATOM (LR-HEAP-NAME)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-HEAP-NAME


(DEFN LR-NODE-SIZE NIL 4)

     From the definition we can conclude that (NUMBERP (LR-NODE-SIZE)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-NODE-SIZE


(DEFN LR-UNDEF-ADDR NIL
      (TAG 'ADDR '(HEAP . 0)))

     Observe that (LISTP (LR-UNDEF-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-UNDEF-ADDR


(DEFN LR-F-ADDR NIL
      (ADD-ADDR (LR-UNDEF-ADDR)
                (LR-NODE-SIZE)))

     From the definition we can conclude that (LISTP (LR-F-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-F-ADDR


(DEFN LR-T-ADDR NIL
      (ADD-ADDR (LR-F-ADDR) (LR-NODE-SIZE)))

     From the definition we can conclude that (LISTP (LR-T-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-T-ADDR


(DEFN LR-0-ADDR NIL
      (ADD-ADDR (LR-T-ADDR) (LR-NODE-SIZE)))

     From the definition we can conclude that (LISTP (LR-0-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-0-ADDR


(DEFN LR-FP-ADDR NIL
      (TAG 'ADDR '(FREE-PTR . 0)))

     Observe that (LISTP (LR-FP-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-FP-ADDR


(DEFN LR-ANSWER-ADDR NIL
      (TAG 'ADDR '(ANSWER . 0)))

     Observe that (LISTP (LR-ANSWER-ADDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-ANSWER-ADDR


(DEFN LR-FETCH-FP
      (DATA-SEG)
      (FETCH (LR-FP-ADDR) DATA-SEG))

   




[ 0.0 0.0 0.0 ]

LR-FETCH-FP


(DEFN LR-MINIMUM-HEAP-SIZE NIL
      (OFFSET (ADD-ADDR (LR-0-ADDR)
                        (LR-NODE-SIZE))))

   




[ 0.0 0.0 0.0 ]

LR-MINIMUM-HEAP-SIZE


(DEFN LR-NEW-NODE
      (TAG REF-COUNT VALUE1 VALUE2)
      (LIST TAG REF-COUNT VALUE1 VALUE2))

     Note that (LISTP (LR-NEW-NODE TAG REF-COUNT VALUE1 VALUE2)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-NEW-NODE


(DEFN LR-REF-COUNT-OFFSET NIL 1)

     From the definition we can conclude that (NUMBERP (LR-REF-COUNT-OFFSET))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-REF-COUNT-OFFSET


(DEFN LR-CAR-OFFSET NIL 2)

     From the definition we can conclude that (NUMBERP (LR-CAR-OFFSET)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-CAR-OFFSET


(DEFN LR-CDR-OFFSET NIL 3)

     From the definition we can conclude that (NUMBERP (LR-CDR-OFFSET)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-CDR-OFFSET


(DEFN LR-UNPACK-OFFSET NIL 2)

     From the definition we can conclude that (NUMBERP (LR-UNPACK-OFFSET)) is
a theorem.




[ 0.0 0.0 0.0 ]

LR-UNPACK-OFFSET


(DEFN LR-UNBOX-NAT-OFFSET NIL 2)

     From the definition we can conclude that (NUMBERP (LR-UNBOX-NAT-OFFSET))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-UNBOX-NAT-OFFSET


(DEFN LR-NEGATIVE-GUTS-OFFSET NIL 2)

     From the definition we can conclude that:
      (NUMBERP (LR-NEGATIVE-GUTS-OFFSET))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-NEGATIVE-GUTS-OFFSET


(DEFN LR-BOUNDARY-OFFSETP
      (OFFSET)
      (EQUAL (REMAINDER OFFSET (LR-NODE-SIZE))
             0))

     From the definition we can conclude that:
      (OR (FALSEP (LR-BOUNDARY-OFFSETP OFFSET))
          (TRUEP (LR-BOUNDARY-OFFSETP OFFSET)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-BOUNDARY-OFFSETP


(DEFN LR-BOUNDARY-NODEP
      (NODE)
      (LR-BOUNDARY-OFFSETP (OFFSET NODE)))

     From the definition we can conclude that:
      (OR (FALSEP (LR-BOUNDARY-NODEP NODE))
          (TRUEP (LR-BOUNDARY-NODEP NODE)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-BOUNDARY-NODEP


(DEFN LR-NODEP
      (ADDR DATA-SEG)
      (AND (EQUAL (TYPE ADDR) 'ADDR)
           (EQUAL (CDDR ADDR) NIL)
           (LISTP ADDR)
           (ADPP (UNTAG ADDR) DATA-SEG)
           (LR-BOUNDARY-NODEP ADDR)
           (EQUAL (AREA-NAME ADDR)
                  (LR-HEAP-NAME))))

     Note that:
      (OR (FALSEP (LR-NODEP ADDR DATA-SEG))
          (TRUEP (LR-NODEP ADDR DATA-SEG)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-NODEP


(DEFN LR-GOOD-POINTERP
      (ADDR DATA-SEG)
      (AND (LR-NODEP ADDR DATA-SEG)
           (EQUAL (TYPE (FETCH (ADD-ADDR ADDR (LR-REF-COUNT-OFFSET))
                               DATA-SEG))
                  'NAT)))

     Observe that:
      (OR (FALSEP (LR-GOOD-POINTERP ADDR DATA-SEG))
          (TRUEP (LR-GOOD-POINTERP ADDR DATA-SEG)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-GOOD-POINTERP


(DEFN LR-EXPR
      (P)
      (CUR-EXPR (OFFSET (P-PC P))
                (PROGRAM-BODY (P-CURRENT-PROGRAM P))))

   




[ 0.0 0.0 0.0 ]

LR-EXPR


(DISABLE LR-EXPR)

[ 0.0 0.0 0.0 ]

LR-EXPR-OFF


(DEFN LR-EXPR-LIST
      (P)
      (RESTN (CAR (LAST (OFFSET (P-PC P))))
             (CUR-EXPR (BUTLAST (OFFSET (P-PC P)))
                       (PROGRAM-BODY (P-CURRENT-PROGRAM P)))))

   




[ 0.0 0.0 0.0 ]

LR-EXPR-LIST


(DISABLE LR-EXPR-LIST)

[ 0.0 0.0 0.0 ]

LR-EXPR-LIST-OFF


(DEFN MARK-INSTR
      (INSTRUCTION-LIST N)
      (IF (ZEROP N)
          (CONS (LIST 'PC-> (CAR INSTRUCTION-LIST))
                (CDR INSTRUCTION-LIST))
          (CONS (CAR INSTRUCTION-LIST)
                (MARK-INSTR (CDR INSTRUCTION-LIST)
                            (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, MARK-INSTR is accepted under
the principle of definition.  Observe that:
      (LISTP (MARK-INSTR INSTRUCTION-LIST N))
is a theorem.




[ 0.0 0.0 0.0 ]

MARK-INSTR


(DEFN FIX-PROGRAM-SEGMENT
      (PROGRAMS PC)
      (IF (LISTP PROGRAMS)
          (LET ((PROG (CAR PROGRAMS)))
               (IF (EQUAL (CAR PROG) (AREA-NAME PC))
                   (CONS (APPEND (LIST (CAR PROG)
                                       (CADR PROG)
                                       (CADDR PROG))
                                 (MARK-INSTR (PROGRAM-BODY PROG)
                                             (OFFSET PC)))
                         (FIX-PROGRAM-SEGMENT (CDR PROGRAMS)
                                              PC))
                   (CONS (CAR PROG)
                         (FIX-PROGRAM-SEGMENT (CDR PROGRAMS)
                                              PC))))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT PROGRAMS) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, FIX-PROGRAM-SEGMENT is accepted under the
definitional principle.  Observe that:
      (OR (LITATOM (FIX-PROGRAM-SEGMENT PROGRAMS PC))
          (LISTP (FIX-PROGRAM-SEGMENT PROGRAMS PC)))
is a theorem.




[ 0.0 0.0 0.0 ]

FIX-PROGRAM-SEGMENT


(DEFN FIX-DATA-SEGMENT
    (DATA-SEGMENT)
    (PUT-VALUE (APPEND (FIRSTN (OFFSET (LR-FETCH-FP DATA-SEGMENT))
                               (VALUE (LR-HEAP-NAME) DATA-SEGMENT))
                       (DIFFERENCE (LENGTH (VALUE (LR-HEAP-NAME) DATA-SEGMENT))
                                   (OFFSET (LR-FETCH-FP DATA-SEGMENT))))
               (LR-HEAP-NAME)
               DATA-SEGMENT))

     Observe that:
      (OR (LISTP (FIX-DATA-SEGMENT DATA-SEGMENT))
          (EQUAL (FIX-DATA-SEGMENT DATA-SEGMENT)
                 DATA-SEGMENT))
is a theorem.




[ 0.0 0.0 0.0 ]

FIX-DATA-SEGMENT


(DEFN FIND-NON-PROPER-INSTR
      (LST NAME P)
      (IF (LISTP LST)
          (IF (AND (LEGAL-LABELP (CAR LST))
                   (PROPER-P-INSTRUCTIONP (UNLABEL (CAR LST))
                                          NAME P))
              (FIND-NON-PROPER-INSTR (CDR LST)
                                     NAME P)
              (CAR LST))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT LST) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, FIND-NON-PROPER-INSTR is accepted under the
principle of definition.




[ 0.0 0.0 0.0 ]

FIND-NON-PROPER-INSTR


(DEFN FIND-NON-PROPER-PROGRAMS
      (PROGS P)
      (IF (LISTP PROGS)
          (IF (PROPER-P-PROGRAMP (CAR PROGS) P)
              (CONS (NAME (CAR PROGS))
                    (FIND-NON-PROPER-PROGRAMS (CDR PROGS)
                                              P))
              (CONS (LIST 'NOT
                          (NAME (CAR PROGS))
                          (FIND-NON-PROPER-INSTR (PROGRAM-BODY (CAR PROGS))
                                                 (NAME (CAR PROGS))
                                                 P))
                    (FIND-NON-PROPER-PROGRAMS (CDR PROGS)
                                              P)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT PROGS) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, FIND-NON-PROPER-PROGRAMS is accepted under the
definitional principle.  From the definition we can conclude that:
      (OR (LITATOM (FIND-NON-PROPER-PROGRAMS PROGS P))
          (LISTP (FIND-NON-PROPER-PROGRAMS PROGS P)))
is a theorem.




[ 0.0 0.0 0.0 ]

FIND-NON-PROPER-PROGRAMS


(DEFN PPS
      (STATE)
      (LIST 'P-STATE
            (P-PC STATE)
            (P-CTRL-STK STATE)
            (P-TEMP-STK STATE)
            (LET ((P (P-CURRENT-PROGRAM STATE)))
                 (APPEND (LIST (NAME P)
                               (FORMAL-VARS P)
                               (TEMP-VAR-DCLS P))
                         (MARK-INSTR (PROGRAM-BODY P)
                                     (OFFSET (P-PC STATE)))))
            (FIX-DATA-SEGMENT (P-DATA-SEGMENT STATE))
            (P-PSW STATE)))

     Observe that (LISTP (PPS STATE)) is a theorem.




[ 0.0 0.0 0.0 ]

PPS


(DEFN LR-NODIFY-TAG
      (TAG)
      (COND ((EQUAL (UNTAG TAG) (LR-FALSE-TAG))
             'FALSE)
            ((EQUAL (UNTAG TAG) (LR-TRUE-TAG))
             'TRUE)
            ((EQUAL (UNTAG TAG) (LR-ADD1-TAG))
             'ADD1)
            ((EQUAL (UNTAG TAG) (LR-CONS-TAG))
             'CONS)
            ((EQUAL (UNTAG TAG) (LR-PACK-TAG))
             'PACK)
            (T 'UNKNOWN)))

     From the definition we can conclude that (LITATOM (LR-NODIFY-TAG TAG)) is
a theorem.




[ 0.0 0.0 0.0 ]

LR-NODIFY-TAG


(DEFN LR-NODIFY
      (NUMBER NODES FINAL)
      (IF (LISTP NODES)
          (CONS (LIST 'NODE
                      NUMBER
                      (LR-NODIFY-TAG (CAR NODES))
                      (CADDR NODES)
                      (CADDDR NODES))
                (LR-NODIFY (PLUS NUMBER (LR-NODE-SIZE))
                           (CDDDDR NODES)
                           FINAL))
          FINAL))

     Linear arithmetic and the lemmas CDR-LESSEQP and CDR-LESSP inform us that
the measure (COUNT NODES) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, LR-NODIFY is accepted under the
principle of definition.  From the definition we can conclude that:
      (OR (LISTP (LR-NODIFY NUMBER NODES FINAL))
          (EQUAL (LR-NODIFY NUMBER NODES FINAL)
                 FINAL))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-NODIFY


(DEFN LR-FIX-DATA-SEGMENT
     (DATA-SEG)
     (PUT-VALUE (LR-NODIFY 0
                           (FIRSTN (OFFSET (LR-FETCH-FP DATA-SEG))
                                   (VALUE (LR-HEAP-NAME) DATA-SEG))
                           (DIFFERENCE (LENGTH (VALUE (LR-HEAP-NAME) DATA-SEG))
                                       (OFFSET (LR-FETCH-FP DATA-SEG))))
                (LR-HEAP-NAME)
                DATA-SEG))

     Observe that:
      (OR (LISTP (LR-FIX-DATA-SEGMENT DATA-SEG))
          (EQUAL (LR-FIX-DATA-SEGMENT DATA-SEG)
                 DATA-SEG))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-FIX-DATA-SEGMENT


(DEFN LRPS
      (STATE)
      (P-STATE (P-PC STATE)
               (P-CTRL-STK STATE)
               (P-TEMP-STK STATE)
               (P-PROG-SEGMENT STATE)
               (LR-FIX-DATA-SEGMENT (P-DATA-SEGMENT STATE))
               (P-MAX-CTRL-STK-SIZE STATE)
               (P-MAX-TEMP-STK-SIZE STATE)
               (P-WORD-SIZE STATE)
               (P-PSW STATE)))

     Observe that (P-STATEP (LRPS STATE)) is a theorem.




[ 0.0 0.0 0.0 ]

LRPS


(DEFN LR-ABS
    (ADDR DATA-SEG N)
    (IF (ZEROP N)
        NIL
        (LET ((TAG (UNTAG (FETCH ADDR DATA-SEG))))
             (COND ((EQUAL TAG (LR-FALSE-TAG)) F)
                   ((EQUAL TAG (LR-TRUE-TAG)) T)
                   ((EQUAL TAG (LR-ADD1-TAG))
                    (UNTAG (FETCH (ADD-ADDR ADDR (LR-UNBOX-NAT-OFFSET))
                                  DATA-SEG)))
                   ((EQUAL TAG (LR-CONS-TAG))
                    (CONS (LR-ABS (FETCH (ADD-ADDR ADDR (LR-CAR-OFFSET))
                                         DATA-SEG)
                                  DATA-SEG
                                  (SUB1 N))
                          (LR-ABS (FETCH (ADD-ADDR ADDR (LR-CDR-OFFSET))
                                         DATA-SEG)
                                  DATA-SEG
                                  (SUB1 N))))
                   ((EQUAL TAG (LR-PACK-TAG))
                    (PACK (LR-ABS (FETCH (ADD-ADDR ADDR (LR-UNPACK-OFFSET))
                                         DATA-SEG)
                                  DATA-SEG
                                  (SUB1 N))))
                   (T (MINUS (UNTAG (FETCH (ADD-ADDR ADDR
                                                     (LR-NEGATIVE-GUTS-OFFSET))
                                           DATA-SEG))))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of
LR-CONS-TAG, LR-ADD1-TAG, LR-TRUE-TAG, LR-FALSE-TAG, ZEROP, and LR-PACK-TAG
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, LR-ABS is accepted
under the principle of definition.




[ 0.0 0.0 0.0 ]

LR-ABS


(DEFN TOP-STK
      (P-OR-P-STATE)
      (LET ((TEMP-STK (IF (P-STATEP P-OR-P-STATE)
                          (P-TEMP-STK P-OR-P-STATE)
                          (P-TEMP-STK P-OR-P-STATE)))
            (DATA-SEGMENT (IF (P-STATEP P-OR-P-STATE)
                              (P-DATA-SEGMENT P-OR-P-STATE)
                              (P-DATA-SEGMENT P-OR-P-STATE))))
           (LR-ABS (TOP TEMP-STK)
                   DATA-SEGMENT 1000)))

   




[ 0.0 0.0 0.0 ]

TOP-STK


(DEFN LR-MAKE-PROGRAM
      (NAME FORMALS TEMPS BODY)
      (CONS NAME
            (CONS FORMALS (CONS TEMPS BODY))))

     From the definition we can conclude that:
      (LISTP (LR-MAKE-PROGRAM NAME FORMALS TEMPS BODY))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-PROGRAM


(DEFN ASCII-0 NIL 48)

     From the definition we can conclude that (NUMBERP (ASCII-0)) is a theorem.




[ 0.0 0.0 0.0 ]

ASCII-0


(DEFN ASCII-1 NIL 49)

     From the definition we can conclude that (NUMBERP (ASCII-1)) is a theorem.




[ 0.0 0.0 0.0 ]

ASCII-1


(DEFN ASCII-9 NIL 57)

     From the definition we can conclude that (NUMBERP (ASCII-9)) is a theorem.




[ 0.0 0.0 0.0 ]

ASCII-9


(DEFN ASCII-DASH NIL 45)

     From the definition we can conclude that (NUMBERP (ASCII-DASH)) is a
theorem.




[ 0.0 0.0 0.0 ]

ASCII-DASH


(DEFN LIST-ASCII-0 NIL
      (LIST (ASCII-0)))

     Observe that (LISTP (LIST-ASCII-0)) is a theorem.




[ 0.0 0.0 0.0 ]

LIST-ASCII-0


(DEFN LIST-ASCII-1 NIL
      (LIST (ASCII-1)))

     Observe that (LISTP (LIST-ASCII-1)) is a theorem.




[ 0.0 0.0 0.0 ]

LIST-ASCII-1


(DEFN INCREMENT-NUMLIST
      (NUMLIST)
      (IF (LISTP NUMLIST)
          (IF (EQUAL (CAR NUMLIST) (ASCII-9))
              (CONS (ASCII-0)
                    (INCREMENT-NUMLIST (CDR NUMLIST)))
              (CONS (ADD1 (CAR NUMLIST))
                    (CDR NUMLIST)))
          (LIST-ASCII-1)))

     Linear arithmetic and the lemma CDR-LESSP can be used to show that the
measure (COUNT NUMLIST) decreases according to the well-founded relation LESSP
in each recursive call.  Hence, INCREMENT-NUMLIST is accepted under the
definitional principle.  Note that (LISTP (INCREMENT-NUMLIST NUMLIST)) is a
theorem.




[ 0.0 0.0 0.0 ]

INCREMENT-NUMLIST


(DEFN MAKE-SYMBOL
      (INITIAL DIGIT-LIST)
      (PACK (APPEND (APPEND INITIAL DIGIT-LIST)
                    0)))

     Note that (LITATOM (MAKE-SYMBOL INITIAL DIGIT-LIST)) is a theorem.




[ 0.0 0.0 0.0 ]

MAKE-SYMBOL


(DISABLE MAKE-SYMBOL)

[ 0.0 0.0 0.0 ]

MAKE-SYMBOL-OFF


(DEFN COUNT-CODELIST1
      (NUMLIST)
      (IF (LISTP NUMLIST)
          (PLUS (CAR NUMLIST)
                (TIMES 10
                       (COUNT-CODELIST1 (CDR NUMLIST))))
          0))

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




[ 0.0 0.0 0.0 ]

COUNT-CODELIST1


(DEFN SUBSEQP
      (LIST1 LIST2)
      (AND (NOT (LESSP (LENGTH LIST2) (LENGTH LIST1)))
           (EQUAL (FIRSTN (LENGTH LIST1) LIST2)
                  LIST1)))

     Observe that:
      (OR (FALSEP (SUBSEQP LIST1 LIST2))
          (TRUEP (SUBSEQP LIST1 LIST2)))
is a theorem.




[ 0.0 0.0 0.0 ]

SUBSEQP


(DISABLE SUBSEQP)

[ 0.0 0.0 0.0 ]

SUBSEQP-OFF


(DEFN COUNT-CODELIST
      (INITIAL ASCII-LIST)
      (IF (SUBSEQP INITIAL ASCII-LIST)
          (COUNT-CODELIST1 (RESTN (LENGTH INITIAL) ASCII-LIST))
          0))

     Note that (NUMBERP (COUNT-CODELIST INITIAL ASCII-LIST)) is a theorem.




[ 0.0 0.0 0.0 ]

COUNT-CODELIST


(DISABLE COUNT-CODELIST)

[ 0.0 0.0 0.0 ]

COUNT-CODELIST-OFF


(DEFN MAX-COUNT-CODELIST
      (INITIAL LIST)
      (IF (LISTP LIST)
          (MAX (COUNT-CODELIST INITIAL
                               (UNPACK (CAR LIST)))
               (MAX-COUNT-CODELIST INITIAL
                                   (CDR LIST)))
          0))

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




[ 0.0 0.0 0.0 ]

MAX-COUNT-CODELIST


(PROVE-LEMMA INCREMENT-NUM-LIST-COUNT-CODE-LIST1
             (REWRITE)
             (LESSP (COUNT-CODELIST1 NUM-LIST)
                    (COUNT-CODELIST1 (INCREMENT-NUMLIST NUM-LIST)))
             ((DISABLE PLUS-ADD1-ARG1)))

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



     Give the conjecture the name *1.


     We will appeal to induction.  Two 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 (AND (LISTP NUM-LIST)
                         (EQUAL (CAR NUM-LIST) (ASCII-9))
                         (p (CDR NUM-LIST)))
                    (p NUM-LIST))
           (IMPLIES (AND (LISTP NUM-LIST)
                         (NOT (EQUAL (CAR NUM-LIST) (ASCII-9))))
                    (p NUM-LIST))
           (IMPLIES (NOT (LISTP NUM-LIST))
                    (p NUM-LIST))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT NUM-LIST) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme produces the
following three new conjectures:

Case 3. (IMPLIES
             (AND (LISTP NUM-LIST)
                  (EQUAL (CAR NUM-LIST) (ASCII-9))
                  (LESSP (COUNT-CODELIST1 (CDR NUM-LIST))
                         (COUNT-CODELIST1 (INCREMENT-NUMLIST (CDR NUM-LIST)))))
             (LESSP (COUNT-CODELIST1 NUM-LIST)
                    (COUNT-CODELIST1 (INCREMENT-NUMLIST NUM-LIST)))).

  This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  functions ASCII-9, COUNT-CODELIST1, INCREMENT-NUMLIST, EQUAL, and ASCII-0,
  to:

        (IMPLIES
         (AND (LISTP NUM-LIST)
              (EQUAL (CAR NUM-LIST) 57)
              (LESSP (COUNT-CODELIST1 (CDR NUM-LIST))
                     (COUNT-CODELIST1 (INCREMENT-NUMLIST (CDR NUM-LIST)))))
         (LESSP
          (PLUS 57
                (TIMES 10
                       (COUNT-CODELIST1 (CDR NUM-LIST))))
          (PLUS 48
               (TIMES 10
                      (COUNT-CODELIST1 (INCREMENT-NUMLIST (CDR NUM-LIST))))))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (LISTP NUM-LIST)
                      (NOT (EQUAL (CAR NUM-LIST) (ASCII-9))))
                 (LESSP (COUNT-CODELIST1 NUM-LIST)
                        (COUNT-CODELIST1 (INCREMENT-NUMLIST NUM-LIST)))),

  which simplifies, applying COMMUTATIVITY-OF-PLUS, SUB1-ADD1, CDR-CONS,
  CAR-CONS, EQUAL-PLUS-0, and EQUAL-TIMES-0, and unfolding the definitions of
  ASCII-9, COUNT-CODELIST1, INCREMENT-NUMLIST, PLUS, NUMBERP, EQUAL, and LESSP,
  to the following three new conjectures:

  Case 2.3.
          (IMPLIES
                  (AND (LISTP NUM-LIST)
                       (NOT (EQUAL (CAR NUM-LIST) 57))
                       (NOT (EQUAL (CAR NUM-LIST) 0))
                       (NUMBERP (CAR NUM-LIST)))
                  (LESSP (SUB1 (PLUS (CAR NUM-LIST)
                                     (TIMES 10
                                            (COUNT-CODELIST1 (CDR NUM-LIST)))))
                         (PLUS (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               (CAR NUM-LIST)))).

    However this again simplifies, using linear arithmetic, to the formula:

          (IMPLIES
                  (AND (EQUAL (PLUS (CAR NUM-LIST)
                                    (TIMES 10
                                           (COUNT-CODELIST1 (CDR NUM-LIST))))
                              0)
                       (LISTP NUM-LIST)
                       (NOT (EQUAL (CAR NUM-LIST) 57))
                       (NOT (EQUAL (CAR NUM-LIST) 0))
                       (NUMBERP (CAR NUM-LIST)))
                  (LESSP (SUB1 (PLUS (CAR NUM-LIST)
                                     (TIMES 10
                                            (COUNT-CODELIST1 (CDR NUM-LIST)))))
                         (PLUS (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               (CAR NUM-LIST)))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 2.2.
          (IMPLIES
                  (AND (LISTP NUM-LIST)
                       (NOT (EQUAL (CAR NUM-LIST) 57))
                       (NOT (EQUAL (COUNT-CODELIST1 (CDR NUM-LIST))
                                   0))
                       (NUMBERP (CAR NUM-LIST)))
                  (LESSP (SUB1 (PLUS (CAR NUM-LIST)
                                     (TIMES 10
                                            (COUNT-CODELIST1 (CDR NUM-LIST)))))
                         (PLUS (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               (CAR NUM-LIST)))),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES
                  (AND (EQUAL (PLUS (CAR NUM-LIST)
                                    (TIMES 10
                                           (COUNT-CODELIST1 (CDR NUM-LIST))))
                              0)
                       (LISTP NUM-LIST)
                       (NOT (EQUAL (CAR NUM-LIST) 57))
                       (NOT (EQUAL (COUNT-CODELIST1 (CDR NUM-LIST))
                                   0))
                       (NUMBERP (CAR NUM-LIST)))
                  (LESSP (SUB1 (PLUS (CAR NUM-LIST)
                                     (TIMES 10
                                            (COUNT-CODELIST1 (CDR NUM-LIST)))))
                         (PLUS (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               (CAR NUM-LIST)))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES
                  (AND (LISTP NUM-LIST)
                       (NOT (EQUAL (CAR NUM-LIST) 57))
                       (NOT (NUMBERP (CAR NUM-LIST)))
                       (NOT (EQUAL (COUNT-CODELIST1 (CDR NUM-LIST))
                                   0)))
                  (LESSP (SUB1 (PLUS (CAR NUM-LIST)
                                     (TIMES 10
                                            (COUNT-CODELIST1 (CDR NUM-LIST)))))
                         (PLUS (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               0))),

    which again simplifies, rewriting with PLUS-ZERO-ARG2, and opening up the
    definitions of PLUS and ZEROP, to the new conjecture:

          (IMPLIES (AND (LISTP NUM-LIST)
                        (NOT (NUMBERP (CAR NUM-LIST)))
                        (NOT (EQUAL (COUNT-CODELIST1 (CDR NUM-LIST))
                                    0)))
                   (LESSP (SUB1 (TIMES 10
                                       (COUNT-CODELIST1 (CDR NUM-LIST))))
                          (TIMES 10
                                 (COUNT-CODELIST1 (CDR NUM-LIST))))),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (EQUAL (TIMES 10
                                      (COUNT-CODELIST1 (CDR NUM-LIST)))
                               0)
                        (LISTP NUM-LIST)
                        (NOT (NUMBERP (CAR NUM-LIST)))
                        (NOT (EQUAL (COUNT-CODELIST1 (CDR NUM-LIST))
                                    0)))
                   (LESSP (SUB1 (TIMES 10
                                       (COUNT-CODELIST1 (CDR NUM-LIST))))
                          (TIMES 10
                                 (COUNT-CODELIST1 (CDR NUM-LIST))))).

    However this again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (NOT (LISTP NUM-LIST))
                 (LESSP (COUNT-CODELIST1 NUM-LIST)
                        (COUNT-CODELIST1 (INCREMENT-NUMLIST NUM-LIST)))),

  which simplifies, opening up COUNT-CODELIST1, INCREMENT-NUMLIST,
  LIST-ASCII-1, and LESSP, to:

        T.


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


[ 0.0 0.1 0.0 ]

INCREMENT-NUM-LIST-COUNT-CODE-LIST1


(PROVE-LEMMA SUBSEQP-APPEND
             (REWRITE)
             (SUBSEQP (PLIST X)
                      (APPEND X ANYTHING))
             ((ENABLE SUBSEQP)))

This conjecture can be simplified, using the abbreviations NOT, LENGTH-PLIST,
LENGTH-APPEND, and SUBSEQP, to two new conjectures:

Case 2. (NOT (LESSP (PLUS (LENGTH X) (LENGTH ANYTHING))
                    (LENGTH X))),

  which simplifies, using linear arithmetic, to:

        T.

Case 1. (EQUAL (FIRSTN (LENGTH X)
                       (APPEND X ANYTHING))
               (PLIST X)),

  which simplifies, applying DIFFERENCE-X-X, FIRSTN-0, APPEND-NIL,
  FIRSTN-WITH-LARGE-INDEX, and FIRSTN-APPEND, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUBSEQP-APPEND


(PROVE-LEMMA COUNT-CODELIST-MAKE-SYMBOL
             (REWRITE)
             (IMPLIES (EQUAL X
                             (MAKE-SYMBOL INITIAL NUM-LIST))
                      (EQUAL (COUNT-CODELIST (PLIST INITIAL)
                                             (UNPACK X))
                             (COUNT-CODELIST1 NUM-LIST)))
             ((ENABLE COUNT-CODELIST MAKE-SYMBOL)))

WARNING:  Note that COUNT-CODELIST-MAKE-SYMBOL contains the free variable
NUM-LIST which will be chosen by instantiating the hypothesis:
      (EQUAL X
             (MAKE-SYMBOL INITIAL NUM-LIST)).



This formula can be simplified, using the abbreviations IMPLIES,
ASSOCIATIVITY-OF-APPEND, and MAKE-SYMBOL, to:

      (IMPLIES (EQUAL X
                      (PACK (APPEND INITIAL (APPEND NUM-LIST 0))))
               (EQUAL (COUNT-CODELIST (PLIST INITIAL)
                                      (UNPACK X))
                      (COUNT-CODELIST1 NUM-LIST))),

which simplifies, rewriting with UNPACK-PACK, APPEND-LASTCDR-ARG1,
RESTN-WITH-LARGE-INDEX, RESTN-APPEND, RESTN-0, DIFFERENCE-X-X, LENGTH-PLIST,
and SUBSEQP-APPEND, and expanding the functions LESSP, EQUAL, and
COUNT-CODELIST, to:

      (EQUAL (COUNT-CODELIST1 (APPEND NUM-LIST 0))
             (COUNT-CODELIST1 NUM-LIST)),

which we will name *1.


     We will appeal to induction.  Two 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 (AND (LISTP NUM-LIST)
                         (p (CDR NUM-LIST)))
                    (p NUM-LIST))
           (IMPLIES (NOT (LISTP NUM-LIST))
                    (p NUM-LIST))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT NUM-LIST) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme produces the
following two new goals:

Case 2. (IMPLIES (AND (LISTP NUM-LIST)
                      (EQUAL (COUNT-CODELIST1 (APPEND (CDR NUM-LIST) 0))
                             (COUNT-CODELIST1 (CDR NUM-LIST))))
                 (EQUAL (COUNT-CODELIST1 (APPEND NUM-LIST 0))
                        (COUNT-CODELIST1 NUM-LIST))).

  This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  definitions of APPEND and COUNT-CODELIST1, to:

        T.

Case 1. (IMPLIES (NOT (LISTP NUM-LIST))
                 (EQUAL (COUNT-CODELIST1 (APPEND NUM-LIST 0))
                        (COUNT-CODELIST1 NUM-LIST))),

  which simplifies, rewriting with APPEND-LEFT-ID, and expanding the
  definitions of COUNT-CODELIST1 and EQUAL, to:

        T.


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


[ 0.0 0.0 0.0 ]

COUNT-CODELIST-MAKE-SYMBOL


(PROVE-LEMMA MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST
             (REWRITE)
             (IMPLIES (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST)
                      (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                      ATOM-LIST)
                                  (COUNT-CODELIST1 NUM-LIST))))
             ((EXPAND (MAX-COUNT-CODELIST (PLIST INITIAL)
                                          ATOM-LIST))))

WARNING:  When the linear lemma MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST is
stored under (MAX-COUNT-CODELIST (PLIST INITIAL) ATOM-LIST) it contains the
free variable NUM-LIST which will be chosen by instantiating the hypothesis:
      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
              ATOM-LIST).



WARNING:  When the linear lemma MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST is
stored under (COUNT-CODELIST1 NUM-LIST) it contains the free variables
ATOM-LIST and INITIAL which will be chosen by instantiating the hypothesis:
      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
              ATOM-LIST).



WARNING:  Note that the proposed lemma MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST
is to be stored as zero type prescription rules, zero compound recognizer
rules, two linear rules, and zero replacement rules.


This simplifies, unfolding the functions MAX-COUNT-CODELIST and MAX, to the
following three new formulas:

Case 3. (IMPLIES (AND (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST)
                      (NOT (LISTP ATOM-LIST)))
                 (NOT (LESSP 0
                             (COUNT-CODELIST1 NUM-LIST)))).

  But this again simplifies, appealing to the lemma MEMBER-NON-LIST, to:

        T.

Case 2. (IMPLIES (AND (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST)
                      (LISTP ATOM-LIST)
                      (LESSP (COUNT-CODELIST (PLIST INITIAL)
                                             (UNPACK (CAR ATOM-LIST)))
                             (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 (CDR ATOM-LIST))))
                 (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 (CDR ATOM-LIST))
                             (COUNT-CODELIST1 NUM-LIST)))).

  Applying the lemma APPEND-PLIST-LASTCDR, replace INITIAL by (APPEND X Z) to
  eliminate (PLIST INITIAL) and (LASTCDR INITIAL).  We use PLISTP-LASTCDR,
  LENGTH-LASTCDR, PLISTP-PLIST, and LENGTH-PLIST to restrict the new variables.
  We thus obtain:

        (IMPLIES (AND (EQUAL (LENGTH X)
                             (LENGTH (APPEND X Z)))
                      (PLISTP X)
                      (EQUAL (LENGTH Z) 0)
                      (EQUAL (PLISTP Z)
                             (PLISTP (APPEND X Z)))
                      (MEMBER (MAKE-SYMBOL (APPEND X Z) NUM-LIST)
                              ATOM-LIST)
                      (LISTP ATOM-LIST)
                      (LESSP (COUNT-CODELIST X
                                             (UNPACK (CAR ATOM-LIST)))
                             (MAX-COUNT-CODELIST X
                                                 (CDR ATOM-LIST))))
                 (NOT (LESSP (MAX-COUNT-CODELIST X (CDR ATOM-LIST))
                             (COUNT-CODELIST1 NUM-LIST)))),

  which further simplifies, applying the lemmas PLUS-ZERO-ARG2, LENGTH-APPEND,
  EQUAL-LENGTH-0, PLISTP-NLISTP, and PLISTP-APPEND, and expanding the
  definition of ZEROP, to:

        (IMPLIES (AND (PLISTP X)
                      (NOT (LISTP Z))
                      (MEMBER (MAKE-SYMBOL (APPEND X Z) NUM-LIST)
                              ATOM-LIST)
                      (LISTP ATOM-LIST)
                      (LESSP (COUNT-CODELIST X
                                             (UNPACK (CAR ATOM-LIST)))
                             (MAX-COUNT-CODELIST X
                                                 (CDR ATOM-LIST))))
                 (NOT (LESSP (MAX-COUNT-CODELIST X (CDR ATOM-LIST))
                             (COUNT-CODELIST1 NUM-LIST)))).

  Appealing to the lemmas CAR-CDR-ELIM and UNPACK-ELIM, we now replace
  ATOM-LIST by (CONS V W) to eliminate (CAR ATOM-LIST) and (CDR ATOM-LIST) and
  V by (PACK D) to eliminate (UNPACK V).  The result is two new formulas:

  Case 2.2.
          (IMPLIES (AND (NOT (LITATOM V))
                        (PLISTP X)
                        (NOT (LISTP Z))
                        (MEMBER (MAKE-SYMBOL (APPEND X Z) NUM-LIST)
                                (CONS V W))
                        (LESSP (COUNT-CODELIST X (UNPACK V))
                               (MAX-COUNT-CODELIST X W)))
                   (NOT (LESSP (MAX-COUNT-CODELIST X W)
                               (COUNT-CODELIST1 NUM-LIST)))),

    which further simplifies, applying the lemmas CDR-CONS, CAR-CONS, and
    UNPACK-NLITATOM, and opening up the definition of MEMBER, to the
    conjecture:

          (IMPLIES (AND (NOT (LITATOM V))
                        (PLISTP X)
                        (NOT (LISTP Z))
                        (MEMBER (MAKE-SYMBOL (APPEND X Z) NUM-LIST)
                                W)
                        (LESSP (COUNT-CODELIST X 0)
                               (MAX-COUNT-CODELIST X W)))
                   (NOT (LESSP (MAX-COUNT-CODELIST X W)
                               (COUNT-CODELIST1 NUM-LIST)))),

    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 (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                 ATOM-LIST)
         (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                         ATOM-LIST)
                     (COUNT-CODELIST1 NUM-LIST)))),

which we named *1 above.  We will appeal to induction.  Two 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 (NLISTP ATOM-LIST)
                    (p INITIAL ATOM-LIST NUM-LIST))
           (IMPLIES (AND (NOT (NLISTP ATOM-LIST))
                         (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                                (CAR ATOM-LIST)))
                    (p INITIAL ATOM-LIST NUM-LIST))
           (IMPLIES (AND (NOT (NLISTP ATOM-LIST))
                         (NOT (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                                     (CAR ATOM-LIST)))
                         (p INITIAL (CDR ATOM-LIST) NUM-LIST))
                    (p INITIAL ATOM-LIST NUM-LIST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT ATOM-LIST) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  The above induction scheme produces four new goals:

Case 4. (IMPLIES (AND (NLISTP ATOM-LIST)
                      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST))
                 (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 ATOM-LIST)
                             (COUNT-CODELIST1 NUM-LIST)))),

  which simplifies, applying MEMBER-NON-LIST, and opening up NLISTP, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP ATOM-LIST))
                      (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                             (CAR ATOM-LIST))
                      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST))
                 (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 ATOM-LIST)
                             (COUNT-CODELIST1 NUM-LIST)))).

  This simplifies, applying COUNT-CODELIST-MAKE-SYMBOL, and unfolding the
  functions NLISTP, MEMBER, MAX-COUNT-CODELIST, and MAX, to two new
  conjectures:

  Case 3.2.
          (IMPLIES (AND (LISTP ATOM-LIST)
                        (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                               (CAR ATOM-LIST))
                        (NOT (LESSP (COUNT-CODELIST1 NUM-LIST)
                                    (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                        (CDR ATOM-LIST)))))
                   (NOT (LESSP (COUNT-CODELIST1 NUM-LIST)
                               (COUNT-CODELIST1 NUM-LIST)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP ATOM-LIST)
                        (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                               (CAR ATOM-LIST))
                        (LESSP (COUNT-CODELIST1 NUM-LIST)
                               (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                   (CDR ATOM-LIST))))
                   (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                   (CDR ATOM-LIST))
                               (COUNT-CODELIST1 NUM-LIST)))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 2. (IMPLIES (AND (NOT (NLISTP ATOM-LIST))
                      (NOT (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                                  (CAR ATOM-LIST)))
                      (NOT (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                                   (CDR ATOM-LIST)))
                      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST))
                 (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 ATOM-LIST)
                             (COUNT-CODELIST1 NUM-LIST)))),

  which simplifies, unfolding the definitions of NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP ATOM-LIST))
                      (NOT (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                                  (CAR ATOM-LIST)))
                      (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                      (CDR ATOM-LIST))
                                  (COUNT-CODELIST1 NUM-LIST)))
                      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST))
                 (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                 ATOM-LIST)
                             (COUNT-CODELIST1 NUM-LIST)))),

  which simplifies, opening up NLISTP, MEMBER, MAX-COUNT-CODELIST, and MAX, to:

        (IMPLIES (AND (LISTP ATOM-LIST)
                      (NOT (EQUAL (MAKE-SYMBOL INITIAL NUM-LIST)
                                  (CAR ATOM-LIST)))
                      (NOT (LESSP (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                      (CDR ATOM-LIST))
                                  (COUNT-CODELIST1 NUM-LIST)))
                      (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              (CDR ATOM-LIST))
                      (NOT (LESSP (COUNT-CODELIST (PLIST INITIAL)
                                                  (UNPACK (CAR ATOM-LIST)))
                                  (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                      (CDR ATOM-LIST)))))
                 (NOT (LESSP (COUNT-CODELIST (PLIST INITIAL)
                                             (UNPACK (CAR ATOM-LIST)))
                             (COUNT-CODELIST1 NUM-LIST)))).

  This again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.1 0.1 ]

MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST


(DEFN GENSYM
      (INITIAL NUM-LIST ATOM-LIST)
      (IF (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                  ATOM-LIST)
          (GENSYM INITIAL
                  (INCREMENT-NUMLIST NUM-LIST)
                  ATOM-LIST)
          (CONS (MAKE-SYMBOL INITIAL NUM-LIST)
                (INCREMENT-NUMLIST NUM-LIST)))
      ((LESSP (DIFFERENCE (ADD1 (MAX-COUNT-CODELIST (PLIST INITIAL)
                                                    ATOM-LIST))
                          (COUNT-CODELIST1 NUM-LIST)))))

     Linear arithmetic, the lemmas INCREMENT-NUM-LIST-COUNT-CODE-LIST1,
DIFFERENCE-SUB1-ARG2, DIFFERENCE-LEQ-ARG1, SUB1-ADD1, and
MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST, and the definitions of EQUAL,
DIFFERENCE, and LESSP establish that the measure:
      (DIFFERENCE (ADD1 (MAX-COUNT-CODELIST (PLIST INITIAL)
                                            ATOM-LIST))
                  (COUNT-CODELIST1 NUM-LIST))
decreases according to the well-founded relation LESSP in each recursive call.
Hence, GENSYM is accepted under the definitional principle.  Note that:
      (LISTP (GENSYM INITIAL NUM-LIST ATOM-LIST))
is a theorem.




[ 0.0 0.1 0.0 ]

GENSYM


(PROVE-LEMMA GENSYM-IS-NEW
             (REWRITE)
             (NOT (MEMBER (CAR (GENSYM INITIAL NUM-LIST ATOM-LIST))
                          ATOM-LIST)))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  There are two plausible inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                                 ATOM-LIST)
                         (p INITIAL
                            (INCREMENT-NUMLIST NUM-LIST)
                            ATOM-LIST))
                    (p INITIAL NUM-LIST ATOM-LIST))
           (IMPLIES (NOT (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                                 ATOM-LIST))
                    (p INITIAL NUM-LIST ATOM-LIST))).
Linear arithmetic, the lemmas INCREMENT-NUM-LIST-COUNT-CODE-LIST1,
DIFFERENCE-SUB1-ARG2, DIFFERENCE-LEQ-ARG1, SUB1-ADD1, and
MEMBER-MAKE-SYMBOL-MAX-COUNT-CODE-LIST, and the definitions of EQUAL,
DIFFERENCE, and LESSP establish that the measure:
      (DIFFERENCE (ADD1 (MAX-COUNT-CODELIST (PLIST INITIAL)
                                            ATOM-LIST))
                  (COUNT-CODELIST1 NUM-LIST))
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces the following two new
goals:

Case 2. (IMPLIES (AND (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST)
                      (NOT (MEMBER (CAR (GENSYM INITIAL
                                                (INCREMENT-NUMLIST NUM-LIST)
                                                ATOM-LIST))
                                   ATOM-LIST)))
                 (NOT (MEMBER (CAR (GENSYM INITIAL NUM-LIST ATOM-LIST))
                              ATOM-LIST))).

  This simplifies, expanding GENSYM, to:

        T.

Case 1. (IMPLIES (NOT (MEMBER (MAKE-SYMBOL INITIAL NUM-LIST)
                              ATOM-LIST))
                 (NOT (MEMBER (CAR (GENSYM INITIAL NUM-LIST ATOM-LIST))
                              ATOM-LIST))).

  This simplifies, rewriting with CAR-CONS, and unfolding the definition of
  GENSYM, to:

        T.


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


[ 0.0 0.0 0.0 ]

GENSYM-IS-NEW


(DEFN LR-MAKE-TEMP-NAME-ALIST-1
      (INITIAL NUM-LIST TEMP-LIST FORMALS)
      (IF (LISTP TEMP-LIST)
          (LET ((GENSYM (GENSYM INITIAL NUM-LIST FORMALS)))
               (CONS (CONS (CAR TEMP-LIST) (CAR GENSYM))
                     (LR-MAKE-TEMP-NAME-ALIST-1 INITIAL
                                                (CDR GENSYM)
                                                (CDR TEMP-LIST)
                                                FORMALS)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TEMP-LIST) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, LR-MAKE-TEMP-NAME-ALIST-1 is accepted under the
principle of definition.  Note that:
      (OR (LITATOM (LR-MAKE-TEMP-NAME-ALIST-1 INITIAL NUM-LIST TEMP-LIST
                                              FORMALS))
          (LISTP (LR-MAKE-TEMP-NAME-ALIST-1 INITIAL NUM-LIST TEMP-LIST
                                            FORMALS)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-TEMP-NAME-ALIST-1


(DEFN LR-MAKE-TEMP-NAME-ALIST
      (TEMP-LIST FORMALS)
      (LR-MAKE-TEMP-NAME-ALIST-1 (UNPACK 'T*)
                                 (LIST-ASCII-0)
                                 TEMP-LIST FORMALS))

     Note that:
      (OR (LITATOM (LR-MAKE-TEMP-NAME-ALIST TEMP-LIST FORMALS))
          (LISTP (LR-MAKE-TEMP-NAME-ALIST TEMP-LIST FORMALS)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-TEMP-NAME-ALIST


(DEFN LR-NEW-CONS
      (CAR CDR)
      (LR-NEW-NODE (TAG 'NAT (LR-CONS-TAG))
                   (TAG 'NAT 1)
                   CAR CDR))

     Note that (LISTP (LR-NEW-CONS CAR CDR)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-NEW-CONS


(DEFN DEPOSIT-A-LIST
      (LIST ADDR DATA-SEG)
      (IF (LISTP LIST)
          (DEPOSIT (CAR LIST)
                   ADDR
                   (DEPOSIT-A-LIST (CDR LIST)
                                   (ADD1-ADDR ADDR)
                                   DATA-SEG))
          DATA-SEG))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LIST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, DEPOSIT-A-LIST is accepted under the principle of
definition.  Note that:
      (OR (LISTP (DEPOSIT-A-LIST LIST ADDR DATA-SEG))
          (EQUAL (DEPOSIT-A-LIST LIST ADDR DATA-SEG)
                 DATA-SEG))
is a theorem.




[ 0.0 0.0 0.0 ]

DEPOSIT-A-LIST


(DEFN LR-INIT-HEAP-CONTENTS
      (ADDR SIZE)
      (IF (ZEROP SIZE)
          (LIST (TAG 'NAT (LR-INIT-TAG)))
          (APPEND (LR-NEW-NODE (TAG 'NAT (LR-INIT-TAG))
                               (ADD-ADDR ADDR (LR-NODE-SIZE))
                               (TAG 'NAT 0)
                               (TAG 'NAT 0))
                  (LR-INIT-HEAP-CONTENTS (ADD-ADDR ADDR (LR-NODE-SIZE))
                                         (SUB1 SIZE)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT SIZE) decreases according to the
well-founded relation LESSP in each recursive call.  Hence,
LR-INIT-HEAP-CONTENTS is accepted under the principle of definition.  Note
that (LISTP (LR-INIT-HEAP-CONTENTS ADDR SIZE)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-INIT-HEAP-CONTENTS


(DEFN LR-ADD-TO-DATA-SEG
      (DATA-SEG NEW-NODE)
      (IF (NOT (LESSP (SUB1 (LENGTH (VALUE (LR-HEAP-NAME) DATA-SEG)))
                      (PLUS (OFFSET (FETCH (LR-FP-ADDR) DATA-SEG))
                            (LENGTH NEW-NODE))))
          (DEPOSIT (FETCH (ADD-ADDR (FETCH (LR-FP-ADDR) DATA-SEG)
                                    (LR-REF-COUNT-OFFSET))
                          DATA-SEG)
                   (LR-FP-ADDR)
                   (DEPOSIT-A-LIST NEW-NODE
                                   (FETCH (LR-FP-ADDR) DATA-SEG)
                                   DATA-SEG))
          DATA-SEG))

     Note that:
      (OR (LISTP (LR-ADD-TO-DATA-SEG DATA-SEG NEW-NODE))
          (EQUAL (LR-ADD-TO-DATA-SEG DATA-SEG NEW-NODE)
                 DATA-SEG))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-ADD-TO-DATA-SEG


(DEFN LR-INIT-DATA-SEG
 (HEAP-SIZE)
 (DEPOSIT-A-LIST
  (LIST (TAG 'NAT (LR-FALSE-TAG))
        (TAG 'NAT 1)
        (LR-UNDEF-ADDR)
        (LR-UNDEF-ADDR))
  (LR-F-ADDR)
  (DEPOSIT-A-LIST
        (LIST (TAG 'NAT (LR-UNDEFINED-TAG))
              (TAG 'NAT 1)
              (LR-UNDEF-ADDR)
              (LR-UNDEF-ADDR))
        (LR-UNDEF-ADDR)
        (LIST (LIST (AREA-NAME (LR-FP-ADDR))
                    (ADD-ADDR (LR-F-ADDR) (LR-NODE-SIZE)))
              (LIST (AREA-NAME (LR-ANSWER-ADDR))
                    (TAG 'NAT 0))
              (CONS (LR-HEAP-NAME)
                    (LR-INIT-HEAP-CONTENTS (TAG 'ADDR (CONS (LR-HEAP-NAME) 0))
                                           HEAP-SIZE))))))

     Note that (LISTP (LR-INIT-DATA-SEG HEAP-SIZE)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-INIT-DATA-SEG


(DEFN COUNT-LIST
      (FLAG OBJECT)
      (COND ((EQUAL FLAG 'LIST)
             (IF (LISTP OBJECT)
                 (PLUS (COUNT-LIST T (CAR OBJECT))
                       (COUNT-LIST 'LIST (CDR OBJECT)))
                 1))
            ((LISTP OBJECT)
             (ADD1 (ADD1 (PLUS (COUNT-LIST T (CAR OBJECT))
                               (COUNT-LIST T (CDR OBJECT))))))
            ((NUMBERP OBJECT)
             (ADD1 (COUNT OBJECT)))
            (T 1)))

     Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP establish that
the measure (COUNT OBJECT) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, COUNT-LIST is accepted under the
principle of definition.  From the definition we can conclude that:
      (NUMBERP (COUNT-LIST FLAG OBJECT))
is a theorem.




[ 0.0 0.0 0.0 ]

COUNT-LIST


(PROVE-LEMMA NOT-EQUAL-0-COUNT-LIST
             (REWRITE)
             (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0)))


     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 (AND (EQUAL FLAG 'LIST)
                         (LISTP OBJECT)
                         (p 'LIST (CDR OBJECT))
                         (p T (CAR OBJECT)))
                    (p FLAG OBJECT))
           (IMPLIES (AND (EQUAL FLAG 'LIST)
                         (NOT (LISTP OBJECT)))
                    (p FLAG OBJECT))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP OBJECT)
                         (p T (CDR OBJECT))
                         (p T (CAR OBJECT)))
                    (p FLAG OBJECT))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (NOT (LISTP OBJECT))
                         (NUMBERP OBJECT))
                    (p FLAG OBJECT))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (NOT (LISTP OBJECT))
                         (NOT (NUMBERP OBJECT)))
                    (p FLAG OBJECT))).
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP can be used to
establish that the measure (COUNT OBJECT) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instances chosen for FLAG.  The above induction scheme
generates the following five new formulas:

Case 5. (IMPLIES (AND (EQUAL FLAG 'LIST)
                      (LISTP OBJECT)
                      (NOT (EQUAL (COUNT-LIST 'LIST (CDR OBJECT))
                                  0))
                      (NOT (EQUAL (COUNT-LIST T (CAR OBJECT))
                                  0)))
                 (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0))).

  This simplifies, applying EQUAL-PLUS-0, and expanding the functions EQUAL
  and COUNT-LIST, to:

        T.

Case 4. (IMPLIES (AND (EQUAL FLAG 'LIST)
                      (NOT (LISTP OBJECT)))
                 (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0))),

  which simplifies, opening up the functions EQUAL and COUNT-LIST, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                      (LISTP OBJECT)
                      (NOT (EQUAL (COUNT-LIST T (CDR OBJECT)) 0))
                      (NOT (EQUAL (COUNT-LIST T (CAR OBJECT))
                                  0)))
                 (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0))),

  which simplifies, expanding COUNT-LIST, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                      (NOT (LISTP OBJECT))
                      (NUMBERP OBJECT))
                 (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0))),

  which simplifies, applying COUNT-NUMBERP, and unfolding the definition of
  COUNT-LIST, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                      (NOT (LISTP OBJECT))
                      (NOT (NUMBERP OBJECT)))
                 (NOT (EQUAL (COUNT-LIST FLAG OBJECT) 0))).

  This simplifies, opening up the functions COUNT-LIST and EQUAL, to:

        T.


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


[ 0.0 0.0 0.0 ]

NOT-EQUAL-0-COUNT-LIST


(PROVE-LEMMA LESSP-COUNT-LIST-CDR-COUNT-LIST-WHOLE
             (REWRITE)
             (IMPLIES (LISTP OBJECT)
                      (LESSP (COUNT-LIST 'LIST (CDR OBJECT))
                             (COUNT-LIST 'LIST OBJECT))))

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


.

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

      (LESSP (COUNT-LIST 'LIST X)
             (COUNT-LIST 'LIST (CONS Z X))).

This simplifies, applying CDR-CONS, CAR-CONS, CORRECTNESS-OF-CANCEL-LESSP-PLUS,
and NOT-EQUAL-0-COUNT-LIST, and expanding the functions EQUAL, COUNT-LIST, FIX,
ZEROP, and NOT, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-COUNT-LIST-CDR-COUNT-LIST-WHOLE


(PROVE-LEMMA LESSP-COUNT-NOT-LIST-CAR-COUNT-LIST-WHOLE
             (REWRITE)
             (IMPLIES (LISTP OBJECT)
                      (LESSP (COUNT-LIST T (CAR OBJECT))
                             (COUNT-LIST 'LIST OBJECT))))

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


.

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

      (LESSP (COUNT-LIST T X)
             (COUNT-LIST 'LIST (CONS X Z))).

This simplifies, applying CDR-CONS, CAR-CONS, CORRECTNESS-OF-CANCEL-LESSP-PLUS,
and NOT-EQUAL-0-COUNT-LIST, and expanding the functions EQUAL, COUNT-LIST, FIX,
ZEROP, and NOT, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-COUNT-NOT-LIST-CAR-COUNT-LIST-WHOLE


(DEFN LR-COMPILE-QUOTE
 (FLAG OBJECT HEAP TABLE)
 (COND
  ((EQUAL FLAG 'LIST)
   (IF (LISTP OBJECT)
       (LET ((CAR-PAIR (LR-COMPILE-QUOTE T
                                         (CAR OBJECT)
                                         HEAP TABLE)))
            (LR-COMPILE-QUOTE 'LIST
                              (CDR OBJECT)
                              (CAR CAR-PAIR)
                              (CDR CAR-PAIR)))
       (CONS HEAP TABLE)))
  ((DEFINEDP OBJECT TABLE)
   (CONS HEAP TABLE))
  ((LISTP OBJECT)
   (LET
    ((PAIR (LR-COMPILE-QUOTE 'LIST
                             (LIST (CAR OBJECT) (CDR OBJECT))
                             HEAP TABLE)))
    (CONS
       (LR-ADD-TO-DATA-SEG (CAR PAIR)
                           (LR-NEW-CONS (CDR (ASSOC (CAR OBJECT) (CDR PAIR)))
                                        (CDR (ASSOC (CDR OBJECT) (CDR PAIR)))))
       (CONS (CONS OBJECT
                   (FETCH (LR-FP-ADDR) (CAR PAIR)))
             (CDR PAIR)))))
  ((NUMBERP OBJECT)
   (CONS (LR-ADD-TO-DATA-SEG HEAP
                             (LR-NEW-NODE (TAG 'NAT (LR-ADD1-TAG))
                                          (TAG 'NAT 1)
                                          (TAG 'NAT OBJECT)
                                          (LR-UNDEF-ADDR)))
         (CONS (CONS OBJECT
                     (FETCH (LR-FP-ADDR) HEAP))
               TABLE)))
  ((TRUEP OBJECT)
   (CONS (LR-ADD-TO-DATA-SEG HEAP
                             (LR-NEW-NODE (TAG 'NAT (LR-TRUE-TAG))
                                          (TAG 'NAT 1)
                                          (LR-UNDEF-ADDR)
                                          (LR-UNDEF-ADDR)))
         (CONS (CONS OBJECT
                     (FETCH (LR-FP-ADDR) HEAP))
               TABLE)))
  (T (CONS HEAP
           (CONS (CONS OBJECT (LR-UNDEF-ADDR))
                 TABLE))))
 ((LESSP (COUNT-LIST FLAG OBJECT))))

     Linear arithmetic, the lemmas LESSP-COUNT-LIST-CDR-COUNT-LIST-WHOLE,
LESSP-COUNT-NOT-LIST-CAR-COUNT-LIST-WHOLE, NOT-EQUAL-0-COUNT-LIST, SUB1-ADD1,
PLUS-ZERO-ARG2, PLUS-ADD1-ARG2, CAR-CONS, CDR-CONS, and EQUAL-PLUS-0, and the
definitions of LESSP, NUMBERP, ZEROP, COUNT-LIST, and EQUAL can be used to
show that the measure (COUNT-LIST FLAG OBJECT) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, LR-COMPILE-QUOTE
is accepted under the definitional principle.  Observe that:
      (LISTP (LR-COMPILE-QUOTE FLAG OBJECT HEAP TABLE))
is a theorem.




[ 0.3 0.0 0.0 ]

LR-COMPILE-QUOTE


(DEFN LR-DATA-SEG-TABLE-BODY
      (FLAG EXPR DATA-SEG TABLE)
      (COND ((EQUAL FLAG 'LIST)
             (IF (LISTP EXPR)
                 (LET ((DST1 (LR-DATA-SEG-TABLE-BODY T
                                                     (CAR EXPR)
                                                     DATA-SEG TABLE)))
                      (LR-DATA-SEG-TABLE-BODY 'LIST
                                              (CDR EXPR)
                                              (CAR DST1)
                                              (CDR DST1)))
                 (CONS DATA-SEG TABLE)))
            ((LISTP EXPR)
             (COND ((OR (EQUAL (CAR EXPR) (S-TEMP-FETCH))
                        (EQUAL (CAR EXPR) (S-TEMP-EVAL))
                        (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                    (LR-DATA-SEG-TABLE-BODY T
                                            (CADR EXPR)
                                            DATA-SEG TABLE))
                   ((EQUAL (CAR EXPR) 'QUOTE)
                    (LR-COMPILE-QUOTE T
                                      (CADR EXPR)
                                      DATA-SEG TABLE))
                   (T (LR-DATA-SEG-TABLE-BODY 'LIST
                                              (CDR EXPR)
                                              DATA-SEG TABLE))))
            (T (CONS DATA-SEG TABLE))))

     Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, and CAR-LESSEQP
inform us that the measure (COUNT EXPR) decreases according to the
well-founded relation LESSP in each recursive call.  Hence,
LR-DATA-SEG-TABLE-BODY is accepted under the definitional principle.  From the
definition we can conclude that:
      (LISTP (LR-DATA-SEG-TABLE-BODY FLAG EXPR DATA-SEG TABLE))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-DATA-SEG-TABLE-BODY


(DEFN LR-DATA-SEG-TABLE-LIST
  (PROGS DATA-SEG TABLE)
  (IF (LISTP PROGS)
      (LR-DATA-SEG-TABLE-LIST (CDR PROGS)
                              (CAR (LR-DATA-SEG-TABLE-BODY T
                                                           (S-BODY (CAR PROGS))
                                                           DATA-SEG TABLE))
                              (CDR (LR-DATA-SEG-TABLE-BODY T
                                                           (S-BODY (CAR PROGS))
                                                           DATA-SEG TABLE)))
      (CONS DATA-SEG TABLE)))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT PROGS) decreases according to the well-founded relation LESSP
in each recursive call.  Hence, LR-DATA-SEG-TABLE-LIST is accepted under the
principle of definition.  Note that:
      (LISTP (LR-DATA-SEG-TABLE-LIST PROGS DATA-SEG TABLE))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-DATA-SEG-TABLE-LIST


(DEFN LR-INIT-DATA-SEG-TABLE
      (PARAMS DATA-SEG TABLE)
      (IF (LISTP PARAMS)
          (LET ((DS-TAB (LR-COMPILE-QUOTE T
                                          (CDAR PARAMS)
                                          DATA-SEG TABLE)))
               (LR-INIT-DATA-SEG-TABLE (CDR PARAMS)
                                       (CAR DS-TAB)
                                       (CDR DS-TAB)))
          (CONS DATA-SEG TABLE)))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT PARAMS) decreases according to the well-founded relation LESSP
in each recursive call.  Hence, LR-INIT-DATA-SEG-TABLE is accepted under the
principle of definition.  Note that:
      (LISTP (LR-INIT-DATA-SEG-TABLE PARAMS DATA-SEG TABLE))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-INIT-DATA-SEG-TABLE


(DEFN LR-DATA-SEG-TABLE
     (PROGS PARAMS HEAP-SIZE)
     (LET ((INIT-DS-TABLE1 (LR-COMPILE-QUOTE 'LIST
                                             (LIST T 0)
                                             (LR-INIT-DATA-SEG HEAP-SIZE)
                                             (LIST (CONS F (LR-F-ADDR))))))
          (LET ((INIT-DS-TABLE2 (LR-INIT-DATA-SEG-TABLE PARAMS
                                                        (CAR INIT-DS-TABLE1)
                                                        (CDR INIT-DS-TABLE1))))
               (LR-DATA-SEG-TABLE-LIST PROGS
                                       (CAR INIT-DS-TABLE2)
                                       (CDR INIT-DS-TABLE2)))))

     Observe that (LISTP (LR-DATA-SEG-TABLE PROGS PARAMS HEAP-SIZE)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-DATA-SEG-TABLE


(DEFN PAIR-FORMALS-WITH-ADDRESSES
      (FORMALS TABLE)
      (IF (LISTP FORMALS)
          (CONS (CONS (CAAR FORMALS)
                      (CDR (ASSOC (CDAR FORMALS) TABLE)))
                (PAIR-FORMALS-WITH-ADDRESSES (CDR FORMALS)
                                             TABLE))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT FORMALS) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, PAIR-FORMALS-WITH-ADDRESSES is accepted under the
definitional principle.  Observe that:
      (OR (LITATOM (PAIR-FORMALS-WITH-ADDRESSES FORMALS TABLE))
          (LISTP (PAIR-FORMALS-WITH-ADDRESSES FORMALS TABLE)))
is a theorem.




[ 0.0 0.0 0.0 ]

PAIR-FORMALS-WITH-ADDRESSES


(DEFN LR-MAKE-INITIAL-TEMPS
      (TEMP-VARS)
      (IF (LISTP TEMP-VARS)
          (CONS (CONS (CAR TEMP-VARS) (LR-UNDEF-ADDR))
                (LR-MAKE-INITIAL-TEMPS (CDR TEMP-VARS)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TEMP-VARS) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, LR-MAKE-INITIAL-TEMPS is accepted under the
definitional principle.  Note that:
      (OR (LITATOM (LR-MAKE-INITIAL-TEMPS TEMP-VARS))
          (LISTP (LR-MAKE-INITIAL-TEMPS TEMP-VARS)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-INITIAL-TEMPS


(DEFN LR-INITIAL-CSTK
      (PARAMS TEMP-ALIST TABLE PC)
      (LIST (P-FRAME (APPEND (PAIR-FORMALS-WITH-ADDRESSES PARAMS TABLE)
                             (LR-MAKE-INITIAL-TEMPS (STRIP-CDRS TEMP-ALIST)))
                     PC)))

     Observe that (LISTP (LR-INITIAL-CSTK PARAMS TEMP-ALIST TABLE PC)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-INITIAL-CSTK


(DEFN LR-COMPILE-BODY
      (FLAG BODY TEMP-ALIST CONST-TABLE)
      (IF (EQUAL FLAG 'LIST)
          (IF (LISTP BODY)
              (CONS (LR-COMPILE-BODY T
                                     (CAR BODY)
                                     TEMP-ALIST CONST-TABLE)
                    (LR-COMPILE-BODY 'LIST
                                     (CDR BODY)
                                     TEMP-ALIST CONST-TABLE))
              NIL)
          (IF (LISTP BODY)
              (COND ((OR (EQUAL (CAR BODY) (S-TEMP-FETCH))
                         (EQUAL (CAR BODY) (S-TEMP-EVAL))
                         (EQUAL (CAR BODY) (S-TEMP-TEST)))
                     (LIST (CAR BODY)
                           (LR-COMPILE-BODY T
                                            (CADR BODY)
                                            TEMP-ALIST CONST-TABLE)
                           (VALUE (CADR BODY) TEMP-ALIST)))
                    ((EQUAL (CAR BODY) 'QUOTE)
                     (LIST 'QUOTE
                           (VALUE (CADR BODY) CONST-TABLE)))
                    (T (CONS (CAR BODY)
                             (LR-COMPILE-BODY 'LIST
                                              (CDR BODY)
                                              TEMP-ALIST CONST-TABLE))))
              BODY)))

     Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, and CAR-LESSEQP
inform us that the measure (COUNT BODY) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, LR-COMPILE-BODY is
accepted under the principle of definition.  Note that:
      (OR (OR (LITATOM (LR-COMPILE-BODY FLAG BODY TEMP-ALIST CONST-TABLE))
              (LISTP (LR-COMPILE-BODY FLAG BODY TEMP-ALIST CONST-TABLE)))
          (EQUAL (LR-COMPILE-BODY FLAG BODY TEMP-ALIST CONST-TABLE)
                 BODY))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-COMPILE-BODY


(DEFN LR-MAKE-TEMP-VAR-DCLS
      (TEMP-ALIST)
      (IF (LISTP TEMP-ALIST)
          (CONS (LIST (CDAR TEMP-ALIST)
                      (LR-UNDEF-ADDR))
                (LR-MAKE-TEMP-VAR-DCLS (CDR TEMP-ALIST)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT TEMP-ALIST) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, LR-MAKE-TEMP-VAR-DCLS is accepted under the
principle of definition.  Note that:
      (OR (LITATOM (LR-MAKE-TEMP-VAR-DCLS TEMP-ALIST))
          (LISTP (LR-MAKE-TEMP-VAR-DCLS TEMP-ALIST)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-TEMP-VAR-DCLS


(DEFN LR-COMPILE-PROGRAMS
      (PROGRAMS CONST-TABLE)
      (IF (LISTP PROGRAMS)
          (LET ((PROG (CAR PROGRAMS)))
               (LET ((TEMP-ALIST (LR-MAKE-TEMP-NAME-ALIST (S-TEMP-LIST PROG)
                                                          (S-FORMALS PROG))))
                    (CONS (LR-MAKE-PROGRAM (CAR PROG)
                                           (S-FORMALS PROG)
                                           (LR-MAKE-TEMP-VAR-DCLS TEMP-ALIST)
                                           (LR-COMPILE-BODY T
                                                            (S-BODY PROG)
                                                            TEMP-ALIST
                                                            CONST-TABLE))
                          (LR-COMPILE-PROGRAMS (CDR PROGRAMS)
                                               CONST-TABLE))))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP can be used to show that the
measure (COUNT PROGRAMS) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, LR-COMPILE-PROGRAMS is accepted under
the principle of definition.  Note that:
      (OR (LITATOM (LR-COMPILE-PROGRAMS PROGRAMS CONST-TABLE))
          (LISTP (LR-COMPILE-PROGRAMS PROGRAMS CONST-TABLE)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-COMPILE-PROGRAMS


(DEFN LR-P-C-SIZE
      (FLAG EXPR)
      (COND ((EQUAL FLAG 'LIST)
             (IF (LISTP EXPR)
                 (PLUS (LR-P-C-SIZE T (CAR EXPR))
                       (LR-P-C-SIZE 'LIST (CDR EXPR)))
                 0))
            ((LISTP EXPR)
             (COND ((EQUAL (CAR EXPR) 'IF)
                    (PLUS (LR-P-C-SIZE T (CADR EXPR))
                          (LR-P-C-SIZE T (CADDR EXPR))
                          (LR-P-C-SIZE T (CADDDR EXPR))
                          4))
                   ((EQUAL (CAR EXPR) (S-TEMP-FETCH)) 1)
                   ((EQUAL (CAR EXPR) (S-TEMP-EVAL))
                    (PLUS (LR-P-C-SIZE T (CADR EXPR)) 1))
                   ((EQUAL (CAR EXPR) (S-TEMP-TEST))
                    (PLUS (LR-P-C-SIZE T (CADR EXPR)) 7))
                   ((EQUAL (CAR EXPR) 'QUOTE) 1)
                   (T (PLUS (LR-P-C-SIZE 'LIST (CDR EXPR))
                            1))))
            (T 1)))

     Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, CAR-LESSEQP, and
CDR-LESSEQP establish that the measure (COUNT EXPR) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, LR-P-C-SIZE is
accepted under the definitional principle.  Observe that:
      (NUMBERP (LR-P-C-SIZE FLAG EXPR))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-P-C-SIZE


(DEFN LR-P-C-SIZE-LIST
      (N EXPR-LIST)
      (IF (ZEROP N)
          0
          (IF (LESSP N (LENGTH EXPR-LIST))
              (PLUS (LR-P-C-SIZE T (GET N EXPR-LIST))
                    (LR-P-C-SIZE-LIST (SUB1 N) EXPR-LIST))
              (LR-P-C-SIZE-LIST (SUB1 (LENGTH EXPR-LIST))
                                EXPR-LIST))))

     Linear arithmetic, the lemmas COUNT-NUMBERP and EQUAL-LENGTH-0, and the
definitions of ZEROP, SUB1, LESSP, and EQUAL establish that the measure
(COUNT N) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, LR-P-C-SIZE-LIST is accepted under the definitional
principle.  Note that (NUMBERP (LR-P-C-SIZE-LIST N EXPR-LIST)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-P-C-SIZE-LIST


(DEFN LR-P-PC-1
      (EXPR POS)
      (COND ((NOT (LISTP POS)) 0)
            ((NOT (LISTP EXPR)) 0)
            ((ZEROP (CAR POS)) 0)
            ((EQUAL (CAR EXPR) 'IF)
             (COND ((ZEROP (CAR POS)) 0)
                   ((EQUAL (CAR POS) 1)
                    (LR-P-PC-1 (CADR EXPR) (CDR POS)))
                   ((EQUAL (CAR POS) 2)
                    (PLUS 3
                          (LR-P-C-SIZE T (CADR EXPR))
                          (LR-P-PC-1 (CADDR EXPR) (CDR POS))))
                   (T (PLUS (LR-P-C-SIZE T (CADR EXPR))
                            (LR-P-C-SIZE T (CADDR EXPR))
                            (LR-P-PC-1 (CADDDR EXPR) (CDR POS))
                            4))))
            ((EQUAL (CAR EXPR) (S-TEMP-FETCH)) 0)
            ((EQUAL (CAR EXPR) (S-TEMP-EVAL))
             (LR-P-PC-1 (CADR EXPR) (CDR POS)))
            ((EQUAL (CAR EXPR) (S-TEMP-TEST))
             (PLUS (LR-P-PC-1 (CADR EXPR) (CDR POS))
                   4))
            ((EQUAL (CAR EXPR) 'QUOTE) 0)
            (T (PLUS (LR-P-C-SIZE-LIST (SUB1 (CAR POS))
                                       EXPR)
                     (LR-P-PC-1 (GET (CAR POS) EXPR)
                                (CDR POS))))))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT POS) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, LR-P-PC-1 is accepted under the principle of
definition.  Observe that (NUMBERP (LR-P-PC-1 EXPR POS)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-P-PC-1


(DEFN LR-P-PC
      (L)
      (TAG 'PC
           (CONS (AREA-NAME (P-PC L))
                 (LR-P-PC-1 (PROGRAM-BODY (P-CURRENT-PROGRAM L))
                            (OFFSET (P-PC L))))))

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




[ 0.0 0.0 0.0 ]

LR-P-PC


(DISABLE LR-P-PC)

[ 0.0 0.0 0.0 ]

LR-P-PC-OFF


(DEFN S->LR1
      (S L TABLE)
      (P-STATE (TAG 'PC
                    (CONS (S-PNAME S) (S-POS S)))
               (P-CTRL-STK L)
               (P-TEMP-STK L)
               (LR-COMPILE-PROGRAMS (S-PROGS S)
                                    TABLE)
               (P-DATA-SEGMENT L)
               (P-MAX-CTRL-STK-SIZE L)
               (P-MAX-TEMP-STK-SIZE L)
               (P-WORD-SIZE L)
               (S-ERR-FLAG S)))

     From the definition we can conclude that (P-STATEP (S->LR1 S L TABLE)) is
a theorem.




[ 0.0 0.0 0.0 ]

S->LR1


(DISABLE S->LR1)

[ 0.0 0.0 0.0 ]

S->LR1-OFF


(DEFN S->LR
 (S FHEAP-SIZE MAX-CTRL MAX-TEMP WORD-SIZE)
 (LET
   ((TEMP-ALIST (LR-MAKE-TEMP-NAME-ALIST (STRIP-CARS (S-TEMPS S))
                                         (STRIP-CARS (S-PARAMS S))))
    (DATASEG-TABLE (LR-DATA-SEG-TABLE (S-PROGS S)
                                      (S-PARAMS S)
                                      FHEAP-SIZE)))
   (LET ((RETURN-PC (TAG 'PC
                         (CONS (S-PNAME S)
                               (LR-P-PC-1 (LR-COMPILE-BODY T
                                                           (S-BODY (S-PROG S))
                                                           TEMP-ALIST
                                                           (CDR DATASEG-TABLE))
                                          (S-POS S))))))
        (S->LR1 S
                (P-STATE NIL
                         (LR-INITIAL-CSTK (S-PARAMS S)
                                          TEMP-ALIST
                                          (CDR DATASEG-TABLE)
                                          RETURN-PC)
                         NIL NIL
                         (CAR DATASEG-TABLE)
                         MAX-CTRL MAX-TEMP WORD-SIZE NIL)
                (CDR DATASEG-TABLE)))))

     From the definition we can conclude that:
      (P-STATEP (S->LR S FHEAP-SIZE MAX-CTRL MAX-TEMP WORD-SIZE))
is a theorem.




[ 0.0 0.0 0.0 ]

S->LR


(DISABLE S->LR)

[ 0.0 0.0 0.0 ]

S->LR-OFF


(DEFN LR-PARAMS
      (FRAME P)
      (FIRSTN (LENGTH (FORMAL-VARS (P-CURRENT-PROGRAM P)))
              (BINDINGS FRAME)))

     From the definition we can conclude that:
      (OR (LITATOM (LR-PARAMS FRAME P))
          (LISTP (LR-PARAMS FRAME P)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-PARAMS


(DISABLE LR-PARAMS)

[ 0.0 0.0 0.0 ]

LR-PARAMS-OFF


(DEFN LR-TEMPS
      (FRAME P)
      (RESTN (LENGTH (FORMAL-VARS (P-CURRENT-PROGRAM P)))
             (BINDINGS FRAME)))

   




[ 0.0 0.0 0.0 ]

LR-TEMPS


(DISABLE LR-TEMPS)

[ 0.0 0.0 0.0 ]

LR-TEMPS-OFF


(DEFN LR-SET-EXPR
      (S1 S2 POS)
      (P-STATE (TAG 'PC
                    (CONS (AREA-NAME (P-PC S2)) POS))
               (P-CTRL-STK S1)
               (P-TEMP-STK S1)
               (P-PROG-SEGMENT S2)
               (P-DATA-SEGMENT S1)
               (P-MAX-CTRL-STK-SIZE S1)
               (P-MAX-TEMP-STK-SIZE S1)
               (P-WORD-SIZE S1)
               (P-PSW S1)))

     From the definition we can conclude that:
      (P-STATEP (LR-SET-EXPR S1 S2 POS))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-SET-EXPR


(DEFN LR-SET-ERROR
      (S FLAG)
      (P-STATE (P-PC S)
               (P-CTRL-STK S)
               (P-TEMP-STK S)
               (P-PROG-SEGMENT S)
               (P-DATA-SEGMENT S)
               (P-MAX-CTRL-STK-SIZE S)
               (P-MAX-TEMP-STK-SIZE S)
               (P-WORD-SIZE S)
               FLAG))

     Observe that (P-STATEP (LR-SET-ERROR S FLAG)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-SET-ERROR


(DEFN LR-SET-POS
      (S POS)
      (P-STATE (TAG 'PC
                    (CONS (AREA-NAME (P-PC S)) POS))
               (P-CTRL-STK S)
               (P-TEMP-STK S)
               (P-PROG-SEGMENT S)
               (P-DATA-SEGMENT S)
               (P-MAX-CTRL-STK-SIZE S)
               (P-MAX-TEMP-STK-SIZE S)
               (P-WORD-SIZE S)
               (P-PSW S)))

     Note that (P-STATEP (LR-SET-POS S POS)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-SET-POS


(DEFN LR-SET-TSTK
      (S TEMP-STK)
      (P-STATE (P-PC S)
               (P-CTRL-STK S)
               TEMP-STK
               (P-PROG-SEGMENT S)
               (P-DATA-SEGMENT S)
               (P-MAX-CTRL-STK-SIZE S)
               (P-MAX-TEMP-STK-SIZE S)
               (P-WORD-SIZE S)
               (P-PSW S)))

     Observe that (P-STATEP (LR-SET-TSTK S TEMP-STK)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-SET-TSTK


(DEFN LR-POP-TSTK
      (S)
      (IF (EQUAL (P-PSW S) 'RUN)
          (IF (LISTP (P-TEMP-STK S))
              (LR-SET-TSTK S (POP (P-TEMP-STK S)))
              (LR-SET-ERROR S 'LR-POP-TSTK-EMPTY-STACK))
          S))

     Note that (OR (P-STATEP (LR-POP-TSTK S)) (EQUAL (LR-POP-TSTK S) S)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-POP-TSTK


(DEFN LR-PUSH-TSTK
      (S VALUE)
      (IF (EQUAL (P-PSW S) 'RUN)
          (IF (LESSP (LENGTH (P-TEMP-STK S))
                     (P-MAX-TEMP-STK-SIZE S))
              (LR-SET-TSTK S
                           (PUSH VALUE (P-TEMP-STK S)))
              (LR-SET-ERROR S 'LR-PUSH-TSTK-FULL-STACK))
          S))

     Observe that:
      (OR (P-STATEP (LR-PUSH-TSTK S VALUE))
          (EQUAL (LR-PUSH-TSTK S VALUE) S))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-PUSH-TSTK


(DISABLE LR-PUSH-TSTK)

[ 0.0 0.0 0.0 ]

LR-PUSH-TSTK-OFF


(DEFN LR-IF-OK
      (L)
      (IF (NOT (LESSP (P-MAX-TEMP-STK-SIZE L)
                      (PLUS 1 (LENGTH (P-TEMP-STK L)))))
          L
          (LR-SET-ERROR L 'IF-TEMP-STK-OVERFLOW)))

     Note that (OR (P-STATEP (LR-IF-OK L)) (EQUAL (LR-IF-OK L) L)) is a
theorem.




[ 0.0 0.0 0.0 ]

LR-IF-OK


(DISABLE LR-IF-OK)

[ 0.0 0.0 0.0 ]

LR-IF-OK-OFF


(DEFN LR-SET-TEMP
      (S VALUE VAR-NAME)
      (IF (EQUAL (P-PSW S) 'RUN)
          (P-STATE (P-PC S)
                   (SET-LOCAL-VAR-VALUE VALUE VAR-NAME
                                        (P-CTRL-STK S))
                   (P-TEMP-STK S)
                   (P-PROG-SEGMENT S)
                   (P-DATA-SEGMENT S)
                   (P-MAX-CTRL-STK-SIZE S)
                   (P-MAX-TEMP-STK-SIZE S)
                   (P-WORD-SIZE S)
                   (P-PSW S))
          S))

     From the definition we can conclude that:
      (OR (P-STATEP (LR-SET-TEMP S VALUE VAR-NAME))
          (EQUAL (LR-SET-TEMP S VALUE VAR-NAME)
                 S))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-SET-TEMP


(DISABLE LR-SET-TEMP)

[ 0.0 0.0 0.0 ]

LR-SET-TEMP-OFF


(DEFN LR-EVAL-TEMP-SETP
      (S)
      (NOT (EQUAL (LOCAL-VAR-VALUE (CADDR (LR-EXPR S))
                                   (P-CTRL-STK S))
                  (LR-UNDEF-ADDR))))

     Note that:
      (OR (FALSEP (LR-EVAL-TEMP-SETP S))
          (TRUEP (LR-EVAL-TEMP-SETP S)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-EVAL-TEMP-SETP


(DISABLE LR-EVAL-TEMP-SETP)

[ 0.0 0.0 0.0 ]

LR-EVAL-TEMP-SETP-OFF


(DEFN LR-DO-TEMP-FETCH
      (S)
      (IF (LR-EVAL-TEMP-SETP S)
          (LR-PUSH-TSTK S
                        (LOCAL-VAR-VALUE (CADDR (LR-EXPR S))
                                         (P-CTRL-STK S)))
          (LR-SET-ERROR S 'TEMP-FETCH-NOT-SET)))

     Observe that:
      (OR (P-STATEP (LR-DO-TEMP-FETCH S))
          (EQUAL (LR-DO-TEMP-FETCH S) S))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-DO-TEMP-FETCH


(DISABLE LR-DO-TEMP-FETCH)

[ 0.0 0.0 0.0 ]

LR-DO-TEMP-FETCH-OFF


(DEFN LR-POP-CSTK
      (S)
      (IF (EQUAL (P-PSW S) 'RUN)
          (P-STATE (P-PC S)
                   (POP (P-CTRL-STK S))
                   (P-TEMP-STK S)
                   (P-PROG-SEGMENT S)
                   (P-DATA-SEGMENT S)
                   (P-MAX-CTRL-STK-SIZE S)
                   (P-MAX-TEMP-STK-SIZE S)
                   (P-WORD-SIZE S)
                   (P-PSW S))
          S))

     Observe that (OR (P-STATEP (LR-POP-CSTK S)) (EQUAL (LR-POP-CSTK S) S)) is
a theorem.




[ 0.0 0.0 0.0 ]

LR-POP-CSTK


(DISABLE LR-POP-CSTK)

[ 0.0 0.0 0.0 ]

LR-POP-CSTK-OFF


(DEFN LR-TYPE-CONTENTS-P
      (OBJECT TAG CONTENTS)
      (AND (EQUAL (TYPE OBJECT) TAG)
           (EQUAL (UNTAG OBJECT) CONTENTS)))

     From the definition we can conclude that:
      (OR (FALSEP (LR-TYPE-CONTENTS-P OBJECT TAG CONTENTS))
          (TRUEP (LR-TYPE-CONTENTS-P OBJECT TAG CONTENTS)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-TYPE-CONTENTS-P


(DEFN P-RECOGNIZER-CODE
      (NAME TAG)
      (LIST NAME 'NIL
            'NIL
            '(FETCH)
            (LIST 'PUSH-CONSTANT (TAG 'NAT TAG))
            '(EQ)
            '(TEST-BOOL-AND-JUMP F FALSE)
            (LIST 'PUSH-CONSTANT (LR-T-ADDR))
            '(RET)
            (LIST 'DL
                  'FALSE
                  'NIL
                  (LIST 'PUSH-CONSTANT (LR-F-ADDR)))
            '(RET)))

     Observe that (LISTP (P-RECOGNIZER-CODE NAME TAG)) is a theorem.




[ 0.0 0.0 0.0 ]

P-RECOGNIZER-CODE


(DEFN P-RECOGNIZER-CLOCK
      (P-STATE TAG)
      7)

WARNING:  P-STATE and TAG are in the arglist but not in the body of the
definition of P-RECOGNIZER-CLOCK.


     Note that (NUMBERP (P-RECOGNIZER-CLOCK P-STATE TAG)) is a theorem.




[ 0.0 0.0 0.0 ]

P-RECOGNIZER-CLOCK


(DEFN P-ACCESSOR-CODE
      (NAME TAG DEFAULT OFFSET)
      (LIST NAME
            '(X)
            'NIL
            '(PUSH-LOCAL X)
            '(FETCH)
            (LIST 'PUSH-CONSTANT (TAG 'NAT TAG))
            '(EQ)
            '(TEST-BOOL-AND-JUMP T ARG1)
            (LIST 'PUSH-CONSTANT DEFAULT)
            '(RET)
            '(DL ARG1 NIL (PUSH-LOCAL X))
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT OFFSET))
            '(ADD-ADDR)
            '(FETCH)
            '(RET)))

     From the definition we can conclude that:
      (LISTP (P-ACCESSOR-CODE NAME TAG DEFAULT OFFSET))
is a theorem.




[ 0.0 0.0 0.0 ]

P-ACCESSOR-CODE


(DEFN P-ACCESSOR-CLOCK
      (P TAG)
      (IF (EQUAL (FETCH (TOP (P-TEMP-STK P))
                        (P-DATA-SEGMENT P))
                 (TAG 'NAT TAG))
          11 8))

     From the definition we can conclude that:
      (NUMBERP (P-ACCESSOR-CLOCK P TAG))
is a theorem.




[ 0.0 0.0 0.0 ]

P-ACCESSOR-CLOCK


(DEFN P-CAR-CODE NIL
      (P-ACCESSOR-CODE 'CAR
                       (LR-CONS-TAG)
                       (LR-0-ADDR)
                       (LR-CAR-OFFSET)))

     From the definition we can conclude that (LISTP (P-CAR-CODE)) is a
theorem.




[ 0.0 0.0 0.0 ]

P-CAR-CODE


(DEFN P-CAR-CLOCK
      (P)
      (P-ACCESSOR-CLOCK P (LR-CONS-TAG)))

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




[ 0.0 0.0 0.0 ]

P-CAR-CLOCK


(DISABLE P-CAR-CLOCK)

[ 0.0 0.0 0.0 ]

P-CAR-CLOCK-OFF


(DEFN P-CDR-CODE NIL
      (P-ACCESSOR-CODE 'CDR
                       (LR-CONS-TAG)
                       (LR-0-ADDR)
                       (LR-CDR-OFFSET)))

     From the definition we can conclude that (LISTP (P-CDR-CODE)) is a
theorem.




[ 0.0 0.0 0.0 ]

P-CDR-CODE


(DEFN P-CDR-CLOCK
      (P)
      (P-ACCESSOR-CLOCK P (LR-CONS-TAG)))

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




[ 0.0 0.0 0.0 ]

P-CDR-CLOCK


(DISABLE P-CDR-CLOCK)

[ 0.0 0.0 0.0 ]

P-CDR-CLOCK-OFF


(DEFN P-CONS-CODE NIL
      (LIST 'CONS
            'NIL
            '((TEMP (NAT 0)))
            '(PUSH-GLOBAL FREE-PTR)
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT (LR-CDR-OFFSET)))
            '(ADD-ADDR)
            '(DEPOSIT)
            '(PUSH-GLOBAL FREE-PTR)
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT (LR-CAR-OFFSET)))
            '(ADD-ADDR)
            '(DEPOSIT)
            '(PUSH-GLOBAL FREE-PTR)
            '(PUSH-GLOBAL FREE-PTR)
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT (LR-REF-COUNT-OFFSET)))
            '(ADD-ADDR)
            '(SET-LOCAL TEMP)
            '(FETCH)
            '(PUSH-CONSTANT (NAT 1))
            '(PUSH-LOCAL TEMP)
            '(DEPOSIT)
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT (LR-CONS-TAG)))
            '(PUSH-GLOBAL FREE-PTR)
            '(DEPOSIT)
            '(POP-GLOBAL FREE-PTR)
            '(RET)))

     Note that (LISTP (P-CONS-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-CONS-CODE


(DEFN P-CONS-CLOCK (P) 23)

WARNING:  P is in the arglist but not in the body of the definition of
P-CONS-CLOCK.


     Observe that (NUMBERP (P-CONS-CLOCK P)) is a theorem.




[ 0.0 0.0 0.0 ]

P-CONS-CLOCK


(DISABLE P-CONS-CLOCK)

[ 0.0 0.0 0.0 ]

P-CONS-CLOCK-OFF


(DEFN P-FALSE-CODE NIL
      (LIST 'FALSE
            'NIL
            'NIL
            (LIST 'PUSH-CONSTANT (LR-F-ADDR))
            '(RET)))

     Observe that (LISTP (P-FALSE-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-FALSE-CODE


(DEFN P-FALSE-CLOCK (P) 3)

WARNING:  P is in the arglist but not in the body of the definition of
P-FALSE-CLOCK.


     Observe that (NUMBERP (P-FALSE-CLOCK P)) is a theorem.




[ 0.0 0.0 0.0 ]

P-FALSE-CLOCK


(DISABLE P-FALSE-CLOCK)

[ 0.0 0.0 0.0 ]

P-FALSE-CLOCK-OFF


(DEFN P-FALSEP-CODE NIL
      (LIST 'FALSEP
            'NIL
            'NIL
            (LIST 'PUSH-CONSTANT (LR-F-ADDR))
            '(EQ)
            '(TEST-BOOL-AND-JUMP T TRUE)
            (LIST 'PUSH-CONSTANT (LR-F-ADDR))
            '(RET)
            (LIST 'DL
                  'TRUE
                  'NIL
                  (LIST 'PUSH-CONSTANT (LR-T-ADDR)))
            '(RET)))

     Note that (LISTP (P-FALSEP-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-FALSEP-CODE


(DEFN P-FALSEP-CLOCK (P) 6)

WARNING:  P is in the arglist but not in the body of the definition of
P-FALSEP-CLOCK.


     Observe that (NUMBERP (P-FALSEP-CLOCK P)) is a theorem.




[ 0.0 0.0 0.0 ]

P-FALSEP-CLOCK


(DISABLE P-FALSEP-CLOCK)

[ 0.0 0.0 0.0 ]

P-FALSEP-CLOCK-OFF


(DEFN P-LISTP-CODE NIL
      (P-RECOGNIZER-CODE 'LISTP
                         (LR-CONS-TAG)))

     Observe that (LISTP (P-LISTP-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-LISTP-CODE


(DEFN P-LISTP-CLOCK
      (P)
      (P-RECOGNIZER-CLOCK P (LR-CONS-TAG)))

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




[ 0.0 0.0 0.0 ]

P-LISTP-CLOCK


(DISABLE P-LISTP-CLOCK)

[ 0.0 0.0 0.0 ]

P-LISTP-CLOCK-OFF


(DEFN P-NLISTP-CODE NIL
      (LIST 'NLISTP
            'NIL
            'NIL
            '(FETCH)
            (LIST 'PUSH-CONSTANT
                  (TAG 'NAT (LR-CONS-TAG)))
            '(EQ)
            '(TEST-BOOL-AND-JUMP F TRUE)
            (LIST 'PUSH-CONSTANT (LR-F-ADDR))
            '(RET)
            (LIST 'DL
                  'TRUE
                  'NIL
                  (LIST 'PUSH-CONSTANT (LR-T-ADDR)))
            '(RET)))

     Note that (LISTP (P-NLISTP-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-NLISTP-CODE


(DEFN P-NLISTP-CLOCK (P) 7)

WARNING:  P is in the arglist but not in the body of the definition of
P-NLISTP-CLOCK.


     Observe that (NUMBERP (P-NLISTP-CLOCK P)) is a theorem.




[ 0.0 0.0 0.0 ]

P-NLISTP-CLOCK


(DISABLE P-NLISTP-CLOCK)

[ 0.0 0.0 0.0 ]

P-NLISTP-CLOCK-OFF


(DEFN P-TRUE-CODE NIL
      (LIST 'TRUE
            'NIL
            'NIL
            (LIST 'PUSH-CONSTANT (LR-T-ADDR))
            '(RET)))

     Observe that (LISTP (P-TRUE-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-TRUE-CODE


(DEFN P-TRUE-CLOCK (P) 3)

WARNING:  P is in the arglist but not in the body of the definition of
P-TRUE-CLOCK.


     Observe that (NUMBERP (P-TRUE-CLOCK P)) is a theorem.




[ 0.0 0.0 0.0 ]

P-TRUE-CLOCK


(DISABLE P-TRUE-CLOCK)

[ 0.0 0.0 0.0 ]

P-TRUE-CLOCK-OFF


(DEFN P-TRUEP-CODE NIL
      (P-RECOGNIZER-CODE 'TRUEP
                         (LR-TRUE-TAG)))

     Observe that (LISTP (P-TRUEP-CODE)) is a theorem.




[ 0.0 0.0 0.0 ]

P-TRUEP-CODE


(DEFN P-TRUEP-CLOCK
      (P)
      (P-RECOGNIZER-CLOCK P (LR-FALSE-TAG)))

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




[ 0.0 0.0 0.0 ]

P-TRUEP-CLOCK


(DISABLE P-TRUEP-CLOCK)

[ 0.0 0.0 0.0 ]

P-TRUEP-CLOCK-OFF


(DEFN P-RUNTIME-SUPPORT-PROGRAMS NIL
      (LIST (P-CAR-CODE)
            (P-CDR-CODE)
            (P-CONS-CODE)
            (P-FALSE-CODE)
            (P-FALSEP-CODE)
            (P-LISTP-CODE)
            (P-NLISTP-CODE)
            (P-TRUE-CODE)
            (P-TRUEP-CODE)))

     From the definition we can conclude that:
      (LISTP (P-RUNTIME-SUPPORT-PROGRAMS))
is a theorem.




[ 0.0 0.0 0.0 ]

P-RUNTIME-SUPPORT-PROGRAMS


(DISABLE P-RUNTIME-SUPPORT-PROGRAMS)

[ 0.0 0.0 0.0 ]

P-RUNTIME-SUPPORT-PROGRAMS-OFF


(DEFN LR-CONVERT-DIGIT-TO-ASCII
      (DIGIT)
      (PLUS (ASCII-0) DIGIT))

     From the definition we can conclude that:
      (NUMBERP (LR-CONVERT-DIGIT-TO-ASCII DIGIT))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-CONVERT-DIGIT-TO-ASCII


(DEFN LR-CONVERT-NUM-TO-ASCII
 (NUMBER LIST)
 (IF
  (LESSP NUMBER 10)
  (CONS (LR-CONVERT-DIGIT-TO-ASCII NUMBER)
        LIST)
  (LR-CONVERT-NUM-TO-ASCII
                        (QUOTIENT NUMBER 10)
                        (CONS (LR-CONVERT-DIGIT-TO-ASCII (REMAINDER NUMBER 10))
                              LIST)))
 ((LESSP (FIX NUMBER))))

     Linear arithmetic, the lemma LESSP-QUOTIENT, and the definitions of FIX,
LESSP, EQUAL, and NUMBERP establish that the measure (FIX NUMBER) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
LR-CONVERT-NUM-TO-ASCII is accepted under the principle of definition.  Note
that (LISTP (LR-CONVERT-NUM-TO-ASCII NUMBER LIST)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-CONVERT-NUM-TO-ASCII


(DEFN LR-MAKE-LABEL
      (N)
      (PACK (CONS (CAR (UNPACK 'L))
                  (CONS (ASCII-DASH)
                        (APPEND (LR-CONVERT-NUM-TO-ASCII N NIL)
                                0)))))

     Note that (LITATOM (LR-MAKE-LABEL N)) is a theorem.




[ 0.0 0.0 0.0 ]

LR-MAKE-LABEL


(DISABLE LR-MAKE-LABEL)

[ 0.0 0.0 0.0 ]

LR-MAKE-LABEL-OFF


(DEFN LABEL-INSTRS
      (INSTRS N)
      (IF (LISTP INSTRS)
          (CONS (DL (LR-MAKE-LABEL N)
                    NIL
                    (CAR INSTRS))
                (LABEL-INSTRS (CDR INSTRS) (ADD1 N)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT INSTRS) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, LABEL-INSTRS is accepted under the
principle of definition.  Note that:
      (OR (LITATOM (LABEL-INSTRS INSTRS N))
          (LISTP (LABEL-INSTRS INSTRS N)))
is a theorem.




[ 0.0 0.0 0.0 ]

LABEL-INSTRS


(DEFN COMP-TEMP-TEST
      (EXPR INSTRS N)
      (APPEND (LIST (LIST 'PUSH-LOCAL (CADDR EXPR))
                    (LIST 'PUSH-CONSTANT (LR-UNDEF-ADDR))
                    '(EQ)
                    (LIST 'TEST-BOOL-AND-JUMP
                          'F
                          (LR-MAKE-LABEL (PLUS N 6 (LENGTH INSTRS)))))
              (APPEND INSTRS
                      (LIST (LIST 'SET-LOCAL (CADDR EXPR))
                            (LIST 'JUMP
                                  (LR-MAKE-LABEL (PLUS N 7 (LENGTH INSTRS))))
                            (LIST 'PUSH-LOCAL (CADDR EXPR))))))

     Observe that (LISTP (COMP-TEMP-TEST EXPR INSTRS N)) is a theorem.




[ 0.0 0.0 0.0 ]

COMP-TEMP-TEST


(DEFN COMP-IF
 (TEST-INSTRS THEN-INSTRS ELSE-INSTRS N)
 (APPEND TEST-INSTRS
       (APPEND (LIST (LIST 'PUSH-CONSTANT (LR-F-ADDR))
                     '(EQ)
                     (LIST 'TEST-BOOL-AND-JUMP
                           'T
                           (LR-MAKE-LABEL (PLUS N 4
                                                (LENGTH TEST-INSTRS)
                                                (LENGTH THEN-INSTRS)))))
               (APPEND THEN-INSTRS
                       (CONS (LIST 'JUMP
                                   (LR-MAKE-LABEL (PLUS N 4
                                                        (LENGTH TEST-INSTRS)
                                                        (LENGTH THEN-INSTRS)
                                                        (LENGTH ELSE-INSTRS))))
                             ELSE-INSTRS)))))

     From the definition we can conclude that:
      (LISTP (COMP-IF TEST-INSTRS THEN-INSTRS ELSE-INSTRS N))
is a theorem.




[ 0.0 0.0 0.0 ]

COMP-IF


(DEFN COMP-BODY-1
      (FLAG EXPR N)
      (COND ((EQUAL FLAG 'LIST)
             (IF (LISTP EXPR)
                 (APPEND (COMP-BODY-1 T (CAR EXPR) N)
                         (COMP-BODY-1 'LIST
                                      (CDR EXPR)
                                      (PLUS N (LR-P-C-SIZE T (CAR EXPR)))))
                 NIL))
            ((LISTP EXPR)
             (COND ((EQUAL (CAR EXPR) 'IF)
                    (COMP-IF (COMP-BODY-1 T (CADR EXPR) N)
                             (COMP-BODY-1 T
                                          (CADDR EXPR)
                                          (PLUS N 3
                                                (LR-P-C-SIZE T (CADR EXPR))))
                             (COMP-BODY-1 T
                                          (CADDDR EXPR)
                                          (PLUS N 4
                                                (LR-P-C-SIZE T (CADR EXPR))
                                                (LR-P-C-SIZE T (CADDR EXPR))))
                             N))
                   ((EQUAL (CAR EXPR) (S-TEMP-FETCH))
                    (LIST (LIST 'PUSH-LOCAL (CADDR EXPR))))
                   ((EQUAL (CAR EXPR) (S-TEMP-EVAL))
                    (APPEND (COMP-BODY-1 T (CADR EXPR) N)
                            (LIST (LIST 'SET-LOCAL (CADDR EXPR)))))
                   ((EQUAL (CAR EXPR) (S-TEMP-TEST))
                    (COMP-TEMP-TEST EXPR
                                    (COMP-BODY-1 T (CADR EXPR) (PLUS N 4))
                                    N))
                   ((EQUAL (CAR EXPR) 'QUOTE)
                    (LIST (LIST 'PUSH-CONSTANT (CADR EXPR))))
                   (T (APPEND (COMP-BODY-1 'LIST (CDR EXPR) N)
                              (IF (DEFINEDP (CAR EXPR)
                                            (P-RUNTIME-SUPPORT-PROGRAMS))
                                  (LIST (LIST 'CALL (CAR EXPR)))
                                  (LIST (LIST 'CALL
                                              (USER-FNAME (CAR EXPR)))))))))
            (T (LIST (LIST 'PUSH-LOCAL EXPR)))))

     Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, CAR-LESSEQP, and
CDR-LESSEQP can be used to show that the measure (COUNT EXPR) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
COMP-BODY-1 is accepted under the definitional principle.  From the definition
we can conclude that:
      (OR (LITATOM (COMP-BODY-1 FLAG EXPR N))
          (LISTP (COMP-BODY-1 FLAG EXPR N)))
is a theorem.




[ 0.0 0.0 0.0 ]

COMP-BODY-1


(DISABLE COMP-BODY-1)

[ 0.0 0.0 0.0 ]

COMP-BODY-1-OFF


(DEFN COMP-BODY
      (BODY)
      (LABEL-INSTRS (APPEND (COMP-BODY-1 T BODY 0)
                            '((RET)))
                    0))

     From the definition we can conclude that:
      (OR (LITATOM (COMP-BODY BODY))
          (LISTP (COMP-BODY BODY)))
is a theorem.




[ 0.0 0.0 0.0 ]

COMP-BODY


(DISABLE COMP-BODY)

[ 0.0 0.0 0.0 ]

COMP-BODY-OFF


(DEFN COMP-PROGRAMS-1
      (PROGRAMS)
      (IF (LISTP PROGRAMS)
          (CONS (LR-MAKE-PROGRAM (NAME (CAR PROGRAMS))
                                 (FORMAL-VARS (CAR PROGRAMS))
                                 (TEMP-VAR-DCLS (CAR PROGRAMS))
                                 (COMP-BODY (PROGRAM-BODY (CAR PROGRAMS))))
                (COMP-PROGRAMS-1 (CDR PROGRAMS)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT PROGRAMS) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, COMP-PROGRAMS-1 is accepted under the principle
of definition.  Note that:
      (OR (LITATOM (COMP-PROGRAMS-1 PROGRAMS))
          (LISTP (COMP-PROGRAMS-1 PROGRAMS)))
is a theorem.




[ 0.0 0.0 0.0 ]

COMP-PROGRAMS-1


(DEFN COMP-PROGRAMS
 (PROGRAMS)
 (CONS
  (LR-MAKE-PROGRAM
               (NAME (CAR PROGRAMS))
               (FORMAL-VARS (CAR PROGRAMS))
               (TEMP-VAR-DCLS (CAR PROGRAMS))
               (LABEL-INSTRS (APPEND (COMP-BODY-1 T
                                                  (PROGRAM-BODY (CAR PROGRAMS))
                                                  0)
                                     (LIST (LIST 'SET-GLOBAL
                                                 (AREA-NAME (LR-ANSWER-ADDR)))
                                           '(RET)))
                             0))
  (APPEND (COMP-PROGRAMS-1 (CDR PROGRAMS))
          (P-RUNTIME-SUPPORT-PROGRAMS))))

     From the definition we can conclude that (LISTP (COMP-PROGRAMS PROGRAMS))
is a theorem.




[ 0.0 0.0 0.0 ]

COMP-PROGRAMS


(DISABLE COMP-PROGRAMS)

[ 0.0 0.0 0.0 ]

COMP-PROGRAMS-OFF


(DEFN LR-PROPER-EXPRP
      (FLAG EXPR PNAMES FORMALS TEMPS TABLE)
      (COND ((EQUAL FLAG 'LIST)
             (IF (LISTP EXPR)
                 (AND (LR-PROPER-EXPRP T
                                       (CAR EXPR)
                                       PNAMES FORMALS TEMPS TABLE)
                      (LR-PROPER-EXPRP 'LIST
                                       (CDR EXPR)
                                       PNAMES FORMALS TEMPS TABLE))
                 (EQUAL EXPR NIL)))
            ((LITATOM EXPR) (MEMBER EXPR FORMALS))
            ((NLISTP EXPR) F)
            ((NOT (PLISTP EXPR)) F)
            ((EQUAL (CAR EXPR) (S-TEMP-FETCH))
             (AND (MEMBER (CADDR EXPR) TEMPS)
                  (EQUAL (LENGTH EXPR) 3)))
            ((OR (EQUAL (CAR EXPR) (S-TEMP-EVAL))
                 (EQUAL (CAR EXPR) (S-TEMP-TEST)))
             (AND (MEMBER (CADDR EXPR) TEMPS)
                  (EQUAL (LENGTH EXPR) 3)
                  (LR-PROPER-EXPRP T
                                   (CADR EXPR)
                                   PNAMES FORMALS TEMPS TABLE)))
            ((EQUAL (CAR EXPR) 'QUOTE)
             (AND (EQUAL (TYPE (CADR EXPR)) 'ADDR)
                  (MEMBER (CADR EXPR)
                          (STRIP-CDRS TABLE))
                  (EQUAL (LENGTH (CDR EXPR))
                         (ARITY (CAR EXPR)))))
            ((SUBRP (CAR EXPR))
             (AND (EQUAL (LENGTH (CDR EXPR))
                         (ARITY (CAR EXPR)))
                  (OR (EQUAL (CAR EXPR) 'IF)
                      (DEFINEDP (CAR EXPR)
                                (P-RUNTIME-SUPPORT-PROGRAMS)))
                  (NOT (MEMBER (CAR EXPR) PNAMES))
                  (LR-PROPER-EXPRP 'LIST
                                   (CDR EXPR)
                                   PNAMES FORMALS TEMPS TABLE)))
            ((BODY (CAR EXPR))
             (AND (EQUAL (LENGTH (CDR EXPR))
                         (ARITY (CAR EXPR)))
                  (MEMBER (CAR EXPR) PNAMES)
                  (LR-PROPER-EXPRP 'LIST
                                   (CDR EXPR)
                                   PNAMES FORMALS TEMPS TABLE)))
            (T F)))

     Linear arithmetic, the lemmas CDR-LESSP, CAR-LESSP, CAR-LESSEQP, and
CDR-LESSEQP, and the definitions of OR, S-TEMP-TEST, S-TEMP-EVAL, S-TEMP-FETCH,
PLISTP, and NLISTP can be used to prove that the measure (COUNT EXPR)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, LR-PROPER-EXPRP is accepted under the principle of definition.  From
the definition we can conclude that:
      (OR (FALSEP (LR-PROPER-EXPRP FLAG EXPR PNAMES FORMALS TEMPS TABLE))
          (TRUEP (LR-PROPER-EXPRP FLAG EXPR PNAMES FORMALS TEMPS TABLE)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-PROPER-EXPRP


(DEFN ALL-UNDEF-ADDRS
      (LIST)
      (IF (LISTP LIST)
          (AND (EQUAL (CAR LIST) (LR-UNDEF-ADDR))
               (ALL-UNDEF-ADDRS (CDR LIST)))
          T))

     Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT LIST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, ALL-UNDEF-ADDRS is accepted under the definitional
principle.  Note that:
      (OR (FALSEP (ALL-UNDEF-ADDRS LIST))
          (TRUEP (ALL-UNDEF-ADDRS LIST)))
is a theorem.




[ 0.0 0.0 0.0 ]

ALL-UNDEF-ADDRS


(DEFN LR-PROGRAMS-PROPERP-1
      (PROGRAMS PROGRAM-NAMES TABLE)
      (IF (LISTP PROGRAMS)
          (AND (ALL-LITATOMS (FORMAL-VARS (CAR PROGRAMS)))
               (ALL-LITATOMS (STRIP-CARS (TEMP-VAR-DCLS (CAR PROGRAMS))))
               (ALL-UNDEF-ADDRS (STRIP-CADRS (TEMP-VAR-DCLS (CAR PROGRAMS))))
               (LR-PROPER-EXPRP T
                                (PROGRAM-BODY (CAR PROGRAMS))
                                PROGRAM-NAMES
                                (FORMAL-VARS (CAR PROGRAMS))
                                (STRIP-CARS (TEMP-VAR-DCLS (CAR PROGRAMS)))
                                TABLE)
               (LR-PROGRAMS-PROPERP-1 (CDR PROGRAMS)
                                      PROGRAM-NAMES TABLE))
          T))

     Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT PROGRAMS) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, LR-PROGRAMS-PROPERP-1 is accepted under
the principle of definition.  Observe that:
      (OR (FALSEP (LR-PROGRAMS-PROPERP-1 PROGRAMS PROGRAM-NAMES TABLE))
          (TRUEP (LR-PROGRAMS-PROPERP-1 PROGRAMS PROGRAM-NAMES TABLE)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-PROGRAMS-PROPERP-1


(DISABLE LR-PROGRAMS-PROPERP-1)

[ 0.0 0.0 0.0 ]

LR-PROGRAMS-PROPERP-1-OFF


(DEFN LR-PROGRAMS-PROPERP
      (L TABLE)
      (AND (DEFINEDP (AREA-NAME (P-PC L))
                     (P-PROG-SEGMENT L))
           (EQUAL (CAAR (P-PROG-SEGMENT L))
                  'MAIN)
           (ALL-USER-FNAMESP (CDR (STRIP-CARS (P-PROG-SEGMENT L))))
           (LR-PROGRAMS-PROPERP-1 (P-PROG-SEGMENT L)
                                  (STRIP-LOGIC-FNAMES (CDR (P-PROG-SEGMENT L)))
                                  TABLE)))

     Note that:
      (OR (FALSEP (LR-PROGRAMS-PROPERP L TABLE))
          (TRUEP (LR-PROGRAMS-PROPERP L TABLE)))
is a theorem.




[ 0.0 0.0 0.0 ]

LR-PROGRAMS-PROPERP


(DISABLE LR-PROGRAMS-PROPERP)

[ 0.0 0.0 0.0 ]

LR-PROGRAMS-PROPERP-OFF


(PROVE-LEMMA LR-P-C-SIZE-FLAG-NOT-LIST-NOT-0
             (REWRITE)
             (IMPLIES (NOT (EQUAL FLAG 'LIST))
                      (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))))


     Give the conjecture the name *1.


     Let us appeal to the induction principle.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (EQUAL FLAG 'LIST)
                         (LISTP EXPR)
                         (p 'LIST (CDR EXPR))
                         (p T (CAR EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (EQUAL FLAG 'LIST)
                         (NOT (LISTP EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (EQUAL (CAR EXPR) 'IF)
                         (p T (CADDDR EXPR))
                         (p T (CADDR EXPR))
                         (p T (CADR EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (NOT (EQUAL (CAR EXPR) 'IF))
                         (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (NOT (EQUAL (CAR EXPR) 'IF))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                         (EQUAL (CAR EXPR) (S-TEMP-EVAL))
                         (p T (CADR EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (NOT (EQUAL (CAR EXPR) 'IF))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                         (EQUAL (CAR EXPR) (S-TEMP-TEST))
                         (p T (CADR EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (NOT (EQUAL (CAR EXPR) 'IF))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                         (EQUAL (CAR EXPR) 'QUOTE))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (LISTP EXPR)
                         (NOT (EQUAL (CAR EXPR) 'IF))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                         (NOT (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                         (NOT (EQUAL (CAR EXPR) 'QUOTE))
                         (p 'LIST (CDR EXPR)))
                    (p FLAG EXPR))
           (IMPLIES (AND (NOT (EQUAL FLAG 'LIST))
                         (NOT (LISTP EXPR)))
                    (p FLAG EXPR))).
Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, CAR-LESSEQP, and
CDR-LESSEQP can be used to show that the measure (COUNT EXPR) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  Note, however, the inductive instances chosen for FLAG.  The above
induction scheme generates the following eight new conjectures:

Case 8. (IMPLIES (AND (LISTP EXPR)
                      (EQUAL (CAR EXPR) 'IF)
                      (NOT (EQUAL (LR-P-C-SIZE T (CADDDR EXPR))
                                  0))
                      (NOT (EQUAL (LR-P-C-SIZE T (CADDR EXPR))
                                  0))
                      (NOT (EQUAL (LR-P-C-SIZE T (CADR EXPR)) 0))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, appealing to the lemmas PLUS-ZERO-ARG2 and PLUS-ADD1-ARG2,
  and expanding the functions LR-P-C-SIZE, EQUAL, NUMBERP, and ZEROP, to:

        T.

Case 7. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (EQUAL (CAR EXPR) (S-TEMP-FETCH))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, expanding the definitions of S-TEMP-FETCH, LR-P-C-SIZE, and
  EQUAL, to:

        T.

Case 6. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                      (EQUAL (CAR EXPR) (S-TEMP-EVAL))
                      (NOT (EQUAL (LR-P-C-SIZE T (CADR EXPR)) 0))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, applying the lemmas PLUS-ZERO-ARG2 and PLUS-ADD1-ARG2, and
  opening up S-TEMP-FETCH, CAR, S-TEMP-EVAL, LR-P-C-SIZE, EQUAL, NUMBERP, and
  ZEROP, to:

        T.

Case 5. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                      (EQUAL (CAR EXPR) (S-TEMP-TEST))
                      (NOT (EQUAL (LR-P-C-SIZE T (CADR EXPR)) 0))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, appealing to the lemmas PLUS-ZERO-ARG2 and PLUS-ADD1-ARG2,
  and unfolding the functions S-TEMP-FETCH, CAR, S-TEMP-EVAL, S-TEMP-TEST,
  LR-P-C-SIZE, EQUAL, NUMBERP, and ZEROP, to:

        T.

Case 4. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                      (EQUAL (CAR EXPR) 'QUOTE)
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, opening up the definitions of EQUAL, S-TEMP-FETCH,
  S-TEMP-EVAL, S-TEMP-TEST, and LR-P-C-SIZE, to:

        T.

Case 3. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                      (NOT (EQUAL (CAR EXPR) 'QUOTE))
                      (EQUAL 'LIST 'LIST)
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, applying the lemmas PLUS-ZERO-ARG2 and PLUS-ADD1-ARG2, and
  expanding the definitions of S-TEMP-FETCH, S-TEMP-EVAL, S-TEMP-TEST, EQUAL,
  LR-P-C-SIZE, NUMBERP, and ZEROP, to:

        T.

Case 2. (IMPLIES (AND (LISTP EXPR)
                      (NOT (EQUAL (CAR EXPR) 'IF))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-FETCH)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-EVAL)))
                      (NOT (EQUAL (CAR EXPR) (S-TEMP-TEST)))
                      (NOT (EQUAL (CAR EXPR) 'QUOTE))
                      (NOT (EQUAL (LR-P-C-SIZE 'LIST (CDR EXPR))
                                  0))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))).

  This simplifies, applying PLUS-ZERO-ARG2 and PLUS-ADD1-ARG2, and expanding
  the definitions of S-TEMP-FETCH, S-TEMP-EVAL, S-TEMP-TEST, LR-P-C-SIZE,
  NUMBERP, and ZEROP, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP EXPR))
                      (NOT (EQUAL FLAG 'LIST)))
                 (NOT (EQUAL (LR-P-C-SIZE FLAG EXPR) 0))),

  which simplifies, expanding the functions LR-P-C-SIZE and EQUAL, to:

        T.


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


[ 0.0 0.1 0.0 ]

LR-P-C-SIZE-FLAG-NOT-LIST-NOT-0


(PROVE-LEMMA DIFFERENCE-DECREASES
             (REWRITE)
             (IMPLIES (AND (NOT (LESSP X Y))
                           (NOT (ZEROP Y)))
                      (EQUAL (LESSP (DIFFERENCE X Y) X) T)))

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

      (IMPLIES (AND (NOT (LESSP X Y))
                    (NOT (EQUAL Y 0))
                    (NUMBERP Y))
               (EQUAL (LESSP (DIFFERE