(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(DEFN FACT
      (N)
      (IF (ZEROP N)
          1
          (TIMES N (FACT (SUB1 N)))))

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




[ 0.0 0.0 0.0 ]

FACT


(DEFN SUM<K*FACT_K>
      (N)
      (IF (ZEROP N)
          0
          (PLUS (SUM<K*FACT_K> (SUB1 N))
                (TIMES N (FACT N)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, SUM<K*FACT_K> is
accepted under the definitional principle.  From the definition we can
conclude that (NUMBERP (SUM<K*FACT_K> N)) is a theorem.




[ 0.0 0.0 0.0 ]

SUM<K*FACT_K>


(PROVE-LEMMA SUM<K*FACT_K>+1=FACT<N+1> NIL
             (EQUAL (ADD1 (SUM<K*FACT_K> N))
                    (FACT (ADD1 N))))

This conjecture simplifies, appealing to the lemma SUB1-ADD1, and expanding
the functions TIMES and FACT, to the following two new goals:

Case 2. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (ADD1 (SUM<K*FACT_K> N))
                        (PLUS (FACT 0) (TIMES 0 (FACT 0))))).

  This again simplifies, unfolding the definitions of SUM<K*FACT_K>, ADD1,
  FACT, TIMES, PLUS, and EQUAL, to:

        T.

Case 1. (IMPLIES (NUMBERP N)
                 (EQUAL (ADD1 (SUM<K*FACT_K> N))
                        (PLUS (FACT N) (TIMES N (FACT N))))),

  which we will name *1.


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

Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N))
                 (EQUAL (ADD1 (SUM<K*FACT_K> N))
                        (PLUS (FACT N) (TIMES N (FACT N))))).

  This simplifies, unfolding the functions ZEROP, NUMBERP, SUM<K*FACT_K>, ADD1,
  FACT, TIMES, PLUS, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (ADD1 (SUM<K*FACT_K> (SUB1 N)))
                             (PLUS (FACT (SUB1 N))
                                   (TIMES (SUB1 N) (FACT (SUB1 N)))))
                      (NUMBERP N))
                 (EQUAL (ADD1 (SUM<K*FACT_K> N))
                        (PLUS (FACT N) (TIMES N (FACT N))))).

  This simplifies, rewriting with SUB1-ADD1, and expanding ZEROP,
  SUM<K*FACT_K>, FACT, TIMES, and PLUS, to:

        T.


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


[ 0.0 0.0 0.0 ]

SUM<K*FACT_K>+1=FACT<N+1>


(PROVE-LEMMA SUM<K*FACT_K>=FACT<N+1>-1 NIL
             (EQUAL (SUM<K*FACT_K> N)
                    (SUB1 (FACT (ADD1 N))))
             ((USE (SUM<K*FACT_K>+1=FACT<N+1> (N N)))))

This formula simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (FACT (ADD1 N)) 0)
                    (EQUAL (ADD1 (SUM<K*FACT_K> N))
                           (FACT (ADD1 N))))
               (EQUAL (SUM<K*FACT_K> N)
                      (SUB1 (FACT (ADD1 N))))).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM<K*FACT_K>=FACT<N+1>-1


(UBT SUM<K*FACT_K>+1=FACT<N+1>)

SUM<K*FACT_K>+1=FACT<N+1>


(PROVE-LEMMA SUM<K*FACT_K>=FACT<N+1>-1 NIL
             (EQUAL (SUM<K*FACT_K> N)
                    (SUB1 (FACT (ADD1 N)))))

This conjecture simplifies, appealing to the lemma SUB1-ADD1, and expanding
the functions TIMES and FACT, to the following two new goals:

Case 2. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (SUM<K*FACT_K> N)
                        (SUB1 (PLUS (FACT 0) (TIMES 0 (FACT 0)))))).

  This again simplifies, unfolding the definitions of SUM<K*FACT_K>, FACT,
  TIMES, PLUS, SUB1, and EQUAL, to:

        T.

Case 1. (IMPLIES (NUMBERP N)
                 (EQUAL (SUM<K*FACT_K> N)
                        (SUB1 (PLUS (FACT N) (TIMES N (FACT N)))))),

  which we will name *1.


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

Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N))
                 (EQUAL (SUM<K*FACT_K> N)
                        (SUB1 (PLUS (FACT N) (TIMES N (FACT N)))))).

  This simplifies, unfolding the functions ZEROP, NUMBERP, SUM<K*FACT_K>, FACT,
  TIMES, PLUS, SUB1, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (SUM<K*FACT_K> (SUB1 N))
                             (SUB1 (PLUS (FACT (SUB1 N))
                                         (TIMES (SUB1 N) (FACT (SUB1 N))))))
                      (NUMBERP N))
                 (EQUAL (SUM<K*FACT_K> N)
                        (SUB1 (PLUS (FACT N) (TIMES N (FACT N)))))).

  This simplifies, unfolding the definitions of ZEROP, SUM<K*FACT_K>, FACT,
  TIMES, and PLUS, to the following two new goals:

  Case 1.2.
          (IMPLIES
           (AND (NOT (EQUAL N 0))
                (EQUAL (SUM<K*FACT_K> (SUB1 N))
                       (SUB1 (PLUS (FACT (SUB1 N))
                                   (TIMES (SUB1 N) (FACT (SUB1 N))))))
                (NUMBERP N)
                (NOT (EQUAL (PLUS (FACT (SUB1 N))
                                  (TIMES (SUB1 N) (FACT (SUB1 N))))
                            0)))
           (EQUAL
            (PLUS (SUM<K*FACT_K> (SUB1 N))
                  (TIMES N
                         (PLUS (FACT (SUB1 N))
                               (TIMES (SUB1 N) (FACT (SUB1 N))))))
            (SUB1
             (ADD1
               (PLUS (SUM<K*FACT_K> (SUB1 N))
                     (ADD1 (PLUS (SUM<K*FACT_K> (SUB1 N))
                                 (TIMES (SUB1 N)
                                        (PLUS (FACT (SUB1 N))
                                              (TIMES (SUB1 N)
                                                     (FACT (SUB1 N)))))))))))).

    However this again simplifies, rewriting with SUB1-ADD1, and opening up
    the definitions of PLUS and TIMES, to:

          T.

  Case 1.1.
          (IMPLIES
                  (AND (NOT (EQUAL N 0))
                       (EQUAL (SUM<K*FACT_K> (SUB1 N))
                              (SUB1 (PLUS (FACT (SUB1 N))
                                          (TIMES (SUB1 N) (FACT (SUB1 N))))))
                       (NUMBERP N)
                       (EQUAL (PLUS (FACT (SUB1 N))
                                    (TIMES (SUB1 N) (FACT (SUB1 N))))
                              0))
                  (EQUAL (PLUS (SUM<K*FACT_K> (SUB1 N))
                               (TIMES N
                                      (PLUS (FACT (SUB1 N))
                                            (TIMES (SUB1 N) (FACT (SUB1 N))))))
                         (SUB1 (TIMES N 0)))).

    However this again simplifies, expanding the functions SUB1, EQUAL, and
    PLUS, to:

          (IMPLIES (AND (NOT (EQUAL N 0))
                        (EQUAL (SUM<K*FACT_K> (SUB1 N)) 0)
                        (NUMBERP N)
                        (EQUAL (PLUS (FACT (SUB1 N))
                                     (TIMES (SUB1 N) (FACT (SUB1 N))))
                               0))
                   (EQUAL (TIMES N 0)
                          (SUB1 (TIMES N 0)))).

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

          (IMPLIES (AND (NUMBERP X)
                        (NOT (EQUAL (ADD1 X) 0))
                        (EQUAL (SUM<K*FACT_K> X) 0)
                        (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                               0))
                   (EQUAL (TIMES (ADD1 X) 0)
                          (SUB1 (TIMES (ADD1 X) 0)))).

    This further simplifies, applying SUB1-ADD1, and expanding the definitions
    of PLUS, EQUAL, and TIMES, to the new conjecture:

          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (SUM<K*FACT_K> X) 0)
                        (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                               0))
                   (EQUAL (TIMES X 0)
                          (SUB1 (TIMES X 0)))),

    which we generalize by replacing (TIMES X 0) by Y.  We restrict the new
    variable by recalling the type restriction lemma noted when TIMES was
    introduced.  We would thus like to prove the new formula:

          (IMPLIES (AND (NUMBERP Y)
                        (NUMBERP X)
                        (EQUAL (SUM<K*FACT_K> X) 0)
                        (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                               0))
                   (EQUAL Y (SUB1 Y))).

    Applying the lemma SUB1-ELIM, replace Y by (ADD1 Z) to eliminate (SUB1 Y).
    We use the type restriction lemma noted when SUB1 was introduced to
    restrict the new variable.  This produces the following two new
    conjectures:

    Case 1.1.2.
            (IMPLIES (AND (EQUAL Y 0)
                          (NUMBERP Y)
                          (NUMBERP X)
                          (EQUAL (SUM<K*FACT_K> X) 0)
                          (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                                 0))
                     (EQUAL Y (SUB1 Y))).

      But this finally simplifies, opening up the functions NUMBERP, SUB1, and
      EQUAL, to:

            T.

    Case 1.1.1.
            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL (ADD1 Z) 0))
                          (NUMBERP X)
                          (EQUAL (SUM<K*FACT_K> X) 0)
                          (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                                 0))
                     (EQUAL (ADD1 Z) Z)),

      which further simplifies, obviously, to:

            (IMPLIES (AND (NUMBERP Z)
                          (NUMBERP X)
                          (EQUAL (SUM<K*FACT_K> X) 0))
                     (NOT (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                                 0))),

      which has an irrelevant term in it.  By eliminating the term we get:

            (IMPLIES (AND (NUMBERP X)
                          (EQUAL (SUM<K*FACT_K> X) 0))
                     (NOT (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                                 0))),

      which we will finally name *1.1.


     Perhaps we can prove it by induction.  Four inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (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
establish that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme generates the following three new goals:

Case 3. (IMPLIES (AND (ZEROP X)
                      (NUMBERP X)
                      (EQUAL (SUM<K*FACT_K> X) 0))
                 (NOT (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                             0))).

  This simplifies, expanding ZEROP, NUMBERP, SUM<K*FACT_K>, EQUAL, FACT, TIMES,
  and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (EQUAL (SUM<K*FACT_K> (SUB1 X)) 0))
                      (NUMBERP X)
                      (EQUAL (SUM<K*FACT_K> X) 0))
                 (NOT (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                             0))).

  This simplifies, opening up the functions ZEROP, SUM<K*FACT_K>, and FACT, to
  the new conjecture:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NOT (EQUAL (SUM<K*FACT_K> (SUB1 X)) 0))
                      (NUMBERP X)
                      (EQUAL (PLUS (SUM<K*FACT_K> (SUB1 X))
                                   (TIMES X X (FACT (SUB1 X))))
                             0))
                 (NOT (EQUAL (PLUS (TIMES X (FACT (SUB1 X)))
                                   (TIMES X X (FACT (SUB1 X))))
                             0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (EQUAL (PLUS (FACT (SUB1 X))
                                        (TIMES (SUB1 X) (FACT (SUB1 X))))
                                  0))
                      (NUMBERP X)
                      (EQUAL (SUM<K*FACT_K> X) 0))
                 (NOT (EQUAL (PLUS (FACT X) (TIMES X (FACT X)))
                             0))),

  which simplifies, expanding the definitions of ZEROP, SUM<K*FACT_K>, FACT,
  and TIMES, to:

        (IMPLIES
             (AND (NOT (EQUAL X 0))
                  (NOT (EQUAL (PLUS (FACT (SUB1 X))
                                    (TIMES (SUB1 X) (FACT (SUB1 X))))
                              0))
                  (NUMBERP X)
                  (EQUAL (PLUS (SUM<K*FACT_K> (SUB1 X))
                               (PLUS (FACT (SUB1 X))
                                     (TIMES (SUB1 X) (FACT (SUB1 X))))
                               (TIMES (SUB1 X)
                                      (PLUS (FACT (SUB1 X))
                                            (TIMES (SUB1 X) (FACT (SUB1 X))))))
                         0))
             (NOT (EQUAL (PLUS (PLUS (FACT (SUB1 X))
                                     (TIMES (SUB1 X) (FACT (SUB1 X))))
                               (PLUS (FACT (SUB1 X))
                                     (TIMES (SUB1 X) (FACT (SUB1 X))))
                               (TIMES (SUB1 X)
                                      (PLUS (FACT (SUB1 X))
                                            (TIMES (SUB1 X) (FACT (SUB1 X))))))
                         0))).

  This again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 0.1 0.0 ]

SUM<K*FACT_K>=FACT<N+1>-1