(NOTE-LIB "piton" T)
Loading ./fm9001-piton/piton.lib
Finished loading ./fm9001-piton/piton.lib
Loading ./fm9001-piton/piton.o
Loading ./fm9001-piton/0piton.o
Finished loading ./fm9001-piton/0piton.o
Loading ./fm9001-piton/1piton.o
Finished loading ./fm9001-piton/1piton.o
Loading ./fm9001-piton/2piton.o
Finished loading ./fm9001-piton/2piton.o
Loading ./fm9001-piton/3piton.o
Finished loading ./fm9001-piton/3piton.o
Loading ./fm9001-piton/4piton.o
Finished loading ./fm9001-piton/4piton.o
Loading ./fm9001-piton/5piton.o
Finished loading ./fm9001-piton/5piton.o
Finished loading ./fm9001-piton/piton.o

(#./fm9001-piton/piton.lib #./fm9001-piton/piton)


(SET-STATUS ADDITION-ON ADDITION
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

ADDITION-ON


(SET-STATUS MULTIPLICATION-ON MULTIPLICATION
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

MULTIPLICATION-ON


(SET-STATUS REMAINDERS-ON REMAINDERS
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

REMAINDERS-ON


(SET-STATUS QUOTIENTS-ON QUOTIENTS
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

QUOTIENTS-ON


(SET-STATUS EXPONENTIATION-ON EXPONENTIATION
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

EXPONENTIATION-ON


(SET-STATUS LOGS-ON LOGS
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

LOGS-ON


(SET-STATUS GCDS-ON GCDS
            ((OTHERWISE ENABLE)))

[ 0.0 0.0 0.0 ]

GCDS-ON


(DEFN CLOCK-PLUS (X Y) (PLUS X Y))

     From the definition we can conclude that (NUMBERP (CLOCK-PLUS X Y)) is a
theorem.




[ 0.0 0.0 0.0 ]

CLOCK-PLUS


(PROVE-LEMMA P-ADD1
             (REWRITE)
             (EQUAL (P P0 (ADD1 N))
                    (P (P-STEP P0) N))
             ((DISABLE P-STEP)))

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

      (IMPLIES (NOT (NUMBERP N))
               (EQUAL (P (P-STEP P0) 0)
                      (P (P-STEP P0) N))).

This again simplifies, expanding EQUAL and P, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-ADD1


(PROVE-LEMMA P-0
             (REWRITE)
             (IMPLIES (ZEROP N)
                      (EQUAL (P P0 N) P0)))

This conjecture simplifies, opening up the functions ZEROP, EQUAL, and P, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-0


(PROVE-LEMMA CLOCK-PLUS-FUNCTION
             (REWRITE)
             (EQUAL (P P0 (CLOCK-PLUS X Y))
                    (P (P P0 X) Y))
             ((INDUCT (P P0 X))
              (DISABLE P P-STEP)))

This formula can be simplified, using the abbreviations ZEROP, NOT, OR, AND,
and CLOCK-PLUS, to the following two new formulas:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (P P0 (PLUS X Y))
                        (P (P P0 X) Y))).

  This simplifies, applying P-0, and opening up the definitions of ZEROP,
  EQUAL, and PLUS, to two new formulas:

  Case 2.2.
          (IMPLIES (AND (EQUAL X 0) (NOT (NUMBERP Y)))
                   (EQUAL (P P0 0) (P P0 Y))),

    which again simplifies, rewriting with the lemma P-0, and unfolding the
    definition of ZEROP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (NUMBERP Y)))
                   (EQUAL (P P0 0) (P P0 Y))),

    which again simplifies, applying P-0, and opening up ZEROP, to:

          T.

Case 1. (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (EQUAL (P (P-STEP P0) (PLUS (SUB1 X) Y))
                             (P (P (P-STEP P0) (SUB1 X)) Y)))
                 (EQUAL (P P0 (PLUS X Y))
                        (P (P P0 X) Y))).

  This simplifies, rewriting with COMMUTATIVITY-OF-PLUS and P-ADD1, and
  opening up PLUS, to:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (EQUAL (P (P-STEP P0) (PLUS Y (SUB1 X)))
                             (P (P (P-STEP P0) (SUB1 X)) Y)))
                 (EQUAL (P (P (P-STEP P0) (SUB1 X)) Y)
                        (P (P P0 X) Y))).

  Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
  (SUB1 X).  We use the type restriction lemma noted when SUB1 was introduced
  to constrain the new variable.  The result is:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (EQUAL (P (P-STEP P0) (PLUS Y Z))
                             (P (P (P-STEP P0) Z) Y)))
                 (EQUAL (P (P (P-STEP P0) Z) Y)
                        (P (P P0 (ADD1 Z)) Y))).

  However this further simplifies, rewriting with the lemma P-ADD1, to:

        T.

Q.E.D.


[ 0.1 0.0 0.0 ]

CLOCK-PLUS-FUNCTION


(DISABLE P-ADD1)

[ 0.0 0.0 0.0 ]

P-ADD1-OFF


(PROVE-LEMMA CLOCK-PLUS-ADD1
             (REWRITE)
             (EQUAL (P P0 (CLOCK-PLUS (ADD1 X) Y))
                    (P P0 (ADD1 (CLOCK-PLUS X Y)))))

WARNING:  the previously added lemma, CLOCK-PLUS-FUNCTION, could be applied
whenever the newly proposed CLOCK-PLUS-ADD1 could!


This formula can be simplified, using the abbreviations PLUS-ADD1-ARG1 and
CLOCK-PLUS, to:

      (EQUAL (P P0 (ADD1 (PLUS X Y)))
             (P P0 (ADD1 (PLUS X Y)))),

which simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CLOCK-PLUS-ADD1


(DISABLE CLOCK-PLUS)

[ 0.0 0.0 0.0 ]

CLOCK-PLUS-OFF


(PROVE-LEMMA CLOCK-PLUS-0
             (REWRITE)
             (IMPLIES (ZEROP X)
                      (EQUAL (CLOCK-PLUS X Y) (FIX Y)))
             ((ENABLE CLOCK-PLUS)))

This formula can be simplified, using the abbreviations IMPLIES and CLOCK-PLUS,
to:

      (IMPLIES (ZEROP X)
               (EQUAL (PLUS X Y) (FIX Y))),

which simplifies, opening up the functions ZEROP, EQUAL, PLUS, and FIX, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

CLOCK-PLUS-0


(PROVE-LEMMA FIX-CLOCK-PLUS
             (REWRITE)
             (EQUAL (FIX (CLOCK-PLUS X Y))
                    (CLOCK-PLUS X Y))
             ((ENABLE CLOCK-PLUS)))

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


This formula can be simplified, using the abbreviation CLOCK-PLUS, to the new
conjecture:

      (EQUAL (FIX (PLUS X Y)) (PLUS X Y)),

which simplifies, opening up FIX, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIX-CLOCK-PLUS


(PROVE-LEMMA P-STEP1-OPENER
             (REWRITE)
             (EQUAL (P-STEP1 (CONS OPCODE OPERANDS) P)
                    (IF (P-INS-OKP (CONS OPCODE OPERANDS) P)
                        (P-INS-STEP (CONS OPCODE OPERANDS) P)
                        (P-HALT P
                                (X-Y-ERROR-MSG 'P OPCODE))))
             ((DISABLE P-INS-OKP P-INS-STEP)))

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


This formula can be simplified, using the abbreviations CDR-CONS, UNPACK-PACK,
and X-Y-ERROR-MSG, to:

      (EQUAL (P-STEP1 (CONS OPCODE OPERANDS) P)
             (IF (P-INS-OKP (CONS OPCODE OPERANDS) P)
                 (P-INS-STEP (CONS OPCODE OPERANDS) P)
                 (P-HALT P
                         (PACK (APPEND '(73 76 76 69 71 65 76 45 . 0)
                                       (APPEND (UNPACK OPCODE)
                                               '(45 73 78 83 84 82 85 67
                                                    84 73 79 78
                                                    . 0))))))),

which simplifies, applying CAR-CONS, and opening up the definitions of P-HALT,
X-Y-ERROR-MSG, UNPACK, CDR, CAR, LISTP, APPEND, and P-STEP1, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-STEP1-OPENER


(DISABLE P-STEP1)

[ 0.0 0.0 0.0 ]

P-STEP1-OFF


(PROVE-LEMMA P-OPENER
             (REWRITE)
             (AND (EQUAL (P S 0) S)
                  (EQUAL (P (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL MAX-TEMP
                                     WORD-SIZE PSW)
                            (ADD1 N))
                         (P (P-STEP (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL
                                             MAX-TEMP WORD-SIZE PSW))
                            N)))
             ((DISABLE P-STEP)))

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


This conjecture can be simplified, using the abbreviation AND, to two new
goals:

Case 2. (EQUAL (P S 0) S),

  which simplifies, rewriting with the lemma P-0, and unfolding the function
  ZEROP, to:

        T.

Case 1. (EQUAL (P (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL MAX-TEMP WORD-SIZE
                           PSW)
                  (ADD1 N))
               (P (P-STEP (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL MAX-TEMP
                                   WORD-SIZE PSW))
                  N)),

  which simplifies, rewriting with SUB1-ADD1, and opening up the definition of
  P, to:

        (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (P (P-STEP (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL
                                            MAX-TEMP WORD-SIZE PSW))
                           0)
                        (P (P-STEP (P-STATE PC CTRL TEMP PROG DATA MAX-CTRL
                                            MAX-TEMP WORD-SIZE PSW))
                           N))),

  which again simplifies, applying P-0, and expanding the definition of ZEROP,
  to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-OPENER


(DISABLE P)

[ 0.0 0.0 0.0 ]

P-OFF


(DEFN AT-LEAST-MOREP
      (BASE DELTA VALUE)
      (NOT (LESSP VALUE (PLUS BASE DELTA))))

     Observe that:
      (OR (FALSEP (AT-LEAST-MOREP BASE DELTA VALUE))
          (TRUEP (AT-LEAST-MOREP BASE DELTA VALUE)))
is a theorem.




[ 0.0 0.0 0.0 ]

AT-LEAST-MOREP


(PROVE-LEMMA AT-LEAST-MOREP-NORMALIZE
             (REWRITE)
             (AND (EQUAL (AT-LEAST-MOREP (ADD1 BASE)
                                         DELTA VALUE)
                         (AT-LEAST-MOREP BASE
                                         (ADD1 DELTA)
                                         VALUE))
                  (EQUAL (AT-LEAST-MOREP BASE
                                         (ADD1 DELTA)
                                         (ADD1 VALUE))
                         (AT-LEAST-MOREP BASE DELTA VALUE))))

WARNING:  Note that the rewrite rule AT-LEAST-MOREP-NORMALIZE will be stored
so as to apply only to terms with the nonrecursive function symbol
AT-LEAST-MOREP.


WARNING:  Note that the rewrite rule AT-LEAST-MOREP-NORMALIZE will be stored
so as to apply only to terms with the nonrecursive function symbol
AT-LEAST-MOREP.


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


This formula can be simplified, using the abbreviation AND, to the following
two new formulas:

Case 2. (EQUAL (AT-LEAST-MOREP (ADD1 BASE)
                               DELTA VALUE)
               (AT-LEAST-MOREP BASE
                               (ADD1 DELTA)
                               VALUE)).

  This simplifies, applying the lemmas SUB1-ADD1, PLUS-ADD1-ARG1, and
  PLUS-ADD1-ARG2, and unfolding LESSP and AT-LEAST-MOREP, to the following
  eight new conjectures:

  Case 2.8.
          (IMPLIES (AND (NUMBERP DELTA)
                        (NOT (LESSP VALUE
                                    (ADD1 (PLUS BASE DELTA)))))
                   (NOT (EQUAL VALUE 0))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.7.
          (IMPLIES (AND (NUMBERP DELTA)
                        (NOT (LESSP VALUE
                                    (ADD1 (PLUS BASE DELTA)))))
                   (NUMBERP VALUE)),

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

          T.

  Case 2.6.
          (IMPLIES (AND (NUMBERP DELTA)
                        (NOT (LESSP VALUE
                                    (ADD1 (PLUS BASE DELTA)))))
                   (NOT (LESSP (SUB1 VALUE)
                               (PLUS BASE DELTA)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.5.
          (IMPLIES (AND (NUMBERP DELTA)
                        (LESSP VALUE (ADD1 (PLUS BASE DELTA)))
                        (NOT (EQUAL VALUE 0))
                        (NUMBERP VALUE))
                   (LESSP (SUB1 VALUE)
                          (PLUS BASE DELTA))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.4.
          (IMPLIES (AND (NOT (NUMBERP DELTA))
                        (NOT (LESSP VALUE (ADD1 BASE))))
                   (NOT (EQUAL VALUE 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.3.
          (IMPLIES (AND (NOT (NUMBERP DELTA))
                        (NOT (LESSP VALUE (ADD1 BASE))))
                   (NUMBERP VALUE)),

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

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP DELTA))
                        (NOT (LESSP VALUE (ADD1 BASE))))
                   (NOT (LESSP (SUB1 VALUE)
                               (PLUS BASE DELTA)))),

    which again simplifies, applying SUB1-ADD1 and PLUS-ZERO-ARG2, and opening
    up LESSP, ZEROP, and EQUAL, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP DELTA))
                        (LESSP VALUE (ADD1 BASE))
                        (NOT (EQUAL VALUE 0))
                        (NUMBERP VALUE))
                   (LESSP (SUB1 VALUE)
                          (PLUS BASE DELTA))).

    This again simplifies, using linear arithmetic, to:

          T.

Case 1. (EQUAL (AT-LEAST-MOREP BASE
                               (ADD1 DELTA)
                               (ADD1 VALUE))
               (AT-LEAST-MOREP BASE DELTA VALUE)),

  which simplifies, applying SUB1-ADD1 and PLUS-ADD1-ARG2, and unfolding the
  definitions of LESSP and AT-LEAST-MOREP, to the following ten new
  conjectures:

  Case 1.10.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NUMBERP DELTA)
                        (NUMBERP VALUE))
                   (LESSP VALUE
                          (SUB1 (ADD1 (PLUS BASE DELTA))))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.9.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NUMBERP DELTA)
                        (NOT (NUMBERP VALUE)))
                   (LESSP 0
                          (SUB1 (ADD1 (PLUS BASE DELTA))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.8.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NUMBERP DELTA))
                   (NOT (EQUAL (ADD1 (PLUS BASE DELTA)) 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.7.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NOT (NUMBERP DELTA))
                        (NUMBERP VALUE))
                   (LESSP VALUE (SUB1 (ADD1 BASE)))),

    which again simplifies, rewriting with PLUS-ZERO-ARG2,
    SUB1-TYPE-RESTRICTION, and SUB1-ADD1, and expanding ZEROP, SUB1, EQUAL,
    and LESSP, to the new goal:

          (IMPLIES (AND (NOT (NUMBERP BASE))
                        (LESSP VALUE 0)
                        (NOT (NUMBERP DELTA)))
                   (NOT (NUMBERP VALUE))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.6.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NOT (NUMBERP DELTA))
                        (NOT (NUMBERP VALUE)))
                   (LESSP 0 (SUB1 (ADD1 BASE)))),

    which again simplifies, rewriting with the lemmas PLUS-ZERO-ARG2 and
    SUB1-ADD1, and opening up the functions ZEROP, LESSP, and EQUAL, to:

          T.

  Case 1.5.
          (IMPLIES (AND (LESSP VALUE (PLUS BASE DELTA))
                        (NOT (NUMBERP DELTA)))
                   (NOT (EQUAL (ADD1 BASE) 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                        (NUMBERP DELTA)
                        (NOT (EQUAL (ADD1 (PLUS BASE DELTA)) 0))
                        (NUMBERP VALUE))
                   (NOT (LESSP VALUE
                               (SUB1 (ADD1 (PLUS BASE DELTA)))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                        (NUMBERP DELTA)
                        (NOT (EQUAL (ADD1 (PLUS BASE DELTA)) 0))
                        (NOT (NUMBERP VALUE)))
                   (NOT (LESSP 0
                               (SUB1 (ADD1 (PLUS BASE DELTA)))))),

    which again simplifies, rewriting with the lemmas EQUAL-PLUS-0 and
    PLUS-ZERO-ARG2, and expanding LESSP, NUMBERP, ZEROP, ADD1, EQUAL, SUB1,
    and PLUS, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                        (NOT (NUMBERP DELTA))
                        (NOT (EQUAL (ADD1 BASE) 0))
                        (NUMBERP VALUE))
                   (NOT (LESSP VALUE (SUB1 (ADD1 BASE))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                        (NOT (NUMBERP DELTA))
                        (NOT (EQUAL (ADD1 BASE) 0))
                        (NOT (NUMBERP VALUE)))
                   (NOT (LESSP 0 (SUB1 (ADD1 BASE))))),

    which again simplifies, rewriting with PLUS-ZERO-ARG2 and
    SUB1-TYPE-RESTRICTION, and expanding the functions ZEROP, LESSP, ADD1,
    EQUAL, and SUB1, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

AT-LEAST-MOREP-NORMALIZE


(PROVE-LEMMA AT-LEAST-MOREP-LINEAR
             (REWRITE)
             (IMPLIES (AND (AT-LEAST-MOREP BASE D1 VALUE)
                           (NOT (LESSP D1 D2)))
                      (AT-LEAST-MOREP BASE D2 VALUE)))

WARNING:  Note that the rewrite rule AT-LEAST-MOREP-LINEAR will be stored so
as to apply only to terms with the nonrecursive function symbol AT-LEAST-MOREP.


WARNING:  Note that AT-LEAST-MOREP-LINEAR contains the free variable D1 which
will be chosen by instantiating the hypothesis (AT-LEAST-MOREP BASE D1 VALUE).


This formula can be simplified, using the abbreviations NOT, AT-LEAST-MOREP,
AND, and IMPLIES, to:

      (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE D1)))
                    (NOT (LESSP D1 D2)))
               (NOT (LESSP VALUE (PLUS BASE D2)))),

which simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

AT-LEAST-MOREP-LINEAR


(PROVE-LEMMA LESSP-AS-AT-LEAST-MOREP
             (REWRITE)
             (IMPLIES (AT-LEAST-MOREP BASE DELTA VALUE)
                      (AND (EQUAL (LESSP VALUE X)
                                  (NOT (AT-LEAST-MOREP X 0 VALUE)))
                           (EQUAL (LESSP X VALUE)
                                  (AT-LEAST-MOREP X 1 VALUE)))))

WARNING:  Note that LESSP-AS-AT-LEAST-MOREP contains the free variables DELTA
and BASE which will be chosen by instantiating the hypothesis:
      (AT-LEAST-MOREP BASE DELTA VALUE).



WARNING:  Note that LESSP-AS-AT-LEAST-MOREP contains the free variables DELTA
and BASE which will be chosen by instantiating the hypothesis:
      (AT-LEAST-MOREP BASE DELTA VALUE).



WARNING:  Note that the proposed lemma LESSP-AS-AT-LEAST-MOREP is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and two replacement rules.


This conjecture can be simplified, using the abbreviations AT-LEAST-MOREP and
IMPLIES, to the formula:

      (IMPLIES (NOT (LESSP VALUE (PLUS BASE DELTA)))
               (AND (EQUAL (LESSP VALUE X)
                           (NOT (AT-LEAST-MOREP X 0 VALUE)))
                    (EQUAL (LESSP X VALUE)
                           (AT-LEAST-MOREP X 1 VALUE)))).

This simplifies, applying PLUS-ZERO-ARG2, SUB1-ADD1, and PLUS-ADD1-ARG2, and
opening up the functions ZEROP, AT-LEAST-MOREP, NOT, LESSP, NUMBERP, and AND,
to seven new conjectures:

Case 7. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (NUMBERP X)))
                 (EQUAL (LESSP VALUE X)
                        (LESSP VALUE 0))),

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

        T.

Case 6. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (EQUAL VALUE 0))
                 (EQUAL (LESSP X VALUE) F)),

  which again simplifies, applying the lemma EQUAL-PLUS-0, and unfolding the
  functions EQUAL and LESSP, to:

        T.

Case 5. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (NUMBERP VALUE)))
                 (EQUAL (LESSP X VALUE) F)),

  which again simplifies, rewriting with EQUAL-PLUS-0, and expanding the
  functions LESSP and EQUAL, to:

        T.

Case 4. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NUMBERP X)
                      (LESSP (SUB1 VALUE) X))
                 (EQUAL (LESSP X VALUE) F)).

  This again simplifies, trivially, to the new goal:

        (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NUMBERP X)
                      (LESSP (SUB1 VALUE) X))
                 (NOT (LESSP X VALUE))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (NUMBERP X))
                      (LESSP (SUB1 VALUE) 0))
                 (EQUAL (LESSP X VALUE) F)),

  which again simplifies, unfolding EQUAL and LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (EQUAL VALUE 0))
                      (NUMBERP VALUE)
                      (NUMBERP X)
                      (NOT (LESSP (SUB1 VALUE) X)))
                 (EQUAL (LESSP X VALUE) T)),

  which again simplifies, obviously, to:

        (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (EQUAL VALUE 0))
                      (NUMBERP VALUE)
                      (NUMBERP X)
                      (NOT (LESSP (SUB1 VALUE) X)))
                 (LESSP X VALUE)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP VALUE (PLUS BASE DELTA)))
                      (NOT (EQUAL VALUE 0))
                      (NUMBERP VALUE)
                      (NOT (NUMBERP X))
                      (NOT (LESSP (SUB1 VALUE) 0)))
                 (EQUAL (LESSP X VALUE) T)),

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

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-AS-AT-LEAST-MOREP


(DISABLE AT-LEAST-MOREP)

[ 0.0 0.0 0.0 ]

AT-LEAST-MOREP-OFF


(DEFN NAT-TO-BV
      (NAT SIZE)
      (IF (ZEROP SIZE)
          NIL
          (IF (LESSP NAT (EXP 2 (SUB1 SIZE)))
              (CONS 0 (NAT-TO-BV NAT (SUB1 SIZE)))
              (CONS 1
                    (NAT-TO-BV (DIFFERENCE NAT (EXP 2 (SUB1 SIZE)))
                               (SUB1 SIZE))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT SIZE) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, NAT-TO-BV is
accepted under the definitional principle.  Observe that:
      (OR (LITATOM (NAT-TO-BV NAT SIZE))
          (LISTP (NAT-TO-BV NAT SIZE)))
is a theorem.




[ 0.0 0.0 0.0 ]

NAT-TO-BV


(DEFN NAT-TO-BV-STATE
      (STATE SIZE)
      (IF (LISTP STATE)
          (CONS (NAT-TO-BV (CAR STATE) SIZE)
                (NAT-TO-BV-STATE (CDR STATE) SIZE))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT STATE) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, NAT-TO-BV-STATE is accepted under the principle of
definition.  Note that:
      (OR (LITATOM (NAT-TO-BV-STATE STATE SIZE))
          (LISTP (NAT-TO-BV-STATE STATE SIZE)))
is a theorem.




[ 0.0 0.0 0.0 ]

NAT-TO-BV-STATE


(DEFN XOR-BVS-PROGRAM NIL
      '(XOR-BVS (VECS-ADDR NUMVECS)
                NIL
                (PUSH-LOCAL VECS-ADDR)
                (FETCH)
                (PUSH-LOCAL NUMVECS)
                (SUB1-NAT)
                (POP-LOCAL NUMVECS)
                (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                (TEST-NAT-AND-JUMP ZERO DONE)
                (PUSH-LOCAL NUMVECS)
                (SUB1-NAT)
                (POP-LOCAL NUMVECS)
                (PUSH-LOCAL VECS-ADDR)
                (PUSH-CONSTANT (NAT 1))
                (ADD-ADDR)
                (SET-LOCAL VECS-ADDR)
                (FETCH)
                (XOR-BITV)
                (JUMP LOOP)
                (DL DONE NIL (RET))))

     Note that (LISTP (XOR-BVS-PROGRAM)) is a theorem.




[ 0.0 0.0 0.0 ]

XOR-BVS-PROGRAM


(DEFN BIT-VECTORS-PITON
      (ARRAY SIZE)
      (IF (LISTP ARRAY)
          (AND (LISTP (CAR ARRAY))
               (EQUAL (CAAR ARRAY) 'BITV)
               (BIT-VECTORP (CADAR ARRAY) SIZE)
               (EQUAL (CDDAR ARRAY) NIL)
               (BIT-VECTORS-PITON (CDR ARRAY) SIZE))
          (EQUAL ARRAY NIL)))

     Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT ARRAY) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, BIT-VECTORS-PITON is accepted under the
definitional principle.  Observe that:
      (OR (FALSEP (BIT-VECTORS-PITON ARRAY SIZE))
          (TRUEP (BIT-VECTORS-PITON ARRAY SIZE)))
is a theorem.




[ 0.0 0.0 0.0 ]

BIT-VECTORS-PITON


(DEFN ARRAY
      (NAME SEGMENT)
      (CDR (ASSOC NAME SEGMENT)))

   




[ 0.0 0.0 0.0 ]

ARRAY


(DEFN XOR-BVS-INPUT-CONDITIONP
      (P0)
      (AND (EQUAL (CAR (TOP (P-TEMP-STK P0)))
                  'NAT)
           (EQUAL (CAR (TOP (CDR (P-TEMP-STK P0))))
                  'ADDR)
           (EQUAL (CDADR (TOP (CDR (P-TEMP-STK P0))))
                  0)
           (LISTP (CADR (TOP (CDR (P-TEMP-STK P0)))))
           (EQUAL (CDDR (TOP (P-TEMP-STK P0)))
                  NIL)
           (EQUAL (CDDR (TOP (CDR (P-TEMP-STK P0))))
                  NIL)
           (DEFINEDP (CAADR (TOP (CDR (P-TEMP-STK P0))))
                     (P-DATA-SEGMENT P0))
           (BIT-VECTORS-PITON (ARRAY (CAADR (TOP (CDR (P-TEMP-STK P0))))
                                     (P-DATA-SEGMENT P0))
                              (P-WORD-SIZE P0))
           (EQUAL (CADR (TOP (P-TEMP-STK P0)))
                  (LENGTH (ARRAY (CAADR (TOP (CDR (P-TEMP-STK P0))))
                                 (P-DATA-SEGMENT P0))))
           (AT-LEAST-MOREP (P-CTRL-STK-SIZE (P-CTRL-STK P0))
                           4
                           (P-MAX-CTRL-STK-SIZE P0))
           (AT-LEAST-MOREP (LENGTH (P-TEMP-STK P0))
                           2
                           (P-MAX-TEMP-STK-SIZE P0))
           (NOT (ZEROP (UNTAG (TOP (P-TEMP-STK P0)))))
           (LESSP (UNTAG (TOP (P-TEMP-STK P0)))
                  (EXP 2 (P-WORD-SIZE P0)))
           (LISTP (P-CTRL-STK P0))))

     From the definition we can conclude that:
      (OR (FALSEP (XOR-BVS-INPUT-CONDITIONP P0))
          (TRUEP (XOR-BVS-INPUT-CONDITIONP P0)))
is a theorem.




[ 0.0 0.0 0.0 ]

XOR-BVS-INPUT-CONDITIONP


(DEFN XOR-BVS-CLOCK-LOOP
      (NUMVECS)
      (IF (ZEROP NUMVECS)
          3
          (PLUS 12
                (XOR-BVS-CLOCK-LOOP (SUB1 NUMVECS)))))

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




[ 0.0 0.0 0.0 ]

XOR-BVS-CLOCK-LOOP


(DEFN XOR-BVS-CLOCK
      (NUMVECS)
      (PLUS 6
            (XOR-BVS-CLOCK-LOOP (SUB1 NUMVECS))))

     From the definition we can conclude that:
      (NUMBERP (XOR-BVS-CLOCK NUMVECS))
is a theorem.




[ 0.3 0.0 0.0 ]

XOR-BVS-CLOCK


(DEFN XOR-BVS-ARRAY
      (CURRENT ARRAY N ARRAY-SIZE)
      (IF (ZEROP N)
          CURRENT
          (XOR-BVS-ARRAY (XOR-BITV CURRENT
                                   (UNTAG (GET (DIFFERENCE ARRAY-SIZE N)
                                               ARRAY)))
                         ARRAY
                         (SUB1 N)
                         ARRAY-SIZE)))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, XOR-BVS-ARRAY is accepted under
the definitional principle.  From the definition we can conclude that:
      (OR (OR (LITATOM (XOR-BVS-ARRAY CURRENT ARRAY N ARRAY-SIZE))
              (LISTP (XOR-BVS-ARRAY CURRENT ARRAY N ARRAY-SIZE)))
          (EQUAL (XOR-BVS-ARRAY CURRENT ARRAY N ARRAY-SIZE)
                 CURRENT))
is a theorem.




[ 0.0 0.0 0.0 ]

XOR-BVS-ARRAY


(PROVE-LEMMA LESSP-1-EXP
             (REWRITE)
             (EQUAL (LESSP 1 (EXP A B))
                    (AND (LESSP 1 A) (NOT (ZEROP B))))
             ((ENABLE EXP)))

This formula simplifies, opening up ZEROP, NOT, and AND, to the following four
new formulas:

Case 4. (IMPLIES (NOT (LESSP 1 A))
                 (EQUAL (LESSP 1 (EXP A B)) F)).

  This again simplifies, trivially, to the new formula:

        (IMPLIES (NOT (LESSP 1 A))
                 (NOT (LESSP 1 (EXP A B)))),

  which we will name *1.

Case 3. (IMPLIES (NOT (NUMBERP B))
                 (EQUAL (LESSP 1 (EXP A B)) F)).

  But this again simplifies, applying EXP-ZERO, and expanding the functions
  ZEROP, LESSP, and EQUAL, to:

        T.

Case 2. (IMPLIES (EQUAL B 0)
                 (EQUAL (LESSP 1 (EXP A B)) F)).

  This again simplifies, rewriting with EXP-0-ARG2, and opening up LESSP and
  EQUAL, to:

        T.

Case 1. (IMPLIES (AND (LESSP 1 A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B))
                 (EQUAL (LESSP 1 (EXP A B)) T)).

  This again simplifies, clearly, to the new conjecture:

        (IMPLIES (AND (LESSP 1 A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B))
                 (LESSP 1 (EXP A B))),

  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:

(EQUAL (LESSP 1 (EXP A B))
       (AND (LESSP 1 A) (NOT (ZEROP B)))),

named *1.  Let us appeal to the induction principle.  There are two plausible
inductions.  However, only one is unflawed.  We will induct according to the
following scheme:
      (AND (IMPLIES (ZEROP B) (p A B))
           (IMPLIES (AND (NOT (ZEROP B)) (p A (SUB1 B)))
                    (p A B))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT B) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates the following two new conjectures:

Case 2. (IMPLIES (ZEROP B)
                 (EQUAL (LESSP 1 (EXP A B))
                        (AND (LESSP 1 A) (NOT (ZEROP B))))).

  This simplifies, applying EXP-0-ARG2 and EXP-ZERO, and unfolding the
  definitions of ZEROP, LESSP, NOT, AND, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP B))
                      (EQUAL (LESSP 1 (EXP A (SUB1 B)))
                             (AND (LESSP 1 A)
                                  (NOT (ZEROP (SUB1 B))))))
                 (EQUAL (LESSP 1 (EXP A B))
                        (AND (LESSP 1 A) (NOT (ZEROP B))))),

  which simplifies, rewriting with EQUAL-SUB1-0, EXP-0-ARG2, TIMES-1-ARG1,
  COMMUTATIVITY-OF-TIMES, EXP-ADD1, EQUAL-EXP-0, EQUAL-EXP-1, and
  LESSP-1-TIMES, and unfolding the definitions of ZEROP, NOT, AND, EXP, and
  EQUAL, to the following five new conjectures:

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (EQUAL B 1)
                        (EQUAL (LESSP 1 (EXP A (SUB1 B))) F)
                        (NOT (NUMBERP A)))
                   (EQUAL (LESSP 1 0) (LESSP 1 A))).

    However this again simplifies, applying EXP-0-ARG2, and opening up EQUAL,
    NUMBERP, SUB1, and LESSP, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (NOT (LESSP 1 A))
                        (EQUAL (LESSP 1 (EXP A (SUB1 B))) F)
                        (NOT (EQUAL A 0))
                        (NUMBERP A))
                   (EQUAL A 1)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (LESSP 1 A)
                        (NOT (EQUAL B 1))
                        (EQUAL (LESSP 1 (EXP A (SUB1 B))) T))
                   (NOT (EQUAL A 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (LESSP 1 A)
                        (NOT (EQUAL B 1))
                        (EQUAL (LESSP 1 (EXP A (SUB1 B))) T))
                   (NUMBERP A)),

    which again simplifies, unfolding the function LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL B 0))
                        (NUMBERP B)
                        (LESSP 1 A)
                        (NOT (EQUAL B 1))
                        (EQUAL (LESSP 1 (EXP A (SUB1 B))) T))
                   (NOT (EQUAL A 1))),

    which again simplifies, using linear arithmetic, to:

          T.


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


[ 0.0 0.1 0.0 ]

LESSP-1-EXP


(PROVE-LEMMA BIT-VECTORS-PITON-MEANS
             (REWRITE)
             (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                           (LESSP P (LENGTH STATE)))
                      (AND (EQUAL (CAR (GET P STATE)) 'BITV)
                           (LISTP (GET P STATE))
                           (BIT-VECTORP (CADR (GET P STATE))
                                        SIZE)
                           (EQUAL (CDDR (GET P STATE)) NIL))))

WARNING:  Note that BIT-VECTORS-PITON-MEANS contains the free variable SIZE
which will be chosen by instantiating the hypothesis:
      (BIT-VECTORS-PITON STATE SIZE).



WARNING:  Note that BIT-VECTORS-PITON-MEANS contains the free variable SIZE
which will be chosen by instantiating the hypothesis:
      (BIT-VECTORS-PITON STATE SIZE).



WARNING:  Note that BIT-VECTORS-PITON-MEANS contains the free variable SIZE
which will be chosen by instantiating the hypothesis:
      (BIT-VECTORS-PITON STATE SIZE).



WARNING:  Note that the proposed lemma BIT-VECTORS-PITON-MEANS is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and four replacement rules.


This simplifies, unfolding AND, to four new conjectures:

Case 4. (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CAR (GET P STATE)) 'BITV)),

  which we will name *1.

Case 3. (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (LISTP (GET P STATE))),

  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:

(AND (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                   (LESSP P (LENGTH STATE)))
              (EQUAL (CAR (GET P STATE)) 'BITV))
     (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                   (LESSP P (LENGTH STATE)))
              (LISTP (GET P STATE)))
     (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                   (LESSP P (LENGTH STATE)))
              (BIT-VECTORP (CADR (GET P STATE))
                           SIZE))
     (IMPLIES (AND (BIT-VECTORS-PITON STATE SIZE)
                   (LESSP P (LENGTH STATE)))
              (EQUAL (CDDR (GET P STATE)) NIL))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  The
recursive terms in the conjecture suggest 16 inductions.  However, they merge
into one likely candidate induction.  We will induct according to the
following scheme:
      (AND (IMPLIES (AND (LISTP STATE)
                         (p (SUB1 P) (CDR STATE) SIZE))
                    (p P STATE SIZE))
           (IMPLIES (NOT (LISTP STATE))
                    (p P STATE SIZE))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT STATE) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  Note, however, the inductive instance chosen
for P.  The above induction scheme produces the following 16 new goals:

Case 16.(IMPLIES (AND (LISTP STATE)
                      (NOT (BIT-VECTORS-PITON (CDR STATE) SIZE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CAR (GET P STATE)) 'BITV)).

  This simplifies, expanding the definition of BIT-VECTORS-PITON, to:

        T.

Case 15.(IMPLIES (AND (LISTP STATE)
                      (NOT (LESSP (SUB1 P) (LENGTH (CDR STATE))))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CAR (GET P STATE)) 'BITV)).

  This simplifies, rewriting with SUB1-ADD1, and opening up the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 14.(IMPLIES (AND (LISTP STATE)
                      (EQUAL (CAR (GET (SUB1 P) (CDR STATE)))
                             'BITV)
                      (LISTP (GET (SUB1 P) (CDR STATE)))
                      (BIT-VECTORP (CADR (GET (SUB1 P) (CDR STATE)))
                                   SIZE)
                      (EQUAL (CDDR (GET (SUB1 P) (CDR STATE)))
                             NIL)
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CAR (GET P STATE)) 'BITV)),

  which simplifies, applying SUB1-ADD1, and unfolding the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 13.(IMPLIES (AND (NOT (LISTP STATE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CAR (GET P STATE)) 'BITV)).

  This simplifies, opening up the functions BIT-VECTORS-PITON, LENGTH, EQUAL,
  and LESSP, to:

        T.

Case 12.(IMPLIES (AND (LISTP STATE)
                      (NOT (BIT-VECTORS-PITON (CDR STATE) SIZE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (LISTP (GET P STATE))).

  This simplifies, expanding the function BIT-VECTORS-PITON, to:

        T.

Case 11.(IMPLIES (AND (LISTP STATE)
                      (NOT (LESSP (SUB1 P) (LENGTH (CDR STATE))))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (LISTP (GET P STATE))).

  This simplifies, rewriting with SUB1-ADD1, and unfolding the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 10.(IMPLIES (AND (LISTP STATE)
                      (EQUAL (CAR (GET (SUB1 P) (CDR STATE)))
                             'BITV)
                      (LISTP (GET (SUB1 P) (CDR STATE)))
                      (BIT-VECTORP (CADR (GET (SUB1 P) (CDR STATE)))
                                   SIZE)
                      (EQUAL (CDDR (GET (SUB1 P) (CDR STATE)))
                             NIL)
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (LISTP (GET P STATE))),

  which simplifies, appealing to the lemma SUB1-ADD1, and unfolding the
  functions BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 9. (IMPLIES (AND (NOT (LISTP STATE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (LISTP (GET P STATE))),

  which simplifies, opening up BIT-VECTORS-PITON, LENGTH, EQUAL, and LESSP, to:

        T.

Case 8. (IMPLIES (AND (LISTP STATE)
                      (NOT (BIT-VECTORS-PITON (CDR STATE) SIZE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (BIT-VECTORP (CADR (GET P STATE))
                              SIZE)),

  which simplifies, opening up the definition of BIT-VECTORS-PITON, to:

        T.

Case 7. (IMPLIES (AND (LISTP STATE)
                      (NOT (LESSP (SUB1 P) (LENGTH (CDR STATE))))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (BIT-VECTORP (CADR (GET P STATE))
                              SIZE)),

  which simplifies, applying SUB1-ADD1, and expanding the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 6. (IMPLIES (AND (LISTP STATE)
                      (EQUAL (CAR (GET (SUB1 P) (CDR STATE)))
                             'BITV)
                      (LISTP (GET (SUB1 P) (CDR STATE)))
                      (BIT-VECTORP (CADR (GET (SUB1 P) (CDR STATE)))
                                   SIZE)
                      (EQUAL (CDDR (GET (SUB1 P) (CDR STATE)))
                             NIL)
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (BIT-VECTORP (CADR (GET P STATE))
                              SIZE)).

  This simplifies, applying SUB1-ADD1, and expanding BIT-VECTORS-PITON, LENGTH,
  LESSP, EQUAL, and GET, to:

        T.

Case 5. (IMPLIES (AND (NOT (LISTP STATE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (BIT-VECTORP (CADR (GET P STATE))
                              SIZE)),

  which simplifies, unfolding the definitions of BIT-VECTORS-PITON, LENGTH,
  EQUAL, and LESSP, to:

        T.

Case 4. (IMPLIES (AND (LISTP STATE)
                      (NOT (BIT-VECTORS-PITON (CDR STATE) SIZE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CDDR (GET P STATE)) NIL)),

  which simplifies, expanding BIT-VECTORS-PITON, to:

        T.

Case 3. (IMPLIES (AND (LISTP STATE)
                      (NOT (LESSP (SUB1 P) (LENGTH (CDR STATE))))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CDDR (GET P STATE)) NIL)),

  which simplifies, rewriting with SUB1-ADD1, and expanding the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 2. (IMPLIES (AND (LISTP STATE)
                      (EQUAL (CAR (GET (SUB1 P) (CDR STATE)))
                             'BITV)
                      (LISTP (GET (SUB1 P) (CDR STATE)))
                      (BIT-VECTORP (CADR (GET (SUB1 P) (CDR STATE)))
                                   SIZE)
                      (EQUAL (CDDR (GET (SUB1 P) (CDR STATE)))
                             NIL)
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CDDR (GET P STATE)) NIL)).

  This simplifies, applying SUB1-ADD1, and unfolding the functions
  BIT-VECTORS-PITON, LENGTH, LESSP, EQUAL, and GET, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP STATE))
                      (BIT-VECTORS-PITON STATE SIZE)
                      (LESSP P (LENGTH STATE)))
                 (EQUAL (CDDR (GET P STATE)) NIL)),

  which simplifies, unfolding the definitions of BIT-VECTORS-PITON, LENGTH,
  EQUAL, and LESSP, to:

        T.


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


[ 0.0 0.2 0.0 ]

BIT-VECTORS-PITON-MEANS


(DEFN XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT
 (I CURRENT N S DATA-SEGMENT)
 (IF
  (ZEROP I)
  T
  (XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT
                                 (SUB1 I)
                                 (XOR-BITV CURRENT
                                           (CADR (GET (DIFFERENCE N I)
                                                      (ARRAY S DATA-SEGMENT))))
                                 N S DATA-SEGMENT)))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT I) decreases according to the well-founded
relation LESSP in each recursive call.  Hence,
      XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT
is accepted under the principle of definition.  Observe that:
      (TRUEP (XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT I CURRENT N S
                                                      DATA-SEGMENT))
is a theorem.




[ 0.0 0.0 0.0 ]

XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT


(ENABLE BIT-VECTORP-XOR-BITV)

[ 0.0 0.0 0.0 ]

BIT-VECTORP-XOR-BITV-ON


(PROVE-LEMMA XOR-BVS-LOOP-CORRECTNESS-GENERAL NIL
 (IMPLIES
  (AND (LESSP (LENGTH (ARRAY S DATA-SEGMENT))
              (EXP 2 WORD-SIZE))
       (NOT (ZEROP WORD-SIZE))
       (LISTP CTRL-STK)
       (BIT-VECTORS-PITON (ARRAY S DATA-SEGMENT)
                          WORD-SIZE)
       (AT-LEAST-MOREP (LENGTH TEMP-STK)
                       3 MAX-TEMP-STK-SIZE)
       (EQUAL (DEFINITION 'XOR-BVS PROG-SEGMENT)
              (XOR-BVS-PROGRAM))
       (DEFINEDP S DATA-SEGMENT)
       (NUMBERP I)
       (LESSP I N)
       (BIT-VECTORP CURRENT WORD-SIZE)
       (EQUAL N
              (LENGTH (ARRAY S DATA-SEGMENT))))
  (EQUAL
   (P (P-STATE '(PC (XOR-BVS . 5))
               (CONS (LIST (LIST (CONS 'VECS-ADDR
                                       (LIST 'ADDR
                                             (CONS S (SUB1 (DIFFERENCE N I)))))
                                 (CONS 'NUMVECS (LIST 'NAT I)))
                           RET-PC)
                     CTRL-STK)
               (CONS (LIST 'BITV CURRENT) TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN)
      (XOR-BVS-CLOCK-LOOP I))
   (P-STATE RET-PC CTRL-STK
            (CONS (LIST 'BITV
                        (XOR-BVS-ARRAY CURRENT
                                       (ARRAY S DATA-SEGMENT)
                                       I N))
                  TEMP-STK)
            PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
            WORD-SIZE 'RUN)))
 ((INDUCT (XOR-BVS-LOOP-CORRECTNESS-GENERAL-INDUCT I CURRENT N S
                                                   DATA-SEGMENT))))

This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, AND, XOR-BVS-PROGRAM, DEFINITION, and ARRAY, to two new goals:

Case 2. (IMPLIES
         (AND (ZEROP I)
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (EQUAL WORD-SIZE 0))
              (NUMBERP WORD-SIZE)
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (NUMBERP I)
              (LESSP I N)
              (BIT-VECTORP CURRENT WORD-SIZE)
              (EQUAL N
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
         (EQUAL
          (P (P-STATE '(PC (XOR-BVS . 5))
                      (CONS (LIST (LIST (LIST 'VECS-ADDR
                                              'ADDR
                                              (CONS S (SUB1 (DIFFERENCE N I))))
                                        (LIST 'NUMVECS 'NAT I))
                                  RET-PC)
                            CTRL-STK)
                      (CONS (LIST 'BITV CURRENT) TEMP-STK)
                      PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                      MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)
             (XOR-BVS-CLOCK-LOOP I))
          (P-STATE RET-PC CTRL-STK
                   (CONS (LIST 'BITV
                               (XOR-BVS-ARRAY CURRENT
                                              (CDR (ASSOC S DATA-SEGMENT))
                                              I N))
                         TEMP-STK)
                   PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                   MAX-TEMP-STK-SIZE WORD-SIZE 'RUN))),

  which simplifies, rewriting with P-STEP1-OPENER, P-WORD-SIZE-P-STATE,
  P-MAX-CTRL-STK-SIZE-P-STATE, P-DATA-SEGMENT-P-STATE, CAR-CONS,
  P-CTRL-STK-P-STATE, LESSP-AS-AT-LEAST-MOREP, AT-LEAST-MOREP-NORMALIZE,
  AT-LEAST-MOREP-LINEAR, P-MAX-TEMP-STK-SIZE-P-STATE, CDR-CONS,
  P-TEMP-STK-P-STATE, P-PC-P-STATE, P-PROG-SEGMENT-P-STATE, P-PSW-P-STATE,
  EQUAL-EXP-0, and P-OPENER, and expanding ZEROP, NUMBERP, EQUAL, LESSP,
  DIFFERENCE, CONS, XOR-BVS-CLOCK-LOOP, P-INS-STEP, PUSH, LOCAL-VAR-VALUE, TOP,
  BINDINGS, ASSOC, DEFINIENS, CDR, ADD1-P-PC, ADD1-ADDR, P-PUSH-LOCAL-STEP,
  P-INS-OKP, CAR, ADD1, LENGTH, P-PUSH-LOCAL-OKP, P-CURRENT-INSTRUCTION,
  OFFSET, DEFINITION, AREA-NAME, P-CURRENT-PROGRAM, PROGRAM-BODY, GET, UNLABEL,
  P-STEP, P-TEST-AND-JUMP-STEP, PC, POP, P-TEST-NAT-AND-JUMP-STEP,
  P-TEST-AND-JUMP-OKP, P-OBJECTP, LISTP, SMALL-NATURALP, TYPE, P-OBJECTP-TYPE,
  P-TEST-NATP, UNTAG, P-TEST-NAT-AND-JUMP-OKP, RET-PC, P-RET-STEP, P-RET-OKP,
  and XOR-BVS-ARRAY, to:

        T.

Case 1. (IMPLIES
         (AND
          (NOT (EQUAL I 0))
          (NUMBERP I)
          (IMPLIES
           (AND
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (ZEROP WORD-SIZE))
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (NUMBERP (SUB1 I))
              (LESSP (SUB1 I) N)
              (BIT-VECTORP (XOR-BITV CURRENT
                                     (CADR (GET (DIFFERENCE N I)
                                                (CDR (ASSOC S DATA-SEGMENT)))))
                           WORD-SIZE)
              (EQUAL N
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 5))
              (CONS (LIST (LIST (LIST 'VECS-ADDR
                                      'ADDR
                                      (CONS S
                                            (SUB1 (DIFFERENCE N (SUB1 I)))))
                                (LIST 'NUMVECS 'NAT (SUB1 I)))
                          RET-PC)
                    CTRL-STK)
              (CONS (LIST 'BITV
                          (XOR-BITV CURRENT
                                    (CADR (GET (DIFFERENCE N I)
                                               (CDR (ASSOC S DATA-SEGMENT))))))
                    TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN)
             (XOR-BVS-CLOCK-LOOP (SUB1 I)))
            (P-STATE RET-PC CTRL-STK
             (CONS
              (LIST 'BITV
               (XOR-BVS-ARRAY
                           (XOR-BITV CURRENT
                                     (CADR (GET (DIFFERENCE N I)
                                                (CDR (ASSOC S DATA-SEGMENT)))))
                           (CDR (ASSOC S DATA-SEGMENT))
                           (SUB1 I)
                           N))
              TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN)))
          (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                 (EXP 2 WORD-SIZE))
          (NOT (EQUAL WORD-SIZE 0))
          (NUMBERP WORD-SIZE)
          (LISTP CTRL-STK)
          (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                             WORD-SIZE)
          (AT-LEAST-MOREP (LENGTH TEMP-STK)
                          3 MAX-TEMP-STK-SIZE)
          (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                 '(XOR-BVS (VECS-ADDR NUMVECS)
                           NIL
                           (PUSH-LOCAL VECS-ADDR)
                           (FETCH)
                           (PUSH-LOCAL NUMVECS)
                           (SUB1-NAT)
                           (POP-LOCAL NUMVECS)
                           (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                           (TEST-NAT-AND-JUMP ZERO DONE)
                           (PUSH-LOCAL NUMVECS)
                           (SUB1-NAT)
                           (POP-LOCAL NUMVECS)
                           (PUSH-LOCAL VECS-ADDR)
                           (PUSH-CONSTANT (NAT 1))
                           (ADD-ADDR)
                           (SET-LOCAL VECS-ADDR)
                           (FETCH)
                           (XOR-BITV)
                           (JUMP LOOP)
                           (DL DONE NIL (RET))))
          (DEFINEDP S DATA-SEGMENT)
          (LESSP I N)
          (BIT-VECTORP CURRENT WORD-SIZE)
          (EQUAL N
                 (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
         (EQUAL
          (P (P-STATE '(PC (XOR-BVS . 5))
                      (CONS (LIST (LIST (LIST 'VECS-ADDR
                                              'ADDR
                                              (CONS S (SUB1 (DIFFERENCE N I))))
                                        (LIST 'NUMVECS 'NAT I))
                                  RET-PC)
                            CTRL-STK)
                      (CONS (LIST 'BITV CURRENT) TEMP-STK)
                      PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                      MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)
             (XOR-BVS-CLOCK-LOOP I))
          (P-STATE RET-PC CTRL-STK
                   (CONS (LIST 'BITV
                               (XOR-BVS-ARRAY CURRENT
                                              (CDR (ASSOC S DATA-SEGMENT))
                                              I N))
                         TEMP-STK)
                   PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                   MAX-TEMP-STK-SIZE WORD-SIZE 'RUN))).

  This simplifies, using linear arithmetic, applying AT-LEAST-MOREP-LINEAR,
  BIT-VECTORS-PITON-MEANS, BIT-VECTORP-XOR-BITV, DIFFERENCE-SUB1-ARG2,
  P-PC-P-STATE, PLUS-ADD1-ARG1, P-STEP1-OPENER, P-WORD-SIZE-P-STATE,
  P-MAX-CTRL-STK-SIZE-P-STATE, P-DATA-SEGMENT-P-STATE, CAR-CONS,
  P-CTRL-STK-P-STATE, LESSP-AS-AT-LEAST-MOREP, AT-LEAST-MOREP-NORMALIZE,
  P-MAX-TEMP-STK-SIZE-P-STATE, CDR-CONS, P-TEMP-STK-P-STATE,
  P-PROG-SEGMENT-P-STATE, P-PSW-P-STATE, and P-OPENER, and opening up ZEROP,
  NOT, LESSP, EQUAL, AND, IMPLIES, PLUS, XOR-BVS-CLOCK-LOOP, P-INS-STEP, PUSH,
  LOCAL-VAR-VALUE, TOP, BINDINGS, ASSOC, DEFINIENS, CDR, ADD1-P-PC, ADD1-ADDR,
  P-PUSH-LOCAL-STEP, P-INS-OKP, CAR, ADD1, LENGTH, P-PUSH-LOCAL-OKP, CONS,
  P-CURRENT-INSTRUCTION, OFFSET, DEFINITION, AREA-NAME, P-CURRENT-PROGRAM,
  PROGRAM-BODY, GET, UNLABEL, P-STEP, P-HALT, X-Y-ERROR-MSG,
  P-TEST-AND-JUMP-STEP, POP, P-TEST-NAT-AND-JUMP-STEP, P-TEST-AND-JUMP-OKP,
  P-OBJECTP, SMALL-NATURALP, TYPE, P-OBJECTP-TYPE, P-TEST-NATP, UNTAG, and
  P-TEST-NAT-AND-JUMP-OKP, to six new conjectures:

  Case 1.6.
          (IMPLIES
           (AND
            (NOT (EQUAL I 0))
            (NUMBERP I)
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   I)
            (IMPLIES
             (AND
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (ZEROP WORD-SIZE))
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET)))
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (NUMBERP (SUB1 I))
              (LESSP (SUB1 I)
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (BIT-VECTORP
               (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
               WORD-SIZE)
              (EQUAL (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
             (EQUAL
              (P
               (P-STATE
                '(PC (XOR-BVS . 5))
                (CONS
                 (LIST
                  (LIST
                   (LIST 'VECS-ADDR
                    'ADDR
                    (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          (SUB1 I)))))
                   (LIST 'NUMVECS 'NAT (SUB1 I)))
                  RET-PC)
                 CTRL-STK)
                (CONS
                 (LIST 'BITV
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                 TEMP-STK)
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN)
               (XOR-BVS-CLOCK-LOOP (SUB1 I)))
              (P-STATE RET-PC CTRL-STK
               (CONS
                (LIST 'BITV
                 (XOR-BVS-ARRAY
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                  (CDR (ASSOC S DATA-SEGMENT))
                  (SUB1 I)
                  (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN)))
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   (EXP 2 WORD-SIZE))
            (NOT (EQUAL WORD-SIZE 0))
            (NUMBERP WORD-SIZE)
            (LISTP CTRL-STK)
            (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                               WORD-SIZE)
            (AT-LEAST-MOREP (LENGTH TEMP-STK)
                            3 MAX-TEMP-STK-SIZE)
            (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                   '(XOR-BVS (VECS-ADDR NUMVECS)
                             NIL
                             (PUSH-LOCAL VECS-ADDR)
                             (FETCH)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                             (TEST-NAT-AND-JUMP ZERO DONE)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (PUSH-LOCAL VECS-ADDR)
                             (PUSH-CONSTANT (NAT 1))
                             (ADD-ADDR)
                             (SET-LOCAL VECS-ADDR)
                             (FETCH)
                             (XOR-BITV)
                             (JUMP LOOP)
                             (DL DONE NIL (RET))))
            (DEFINEDP S DATA-SEGMENT)
            (LESSP I
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
            (BIT-VECTORP CURRENT WORD-SIZE)
            (NOT (LESSP I (EXP 2 WORD-SIZE))))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 6))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'NAT I)
                    (CONS (LIST 'BITV CURRENT) TEMP-STK))
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'ILLEGAL-TEST-NAT-AND-JUMP-INSTRUCTION)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.5.
          (IMPLIES
           (AND
            (NOT (EQUAL I 0))
            (NUMBERP I)
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   I)
            (IMPLIES
             (AND
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (ZEROP WORD-SIZE))
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET)))
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (NUMBERP (SUB1 I))
              (LESSP (SUB1 I)
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (BIT-VECTORP
               (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
               WORD-SIZE)
              (EQUAL (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
             (EQUAL
              (P
               (P-STATE
                '(PC (XOR-BVS . 5))
                (CONS
                 (LIST
                  (LIST
                   (LIST 'VECS-ADDR
                    'ADDR
                    (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          (SUB1 I)))))
                   (LIST 'NUMVECS 'NAT (SUB1 I)))
                  RET-PC)
                 CTRL-STK)
                (CONS
                 (LIST 'BITV
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                 TEMP-STK)
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN)
               (XOR-BVS-CLOCK-LOOP (SUB1 I)))
              (P-STATE RET-PC CTRL-STK
               (CONS
                (LIST 'BITV
                 (XOR-BVS-ARRAY
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                  (CDR (ASSOC S DATA-SEGMENT))
                  (SUB1 I)
                  (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN)))
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   (EXP 2 WORD-SIZE))
            (NOT (EQUAL WORD-SIZE 0))
            (NUMBERP WORD-SIZE)
            (LISTP CTRL-STK)
            (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                               WORD-SIZE)
            (AT-LEAST-MOREP (LENGTH TEMP-STK)
                            3 MAX-TEMP-STK-SIZE)
            (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                   '(XOR-BVS (VECS-ADDR NUMVECS)
                             NIL
                             (PUSH-LOCAL VECS-ADDR)
                             (FETCH)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                             (TEST-NAT-AND-JUMP ZERO DONE)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (PUSH-LOCAL VECS-ADDR)
                             (PUSH-CONSTANT (NAT 1))
                             (ADD-ADDR)
                             (SET-LOCAL VECS-ADDR)
                             (FETCH)
                             (XOR-BITV)
                             (JUMP LOOP)
                             (DL DONE NIL (RET))))
            (DEFINEDP S DATA-SEGMENT)
            (LESSP I
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
            (BIT-VECTORP CURRENT WORD-SIZE)
            (LESSP I (EXP 2 WORD-SIZE)))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 7))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'BITV CURRENT) TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES
           (AND (NOT (EQUAL I 0))
                (NUMBERP I)
                (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                            I))
                (NOT (LESSP (SUB1 I)
                            (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                       (EXP 2 WORD-SIZE))
                (NOT (EQUAL WORD-SIZE 0))
                (NUMBERP WORD-SIZE)
                (LISTP CTRL-STK)
                (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                   WORD-SIZE)
                (AT-LEAST-MOREP (LENGTH TEMP-STK)
                                3 MAX-TEMP-STK-SIZE)
                (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                       '(XOR-BVS (VECS-ADDR NUMVECS)
                                 NIL
                                 (PUSH-LOCAL VECS-ADDR)
                                 (FETCH)
                                 (PUSH-LOCAL NUMVECS)
                                 (SUB1-NAT)
                                 (POP-LOCAL NUMVECS)
                                 (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                                 (TEST-NAT-AND-JUMP ZERO DONE)
                                 (PUSH-LOCAL NUMVECS)
                                 (SUB1-NAT)
                                 (POP-LOCAL NUMVECS)
                                 (PUSH-LOCAL VECS-ADDR)
                                 (PUSH-CONSTANT (NAT 1))
                                 (ADD-ADDR)
                                 (SET-LOCAL VECS-ADDR)
                                 (FETCH)
                                 (XOR-BITV)
                                 (JUMP LOOP)
                                 (DL DONE NIL (RET))))
                (DEFINEDP S DATA-SEGMENT)
                (LESSP I
                       (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
                (BIT-VECTORP CURRENT WORD-SIZE)
                (NOT (LESSP I (EXP 2 WORD-SIZE))))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 6))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'NAT I)
                    (CONS (LIST 'BITV CURRENT) TEMP-STK))
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'ILLEGAL-TEST-NAT-AND-JUMP-INSTRUCTION)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES
           (AND (NOT (EQUAL I 0))
                (NUMBERP I)
                (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                            I))
                (NOT (LESSP (SUB1 I)
                            (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                       (EXP 2 WORD-SIZE))
                (NOT (EQUAL WORD-SIZE 0))
                (NUMBERP WORD-SIZE)
                (LISTP CTRL-STK)
                (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                   WORD-SIZE)
                (AT-LEAST-MOREP (LENGTH TEMP-STK)
                                3 MAX-TEMP-STK-SIZE)
                (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                       '(XOR-BVS (VECS-ADDR NUMVECS)
                                 NIL
                                 (PUSH-LOCAL VECS-ADDR)
                                 (FETCH)
                                 (PUSH-LOCAL NUMVECS)
                                 (SUB1-NAT)
                                 (POP-LOCAL NUMVECS)
                                 (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                                 (TEST-NAT-AND-JUMP ZERO DONE)
                                 (PUSH-LOCAL NUMVECS)
                                 (SUB1-NAT)
                                 (POP-LOCAL NUMVECS)
                                 (PUSH-LOCAL VECS-ADDR)
                                 (PUSH-CONSTANT (NAT 1))
                                 (ADD-ADDR)
                                 (SET-LOCAL VECS-ADDR)
                                 (FETCH)
                                 (XOR-BITV)
                                 (JUMP LOOP)
                                 (DL DONE NIL (RET))))
                (DEFINEDP S DATA-SEGMENT)
                (LESSP I
                       (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
                (BIT-VECTORP CURRENT WORD-SIZE)
                (LESSP I (EXP 2 WORD-SIZE)))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 7))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'BITV CURRENT) TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES
           (AND
            (NOT (EQUAL I 0))
            (NUMBERP I)
            (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                        I))
            (EQUAL
             (P
              (P-STATE
               '(PC (XOR-BVS . 5))
               (CONS
                (LIST
                 (LIST
                  (LIST 'VECS-ADDR
                   'ADDR
                   (CONS S
                    (SUB1
                        (ADD1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))))
                  (LIST 'NUMVECS 'NAT (SUB1 I)))
                 RET-PC)
                CTRL-STK)
               (CONS
                (LIST 'BITV
                 (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN)
              (XOR-BVS-CLOCK-LOOP (SUB1 I)))
             (P-STATE RET-PC CTRL-STK
              (CONS
               (LIST 'BITV
                (XOR-BVS-ARRAY
                 (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                 (CDR (ASSOC S DATA-SEGMENT))
                 (SUB1 I)
                 (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
               TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN))
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   (EXP 2 WORD-SIZE))
            (NOT (EQUAL WORD-SIZE 0))
            (NUMBERP WORD-SIZE)
            (LISTP CTRL-STK)
            (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                               WORD-SIZE)
            (AT-LEAST-MOREP (LENGTH TEMP-STK)
                            3 MAX-TEMP-STK-SIZE)
            (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                   '(XOR-BVS (VECS-ADDR NUMVECS)
                             NIL
                             (PUSH-LOCAL VECS-ADDR)
                             (FETCH)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                             (TEST-NAT-AND-JUMP ZERO DONE)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (PUSH-LOCAL VECS-ADDR)
                             (PUSH-CONSTANT (NAT 1))
                             (ADD-ADDR)
                             (SET-LOCAL VECS-ADDR)
                             (FETCH)
                             (XOR-BITV)
                             (JUMP LOOP)
                             (DL DONE NIL (RET))))
            (DEFINEDP S DATA-SEGMENT)
            (LESSP I
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
            (BIT-VECTORP CURRENT WORD-SIZE)
            (NOT (LESSP I (EXP 2 WORD-SIZE))))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 6))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'NAT I)
                    (CONS (LIST 'BITV CURRENT) TEMP-STK))
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'ILLEGAL-TEST-NAT-AND-JUMP-INSTRUCTION)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES
           (AND
            (NOT (EQUAL I 0))
            (NUMBERP I)
            (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                        I))
            (EQUAL
             (P
              (P-STATE
               '(PC (XOR-BVS . 5))
               (CONS
                (LIST
                 (LIST
                  (LIST 'VECS-ADDR
                   'ADDR
                   (CONS S
                    (SUB1
                        (ADD1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))))
                  (LIST 'NUMVECS 'NAT (SUB1 I)))
                 RET-PC)
                CTRL-STK)
               (CONS
                (LIST 'BITV
                 (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN)
              (XOR-BVS-CLOCK-LOOP (SUB1 I)))
             (P-STATE RET-PC CTRL-STK
              (CONS
               (LIST 'BITV
                (XOR-BVS-ARRAY
                 (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                 (CDR (ASSOC S DATA-SEGMENT))
                 (SUB1 I)
                 (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
               TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN))
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   (EXP 2 WORD-SIZE))
            (NOT (EQUAL WORD-SIZE 0))
            (NUMBERP WORD-SIZE)
            (LISTP CTRL-STK)
            (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                               WORD-SIZE)
            (AT-LEAST-MOREP (LENGTH TEMP-STK)
                            3 MAX-TEMP-STK-SIZE)
            (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                   '(XOR-BVS (VECS-ADDR NUMVECS)
                             NIL
                             (PUSH-LOCAL VECS-ADDR)
                             (FETCH)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                             (TEST-NAT-AND-JUMP ZERO DONE)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (PUSH-LOCAL VECS-ADDR)
                             (PUSH-CONSTANT (NAT 1))
                             (ADD-ADDR)
                             (SET-LOCAL VECS-ADDR)
                             (FETCH)
                             (XOR-BITV)
                             (JUMP LOOP)
                             (DL DONE NIL (RET))))
            (DEFINEDP S DATA-SEGMENT)
            (LESSP I
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
            (BIT-VECTORP CURRENT WORD-SIZE)
            (LESSP I (EXP 2 WORD-SIZE)))
           (EQUAL
            (P
             (P-STATE
              '(PC (XOR-BVS . 7))
              (CONS
               (LIST
                (LIST
                 (LIST 'VECS-ADDR
                  'ADDR
                  (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                 (LIST 'NUMVECS 'NAT I))
                RET-PC)
               CTRL-STK)
              (CONS (LIST 'BITV CURRENT) TEMP-STK)
              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
              WORD-SIZE 'RUN)
             (ADD1
              (ADD1
               (ADD1
                (ADD1
                 (ADD1
                  (ADD1
                   (ADD1
                     (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))))))))
            (P-STATE RET-PC CTRL-STK
             (CONS (LIST 'BITV
                         (XOR-BVS-ARRAY CURRENT
                                        (CDR (ASSOC S DATA-SEGMENT))
                                        I
                                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                   TEMP-STK)
             PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
             WORD-SIZE 'RUN))),

    which again simplifies, applying SUB1-ADD1, P-PC-P-STATE, P-STEP1-OPENER,
    P-WORD-SIZE-P-STATE, P-MAX-CTRL-STK-SIZE-P-STATE, P-DATA-SEGMENT-P-STATE,
    CAR-CONS, P-CTRL-STK-P-STATE, LESSP-AS-AT-LEAST-MOREP,
    AT-LEAST-MOREP-NORMALIZE, AT-LEAST-MOREP-LINEAR,
    P-MAX-TEMP-STK-SIZE-P-STATE, CDR-CONS, P-TEMP-STK-P-STATE,
    P-PROG-SEGMENT-P-STATE, P-PSW-P-STATE, PLUS-ADD1-ARG2, ADD1-SUB1,
    EQUAL-DIFFERENCE-0, PLUS-ZERO-ARG2, LESSP-1-EXP, and P-OPENER, and opening
    up P-INS-STEP, PUSH, LOCAL-VAR-VALUE, TOP, BINDINGS, ASSOC, DEFINIENS, CDR,
    ADD1-P-PC, ADD1-ADDR, P-PUSH-LOCAL-STEP, P-INS-OKP, CAR, LESSP, ADD1,
    LENGTH, P-PUSH-LOCAL-OKP, CONS, P-CURRENT-INSTRUCTION, OFFSET, DEFINITION,
    AREA-NAME, P-CURRENT-PROGRAM, PROGRAM-BODY, GET, UNLABEL, EQUAL, P-STEP,
    POP, TAG, P-SUB1-NAT-STEP, P-OBJECTP-TYPE, TYPE, SMALL-NATURALP, UNTAG,
    P-OBJECTP, P-SUB1-NAT-OKP, SET-LOCAL-VAR-VALUE, PUT-ASSOC, PUT-VALUE,
    RET-PC, P-FRAME, P-POP-LOCAL-STEP, P-POP-LOCAL-OKP, UNABBREVIATE-CONSTANT,
    LISTP, P-PUSH-CONSTANT-STEP, P-PUSH-CONSTANT-OKP, P-HALT, X-Y-ERROR-MSG,
    P-ADD-ADDR-STEP, ADD-ADDR, ZEROP, ADD-ADP, ADPP, ADP-OFFSET, ADP-NAME,
    TOP1, NUMBERP, P-ADD-ADDR-OKP, and XOR-BVS-ARRAY, to the following three
    new conjectures:

    Case 1.1.3.
            (IMPLIES
             (AND
              (NOT (EQUAL I 0))
              (NUMBERP I)
              (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                          I))
              (EQUAL
               (P
                (P-STATE
                 '(PC (XOR-BVS . 5))
                 (CONS
                  (LIST
                   (LIST
                    (LIST 'VECS-ADDR
                        'ADDR
                        (CONS S
                              (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))
                    (LIST 'NUMVECS 'NAT (SUB1 I)))
                   RET-PC)
                  CTRL-STK)
                 (CONS
                  (LIST 'BITV
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                  TEMP-STK)
                 PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                 WORD-SIZE 'RUN)
                (XOR-BVS-CLOCK-LOOP (SUB1 I)))
               (P-STATE RET-PC CTRL-STK
                (CONS
                 (LIST 'BITV
                  (XOR-BVS-ARRAY
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                   (CDR (ASSOC S DATA-SEGMENT))
                   (SUB1 I)
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                 TEMP-STK)
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN))
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (EQUAL WORD-SIZE 0))
              (NUMBERP WORD-SIZE)
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (LESSP I
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (BIT-VECTORP CURRENT WORD-SIZE)
              (LESSP I (EXP 2 WORD-SIZE))
              (NOT
                 (LESSP (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))
                        (LENGTH (CDR (ASSOC S DATA-SEGMENT))))))
             (EQUAL
              (P
               (P-STATE
                '(PC (XOR-BVS . 12))
                (CONS
                 (LIST
                  (LIST
                   (LIST 'VECS-ADDR
                    'ADDR
                    (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                   (LIST 'NUMVECS 'NAT (SUB1 I)))
                  RET-PC)
                 CTRL-STK)
                (CONS
                 '(NAT 1)
                 (CONS
                  (LIST 'ADDR
                   (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                  (CONS (LIST 'BITV CURRENT)
                        TEMP-STK)))
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'ILLEGAL-ADD-ADDR-INSTRUCTION)
               (ADD1 (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))
              (P-STATE RET-PC CTRL-STK
               (CONS
                (LIST 'BITV
                 (XOR-BVS-ARRAY
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                  (CDR (ASSOC S DATA-SEGMENT))
                  (SUB1 I)
                  (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN))).

      However this again simplifies, using linear arithmetic, to:

            T.

    Case 1.1.2.
            (IMPLIES
             (AND
              (NOT (EQUAL I 0))
              (NUMBERP I)
              (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                          I))
              (EQUAL
               (P
                (P-STATE
                 '(PC (XOR-BVS . 5))
                 (CONS
                  (LIST
                   (LIST
                    (LIST 'VECS-ADDR
                        'ADDR
                        (CONS S
                              (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))
                    (LIST 'NUMVECS 'NAT (SUB1 I)))
                   RET-PC)
                  CTRL-STK)
                 (CONS
                  (LIST 'BITV
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                  TEMP-STK)
                 PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                 WORD-SIZE 'RUN)
                (XOR-BVS-CLOCK-LOOP (SUB1 I)))
               (P-STATE RET-PC CTRL-STK
                (CONS
                 (LIST 'BITV
                  (XOR-BVS-ARRAY
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                   (CDR (ASSOC S DATA-SEGMENT))
                   (SUB1 I)
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                 TEMP-STK)
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN))
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (EQUAL WORD-SIZE 0))
              (NUMBERP WORD-SIZE)
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (LESSP I
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (BIT-VECTORP CURRENT WORD-SIZE)
              (LESSP I (EXP 2 WORD-SIZE))
              (NOT (LESSP (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                      I)
                          (LENGTH (CDR (ASSOC S DATA-SEGMENT))))))
             (EQUAL
              (P
               (P-STATE
                '(PC (XOR-BVS . 12))
                (CONS
                 (LIST
                  (LIST
                   (LIST 'VECS-ADDR
                    'ADDR
                    (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                   (LIST 'NUMVECS 'NAT (SUB1 I)))
                  RET-PC)
                 CTRL-STK)
                (CONS
                 '(NAT 1)
                 (CONS
                  (LIST 'ADDR
                   (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                  (CONS (LIST 'BITV CURRENT)
                        TEMP-STK)))
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'ILLEGAL-ADD-ADDR-INSTRUCTION)
               (ADD1 (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))
              (P-STATE RET-PC CTRL-STK
               (CONS
                (LIST 'BITV
                 (XOR-BVS-ARRAY
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                  (CDR (ASSOC S DATA-SEGMENT))
                  (SUB1 I)
                  (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 1.1.1.
            (IMPLIES
             (AND
              (NOT (EQUAL I 0))
              (NUMBERP I)
              (NOT (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                          I))
              (EQUAL
               (P
                (P-STATE
                 '(PC (XOR-BVS . 5))
                 (CONS
                  (LIST
                   (LIST
                    (LIST 'VECS-ADDR
                        'ADDR
                        (CONS S
                              (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))
                    (LIST 'NUMVECS 'NAT (SUB1 I)))
                   RET-PC)
                  CTRL-STK)
                 (CONS
                  (LIST 'BITV
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT))))))
                  TEMP-STK)
                 PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                 WORD-SIZE 'RUN)
                (XOR-BVS-CLOCK-LOOP (SUB1 I)))
               (P-STATE RET-PC CTRL-STK
                (CONS
                 (LIST 'BITV
                  (XOR-BVS-ARRAY
                   (XOR-BITV CURRENT
                    (CADR
                         (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                   (CDR (ASSOC S DATA-SEGMENT))
                   (SUB1 I)
                   (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                 TEMP-STK)
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN))
              (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (EQUAL WORD-SIZE 0))
              (NUMBERP WORD-SIZE)
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (LESSP I
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (BIT-VECTORP CURRENT WORD-SIZE)
              (LESSP I (EXP 2 WORD-SIZE))
              (LESSP (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                       I))
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
              (LESSP (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                 I)
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
             (EQUAL
              (P
               (P-STATE
                '(PC (XOR-BVS . 13))
                (CONS
                 (LIST
                  (LIST
                   (LIST 'VECS-ADDR
                    'ADDR
                    (CONS S
                        (SUB1 (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I))))
                   (LIST 'NUMVECS 'NAT (SUB1 I)))
                  RET-PC)
                 CTRL-STK)
                (CONS
                  (LIST 'ADDR
                        (CONS S
                              (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)))
                  (CONS (LIST 'BITV CURRENT) TEMP-STK))
                PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                WORD-SIZE 'RUN)
               (ADD1 (ADD1 (ADD1 (ADD1 (XOR-BVS-CLOCK-LOOP (SUB1 I)))))))
              (P-STATE RET-PC CTRL-STK
               (CONS
                (LIST 'BITV
                 (XOR-BVS-ARRAY
                  (XOR-BITV CURRENT
                   (CADR (GET (DIFFERENCE (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                                          I)
                              (CDR (ASSOC S DATA-SEGMENT)))))
                  (CDR (ASSOC S DATA-SEGMENT))
                  (SUB1 I)
                  (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
                TEMP-STK)
               PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
               WORD-SIZE 'RUN))),

      which again simplifies, applying P-PC-P-STATE, P-STEP1-OPENER,
      P-WORD-SIZE-P-STATE, P-MAX-TEMP-STK-SIZE-P-STATE,
      P-MAX-CTRL-STK-SIZE-P-STATE, P-DATA-SEGMENT-P-STATE, CDR-CONS,
      P-CTRL-STK-P-STATE, CAR-CONS, P-TEMP-STK-P-STATE, P-PROG-SEGMENT-P-STATE,
      P-PSW-P-STATE, BIT-VECTORS-PITON-MEANS, and P-OPENER, and expanding the
      functions P-INS-STEP, SET-LOCAL-VAR-VALUE, BINDINGS, PUT-ASSOC,
      PUT-VALUE, RET-PC, P-FRAME, POP, PUSH, CDR, TOP, ADD1-P-PC, ADD1-ADDR,
      P-SET-LOCAL-STEP, P-INS-OKP, CAR, P-SET-LOCAL-OKP, CONS,
      P-CURRENT-INSTRUCTION, OFFSET, DEFINITION, AREA-NAME, P-CURRENT-PROGRAM,
      PROGRAM-BODY, GET, UNLABEL, EQUAL, P-STEP, FETCH, FETCH-ADP,
      P-FETCH-STEP, P-OBJECTP-TYPE, TYPE, ADPP, ADP-OFFSET, ADP-NAME,
      DEFINIENS, UNTAG, P-OBJECTP, P-FETCH-OKP, TAG, P-XOR-BITV-STEP, TOP1,
      P-XOR-BITV-OKP, PC, P-JUMP-STEP, and P-JUMP-OKP, to:

            T.

Q.E.D.


[ 0.0 1.0 0.3 ]

XOR-BVS-LOOP-CORRECTNESS-GENERAL


(PROVE-LEMMA DIFFERENCE-X-SUB1-X-BETTER
             (REWRITE)
             (EQUAL (DIFFERENCE X (SUB1 X))
                    (IF (LESSP 0 X) 1 0)))

WARNING:  the previously added lemma, DIFFERENCE-SUB1-ARG2, could be applied
whenever the newly proposed DIFFERENCE-X-SUB1-X-BETTER could!


This simplifies, rewriting with DIFFERENCE-X-X and DIFFERENCE-SUB1-ARG2, and
opening up NUMBERP, LESSP, ADD1, and EQUAL, to:

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

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-X-SUB1-X-BETTER


(PROVE-LEMMA XOR-BVS-LOOP-CORRECTNESS NIL
  (IMPLIES (AND (LESSP (LENGTH (ARRAY S DATA-SEGMENT))
                       (EXP 2 WORD-SIZE))
                (NOT (ZEROP WORD-SIZE))
                (LISTP CTRL-STK)
                (BIT-VECTORS-PITON (ARRAY S DATA-SEGMENT)
                                   WORD-SIZE)
                (AT-LEAST-MOREP (LENGTH TEMP-STK)
                                3 MAX-TEMP-STK-SIZE)
                (EQUAL (DEFINITION 'XOR-BVS PROG-SEGMENT)
                       (XOR-BVS-PROGRAM))
                (DEFINEDP S DATA-SEGMENT)
                (LESSP 0 N)
                (BIT-VECTORP CURRENT WORD-SIZE)
                (EQUAL N
                       (LENGTH (ARRAY S DATA-SEGMENT))))
           (EQUAL (P (P-STATE '(PC (XOR-BVS . 5))
                              (CONS (LIST (LIST (CONS 'VECS-ADDR
                                                      (LIST 'ADDR (CONS S 0)))
                                                (CONS 'NUMVECS
                                                      (LIST 'NAT (SUB1 N))))
                                          RET-PC)
                                    CTRL-STK)
                              (CONS (LIST 'BITV CURRENT) TEMP-STK)
                              PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                              MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)
                     (XOR-BVS-CLOCK-LOOP (SUB1 N)))
                  (P-STATE RET-PC CTRL-STK
                           (CONS (LIST 'BITV
                                       (XOR-BVS-ARRAY CURRENT
                                                      (ARRAY S DATA-SEGMENT)
                                                      (SUB1 N)
                                                      N))
                                 TEMP-STK)
                           PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                           MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)))
  ((USE (XOR-BVS-LOOP-CORRECTNESS-GENERAL (I (SUB1 N))))))

This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
IMPLIES, XOR-BVS-PROGRAM, DEFINITION, and ARRAY, to the goal:

      (IMPLIES
       (AND
        (IMPLIES
         (AND (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                     (EXP 2 WORD-SIZE))
              (NOT (ZEROP WORD-SIZE))
              (LISTP CTRL-STK)
              (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                                 WORD-SIZE)
              (AT-LEAST-MOREP (LENGTH TEMP-STK)
                              3 MAX-TEMP-STK-SIZE)
              (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                     '(XOR-BVS (VECS-ADDR NUMVECS)
                               NIL
                               (PUSH-LOCAL VECS-ADDR)
                               (FETCH)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                               (TEST-NAT-AND-JUMP ZERO DONE)
                               (PUSH-LOCAL NUMVECS)
                               (SUB1-NAT)
                               (POP-LOCAL NUMVECS)
                               (PUSH-LOCAL VECS-ADDR)
                               (PUSH-CONSTANT (NAT 1))
                               (ADD-ADDR)
                               (SET-LOCAL VECS-ADDR)
                               (FETCH)
                               (XOR-BITV)
                               (JUMP LOOP)
                               (DL DONE NIL (RET))))
              (DEFINEDP S DATA-SEGMENT)
              (NUMBERP (SUB1 N))
              (LESSP (SUB1 N) N)
              (BIT-VECTORP CURRENT WORD-SIZE)
              (EQUAL N
                     (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
         (EQUAL
          (P
           (P-STATE
                 '(PC (XOR-BVS . 5))
                 (CONS (LIST (LIST (LIST 'VECS-ADDR
                                         'ADDR
                                         (CONS S
                                               (SUB1 (DIFFERENCE N (SUB1 N)))))
                                   (LIST 'NUMVECS 'NAT (SUB1 N)))
                             RET-PC)
                       CTRL-STK)
                 (CONS (LIST 'BITV CURRENT) TEMP-STK)
                 PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
                 WORD-SIZE 'RUN)
           (XOR-BVS-CLOCK-LOOP (SUB1 N)))
          (P-STATE RET-PC CTRL-STK
                   (CONS (LIST 'BITV
                               (XOR-BVS-ARRAY CURRENT
                                              (CDR (ASSOC S DATA-SEGMENT))
                                              (SUB1 N)
                                              N))
                         TEMP-STK)
                   PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                   MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)))
        (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
               (EXP 2 WORD-SIZE))
        (NOT (EQUAL WORD-SIZE 0))
        (NUMBERP WORD-SIZE)
        (LISTP CTRL-STK)
        (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                           WORD-SIZE)
        (AT-LEAST-MOREP (LENGTH TEMP-STK)
                        3 MAX-TEMP-STK-SIZE)
        (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
               '(XOR-BVS (VECS-ADDR NUMVECS)
                         NIL
                         (PUSH-LOCAL VECS-ADDR)
                         (FETCH)
                         (PUSH-LOCAL NUMVECS)
                         (SUB1-NAT)
                         (POP-LOCAL NUMVECS)
                         (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                         (TEST-NAT-AND-JUMP ZERO DONE)
                         (PUSH-LOCAL NUMVECS)
                         (SUB1-NAT)
                         (POP-LOCAL NUMVECS)
                         (PUSH-LOCAL VECS-ADDR)
                         (PUSH-CONSTANT (NAT 1))
                         (ADD-ADDR)
                         (SET-LOCAL VECS-ADDR)
                         (FETCH)
                         (XOR-BITV)
                         (JUMP LOOP)
                         (DL DONE NIL (RET))))
        (DEFINEDP S DATA-SEGMENT)
        (LESSP 0 N)
        (BIT-VECTORP CURRENT WORD-SIZE)
        (EQUAL N
               (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
       (EQUAL
             (P (P-STATE '(PC (XOR-BVS . 5))
                         (CONS (LIST (LIST (LIST 'VECS-ADDR 'ADDR (CONS S 0))
                                           (LIST 'NUMVECS 'NAT (SUB1 N)))
                                     RET-PC)
                               CTRL-STK)
                         (CONS (LIST 'BITV CURRENT) TEMP-STK)
                         PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                         MAX-TEMP-STK-SIZE WORD-SIZE 'RUN)
                (XOR-BVS-CLOCK-LOOP (SUB1 N)))
             (P-STATE RET-PC CTRL-STK
                      (CONS (LIST 'BITV
                                  (XOR-BVS-ARRAY CURRENT
                                                 (CDR (ASSOC S DATA-SEGMENT))
                                                 (SUB1 N)
                                                 N))
                            TEMP-STK)
                      PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE
                      MAX-TEMP-STK-SIZE WORD-SIZE 'RUN))).

This simplifies, rewriting with AT-LEAST-MOREP-LINEAR,
DIFFERENCE-X-SUB1-X-BETTER, P-PC-P-STATE, and EQUAL-EXP-0, and unfolding ZEROP,
NOT, LESSP, EQUAL, AND, IMPLIES, SUB1, and NUMBERP, to:

      (IMPLIES
       (AND (NOT (LESSP (SUB1 (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
                        (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
            (LESSP (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                   (EXP 2 WORD-SIZE))
            (NOT (EQUAL WORD-SIZE 0))
            (NUMBERP WORD-SIZE)
            (LISTP CTRL-STK)
            (BIT-VECTORS-PITON (CDR (ASSOC S DATA-SEGMENT))
                               WORD-SIZE)
            (AT-LEAST-MOREP (LENGTH TEMP-STK)
                            3 MAX-TEMP-STK-SIZE)
            (EQUAL (ASSOC 'XOR-BVS PROG-SEGMENT)
                   '(XOR-BVS (VECS-ADDR NUMVECS)
                             NIL
                             (PUSH-LOCAL VECS-ADDR)
                             (FETCH)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (DL LOOP NIL (PUSH-LOCAL NUMVECS))
                             (TEST-NAT-AND-JUMP ZERO DONE)
                             (PUSH-LOCAL NUMVECS)
                             (SUB1-NAT)
                             (POP-LOCAL NUMVECS)
                             (PUSH-LOCAL VECS-ADDR)
                             (PUSH-CONSTANT (NAT 1))
                             (ADD-ADDR)
                             (SET-LOCAL VECS-ADDR)
                             (FETCH)
                             (XOR-BITV)
                             (JUMP LOOP)
                             (DL DONE NIL (RET))))
            (DEFINEDP S DATA-SEGMENT)
            (NOT (EQUAL (LENGTH (CDR (ASSOC S DATA-SEGMENT)))
                        0))
            (BIT-VECTORP CURRENT WORD-SIZE))
       (EQUAL
        (P
         (P-STATE
          '(PC (XOR-BVS . 5))
          (CONS
               (LIST (LIST (LIST 'VECS-ADDR 'ADDR (CONS S 0))
                           (LIST 'NUMVECS
                                 'NAT
                                 (SUB1 (LENGTH (CDR (ASSOC S DATA-SEGMENT))))))
                     RET-PC)
               CTRL-STK)
          (CONS (LIST 'BITV CURRENT) TEMP-STK)
          PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
          WORD-SIZE 'RUN)
         (XOR-BVS-CLOCK-LOOP (SUB1 (LENGTH (CDR (ASSOC S DATA-SEGMENT))))))
        (P-STATE RET-PC CTRL-STK
         (CONS
              (LIST 'BITV
                    (XOR-BVS-ARRAY CURRENT
                                   (CDR (ASSOC S DATA-SEGMENT))
                                   (SUB1 (LENGTH (CDR (ASSOC S DATA-SEGMENT))))
                                   (LENGTH (CDR (ASSOC S DATA-SEGMENT)))))
              TEMP-STK)
         PROG-SEGMENT DATA-SEGMENT MAX-CTRL-STK-SIZE MAX-TEMP-STK-SIZE
         WORD-SIZE 'RUN))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.3 0.0 ]

XOR-BVS-LOOP-CORRECTNESS


(PROVE-LEMMA EXP-0
             (REWRITE)
             (IMPLIES (ZEROP X)
                      (AND (EQUAL (EXP X Y) (IF (ZEROP Y) 1 0))
                           (EQUAL (EXP Y X) 1)))
             ((ENABLE EXP)))

WARNING:  the previously added lemma, EXP-ZERO, could be applied whenever the
newly proposed EXP-0 could!


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


This simplifies, applying EXP-0-ARG1, EXP-0-ARG2, and EXP-ZERO, and expanding
the definitions of ZEROP, EQUAL, AND, TIMES, and EXP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EXP-0


(PROVE-LEMMA BIT-VECTORS-PITON-MEANS-MORE
             (REWRITE)
             (IMPLIES (AND (LISTP X)
                           (BIT-VECTORS-PITON X SIZE))
                      (EQUAL (LIST 'BITV (CADAR X))
                             (CAR X))))

WARNING:  Note that BIT-VECTORS-PITON-MEANS-MORE contains the free variable
SIZE which will be chosen by instantiating the hypothesis:
      (BIT-VECTORS-PITON X SIZE).



.

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

Case 3. (IMPLIES (AND (NOT (LISTP Z))
                      (BIT-VECTORS-PITON (CONS Z V) SIZE))
                 (EQUAL (LIST 'BITV (CADR Z)) Z)),

  which simplifies, rewriting with CAR-CONS, and unfolding BIT-VECTORS-PITON,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (LISTP W))
                      (BIT-VECTORS-PITON (CONS (CONS D W) V)
                                         SIZE))
                 (EQUAL (LIST 'BITV (CAR W))
                        (CONS D W))).

  This simplifies, applying CAR-NLISTP, CDR-CONS, and CAR-CONS, and opening up
  the definitions of BIT-VECTORP, LISTP, EQUAL, and BIT-VECTORS-PITON, to:

        T.

Case 1. (IMPLIES (BIT-VECTORS-PITON (CONS (CONS D (CONS Z C)) V)
                                    SIZE)
                 (EQUAL (LIST 'BITV Z)
                        (CONS D (CONS Z C)))).

  But this simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  function BIT-VECTORS-PITON, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

BIT-VECTORS-PITON-MEANS-MORE


(DEFN XOR-BVS
      (ARRAY)
      (IF (LISTP ARRAY)
          (XOR-BITV (CAR ARRAY)
                    (XOR-BVS (CDR ARRAY)))
          NIL))

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




[ 0.0 0.0 0.0 ]

XOR-BVS


(DEFN UNTAG-ARRAY
      (ARRAY)
      (IF (LISTP ARRAY)
          (CONS (UNTAG (CAR ARRAY))
                (UNTAG-ARRAY (CDR ARRAY)))
          NIL))

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




[ 0.3 0.0 0.0 ]

UNTAG-ARRAY


(PROVE-LEMMA BIT-VECTORP-GET
             (REWRITE)
             (IMPLIES (BIT-VECTORS-PITON ARRAY SIZE)
                      (EQUAL (BIT-VECTORP (UNTAG (GET N ARRAY))
                                          SIZE)
                             (LESSP N (LENGTH ARRAY)))))

This conjecture can be simplified, using the abbreviations IMPLIES and UNTAG,
to:

      (IMPLIES (BIT-VECTORS-PITON ARRAY SIZE)
               (EQUAL (BIT-VECTORP (CADR (GET N ARRAY))
                                   SIZE)
                      (LESSP N (LENGTH ARRAY)))).

Name the above subgoal *1.


     Perhaps we can prove it by induction.  There are four plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP ARRAY)
                         (p (SUB1 N) (CDR ARRAY) SIZE))
                    (p N ARRAY SIZE))
           (IMPLIES (NOT (LISTP ARRAY))
                    (p N ARRAY SIZE))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT ARRAY) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  Note, however, the inductive instance chosen
for N.  The above induction scheme leads to the following three new goals:

Case 3. (IMPLIES (AND (LISTP ARRAY)
                      (NOT (BIT-VECTORS-PITON (CDR ARRAY) SIZE))
                      (BIT-VECTORS-PITON ARRAY SIZE))
                 (EQUAL (BIT-VECTORP (CADR (GET N ARRAY))
                                     SIZE)
                        (LESSP N (LENGTH ARRAY)))).

  This simplifies, opening up BIT-VECTORS-PITON, to:

        T.

Case 2. (IMPLIES (AND (LISTP ARRAY)
                      (EQUAL (BIT-VECTORP (CADR (GET (SUB1 N) (CDR ARRAY)))
                                          SIZE)
                             (LESSP (SUB1 N) (LENGTH (CDR ARRAY))))
                      (BIT-VECTORS-PITON ARRAY SIZE))
                 (EQUAL (BIT-VECTORP (CADR (GET N ARRAY))
                                     SIZE)
                        (LESSP N (LENGTH ARRAY)))).

  This simplifies, applying the lemma SUB1-ADD1, and expanding the definitions
  of BIT-VECTORS-PITON, GET, LENGTH, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP ARRAY))
                      (BIT-VECTORS-PITON ARRAY SIZE))
                 (EQUAL (BIT-VECTORP (CADR (GET N ARRAY))
                                     SIZE)
                        (LESSP N (LENGTH ARRAY)))).

  This simplifies, unfolding BIT-VECTORS-PITON, LENGTH, EQUAL, and LESSP, to:

        (IMPLIES (AND (NOT (LISTP ARRAY))
                      (EQUAL ARRAY NIL))
                 (NOT (BIT-VECTORP (CADR (GET N NIL))
                                   SIZE))),

  which again simplifies, unfolding the definition of LISTP, to the conjecture:

        (NOT (BIT-VECTORP (CADR (GET N NIL))
                          SIZE)).

  Name the above subgoal *1.1.


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

Case 2. (IMPLIES (ZEROP N)
                 (NOT (BIT-VECTORP (CADR (GET N NIL))
                                   SIZE))),

  which simplifies, unfolding ZEROP, GET, CDR, CAR, EQUAL, LISTP, and
  BIT-VECTORP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (BIT-VECTORP (CADR (GET (SUB1 N) NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET N NIL))
                                   SIZE))),

  which simplifies, unfolding ZEROP, GET, and CDR, to:

        (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (BIT-VECTORP (CADR (GET (SUB1 N) NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET (SUB1 N) 0))
                                   SIZE))).

  Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 X) to eliminate
  (SUB1 N).  We use the type restriction lemma noted when SUB1 was introduced
  to constrain the new variable.  The result is the conjecture:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ADD1 X) 0))
                      (NOT (BIT-VECTORP (CADR (GET X NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET X 0)) SIZE))).

  This further simplifies, obviously, to:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (BIT-VECTORP (CADR (GET X NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET X 0)) SIZE))),

  which we will name *1.1.1.


     Perhaps we can prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X SIZE))
           (IMPLIES (AND (NOT (ZEROP X))
                         (p (SUB1 X) SIZE))
                    (p X SIZE))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme generates the following three new formulas:

Case 3. (IMPLIES (AND (ZEROP X)
                      (NUMBERP X)
                      (NOT (BIT-VECTORP (CADR (GET X NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET X 0)) SIZE))).

  This simplifies, expanding ZEROP, NUMBERP, GET, CDR, CAR, EQUAL, LISTP, and
  BIT-VECTORP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (BIT-VECTORP (CADR (GET (SUB1 X) NIL))
                                   SIZE)
                      (NUMBERP X)
                      (NOT (BIT-VECTORP (CADR (GET X NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET X 0)) SIZE))).

  This simplifies, unfolding ZEROP, GET, and CDR, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (BIT-VECTORP (CADR (GET (SUB1 X) 0))
                                        SIZE))
                      (NUMBERP X)
                      (NOT (BIT-VECTORP (CADR (GET X NIL))
                                        SIZE)))
                 (NOT (BIT-VECTORP (CADR (GET X 0)) SIZE))).

  This simplifies, opening up ZEROP, GET, and CDR, to:

        T.


     That finishes the proof of *1.1.1, which also finishes the proof of *1.1,
which, in turn, also finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

BIT-VECTORP-GET


(ENABLE DIFFERENCE-SUB1-ARG2)

[ 0.0 0.0 0.0 ]

DIFFERENCE-SUB1-ARG2-ON1


(PROVE-LEMMA XOR-BITV-COMMUTATIVE
             (REWRITE)
             (IMPLIES (EQUAL (LENGTH A) (LENGTH B))
                      (EQUAL (XOR-BITV A B)
                             (XOR-BITV B A))))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  Four inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP A) (p (CDR A) (CDR B)))
                    (p A B))
           (IMPLIES (NOT (LISTP A)) (p A B))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for B.  The above
induction scheme leads to the following three new conjectures:

Case 3. (IMPLIES (AND (LISTP A)
                      (NOT (EQUAL (LENGTH (CDR A))
                                  (LENGTH (CDR B))))
                      (EQUAL (LENGTH A) (LENGTH B)))
                 (EQUAL (XOR-BITV A B)
                        (XOR-BITV B A))).

  This simplifies, rewriting with the lemmas CAR-NLISTP, CAR-CONS, and
  CONS-EQUAL, and opening up the defi