(NOTE-LIB "naturals" T)
Loading ./numbers/naturals.lib
Finished loading ./numbers/naturals.lib
Loading ./numbers/naturals.o
Finished loading ./numbers/naturals.o
(#./numbers/naturals.lib #./numbers/naturals)
(CONSTRAIN FN-INTRO
(REWRITE)
(AND (EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NUMBERP (Q))
(NOT (EQUAL 0 (Q)))
(NUMBERP (FN X))
(IMPLIES (AND (LESSP 0 P) (LESSP P (Q)))
(EQUAL (TIMES 2 (FN P))
(PLUS (FN (SUB1 P)) (FN (ADD1 P))))))
((Q (LAMBDA NIL 1)) (FN FIX)))
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed FN-INTRO could!
WARNING: Note that the proposed lemma FN-INTRO is to be stored as two type
prescription rules, zero compound recognizer rules, zero linear rules, and
four replacement rules.
We will verify the consistency and the conservative nature of this constraint
by attempting to prove:
(AND (EQUAL (FIX 0) 0)
(EQUAL (FIX 1) 1)
(NUMBERP 1)
(NOT (EQUAL 0 1))
(NUMBERP (FIX X))
(IMPLIES (AND (LESSP 0 P) (LESSP P 1))
(EQUAL (TIMES 2 (FIX P))
(PLUS (FIX (SUB1 P))
(FIX (ADD1 P)))))).
This formula can be simplified, using the abbreviations IMPLIES, NOT, and AND,
to the following six new formulas:
Case 6. (EQUAL (FIX 0) 0).
This simplifies, expanding the functions FIX and EQUAL, to:
T.
Case 5. (EQUAL (FIX 1) 1).
This simplifies, expanding the definitions of FIX and EQUAL, to:
T.
Case 4. (NUMBERP 1).
This simplifies, trivially, to:
T.
Case 3. (NOT (EQUAL 0 1)).
This simplifies, using linear arithmetic, to:
T.
Case 2. (NUMBERP (FIX X)).
This simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (LESSP 0 P) (LESSP P 1))
(EQUAL (TIMES 2 (FIX P))
(PLUS (FIX (SUB1 P))
(FIX (ADD1 P))))).
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FN-INTRO
(DEFN MY-INDUCTION
(P)
(IF (OR (ZEROP P) (EQUAL P 1))
T
(AND (MY-INDUCTION (SUB1 P))
(MY-INDUCTION (SUB1 (SUB1 P))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of OR and
ZEROP can be used to establish that the measure (COUNT P) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
MY-INDUCTION is accepted under the principle of definition. Note that
(TRUEP (MY-INDUCTION P)) is a theorem.
[ 0.0 0.0 0.0 ]
MY-INDUCTION
(PROVE-LEMMA MAIN-INDUCTIVE-CASE
(REWRITE)
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(EQUAL (FN (SUB1 (SUB1 P)))
(TIMES (FN 1) (SUB1 (SUB1 P))))
(EQUAL (FN (SUB1 P))
(TIMES (FN 1) (SUB1 P)))
(NOT (LESSP (Q) P)))
(EQUAL (EQUAL (FN P) (TIMES (FN 1) P))
T))
((USE (FN-INTRO (P (SUB1 P))))
(DISABLE FN-INTRO)))
This simplifies, appealing to the lemmas EQUAL-SUB1-0, TIMES-1-ARG1, ADD1-SUB1,
and COMMUTATIVITY-OF-PLUS, and unfolding the functions EQUAL, LESSP, AND, SUB1,
NUMBERP, TIMES, and IMPLIES, to the following two new formulas:
Case 2. (IMPLIES (AND (EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NOT (EQUAL 0 (Q)))
(NOT (LESSP (SUB1 P) (Q)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(EQUAL (FN (SUB1 (SUB1 P)))
(TIMES (FN 1) (SUB1 (SUB1 P))))
(EQUAL (FN (SUB1 P))
(TIMES (FN 1) (SUB1 P)))
(NOT (LESSP (Q) P)))
(EQUAL (FN P) (TIMES (FN 1) P))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NOT (EQUAL 0 (Q)))
(EQUAL (PLUS (FN (SUB1 P)) (FN (SUB1 P)))
(PLUS (FN P) (FN (SUB1 (SUB1 P)))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(EQUAL (FN (SUB1 (SUB1 P)))
(TIMES (FN 1) (SUB1 (SUB1 P))))
(EQUAL (FN (SUB1 P))
(TIMES (FN 1) (SUB1 P)))
(NOT (LESSP (Q) P)))
(EQUAL (FN P) (TIMES (FN 1) P))).
Applying the lemma SUB1-ELIM, replace P by (ADD1 Z) to eliminate (SUB1 P)
and Z by (ADD1 V) to eliminate (SUB1 Z). We rely upon the type restriction
lemma noted when SUB1 was introduced to restrict the new variable. This
produces the following two new conjectures:
Case 1.2.
(IMPLIES (AND (EQUAL Z 0)
(NUMBERP Z)
(EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NOT (EQUAL 0 (Q)))
(EQUAL (PLUS (FN Z) (FN Z))
(PLUS (FN (ADD1 Z)) (FN (SUB1 Z))))
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL (ADD1 Z) 1))
(EQUAL (FN (SUB1 Z))
(TIMES (FN 1) (SUB1 Z)))
(EQUAL (FN Z) (TIMES (FN 1) Z))
(NOT (LESSP (Q) (ADD1 Z))))
(EQUAL (FN (ADD1 Z))
(TIMES (FN 1) (ADD1 Z)))).
This further simplifies, trivially, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP V)
(NOT (EQUAL (ADD1 V) 0))
(EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NOT (EQUAL 0 (Q)))
(EQUAL (PLUS (FN (ADD1 V)) (FN (ADD1 V)))
(PLUS (FN (ADD1 (ADD1 V))) (FN V)))
(NOT (EQUAL (ADD1 (ADD1 V)) 0))
(NOT (EQUAL (ADD1 (ADD1 V)) 1))
(EQUAL (FN V) (TIMES (FN 1) V))
(EQUAL (FN (ADD1 V))
(TIMES (FN 1) (ADD1 V)))
(NOT (LESSP (Q) (ADD1 (ADD1 V)))))
(EQUAL (FN (ADD1 (ADD1 V)))
(TIMES (FN 1) (ADD1 (ADD1 V))))).
But this further simplifies, applying COMMUTATIVITY-OF-PLUS, ADD1-EQUAL,
TIMES-ADD1, SUB1-ADD1, and EQUAL-SUB1-0, and unfolding the definitions of
NUMBERP and LESSP, to:
(IMPLIES (AND (NUMBERP V)
(EQUAL (FN 0) 0)
(EQUAL (FN (Q)) (Q))
(NOT (EQUAL 0 (Q)))
(EQUAL (PLUS (FN (ADD1 V)) (FN (ADD1 V)))
(PLUS (FN V) (FN (ADD1 (ADD1 V)))))
(EQUAL (FN V) (TIMES (FN 1) V))
(EQUAL (FN (ADD1 V))
(PLUS (FN 1) (FN V)))
(NOT (EQUAL (Q) 1))
(NOT (LESSP (SUB1 (SUB1 (Q))) V)))
(EQUAL (FN (ADD1 (ADD1 V)))
(PLUS (FN 1) (FN (ADD1 V))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
MAIN-INDUCTIVE-CASE
(PROVE-LEMMA MAIN NIL
(IMPLIES (AND (NUMBERP P)
(LEQ 0 P)
(LEQ P (Q)))
(EQUAL (TIMES P (FN 1)) (FN P)))
((INDUCT (MY-INDUCTION P))))
This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to the following two new conjectures:
Case 2. (IMPLIES (AND (OR (ZEROP P) (EQUAL P 1))
(NUMBERP P)
(NOT (LESSP P 0))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES P (FN 1)) (FN P))).
This simplifies, applying FN-INTRO and TIMES-1-ARG1, and expanding ZEROP, OR,
NUMBERP, LESSP, EQUAL, and TIMES, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(IMPLIES (AND (NUMBERP (SUB1 (SUB1 P)))
(IF (LESSP (SUB1 (SUB1 P)) 0) F T)
(IF (LESSP (Q) (SUB1 (SUB1 P))) F T))
(EQUAL (TIMES (SUB1 (SUB1 P)) (FN 1))
(FN (SUB1 (SUB1 P)))))
(IMPLIES (AND (NUMBERP (SUB1 P))
(IF (LESSP (SUB1 P) 0) F T)
(IF (LESSP (Q) (SUB1 P)) F T))
(EQUAL (TIMES (SUB1 P) (FN 1))
(FN (SUB1 P))))
(NOT (LESSP P 0))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES P (FN 1)) (FN P))),
which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
MAIN-INDUCTIVE-CASE, and unfolding the definitions of EQUAL, LESSP, AND, and
IMPLIES, to three new goals:
Case 1.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(LESSP (Q) (SUB1 (SUB1 P)))
(LESSP (Q) (SUB1 P))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES (FN 1) P) (FN P))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(LESSP (Q) (SUB1 (SUB1 P)))
(EQUAL (TIMES (FN 1) (SUB1 P))
(FN (SUB1 P)))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES (FN 1) P) (FN P))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (SUB1 P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(LESSP (Q) (SUB1 (SUB1 P)))
(EQUAL (TIMES (FN 1) (SUB1 P))
(FN (SUB1 P)))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES (FN 1) P) (FN P))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(EQUAL (TIMES (FN 1) (SUB1 (SUB1 P)))
(FN (SUB1 (SUB1 P))))
(LESSP (Q) (SUB1 P))
(NOT (LESSP (Q) P)))
(EQUAL (TIMES (FN 1) P) (FN P))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
MAIN
(PROVE-LEMMA HELPER
(REWRITE)
(EQUAL (FN 1) 1)
((USE (MAIN (P (Q))))))
This conjecture can be simplified, using the abbreviation FN-INTRO, to:
(IMPLIES (IMPLIES (AND (NUMBERP (Q))
(IF (LESSP (Q) 0) F T)
(IF (LESSP (Q) (Q)) F T))
(EQUAL (TIMES (Q) (FN 1)) (Q)))
(EQUAL (FN 1) 1)).
This simplifies, appealing to the lemmas FN-INTRO and EQUAL-TIMES-X-X, and
expanding EQUAL, LESSP, AND, and IMPLIES, to the new goal:
(IMPLIES (LESSP (Q) (Q))
(EQUAL (FN 1) 1)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
HELPER
(PROVE-LEMMA FINAL-THEOREM NIL
(IMPLIES (AND (NUMBERP P)
(LEQ 0 P)
(LEQ P (Q)))
(EQUAL (FN P) P))
((USE (MAIN))))
This formula can be simplified, using the abbreviations AND, IMPLIES, and
HELPER, to the new conjecture:
(IMPLIES (AND (IMPLIES (AND (NUMBERP P)
(IF (LESSP P 0) F T)
(IF (LESSP (Q) P) F T))
(EQUAL (TIMES P 1) (FN P)))
(NUMBERP P)
(NOT (LESSP P 0))
(NOT (LESSP (Q) P)))
(EQUAL (FN P) P)),
which simplifies, applying TIMES-1-ARG1 and COMMUTATIVITY-OF-TIMES, and
expanding the definitions of EQUAL, LESSP, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FINAL-THEOREM