(NOTE-LIB "fortran" T)
Loading ./fortran-vcg/fortran.lib
Finished loading ./fortran-vcg/fortran.lib
Loading ./fortran-vcg/fortran.o
Finished loading ./fortran-vcg/fortran.o

(#./fortran-vcg/fortran.lib #./fortran-vcg/fortran)


(ADD-AXIOM FORTRAN NIL T)

[ 0.0 0.0 0.0 ]

FORTRAN


(DCL A$0 NIL)

[ 0.0 0.0 0.0 ]

A$0


(DCL BLK-DELTA1$0 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$0


(DCL BLK-DELTA1$1 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$1


(DCL BLK-DELTA1$2 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$2


(DCL BLK-DELTA1$3 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$3


(DCL BLK-DELTA1$4 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$4


(DCL C$0 NIL)

[ 0.0 0.0 0.0 ]

C$0


(DCL C$1 NIL)

[ 0.0 0.0 0.0 ]

C$1


(DCL C$2 NIL)

[ 0.0 0.0 0.0 ]

C$2


(DCL C$3 NIL)

[ 0.0 0.0 0.0 ]

C$3


(DCL C$4 NIL)

[ 0.0 0.0 0.0 ]

C$4


(DCL I$1 NIL)

[ 0.0 0.0 0.0 ]

I$1


(DCL I$2 NIL)

[ 0.0 0.0 0.0 ]

I$2


(DCL I$3 NIL)

[ 0.0 0.0 0.0 ]

I$3


(DCL I$4 NIL)

[ 0.0 0.0 0.0 ]

I$4


(DCL MAXI$0 NIL)

[ 0.0 0.0 0.0 ]

MAXI$0


(DCL ASIZE& NIL)

[ 0.0 0.0 0.0 ]

ASIZE&


(ADD-AXIOM ASIZE&-NUMBERP
           (REWRITE)
           (NUMBERP (ASIZE&)))

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


[ 0.0 0.0 0.0 ]

ASIZE&-NUMBERP


(DEFN DELTA1
      (A C MAXI)
      (IF (ZEROP MAXI)
          0
          (IF (EQUAL C (ELT1 A MAXI))
              0
              (ADD1 (DELTA1 A C (SUB1 MAXI))))))

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




[ 0.0 0.0 0.0 ]

DELTA1


(DEFN STRINGP
      (A I SIZE)
      (IF (ZEROP I)
          T
          (AND (NUMBERP (ELT1 A I))
               (NOT (EQUAL (ELT1 A I) 0))
               (NOT (LESSP SIZE (ELT1 A I)))
               (STRINGP A (SUB1 I) SIZE))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT I) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, STRINGP is
accepted under the definitional principle.  Note that:
      (OR (FALSEP (STRINGP A I SIZE))
          (TRUEP (STRINGP A I SIZE)))
is a theorem.




[ 0.0 0.0 0.0 ]

STRINGP


(ADD-AXIOM INPUT-CONDITIONS
           (REWRITE)
           '*1*TRUE)

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


[ 0.0 0.0 0.0 ]

INPUT-CONDITIONS


(DEFN GLOBAL-HYPS NIL
      (AND (NOT (EQUAL (ASIZE&) '0))
           (AND (STRINGP (A$0) (MAXI$0) (ASIZE&))
                (AND (NOT (EQUAL (MAXI$0) '0))
                     (AND (LESSP (ADD1 (ASIZE&))
                                 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                          (AND (LESSP (ADD1 (MAXI$0))
                                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                               (NUMBERP (MAXI$0))))))))

     From the definition we can conclude that:
      (OR (FALSEP (GLOBAL-HYPS))
          (TRUEP (GLOBAL-HYPS)))
is a theorem.




[ 0.0 0.0 0.0 ]

GLOBAL-HYPS


(PROVE-LEMMA STRINGP-IS-A-UNIV-QUANTIFIER
             (REWRITE)
             (IMPLIES (AND (STRINGP A I (ASIZE&))
                           (NOT (EQUAL J 0))
                           (NUMBERP J)
                           (NOT (LESSP I J)))
                      (AND (NUMBERP (ELT1 A J))
                           (NOT (LESSP (ASIZE&) (ELT1 A J)))
                           (NOT (EQUAL (ELT1 A J) 0)))))

WARNING:  Note that STRINGP-IS-A-UNIV-QUANTIFIER contains the free variable I
which will be chosen by instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  When the linear lemma STRINGP-IS-A-UNIV-QUANTIFIER is stored under
(ELT1 A J) it contains the free variable I which will be chosen by
instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  When the linear lemma STRINGP-IS-A-UNIV-QUANTIFIER is stored under
(ASIZE&) it contains the free variables J, I, and A which will be chosen by
instantiating the hypotheses (STRINGP A I (ASIZE&)) and (NOT (EQUAL J 0)).


WARNING:  Note that STRINGP-IS-A-UNIV-QUANTIFIER contains the free variable I
which will be chosen by instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  Note that the proposed lemma STRINGP-IS-A-UNIV-QUANTIFIER is to be
stored as zero type prescription rules, zero compound recognizer rules, two
linear rules, and two replacement rules.


This conjecture simplifies, unfolding the functions NOT and AND, to the
following three new formulas:

Case 3. (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))).

  Name the above subgoal *1.

Case 2. (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

  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 (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NUMBERP (ELT1 A J)))
     (IMPLIES (AND (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NOT (LESSP (ASIZE&) (ELT1 A J))))
     (IMPLIES (AND (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NOT (EQUAL (ELT1 A J) 0)))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  There
are three plausible inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP I) (p A J I))
           (IMPLIES (AND (NOT (ZEROP I)) (p A J (SUB1 I)))
                    (p A J I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT I) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces nine new conjectures:

Case 9. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, expanding the definitions of ZEROP, EQUAL, STRINGP, and
  LESSP, to:

        T.

Case 8. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, expanding the functions ZEROP and STRINGP, to:

        T.

Case 7. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, using linear arithmetic, to two new goals:

  Case 7.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NUMBERP (ELT1 A J))),

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

          T.

  Case 7.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NUMBERP (ELT1 A I))),

    which again simplifies, unfolding the definitions of ZEROP and STRINGP, to:

          T.

Case 6. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

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

        T.

Case 5. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

  which simplifies, expanding ZEROP and STRINGP, to:

        T.

Case 4. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

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

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NOT (LESSP (ASIZE&) (ELT1 A J)))),

    which again simplifies, opening up ZEROP, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NOT (LESSP (ASIZE&) (ELT1 A I)))),

    which again simplifies, unfolding the functions ZEROP and STRINGP, to:

          T.

Case 3. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, unfolding the definitions of ZEROP, EQUAL, STRINGP, and
  LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, unfolding the functions ZEROP and STRINGP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, using linear arithmetic, to two new goals:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NOT (EQUAL (ELT1 A J) 0))),

    which again simplifies, opening up ZEROP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NOT (EQUAL (ELT1 A I) 0))),

    which again simplifies, expanding ZEROP, STRINGP, NUMBERP, and EQUAL, to:

          T.


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


[ 0.0 0.1 0.0 ]

STRINGP-IS-A-UNIV-QUANTIFIER


(PROVE-LEMMA INPUT-DEFINEDNESS NIL
             (IMPLIES (GLOBAL-HYPS) '*1*TRUE))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS and
IMPLIES, to:

      T.

This simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-DEFINEDNESS


(ADD-AXIOM INPUT NIL T)

[ 0.0 0.0 0.0 ]

INPUT


(ADD-AXIOM LOGICAL-IF-F NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F


(ADD-AXIOM ASSIGNMENT
           (REWRITE)
           (AND (EQUAL (I$1) '1)
                (AND (EQUAL (C$1) (C$0))
                     (EQUAL (BLK-DELTA1$1)
                            (BLK-DELTA1$0)))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT


(PROVE-LEMMA PASS1-INVRT NIL
       (IMPLIES (GLOBAL-HYPS)
                (AND (AND (NUMBERP (I$1))
                          (AND (NOT (EQUAL (I$1) '0))
                               (AND (NOT (LESSP (ADD1 (ASIZE&)) (I$1)))
                                    (IMPLIES (AND (NUMBERP J)
                                                  (AND (NOT (EQUAL J '0))
                                                       (LESSP J (I$1))))
                                             (EQUAL (ELT1 (BLK-DELTA1$1) J)
                                                    (MAXI$0))))))
                     (LEX (CONS (DIFFERENCE (PLUS '2 (PLUS (ASIZE&) (MAXI$0)))
                                            (I$1))
                                'NIL)
                          (CONS (PLUS '2 (PLUS (ASIZE&) (MAXI$0)))
                                'NIL)))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, IMPLIES,
and ASSIGNMENT, to:

      (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0)))
               (AND (AND (NUMBERP 1)
                         (NOT (EQUAL 1 0))
                         (NOT (LESSP (ADD1 (ASIZE&)) 1))
                         (IMPLIES (AND (NUMBERP J)
                                       (NOT (EQUAL J 0))
                                       (LESSP J 1))
                                  (EQUAL (ELT1 (BLK-DELTA1$0) J)
                                         (MAXI$0))))
                    (LEX (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI$0))
                                           1))
                         (LIST (PLUS 2 (ASIZE&) (MAXI$0)))))),

which simplifies, rewriting with SUB1-ADD1, ADD1-EQUAL, and CAR-CONS, and
unfolding the definitions of LESSP, NUMBERP, EQUAL, NOT, SUB1, AND, IMPLIES,
PLUS, DIFFERENCE, and LEX, to the following two new conjectures:

Case 2. (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP J)
                      (NOT (EQUAL J 0))
                      (LESSP J 1))
                 (EQUAL (ELT1 (BLK-DELTA1$0) J)
                        (MAXI$0))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NOT (EQUAL (PLUS (ASIZE&) (MAXI$0)) 0)))
                 (LESSP (SUB1 (PLUS (ASIZE&) (MAXI$0)))
                        (PLUS (ASIZE&) (MAXI$0)))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PASS1-INVRT


(UBT INPUT)

INPUT


(ADD-AXIOM PATHS-FROM-PASS1-INVRT
           (REWRITE)
           (IMPLIES (AND (NUMBERP J)
                         (AND (NOT (EQUAL J '0))
                              (LESSP J (I$1))))
                    (EQUAL (ELT1 (BLK-DELTA1$1) J)
                           (MAXI$0))))

[ 0.0 0.0 0.0 ]

PATHS-FROM-PASS1-INVRT


(DEFN PATH-HYPS NIL
      (AND (GLOBAL-HYPS)
           (AND (NUMBERP (I$1))
                (AND (NOT (EQUAL (I$1) '0))
                     (NOT (LESSP (ADD1 (ASIZE&)) (I$1)))))))

     From the definition we can conclude that:
      (OR (FALSEP (PATH-HYPS))
          (TRUEP (PATH-HYPS)))
is a theorem.




[ 0.0 0.0 0.0 ]

PATH-HYPS


(PROVE-LEMMA DEFINEDNESS NIL
             (IMPLIES (PATH-HYPS)
                      (ZNUMBERP (I$1))))

This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to:

      T,

which simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DEFINEDNESS


(ADD-AXIOM LOGICAL-IF-T NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-T


(ADD-AXIOM EFFECTS-OF-UNDEFINER
           (REWRITE)
           (AND (EQUAL (C$2) (C$1))
                (EQUAL (BLK-DELTA1$2)
                       (BLK-DELTA1$1))))

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


[ 0.0 0.0 0.0 ]

EFFECTS-OF-UNDEFINER


(ADD-AXIOM LOGICAL-IF-F1 NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F1


(ADD-AXIOM ASSIGNMENT1
           (REWRITE)
           (AND (EQUAL (I$3) '1)
                (AND (EQUAL (C$3) (C$2))
                     (EQUAL (BLK-DELTA1$3)
                            (BLK-DELTA1$2)))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT1


(PROVE-LEMMA PASS2-INVRT NIL
 (IMPLIES
      (AND (I$1)
           (AND (ZGREATERP (I$1) (ASIZE&))
                (PATH-HYPS)))
      (AND (AND (NUMBERP (I$3))
                (AND (NOT (EQUAL (I$3) '0))
                     (AND (NOT (LESSP (ADD1 (MAXI$0)) (I$3)))
                          (IMPLIES (AND (NOT (ZEROP J))
                                        (NOT (LESSP (ASIZE&) J)))
                                   (EQUAL (ELT1 (BLK-DELTA1$3) J)
                                          (PLUS (DELTA1 (A$0) J (SUB1 (I$3)))
                                                (DIFFERENCE (MAXI$0)
                                                            (SUB1 (I$3)))))))))
           (LEX (CONS (DIFFERENCE (ADD1 (MAXI$0)) (I$3))
                      'NIL)
                (CONS (DIFFERENCE (PLUS '2 (PLUS (ASIZE&) (MAXI$0)))
                                  (I$1))
                      'NIL)))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
AND, IMPLIES, EFFECTS-OF-UNDEFINER, ASSIGNMENT1, and ZGREATERP, to:

      (IMPLIES
             (AND (I$1)
                  (ZLESSP (ASIZE&) (I$1))
                  (NOT (EQUAL (ASIZE&) 0))
                  (STRINGP (A$0) (MAXI$0) (ASIZE&))
                  (NOT (EQUAL (MAXI$0) 0))
                  (LESSP (ADD1 (ASIZE&))
                         (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                  (LESSP (ADD1 (MAXI$0))
                         (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                  (NUMBERP (MAXI$0))
                  (NUMBERP (I$1))
                  (NOT (EQUAL (I$1) 0))
                  (NOT (LESSP (ADD1 (ASIZE&)) (I$1))))
             (AND (AND (NUMBERP 1)
                       (NOT (EQUAL 1 0))
                       (NOT (LESSP (ADD1 (MAXI$0)) 1))
                       (IMPLIES (AND (NOT (ZEROP J))
                                     (NOT (LESSP (ASIZE&) J)))
                                (EQUAL (ELT1 (BLK-DELTA1$1) J)
                                       (PLUS (DELTA1 (A$0) J (SUB1 1))
                                             (DIFFERENCE (MAXI$0) (SUB1 1))))))
                  (LEX (LIST (DIFFERENCE (ADD1 (MAXI$0)) 1))
                       (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI$0))
                                         (I$1)))))),

which simplifies, appealing to the lemmas SUB1-ADD1, CDR-CONS, and CAR-CONS,
and expanding ZLESSP, LESSP, NUMBERP, EQUAL, NOT, SUB1, ZEROP, AND, DELTA1,
DIFFERENCE, PLUS, IMPLIES, and LEX, to three new formulas:

Case 3. (IMPLIES (AND (LESSP (ASIZE&) (I$1))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (ASIZE&) J)))
                 (EQUAL (ELT1 (BLK-DELTA1$1) J)
                        (MAXI$0))),

  which again simplifies, using linear arithmetic, to the goal:

        (IMPLIES (AND (EQUAL (I$1) (PLUS 1 (ASIZE&)))
                      (LESSP (ASIZE&) (PLUS 1 (ASIZE&)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (PLUS 1 (ASIZE&)))
                      (NOT (EQUAL (PLUS 1 (ASIZE&)) 0))
                      (NOT (LESSP (ASIZE&)
                                  (SUB1 (PLUS 1 (ASIZE&)))))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (ASIZE&) J)))
                 (EQUAL (ELT1 (BLK-DELTA1$1) J)
                        (MAXI$0))).

  But this again simplifies, using linear arithmetic, applying the lemma
  PATHS-FROM-PASS1-INVRT, and opening up the definitions of SUB1, NUMBERP,
  EQUAL, and PLUS, to:

        T.

Case 2. (IMPLIES (AND (LESSP (ASIZE&) (I$1))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (NOT (EQUAL (SUB1 (I$1)) 0)))
                 (LESSP (MAXI$0)
                        (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (SUB1 (I$1)))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (LESSP (ASIZE&) (I$1))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (EQUAL (SUB1 (I$1)) 0))
                 (LESSP (MAXI$0)
                        (ADD1 (PLUS (ASIZE&) (MAXI$0))))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PASS2-INVRT


(UBT LOGICAL-IF-T)

LOGICAL-IF-T


(ADD-AXIOM LOGICAL-IF-F1 NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F1


(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-DELTA1 NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$1) (ASIZE&)))
                           (PATH-HYPS))
                      (AND (LESSP '0 (I$1))
                           (NOT (LESSP (ASIZE&) (I$1))))))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, and ZGREATERP, to the formula:

      (IMPLIES (AND (NOT (ZLESSP (ASIZE&) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (ASIZE&)) (I$1))))
               (AND (LESSP 0 (I$1))
                    (NOT (LESSP (ASIZE&) (I$1))))).

This simplifies, rewriting with SUB1-ADD1, and expanding the functions ZLESSP,
LESSP, EQUAL, NOT, and AND, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ARRAY-BOUNDS-CHECK-FOR-DELTA1


(ADD-AXIOM ASSIGNMENT1
           (REWRITE)
           (AND (EQUAL (I$2) (I$1))
                (AND (EQUAL (C$2) (C$1))
                     (EQUAL (ELT1 (BLK-DELTA1$2) I)
                            (IF (EQUAL I (I$1))
                                (MAXI$0)
                                (ELT1 (BLK-DELTA1$1) I))))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT1


(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
             (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                          (BLK-DELTA1$2)
                                          '1
                                          (ASIZE&)
                                          (I$1)
                                          (MAXI$0))
                           (AND (NOT (ZGREATERP (I$1) (ASIZE&)))
                                (PATH-HYPS)))
                      (EXPRESSIBLE-ZNUMBERP (ZPLUS (I$2) '1))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ASSIGNMENT1, and ZGREATERP, to:

      (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                   (BLK-DELTA1$2)
                                   1
                                   (ASIZE&)
                                   (I$1)
                                   (MAXI$0))
                    (NOT (ZLESSP (ASIZE&) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (ASIZE&)) (I$1))))
               (EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) 1))),

which simplifies, applying SUB1-ADD1 and COMMUTATIVITY-OF-PLUS, and unfolding
the functions ZLESSP, LESSP, PLUS, EQUAL, NUMBERP, SUB1, NEGATIVEP, ZPLUS, and
EXPRESSIBLE-ZNUMBERP, to the new formula:

      (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                   (BLK-DELTA1$2)
                                   1
                                   (ASIZE&)
                                   (I$1)
                                   (MAXI$0))
                    (NOT (LESSP (ASIZE&) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ASIZE&) (SUB1 (I$1)))))
               (LESSP (I$1)
                      (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZPLUS


(ADD-AXIOM ASSIGNMENT2
           (REWRITE)
           (AND (EQUAL (I$3) (ZPLUS (I$2) '1))
                (AND (EQUAL (C$3) (C$2))
                     (EQUAL (BLK-DELTA1$3)
                            (BLK-DELTA1$2)))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT2


(PROVE-LEMMA PASS1-INVRT1 NIL
       (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                    (BLK-DELTA1$2)
                                    '1
                                    (ASIZE&)
                                    (I$1)
                                    (MAXI$0))
                     (AND (NOT (ZGREATERP (I$1) (ASIZE&)))
                          (PATH-HYPS)))
                (AND (AND (NUMBERP (I$3))
                          (AND (NOT (EQUAL (I$3) '0))
                               (AND (NOT (LESSP (ADD1 (ASIZE&)) (I$3)))
                                    (IMPLIES (AND (NUMBERP J)
                                                  (AND (NOT (EQUAL J '0))
                                                       (LESSP J (I$3))))
                                             (EQUAL (ELT1 (BLK-DELTA1$3) J)
                                                    (MAXI$0))))))
                     (LEX (CONS (DIFFERENCE (PLUS '2 (PLUS (ASIZE&) (MAXI$0)))
                                            (I$3))
                                'NIL)
                          (CONS (DIFFERENCE (PLUS '2 (PLUS (ASIZE&) (MAXI$0)))
                                            (I$1))
                                'NIL)))))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT1, ASSIGNMENT2, and ZGREATERP, to the
formula:

      (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                   (BLK-DELTA1$2)
                                   1
                                   (ASIZE&)
                                   (I$1)
                                   (MAXI$0))
                    (NOT (ZLESSP (ASIZE&) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (ASIZE&)) (I$1))))
               (AND (AND (NUMBERP (ZPLUS (I$1) 1))
                         (NOT (EQUAL (ZPLUS (I$1) 1) 0))
                         (NOT (LESSP (ADD1 (ASIZE&))
                                     (ZPLUS (I$1) 1)))
                         (IMPLIES (AND (NUMBERP J)
                                       (NOT (EQUAL J 0))
                                       (LESSP J (ZPLUS (I$1) 1)))
                                  (EQUAL (ELT1 (BLK-DELTA1$2) J)
                                         (MAXI$0))))
                    (LEX (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI$0))
                                           (ZPLUS (I$1) 1)))
                         (LIST (DIFFERENCE (PLUS 2 (ASIZE&) (MAXI$0))
                                           (I$1)))))).

This simplifies, applying SUB1-ADD1, COMMUTATIVITY-OF-PLUS, ASSIGNMENT1,
CDR-CONS, and CAR-CONS, and unfolding the functions ZLESSP, LESSP, PLUS, EQUAL,
NUMBERP, SUB1, NEGATIVEP, ZPLUS, NOT, AND, IMPLIES, DIFFERENCE, and LEX, to
three new conjectures:

Case 3. (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$2)
                                     1
                                     (ASIZE&)
                                     (I$1)
                                     (MAXI$0))
                      (NOT (LESSP (ASIZE&) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (NUMBERP J)
                      (NOT (EQUAL J 0))
                      (LESSP (SUB1 J) (I$1))
                      (NOT (EQUAL J (I$1))))
                 (EQUAL (ELT1 (BLK-DELTA1$1) J)
                        (MAXI$0))),

  which again simplifies, using linear arithmetic and applying
  PATHS-FROM-PASS1-INVRT, to:

        T.

Case 2. (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$2)
                                     1
                                     (ASIZE&)
                                     (I$1)
                                     (MAXI$0))
                      (NOT (LESSP (ASIZE&) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (NOT (EQUAL (SUB1 (I$1)) 0)))
                 (LESSP (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (I$1)))
                        (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (SUB1 (I$1)))))).

  This again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP (PLUS (ASIZE&) (MAXI$0))
                             (SUB1 (I$1)))
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$2)
                                     1
                                     (ASIZE&)
                                     (I$1)
                                     (MAXI$0))
                      (NOT (LESSP (ASIZE&) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (NOT (EQUAL (SUB1 (I$1)) 0)))
                 (LESSP (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (I$1)))
                        (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (SUB1 (I$1)))))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$2)
                                     1
                                     (ASIZE&)
                                     (I$1)
                                     (MAXI$0))
                      (NOT (LESSP (ASIZE&) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) (SUB1 (I$1))))
                      (EQUAL (SUB1 (I$1)) 0))
                 (LESSP (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    (SUB1 (I$1)))
                        (ADD1 (PLUS (ASIZE&) (MAXI$0))))),

  which again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP (PLUS (ASIZE&) (MAXI$0)) 0)
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$2)
                                     1
                                     (ASIZE&)
                                     (I$1)
                                     (MAXI$0))
                      (NOT (LESSP (ASIZE&) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (ASIZE&) 0))
                      (EQUAL (SUB1 (I$1)) 0))
                 (LESSP (DIFFERENCE (PLUS (ASIZE&) (MAXI$0))
                                    0)
                        (ADD1 (PLUS (ASIZE&) (MAXI$0))))).

  But this again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PASS1-INVRT1


(UBT PATHS-FROM-PASS1-INVRT)

PATHS-FROM-PASS1-INVRT


(ADD-AXIOM PATHS-FROM-PASS2-INVRT
           (REWRITE)
           (IMPLIES (AND (NOT (ZEROP J))
                         (NOT (LESSP (ASIZE&) J)))
                    (EQUAL (ELT1 (BLK-DELTA1$1) J)
                           (PLUS (DELTA1 (A$0) J (SUB1 (I$1)))
                                 (DIFFERENCE (MAXI$0) (SUB1 (I$1)))))))

[ 0.0 0.0 0.0 ]

PATHS-FROM-PASS2-INVRT


(DEFN PATH-HYPS NIL
      (AND (GLOBAL-HYPS)
           (AND (NUMBERP (I$1))
                (AND (NOT (EQUAL (I$1) '0))
                     (NOT (LESSP (ADD1 (MAXI$0)) (I$1)))))))

     From the definition we can conclude that:
      (OR (FALSEP (PATH-HYPS))
          (TRUEP (PATH-HYPS)))
is a theorem.




[ 0.0 0.0 0.0 ]

PATH-HYPS


(PROVE-LEMMA DEFINEDNESS NIL
             (IMPLIES (PATH-HYPS)
                      (ZNUMBERP (I$1))))

This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to:

      T,

which simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DEFINEDNESS


(ADD-AXIOM LOGICAL-IF-T NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-T


(ADD-AXIOM EFFECTS-OF-UNDEFINER
           (REWRITE)
           (AND (EQUAL (C$2) (C$1))
                (EQUAL (BLK-DELTA1$2)
                       (BLK-DELTA1$1))))

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


[ 0.0 0.0 0.0 ]

EFFECTS-OF-UNDEFINER


(PROVE-LEMMA OUTPUT NIL
             (IMPLIES (AND (I$1)
                           (AND (ZGREATERP (I$1) (MAXI$0))
                                (PATH-HYPS)))
                      (IMPLIES (AND (NUMBERP C)
                                    (AND (NOT (EQUAL C '0))
                                         (NOT (LESSP (ASIZE&) C))))
                               (EQUAL (ELT1 (BLK-DELTA1$2) C)
                                      (DELTA1 (A$0) C (MAXI$0))))))

This formula can be simplified, using the abbreviations NOT, GLOBAL-HYPS,
PATH-HYPS, AND, IMPLIES, EFFECTS-OF-UNDEFINER, and ZGREATERP, to:

      (IMPLIES (AND (I$1)
                    (ZLESSP (MAXI$0) (I$1))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1)))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (ELT1 (BLK-DELTA1$1) C)
                      (DELTA1 (A$0) C (MAXI$0)))),

which simplifies, applying the lemmas SUB1-ADD1, COMMUTATIVITY-OF-PLUS, and
PATHS-FROM-PASS2-INVRT, and opening up the definitions of ZLESSP and LESSP, to
the goal:

      (IMPLIES (AND (LESSP (MAXI$0) (I$1))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                            (DELTA1 (A$0) C (SUB1 (I$1))))
                      (DELTA1 (A$0) C (MAXI$0)))).

This again simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (I$1) (PLUS 1 (MAXI$0)))
                    (LESSP (MAXI$0) (PLUS 1 (MAXI$0)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (PLUS 1 (MAXI$0)))
                    (NOT (EQUAL (PLUS 1 (MAXI$0)) 0))
                    (NOT (LESSP (MAXI$0)
                                (SUB1 (PLUS 1 (MAXI$0)))))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                        (SUB1 (PLUS 1 (MAXI$0))))
                            (DELTA1 (A$0)
                                    C
                                    (SUB1 (PLUS 1 (MAXI$0)))))
                      (DELTA1 (A$0) C (MAXI$0)))).

However this again simplifies, opening up SUB1, NUMBERP, EQUAL, and PLUS, to
the conjecture:

      (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                    (LESSP (MAXI$0) (I$1))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                            (DELTA1 (A$0) C (SUB1 (I$1))))
                      (DELTA1 (A$0) C (MAXI$0)))).

We now use the above equality hypothesis by substituting (ADD1 (MAXI$0)) for
(I$1) and keeping the equality hypothesis.  This produces:

      (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                    (LESSP (MAXI$0) (ADD1 (MAXI$0)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NOT (EQUAL (ADD1 (MAXI$0)) 0))
                    (NOT (LESSP (MAXI$0)
                                (SUB1 (ADD1 (MAXI$0)))))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                        (SUB1 (ADD1 (MAXI$0))))
                            (DELTA1 (A$0)
                                    C
                                    (SUB1 (ADD1 (MAXI$0)))))
                      (DELTA1 (A$0) C (MAXI$0)))),

which further simplifies, obviously, to the new goal:

      (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                    (LESSP (MAXI$0) (I$1))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                    (NUMBERP C)
                    (NOT (EQUAL C 0))
                    (NOT (LESSP (ASIZE&) C)))
               (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                            (DELTA1 (A$0) C (SUB1 (I$1))))
                      (DELTA1 (A$0) C (MAXI$0)))),

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


     So now let us return to:

(IMPLIES (AND (I$1)
              (ZGREATERP (I$1) (MAXI$0))
              (PATH-HYPS)
              (NUMBERP C)
              (NOT (EQUAL C 0))
              (NOT (LESSP (ASIZE&) C)))
         (EQUAL (ELT1 (BLK-DELTA1$2) C)
                (DELTA1 (A$0) C (MAXI$0)))).

We named this *1.  We will try to prove it by induction.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (OR (EQUAL C 0) (NOT (NUMBERP C)))
                    (p C))
           (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                         (OR (EQUAL (ASIZE&) 0)
                             (NOT (NUMBERP (ASIZE&)))))
                    (p C))
           (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                         (NOT (OR (EQUAL (ASIZE&) 0)
                                  (NOT (NUMBERP (ASIZE&)))))
                         (p (SUB1 C)))
                    (p C))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT C) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces five new conjectures:

Case 5. (IMPLIES (AND (OR (EQUAL C 0) (NOT (NUMBERP C)))
                      (I$1)
                      (ZGREATERP (I$1) (MAXI$0))
                      (PATH-HYPS)
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1$2) C)
                        (DELTA1 (A$0) C (MAXI$0)))),

  which simplifies, expanding the definitions of NOT and OR, to:

        T.

Case 4. (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (OR (EQUAL (ASIZE&) 0)
                          (NOT (NUMBERP (ASIZE&))))
                      (I$1)
                      (ZGREATERP (I$1) (MAXI$0))
                      (PATH-HYPS)
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1$2) C)
                        (DELTA1 (A$0) C (MAXI$0)))),

  which simplifies, unfolding the definitions of NOT, OR, ZLESSP, ZGREATERP,
  GLOBAL-HYPS, EQUAL, and PATH-HYPS, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (NOT (OR (EQUAL (ASIZE&) 0)
                               (NOT (NUMBERP (ASIZE&)))))
                      (EQUAL (SUB1 C) 0)
                      (I$1)
                      (ZGREATERP (I$1) (MAXI$0))
                      (PATH-HYPS)
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1$2) C)
                        (DELTA1 (A$0) C (MAXI$0)))),

  which simplifies, applying SUB1-ADD1, EFFECTS-OF-UNDEFINER,
  COMMUTATIVITY-OF-PLUS, PATHS-FROM-PASS2-INVRT, and SUB1-TYPE-RESTRICTION,
  and opening up the functions NOT, OR, ZLESSP, ZGREATERP, GLOBAL-HYPS, LESSP,
  PATH-HYPS, EQUAL, and STRINGP, to:

        (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (SUB1 C) 0)
                      (I$1)
                      (NOT (NEGATIVEP (MAXI$0)))
                      (NOT (NEGATIVEP (I$1)))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) C (SUB1 (I$1))))
                        (DELTA1 (A$0) C (MAXI$0)))),

  which again simplifies, using linear arithmetic, to the conjecture:

        (IMPLIES (AND (EQUAL (I$1) (PLUS 1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (SUB1 C) 0)
                      (PLUS 1 (MAXI$0))
                      (NOT (NEGATIVEP (MAXI$0)))
                      (NOT (NEGATIVEP (PLUS 1 (MAXI$0))))
                      (LESSP (MAXI$0) (PLUS 1 (MAXI$0)))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (PLUS 1 (MAXI$0)))
                      (NOT (EQUAL (PLUS 1 (MAXI$0)) 0))
                      (NOT (LESSP (MAXI$0)
                                  (SUB1 (PLUS 1 (MAXI$0)))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                          (SUB1 (PLUS 1 (MAXI$0))))
                              (DELTA1 (A$0)
                                      C
                                      (SUB1 (PLUS 1 (MAXI$0)))))
                        (DELTA1 (A$0) C (MAXI$0)))).

  However this again simplifies, expanding the definitions of SUB1, NUMBERP,
  EQUAL, and PLUS, to:

        (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (SUB1 C) 0)
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) C (SUB1 (I$1))))
                        (DELTA1 (A$0) C (MAXI$0)))).

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

        (IMPLIES (AND (NUMBERP X)
                      (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL X 0)
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (EQUAL (ADD1 X) 0)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) (ADD1 X) (SUB1 (I$1))))
                        (DELTA1 (A$0) (ADD1 X) (MAXI$0)))).

  This further simplifies, expanding the definitions of NUMBERP and EQUAL, to
  the goal:

        (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1)))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) 1 (SUB1 (I$1))))
                        (DELTA1 (A$0) 1 (MAXI$0)))).

  We now use the above equality hypothesis by substituting (ADD1 (MAXI$0)) for
  (I$1) and throwing away the equality.  This produces:

        (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (LESSP (MAXI$0) (ADD1 (MAXI$0)))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (ADD1 (MAXI$0)) 0))
                      (NOT (LESSP (MAXI$0)
                                  (SUB1 (ADD1 (MAXI$0))))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                          (SUB1 (ADD1 (MAXI$0))))
                              (DELTA1 (A$0)
                                      1
                                      (SUB1 (ADD1 (MAXI$0)))))
                        (DELTA1 (A$0) 1 (MAXI$0)))),

  which further simplifies, applying SUB1-ADD1, and unfolding the definition
  of LESSP, to:

        (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (LESSP (SUB1 (MAXI$0)) (MAXI$0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (LESSP (MAXI$0) (MAXI$0))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (MAXI$0))
                              (DELTA1 (A$0) 1 (MAXI$0)))
                        (DELTA1 (A$0) 1 (MAXI$0)))),

  which finally simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (NOT (OR (EQUAL (ASIZE&) 0)
                               (NOT (NUMBERP (ASIZE&)))))
                      (LESSP (ASIZE&) (SUB1 C))
                      (I$1)
                      (ZGREATERP (I$1) (MAXI$0))
                      (PATH-HYPS)
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1$2) C)
                        (DELTA1 (A$0) C (MAXI$0)))),

  which simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL C 0) (NOT (NUMBERP C))))
                      (NOT (OR (EQUAL (ASIZE&) 0)
                               (NOT (NUMBERP (ASIZE&)))))
                      (EQUAL (ELT1 (BLK-DELTA1$2) (SUB1 C))
                             (DELTA1 (A$0) (SUB1 C) (MAXI$0)))
                      (I$1)
                      (ZGREATERP (I$1) (MAXI$0))
                      (PATH-HYPS)
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (ASIZE&) C)))
                 (EQUAL (ELT1 (BLK-DELTA1$2) C)
                        (DELTA1 (A$0) C (MAXI$0)))),

  which simplifies, using linear arithmetic, rewriting with
  EFFECTS-OF-UNDEFINER, SUB1-ADD1, COMMUTATIVITY-OF-PLUS,
  PATHS-FROM-PASS2-INVRT, and SUB1-TYPE-RESTRICTION, and opening up the
  definitions of NOT, OR, ZLESSP, ZGREATERP, GLOBAL-HYPS, LESSP, PATH-HYPS,
  and STRINGP, to:

        (IMPLIES (AND (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) (SUB1 C))
                             (DELTA1 (A$0) (SUB1 C) (MAXI$0)))
                      (I$1)
                      (NOT (NEGATIVEP (MAXI$0)))
                      (NOT (NEGATIVEP (I$1)))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (SUB1 (ASIZE&)) (SUB1 C))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) C (SUB1 (I$1))))
                        (DELTA1 (A$0) C (MAXI$0)))),

  which again simplifies, using linear arithmetic, to the conjecture:

        (IMPLIES (AND (EQUAL (I$1) (PLUS 1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) (SUB1 C))
                             (DELTA1 (A$0) (SUB1 C) (MAXI$0)))
                      (PLUS 1 (MAXI$0))
                      (NOT (NEGATIVEP (MAXI$0)))
                      (NOT (NEGATIVEP (PLUS 1 (MAXI$0))))
                      (LESSP (MAXI$0) (PLUS 1 (MAXI$0)))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (PLUS 1 (MAXI$0)))
                      (NOT (EQUAL (PLUS 1 (MAXI$0)) 0))
                      (NOT (LESSP (MAXI$0)
                                  (SUB1 (PLUS 1 (MAXI$0)))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (SUB1 (ASIZE&)) (SUB1 C))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                          (SUB1 (PLUS 1 (MAXI$0))))
                              (DELTA1 (A$0)
                                      C
                                      (SUB1 (PLUS 1 (MAXI$0)))))
                        (DELTA1 (A$0) C (MAXI$0)))).

  This again simplifies, expanding the functions SUB1, NUMBERP, EQUAL, and
  PLUS, to:

        (IMPLIES (AND (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) (SUB1 C))
                             (DELTA1 (A$0) (SUB1 C) (MAXI$0)))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NUMBERP C)
                      (NOT (EQUAL C 0))
                      (NOT (LESSP (SUB1 (ASIZE&)) (SUB1 C))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) C (SUB1 (I$1))))
                        (DELTA1 (A$0) C (MAXI$0)))).

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

        (IMPLIES (AND (NUMBERP X)
                      (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) X)
                             (DELTA1 (A$0) X (MAXI$0)))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (EQUAL (ADD1 X) 0))
                      (NOT (LESSP (SUB1 (ASIZE&)) X)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) (ADD1 X) (SUB1 (I$1))))
                        (DELTA1 (A$0) (ADD1 X) (MAXI$0)))).

  This further simplifies, obviously, to the new conjecture:

        (IMPLIES (AND (NUMBERP X)
                      (EQUAL (I$1) (ADD1 (MAXI$0)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) X)
                             (DELTA1 (A$0) X (MAXI$0)))
                      (LESSP (MAXI$0) (I$1))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (LESSP (SUB1 (ASIZE&)) X)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) (ADD1 X) (SUB1 (I$1))))
                        (DELTA1 (A$0) (ADD1 X) (MAXI$0)))).

  We use the first equality hypothesis by substituting (ADD1 (MAXI$0)) for
  (I$1) and throwing away the equality.  We must thus prove:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) X)
                             (DELTA1 (A$0) X (MAXI$0)))
                      (LESSP (MAXI$0) (ADD1 (MAXI$0)))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (EQUAL (ADD1 (MAXI$0)) 0))
                      (NOT (LESSP (MAXI$0)
                                  (SUB1 (ADD1 (MAXI$0)))))
                      (NOT (LESSP (SUB1 (ASIZE&)) X)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0)
                                          (SUB1 (ADD1 (MAXI$0))))
                              (DELTA1 (A$0)
                                      (ADD1 X)
                                      (SUB1 (ADD1 (MAXI$0)))))
                        (DELTA1 (A$0) (ADD1 X) (MAXI$0)))).

  This further simplifies, appealing to the lemma SUB1-ADD1, and unfolding the
  definition of LESSP, to the goal:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ASIZE&) 0))
                      (EQUAL (ELT1 (BLK-DELTA1$1) X)
                             (DELTA1 (A$0) X (MAXI$0)))
                      (LESSP (SUB1 (MAXI$0)) (MAXI$0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NOT (LESSP (MAXI$0) (MAXI$0)))
                      (NOT (LESSP (SUB1 (ASIZE&)) X)))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (MAXI$0))
                              (DELTA1 (A$0) (ADD1 X) (MAXI$0)))
                        (DELTA1 (A$0) (ADD1 X) (MAXI$0)))).

  This finally simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.2 0.0 ]

OUTPUT


(UBT LOGICAL-IF-T)

LOGICAL-IF-T


(ADD-AXIOM LOGICAL-IF-F1 NIL T)

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F1


(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                           (PATH-HYPS))
                      (AND (LESSP '0 (I$1))
                           (NOT (LESSP (MAXI$0) (I$1))))))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, and ZGREATERP, to the formula:

      (IMPLIES (AND (NOT (ZLESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1))))
               (AND (LESSP 0 (I$1))
                    (NOT (LESSP (MAXI$0) (I$1))))).

This simplifies, rewriting with SUB1-ADD1, and expanding the functions ZLESSP,
LESSP, EQUAL, NOT, and AND, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ARRAY-BOUNDS-CHECK-FOR-A


(PROVE-LEMMA DEFINEDNESS1 NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                           (PATH-HYPS))
                      (ZNUMBERP (ELT1 (A$0) (I$1)))))

This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, and ZGREATERP, to:

      (IMPLIES (AND (NOT (ZLESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1)))
                    (NOT (NEGATIVEP (ELT1 (A$0) (I$1)))))
               (NUMBERP (ELT1 (A$0) (I$1)))),

which simplifies, rewriting with SUB1-ADD1 and STRINGP-IS-A-UNIV-QUANTIFIER,
and expanding the functions ZLESSP and LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DEFINEDNESS1


(ADD-AXIOM ASSIGNMENT1
           (REWRITE)
           (AND (EQUAL (I$2) (I$1))
                (AND (EQUAL (C$2) (ELT1 (A$0) (I$1)))
                     (EQUAL (BLK-DELTA1$2)
                            (BLK-DELTA1$1)))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT1


(PROVE-LEMMA INPUT-COND-OF-ZDIFFERENCE NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                           (PATH-HYPS))
                      (EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE (MAXI$0) (I$2)))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ASSIGNMENT1, and ZGREATERP, to:

      (IMPLIES (AND (NOT (ZLESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1))))
               (EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE (MAXI$0) (I$1)))),

which simplifies, rewriting with SUB1-ADD1, and expanding the functions ZLESSP,
LESSP, ZDIFFERENCE, and EXPRESSIBLE-ZNUMBERP, to the following two new goals:

Case 2. (IMPLIES
          (AND (NOT (LESSP (MAXI$0) (I$1)))
               (NOT (EQUAL (ASIZE&) 0))
               (STRINGP (A$0) (MAXI$0) (ASIZE&))
               (NOT (EQUAL (MAXI$0) 0))
               (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                           0))
               (LESSP (ASIZE&)
                      (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
               (LESSP (MAXI$0)
                      (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
               (NUMBERP (MAXI$0))
               (NUMBERP (I$1))
               (NOT (EQUAL (I$1) 0))
               (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (DIFFERENCE (MAXI$0) (I$1))
                      0))).

  This again simplifies, using linear arithmetic and applying the lemma
  INTEGER-SIZE, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1)))))
                 (LESSP (DIFFERENCE (MAXI$0) (I$1))
                        (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZDIFFERENCE


(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-DELTA1 NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                           (PATH-HYPS))
                      (AND (LESSP '0 (C$2))
                           (NOT (LESSP (ASIZE&) (C$2))))))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT1, and ZGREATERP, to the formula:

      (IMPLIES (AND (NOT (ZLESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1))))
               (AND (LESSP 0 (ELT1 (A$0) (I$1)))
                    (NOT (LESSP (ASIZE&)
                                (ELT1 (A$0) (I$1)))))).

This simplifies, rewriting with SUB1-ADD1 and STRINGP-IS-A-UNIV-QUANTIFIER,
and expanding the functions ZLESSP, LESSP, EQUAL, NOT, and AND, to:

      (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (MAXI$0) (SUB1 (I$1)))))
               (NOT (LESSP (ASIZE&) (ELT1 (A$0) (I$1))))).

But this again simplifies, using linear arithmetic and rewriting with
STRINGP-IS-A-UNIV-QUANTIFIER, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ARRAY-BOUNDS-CHECK-FOR-DELTA1


(ADD-AXIOM ASSIGNMENT2
           (REWRITE)
           (AND (EQUAL (I$3) (I$2))
                (AND (EQUAL (C$3) (C$2))
                     (EQUAL (ELT1 (BLK-DELTA1$3) I)
                            (IF (EQUAL I (C$2))
                                (ZDIFFERENCE (MAXI$0) (I$2))
                                (ELT1 (BLK-DELTA1$2) I))))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT2


(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
             (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$2)
                                          (BLK-DELTA1$3)
                                          '1
                                          (ASIZE&)
                                          (C$2)
                                          (ZDIFFERENCE (MAXI$0) (I$2)))
                           (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                                (PATH-HYPS)))
                      (EXPRESSIBLE-ZNUMBERP (ZPLUS (I$3) '1))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ASSIGNMENT2, ZGREATERP, and ASSIGNMENT1, to the new
conjecture:

      (IMPLIES (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                   (BLK-DELTA1$3)
                                   1
                                   (ASIZE&)
                                   (ELT1 (A$0) (I$1))
                                   (ZDIFFERENCE (MAXI$0) (I$1)))
                    (NOT (ZLESSP (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (LESSP (ADD1 (ASIZE&))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (LESSP (ADD1 (MAXI$0))
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (ADD1 (MAXI$0)) (I$1))))
               (EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) 1))),

which simplifies, applying SUB1-ADD1 and COMMUTATIVITY-OF-PLUS, and unfolding
the definitions of ZDIFFERENCE, ZLESSP, LESSP, PLUS, EQUAL, NUMBERP, SUB1,
NEGATIVEP, ZPLUS, and EXPRESSIBLE-ZNUMBERP, to:

      (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                    (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                   (BLK-DELTA1$3)
                                   1
                                   (ASIZE&)
                                   (ELT1 (A$0) (I$1))
                                   (DIFFERENCE (MAXI$0) (I$1)))
                    (NOT (EQUAL (ASIZE&) 0))
                    (STRINGP (A$0) (MAXI$0) (ASIZE&))
                    (NOT (EQUAL (MAXI$0) 0))
                    (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                0))
                    (LESSP (ASIZE&)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (LESSP (MAXI$0)
                           (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                    (NUMBERP (MAXI$0))
                    (NUMBERP (I$1))
                    (NOT (EQUAL (I$1) 0))
                    (NOT (LESSP (MAXI$0) (SUB1 (I$1)))))
               (LESSP (I$1)
                      (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZPLUS


(ADD-AXIOM ASSIGNMENT3
           (REWRITE)
           (AND (EQUAL (I$4) (ZPLUS (I$3) '1))
                (AND (EQUAL (C$4) (C$3))
                     (EQUAL (BLK-DELTA1$4)
                            (BLK-DELTA1$3)))))

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


[ 0.0 0.0 0.0 ]

ASSIGNMENT3


(PROVE-LEMMA DELTA1-SKIP
             (REWRITE)
             (IMPLIES (AND (NOT (EQUAL J (ELT1 PAT I)))
                           (NOT (ZEROP I)))
                      (EQUAL (DELTA1 PAT J I)
                             (ADD1 (DELTA1 PAT J (SUB1 I))))))

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

      (IMPLIES (AND (NOT (EQUAL J (ELT1 PAT I)))
                    (NOT (EQUAL I 0))
                    (NUMBERP I))
               (EQUAL (DELTA1 PAT J I)
                      (ADD1 (DELTA1 PAT J (SUB1 I))))),

which simplifies, expanding the function DELTA1, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DELTA1-SKIP


(PROVE-LEMMA PASS2-INVRT1 NIL
 (IMPLIES
      (AND (ALMOST-EQUAL1 (BLK-DELTA1$2)
                          (BLK-DELTA1$3)
                          '1
                          (ASIZE&)
                          (C$2)
                          (ZDIFFERENCE (MAXI$0) (I$2)))
           (AND (NOT (ZGREATERP (I$1) (MAXI$0)))
                (PATH-HYPS)))
      (AND (AND (NUMBERP (I$4))
                (AND (NOT (EQUAL (I$4) '0))
                     (AND (NOT (LESSP (ADD1 (MAXI$0)) (I$4)))
                          (IMPLIES (AND (NOT (ZEROP J))
                                        (NOT (LESSP (ASIZE&) J)))
                                   (EQUAL (ELT1 (BLK-DELTA1$4) J)
                                          (PLUS (DELTA1 (A$0) J (SUB1 (I$4)))
                                                (DIFFERENCE (MAXI$0)
                                                            (SUB1 (I$4)))))))))
           (LEX (CONS (DIFFERENCE (ADD1 (MAXI$0)) (I$4))
                      'NIL)
                (CONS (DIFFERENCE (ADD1 (MAXI$0)) (I$1))
                      'NIL)))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ASSIGNMENT2, ASSIGNMENT3, ZGREATERP, and ASSIGNMENT1, to:

      (IMPLIES
        (AND (ALMOST-EQUAL1 (BLK-DELTA1$1)
                            (BLK-DELTA1$3)
                            1
                            (ASIZE&)
                            (ELT1 (A$0) (I$1))
                            (ZDIFFERENCE (MAXI$0) (I$1)))
             (NOT (ZLESSP (MAXI$0) (I$1)))
             (NOT (EQUAL (ASIZE&) 0))
             (STRINGP (A$0) (MAXI$0) (ASIZE&))
             (NOT (EQUAL (MAXI$0) 0))
             (LESSP (ADD1 (ASIZE&))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
             (LESSP (ADD1 (MAXI$0))
                    (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
             (NUMBERP (MAXI$0))
             (NUMBERP (I$1))
             (NOT (EQUAL (I$1) 0))
             (NOT (LESSP (ADD1 (MAXI$0)) (I$1))))
        (AND (AND (NUMBERP (ZPLUS (I$1) 1))
                  (NOT (EQUAL (ZPLUS (I$1) 1) 0))
                  (NOT (LESSP (ADD1 (MAXI$0))
                              (ZPLUS (I$1) 1)))
                  (IMPLIES (AND (NOT (ZEROP J))
                                (NOT (LESSP (ASIZE&) J)))
                           (EQUAL (ELT1 (BLK-DELTA1$3) J)
                                  (PLUS (DELTA1 (A$0)
                                                J
                                                (SUB1 (ZPLUS (I$1) 1)))
                                        (DIFFERENCE (MAXI$0)
                                                    (SUB1 (ZPLUS (I$1) 1)))))))
             (LEX (LIST (DIFFERENCE (ADD1 (MAXI$0))
                                    (ZPLUS (I$1) 1)))
                  (LIST (DIFFERENCE (ADD1 (MAXI$0))
                                    (I$1)))))),

which simplifies, rewriting with SUB1-ADD1, COMMUTATIVITY-OF-PLUS, ASSIGNMENT1,
ASSIGNMENT2, CDR-CONS, and CAR-CONS, and opening up ZDIFFERENCE, ZLESSP, LESSP,
PLUS, EQUAL, NUMBERP, SUB1, NEGATIVEP, ZPLUS, NOT, ZEROP, AND, IMPLIES,
DIFFERENCE, and LEX, to the following three new goals:

Case 3. (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$3)
                                     1
                                     (ASIZE&)
                                     (ELT1 (A$0) (I$1))
                                     (DIFFERENCE (MAXI$0) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (ASIZE&) J))
                      (EQUAL J (ELT1 (A$0) (I$1))))
                 (EQUAL (DIFFERENCE (MAXI$0) (I$1))
                        (PLUS (DIFFERENCE (MAXI$0) (I$1))
                              (DELTA1 (A$0) J (I$1))))).

  However this again simplifies, rewriting with the lemmas
  STRINGP-IS-A-UNIV-QUANTIFIER and COMMUTATIVITY-OF-PLUS, and unfolding the
  definitions of DELTA1, EQUAL, and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$3)
                                     1
                                     (ASIZE&)
                                     (ELT1 (A$0) (I$1))
                                     (DIFFERENCE (MAXI$0) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (ASIZE&) J))
                      (NOT (EQUAL J (ELT1 (A$0) (I$1)))))
                 (EQUAL (ELT1 (BLK-DELTA1$1) J)
                        (PLUS (DIFFERENCE (MAXI$0) (I$1))
                              (DELTA1 (A$0) J (I$1))))),

  which again simplifies, applying COMMUTATIVITY-OF-PLUS,
  PATHS-FROM-PASS2-INVRT, DELTA1-SKIP, and PLUS-ADD1, to the new goal:

        (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$3)
                                     1
                                     (ASIZE&)
                                     (ELT1 (A$0) (I$1))
                                     (DIFFERENCE (MAXI$0) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1))))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (ASIZE&) J))
                      (NOT (EQUAL J (ELT1 (A$0) (I$1)))))
                 (EQUAL (PLUS (DIFFERENCE (MAXI$0) (SUB1 (I$1)))
                              (DELTA1 (A$0) J (SUB1 (I$1))))
                        (ADD1 (PLUS (DIFFERENCE (MAXI$0) (I$1))
                                    (DELTA1 (A$0) J (SUB1 (I$1))))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP (MAXI$0) (I$1)))
                      (ALMOST-EQUAL1 (BLK-DELTA1$1)
                                     (BLK-DELTA1$3)
                                     1
                                     (ASIZE&)
                                     (ELT1 (A$0) (I$1))
                                     (DIFFERENCE (MAXI$0) (I$1)))
                      (NOT (EQUAL (ASIZE&) 0))
                      (STRINGP (A$0) (MAXI$0) (ASIZE&))
                      (NOT (EQUAL (MAXI$0) 0))
                      (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                                  0))
                      (LESSP (ASIZE&)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (LESSP (MAXI$0)
                             (SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                      (NUMBERP (MAXI$0))
                      (NUMBERP (I$1))
                      (NOT (EQUAL (I$1) 0))
                      (NOT (LESSP (MAXI$0) (SUB1 (I$1)))))
                 (LESSP (DIFFERENCE (MAXI$0) (I$1))
                        (DIFFERENCE (MAXI$0) (SUB1 (I$1))))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PASS2-INVRT1


(UBT PATHS-FROM-PASS2-INVRT)

PATHS-FROM-PASS2-INVRT


(UBT FORTRAN)

FORTRAN


(ADD-AXIOM FORTRAN NIL T)

[ 0.0 0.0 0.0 ]

FORTRAN


(DCL BLK-DELTA1$1 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$1


(DCL BLK-DELTA1$2 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$2


(DCL BLK-DELTA1$3 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$3


(DCL BLK-DELTA1$4 NIL)

[ 0.0 0.0 0.0 ]

BLK-DELTA1$4


(DCL C$0 NIL)

[ 0.0 0.0 0.0 ]

C$0


(DCL C$1 NIL)

[ 0.0 0.0 0.0 ]

C$1


(DCL C$2 NIL)

[ 0.0 0.0 0.0 ]

C$2


(DCL C$3 NIL)

[ 0.0 0.0 0.0 ]

C$3


(DCL C$4 NIL)

[ 0.0 0.0 0.0 ]

C$4


(DCL I$0 NIL)

[ 0.0 0.0 0.0 ]

I$0


(DCL I$1 NIL)

[ 0.0 0.0 0.0 ]

I$1


(DCL I$2 NIL)

[ 0.0 0.0 0.0 ]

I$2


(DCL I$3 NIL)

[ 0.0 0.0 0.0 ]

I$3


(DCL I$4 NIL)

[ 0.0 0.0 0.0 ]

I$4


(DCL J$0 NIL)

[ 0.3 0.0 0.0 ]

J$0


(DCL J$1 NIL)

[ 0.0 0.0 0.0 ]

J$1


(DCL J$2 NIL)

[ 0.0 0.0 0.0 ]

J$2


(DCL J$3 NIL)

[ 0.0 0.0 0.0 ]

J$3


(DCL J$4 NIL)

[ 0.0 0.0 0.0 ]

J$4


(DCL NEXTI$0 NIL)

[ 0.0 0.0 0.0 ]

NEXTI$0


(DCL NEXTI$1 NIL)

[ 0.0 0.0 0.0 ]

NEXTI$1


(DCL NEXTI$2 NIL)

[ 0.0 0.0 0.0 ]

NEXTI$2


(DCL NEXTI$3 NIL)

[ 0.0 0.0 0.0 ]

NEXTI$3


(DCL NEXTI$4 NIL)

[ 0.0 0.0 0.0 ]

NEXTI$4


(DCL PAT$0 NIL)

[ 0.0 0.0 0.0 ]

PAT$0


(DCL PATLEN$0 NIL)

[ 0.0 0.0 0.0 ]

PATLEN$0


(DCL STR$0 NIL)

[ 0.0 0.0 0.0 ]

STR$0


(DCL STRLEN$0 NIL)

[ 0.0 0.0 0.0 ]

STRLEN$0


(DCL X$0 NIL)

[ 0.0 0.0 0.0 ]

X$0


(DCL X$1 NIL)

[ 0.0 0.0 0.0 ]

X$1


(DCL X$2 NIL)

[ 0.0 0.0 0.0 ]

X$2


(DCL X$3 NIL)

[ 0.0 0.0 0.0 ]

X$3


(DCL X$4 NIL)

[ 0.0 0.0 0.0 ]

X$4


(DCL ASIZE& NIL)

[ 0.0 0.0 0.0 ]

ASIZE&


(ADD-AXIOM ASIZE&-NUMBERP
           (REWRITE)
           (NUMBERP (ASIZE&)))

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


[ 0.0 0.0 0.0 ]

ASIZE&-NUMBERP


(DEFN DELTA1
      (A C MAXI)
      (IF (ZEROP MAXI)
          0
          (IF (EQUAL C (ELT1 A MAXI))
              0
              (ADD1 (DELTA1 A C (SUB1 MAXI))))))

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




[ 0.0 0.0 0.0 ]

DELTA1


(DEFN STRINGP
      (A I SIZE)
      (IF (ZEROP I)
          T
          (AND (NUMBERP (ELT1 A I))
               (NOT (EQUAL (ELT1 A I) 0))
               (NOT (LESSP SIZE (ELT1 A I)))
               (STRINGP A (SUB1 I) SIZE))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT I) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, STRINGP is
accepted under the definitional principle.  Note that:
      (OR (FALSEP (STRINGP A I SIZE))
          (TRUEP (STRINGP A I SIZE)))
is a theorem.




[ 0.0 0.0 0.0 ]

STRINGP


(PROVE-LEMMA STRINGP-IS-A-UNIV-QUANTIFIER
             (REWRITE)
             (IMPLIES (AND (STRINGP A I (ASIZE&))
                           (NOT (EQUAL J 0))
                           (NUMBERP J)
                           (NOT (LESSP I J)))
                      (AND (NUMBERP (ELT1 A J))
                           (NOT (LESSP (ASIZE&) (ELT1 A J)))
                           (NOT (EQUAL (ELT1 A J) 0)))))

WARNING:  Note that STRINGP-IS-A-UNIV-QUANTIFIER contains the free variable I
which will be chosen by instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  When the linear lemma STRINGP-IS-A-UNIV-QUANTIFIER is stored under
(ELT1 A J) it contains the free variable I which will be chosen by
instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  When the linear lemma STRINGP-IS-A-UNIV-QUANTIFIER is stored under
(ASIZE&) it contains the free variables J, I, and A which will be chosen by
instantiating the hypotheses (STRINGP A I (ASIZE&)) and (NOT (EQUAL J 0)).


WARNING:  Note that STRINGP-IS-A-UNIV-QUANTIFIER contains the free variable I
which will be chosen by instantiating the hypothesis (STRINGP A I (ASIZE&)).


WARNING:  Note that the proposed lemma STRINGP-IS-A-UNIV-QUANTIFIER is to be
stored as zero type prescription rules, zero compound recognizer rules, two
linear rules, and two replacement rules.


This conjecture simplifies, unfolding the functions NOT and AND, to the
following three new formulas:

Case 3. (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))).

  Name the above subgoal *1.

Case 2. (IMPLIES (AND (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

  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 (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NUMBERP (ELT1 A J)))
     (IMPLIES (AND (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NOT (LESSP (ASIZE&) (ELT1 A J))))
     (IMPLIES (AND (STRINGP A I (ASIZE&))
                   (NOT (EQUAL J 0))
                   (NUMBERP J)
                   (NOT (LESSP I J)))
              (NOT (EQUAL (ELT1 A J) 0)))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  There
are three plausible inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP I) (p A J I))
           (IMPLIES (AND (NOT (ZEROP I)) (p A J (SUB1 I)))
                    (p A J I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT I) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces nine new conjectures:

Case 9. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, expanding the definitions of ZEROP, EQUAL, STRINGP, and
  LESSP, to:

        T.

Case 8. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, expanding the functions ZEROP and STRINGP, to:

        T.

Case 7. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NUMBERP (ELT1 A J))),

  which simplifies, using linear arithmetic, to two new goals:

  Case 7.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NUMBERP (ELT1 A J))),

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

          T.

  Case 7.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NUMBERP (ELT1 A I))),

    which again simplifies, unfolding the definitions of ZEROP and STRINGP, to:

          T.

Case 6. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

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

        T.

Case 5. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

  which simplifies, expanding ZEROP and STRINGP, to:

        T.

Case 4. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (LESSP (ASIZE&) (ELT1 A J)))),

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

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NOT (LESSP (ASIZE&) (ELT1 A J)))),

    which again simplifies, opening up ZEROP, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NOT (LESSP (ASIZE&) (ELT1 A I)))),

    which again simplifies, unfolding the functions ZEROP and STRINGP, to:

          T.

Case 3. (IMPLIES (AND (ZEROP I)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, unfolding the definitions of ZEROP, EQUAL, STRINGP, and
  LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (STRINGP A (SUB1 I) (ASIZE&)))
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, unfolding the functions ZEROP and STRINGP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (LESSP (SUB1 I) J)
                      (STRINGP A I (ASIZE&))
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP I J)))
                 (NOT (EQUAL (ELT1 A J) 0))),

  which simplifies, using linear arithmetic, to two new goals:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) J)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J)))
                   (NOT (EQUAL (ELT1 A J) 0))),

    which again simplifies, opening up ZEROP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP I)
                        (NOT (ZEROP I))
                        (LESSP (SUB1 I) I)
                        (STRINGP A I (ASIZE&))
                        (NOT (EQUAL I 0))
                        (NOT (LESSP I I)))
                   (NOT (EQUAL (ELT1 A I) 0))),

    which again simplifies, expanding ZEROP, STRINGP, NUMBERP, and EQUAL, to:

          T.


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


[ 0.0 0.1 0.0 ]

STRINGP-IS-A-UNIV-QUANTIFIER


(DEFN MATCH
      (PAT J PATLEN STR I STRLEN)
      (IF (LESSP PATLEN J)
          T
          (IF (LESSP STRLEN I)
              F
              (AND (EQUAL (ELT1 PAT J) (ELT1 STR I))
                   (MATCH PAT
                          (ADD1 J)
                          PATLEN STR
                          (ADD1 I)
                          STRLEN))))
      ((LESSP (DIFFERENCE (ADD1 PATLEN) J))
       (LESSP (DIFFERENCE (ADD1 STRLEN) I))))

     Linear arithmetic can be used to establish that the measure:
      (DIFFERENCE (ADD1 PATLEN) J)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, MATCH is accepted under the definitional principle.  The definition of
MATCH can be justified in another way.  Linear arithmetic informs us that the
measure (DIFFERENCE (ADD1 STRLEN) I) decreases according to the well-founded
relation LESSP in each recursive call.  Note that:
      (OR (FALSEP (MATCH PAT J PATLEN STR I STRLEN))
          (TRUEP (MATCH PAT J PATLEN STR I STRLEN)))
is a theorem.




[ 0.0 0.0 0.0 ]

MATCH


(DEFN SEARCH
      (PAT STR PATLEN STRLEN I)
      (IF (LESSP STRLEN I)
          (ADD1 STRLEN)
          (IF (MATCH PAT 1 PATLEN STR I STRLEN)
              I
              (SEARCH PAT STR PATLEN STRLEN
                      (ADD1 I))))
      ((LESSP (DIFFERENCE (ADD1 STRLEN) I))))

     Linear arithmetic establishes that the measure:
      (DIFFERENCE (ADD1 STRLEN) I)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, SEARCH is accepted under the principle of definition.  Note that:
      (OR (NUMBERP (SEARCH PAT STR PATLEN STRLEN I))
          (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                 I))
is a theorem.




[ 0.0 0.0 0.0 ]

SEARCH


(ADD-AXIOM INPUT-CONDITIONS
           (REWRITE)
           '*1*TRUE)

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


[ 0.0 0.0 0.0 ]

INPUT-CONDITIONS


(DEFN GLOBAL-HYPS NIL
 (AND
   (NOT (EQUAL (ASIZE&) '0))
   (AND (LESSP (ADD1 (ASIZE&))
               (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
        (AND (STRINGP (PAT$0) (PATLEN$0) (ASIZE&))
             (AND (LESSP '0 (PATLEN$0))
                  (AND (STRINGP (STR$0) (STRLEN$0) (ASIZE&))
                       (AND (LESSP '0 (STRLEN$0))
                            (AND (LESSP (PLUS (PATLEN$0) (STRLEN$0))
                                        (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                                 (AND (NUMBERP (PATLEN$0))
                                      (NUMBERP (STRLEN$0)))))))))))

     From the definition we can conclude that:
      (OR (FALSEP (GLOBAL-HYPS))
          (TRUEP (GLOBAL-HYPS)))
is a theorem.




[ 0.0 0.0 0.0 ]

GLOBAL-HYPS


(PROVE-LEMMA SEARCH-NON-ZERO
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (LESSP 0
                             (SEARCH PAT STR PATLEN STRLEN I))))

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


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

      (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
               (LESSP 0
                      (SEARCH PAT STR PATLEN STRLEN I))).

This simplifies, opening up the definitions of EQUAL and LESSP, to:

      (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
               (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                           0))),

which we will name *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (LESSP STRLEN I)
                    (p PAT STR PATLEN STRLEN I))
           (IMPLIES (AND (NOT (LESSP STRLEN I))
                         (MATCH PAT 1 PATLEN STR I STRLEN))
                    (p PAT STR PATLEN STRLEN I))
           (IMPLIES (AND (NOT (LESSP STRLEN I))
                         (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                         (p PAT STR PATLEN STRLEN (ADD1 I)))
                    (p PAT STR PATLEN STRLEN I))).
Linear arithmetic can be used to show that the measure:
      (DIFFERENCE (ADD1 STRLEN) I)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme leads to four new formulas:

Case 4. (IMPLIES (AND (LESSP STRLEN I)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                             0))),

  which simplifies, opening up the definition of SEARCH, to:

        T.

Case 3. (IMPLIES (AND (NOT (LESSP STRLEN I))
                      (MATCH PAT 1 PATLEN STR I STRLEN)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                             0))),

  which simplifies, opening up the definition of SEARCH, to:

        T.

Case 2. (IMPLIES (AND (NOT (LESSP STRLEN I))
                      (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                      (EQUAL (ADD1 I) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                             0))),

  which simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP STRLEN I))
                      (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                      (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN
                                          (ADD1 I))
                                  0))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                             0))),

  which simplifies, opening up the definition of SEARCH, to:

        T.


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


[ 0.0 0.0 0.0 ]

SEARCH-NON-ZERO


(PROVE-LEMMA MATCH-AT-PATLEN
             (REWRITE)
             (IMPLIES (LESSP PATLEN J)
                      (MATCH PAT J PATLEN STR I STRLEN)))

This conjecture simplifies, expanding MATCH, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MATCH-AT-PATLEN


(PROVE-LEMMA MATCH-AT-STRLEN
             (REWRITE)
             (IMPLIES (LESSP STRLEN I)
                      (EQUAL (MATCH PAT J PATLEN STR I STRLEN)
                             (LESSP PATLEN J))))

This conjecture simplifies, expanding the definition of MATCH, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MATCH-AT-STRLEN


(PROVE-LEMMA MATCH-NEEDS-PATLEN-CHARS
             (REWRITE)
             (IMPLIES (AND (NUMBERP PATLEN)
                           (NUMBERP STRLEN)
                           (NOT (LESSP PATLEN J))
                           (NOT (LESSP STRLEN I))
                           (LESSP (PLUS J STRLEN)
                                  (PLUS I PATLEN)))
                      (NOT (MATCH PAT J PATLEN STR I STRLEN))))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  There are eight plausible
inductions.  They merge into three likely candidate inductions.  However, only
one is unflawed.  We will induct according to the following scheme:
      (AND (IMPLIES (LESSP PATLEN J)
                    (p PAT J PATLEN STR I STRLEN))
           (IMPLIES (AND (NOT (LESSP PATLEN J))
                         (LESSP STRLEN I))
                    (p PAT J PATLEN STR I STRLEN))
           (IMPLIES (AND (NOT (LESSP PATLEN J))
                         (NOT (LESSP STRLEN I))
                         (p PAT
                            (ADD1 J)
                            PATLEN STR
                            (ADD1 I)
                            STRLEN))
                    (p PAT J PATLEN STR I STRLEN))).
Linear arithmetic can be used to prove that the measure:
      (DIFFERENCE (ADD1 PATLEN) J)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for I.  The above
induction scheme leads to four new goals:

Case 4. (IMPLIES (AND (LESSP PATLEN (ADD1 J))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN))),

  which simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (LESSP STRLEN (ADD1 I))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN))),

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

  Case 3.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (LESSP STRLEN (ADD1 I))
                        (NUMBERP PATLEN)
                        (NUMBERP STRLEN)
                        (NOT (LESSP PATLEN J))
                        (NOT (LESSP STRLEN I))
                        (LESSP (PLUS J STRLEN)
                               (PLUS I PATLEN)))
                   (NOT (MATCH PAT J PATLEN STR I STRLEN))),

    which again simplifies, rewriting with SUB1-TYPE-RESTRICTION, and
    unfolding the definitions of LESSP, PLUS, and MATCH, to:

          (IMPLIES (AND (NOT (NUMBERP I))
                        (LESSP STRLEN 1)
                        (NUMBERP PATLEN)
                        (NUMBERP STRLEN)
                        (NOT (LESSP PATLEN J))
                        (LESSP (PLUS J STRLEN) PATLEN)
                        (EQUAL (ELT1 PAT J) (ELT1 STR I)))
                   (NOT (MATCH PAT
                               (ADD1 J)
                               PATLEN STR
                               (ADD1 I)
                               STRLEN))),

    which further simplifies, applying SUB1-TYPE-RESTRICTION, SUB1-ADD1, and
    MATCH-AT-STRLEN, and expanding the definition of LESSP, to the following
    three new conjectures:

    Case 3.2.3.
            (IMPLIES (AND (NOT (NUMBERP I))
                          (LESSP STRLEN 1)
                          (NUMBERP PATLEN)
                          (NUMBERP STRLEN)
                          (NOT (LESSP PATLEN J))
                          (LESSP (PLUS J STRLEN) PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR I)))
                     (NOT (EQUAL PATLEN 0))).

      But this again simplifies, using linear arithmetic, to:

            T.

    Case 3.2.2.
            (IMPLIES (AND (NOT (NUMBERP I))
                          (LESSP STRLEN 1)
                          (NUMBERP PATLEN)
                          (NUMBERP STRLEN)
                          (NOT (LESSP PATLEN J))
                          (LESSP (PLUS J STRLEN) PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR I))
                          (NOT (NUMBERP J)))
                     (NOT (LESSP (SUB1 PATLEN) 0))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 3.2.1.
            (IMPLIES (AND (NOT (NUMBERP I))
                          (LESSP STRLEN 1)
                          (NUMBERP PATLEN)
                          (NUMBERP STRLEN)
                          (NOT (LESSP PATLEN J))
                          (LESSP (PLUS J STRLEN) PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR I))
                          (NUMBERP J))
                     (NOT (LESSP (SUB1 PATLEN) J))),

      which again simplifies, using linear arithmetic, to:

            T.

  Case 3.1.
          (IMPLIES (AND (NUMBERP I)
                        (LESSP I (ADD1 I))
                        (NUMBERP PATLEN)
                        (NOT (LESSP PATLEN J))
                        (NOT (LESSP I I))
                        (LESSP (PLUS J I) (PLUS I PATLEN)))
                   (NOT (MATCH PAT J PATLEN STR I I))),

    which again simplifies, using linear arithmetic, applying SUB1-ADD1,
    COMMUTATIVITY-OF-PLUS, MATCH-AT-STRLEN, and SUB1-TYPE-RESTRICTION, and
    unfolding the definitions of LESSP, EQUAL, PLUS, ADD1, and MATCH, to the
    following six new goals:

    Case 3.1.6.
            (IMPLIES (AND (NUMBERP I)
                          (EQUAL I 0)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NOT (NUMBERP J))
                          (LESSP 0 PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR 0)))
                     (NOT (LESSP PATLEN 1))).

      But this again simplifies, using linear arithmetic, to:

            T.

    Case 3.1.5.
            (IMPLIES (AND (NUMBERP I)
                          (EQUAL I 0)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NUMBERP J)
                          (LESSP J PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR 0)))
                     (NOT (LESSP (SUB1 PATLEN) J))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 3.1.4.
            (IMPLIES (AND (NUMBERP I)
                          (EQUAL I 0)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NUMBERP J)
                          (LESSP J PATLEN)
                          (EQUAL (ELT1 PAT J) (ELT1 STR 0)))
                     (NOT (EQUAL PATLEN 0))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 3.1.3.
            (IMPLIES (AND (NUMBERP I)
                          (LESSP (SUB1 I) I)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NOT (LESSP I I))
                          (LESSP (PLUS I J) (PLUS I PATLEN))
                          (EQUAL (ELT1 PAT J) (ELT1 STR I))
                          (NUMBERP J))
                     (NOT (LESSP (SUB1 PATLEN) J))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 3.1.2.
            (IMPLIES (AND (NUMBERP I)
                          (LESSP (SUB1 I) I)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NOT (LESSP I I))
                          (LESSP (PLUS I J) (PLUS I PATLEN))
                          (EQUAL (ELT1 PAT J) (ELT1 STR I))
                          (NOT (NUMBERP J)))
                     (NOT (LESSP (SUB1 PATLEN) 0))),

      which again simplifies, using linear arithmetic, to:

            T.

    Case 3.1.1.
            (IMPLIES (AND (NUMBERP I)
                          (LESSP (SUB1 I) I)
                          (NUMBERP PATLEN)
                          (NOT (LESSP PATLEN J))
                          (NOT (LESSP I I))
                          (LESSP (PLUS I J) (PLUS I PATLEN))
                          (EQUAL (ELT1 PAT J) (ELT1 STR I)))
                     (NOT (EQUAL PATLEN 0))),

      which again simplifies, using linear arithmetic, to:

            T.

Case 2. (IMPLIES (AND (NOT (LESSP (PLUS (ADD1 J) STRLEN)
                                  (PLUS (ADD1 I) PATLEN)))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN))),

  which simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (MATCH PAT
                                  (ADD1 J)
                                  PATLEN STR
                                  (ADD1 I)
                                  STRLEN))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP PATLEN J))
                      (NOT (LESSP STRLEN I))
                      (LESSP (PLUS J STRLEN)
                             (PLUS I PATLEN)))
                 (NOT (MATCH PAT J PATLEN STR I STRLEN))),

  which simplifies, opening up MATCH, to:

        T.


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


[ 0.0 0.0 0.0 ]

MATCH-NEEDS-PATLEN-CHARS


(PROVE-LEMMA SEARCH-BOUNDARY
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP PATLEN))
                           (NUMBERP STRLEN)
                           (NOT (LESSP STRLEN I))
                           (LESSP (ADD1 STRLEN)
                                  (PLUS PATLEN
                                        (SEARCH PAT STR PATLEN STRLEN I))))
                      (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                             (ADD1 STRLEN))))

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

      (IMPLIES (AND (NOT (EQUAL PATLEN 0))
                    (NUMBERP PATLEN)
                    (NUMBERP STRLEN)
                    (NOT (LESSP STRLEN I))
                    (LESSP (ADD1 STRLEN)
                           (PLUS PATLEN
                                 (SEARCH PAT STR PATLEN STRLEN I))))
               (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                      (ADD1 STRLEN))).

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

      (IMPLIES (AND (NOT (EQUAL PATLEN 0))
                    (NUMBERP PATLEN)
                    (NUMBERP STRLEN)
                    (NOT (LESSP STRLEN I))
                    (NOT (EQUAL (PLUS PATLEN
                                      (SEARCH PAT STR PATLEN STRLEN I))
                                0))
                    (LESSP STRLEN
                           (SUB1 (PLUS PATLEN
                                       (SEARCH PAT STR PATLEN STRLEN I)))))
               (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                      (ADD1 STRLEN))).

Name the above subgoal *1.


     We will appeal to induction.  There are eight plausible inductions.  They
merge into three likely candidate inductions.  However, only one is unflawed.
We will induct according to the following scheme:
      (AND (IMPLIES (LESSP STRLEN I)
                    (p PAT STR PATLEN STRLEN I))
           (IMPLIES (AND (NOT (LESSP STRLEN I))
                         (MATCH PAT 1 PATLEN STR I STRLEN))
                    (p PAT STR PATLEN STRLEN I))
           (IMPLIES (AND (NOT (LESSP STRLEN I))
                         (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                         (p PAT STR PATLEN STRLEN (ADD1 I)))
                    (p PAT STR PATLEN STRLEN I))).
Linear arithmetic informs us that the measure (DIFFERENCE (ADD1 STRLEN) I)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces the following five new
formulas:

Case 5. (IMPLIES (AND (MATCH PAT 1 PATLEN STR I STRLEN)
                      (NOT (EQUAL PATLEN 0))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP STRLEN I))
                      (NOT (EQUAL (PLUS PATLEN
                                        (SEARCH PAT STR PATLEN STRLEN I))
                                  0))
                      (LESSP STRLEN
                             (SUB1 (PLUS PATLEN
                                         (SEARCH PAT STR PATLEN STRLEN I)))))
                 (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                        (ADD1 STRLEN))).

  This simplifies, using linear arithmetic, rewriting with the lemmas
  COMMUTATIVITY-OF-PLUS, SUB1-ADD1, and MATCH-NEEDS-PATLEN-CHARS, and opening
  up SEARCH, LESSP, PLUS, EQUAL, NUMBERP, and SUB1, to:

        (IMPLIES (AND (MATCH PAT 1 PATLEN STR I STRLEN)
                      (NOT (EQUAL PATLEN 0))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP STRLEN I))
                      (NOT (EQUAL (PLUS I PATLEN) 0))
                      (LESSP STRLEN (SUB1 (PLUS I PATLEN))))
                 (EQUAL (SEARCH PAT STR PATLEN STRLEN
                                (ADD1 I))
                        (ADD1 STRLEN))),

  which again simplifies, using linear arithmetic, rewriting with
  MATCH-NEEDS-PATLEN-CHARS, and expanding the functions PLUS, EQUAL, NUMBERP,
  and SUB1, to:

        T.

Case 4. (IMPLIES (AND (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                      (LESSP STRLEN (ADD1 I))
                      (NOT (EQUAL PATLEN 0))
                      (NUMBERP PATLEN)
                      (NUMBERP STRLEN)
                      (NOT (LESSP STRLEN I))
                      (NOT (EQUAL (PLUS PATLEN
                                        (SEARCH PAT STR PATLEN STRLEN I))
                                  0))
                      (LESSP STRLEN
                             (SUB1 (PLUS PATLEN
                                         (SEARCH PAT STR PATLEN STRLEN I)))))
                 (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                        (ADD1 STRLEN))).

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

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                        (LESSP STRLEN (ADD1 I))
                        (NOT (EQUAL PATLEN 0))
                        (NUMBERP PATLEN)
                        (NUMBERP STRLEN)
                        (NOT (LESSP STRLEN I))
                        (NOT (EQUAL (PLUS PATLEN
                                          (SEARCH PAT STR PATLEN STRLEN I))
                                    0))
                        (LESSP STRLEN
                               (SUB1 (PLUS PATLEN
                                           (SEARCH PAT STR PATLEN STRLEN I)))))
                   (EQUAL (SEARCH PAT STR PATLEN STRLEN I)
                          (ADD1 STRLEN))).

    But this again simplifies, using linear arithmetic, rewriting with
    SUB1-TYPE-RESTRICTION, MATCH-AT-STRLEN, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
    MATCH-NEEDS-PATLEN-CHARS, and MATCH-AT-PATLEN, and opening up the
    functions LESSP, SEARCH, ADD1, MATCH, PLUS, EQUAL, NUMBERP, and SUB1, to
    the following four new formulas:

    Case 4.2.4.
            (IMPLIES (AND (NOT (NUMBERP I))
                          (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                          (LESSP STRLEN 1)
                          (NOT (EQUAL PATLEN 0))
                          (NUMBERP PATLEN)
                          (NUMBERP STRLEN)
                          (EQUAL (ELT1 PAT 1) (ELT1 STR I))
                          (LESSP PATLEN 2)
                          (NOT (EQUAL (PLUS PATLEN I) 0))
                          (LESSP STRLEN (SUB1 PATLEN)))
                     (EQUAL (SEARCH PAT STR PATLEN STRLEN
                                    (ADD1 I))
                            (ADD1 STRLEN))).

      This again simplifies, using linear arithmetic, to:

            T.

    Case 4.2.3.
            (IMPLIES (AND (NOT (NUMBERP I))
                          (NOT (MATCH PAT 1 PATLEN STR I STRLEN))
                          (LESSP STRLEN 1)
                          (NOT (EQUAL PATLEN 0))
                          (NUMBERP PATLEN)
                          (NUMBERP STRLEN)
                          (LESSP PATLEN 1)
                          (NOT (EQUAL (PLUS PATLEN I) 0)))