(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(DEFN A
      (M N A)
      (IF (ZEROP M)
          (PLUS N A)
          (IF (ZEROP N)
              0
              (IF (EQUAL N 1)
                  A
                  (A (SUB1 M) (A M (SUB1 N) A) A))))
      ((ORD-LESSP (CONS (ADD1 (COUNT M)) (COUNT N)))))

     Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-SUB1,
and COUNT-NUMBERP, and the definitions of ORDINALP, LESSP, ORD-LESSP, and
ZEROP establish that the measure (CONS (ADD1 (COUNT M)) (COUNT N)) decreases
according to the well-founded relation ORD-LESSP in each recursive call.
Hence, A is accepted under the principle of definition.  Note that:
      (OR (NUMBERP (A M N A))
          (EQUAL (A M N A) A))
is a theorem.




[ 0.0 0.0 0.0 ]

A


(DEFN P
      (M N)
      (IF (ZEROP M)
          (ADD1 N)
          (IF (ZEROP N)
              (P (SUB1 M) 1)
              (P (SUB1 M) (P M (SUB1 N)))))
      ((ORD-LESSP (CONS (ADD1 (COUNT M)) (COUNT N)))))

     Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-SUB1,
and COUNT-NUMBERP, and the definitions of ORDINALP, LESSP, ORD-LESSP, COUNT,
and ZEROP establish that the measure (CONS (ADD1 (COUNT M)) (COUNT N))
decreases according to the well-founded relation ORD-LESSP in each recursive
call.  Hence, P is accepted under the principle of definition.  From the
definition we can conclude that (NUMBERP (P M N)) is a theorem.




[ 0.0 0.0 0.0 ]

P


(PROVE-LEMMA A-OPEN
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP M)) (LESSP 1 N))
                      (EQUAL (A M N A)
                             (A (SUB1 M) (A M (SUB1 N) A) A))))

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

      (IMPLIES (AND (NOT (EQUAL M 0))
                    (NUMBERP M)
                    (LESSP 1 N))
               (EQUAL (A M N A)
                      (A (SUB1 M) (A M (SUB1 N) A) A))).

This simplifies, opening up the functions SUB1, NUMBERP, EQUAL, LESSP, and A,
to:

      (IMPLIES (AND (NOT (EQUAL M 0))
                    (NUMBERP M)
                    (NOT (EQUAL N 0))
                    (NUMBERP N)
                    (NOT (EQUAL (SUB1 N) 0))
                    (EQUAL N 1))
               (EQUAL A
                      (A (SUB1 M) (A M (SUB1 N) A) A))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

A-OPEN


(PROVE-LEMMA A-2-2->4
             (REWRITE)
             (EQUAL (A M 2 2) 4)
             ((INDUCT (PLUS M N))))

This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new goals:

Case 2. (IMPLIES (ZEROP M)
                 (EQUAL (A M 2 2) 4)).

  This simplifies, unfolding the definitions of ZEROP, A, EQUAL, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL M 0))
                      (NUMBERP M)
                      (EQUAL (A (SUB1 M) 2 2) 4))
                 (EQUAL (A M 2 2) 4)).

  This simplifies, rewriting with the lemma A-OPEN, and opening up the
  functions LESSP, SUB1, NUMBERP, EQUAL, and A, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

A-2-2->4


(PROVE-LEMMA PLUS-2
             (REWRITE)
             (EQUAL (PLUS 2 X) (ADD1 (ADD1 X)))
             ((INDUCT (PLUS X Y))))

This conjecture can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to two new formulas:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (PLUS 2 X) (ADD1 (ADD1 X)))),

  which simplifies, using linear arithmetic, to:

        T.

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

  which simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-2


(PROVE-LEMMA A->P NIL
             (AND (EQUAL (P 0 N) (ADD1 N))
                  (IMPLIES (LESSP 0 M)
                           (EQUAL (PLUS 3 (P M N))
                                  (A (SUB1 M)
                                     (ADD1 (ADD1 (ADD1 N)))
                                     2)))))

This conjecture can be simplified, using the abbreviations IMPLIES and AND, to
two new formulas:

Case 2. (EQUAL (P 0 N) (ADD1 N)),

  which simplifies, opening up the functions EQUAL and P, to:

        T.

Case 1. (IMPLIES (LESSP 0 M)
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))),

  which simplifies, applying PLUS-2, and unfolding the functions EQUAL, LESSP,
  SUB1, NUMBERP, and PLUS, to:

        (IMPLIES (AND (NOT (EQUAL M 0)) (NUMBERP M))
                 (EQUAL (ADD1 (ADD1 (ADD1 (P M N))))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))).

  Applying the lemma SUB1-ELIM, replace M by (ADD1 X) to eliminate (SUB1 M).
  We employ the type restriction lemma noted when SUB1 was introduced to
  restrict the new variable.  We would thus like to prove:

        (IMPLIES (AND (NUMBERP X)
                      (NOT (EQUAL (ADD1 X) 0)))
                 (EQUAL (ADD1 (ADD1 (ADD1 (P (ADD1 X) N))))
                        (A X (ADD1 (ADD1 (ADD1 N))) 2))),

  which further simplifies, obviously, to:

        (IMPLIES (NUMBERP X)
                 (EQUAL (ADD1 (ADD1 (ADD1 (P (ADD1 X) N))))
                        (A X (ADD1 (ADD1 (ADD1 N))) 2))),

  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:

(AND (EQUAL (P 0 N) (ADD1 N))
     (IMPLIES (LESSP 0 M)
              (EQUAL (PLUS 3 (P M N))
                     (A (SUB1 M)
                        (ADD1 (ADD1 (ADD1 N)))
                        2)))),

named *1.  Let us appeal to the induction principle.  There are two plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP M) (p M N))
           (IMPLIES (AND (NOT (ZEROP M))
                         (ZEROP N)
                         (p (SUB1 M) 1))
                    (p M N))
           (IMPLIES (AND (NOT (ZEROP M))
                         (NOT (ZEROP N))
                         (p M (SUB1 N))
                         (p (SUB1 M) (P M (SUB1 N))))
                    (p M N))).
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-SUB1, and
COUNT-NUMBERP, and the definitions of ORDINALP, LESSP, ORD-LESSP, COUNT, and
ZEROP inform us that the measure (CONS (ADD1 (COUNT M)) (COUNT N)) decreases
according to the well-founded relation ORD-LESSP in each induction step of the
scheme.  The above induction scheme generates 12 new conjectures:

Case 12.(IMPLIES (ZEROP M)
                 (EQUAL (P 0 N) (ADD1 N))),

  which simplifies, expanding the functions ZEROP, EQUAL, and P, to:

        T.

Case 11.(IMPLIES (AND (NOT (ZEROP M))
                      (ZEROP N)
                      (EQUAL (P 0 1) 2)
                      (NOT (LESSP 0 (SUB1 M))))
                 (EQUAL (P 0 N) (ADD1 N))),

  which simplifies, rewriting with SUB1-TYPE-RESTRICTION, and unfolding the
  functions ZEROP, P, EQUAL, and ADD1, to:

        T.

Case 10.(IMPLIES (AND (NOT (ZEROP M))
                      (ZEROP N)
                      (EQUAL (P 0 1) 2)
                      (EQUAL (PLUS 3 (P (SUB1 M) 1))
                             (A (SUB1 (SUB1 M)) 4 2)))
                 (EQUAL (P 0 N) (ADD1 N))).

  This simplifies, applying PLUS-2 and SUB1-TYPE-RESTRICTION, and opening up
  the definitions of ZEROP, P, EQUAL, SUB1, NUMBERP, PLUS, and ADD1, to:

        T.

Case 9. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (NOT (LESSP 0 M))
                      (NOT (LESSP 0 (SUB1 M))))
                 (EQUAL (P 0 N) (ADD1 N))),

  which simplifies, applying ADD1-SUB1, and expanding the definitions of ZEROP,
  EQUAL, and P, to:

        T.

Case 8. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (EQUAL (PLUS 3 (P M (SUB1 N)))
                             (A (SUB1 M)
                                (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                2))
                      (NOT (LESSP 0 (SUB1 M))))
                 (EQUAL (P 0 N) (ADD1 N))).

  This simplifies, rewriting with ADD1-SUB1 and PLUS-2, and expanding ZEROP,
  EQUAL, P, SUB1, NUMBERP, and PLUS, to:

        T.

Case 7. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (NOT (LESSP 0 M))
                      (EQUAL (PLUS 3 (P (SUB1 M) (P M (SUB1 N))))
                             (A (SUB1 (SUB1 M))
                                (ADD1 (ADD1 (ADD1 (P M (SUB1 N)))))
                                2)))
                 (EQUAL (P 0 N) (ADD1 N))),

  which simplifies, using linear arithmetic, appealing to the lemmas ADD1-SUB1,
  PLUS-2, SUB1-ADD1, and A-OPEN, and expanding the functions ZEROP, EQUAL, P,
  SUB1, NUMBERP, and PLUS, to:

        T.

Case 6. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (EQUAL (PLUS 3 (P M (SUB1 N)))
                             (A (SUB1 M)
                                (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                2))
                      (EQUAL (PLUS 3 (P (SUB1 M) (P M (SUB1 N))))
                             (A (SUB1 (SUB1 M))
                                (ADD1 (ADD1 (ADD1 (P M (SUB1 N)))))
                                2)))
                 (EQUAL (P 0 N) (ADD1 N))),

  which simplifies, applying ADD1-SUB1 and PLUS-2, and opening up the
  functions ZEROP, EQUAL, P, SUB1, NUMBERP, and PLUS, to:

        T.

Case 5. (IMPLIES (AND (ZEROP M) (LESSP 0 M))
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))).

  This simplifies, rewriting with the lemmas PLUS-2, SUB1-ADD1, ADD1-EQUAL,
  and SUB1-NNUMBERP, and unfolding ZEROP, EQUAL, P, SUB1, NUMBERP, PLUS, and A,
  to the following four new goals:

  Case 5.4.
          (IMPLIES (AND (EQUAL M 0)
                        (LESSP 0 M)
                        (NOT (NUMBERP N)))
                   (EQUAL (ADD1 N) (PLUS 0 2))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 5.3.
          (IMPLIES (AND (EQUAL M 0)
                        (LESSP 0 M)
                        (NUMBERP N))
                   (EQUAL (ADD1 N) (PLUS N 2))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 5.2.
          (IMPLIES (AND (NOT (NUMBERP M))
                        (LESSP 0 M)
                        (NOT (NUMBERP N)))
                   (EQUAL (ADD1 N) (PLUS 0 2))),

    which again simplifies, applying SUB1-TYPE-RESTRICTION, and unfolding PLUS
    and EQUAL, to:

          (IMPLIES (AND (NOT (NUMBERP M)) (LESSP 0 M))
                   (NUMBERP N)),

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

          T.

  Case 5.1.
          (IMPLIES (AND (NOT (NUMBERP M))
                        (LESSP 0 M)
                        (NUMBERP N))
                   (EQUAL (ADD1 N) (PLUS N 2))),

    which further simplifies, unfolding LESSP, to:

          T.

Case 4. (IMPLIES (AND (NOT (ZEROP M))
                      (ZEROP N)
                      (EQUAL (P 0 1) 2)
                      (NOT (LESSP 0 (SUB1 M)))
                      (LESSP 0 M))
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))),

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

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP M))
                        (NOT (ZEROP M))
                        (ZEROP N)
                        (EQUAL (P 0 1) 2)
                        (NOT (LESSP 0 (SUB1 M)))
                        (LESSP 0 M))
                   (EQUAL (PLUS 3 (P M N))
                          (A (SUB1 M)
                             (ADD1 (ADD1 (ADD1 N)))
                             2))),

    which again simplifies, unfolding ZEROP, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP M)
                        (NOT (ZEROP 1))
                        (ZEROP N)
                        (EQUAL (P 0 1) 2)
                        (NOT (LESSP 0 (SUB1 1)))
                        (LESSP 0 1))
                   (EQUAL (PLUS 3 (P 1 N))
                          (A (SUB1 1)
                             (ADD1 (ADD1 (ADD1 N)))
                             2))),

    which again simplifies, applying SUB1-TYPE-RESTRICTION, and opening up the
    functions ZEROP, P, EQUAL, SUB1, LESSP, PLUS, ADD1, A, and NUMBERP, to:

          T.

Case 3. (IMPLIES (AND (NOT (ZEROP M))
                      (ZEROP N)
                      (EQUAL (P 0 1) 2)
                      (EQUAL (PLUS 3 (P (SUB1 M) 1))
                             (A (SUB1 (SUB1 M)) 4 2))
                      (LESSP 0 M))
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))).

  This simplifies, rewriting with PLUS-2, A-2-2->4, and SUB1-TYPE-RESTRICTION,
  and opening up the functions ZEROP, P, EQUAL, SUB1, NUMBERP, PLUS, ADD1, and
  A, to two new formulas:

  Case 3.2.
          (IMPLIES (AND (NOT (EQUAL M 0))
                        (NUMBERP M)
                        (EQUAL N 0)
                        (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) 1))))
                               (A (SUB1 (SUB1 M)) 4 2))
                        (LESSP 0 M)
                        (EQUAL (SUB1 M) 0))
                   (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) 1))))
                          5)),

    which again simplifies, unfolding P, ADD1, SUB1, A, and EQUAL, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (EQUAL M 0))
                        (NUMBERP M)
                        (NOT (NUMBERP N))
                        (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) 1))))
                               (A (SUB1 (SUB1 M)) 4 2))
                        (LESSP 0 M)
                        (EQUAL (SUB1 M) 0))
                   (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) 1))))
                          5)),

    which again simplifies, opening up the definitions of P, ADD1, SUB1, A,
    and EQUAL, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (EQUAL (PLUS 3 (P M (SUB1 N)))
                             (A (SUB1 M)
                                (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                2))
                      (NOT (LESSP 0 (SUB1 M)))
                      (LESSP 0 M))
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))),

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

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP M))
                        (NOT (ZEROP M))
                        (NOT (ZEROP N))
                        (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                        (EQUAL (P 0 (P M (SUB1 N)))
                               (ADD1 (P M (SUB1 N))))
                        (EQUAL (PLUS 3 (P M (SUB1 N)))
                               (A (SUB1 M)
                                  (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                  2))
                        (NOT (LESSP 0 (SUB1 M)))
                        (LESSP 0 M))
                   (EQUAL (PLUS 3 (P M N))
                          (A (SUB1 M)
                             (ADD1 (ADD1 (ADD1 N)))
                             2))),

    which again simplifies, opening up ZEROP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP M)
                        (NOT (ZEROP 1))
                        (NOT (ZEROP N))
                        (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                        (EQUAL (P 0 (P 1 (SUB1 N)))
                               (ADD1 (P 1 (SUB1 N))))
                        (EQUAL (PLUS 3 (P 1 (SUB1 N)))
                               (A (SUB1 1)
                                  (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                  2))
                        (NOT (LESSP 0 (SUB1 1)))
                        (LESSP 0 1))
                   (EQUAL (PLUS 3 (P 1 N))
                          (A (SUB1 1)
                             (ADD1 (ADD1 (ADD1 N)))
                             2))),

    which again simplifies, rewriting with the lemmas ADD1-SUB1, PLUS-2,
    SUB1-ADD1, and ADD1-EQUAL, and expanding ZEROP, EQUAL, P, SUB1, NUMBERP,
    PLUS, A, and LESSP, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP M))
                      (NOT (ZEROP N))
                      (EQUAL (P 0 (SUB1 N)) (ADD1 (SUB1 N)))
                      (EQUAL (P 0 (P M (SUB1 N)))
                             (ADD1 (P M (SUB1 N))))
                      (EQUAL (PLUS 3 (P M (SUB1 N)))
                             (A (SUB1 M)
                                (ADD1 (ADD1 (ADD1 (SUB1 N))))
                                2))
                      (EQUAL (PLUS 3 (P (SUB1 M) (P M (SUB1 N))))
                             (A (SUB1 (SUB1 M))
                                (ADD1 (ADD1 (ADD1 (P M (SUB1 N)))))
                                2))
                      (LESSP 0 M))
                 (EQUAL (PLUS 3 (P M N))
                        (A (SUB1 M)
                           (ADD1 (ADD1 (ADD1 N)))
                           2))),

  which simplifies, appealing to the lemmas ADD1-SUB1, PLUS-2, ADD1-EQUAL, and
  SUB1-ADD1, and expanding the functions ZEROP, EQUAL, P, SUB1, NUMBERP, PLUS,
  and A, to the goal:

        (IMPLIES (AND (NOT (EQUAL M 0))
                      (NUMBERP M)
                      (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (EQUAL (ADD1 (ADD1 (ADD1 (P M (SUB1 N)))))
                             (A (SUB1 M) (ADD1 (ADD1 N)) 2))
                      (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) (P M (SUB1 N))))))
                             (A (SUB1 (SUB1 M))
                                (ADD1 (ADD1 (ADD1 (P M (SUB1 N)))))
                                2))
                      (LESSP 0 M)
                      (EQUAL (SUB1 M) 0))
                 (EQUAL (ADD1 (ADD1 (ADD1 (P (SUB1 M) (P M (SUB1 N))))))
                        (ADD1 (ADD1 (ADD1 (ADD1 (PLUS (SUB1 N) 2))))))).

  But this again simplifies, rewriting with SUB1-ADD1 and ADD1-EQUAL, and
  opening up PLUS, EQUAL, A, P, and SUB1, to:

        T.


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


[ 0.0 0.1 0.0 ]

A->P