(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(DEFN REP (I J) (CONS (ADD1 I) J))

     Note that (LISTP (REP I J)) is a theorem.




[ 0.0 0.0 0.0 ]

REP


(DEFN LEX2
      (I1 J1 I2 J2)
      (OR (LESSP I1 I2)
          (AND (EQUAL I1 I2) (LESSP J1 J2))))

     From the definition we can conclude that:
      (OR (FALSEP (LEX2 I1 J1 I2 J2))
          (TRUEP (LEX2 I1 J1 I2 J2)))
is a theorem.




[ 0.0 0.0 0.0 ]

LEX2


(PROVE-LEMMA REP-RESPECTS-LEX
             (REWRITE)
             (IMPLIES (AND (NUMBERP I1)
                           (NUMBERP I2)
                           (NUMBERP J1)
                           (NUMBERP J2))
                      (EQUAL (LEX2 I1 J1 I2 J2)
                             (ORD-LESSP (REP I1 J1) (REP I2 J2)))))

WARNING:  Note that the rewrite rule REP-RESPECTS-LEX will be stored so as to
apply only to terms with the nonrecursive function symbol LEX2.


This formula can be simplified, using the abbreviations AND, IMPLIES, and REP,
to the new conjecture:

      (IMPLIES (AND (NUMBERP I1)
                    (NUMBERP I2)
                    (NUMBERP J1)
                    (NUMBERP J2))
               (EQUAL (LEX2 I1 J1 I2 J2)
                      (ORD-LESSP (CONS (ADD1 I1) J1)
                                 (CONS (ADD1 I2) J2)))),

which simplifies, rewriting with CDR-CONS, ADD1-EQUAL, CAR-CONS, and SUB1-ADD1,
and opening up the functions LEX2, ORD-LESSP, and LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REP-RESPECTS-LEX


(DEFN ACK
      (X Y)
      (IF (ZEROP X)
          1
          (IF (ZEROP Y)
              (IF (EQUAL X 1) 2 (PLUS X 2))
              (ACK (ACK (SUB1 X) Y) (SUB1 Y))))
      ((ORD-LESSP (REP (FIX Y) (FIX X)))))

     Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, and
ADD1-SUB1, and the definitions of ORDINALP, REP, FIX, LESSP, ORD-LESSP, and
ZEROP can be used to prove that the measure (REP (FIX Y) (FIX X)) decreases
according to the well-founded relation ORD-LESSP in each recursive call.
Hence, ACK is accepted under the principle of definition.  From the definition
we can conclude that (NUMBERP (ACK X Y)) is a theorem.




[ 0.0 0.0 0.0 ]

ACK


(PROVE-LEMMA ACK-IS-POSITIVE
             (REWRITE)
             (EQUAL (ZEROP (ACK X Y)) F))

WARNING:  Note that the rewrite rule ACK-IS-POSITIVE will be stored so as to
apply only to terms with the nonrecursive function symbol ZEROP.


This simplifies, unfolding ZEROP, to:

      (NOT (EQUAL (ACK X Y) 0)).

Name the above subgoal *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X))
                         (ZEROP Y)
                         (EQUAL X 1))
                    (p X Y))
           (IMPLIES (AND (NOT (ZEROP X))
                         (ZEROP Y)
                         (NOT (EQUAL X 1)))
                    (p X Y))
           (IMPLIES (AND (NOT (ZEROP X))
                         (NOT (ZEROP Y))
                         (p (ACK (SUB1 X) Y) (SUB1 Y))
                         (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, and ADD1-SUB1,
and the definitions of ORDINALP, REP, FIX, LESSP, ORD-LESSP, and ZEROP can be
used to show that the measure (REP (FIX Y) (FIX X)) decreases according to the
well-founded relation ORD-LESSP in each induction step of the scheme.  The
above induction scheme generates four new goals:

Case 4. (IMPLIES (ZEROP X)
                 (NOT (EQUAL (ACK X Y) 0))),

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

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP X))
                      (ZEROP Y)
                      (EQUAL X 1))
                 (NOT (EQUAL (ACK X Y) 0))),

  which simplifies, expanding ZEROP, ACK, EQUAL, and NUMBERP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (ZEROP Y)
                      (NOT (EQUAL X 1)))
                 (NOT (EQUAL (ACK X Y) 0))),

  which simplifies, expanding ZEROP, EQUAL, and ACK, to two new conjectures:

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL Y 0)
                        (NOT (EQUAL X 1)))
                   (NOT (EQUAL (PLUS X 2) 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (NUMBERP Y))
                        (NOT (EQUAL X 1)))
                   (NOT (EQUAL (PLUS X 2) 0))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (ZEROP Y))
                      (NOT (EQUAL (ACK (ACK (SUB1 X) Y) (SUB1 Y))
                                  0))
                      (NOT (EQUAL (ACK (SUB1 X) Y) 0)))
                 (NOT (EQUAL (ACK X Y) 0))),

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

        T.


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


[ 0.0 0.0 0.0 ]

ACK-IS-POSITIVE


(PROVE-LEMMA ACK-OF-1
             (REWRITE)
             (IMPLIES (NOT (ZEROP X))
                      (EQUAL (ACK X 1) (TIMES X 2))))

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

      (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X))
               (EQUAL (ACK X 1) (TIMES X 2))).

Call the above conjecture *1.


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

Case 3. (IMPLIES (AND (ZEROP X)
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (EQUAL (ACK X 1) (TIMES X 2))),

  which simplifies, opening up ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (SUB1 X) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (EQUAL (ACK X 1) (TIMES X 2))),

  which simplifies, expanding the definitions of ZEROP, SUB1, ACK, NUMBERP,
  EQUAL, and TIMES, to:

        (IMPLIES (AND (EQUAL (SUB1 X) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (EQUAL 2
                        (PLUS 2 (TIMES (SUB1 X) 2)))).

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

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (ACK (SUB1 X) 1)
                             (TIMES (SUB1 X) 2))
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (EQUAL (ACK X 1) (TIMES X 2))),

  which simplifies, opening up ZEROP, SUB1, NUMBERP, EQUAL, ACK, TIMES, and
  PLUS, to three new formulas:

  Case 1.3.
          (IMPLIES (AND (EQUAL (ACK (SUB1 X) 1)
                               (TIMES (SUB1 X) 2))
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL (ACK (SUB1 X) 1) 0))
                        (EQUAL (ACK (SUB1 X) 1) 1))
                   (EQUAL 2
                          (ADD1 (ADD1 (ACK (SUB1 X) 1))))),

    which again simplifies, expanding the function EQUAL, to:

          (IMPLIES (AND (EQUAL 1 (TIMES (SUB1 X) 2))
                        (NOT (EQUAL X 0))
                        (NUMBERP X))
                   (NOT (EQUAL (ACK (SUB1 X) 1) 1))).

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

          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL 1 (TIMES Z 2))
                        (NOT (EQUAL (ADD1 Z) 0)))
                   (NOT (EQUAL (ACK Z 1) 1))).

    This further simplifies, clearly, to:

          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL 1 (TIMES Z 2)))
                   (NOT (EQUAL (ACK Z 1) 1))),

    which we will name *1.1.

  Case 1.2.
          (IMPLIES (AND (EQUAL (ACK (SUB1 X) 1)
                               (TIMES (SUB1 X) 2))
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL (ACK (SUB1 X) 1) 0))
                        (NOT (EQUAL (ACK (SUB1 X) 1) 1)))
                   (EQUAL (PLUS (ACK (SUB1 X) 1) 2)
                          (ADD1 (ADD1 (ACK (SUB1 X) 1))))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (EQUAL (ACK (SUB1 X) 1)
                               (TIMES (SUB1 X) 2))
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (ACK (SUB1 X) 1) 0))
                   (EQUAL 1
                          (ADD1 (ADD1 (ACK (SUB1 X) 1))))),

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

          (IMPLIES (AND (EQUAL 0 (TIMES (SUB1 X) 2))
                        (NOT (EQUAL X 0))
                        (NUMBERP X))
                   (NOT (EQUAL (ACK (SUB1 X) 1) 0))).

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

          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL 0 (TIMES Z 2))
                        (NOT (EQUAL (ADD1 Z) 0)))
                   (NOT (EQUAL (ACK Z 1) 0))).

    This further simplifies, obviously, to:

          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL 0 (TIMES Z 2)))
                   (NOT (EQUAL (ACK Z 1) 0))),

    which we will name *1.2.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Z) (p Z))
           (IMPLIES (AND (NOT (ZEROP Z)) (p (SUB1 Z)))
                    (p Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT Z) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme leads
to the following three new conjectures:

Case 3. (IMPLIES (AND (ZEROP Z)
                      (NUMBERP Z)
                      (EQUAL 0 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 0))).

  This simplifies, unfolding ZEROP, NUMBERP, TIMES, EQUAL, and ACK, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL 0 (TIMES (SUB1 Z) 2)))
                      (NUMBERP Z)
                      (EQUAL 0 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 0))).

  This simplifies, unfolding the definitions of ZEROP, TIMES, SUB1, NUMBERP,
  EQUAL, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL (ACK (SUB1 Z) 1) 0))
                      (NUMBERP Z)
                      (EQUAL 0 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 0))).

  This simplifies, unfolding the functions ZEROP, TIMES, SUB1, NUMBERP, EQUAL,
  and ACK, to the new formula:

        (IMPLIES (AND (NOT (EQUAL Z 0))
                      (NOT (EQUAL (ACK (SUB1 Z) 1) 0))
                      (NUMBERP Z)
                      (EQUAL 0 (PLUS 2 (TIMES (SUB1 Z) 2)))
                      (NOT (EQUAL (ACK (SUB1 Z) 1) 1)))
                 (NOT (EQUAL (PLUS (ACK (SUB1 Z) 1) 2) 0))),

  which again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.2.


     So next consider:

      (IMPLIES (AND (NUMBERP Z)
                    (EQUAL 1 (TIMES Z 2)))
               (NOT (EQUAL (ACK Z 1) 1))),

which is formula *1.1 above.  We will try to prove it by induction.  There is
only one suggested induction.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP Z) (p Z))
           (IMPLIES (AND (NOT (ZEROP Z)) (p (SUB1 Z)))
                    (p Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT Z) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates the following three new goals:

Case 3. (IMPLIES (AND (ZEROP Z)
                      (NUMBERP Z)
                      (EQUAL 1 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 1))).

  This simplifies, expanding the functions ZEROP, NUMBERP, TIMES, and EQUAL,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL 1 (TIMES (SUB1 Z) 2)))
                      (NUMBERP Z)
                      (EQUAL 1 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 1))).

  This simplifies, applying ADD1-EQUAL, and expanding the functions ZEROP,
  TIMES, SUB1, NUMBERP, EQUAL, and PLUS, to the goal:

        (IMPLIES (AND (NOT (EQUAL Z 0))
                      (NOT (EQUAL 1 (TIMES (SUB1 Z) 2)))
                      (NUMBERP Z)
                      (EQUAL 0 (PLUS 1 (TIMES (SUB1 Z) 2))))
                 (NOT (EQUAL (ACK Z 1) 1))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL (ACK (SUB1 Z) 1) 1))
                      (NUMBERP Z)
                      (EQUAL 1 (TIMES Z 2)))
                 (NOT (EQUAL (ACK Z 1) 1))),

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

        (IMPLIES (AND (NOT (EQUAL Z 0))
                      (NOT (EQUAL (ACK (SUB1 Z) 1) 1))
                      (NUMBERP Z)
                      (EQUAL 1 (PLUS 2 (TIMES (SUB1 Z) 2))))
                 (NOT (EQUAL (ACK Z 1) 1))).

  But this again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.0 0.0 ]

ACK-OF-1


(DEFN EXPT2
      (X)
      (IF (ZEROP X)
          1
          (TIMES (EXPT2 (SUB1 X)) 2)))

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




[ 0.0 0.0 0.0 ]

EXPT2


(PROVE-LEMMA ACK-OF-2-AUX1
             (REWRITE)
             (IMPLIES (NOT (ZEROP X))
                      (EQUAL (ACK X 2)
                             (ACK (ACK (SUB1 X) 2) 1))))

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

      (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X))
               (EQUAL (ACK X 2)
                      (ACK (ACK (SUB1 X) 2) 1))),

which simplifies, unfolding SUB1, NUMBERP, EQUAL, and ACK, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ACK-OF-2-AUX1


(PROVE-LEMMA ACK-OF-2-AUX2
             (REWRITE)
             (IMPLIES (NOT (ZEROP X))
                      (EQUAL (ACK X 2)
                             (TIMES (ACK (SUB1 X) 2) 2)))
             ((DO-NOT-INDUCT T)
              (USE (ACK-OF-2-AUX1 (X X))
                   (ACK-OF-1 (X (ACK (SUB1 X) 2))))
              (DISABLE ACK-OF-2-AUX1 ACK-OF-1)))

WARNING:  the previously added lemma, ACK-OF-2-AUX1, could be applied whenever
the newly proposed ACK-OF-2-AUX2 could!


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

      (IMPLIES (AND (IMPLIES (NOT (ZEROP X))
                             (EQUAL (ACK X 2)
                                    (ACK (ACK (SUB1 X) 2) 1)))
                    (IMPLIES (NOT F)
                             (EQUAL (ACK (ACK (SUB1 X) 2) 1)
                                    (TIMES (ACK (SUB1 X) 2) 2)))
                    (NOT (EQUAL X 0))
                    (NUMBERP X))
               (EQUAL (ACK X 2)
                      (TIMES (ACK (SUB1 X) 2) 2))).

This simplifies, opening up ZEROP, NOT, SUB1, NUMBERP, EQUAL, ACK, and IMPLIES,
to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ACK-OF-2-AUX2


(PROVE-LEMMA ACK-OF-2
             (REWRITE)
             (EQUAL (ACK X 2) (EXPT2 X)))

WARNING:  the newly proposed lemma, ACK-OF-2, could be applied whenever the
previously added lemma ACK-OF-2-AUX2 could.




WARNING:  the newly proposed lemma, ACK-OF-2, could be applied whenever the
previously added lemma ACK-OF-2-AUX1 could.





     Call the conjecture *1.


     We will try to prove it by induction.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X)))
                    (p X))).
Linear arithmetic, the lemma COUNT-NUMBERP, 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 generates the following two new formulas:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (ACK X 2) (EXPT2 X))).

  This simplifies, expanding the definitions of ZEROP, ACK, EXPT2, and EQUAL,
  to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (ACK (SUB1 X) 2)
                             (EXPT2 (SUB1 X))))
                 (EQUAL (ACK X 2) (EXPT2 X))).

  This simplifies, appealing to the lemma ACK-OF-2-AUX2, and opening up ZEROP
  and EXPT2, to:

        T.


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


[ 0.0 0.0 0.0 ]

ACK-OF-2