(BOOT-STRAP NQTHM)

[ 0.1 0.1 0.0 ]

GROUND-ZERO


(CONSTRAIN P-Q-R-INTRO
           (REWRITE)
           T
           ((P (LAMBDA (X) X))
            (Q (LAMBDA (X) X))
            (R (LAMBDA (X) X))))

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



We will verify the consistency and the conservative nature of this constraint
by attempting to prove T.

This conjecture can be propositionally simplified to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

P-Q-R-INTRO


(CONSTRAIN INTRO-H
           (REWRITE)
           (EQUAL (H X (H Y Z)) (H Y (H X Z)))
           ((H PLUS)))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (EQUAL (PLUS X Y Z) (PLUS Y X Z)).

This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INTRO-H


(DEFN PR-H
      (L Z)
      (IF (NLISTP L)
          Z
          (H (CAR L) (PR-H (CDR L) Z))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, PR-H is
accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

PR-H


(DEFN AC-H
      (L Z)
      (IF (NLISTP L)
          Z
          (AC-H (CDR L) (H (CAR L) Z))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, AC-H is
accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

AC-H


(PROVE-LEMMA PR-IS-AC
             (REWRITE)
             (EQUAL (AC-H L Z) (PR-H L Z))
             ((INDUCT (AC-H L Z))))

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

Case 2. (IMPLIES (NOT (LISTP L))
                 (EQUAL (AC-H L Z) (PR-H L Z))).

  This simplifies, unfolding the definitions of AC-H and PR-H, to:

        T.

Case 1. (IMPLIES (AND (LISTP L)
                      (EQUAL (AC-H (CDR L) (H (CAR L) Z))
                             (PR-H (CDR L) (H (CAR L) Z))))
                 (EQUAL (AC-H L Z) (PR-H L Z))).

  This simplifies, opening up AC-H and PR-H, to the new formula:

        (IMPLIES (AND (LISTP L)
                      (EQUAL (AC-H (CDR L) (H (CAR L) Z))
                             (PR-H (CDR L) (H (CAR L) Z))))
                 (EQUAL (AC-H (CDR L) (H (CAR L) Z))
                        (H (CAR L) (PR-H (CDR L) Z)))).

  Applying the lemma CAR-CDR-ELIM, replace L by (CONS V X) to eliminate
  (CDR L) and (CAR L).  This produces:

        (IMPLIES (EQUAL (AC-H X (H V Z))
                        (PR-H X (H V Z)))
                 (EQUAL (AC-H X (H V Z))
                        (H V (PR-H X Z)))).

  We use the above equality hypothesis by substituting (PR-H X (H V Z)) for
  (AC-H X (H V Z)) and throwing away the equality.  The result is:

        (EQUAL (PR-H X (H V Z))
               (H V (PR-H X Z))).

  Name the above subgoal *1.


     Perhaps we can prove it by induction.  Two 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 (NLISTP X) (p X V Z))
           (IMPLIES (AND (NOT (NLISTP X)) (p (CDR X) V Z))
                    (p X V Z))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP 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 the following two new goals:

Case 2. (IMPLIES (NLISTP X)
                 (EQUAL (PR-H X (H V Z))
                        (H V (PR-H X Z)))).

  This simplifies, opening up the functions NLISTP and PR-H, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP X))
                      (EQUAL (PR-H (CDR X) (H V Z))
                             (H V (PR-H (CDR X) Z))))
                 (EQUAL (PR-H X (H V Z))
                        (H V (PR-H X Z)))).

  This simplifies, rewriting with the lemma INTRO-H, and expanding NLISTP and
  PR-H, to:

        T.


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


[ 0.0 0.0 0.0 ]

PR-IS-AC


(DEFN PR-TIMES
      (L Z)
      (IF (NLISTP L)
          Z
          (TIMES (CAR L) (PR-TIMES (CDR L) Z))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, PR-TIMES is
accepted under the definitional principle.  From the definition we can
conclude that (OR (NUMBERP (PR-TIMES L Z)) (EQUAL (PR-TIMES L Z) Z)) is a
theorem.




[ 0.0 0.0 0.0 ]

PR-TIMES


(DEFN AC-TIMES
      (L Z)
      (IF (NLISTP L)
          Z
          (AC-TIMES (CDR L) (TIMES (CAR L) Z))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, AC-TIMES is
accepted under the definitional principle.  From the definition we can
conclude that (OR (NUMBERP (AC-TIMES L Z)) (EQUAL (AC-TIMES L Z) Z)) is a
theorem.




[ 0.0 0.0 0.0 ]

AC-TIMES


(FUNCTIONALLY-INSTANTIATE PR-TIMES-IS-AC-TIMES
                          (REWRITE)
                          (EQUAL (AC-TIMES L Z) (PR-TIMES L Z))
                          PR-IS-AC
                          ((H TIMES)
                           (PR-H PR-TIMES)
                           (AC-H (LAMBDA (X Y) (AC-TIMES X Y)))))


The functional instantiation of PR-IS-AC under:
      ((H TIMES)
       (PR-H PR-TIMES)
       (AC-H (LAMBDA (X Y) (AC-TIMES X Y))))
requires us to prove:
      (AND (EQUAL (AC-TIMES L Z)
                  (IF (NLISTP L)
                      Z
                      (AC-TIMES (CDR L) (TIMES (CAR L) Z))))
           (EQUAL (PR-TIMES L Z)
                  (IF (NLISTP L)
                      Z
                      (TIMES (CAR L) (PR-TIMES (CDR L) Z))))
           (EQUAL (TIMES X Y Z) (TIMES Y X Z))).



This formula can be simplified, using the abbreviation AND, to the following
three new conjectures:

Case 3. (EQUAL (AC-TIMES L Z)
               (IF (NLISTP L)
                   Z
                   (AC-TIMES (CDR L)
                             (TIMES (CAR L) Z)))).

  This simplifies, expanding AC-TIMES and NLISTP, to:

        T.

Case 2. (EQUAL (PR-TIMES L Z)
               (IF (NLISTP L)
                   Z
                   (TIMES (CAR L)
                          (PR-TIMES (CDR L) Z)))).

  This simplifies, opening up the functions PR-TIMES and NLISTP, to:

        T.

Case 1. (EQUAL (TIMES X Y Z) (TIMES Y X Z)).

  Name the above subgoal *1.


     We will appeal to induction.  There are four plausible inductions.  They
merge into two likely candidate inductions, both of which are unflawed.  Since
both of these are equally likely, we will choose arbitrarily.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Y)) (p X (SUB1 Y) Z))
                    (p X Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates two new formulas:

Case 2. (IMPLIES (ZEROP Y)
                 (EQUAL (TIMES X Y Z) (TIMES Y X Z))),

  which simplifies, opening up the functions ZEROP, EQUAL, and TIMES, to two
  new formulas:

  Case 2.2.
          (IMPLIES (EQUAL Y 0)
                   (EQUAL (TIMES X 0) 0)),

    which again simplifies, trivially, to the new formula:

          (EQUAL (TIMES X 0) 0),

    which we will name *1.1.

  Case 2.1.
          (IMPLIES (NOT (NUMBERP Y))
                   (EQUAL (TIMES X 0) 0)).

    Eliminate the irrelevant term.  We thus obtain:

          (EQUAL (TIMES X 0) 0),

    which we will name *1.2.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (EQUAL (TIMES X (SUB1 Y) Z)
                             (TIMES (SUB1 Y) X Z)))
                 (EQUAL (TIMES X Y Z) (TIMES Y X Z))).

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

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

  Applying the lemma SUB1-ELIM, replace Y by (ADD1 V) to eliminate (SUB1 Y).
  We use the type restriction lemma noted when SUB1 was introduced to restrict
  the new variable.  We thus obtain:

        (IMPLIES (AND (NUMBERP V)
                      (NOT (EQUAL (ADD1 V) 0))
                      (EQUAL (TIMES X V Z) (TIMES V X Z)))
                 (EQUAL (TIMES X (PLUS Z (TIMES V Z)))
                        (PLUS (TIMES X Z) (TIMES X V Z)))),

  which further simplifies, obviously, to:

        (IMPLIES (AND (NUMBERP V)
                      (EQUAL (TIMES X V Z) (TIMES V X Z)))
                 (EQUAL (TIMES X (PLUS Z (TIMES V Z)))
                        (PLUS (TIMES X Z) (TIMES V X Z)))).

  We use the above equality hypothesis by substituting (TIMES X V Z) for
  (TIMES V X Z) and throwing away the equality.  This generates:

        (IMPLIES (NUMBERP V)
                 (EQUAL (TIMES X (PLUS Z (TIMES V Z)))
                        (PLUS (TIMES X Z) (TIMES X V Z)))).

  We will try to prove the above formula by generalizing it, replacing
  (TIMES V Z) by A.  We restrict the new variable by recalling the type
  restriction lemma noted when TIMES was introduced.  We thus obtain the new
  formula:

        (IMPLIES (AND (NUMBERP A) (NUMBERP V))
                 (EQUAL (TIMES X (PLUS Z A))
                        (PLUS (TIMES X Z) (TIMES X A)))),

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

        (IMPLIES (NUMBERP A)
                 (EQUAL (TIMES X (PLUS Z A))
                        (PLUS (TIMES X Z) (TIMES X A)))),

  which we will finally name *1.3.


     We will appeal to induction.  The recursive terms in the conjecture
suggest four inductions.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP X) (p X Z A))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z A))
                    (p X Z A))).
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 produces two new conjectures:

Case 2. (IMPLIES (AND (ZEROP X) (NUMBERP A))
                 (EQUAL (TIMES X (PLUS Z A))
                        (PLUS (TIMES X Z) (TIMES X A)))),

  which simplifies, opening up ZEROP, EQUAL, TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) (PLUS Z A))
                             (PLUS (TIMES (SUB1 X) Z)
                                   (TIMES (SUB1 X) A)))
                      (NUMBERP A))
                 (EQUAL (TIMES X (PLUS Z A))
                        (PLUS (TIMES X Z) (TIMES X A)))),

  which simplifies, opening up the functions ZEROP and TIMES, to:

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

  But this again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.3.


     So let us turn our attention to:

      (EQUAL (TIMES X 0) 0),

which we named *1.2 above.  What luck!  This conjecture is subsumed by
formula *1.1 above.


     So next consider:

      (EQUAL (TIMES X 0) 0),

which is formula *1.1 above.  Let us appeal to the induction principle.  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 prove 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 the following two new goals:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (TIMES X 0) 0)).

  This simplifies, opening up the functions ZEROP, TIMES, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) 0) 0))
                 (EQUAL (TIMES X 0) 0)).

  This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL,
  to:

        T.


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


[ 0.0 0.0 0.0 ]

PR-TIMES-IS-AC-TIMES


(CONSTRAIN LT-INTRO
           (REWRITE)
           (IMPLIES (LT Z V) (NOT (LT V Z)))
           ((LT (LAMBDA (X Y) F))))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (IMPLIES F (NOT F)).

This formula simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LT-INTRO


(DEFN ORDERED-LT
      (L)
      (IF (LISTP L)
          (IF (LISTP (CDR L))
              (IF (LT (CADR L) (CAR L))
                  F
                  (ORDERED-LT (CDR L)))
              T)
          T))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT L) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, ORDERED-LT is accepted under the principle of
definition.  Observe that (OR (FALSEP (ORDERED-LT L)) (TRUEP (ORDERED-LT L)))
is a theorem.




[ 0.0 0.0 0.0 ]

ORDERED-LT


(DEFN ADDTOLIST-LT
      (X L)
      (IF (LISTP L)
          (IF (LT X (CAR L))
              (CONS X L)
              (CONS (CAR L)
                    (ADDTOLIST-LT X (CDR L))))
          (LIST X)))

     Linear arithmetic and the lemma CDR-LESSP can be used to show that the
measure (COUNT L) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, ADDTOLIST-LT is accepted under the definitional
principle.  Note that (LISTP (ADDTOLIST-LT X L)) is a theorem.




[ 0.0 0.0 0.0 ]

ADDTOLIST-LT


(DEFN SORT-LT
      (L)
      (IF (LISTP L)
          (ADDTOLIST-LT (CAR L)
                        (SORT-LT (CDR L)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, SORT-LT is accepted under the definitional principle.
From the definition we can conclude that:
      (OR (LITATOM (SORT-LT L))
          (LISTP (SORT-LT L)))
is a theorem.




[ 0.0 0.0 0.0 ]

SORT-LT


(PROVE-LEMMA ORDERED-SORT-LT
             (REWRITE)
             (ORDERED-LT (SORT-LT L)))


     Call the conjecture *1.


     Let us appeal to the induction principle.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP L) (p (CDR L)))
                    (p L))
           (IMPLIES (NOT (LISTP L)) (p L))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme leads to two new goals:

Case 2. (IMPLIES (AND (LISTP L)
                      (ORDERED-LT (SORT-LT (CDR L))))
                 (ORDERED-LT (SORT-LT L))),

  which simplifies, expanding the definition of SORT-LT, to the conjecture:

        (IMPLIES (AND (LISTP L)
                      (ORDERED-LT (SORT-LT (CDR L))))
                 (ORDERED-LT (ADDTOLIST-LT (CAR L)
                                           (SORT-LT (CDR L))))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS Z X) to
  eliminate (CDR L) and (CAR L).  This generates:

        (IMPLIES (ORDERED-LT (SORT-LT X))
                 (ORDERED-LT (ADDTOLIST-LT Z (SORT-LT X)))).

  We will try to prove the above formula by generalizing it, replacing
  (SORT-LT X) by Y.  The result is:

        (IMPLIES (ORDERED-LT Y)
                 (ORDERED-LT (ADDTOLIST-LT Z Y))).

  Give the above formula the name *1.1.

Case 1. (IMPLIES (NOT (LISTP L))
                 (ORDERED-LT (SORT-LT L))).

  This simplifies, expanding SORT-LT and ORDERED-LT, to:

        T.


     So let us turn our attention to:

      (IMPLIES (ORDERED-LT Y)
               (ORDERED-LT (ADDTOLIST-LT Z Y))),

named *1.1 above.  Perhaps we can 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 (AND (LISTP Y)
                         (LISTP (CDR Y))
                         (LT (CADR Y) (CAR Y)))
                    (p Z Y))
           (IMPLIES (AND (LISTP Y)
                         (LISTP (CDR Y))
                         (NOT (LT (CADR Y) (CAR Y)))
                         (p Z (CDR Y)))
                    (p Z Y))
           (IMPLIES (AND (LISTP Y) (NOT (LISTP (CDR Y))))
                    (p Z Y))
           (IMPLIES (NOT (LISTP Y)) (p Z Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme generates the following five new
conjectures:

Case 5. (IMPLIES (AND (LISTP Y)
                      (LISTP (CDR Y))
                      (LT (CADR Y) (CAR Y))
                      (ORDERED-LT Y))
                 (ORDERED-LT (ADDTOLIST-LT Z Y))).

  This simplifies, expanding ORDERED-LT, to:

        T.

Case 4. (IMPLIES (AND (LISTP Y)
                      (LISTP (CDR Y))
                      (NOT (LT (CADR Y) (CAR Y)))
                      (NOT (ORDERED-LT (CDR Y)))
                      (ORDERED-LT Y))
                 (ORDERED-LT (ADDTOLIST-LT Z Y))).

  This simplifies, expanding ORDERED-LT, to:

        T.

Case 3. (IMPLIES (AND (LISTP Y)
                      (LISTP (CDR Y))
                      (NOT (LT (CADR Y) (CAR Y)))
                      (ORDERED-LT (ADDTOLIST-LT Z (CDR Y)))
                      (ORDERED-LT Y))
                 (ORDERED-LT (ADDTOLIST-LT Z Y))).

  This simplifies, opening up the definitions of ORDERED-LT and ADDTOLIST-LT,
  to the following two new formulas:

  Case 3.2.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LT (CADR Y) (CAR Y)))
                        (ORDERED-LT (ADDTOLIST-LT Z (CDR Y)))
                        (ORDERED-LT (CDR Y))
                        (NOT (LT Z (CAR Y))))
                   (ORDERED-LT (CONS (CAR Y)
                                     (ADDTOLIST-LT Z (CDR Y))))).

    This again simplifies, rewriting with CAR-CONS and CDR-CONS, and opening
    up the function ORDERED-LT, to:

          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LT (CADR Y) (CAR Y)))
                        (ORDERED-LT (ADDTOLIST-LT Z (CDR Y)))
                        (ORDERED-LT (CDR Y))
                        (NOT (LT Z (CAR Y))))
                   (NOT (LT (CAR (ADDTOLIST-LT Z (CDR Y)))
                            (CAR Y)))).

    Applying the lemma CAR-CDR-ELIM, replace Y by (CONS V X) to eliminate
    (CDR Y) and (CAR Y) and X by (CONS W D) to eliminate (CAR X) and (CDR X).
    We thus obtain:

          (IMPLIES (AND (NOT (LT W V))
                        (ORDERED-LT (ADDTOLIST-LT Z (CONS W D)))
                        (ORDERED-LT (CONS W D))
                        (NOT (LT Z V)))
                   (NOT (LT (CAR (ADDTOLIST-LT Z (CONS W D)))
                            V))),

    which further simplifies, appealing to the lemmas CDR-CONS and CAR-CONS,
    and opening up the definitions of ADDTOLIST-LT and ORDERED-LT, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP Y)
                        (LISTP (CDR Y))
                        (NOT (LT (CADR Y) (CAR Y)))
                        (ORDERED-LT (ADDTOLIST-LT Z (CDR Y)))
                        (ORDERED-LT (CDR Y))
                        (LT Z (CAR Y)))
                   (ORDERED-LT (CONS Z Y))),

    which again simplifies, rewriting with the lemmas LT-INTRO, CAR-CONS, and
    CDR-CONS, and opening up the function ORDERED-LT, to:

          T.

Case 2. (IMPLIES (AND (LISTP Y)
                      (NOT (LISTP (CDR Y)))
                      (ORDERED-LT Y))
                 (ORDERED-LT (ADDTOLIST-LT Z Y))),

  which simplifies, expanding the functions ORDERED-LT and ADDTOLIST-LT, to
  two new formulas:

  Case 2.2.
          (IMPLIES (AND (LISTP Y)
                        (NOT (LISTP (CDR Y)))
                        (NOT (LT Z (CAR Y))))
                   (ORDERED-LT (CONS (CAR Y)
                                     (ADDTOLIST-LT Z (CDR Y))))),

    which again simplifies, rewriting with CAR-CONS and CDR-CONS, and
    unfolding the definition of ORDERED-LT, to the following two new goals:

    Case 2.2.2.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NOT (LT Z (CAR Y))))
                     (NOT (LT (CAR (ADDTOLIST-LT Z (CDR Y)))
                              (CAR Y)))).

      This further simplifies, applying the lemma CAR-CONS, and opening up the
      definition of ADDTOLIST-LT, to:

            T.

    Case 2.2.1.
            (IMPLIES (AND (LISTP Y)
                          (NOT (LISTP (CDR Y)))
                          (NOT (LT Z (CAR Y))))
                     (ORDERED-LT (ADDTOLIST-LT Z (CDR Y)))),

      which further simplifies, applying CDR-CONS, and unfolding ADDTOLIST-LT,
      LISTP, and ORDERED-LT, to:

            T.

  Case 2.1.
          (IMPLIES (AND (LISTP Y)
                        (NOT (LISTP (CDR Y)))
                        (LT Z (CAR Y)))
                   (ORDERED-LT (CONS Z Y))).

    But this again simplifies, appealing to the lemmas LT-INTRO, CAR-CONS, and
    CDR-CONS, and unfolding the function ORDERED-LT, to:

          T.

Case 1. (IMPLIES (AND (NOT (LISTP Y)) (ORDERED-LT Y))
                 (ORDERED-LT (ADDTOLIST-LT Z Y))),

  which simplifies, rewriting with the lemma CDR-CONS, and expanding the
  functions ORDERED-LT, ADDTOLIST-LT, and LISTP, 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 ]

ORDERED-SORT-LT


(DEFN ORDERED-LESSP
      (L)
      (IF (LISTP L)
          (IF (LISTP (CDR L))
              (IF (LESSP (CADR L) (CAR L))
                  F
                  (ORDERED-LESSP (CDR L)))
              T)
          T))

     Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT L) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, ORDERED-LESSP is accepted under the principle of
definition.  Observe that:
      (OR (FALSEP (ORDERED-LESSP L))
          (TRUEP (ORDERED-LESSP L)))
is a theorem.




[ 0.0 0.0 0.0 ]

ORDERED-LESSP


(DEFN ADDTOLIST-LESSP
      (X L)
      (IF (LISTP L)
          (IF (LESSP X (CAR L))
              (CONS X L)
              (CONS (CAR L)
                    (ADDTOLIST-LESSP X (CDR L))))
          (LIST X)))

     Linear arithmetic and the lemma CDR-LESSP can be used to show that the
measure (COUNT L) decreases according to the well-founded relation LESSP in
each recursive call.  Hence, ADDTOLIST-LESSP is accepted under the
definitional principle.  Note that (LISTP (ADDTOLIST-LESSP X L)) is a theorem.




[ 0.0 0.0 0.0 ]

ADDTOLIST-LESSP


(DEFN SORT-LESSP
      (L)
      (IF (LISTP L)
          (ADDTOLIST-LESSP (CAR L)
                           (SORT-LESSP (CDR L)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, SORT-LESSP is accepted under the definitional
principle.  From the definition we can conclude that:
      (OR (LITATOM (SORT-LESSP L))
          (LISTP (SORT-LESSP L)))
is a theorem.




[ 0.0 0.0 0.0 ]

SORT-LESSP


(FUNCTIONALLY-INSTANTIATE ORDERED-SORT-LESSP
                          (REWRITE)
                          (ORDERED-LESSP (SORT-LESSP L))
                          ORDERED-SORT-LT
                          ((LT LESSP)
                           (ORDERED-LT ORDERED-LESSP)
                           (ADDTOLIST-LT ADDTOLIST-LESSP)
                           (SORT-LT SORT-LESSP)))


The functional instantiation of ORDERED-SORT-LT under:
      ((LT LESSP)
       (ORDERED-LT ORDERED-LESSP)
       (ADDTOLIST-LT ADDTOLIST-LESSP)
       (SORT-LT SORT-LESSP))
requires us to prove:
      (AND (EQUAL (SORT-LESSP L)
                  (IF (LISTP L)
                      (ADDTOLIST-LESSP (CAR L)
                                       (SORT-LESSP (CDR L)))
                      NIL))
           (EQUAL (ADDTOLIST-LESSP X L)
                  (IF (LISTP L)
                      (IF (LESSP X (CAR L))
                          (CONS X L)
                          (CONS (CAR L)
                                (ADDTOLIST-LESSP X (CDR L))))
                      (LIST X)))
           (EQUAL (ORDERED-LESSP L)
                  (IF (LISTP L)
                      (IF (LISTP (CDR L))
                          (IF (LESSP (CADR L) (CAR L))
                              F
                              (ORDERED-LESSP (CDR L)))
                          T)
                      T))
           (IMPLIES (LESSP Z V)
                    (NOT (LESSP V Z)))).



This formula can be simplified, using the abbreviations NOT, IMPLIES, and AND,
to the following four new formulas:

Case 4. (EQUAL (SORT-LESSP L)
               (IF (LISTP L)
                   (ADDTOLIST-LESSP (CAR L)
                                    (SORT-LESSP (CDR L)))
                   NIL)).

  This simplifies, opening up the definition of SORT-LESSP, to:

        T.

Case 3. (EQUAL (ADDTOLIST-LESSP X L)
               (IF (LISTP L)
                   (IF (LESSP X (CAR L))
                       (CONS X L)
                       (CONS (CAR L)
                             (ADDTOLIST-LESSP X (CDR L))))
                   (LIST X))).

  This simplifies, unfolding ADDTOLIST-LESSP, to:

        T.

Case 2. (EQUAL (ORDERED-LESSP L)
               (IF (LISTP L)
                   (IF (LISTP (CDR L))
                       (IF (LESSP (CADR L) (CAR L))
                           F
                           (ORDERED-LESSP (CDR L)))
                       T)
                   T)).

  This simplifies, unfolding the function ORDERED-LESSP, to:

        T.

Case 1. (IMPLIES (LESSP Z V)
                 (NOT (LESSP V Z))).

  This simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ORDERED-SORT-LESSP


(CONSTRAIN FN-INTRO NIL T ((FN ADD1)))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove T.

This conjecture can be propositionally simplified to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FN-INTRO


(DEFN MAP-FN
      (X)
      (IF (NLISTP X)
          NIL
          (CONS (FN (CAR X)) (MAP-FN (CDR X)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, MAP-FN is
accepted under the definitional principle.  Observe that:
      (OR (LITATOM (MAP-FN X))
          (LISTP (MAP-FN X)))
is a theorem.




[ 0.0 0.0 0.0 ]

MAP-FN


(PROVE-LEMMA MAP-DISTRIBUTES-OVER-APPEND
             (REWRITE)
             (EQUAL (MAP-FN (APPEND U V))
                    (APPEND (MAP-FN U) (MAP-FN V))))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Three 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 (AND (LISTP U) (p (CDR U) V))
                    (p U V))
           (IMPLIES (NOT (LISTP U)) (p U V))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT U) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme leads to two
new goals:

Case 2. (IMPLIES (AND (LISTP U)
                      (EQUAL (MAP-FN (APPEND (CDR U) V))
                             (APPEND (MAP-FN (CDR U)) (MAP-FN V))))
                 (EQUAL (MAP-FN (APPEND U V))
                        (APPEND (MAP-FN U) (MAP-FN V)))),

  which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
  the definitions of APPEND and MAP-FN, to:

        T.

Case 1. (IMPLIES (NOT (LISTP U))
                 (EQUAL (MAP-FN (APPEND U V))
                        (APPEND (MAP-FN U) (MAP-FN V)))),

  which simplifies, unfolding the functions APPEND, MAP-FN, and LISTP, to:

        T.


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


[ 0.0 0.0 0.0 ]

MAP-DISTRIBUTES-OVER-APPEND


(DEFN MAP-PLUS-Y
      (X Y)
      (IF (NLISTP X)
          NIL
          (CONS (PLUS (CAR X) Y)
                (MAP-PLUS-Y (CDR X) Y))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, MAP-PLUS-Y
is accepted under the principle of definition.  Note that:
      (OR (LITATOM (MAP-PLUS-Y X Y))
          (LISTP (MAP-PLUS-Y X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

MAP-PLUS-Y


(FUNCTIONALLY-INSTANTIATE MAP-PLUS-Y-DISTRIBUTES-OVER-APPEND
                          (REWRITE)
                          (EQUAL (MAP-PLUS-Y (APPEND U V) Z)
                                 (APPEND (MAP-PLUS-Y U Z)
                                         (MAP-PLUS-Y V Z)))
                          MAP-DISTRIBUTES-OVER-APPEND
                          ((FN (LAMBDA (X) (PLUS X Z)))
                           (MAP-FN (LAMBDA (X) (MAP-PLUS-Y X Z)))))


The functional instantiation of MAP-DISTRIBUTES-OVER-APPEND under:
      ((FN (LAMBDA (X) (PLUS X Z)))
       (MAP-FN (LAMBDA (X) (MAP-PLUS-Y X Z))))
requires us to prove:
      (EQUAL (MAP-PLUS-Y X Z)
             (IF (NLISTP X)
                 NIL
                 (CONS (PLUS (CAR X) Z)
                       (MAP-PLUS-Y (CDR X) Z)))).



This conjecture simplifies, expanding the functions MAP-PLUS-Y and NLISTP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

MAP-PLUS-Y-DISTRIBUTES-OVER-APPEND


(DEFN TRUE-REC
      (X)
      (IF (NLISTP X) T (TRUE-REC (CDR X))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
TRUE-REC is accepted under the definitional principle.  Note that
(TRUEP (TRUE-REC X)) is a theorem.




[ 0.0 0.0 0.0 ]

TRUE-REC


(PROVE-LEMMA TRUE-REC-IS-TRUE
             (REWRITE)
             (TRUE-REC X))

This conjecture simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TRUE-REC-IS-TRUE


(DEFN APP
      (X Y)
      (IF (NLISTP X)
          Y
          (CONS (CAR X) (APP (CDR X) Y))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, APP is
accepted under the definitional principle.  From the definition we can
conclude that (OR (LISTP (APP X Y)) (EQUAL (APP X Y) Y)) is a theorem.




[ 0.0 0.0 0.0 ]

APP


(FUNCTIONALLY-INSTANTIATE ASSOC-OF-APP
                          (REWRITE)
                          (EQUAL (APP (APP X Y) Z)
                                 (APP X (APP Y Z)))
                          TRUE-REC-IS-TRUE
                          ((TRUE-REC (LAMBDA (X)
                                             (EQUAL (APP (APP X Y) Z)
                                                    (APP X (APP Y Z)))))))


The functional instantiation of TRUE-REC-IS-TRUE under:
      ((TRUE-REC (LAMBDA (X)
                         (EQUAL (APP (APP X Y) Z)
                                (APP X (APP Y Z))))))
requires us to prove:
      (EQUAL (EQUAL (APP (APP X Y) Z)
                    (APP X (APP Y Z)))
             (IF (NLISTP X)
                 T
                 (EQUAL (APP (APP (CDR X) Y) Z)
                        (APP (CDR X) (APP Y Z))))).



This formula simplifies, expanding the definitions of APP and NLISTP, to the
following two new goals:

Case 2. (IMPLIES (AND (LISTP X)
                      (NOT (EQUAL (APP (CONS (CAR X) (APP (CDR X) Y)) Z)
                                  (CONS (CAR X)
                                        (APP (CDR X) (APP Y Z))))))
                 (NOT (EQUAL (APP (APP (CDR X) Y) Z)
                             (APP (CDR X) (APP Y Z))))).

  However this again simplifies, applying the lemmas CDR-CONS and CAR-CONS,
  and expanding the function APP, to:

        T.

Case 1. (IMPLIES (AND (LISTP X)
                      (EQUAL (APP (CONS (CAR X) (APP (CDR X) Y)) Z)
                             (CONS (CAR X)
                                   (APP (CDR X) (APP Y Z)))))
                 (EQUAL (EQUAL (APP (APP (CDR X) Y) Z)
                               (APP (CDR X) (APP Y Z)))
                        T)),

  which again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
  opening up the definition of APP, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOC-OF-APP


(CONSTRAIN ALL-X-P-X-INTRO
           (REWRITE)
           (IMPLIES (ALL-X-P-X) (P X))
           ((ALL-X-P-X FALSE)))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (IMPLIES F (P X)).

This simplifies, clearly, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ALL-X-P-X-INTRO


(CONSTRAIN ALL-X-NOT-P-X-INTO
           (REWRITE)
           (IMPLIES (ALL-X-NOT-P-X) (NOT (P X)))
           ((ALL-X-NOT-P-X FALSE)))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (IMPLIES F (NOT (P X))).

This formula simplifies, obviously, to:

      T.

Q.E.D.


[ 0.1 0.0 0.0 ]

ALL-X-NOT-P-X-INTO


(PROVE-LEMMA ALL-X-NOT-P-X-INTO-CONVERSE
             (REWRITE)
             (IMPLIES (P X) (NOT (ALL-X-NOT-P-X))))

WARNING:  Note that ALL-X-NOT-P-X-INTO-CONVERSE contains the free variable X
which will be chosen by instantiating the hypothesis (P X).


This conjecture simplifies, rewriting with ALL-X-NOT-P-X-INTO, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ALL-X-NOT-P-X-INTO-CONVERSE


(DEFN SOME-X-P-X NIL
      (NOT (ALL-X-NOT-P-X)))

     Observe that (OR (FALSEP (SOME-X-P-X)) (TRUEP (SOME-X-P-X))) is a theorem.




[ 0.0 0.0 0.0 ]

SOME-X-P-X


(PROVE-LEMMA ALL-IMPLIES-SOME NIL
             (IMPLIES (ALL-X-P-X) (SOME-X-P-X))
             ((USE (ALL-X-P-X-INTRO))))

This formula can be simplified, using the abbreviations SOME-X-P-X and IMPLIES,
to the new conjecture:

      (IMPLIES (AND (IMPLIES (ALL-X-P-X) (P X))
                    (ALL-X-P-X))
               (NOT (ALL-X-NOT-P-X))),

which simplifies, rewriting with ALL-X-NOT-P-X-INTO, and opening up IMPLIES,
to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ALL-IMPLIES-SOME


(DEFN EVEN
      (X)
      (IF (ZEROP X)
          T
          (IF (EQUAL X 1)
              (FALSE)
              (NOT (EVEN (SUB1 X))))))

     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, EVEN is accepted under the
definitional principle.  Note that (OR (FALSEP (EVEN X)) (TRUEP (EVEN X))) is
a theorem.




[ 0.0 0.0 0.0 ]

EVEN


(CONSTRAIN FAIR-INTRO
           (REWRITE)
           (AND (FAIR (FAIR-TRUE-WITNESS N))
                (NOT (FAIR (FAIR-FALSE-WITNESS N)))
                (NOT (LESSP (FAIR-TRUE-WITNESS N) N))
                (NOT (LESSP (FAIR-FALSE-WITNESS N) N)))
           ((FAIR EVEN)
            (FAIR-TRUE-WITNESS (LAMBDA (X) (IF (EVEN X) X (ADD1 X))))
            (FAIR-FALSE-WITNESS (LAMBDA (X)
                                        (IF (EVEN X) (ADD1 X) X)))))

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



We will verify the consistency and the conservative nature of this constraint
by attempting to prove:
      (AND (EVEN (IF (EVEN N) N (ADD1 N)))
           (NOT (EVEN (IF (EVEN N) (ADD1 N) N)))
           (NOT (LESSP (IF (EVEN N) N (ADD1 N)) N))
           (NOT (LESSP (IF (EVEN N) (ADD1 N) N) N))).


This formula can be simplified, using the abbreviations NOT and AND, to the
following four new formulas:

Case 4. (EVEN (IF (EVEN N) N (ADD1 N))).

  This simplifies, clearly, to:

        (IMPLIES (NOT (EVEN N))
                 (EVEN (ADD1 N))),

  which again simplifies, applying SUB1-ADD1 and ADD1-EQUAL, and opening up
  EQUAL, NUMBERP, and EVEN, to the following two new conjectures:

  Case 4.2.
          (IMPLIES (NOT (EVEN N)) (NUMBERP N)).

    But this again simplifies, expanding the function EVEN, to:

          T.

  Case 4.1.
          (IMPLIES (NOT (EVEN N))
                   (NOT (EQUAL N 0))),

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

          T.

Case 3. (NOT (EVEN (IF (EVEN N) (ADD1 N) N))),

  which simplifies, trivially, to the new goal:

        (IMPLIES (EVEN N)
                 (NOT (EVEN (ADD1 N)))),

  which again simplifies, appealing to the lemmas SUB1-ADD1 and ADD1-EQUAL,
  and expanding EQUAL, NUMBERP, and EVEN, to:

        T.

Case 2. (NOT (LESSP (IF (EVEN N) N (ADD1 N)) N)),

  which simplifies, trivially, to the following two new formulas:

  Case 2.2.
          (IMPLIES (NOT (EVEN N))
                   (NOT (LESSP (ADD1 N) N))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (EVEN N) (NOT (LESSP N N))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (NOT (LESSP (IF (EVEN N) (ADD1 N) N) N)),

  which simplifies, obviously, to the following two new conjectures:

  Case 1.2.
          (IMPLIES (NOT (EVEN N))
                   (NOT (LESSP N N))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (EVEN N)
                   (NOT (LESSP (ADD1 N) N))),

    which again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FAIR-INTRO


(CONSTRAIN NUM-INTRO
           (REWRITE)
           (NUMBERP (NUM X))
           ((NUM ADD1)))

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



We will verify the consistency and the conservative nature of this constraint
by attempting to prove (NUMBERP (ADD1 X)).

This simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NUM-INTRO


(DEFN INTERP
      (X)
      (IF (NOT (ZEROP X))
          (TIMES X X)
          (NUM X)))

     Observe that (NUMBERP (INTERP X)) is a theorem.




[ 0.0 0.0 0.0 ]

INTERP


(PROVE-LEMMA INTERP-IS-NUMERIC
             (REWRITE)
             (NUMBERP (INTERP X)))

This simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INTERP-IS-NUMERIC


(DEFN INTERP2
      (X)
      (IF (NOT (ZEROP X))
          (TIMES X X)
          (PLUS X X)))

     Note that (NUMBERP (INTERP2 X)) is a theorem.




[ 0.0 0.0 0.0 ]

INTERP2


(FUNCTIONALLY-INSTANTIATE INTERP2-IS-NUMERIC
                          (REWRITE)
                          (NUMBERP (INTERP2 X))
                          INTERP-IS-NUMERIC
                          ((INTERP INTERP2)
                           (NUM (LAMBDA (X) (PLUS X X)))))


The functional instantiation of INTERP-IS-NUMERIC under:
      ((INTERP INTERP2)
       (NUM (LAMBDA (X) (PLUS X X))))
requires us to prove:
      (AND (EQUAL (INTERP2 X)
                  (IF (NOT (ZEROP X))
                      (TIMES X X)
                      (PLUS X X)))
           (NUMBERP (PLUS X X))).



This formula can be simplified, using the abbreviation AND, to the following
two new goals:

Case 2. (EQUAL (INTERP2 X)
               (IF (NOT (ZEROP X))
                   (TIMES X X)
                   (PLUS X X))).

  This simplifies, unfolding PLUS, INTERP2, ZEROP, and NOT, to the following
  two new conjectures:

  Case 2.2.
          (IMPLIES (NOT (NUMBERP X))
                   (EQUAL 0 (PLUS X X))).

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

          T.

  Case 2.1.
          (IMPLIES (EQUAL X 0)
                   (EQUAL 0 (PLUS X X))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (NUMBERP (PLUS X X)),

  which simplifies, obviously, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INTERP2-IS-NUMERIC


(DEFN P-ALIAS (X) (P X))

   




[ 0.0 0.0 0.0 ]

P-ALIAS


(ADD-AXIOM EVEN-P-ALIAS
           (REWRITE)
           (EVEN (P-ALIAS X)))

[ 0.0 0.0 0.0 ]

EVEN-P-ALIAS


(PROVE-LEMMA EVEN-P
             (REWRITE)
             (EVEN (P X))
             ((USE (EVEN-P-ALIAS))))

This conjecture can be simplified, using the abbreviation P-ALIAS, to:

      T.

This simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EVEN-P


(CONSTRAIN PP-INTRO
           (REWRITE)
           (IMPLIES (EQUAL Y 0) (EQUAL (PP) Y))
           ((PP (LAMBDA NIL 0))))

WARNING:  Note that PP-INTRO contains the free variable Y which will be chosen
by instantiating the hypothesis (EQUAL Y 0).



We will verify the consistency and the conservative nature of this constraint
by attempting to prove (IMPLIES (EQUAL Y 0) (EQUAL 0 Y)).

This conjecture simplifies, clearly, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PP-INTRO


(PROVE-LEMMA PP-IS-0
             (REWRITE)
             (EQUAL 0 (PP)))

This formula simplifies, applying PP-INTRO, and unfolding the definition of
EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PP-IS-0


(CONSTRAIN FN-COMMUTATIVE
           (REWRITE)
           (EQUAL (FN2 X Y) (FN2 Y X))
           ((FN2 PLUS)))


We will verify the consistency and the conservative nature of this constraint
by attempting to prove (EQUAL (PLUS X Y) (PLUS Y X)).

This formula simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FN-COMMUTATIVE


(DEFN FOLDR-FN
      (LST R)
      (IF (LISTP LST)
          (FN2 (CAR LST) (FOLDR-FN (CDR LST) R))
          R))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, FOLDR-FN is accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

FOLDR-FN


(DEFN FOLDL-FN
      (LST R)
      (IF (LISTP LST)
          (FOLDL-FN (CDR LST) (FN2 R (CAR LST)))
          R))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, FOLDL-FN is accepted under the definitional principle.




[ 0.0 0.0 0.0 ]

FOLDL-FN


(DEFN REVERSE
      (X)
      (IF (LISTP X)
          (APPEND (REVERSE (CDR X))
                  (LIST (CAR X)))
          NIL))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, REVERSE is accepted under the principle of definition.
Note that (OR (LITATOM (REVERSE X)) (LISTP (REVERSE X))) is a theorem.




[ 0.0 0.0 0.0 ]

REVERSE


(PROVE-LEMMA FOLDL-IS-FOLDR
             (REWRITE)
             (EQUAL (FOLDR-FN LST R)
                    (FOLDL-FN (REVERSE LST) R)))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (AND (LISTP LST) (p (CDR LST) R))
                    (p LST R))
           (IMPLIES (NOT (LISTP LST))
                    (p LST R))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  The above induction scheme produces the
following two new goals:

Case 2. (IMPLIES (AND (LISTP LST)
                      (EQUAL (FOLDR-FN (CDR LST) R)
                             (FOLDL-FN (REVERSE (CDR LST)) R)))
                 (EQUAL (FOLDR-FN LST R)
                        (FOLDL-FN (REVERSE LST) R))).

  This simplifies, expanding FOLDR-FN and REVERSE, to:

        (IMPLIES (AND (LISTP LST)
                      (EQUAL (FOLDR-FN (CDR LST) R)
                             (FOLDL-FN (REVERSE (CDR LST)) R)))
                 (EQUAL (FN2 (CAR LST) (FOLDR-FN (CDR LST) R))
                        (FOLDL-FN (APPEND (REVERSE (CDR LST))
                                          (LIST (CAR LST)))
                                  R))).

  Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
  (CDR LST) and (CAR LST).  This produces:

        (IMPLIES (EQUAL (FOLDR-FN X R)
                        (FOLDL-FN (REVERSE X) R))
                 (EQUAL (FN2 Z (FOLDR-FN X R))
                        (FOLDL-FN (APPEND (REVERSE X) (LIST Z))
                                  R))).

  We use the above equality hypothesis by substituting
  (FOLDL-FN (REVERSE X) R) for (FOLDR-FN X R) and throwing away the equality.
  This generates:

        (EQUAL (FN2 Z (FOLDL-FN (REVERSE X) R))
               (FOLDL-FN (APPEND (REVERSE X) (LIST Z))
                         R)).

  We will try to prove the above formula by generalizing it, replacing
  (REVERSE X) by Y.  We must thus prove the formula:

        (EQUAL (FN2 Z (FOLDL-FN Y R))
               (FOLDL-FN (APPEND Y (LIST Z)) R)).

  Name the above subgoal *1.1.

Case 1. (IMPLIES (NOT (LISTP LST))
                 (EQUAL (FOLDR-FN LST R)
                        (FOLDL-FN (REVERSE LST) R))).

  This simplifies, opening up FOLDR-FN, REVERSE, LISTP, and FOLDL-FN, to:

        T.


     So next consider:

      (EQUAL (FN2 Z (FOLDL-FN Y R))
             (FOLDL-FN (APPEND Y (LIST Z)) R)),

which is formula *1.1 above.  Perhaps we can prove it by induction.  Two
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 (AND (LISTP Y)
                         (p Z (CDR Y) (FN2 R (CAR Y))))
                    (p Z Y R))
           (IMPLIES (NOT (LISTP Y)) (p Z Y R))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  Note, however, the inductive instance chosen for R.  The above
induction scheme leads to the following two new conjectures:

Case 2. (IMPLIES (AND (LISTP Y)
                      (EQUAL (FN2 Z
                                  (FOLDL-FN (CDR Y) (FN2 R (CAR Y))))
                             (FOLDL-FN (APPEND (CDR Y) (LIST Z))
                                       (FN2 R (CAR Y)))))
                 (EQUAL (FN2 Z (FOLDL-FN Y R))
                        (FOLDL-FN (APPEND Y (LIST Z)) R))).

  This simplifies, rewriting with CAR-CONS and CDR-CONS, and expanding the
  definitions of FOLDL-FN and APPEND, to:

        T.

Case 1. (IMPLIES (NOT (LISTP Y))
                 (EQUAL (FN2 Z (FOLDL-FN Y R))
                        (FOLDL-FN (APPEND Y (LIST Z)) R))),

  which simplifies, applying FN-COMMUTATIVE, CAR-CONS, and CDR-CONS, and
  unfolding the definitions of FOLDL-FN, APPEND, and LISTP, to:

        T.


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


[ 0.0 0.0 0.0 ]

FOLDL-IS-FOLDR


(PROVE-LEMMA TIMES-ADD1
             (REWRITE)
             (EQUAL (TIMES X (ADD1 Y))
                    (PLUS X (TIMES X Y))))


     Give the conjecture the name *1.


     We will try to prove it by induction.  There are three plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
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 induction step of the scheme.  The above induction scheme
generates two new goals:

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

  which simplifies, expanding ZEROP, EQUAL, TIMES, PLUS, and NUMBERP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                             (PLUS (SUB1 X) (TIMES (SUB1 X) Y))))
                 (EQUAL (TIMES X (ADD1 Y))
                        (PLUS X (TIMES X Y)))),

  which simplifies, appealing to the lemma SUB1-ADD1, and unfolding the
  definitions of ZEROP, TIMES, and PLUS, to two new conjectures:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                               (PLUS (SUB1 X) (TIMES (SUB1 X) Y)))
                        (NOT (NUMBERP Y)))
                   (EQUAL (ADD1 (PLUS 0 (TIMES (SUB1 X) (ADD1 Y))))
                          (PLUS X Y (TIMES (SUB1 X) Y)))),

    which again simplifies, opening up EQUAL and PLUS, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                               (PLUS (SUB1 X) (TIMES (SUB1 X) Y)))
                        (NUMBERP Y))
                   (EQUAL (ADD1 (PLUS Y (TIMES (SUB1 X) (ADD1 Y))))
                          (PLUS X Y (TIMES (SUB1 X) Y)))),

    which again simplifies, using linear arithmetic, to:

          T.


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


[ 0.0 0.0 0.0 ]

TIMES-ADD1


(PROVE-LEMMA TIMES-COMM
             (REWRITE)
             (EQUAL (TIMES X Y) (TIMES Y X)))

WARNING:  the newly proposed lemma, TIMES-COMM, could be applied whenever the
previously added lemma TIMES-ADD1 could.





     Give the conjecture the name *1.


     We will appeal to induction.  Two inductions are suggested by terms in
the conjecture, both of which are flawed.  We limit our consideration to the
two suggested by the largest number of nonprimitive recursive functions in the
conjecture.  Since both of these are equally likely, we will choose
arbitrarily.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
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 induction step of the scheme.  The above induction scheme
produces the following two new conjectures:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (TIMES X Y) (TIMES Y X))).

  This simplifies, expanding the functions ZEROP, EQUAL, and TIMES, to the
  following two new conjectures:

  Case 2.2.
          (IMPLIES (EQUAL X 0)
                   (EQUAL 0 (TIMES Y 0))).

    This again simplifies, obviously, to:

          (EQUAL 0 (TIMES Y 0)),

    which we will name *1.1.

  Case 2.1.
          (IMPLIES (NOT (NUMBERP X))
                   (EQUAL 0 (TIMES Y X))).

    Name the above subgoal *1.2.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) Y)
                             (TIMES Y (SUB1 X))))
                 (EQUAL (TIMES X Y) (TIMES Y X))).

  This simplifies, opening up ZEROP and TIMES, to the new conjecture:

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

  Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X).
  We employ the type restriction lemma noted when SUB1 was introduced to
  restrict the new variable.  This produces the new conjecture:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (EQUAL (TIMES Z Y) (TIMES Y Z)))
                 (EQUAL (PLUS Y (TIMES Y Z))
                        (TIMES Y (ADD1 Z)))),

  which further simplifies, rewriting with TIMES-ADD1, to:

        T.


     So we now return to:

      (IMPLIES (NOT (NUMBERP X))
               (EQUAL 0 (TIMES Y X))),

which is formula *1.2 above.  We will appeal to induction.  There is only one
plausible induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p Y X))
           (IMPLIES (AND (NOT (ZEROP Y)) (p (SUB1 Y) X))
                    (p Y X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT Y) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates the following two new goals:

Case 2. (IMPLIES (AND (ZEROP Y) (NOT (NUMBERP X)))
                 (EQUAL 0 (TIMES Y X))).

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

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (EQUAL 0 (TIMES (SUB1 Y) X))
                      (NOT (NUMBERP X)))
                 (EQUAL 0 (TIMES Y X))).

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

        T.


     That finishes the proof of *1.2.


     So we now return to:

      (EQUAL 0 (TIMES Y 0)),

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

Case 2. (IMPLIES (ZEROP Y)
                 (EQUAL 0 (TIMES Y 0))),

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

        T.

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

  which simplifies, unfolding ZEROP, TIMES, PLUS, and EQUAL, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-COMM


(DEFN FOLDR-TIMES
      (LST R)
      (IF (LISTP LST)
          (TIMES (CAR LST)
                 (FOLDR-TIMES (CDR LST) R))
          R))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, FOLDR-TIMES is accepted under the definitional
principle.  From the definition we can conclude that:
      (OR (NUMBERP (FOLDR-TIMES LST R))
          (EQUAL (FOLDR-TIMES LST R) R))
is a theorem.




[ 0.0 0.0 0.0 ]

FOLDR-TIMES


(DEFN FOLDL-TIMES
      (LST R)
      (IF (LISTP LST)
          (FOLDL-TIMES (CDR LST)
                       (TIMES R (CAR LST)))
          R))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, FOLDL-TIMES is accepted under the definitional
principle.  From the definition we can conclude that:
      (OR (NUMBERP (FOLDL-TIMES LST R))
          (EQUAL (FOLDL-TIMES LST R) R))
is a theorem.




[ 0.0 0.0 0.0 ]

FOLDL-TIMES


(FUNCTIONALLY-INSTANTIATE FOLDL-TIMES-IS-FOLDR-TIMES
                          (REWRITE)
                          (EQUAL (FOLDR-TIMES LST R)
                                 (FOLDL-TIMES (REVERSE LST) R))
                          FOLDL-IS-FOLDR
                          ((FOLDR-FN FOLDR-TIMES)
                           (FOLDL-FN FOLDL-TIMES)
                           (FN2 TIMES)))


The functional instantiation of FOLDL-IS-FOLDR under:
      ((FOLDR-FN FOLDR-TIMES)
       (FOLDL-FN FOLDL-TIMES)
       (FN2 TIMES))
requires us to prove:
      (AND (EQUAL (FOLDL-TIMES LST R)
                  (IF (LISTP LST)
                      (FOLDL-TIMES (CDR LST)
                                   (TIMES R (CAR LST)))
                      R))
           (EQUAL (FOLDR-TIMES LST R)
                  (IF (LISTP LST)
                      (TIMES (CAR LST)
                             (FOLDR-TIMES (CDR LST) R))
                      R))
           (EQUAL (TIMES X Y) (TIMES Y X))).



This formula can be simplified, using the abbreviation AND, to the following
three new conjectures:

Case 3. (EQUAL (FOLDL-TIMES LST R)
               (IF (LISTP LST)
                   (FOLDL-TIMES (CDR LST)
                                (TIMES R (CAR LST)))
                   R)).

  This simplifies, unfolding the function FOLDL-TIMES, to:

        T.

Case 2. (EQUAL (FOLDR-TIMES LST R)
               (IF (LISTP LST)
                   (TIMES (CAR LST)
                          (FOLDR-TIMES (CDR LST) R))
                   R)).

  This simplifies, opening up the function FOLDR-TIMES, to:

        T.

Case 1. (EQUAL (TIMES X Y) (TIMES Y X)).

  This simplifies, rewriting with TIMES-COMM, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FOLDL-TIMES-IS-FOLDR-TIMES