(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 I$0 NIL)

[ 0.0 0.0 0.0 ]

I$0


(DCL ISQRT$1 NIL)

[ 0.0 0.0 0.0 ]

ISQRT$1


(DCL ISQRT$2 NIL)

[ 0.0 0.0 0.0 ]

ISQRT$2


(DEFN SQ (I) (TIMES I I))

     Note that (NUMBERP (SQ I)) is a theorem.




[ 0.0 0.0 0.0 ]

SQ


(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 (NUMBERP (I$0))
           (AND (LESSP (I$0)
                       (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                (ZNUMBERP (I$0)))))

     Observe that (OR (FALSEP (GLOBAL-HYPS)) (TRUEP (GLOBAL-HYPS))) is a
theorem.




[ 0.0 0.0 0.0 ]

GLOBAL-HYPS


(PROVE-LEMMA PLUS-1
             (REWRITE)
             (EQUAL (PLUS 1 X) (ADD1 X)))

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


This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-1


(PROVE-LEMMA DIFFERENCE-2
             (REWRITE)
             (EQUAL (DIFFERENCE (ADD1 (ADD1 X)) 2)
                    (FIX X)))

This formula simplifies, applying SUB1-ADD1, and opening up the functions SUB1,
NUMBERP, EQUAL, DIFFERENCE, and FIX, to:

      (IMPLIES (AND (NUMBERP X) (EQUAL X 0))
               (EQUAL 0 X)),

which again simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-2


(PROVE-LEMMA QUOTIENT-BY-2
             (REWRITE)
             (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                         (SUB1 A))))

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


.

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

Case 3. (IMPLIES (EQUAL A 0)
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))),

  which simplifies, opening up the functions QUOTIENT, PLUS, SUB1, and LESSP,
  to:

        T.

Case 2. (IMPLIES (NOT (NUMBERP A))
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))),

  which simplifies, rewriting with the lemma SUB1-NNUMBERP, and opening up the
  definitions of LESSP, NUMBERP, EQUAL, QUOTIENT, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ADD1 X) 0)))
                 (NOT (LESSP (PLUS (QUOTIENT (ADD1 X) 2)
                                   (QUOTIENT (ADD1 X) 2))
                             X))),

  which simplifies, obviously, to the new goal:

        (IMPLIES (NUMBERP X)
                 (NOT (LESSP (PLUS (QUOTIENT (ADD1 X) 2)
                                   (QUOTIENT (ADD1 X) 2))
                             X))),

  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:

(NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
            (SUB1 A))).

We named this *1.  We will try to prove it by induction.  The recursive terms
in the conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP 2) (p A))
           (IMPLIES (AND (NOT (ZEROP 2)) (LESSP A 2))
                    (p A))
           (IMPLIES (AND (NOT (ZEROP 2))
                         (NOT (LESSP A 2))
                         (p (DIFFERENCE A 2)))
                    (p A))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT A) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to three new goals:

Case 3. (IMPLIES (ZEROP 2)
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))),

  which simplifies, unfolding the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP 2)) (LESSP A 2))
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))),

  which simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP A 1)
                      (NOT (ZEROP 2))
                      (LESSP A 2))
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))).

  This again simplifies, expanding the definitions of ZEROP, QUOTIENT, EQUAL,
  NUMBERP, PLUS, and LESSP, to:

        (IMPLIES (AND (LESSP A 1) (LESSP A 2))
                 (EQUAL (SUB1 A) 0)).

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

  Case 2.3.
          (IMPLIES (AND (EQUAL A 0)
                        (LESSP A 1)
                        (LESSP A 2))
                   (EQUAL (SUB1 A) 0)),

    which further simplifies, expanding the definitions of LESSP, SUB1, and
    EQUAL, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (LESSP A 1)
                        (LESSP A 2))
                   (EQUAL (SUB1 A) 0)),

    which further simplifies, rewriting with SUB1-NNUMBERP, and opening up the
    functions NUMBERP, EQUAL, and LESSP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP X)
                        (NOT (EQUAL (ADD1 X) 0))
                        (LESSP (ADD1 X) 1)
                        (LESSP (ADD1 X) 2))
                   (EQUAL X 0)).

    This further simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP 2))
                      (NOT (LESSP A 2))
                      (NOT (LESSP (PLUS (QUOTIENT (DIFFERENCE A 2) 2)
                                        (QUOTIENT (DIFFERENCE A 2) 2))
                                  (SUB1 (DIFFERENCE A 2)))))
                 (NOT (LESSP (PLUS (QUOTIENT A 2) (QUOTIENT A 2))
                             (SUB1 A)))),

  which simplifies, rewriting with PLUS-ADD1, COMMUTATIVITY-OF-PLUS, and
  SUB1-ADD1, and unfolding ZEROP, QUOTIENT, EQUAL, NUMBERP, and LESSP, to:

        (IMPLIES (AND (NOT (LESSP A 2))
                      (NOT (LESSP (PLUS (QUOTIENT (DIFFERENCE A 2) 2)
                                        (QUOTIENT (DIFFERENCE A 2) 2))
                                  (SUB1 (DIFFERENCE A 2))))
                      (NOT (EQUAL (SUB1 A) 0))
                      (NOT (EQUAL (SUB1 (SUB1 A)) 0)))
                 (NOT (LESSP (PLUS (QUOTIENT (DIFFERENCE A 2) 2)
                                   (QUOTIENT (DIFFERENCE A 2) 2))
                             (SUB1 (SUB1 (SUB1 A)))))),

  which again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP A 1)
                      (NOT (LESSP A 2))
                      (NOT (LESSP (PLUS (QUOTIENT (DIFFERENCE A 2) 2)
                                        (QUOTIENT (DIFFERENCE A 2) 2))
                                  (SUB1 (DIFFERENCE A 2))))
                      (NOT (EQUAL (SUB1 A) 0))
                      (NOT (EQUAL (SUB1 (SUB1 A)) 0)))
                 (NOT (LESSP (PLUS (QUOTIENT (DIFFERENCE A 2) 2)
                                   (QUOTIENT (DIFFERENCE A 2) 2))
                             (SUB1 (SUB1 (SUB1 A)))))).

  This again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

QUOTIENT-BY-2


(PROVE-LEMMA MAIN-TRICK
             (REWRITE)
             (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS J K) 2)))
                         (PLUS (TIMES J K) J)))
             ((INDUCT (LESSP J K))))

WARNING:  Note that the linear lemma MAIN-TRICK is being stored under the term:
      (SQ (ADD1 (QUOTIENT (PLUS J K) 2))),
which is unusual because SQ is a nonrecursive function symbol.


WARNING:  Note that the proposed lemma MAIN-TRICK 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 NOT, OR, and AND,
to three new goals:

Case 3. (IMPLIES (OR (EQUAL K 0) (NOT (NUMBERP K)))
                 (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS J K) 2)))
                             (PLUS (TIMES J K) J)))),

  which simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS,
  COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1, COMMUTATIVITY-OF-TIMES,
  TIMES-ADD1, PLUS-NON-NUMBERP, and TIMES-NON-NUMBERP, and unfolding the
  functions NOT, OR, EQUAL, PLUS, SQ, TIMES, and LESSP, to two new formulas:

  Case 3.2.
          (IMPLIES (AND (EQUAL K 0)
                        (NUMBERP J)
                        (NOT (EQUAL J 0)))
                   (NOT (LESSP (PLUS (QUOTIENT J 2)
                                     (QUOTIENT J 2)
                                     (TIMES (QUOTIENT J 2) (QUOTIENT J 2)))
                               (SUB1 J)))),

    which again simplifies, using linear arithmetic and rewriting with
    QUOTIENT-BY-2, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (NUMBERP K))
                        (NUMBERP J)
                        (NOT (EQUAL J 0)))
                   (NOT (LESSP (PLUS (QUOTIENT J 2)
                                     (QUOTIENT J 2)
                                     (TIMES (QUOTIENT J 2) (QUOTIENT J 2)))
                               (SUB1 J)))).

    However this again simplifies, using linear arithmetic and rewriting with
    the lemma QUOTIENT-BY-2, to:

          T.

Case 2. (IMPLIES (AND (NOT (EQUAL K 0))
                      (NUMBERP K)
                      (OR (EQUAL J 0) (NOT (NUMBERP J))))
                 (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS J K) 2)))
                             (PLUS (TIMES J K) J)))),

  which simplifies, rewriting with COMMUTATIVITY2-OF-PLUS, PLUS-ADD1,
  SUB1-ADD1, COMMUTATIVITY-OF-TIMES, TIMES-ADD1, and PLUS-NON-NUMBERP, and
  expanding NOT, OR, EQUAL, PLUS, SQ, TIMES, LESSP, and NUMBERP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL K 0))
                      (NUMBERP K)
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS (SUB1 J) (SUB1 K))
                                                      2)))
                                  (PLUS (TIMES (SUB1 J) (SUB1 K))
                                        (SUB1 J)))))
                 (NOT (LESSP (SQ (ADD1 (QUOTIENT (PLUS J K) 2)))
                             (PLUS (TIMES J K) J)))).

  This simplifies, applying the lemmas COMMUTATIVITY2-OF-PLUS, PLUS-ADD1,
  SUB1-ADD1, COMMUTATIVITY-OF-TIMES, TIMES-ADD1, COMMUTATIVITY-OF-PLUS,
  DIFFERENCE-2, and ASSOCIATIVITY-OF-PLUS, and expanding the definitions of
  PLUS, SQ, LESSP, SUB1, NUMBERP, EQUAL, QUOTIENT, and TIMES, to the following
  two new goals:

  Case 1.2.
          (IMPLIES
                 (AND (NOT (EQUAL K 0))
                      (NUMBERP K)
                      (NOT (EQUAL J 0))
                      (NUMBERP J)
                      (EQUAL (PLUS (SUB1 J)
                                   (TIMES (SUB1 J) (SUB1 K)))
                             0)
                      (NOT (EQUAL (PLUS (SUB1 J) (SUB1 K)) 0))
                      (NOT (EQUAL (SUB1 (PLUS (SUB1 J) (SUB1 K)))
                                  0)))
                 (NOT (LESSP (PLUS (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                   (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                   (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                   (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                   (TIMES (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                          (QUOTIENT (PLUS (SUB1 J) (SUB1 K))
                                                    2)))
                             (SUB1 (SUB1 (PLUS (SUB1 J) (SUB1 K))))))).

    But this again simplifies, using linear arithmetic and applying
    QUOTIENT-BY-2, to:

          T.

  Case 1.1.
          (IMPLIES
           (AND (NOT (EQUAL K 0))
                (NUMBERP K)
                (NOT (EQUAL J 0))
                (NUMBERP J)
                (NOT (LESSP (PLUS (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                  (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                  (TIMES (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                         (QUOTIENT (PLUS (SUB1 J) (SUB1 K))
                                                   2)))
                            (SUB1 (PLUS (SUB1 J)
                                        (TIMES (SUB1 J) (SUB1 K))))))
                (NOT (EQUAL (PLUS K
                                  (SUB1 J)
                                  (SUB1 J)
                                  (TIMES (SUB1 J) (SUB1 K)))
                            0))
                (NOT (EQUAL (SUB1 (PLUS K
                                        (SUB1 J)
                                        (SUB1 J)
                                        (TIMES (SUB1 J) (SUB1 K))))
                            0))
                (NOT (EQUAL (SUB1 (SUB1 (PLUS K
                                              (SUB1 J)
                                              (SUB1 J)
                                              (TIMES (SUB1 J) (SUB1 K)))))
                            0)))
           (NOT
               (LESSP (PLUS (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                            (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                            (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                            (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                            (TIMES (QUOTIENT (PLUS (SUB1 J) (SUB1 K)) 2)
                                   (QUOTIENT (PLUS (SUB1 J) (SUB1 K))
                                             2)))
                      (SUB1 (SUB1 (SUB1 (PLUS K
                                              (SUB1 J)
                                              (SUB1 J)
                                              (TIMES (SUB1 J) (SUB1 K))))))))).

    However this again simplifies, using linear arithmetic and rewriting with
    the lemma QUOTIENT-BY-2, to:

          T.

Q.E.D.


[ 0.0 0.2 0.0 ]

MAIN-TRICK


(PROVE-LEMMA LESSP-REMAINDER2
             (REWRITE GENERALIZE)
             (EQUAL (LESSP (REMAINDER X Y) Y)
                    (NOT (ZEROP Y))))

This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions
ZEROP and NOT, to three new goals:

Case 3. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which we will name *1.

Case 2. (IMPLIES (LESSP (REMAINDER X Y) Y)
                 (NUMBERP Y)).

  This again simplifies, expanding REMAINDER and LESSP, to:

        T.

Case 1. (IMPLIES (LESSP (REMAINDER X Y) Y)
                 (NOT (EQUAL Y 0))),

  which again simplifies, using linear arithmetic, to:

        T.


     So let us turn our attention to:

      (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
                    (NOT (EQUAL Y 0)))
               (NOT (NUMBERP Y))),

which we named *1 above.  We will try to prove it by induction.  There are two
plausible inductions.  However, only one is unflawed.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p Y X))
           (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
                    (p Y X))
           (IMPLIES (AND (NOT (ZEROP Y))
                         (NOT (LESSP X Y))
                         (p Y (DIFFERENCE X Y)))
                    (p Y X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to three new goals:

Case 3. (IMPLIES (AND (ZEROP Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, opening up ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Y))
                      (LESSP X Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

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

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

  However this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (NOT (LESSP X Y))
                      (LESSP (REMAINDER (DIFFERENCE X Y) Y)
                             Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

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

        T.


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


[ 0.0 0.0 0.0 ]

LESSP-REMAINDER2


(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
             (ELIM)
             (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
                      (EQUAL (PLUS (REMAINDER X Y)
                                   (TIMES Y (QUOTIENT X Y)))
                             X)))

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

      (IMPLIES (AND (NOT (EQUAL Y 0))
                    (NUMBERP Y)
                    (NUMBERP X))
               (EQUAL (PLUS (REMAINDER X Y)
                            (TIMES Y (QUOTIENT X Y)))
                      X)),

which we will name *1.


     We will appeal to induction.  The recursive terms in the conjecture
suggest three inductions.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP Y) (p X Y))
           (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
                    (p X Y))
           (IMPLIES (AND (NOT (ZEROP Y))
                         (NOT (LESSP X Y))
                         (p (DIFFERENCE X Y) Y))
                    (p X Y))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP can be used to establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces three new goals:

Case 3. (IMPLIES (AND (ZEROP Y)
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)),

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

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Y))
                      (LESSP X Y)
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)),

  which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and unfolding ZEROP, REMAINDER, QUOTIENT, EQUAL,
  TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (NOT (LESSP X Y))
                      (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
                                   (TIMES Y
                                          (QUOTIENT (DIFFERENCE X Y) Y)))
                             (DIFFERENCE X Y))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)).

  This simplifies, rewriting with TIMES-ADD1 and COMMUTATIVITY2-OF-PLUS, and
  opening up the definitions of ZEROP, REMAINDER, and QUOTIENT, to the goal:

        (IMPLIES (AND (NOT (LESSP X Y))
                      (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
                                   (TIMES Y
                                          (QUOTIENT (DIFFERENCE X Y) Y)))
                             (DIFFERENCE X Y))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (PLUS Y (DIFFERENCE X Y)) X)).

  However this again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

REMAINDER-QUOTIENT-ELIM


(PROVE-LEMMA SQ-ADD1-NON-ZERO
             (REWRITE)
             (NOT (EQUAL (SQ (ADD1 X)) 0)))

This conjecture simplifies, appealing to the lemmas COMMUTATIVITY2-OF-PLUS,
PLUS-ADD1, SUB1-ADD1, COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding
the functions PLUS and SQ, to the following two new goals:

Case 2. (IMPLIES (NOT (NUMBERP X))
                 (NOT (EQUAL (ADD1 X) 0))).

  This again simplifies, using linear arithmetic, to:

        T.

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

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SQ-ADD1-NON-ZERO


(DISABLE SQ)

[ 0.0 0.0 0.0 ]

SQ-OFF


(PROVE-LEMMA MAIN
             (REWRITE)
             (IMPLIES (NOT (ZEROP J))
                      (LESSP I
                             (SQ (ADD1 (QUOTIENT (PLUS J (QUOTIENT I J))
                                                 2))))))

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


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

      (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J))
               (LESSP I
                      (SQ (ADD1 (QUOTIENT (PLUS J (QUOTIENT I J))
                                          2))))).

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by (PLUS Z (TIMES J X))
to eliminate (QUOTIENT I J) and (REMAINDER I J).  We use LESSP-REMAINDER2, the
type restriction lemma noted when QUOTIENT was introduced, and the type
restriction lemma noted when REMAINDER was introduced to restrict the new
variables.  This produces the following two new formulas:

Case 2. (IMPLIES (AND (NOT (NUMBERP I))
                      (NOT (EQUAL J 0))
                      (NUMBERP J))
                 (LESSP I
                        (SQ (ADD1 (QUOTIENT (PLUS J (QUOTIENT I J))
                                            2))))).

  This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-PLUS and
  SQ-ADD1-NON-ZERO, and opening up LESSP, QUOTIENT, EQUAL, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (EQUAL (LESSP Z J) (NOT (ZEROP J)))
                      (NOT (EQUAL J 0))
                      (NUMBERP J))
                 (LESSP (PLUS Z (TIMES J X))
                        (SQ (ADD1 (QUOTIENT (PLUS J X) 2))))),

  which simplifies, opening up ZEROP and NOT, to:

        (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (LESSP Z J)
                      (NOT (EQUAL J 0))
                      (NUMBERP J))
                 (LESSP (PLUS Z (TIMES J X))
                        (SQ (ADD1 (QUOTIENT (PLUS J X) 2))))).

  However this again simplifies, using linear arithmetic and rewriting with
  MAIN-TRICK and COMMUTATIVITY-OF-PLUS, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MAIN


(ENABLE SQ)

[ 0.0 0.0 0.0 ]

SQ-ON


(PROVE-LEMMA LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR
             (REWRITE)
             (IMPLIES (NOT (LESSP I J))
                      (NOT (LESSP (TIMES A I) (TIMES A J))))
             NIL)

WARNING:  When the linear lemma LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR
is stored under (TIMES A J) it contains the free variable I which will be
chosen by instantiating the hypothesis (NOT (LESSP I J)).


WARNING:  When the linear lemma LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR
is stored under (TIMES A I) it contains the free variable J which will be
chosen by instantiating the hypothesis (NOT (LESSP I J)).


WARNING:  Note that the proposed lemma:
      LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR
is to be stored as zero type prescription rules, zero compound recognizer
rules, two linear rules, and zero replacement rules.



     Name the conjecture *1.


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

Case 2. (IMPLIES (AND (ZEROP A) (NOT (LESSP I J)))
                 (NOT (LESSP (TIMES A I) (TIMES A J)))).

  This simplifies, opening up ZEROP, EQUAL, TIMES, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP A))
                      (NOT (LESSP (TIMES (SUB1 A) I)
                                  (TIMES (SUB1 A) J)))
                      (NOT (LESSP I J)))
                 (NOT (LESSP (TIMES A I) (TIMES A J)))).

  This simplifies, unfolding the definitions of ZEROP and TIMES, to the new
  conjecture:

        (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (LESSP (TIMES (SUB1 A) I)
                                  (TIMES (SUB1 A) J)))
                      (NOT (LESSP I J)))
                 (NOT (LESSP (PLUS I (TIMES (SUB1 A) I))
                             (PLUS J (TIMES (SUB1 A) J))))),

  which again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR


(PROVE-LEMMA MULTIPLY-THRU-BY-DIVISOR
             (REWRITE)
             (IMPLIES (LESSP A (TIMES B C))
                      (EQUAL (LESSP (QUOTIENT A B) C) T)))

.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS Z (TIMES B X)) to eliminate (QUOTIENT A B) and (REMAINDER A B).  We
employ LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to constrain the new variables.  The result is four new formulas:

Case 4. (IMPLIES (AND (NOT (NUMBERP A))
                      (LESSP A (TIMES B C)))
                 (LESSP (QUOTIENT A B) C)),

  which further simplifies, appealing to the lemma EQUAL-TIMES-0, and opening
  up the definitions of LESSP, QUOTIENT, and EQUAL, to:

        T.

Case 3. (IMPLIES (AND (EQUAL B 0)
                      (LESSP A (TIMES B C)))
                 (LESSP (QUOTIENT A B) C)),

  which further simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP B))
                      (LESSP A (TIMES B C)))
                 (LESSP (QUOTIENT A B) C)),

  which further simplifies, expanding the definitions of TIMES, EQUAL, and
  LESSP, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (EQUAL (LESSP Z B) (NOT (ZEROP B)))
                      (NUMBERP B)
                      (NOT (EQUAL B 0))
                      (LESSP (PLUS Z (TIMES B X))
                             (TIMES B C)))
                 (LESSP X C)),

  which further simplifies, using linear arithmetic and applying
  LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MULTIPLY-THRU-BY-DIVISOR


(PROVE-LEMMA TIMES-GREATERP-ZERO
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP X)) (NOT (ZEROP Y)))
                      (LESSP 0 (TIMES X Y))))

WARNING:  Note that the proposed lemma TIMES-GREATERP-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,
and IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL X 0))
                    (NUMBERP X)
                    (NOT (EQUAL Y 0))
                    (NUMBERP Y))
               (LESSP 0 (TIMES X Y))).

This simplifies, applying EQUAL-TIMES-0, and opening up the definitions of
EQUAL and LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-GREATERP-ZERO


(PROVE-LEMMA QUOTIENT-SHRINKS
             (REWRITE)
             (NOT (LESSP I (QUOTIENT I J))))

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


.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace I by
(PLUS Z (TIMES J X)) to eliminate (QUOTIENT I J) and (REMAINDER I J).  We rely
upon LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to constrain the new variables.  We must thus prove four new conjectures:

Case 4. (IMPLIES (NOT (NUMBERP I))
                 (NOT (LESSP I (QUOTIENT I J)))),

  which simplifies, expanding LESSP, QUOTIENT, and EQUAL, to:

        T.

Case 3. (IMPLIES (EQUAL J 0)
                 (NOT (LESSP I (QUOTIENT I J)))),

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

        T.

Case 2. (IMPLIES (NOT (NUMBERP J))
                 (NOT (LESSP I (QUOTIENT I J)))),

  which simplifies, unfolding QUOTIENT, EQUAL, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (EQUAL (LESSP Z J) (NOT (ZEROP J)))
                      (NUMBERP J)
                      (NOT (EQUAL J 0)))
                 (NOT (LESSP (PLUS Z (TIMES J X)) X))),

  which simplifies, unfolding ZEROP and NOT, to:

        (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (LESSP Z J)
                      (NUMBERP J)
                      (NOT (EQUAL J 0)))
                 (NOT (LESSP (PLUS Z (TIMES J X)) X))),

  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:

(NOT (LESSP I (QUOTIENT I J))),

which we named *1 above.  We will appeal to induction.  There are two
plausible inductions, both of which are unflawed.  So we will choose the one
suggested by the largest number of nonprimitive recursive functions.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP J) (p I J))
           (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J))
                    (p I J))
           (IMPLIES (AND (NOT (ZEROP J))
                         (NOT (LESSP I J))
                         (p (DIFFERENCE I J) J))
                    (p I J))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP establish that the measure (COUNT I) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme generates the following three new conjectures:

Case 3. (IMPLIES (ZEROP J)
                 (NOT (LESSP I (QUOTIENT I J)))).

  This simplifies, expanding the definitions of ZEROP, EQUAL, QUOTIENT, and
  LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J))
                 (NOT (LESSP I (QUOTIENT I J)))).

  This simplifies, expanding the definitions of ZEROP, QUOTIENT, EQUAL, and
  LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP J))
                      (NOT (LESSP I J))
                      (NOT (LESSP (DIFFERENCE I J)
                                  (QUOTIENT (DIFFERENCE I J) J))))
                 (NOT (LESSP I (QUOTIENT I J)))).

  This simplifies, applying SUB1-ADD1, and unfolding the definitions of ZEROP,
  QUOTIENT, and LESSP, to three new goals:

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

    which again simplifies, using linear arithmetic, to:

          T.

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

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

          T.

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

    which again simplifies, using linear arithmetic, to:

          T.


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


[ 0.0 0.0 0.0 ]

QUOTIENT-SHRINKS


(PROVE-LEMMA QUOTIENT-SHRINKS-FAST
             (REWRITE)
             (NOT (LESSP I (TIMES 2 (QUOTIENT I 2)))))

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


.

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by (PLUS Z (TIMES 2 X))
to eliminate (QUOTIENT I 2) and (REMAINDER I 2).  We rely upon
LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to restrict the new variables.  We thus obtain the following four new
conjectures:

Case 4. (IMPLIES (NOT (NUMBERP I))
                 (NOT (LESSP I (TIMES 2 (QUOTIENT I 2))))).

  But this simplifies, opening up the definitions of LESSP, NUMBERP, EQUAL,
  QUOTIENT, and TIMES, to:

        T.

Case 3. (IMPLIES (EQUAL 2 0)
                 (NOT (LESSP I (TIMES 2 (QUOTIENT I 2))))),

  which simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (NOT (NUMBERP 2))
                 (NOT (LESSP I (TIMES 2 (QUOTIENT I 2))))),

  which simplifies, obviously, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (NUMBERP Z)
                      (EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
                      (NOT (EQUAL 2 0)))
                 (NOT (LESSP (PLUS Z (TIMES 2 X))
                             (TIMES 2 X)))).

  But this simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-SHRINKS-FAST


(PROVE-LEMMA QUOTIENT-BY-1
             (REWRITE)
             (EQUAL (QUOTIENT I 1) (FIX I)))

This simplifies, unfolding FIX, to two new formulas:

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

  which again simplifies, unfolding LESSP, NUMBERP, EQUAL, and QUOTIENT, to:

        T.

Case 1. (IMPLIES (NUMBERP I)
                 (EQUAL (QUOTIENT I 1) I)).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by
  (PLUS Z (TIMES 1 X)) to eliminate (QUOTIENT I 1) and (REMAINDER I 1).  We
  rely upon LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT
  was introduced, and the type restriction lemma noted when REMAINDER was
  introduced to restrict the new variables.  We would thus like to prove the
  following three new goals:

  Case 1.3.
          (IMPLIES (AND (EQUAL 1 0) (NUMBERP I))
                   (EQUAL (QUOTIENT I 1) I)).

    However this further simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP 1)) (NUMBERP I))
                   (EQUAL (QUOTIENT I 1) I)),

    which further simplifies, obviously, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Z)
                        (EQUAL (LESSP Z 1) (NOT (ZEROP 1)))
                        (NOT (EQUAL 1 0)))
                   (EQUAL X (PLUS Z (TIMES 1 X)))).

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

          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Z)
                        (LESSP Z 1))
                   (EQUAL X (PLUS Z (TIMES 1 X)))).

    But this again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-BY-1


(ADD-AXIOM INPUT NIL T)

[ 0.0 0.0 0.0 ]

INPUT


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-T


(PROVE-LEMMA STOP NIL
             (OR (NOT (ZLESSP (I$0) '0))
                 (NOT (GLOBAL-HYPS))))

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

      (IMPLIES (AND (ZLESSP (I$0) 0)
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
               (NOT (ZNUMBERP (I$0)))).

This simplifies, expanding LESSP, EQUAL, NEGATIVEP, and ZLESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

STOP


(UBT LOGICAL-IF-T)

LOGICAL-IF-T


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-T


(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT NIL
             (IMPLIES (AND (ZGREATERP (I$0) '1)
                           (GLOBAL-HYPS))
                      (AND (NOT (ZEQP '2 '0))
                           (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) '2)))))

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

      (IMPLIES (AND (ZLESSP 1 (I$0))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0)))
               (AND (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
                    (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) 2)))),

which simplifies, using linear arithmetic, applying COMMUTATIVITY-OF-PLUS and
MULTIPLY-THRU-BY-DIVISOR, and opening up the definitions of NEGATIVEP, ZLESSP,
ZNUMBERP, ZNORMALIZE, EQUAL, NOT, ZQUOTIENT, PLUS, TIMES, NUMBERP, SUB1,
EXPRESSIBLE-ZNUMBERP, and AND, to:

      (IMPLIES
          (AND (LESSP 1 (I$0))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (QUOTIENT (I$0) 2) 0))),

which again simplifies, using linear arithmetic and applying INTEGER-SIZE, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZQUOTIENT


(ADD-AXIOM ASSIGNMENT
           (REWRITE)
           (EQUAL (ISQRT$1)
                  (ZQUOTIENT (I$0) '2)))

[ 0.0 0.0 0.0 ]

ASSIGNMENT


(PROVE-LEMMA LP NIL
            (IMPLIES (AND (ZGREATERP (I$0) '1)
                          (GLOBAL-HYPS))
                     (AND (AND (LESSP '0 (ISQRT$1))
                               (AND (NOT (LESSP (I$0) (TIMES '2 (ISQRT$1))))
                                    (AND (NUMBERP (ISQRT$1))
                                         (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))))
                          (LEX (CONS (ISQRT$1) 'NIL)
                               (CONS (I$0) 'NIL)))))

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

      (IMPLIES (AND (ZLESSP 1 (I$0))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0)))
               (AND (AND (LESSP 0 (ZQUOTIENT (I$0) 2))
                         (NOT (LESSP (I$0)
                                     (TIMES 2 (ZQUOTIENT (I$0) 2))))
                         (NUMBERP (ZQUOTIENT (I$0) 2))
                         (LESSP (I$0)
                                (SQ (ADD1 (ZQUOTIENT (I$0) 2)))))
                    (LEX (LIST (ZQUOTIENT (I$0) 2))
                         (LIST (I$0))))).

This simplifies, appealing to the lemmas COMMUTATIVITY2-OF-PLUS, PLUS-ADD1,
SUB1-ADD1, COMMUTATIVITY-OF-TIMES, TIMES-ADD1, CDR-CONS, and CAR-CONS, and
unfolding the functions NEGATIVEP, ZLESSP, ZNUMBERP, ZQUOTIENT, EQUAL, LESSP,
NOT, PLUS, SQ, AND, and LEX, to the following four new formulas:

Case 4. (IMPLIES (AND (LESSP 1 (I$0))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                 (NOT (EQUAL (QUOTIENT (I$0) 2) 0))).

  However this again simplifies, using linear arithmetic, rewriting with the
  lemma QUOTIENT-BY-2, and unfolding PLUS, to:

        T.

Case 3. (IMPLIES (AND (LESSP 1 (I$0))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                 (NOT (LESSP (I$0)
                             (TIMES 2 (QUOTIENT (I$0) 2))))),

  which again simplifies, using linear arithmetic and rewriting with
  QUOTIENT-SHRINKS-FAST, to:

        T.

Case 2. (IMPLIES (AND (LESSP 1 (I$0))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (I$0) 0)))
                 (LESSP (SUB1 (I$0))
                        (PLUS (QUOTIENT (I$0) 2)
                              (QUOTIENT (I$0) 2)
                              (TIMES (QUOTIENT (I$0) 2)
                                     (QUOTIENT (I$0) 2))))).

  However this again simplifies, using linear arithmetic and applying
  TIMES-GREATERP-ZERO and QUOTIENT-BY-2, to:

        T.

Case 1. (IMPLIES (AND (LESSP 1 (I$0))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                 (LESSP (QUOTIENT (I$0) 2) (I$0))).

  This again simplifies, using linear arithmetic and appealing to the lemma
  QUOTIENT-SHRINKS-FAST, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LP


(UBT LOGICAL-IF-T)

LOGICAL-IF-T


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F1


(ADD-AXIOM ASSIGNMENT
           (REWRITE)
           (EQUAL (ISQRT$1) (I$0)))

[ 0.0 0.0 0.0 ]

ASSIGNMENT


(PROVE-LEMMA OUTPUT NIL
             (IMPLIES (AND (NOT (ZGREATERP (I$0) '1))
                           (GLOBAL-HYPS))
                      (AND (ZNUMBERP (ISQRT$1))
                           (AND (ZGREATEREQP (ISQRT$1) '0)
                                (AND (NOT (LESSP (I$0) (SQ (ISQRT$1))))
                                     (LESSP (I$0)
                                            (SQ (PLUS '1 (ISQRT$1)))))))))

This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, PLUS-1, ASSIGNMENT, and ZGREATERP, to:

      (IMPLIES (AND (NOT (ZLESSP 1 (I$0)))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0)))
               (AND (ZNUMBERP (I$0))
                    (ZGREATEREQP (I$0) 0)
                    (NOT (LESSP (I$0) (SQ (I$0))))
                    (LESSP (I$0) (SQ (ADD1 (I$0)))))).

This simplifies, applying COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding the definitions of
NEGATIVEP, ZLESSP, ZNUMBERP, EQUAL, LESSP, ZGREATEREQP, SQ, NOT, PLUS, and AND,
to two new formulas:

Case 2. (IMPLIES (AND (NOT (LESSP 1 (I$0)))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
                 (NOT (LESSP (I$0) (TIMES (I$0) (I$0))))),

  which again simplifies, using linear arithmetic, rewriting with
  LESSP-TIMES-CANCELLATION-RESTATED-FOR-LINEAR, COMMUTATIVITY-OF-TIMES, and
  COMMUTATIVITY-OF-PLUS, and expanding the functions PLUS, TIMES, EQUAL,
  NUMBERP, and SUB1, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP 1 (I$0)))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (I$0) 0)))
                 (LESSP (SUB1 (I$0))
                        (PLUS (I$0)
                              (I$0)
                              (TIMES (I$0) (I$0))))).

  This again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

OUTPUT


(UBT INPUT)

INPUT


(ADD-AXIOM PATHS-FROM-LP
           (REWRITE)
           '*1*TRUE)

WARNING:  Note that the proposed lemma PATHS-FROM-LP 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 ]

PATHS-FROM-LP


(DEFN PATH-HYPS NIL
      (AND (GLOBAL-HYPS)
           (AND (LESSP '0 (ISQRT$1))
                (AND (NOT (LESSP (I$0) (TIMES '2 (ISQRT$1))))
                     (AND (NUMBERP (ISQRT$1))
                          (LESSP (I$0)
                                 (SQ (ADD1 (ISQRT$1)))))))))

     Note 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 (ISQRT$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


(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT NIL
            (IMPLIES (PATH-HYPS)
                     (AND (NOT (ZEQP (ISQRT$1) '0))
                          (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) (ISQRT$1))))))

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

      (IMPLIES (AND (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0))
                    (LESSP 0 (ISQRT$1))
                    (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                    (NUMBERP (ISQRT$1))
                    (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
               (AND (NOT (EQUAL (ZNORMALIZE (ISQRT$1))
                                (ZNORMALIZE 0)))
                    (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) (ISQRT$1))))).

This simplifies, applying COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and opening up the definitions of
ZNUMBERP, EQUAL, LESSP, PLUS, SQ, ZNORMALIZE, NOT, QUOTIENT, NEGATIVEP,
ZQUOTIENT, ZLESSP, EXPRESSIBLE-ZNUMBERP, and AND, to four new goals:

Case 4. (IMPLIES
          (AND (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (EQUAL (I$0) 0))
          (NOT (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (EQUAL (I$0) 0))
                 (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                             0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES
          (AND (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (LESSP (SUB1 (I$0))
                      (PLUS (ISQRT$1)
                            (ISQRT$1)
                            (TIMES (ISQRT$1) (ISQRT$1))))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (QUOTIENT (I$0) (ISQRT$1))
                      0))),

  which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
  to:

        T.

Case 1. (IMPLIES (AND (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (SUB1 (I$0))
                             (PLUS (ISQRT$1)
                                   (ISQRT$1)
                                   (TIMES (ISQRT$1) (ISQRT$1)))))
                 (LESSP (QUOTIENT (I$0) (ISQRT$1))
                        (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))).

  This again simplifies, using linear arithmetic and applying QUOTIENT-SHRINKS,
  to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZQUOTIENT


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-T


(PROVE-LEMMA OUTPUT1 NIL
             (IMPLIES (AND (ZGREATEREQP (ZQUOTIENT (I$0) (ISQRT$1))
                                        (ISQRT$1))
                           (PATH-HYPS))
                      (AND (ZNUMBERP (ISQRT$1))
                           (AND (ZGREATEREQP (ISQRT$1) '0)
                                (AND (NOT (LESSP (I$0) (SQ (ISQRT$1))))
                                     (LESSP (I$0)
                                            (SQ (PLUS '1 (ISQRT$1)))))))))

This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
ZGREATEREQP, AND, IMPLIES, and PLUS-1, to:

      (IMPLIES (AND (NOT (ZLESSP (ZQUOTIENT (I$0) (ISQRT$1))
                                 (ISQRT$1)))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0))
                    (LESSP 0 (ISQRT$1))
                    (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                    (NUMBERP (ISQRT$1))
                    (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
               (AND (ZNUMBERP (ISQRT$1))
                    (ZGREATEREQP (ISQRT$1) 0)
                    (NOT (LESSP (I$0) (SQ (ISQRT$1))))
                    (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))),

which simplifies, rewriting with COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1,
COMMUTATIVITY-OF-TIMES, TIMES-ADD1, and EQUAL-TIMES-0, and opening up
ZQUOTIENT, ZLESSP, ZNUMBERP, EQUAL, LESSP, PLUS, SQ, NEGATIVEP, ZGREATEREQP,
NOT, and AND, to the following two new formulas:

Case 2. (IMPLIES (AND (NOT (LESSP (QUOTIENT (I$0) (ISQRT$1))
                                  (ISQRT$1)))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1)))
                 (NOT (EQUAL (I$0) 0))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP (QUOTIENT (I$0) (ISQRT$1))
                                  (ISQRT$1)))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (SUB1 (I$0))
                             (PLUS (ISQRT$1)
                                   (ISQRT$1)
                                   (TIMES (ISQRT$1) (ISQRT$1)))))
                 (NOT (LESSP (I$0)
                             (TIMES (ISQRT$1) (ISQRT$1))))),

  which again simplifies, applying MULTIPLY-THRU-BY-DIVISOR, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

OUTPUT1


(UBT LOGICAL-IF-T)

LOGICAL-IF-T


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

[ 0.0 0.0 0.0 ]

LOGICAL-IF-F2


(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT1 NIL
            (IMPLIES (AND (NOT (ZGREATEREQP (ZQUOTIENT (I$0) (ISQRT$1))
                                            (ISQRT$1)))
                          (PATH-HYPS))
                     (AND (NOT (ZEQP (ISQRT$1) '0))
                          (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) (ISQRT$1))))))

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

      (IMPLIES (AND (ZLESSP (ZQUOTIENT (I$0) (ISQRT$1))
                            (ISQRT$1))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0))
                    (LESSP 0 (ISQRT$1))
                    (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                    (NUMBERP (ISQRT$1))
                    (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
               (AND (NOT (EQUAL (ZNORMALIZE (ISQRT$1))
                                (ZNORMALIZE 0)))
                    (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (I$0) (ISQRT$1))))).

This simplifies, applying COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and opening up the functions ZQUOTIENT,
ZLESSP, ZNUMBERP, EQUAL, LESSP, PLUS, SQ, ZNORMALIZE, NOT, QUOTIENT, NEGATIVEP,
EXPRESSIBLE-ZNUMBERP, and AND, to four new conjectures:

Case 4. (IMPLIES
          (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                      (ISQRT$1))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (EQUAL (I$0) 0))
          (NOT (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (EQUAL (I$0) 0))
                 (NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
                             0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES
          (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                      (ISQRT$1))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (LESSP (SUB1 (I$0))
                      (PLUS (ISQRT$1)
                            (ISQRT$1)
                            (TIMES (ISQRT$1) (ISQRT$1))))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (QUOTIENT (I$0) (ISQRT$1))
                      0))),

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

        T.

Case 1. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (SUB1 (I$0))
                             (PLUS (ISQRT$1)
                                   (ISQRT$1)
                                   (TIMES (ISQRT$1) (ISQRT$1)))))
                 (LESSP (QUOTIENT (I$0) (ISQRT$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-ZQUOTIENT1


(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
          (IMPLIES (AND (NOT (ZGREATEREQP (ZQUOTIENT (I$0) (ISQRT$1))
                                          (ISQRT$1)))
                        (PATH-HYPS))
                   (EXPRESSIBLE-ZNUMBERP (ZPLUS (ISQRT$1)
                                                (ZQUOTIENT (I$0) (ISQRT$1))))))

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

      (IMPLIES (AND (ZLESSP (ZQUOTIENT (I$0) (ISQRT$1))
                            (ISQRT$1))
                    (NUMBERP (I$0))
                    (LESSP (I$0)
                           (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                    (ZNUMBERP (I$0))
                    (LESSP 0 (ISQRT$1))
                    (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                    (NUMBERP (ISQRT$1))
                    (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
               (EXPRESSIBLE-ZNUMBERP (ZPLUS (ISQRT$1)
                                            (ZQUOTIENT (I$0) (ISQRT$1))))),

which simplifies, rewriting with COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1,
COMMUTATIVITY-OF-TIMES, TIMES-ADD1, and COMMUTATIVITY-OF-PLUS, and expanding
the definitions of ZQUOTIENT, ZLESSP, ZNUMBERP, EQUAL, LESSP, PLUS, SQ,
QUOTIENT, NEGATIVEP, ZPLUS, and EXPRESSIBLE-ZNUMBERP, to the following three
new goals:

Case 3. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (EQUAL (I$0) 0))
                 (LESSP (ISQRT$1)
                        (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES
          (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                      (ISQRT$1))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (LESSP (SUB1 (I$0))
                      (PLUS (ISQRT$1)
                            (ISQRT$1)
                            (TIMES (ISQRT$1) (ISQRT$1))))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (PLUS (ISQRT$1)
                            (QUOTIENT (I$0) (ISQRT$1)))
                      0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (SUB1 (I$0))
                             (PLUS (ISQRT$1)
                                   (ISQRT$1)
                                   (TIMES (ISQRT$1) (ISQRT$1)))))
                 (LESSP (PLUS (ISQRT$1)
                              (QUOTIENT (I$0) (ISQRT$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-ZPLUS


(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT2 NIL
 (IMPLIES
      (AND (NOT (ZGREATEREQP (ZQUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1)))
           (PATH-HYPS))
      (AND (NOT (ZEQP '2 '0))
           (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (ZPLUS (ISQRT$1)
                                                   (ZQUOTIENT (I$0) (ISQRT$1)))
                                            '2)))))

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

      (IMPLIES
       (AND (ZLESSP (ZQUOTIENT (I$0) (ISQRT$1))
                    (ISQRT$1))
            (NUMBERP (I$0))
            (LESSP (I$0)
                   (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
            (ZNUMBERP (I$0))
            (LESSP 0 (ISQRT$1))
            (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
            (NUMBERP (ISQRT$1))
            (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
       (AND
           (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
           (EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (ZPLUS (ISQRT$1)
                                                   (ZQUOTIENT (I$0) (ISQRT$1)))
                                            2)))).

This simplifies, using linear arithmetic, rewriting with
COMMUTATIVITY2-OF-PLUS, PLUS-ADD1, SUB1-ADD1, COMMUTATIVITY-OF-TIMES,
TIMES-ADD1, COMMUTATIVITY-OF-PLUS, MULTIPLY-THRU-BY-DIVISOR, and
QUOTIENT-SHRINKS, and opening up the functions ZQUOTIENT, ZLESSP, ZNUMBERP,
EQUAL, LESSP, PLUS, SQ, ZNORMALIZE, NOT, QUOTIENT, NEGATIVEP, ZPLUS,
EXPRESSIBLE-ZNUMBERP, and AND, to two new formulas:

Case 2. (IMPLIES
          (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                      (ISQRT$1))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (EQUAL (I$0) 0)
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (QUOTIENT (ISQRT$1) 2) 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES
          (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                      (ISQRT$1))
               (NUMBERP (I$0))
               (LESSP (I$0)
                      (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
               (NOT (EQUAL (ISQRT$1) 0))
               (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
               (NUMBERP (ISQRT$1))
               (LESSP (SUB1 (I$0))
                      (PLUS (ISQRT$1)
                            (ISQRT$1)
                            (TIMES (ISQRT$1) (ISQRT$1))))
               (EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
                      0))
          (NOT (EQUAL (QUOTIENT (PLUS (ISQRT$1)
                                      (QUOTIENT (I$0) (ISQRT$1)))
                                2)
                      0))),

  which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
  to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INPUT-COND-OF-ZQUOTIENT2


(ADD-AXIOM ASSIGNMENT1
           (REWRITE)
           (EQUAL (ISQRT$2)
                  (ZQUOTIENT (ZPLUS (ISQRT$1)
                                    (ZQUOTIENT (I$0) (ISQRT$1)))
                             '2)))

[ 0.0 0.0 0.0 ]

ASSIGNMENT1


(DISABLE SQ)

[ 0.0 0.0 0.0 ]

SQ-OFF1


(PROVE-LEMMA LP1 NIL
            (IMPLIES (AND (NOT (ZGREATEREQP (ZQUOTIENT (I$0) (ISQRT$1))
                                            (ISQRT$1)))
                          (PATH-HYPS))
                     (AND (AND (LESSP '0 (ISQRT$2))
                               (AND (NOT (LESSP (I$0) (TIMES '2 (ISQRT$2))))
                                    (AND (NUMBERP (ISQRT$2))
                                         (LESSP (I$0) (SQ (ADD1 (ISQRT$2)))))))
                          (LEX (CONS (ISQRT$2) 'NIL)
                               (CONS (ISQRT$1) 'NIL)))))

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

      (IMPLIES
       (AND (ZLESSP (ZQUOTIENT (I$0) (ISQRT$1))
                    (ISQRT$1))
            (NUMBERP (I$0))
            (LESSP (I$0)
                   (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
            (ZNUMBERP (I$0))
            (LESSP 0 (ISQRT$1))
            (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
            (NUMBERP (ISQRT$1))
            (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
       (AND
         (AND (LESSP 0
                     (ZQUOTIENT (ZPLUS (ISQRT$1)
                                       (ZQUOTIENT (I$0) (ISQRT$1)))
                                2))
              (NOT (LESSP (I$0)
                          (TIMES 2
                                 (ZQUOTIENT (ZPLUS (ISQRT$1)
                                                   (ZQUOTIENT (I$0) (ISQRT$1)))
                                            2))))
              (NUMBERP (ZQUOTIENT (ZPLUS (ISQRT$1)
                                         (ZQUOTIENT (I$0) (ISQRT$1)))
                                  2))
              (LESSP (I$0)
                     (SQ (ADD1 (ZQUOTIENT (ZPLUS (ISQRT$1)
                                                 (ZQUOTIENT (I$0) (ISQRT$1)))
                                          2)))))
         (LEX (LIST (ZQUOTIENT (ZPLUS (ISQRT$1)
                                      (ZQUOTIENT (I$0) (ISQRT$1)))
                               2))
              (LIST (ISQRT$1))))),

which simplifies, applying CDR-CONS and CAR-CONS, and expanding the functions
ZQUOTIENT, ZLESSP, ZNUMBERP, EQUAL, LESSP, ZPLUS, NEGATIVEP, NOT, AND, and LEX,
to the following four new conjectures:

Case 4. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
                 (NOT (EQUAL (QUOTIENT (PLUS (ISQRT$1)
                                             (QUOTIENT (I$0) (ISQRT$1)))
                                       2)
                             0))).

  However this again simplifies, using linear arithmetic, applying
  QUOTIENT-BY-2, and unfolding the definition of PLUS, to:

        (IMPLIES (AND (EQUAL (ISQRT$1) 1)
                      (LESSP (QUOTIENT (I$0) 1) 1)
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL 1 0))
                      (NOT (LESSP (I$0) (TIMES 2 1)))
                      (NUMBERP 1)
                      (LESSP (I$0) (SQ 2)))
                 (NOT (EQUAL (QUOTIENT (PLUS 1 (QUOTIENT (I$0) 1))
                                       2)
                             0))),

  which again simplifies, applying QUOTIENT-BY-1, PLUS-1, and SUB1-ADD1, and
  opening up EQUAL, TIMES, NUMBERP, SQ, LESSP, SUB1, and QUOTIENT, to:

        (IMPLIES (AND (EQUAL (ISQRT$1) 1)
                      (LESSP (I$0) 1)
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (LESSP (I$0) 2)))
                 (NOT (LESSP (I$0) 4))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
                 (NOT (LESSP (I$0)
                             (TIMES 2
                                    (QUOTIENT (PLUS (ISQRT$1)
                                                    (QUOTIENT (I$0) (ISQRT$1)))
                                              2))))),

  which again simplifies, using linear arithmetic and appealing to the lemma
  QUOTIENT-SHRINKS-FAST, to:

        T.

Case 2. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
                 (LESSP (I$0)
                        (SQ (ADD1 (QUOTIENT (PLUS (ISQRT$1)
                                                  (QUOTIENT (I$0) (ISQRT$1)))
                                            2))))),

  which again simplifies, using linear arithmetic and rewriting with MAIN, to:

        T.

Case 1. (IMPLIES (AND (LESSP (QUOTIENT (I$0) (ISQRT$1))
                             (ISQRT$1))
                      (NUMBERP (I$0))
                      (LESSP (I$0)
                             (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
                      (NOT (EQUAL (ISQRT$1) 0))
                      (NOT (LESSP (I$0) (TIMES 2 (ISQRT$1))))
                      (NUMBERP (ISQRT$1))
                      (LESSP (I$0) (SQ (ADD1 (ISQRT$1)))))
                 (LESSP (QUOTIENT (PLUS (ISQRT$1)
                                        (QUOTIENT (I$0) (ISQRT$1)))
                                  2)
                        (ISQRT$1))).

  This again simplifies, using linear arithmetic and appealing to the lemma
  QUOTIENT-SHRINKS-FAST, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

LP1


(UBT PATHS-FROM-LP)

PATHS-FROM-LP


(UBT FORTRAN)

FORTRAN