(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(DEFN ORDP
(P)
(AND (LISTP P)
(NUMBERP (CAR P))
(NUMBERP (CDR P))))
Observe that (OR (FALSEP (ORDP P)) (TRUEP (ORDP P))) is a theorem.
[ 0.0 0.0 0.0 ]
ORDP
(DEFN LEXP
(P1 P2)
(OR (LESSP (CAR P1) (CAR P2))
(AND (EQUAL (CAR P1) (CAR P2))
(LESSP (CDR P1) (CDR P2)))))
Note that (OR (FALSEP (LEXP P1 P2)) (TRUEP (LEXP P1 P2))) is a theorem.
[ 0.0 0.0 0.0 ]
LEXP
(DCL Q (P))
[ 0.0 0.0 0.0 ]
Q
(DCL G (P))
[ 0.0 0.0 0.0 ]
G
(ADD-AXIOM Q-INDUCTION
(REWRITE)
(IMPLIES (AND (ORDP P) (NOT (Q P)))
(AND (ORDP (G P))
(LEXP (G P) P)
(NOT (Q (G P))))))
WARNING: Note that the rewrite rule Q-INDUCTION will be stored so as to apply
only to terms with the nonrecursive function symbol ORDP.
WARNING: Note that the rewrite rule Q-INDUCTION will be stored so as to apply
only to terms with the nonrecursive function symbol LEXP.
WARNING: Note that the proposed lemma Q-INDUCTION is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and three replacement rules.
[ 0.0 0.0 0.0 ]
Q-INDUCTION
(DEFN FY
(X Y)
(IF (NOT (NUMBERP Y))
F
(IF (EQUAL Y 0)
(IF (Q (CONS X Y)) F Y)
(IF (FY X (SUB1 Y))
(FY X (SUB1 Y))
(IF (Q (CONS X Y)) F Y)))))
Linear arithmetic and the lemma COUNT-NUMBERP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in each
recursive call. Hence, FY is accepted under the principle of definition.
Observe that (OR (FALSEP (FY X Y)) (NUMBERP (FY X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
FY
(PROVE-LEMMA Q-FAILS-AT-X-FY
(REWRITE)
(IMPLIES (FY X Y)
(NOT (Q (CONS X (FY X Y))))))
Name the conjecture *1.
Let us appeal to the induction principle. 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 (NOT (NUMBERP Y)) (p X Y))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y)))
(p X Y))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y))))
(p X Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(p X (SUB1 Y)))
(p X Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(p X (SUB1 Y)))
(p X Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(NOT (Q (CONS X Y)))
(p X (SUB1 Y)))
(p X Y))).
Linear arithmetic and the lemma COUNT-NUMBERP can be used to show that the
measure (COUNT Y) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to the
following six new goals:
Case 6. (IMPLIES (AND (NOT (NUMBERP Y)) (FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, expanding the definition of FY, to:
T.
Case 5. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y))
(FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, unfolding NUMBERP, EQUAL, and FY, to:
T.
Case 4. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y)))
(FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, unfolding the definitions of NUMBERP, EQUAL, and FY, to:
T.
Case 3. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(NOT (Q (CONS X (FY X (SUB1 Y)))))
(FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, expanding the definition of FY, to:
T.
Case 2. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(Q (CONS X Y))
(NOT (FY X (SUB1 Y)))
(FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, expanding the definition of FY, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (Q (CONS X Y)))
(NOT (FY X (SUB1 Y)))
(FY X Y))
(NOT (Q (CONS X (FY X Y))))).
This simplifies, expanding the function FY, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
Q-FAILS-AT-X-FY
(PROVE-LEMMA FY-IS-A-NUMBER
(REWRITE)
(IMPLIES (FY X Y) (NUMBERP (FY X Y))))
This conjecture simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FY-IS-A-NUMBER
(PROVE-LEMMA FY-IS-DEFINED
(REWRITE)
(IMPLIES (AND (NOT (Q (CONS X Y))) (NUMBERP Y))
(FY X Y)))
This simplifies, opening up the function FY, to the conjecture:
(IMPLIES (AND (NOT (Q (CONS X Y)))
(NUMBERP Y)
(EQUAL Y 0))
(NOT (Q (CONS X 0)))).
This again simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FY-IS-DEFINED
(PROVE-LEMMA FY-LEQ NIL
(IMPLIES (FY X Y) (LEQ (FY X Y) Y)))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP Y)) (p Y X))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y)))
(p Y X))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y))))
(p Y X))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(p (SUB1 Y) X))
(p Y X))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(p (SUB1 Y) X))
(p Y X))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(NOT (Q (CONS X Y)))
(p (SUB1 Y) X))
(p Y X))).
Linear arithmetic and the lemma COUNT-NUMBERP can be used to show 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 six new conjectures:
Case 6. (IMPLIES (AND (NOT (NUMBERP Y)) (FY X Y))
(NOT (LESSP Y (FY X Y)))).
This simplifies, opening up the function FY, to:
T.
Case 5. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y))
(FY X Y))
(NOT (LESSP Y (FY X Y)))).
This simplifies, unfolding the functions NUMBERP, EQUAL, and FY, to:
T.
Case 4. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y)))
(FY X Y))
(NOT (LESSP Y (FY X Y)))).
This simplifies, applying FY-IS-DEFINED, and unfolding the functions NUMBERP,
EQUAL, FY, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(NOT (LESSP (SUB1 Y) (FY X (SUB1 Y))))
(FY X Y))
(NOT (LESSP Y (FY X Y)))),
which simplifies, unfolding the definition of FY, to the goal:
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(NOT (LESSP (SUB1 Y) (FY X (SUB1 Y)))))
(NOT (LESSP Y (FY X (SUB1 Y))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(Q (CONS X Y))
(NOT (FY X (SUB1 Y)))
(FY X Y))
(NOT (LESSP Y (FY X Y)))),
which simplifies, expanding the function FY, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (Q (CONS X Y)))
(NOT (FY X (SUB1 Y)))
(FY X Y))
(NOT (LESSP Y (FY X Y)))),
which simplifies, applying FY-IS-DEFINED, and expanding the definitions of
FY and LESSP, to:
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (Q (CONS X Y)))
(NOT (FY X (SUB1 Y))))
(NOT (LESSP (SUB1 Y) (SUB1 Y)))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FY-LEQ
(PROVE-LEMMA FY-LESSP
(REWRITE)
(IMPLIES (AND (FY X Y) (Q (CONS X Y)))
(LESSP (FY X Y) Y))
((DO-NOT-INDUCT T)
(USE (FY-LEQ) (Q-FAILS-AT-X-FY))
(DISABLE Q-FAILS-AT-X-FY)))
WARNING: Note that the proposed lemma FY-LESSP is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
This simplifies, using linear arithmetic, to the following two new conjectures:
Case 2. (IMPLIES (AND (NOT (NUMBERP Y))
(NOT (LESSP Y (FY X Y)))
(NOT (Q (CONS X (FY X Y))))
(FY X Y)
(Q (CONS X Y)))
(LESSP (FY X Y) Y)).
However this again simplifies, unfolding FY, NUMBERP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Y)
(EQUAL (FY X Y) Y)
(NOT (LESSP Y Y))
(NOT (Q (CONS X Y)))
Y
(Q (CONS X Y)))
(LESSP Y Y)),
which again simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FY-LESSP
(PROVE-LEMMA Q-BELOW-UNDEFINED-FY
(REWRITE)
(IMPLIES (AND (NOT (FY X Y))
(NUMBERP Y)
(NUMBERP Y1)
(LEQ Y1 Y))
(Q (CONS X Y1)))
((INDUCT (FY X Y))))
WARNING: Note that Q-BELOW-UNDEFINED-FY contains the free variable Y which
will be chosen by instantiating the hypothesis (NOT (FY X Y)).
This formula can be simplified, using the abbreviations NOT, IMPLIES, OR, and
AND, to the following six new conjectures:
Case 6. T.
This simplifies, clearly, to:
T.
Case 5. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y))
(NOT (FY X Y))
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))).
This simplifies, unfolding the definitions of NUMBERP, EQUAL, FY, and LESSP,
to:
T.
Case 4. (IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y)))
(NOT (FY X Y))
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))).
This simplifies, rewriting with FY-IS-DEFINED, and expanding the definition
of NUMBERP, to:
T.
Case 3. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(IMPLIES (AND (NOT (FY X (SUB1 Y)))
(NUMBERP (SUB1 Y))
(NUMBERP Y1)
(IF (LESSP (SUB1 Y) Y1) F T))
(Q (CONS X Y1)))
(NOT (FY X Y))
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))),
which simplifies, expanding the functions NOT, AND, IMPLIES, and FY, to:
T.
Case 2. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(IMPLIES (AND (NOT (FY X (SUB1 Y)))
(NUMBERP (SUB1 Y))
(NUMBERP Y1)
(IF (LESSP (SUB1 Y) Y1) F T))
(Q (CONS X Y1)))
(NOT (FY X Y))
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))),
which simplifies, unfolding NOT, AND, IMPLIES, and FY, to the conjecture:
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(LESSP (SUB1 Y) Y1)
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))).
This again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(LESSP (SUB1 Y) Y)
(NUMBERP Y)
(NOT (LESSP Y Y)))
(Q (CONS X Y))).
This again simplifies, clearly, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(NOT (Q (CONS X Y)))
(IMPLIES (AND (NOT (FY X (SUB1 Y)))
(NUMBERP (SUB1 Y))
(NUMBERP Y1)
(IF (LESSP (SUB1 Y) Y1) F T))
(Q (CONS X Y1)))
(NOT (FY X Y))
(NUMBERP Y1)
(NOT (LESSP Y Y1)))
(Q (CONS X Y1))).
This simplifies, applying the lemma FY-IS-DEFINED, and expanding the
definitions of NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
Q-BELOW-UNDEFINED-FY
(PROVE-LEMMA FY-IS-FIRST
(REWRITE)
(IMPLIES (AND (FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))))
WARNING: Note that FY-IS-FIRST contains the free variable Y which will be
chosen by instantiating the hypothesis (FY X Y).
Name the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest three inductions. They merge into two likely candidate
inductions, both of which are unflawed. However, one of these is more likely
than the other. We will induct according to the following scheme:
(AND (IMPLIES (NOT (NUMBERP Y)) (p X Y1 Y))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(Q (CONS X Y)))
(p X Y1 Y))
(IMPLIES (AND (NUMBERP Y)
(EQUAL Y 0)
(NOT (Q (CONS X Y))))
(p X Y1 Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(p X Y1 (SUB1 Y)))
(p X Y1 Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(Q (CONS X Y))
(p X Y1 (SUB1 Y)))
(p X Y1 Y))
(IMPLIES (AND (NUMBERP Y)
(NOT (EQUAL Y 0))
(NOT (FY X (SUB1 Y)))
(NOT (Q (CONS X Y)))
(p X Y1 (SUB1 Y)))
(p X Y1 Y))).
Linear arithmetic and the lemma COUNT-NUMBERP 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 the
following five new conjectures:
Case 5. (IMPLIES (AND (EQUAL Y 0)
(Q (CONS X Y))
(FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))).
This simplifies, using linear arithmetic, applying FY-LESSP, and opening up
the definitions of FY, NUMBERP, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (EQUAL Y 0)
(NOT (Q (CONS X Y)))
(FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))),
which simplifies, appealing to the lemma FY-IS-DEFINED, and unfolding
NUMBERP, EQUAL, FY, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL Y 0))
(FY X (SUB1 Y))
(NOT (LESSP Y1 (FY X (SUB1 Y))))
(FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))),
which simplifies, unfolding FY, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL Y 0))
(Q (CONS X Y))
(NOT (FY X (SUB1 Y)))
(FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))),
which simplifies, unfolding FY, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL Y 0))
(NOT (Q (CONS X Y)))
(NOT (FY X (SUB1 Y)))
(FY X Y)
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 (FY X Y)))
(Q (CONS X Y1))),
which simplifies, rewriting with the lemma FY-IS-DEFINED, and expanding FY,
to the goal:
(IMPLIES (AND (NOT (EQUAL Y 0))
(NOT (Q (CONS X Y)))
(NOT (FY X (SUB1 Y)))
(NUMBERP Y1)
(NUMBERP Y)
(LESSP Y1 Y))
(Q (CONS X Y1))).
This again simplifies, using linear arithmetic and rewriting with
Q-BELOW-UNDEFINED-FY, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
FY-IS-FIRST
(PROVE-LEMMA FORM-OF-G NIL
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y)))
(EQUAL X1 (CAR (G (CONS X Y))))
(EQUAL Y1 (CDR (G (CONS X Y)))))
(AND (NUMBERP X1)
(NUMBERP Y1)
(EQUAL (G (CONS X Y)) (CONS X1 Y1))))
((USE (Q-INDUCTION (P (CONS X Y))))
(DISABLE Q-INDUCTION)))
This simplifies, rewriting with CDR-CONS, CAR-CONS, and CONS-CAR-CDR, and
opening up ORDP, NOT, AND, LEXP, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FORM-OF-G
(PROVE-LEMMA G-IS-BELOW
(REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y)))
(EQUAL X1 (CAR (G (CONS X Y))))
(EQUAL Y1 (CDR (G (CONS X Y)))))
(OR (LESSP X1 X)
(AND (EQUAL X1 X) (LESSP Y1 Y))))
((USE (Q-INDUCTION (P (CONS X Y))))
(DISABLE Q-INDUCTION)))
WARNING: Note that the rewrite rule G-IS-BELOW will be stored so as to apply
only to terms with the nonrecursive function symbol OR.
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up ORDP,
NOT, AND, LEXP, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
G-IS-BELOW
(PROVE-LEMMA Q-FAILS-AT-G-AUX1
(REWRITE)
(IMPLIES (AND (NOT (Q (G (CONS X Y))))
(EQUAL (G (CONS X Y)) (CONS X1 Y1)))
(NOT (Q (CONS X1 Y1)))))
WARNING: Note that Q-FAILS-AT-G-AUX1 contains the free variables Y and X
which will be chosen by instantiating the hypothesis (NOT (Q (G (CONS X Y)))).
This conjecture simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
Q-FAILS-AT-G-AUX1
(PROVE-LEMMA Q-FAILS-AT-G
(REWRITE)
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y)))
(EQUAL X1 (CAR (G (CONS X Y))))
(EQUAL Y1 (CDR (G (CONS X Y)))))
(NOT (Q (CONS X1 Y1))))
((USE (FORM-OF-G)
(Q-INDUCTION (P (CONS X Y))))
(DISABLE Q-INDUCTION)))
WARNING: Note that Q-FAILS-AT-G contains the free variables Y and X which
will be chosen by instantiating the hypotheses (NUMBERP X) and (NUMBERP Y).
This simplifies, applying CONS-CAR-CDR, CDR-CONS, CAR-CONS, and
Q-FAILS-AT-G-AUX1, and unfolding NOT, AND, IMPLIES, ORDP, CDR, LESSP, EQUAL,
CAR, LEXP, and CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
Q-FAILS-AT-G
(DISABLE Q-FAILS-AT-G-AUX1)
[ 0.0 0.0 0.0 ]
Q-FAILS-AT-G-AUX1-OFF
(PROVE-LEMMA SMALLER-X NIL
(IMPLIES (AND (NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y)))
(EQUAL X1 (CAR (G (CONS X (FY X Y)))))
(EQUAL Y1
(CDR (G (CONS X (FY X Y))))))
(AND (NUMBERP X1)
(NUMBERP Y1)
(LESSP X1 X)
(NOT (Q (CONS X1 Y1)))))
((DO-NOT-INDUCT T)
(USE (FY-IS-DEFINED)
(Q-FAILS-AT-X-FY)
(FORM-OF-G (X X) (Y (FY X Y)))
(G-IS-BELOW (X X) (Y (FY X Y)))
(Q-FAILS-AT-G (X X) (Y (FY X Y))))
(DISABLE FY Q-INDUCTION G-IS-BELOW Q-FAILS-AT-G FY-IS-DEFINED
Q-FAILS-AT-X-FY)))
This conjecture simplifies, using linear arithmetic, rewriting with
CONS-CAR-CDR, Q-BELOW-UNDEFINED-FY, CAR-NLISTP, CDR-NLISTP, and FY-IS-FIRST,
and expanding NOT, AND, IMPLIES, CAR, EQUAL, CDR, LESSP, OR, CONS, and NUMBERP,
to the following four new conjectures:
Case 4. (IMPLIES (AND (FY X Y)
(NOT (Q (CONS X (FY X Y))))
(NUMBERP (CAR (G (CONS X (FY X Y)))))
(NUMBERP (CDR (G (CONS X (FY X Y)))))
(EQUAL (G (CONS X (FY X Y)))
'(0 . 0))
(EQUAL 0 X)
(NOT (EQUAL (FY X Y) 0))
(Q (CONS 0 (FY 0 Y)))
(NUMBERP Y))
(Q (CONS 0 Y))).
This again simplifies, trivially, to:
T.
Case 3. (IMPLIES (AND (FY X Y)
(NOT (Q (CONS X (FY X Y))))
(NUMBERP (CAR (G (CONS X (FY X Y)))))
(NUMBERP (CDR (G (CONS X (FY X Y)))))
(EQUAL (G (CONS X (FY X Y)))
'(0 . 0))
(EQUAL 0 X)
(NOT (EQUAL (FY X Y) 0))
(NOT (LISTP (G (CONS 0 (FY 0 Y)))))
(NOT (Q '(0 . 0)))
(NUMBERP Y))
(Q (CONS 0 Y))).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (FY X Y)
(NOT (Q (CONS X (FY X Y))))
(NUMBERP (CAR (G (CONS X (FY X Y)))))
(NUMBERP (CDR (G (CONS X (FY X Y)))))
(EQUAL (G (CONS X (FY X Y)))
'(0 . 0))
(EQUAL 0 X)
(NOT (EQUAL (FY X Y) 0))
(LISTP (G (CONS 0 (FY 0 Y))))
(NOT (Q (G (CONS 0 (FY 0 Y)))))
(NUMBERP Y))
(Q (CONS 0 Y))).
However this again simplifies, using linear arithmetic, rewriting with
FY-IS-FIRST, and expanding CAR, NUMBERP, CDR, and LISTP, to:
T.
Case 1. (IMPLIES (AND (FY X Y)
(NOT (Q (CONS X (FY X Y))))
(NUMBERP (CAR (G (CONS X (FY X Y)))))
(NUMBERP (CDR (G (CONS X (FY X Y)))))
(LISTP (G (CONS X (FY X Y))))
(EQUAL (CAR (G (CONS X (FY X Y)))) X)
(LESSP (CDR (G (CONS X (FY X Y))))
(FY X Y))
(NOT (Q (CONS X (CDR (G (CONS X (FY X Y)))))))
(NUMBERP Y))
(Q (CONS X Y))).
However this again simplifies, rewriting with FY-IS-FIRST, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SMALLER-X
(DEFN Q-HOLDS-KLUDGE
(X Y)
(IF (AND (NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y)))
(NUMBERP (CAR (G (CONS X (FY X Y)))))
(LESSP (CAR (G (CONS X (FY X Y)))) X))
(Q-HOLDS-KLUDGE (CAR (G (CONS X (FY X Y))))
(CDR (G (CONS X (FY X Y)))))
0))
The lemma COUNT-NUMBERP and the definitions of AND and NOT inform us that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, Q-HOLDS-KLUDGE is accepted under the principle
of definition. Note that (NUMBERP (Q-HOLDS-KLUDGE X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
Q-HOLDS-KLUDGE
(PROVE-LEMMA Q-HOLDS
(REWRITE)
(IMPLIES (AND (NUMBERP X) (NUMBERP Y))
(Q (CONS X Y)))
((INDUCT (Q-HOLDS-KLUDGE X Y))
(USE (SMALLER-X (X1 (CAR (G (CONS X (FY X Y)))))
(Y1 (CDR (G (CONS X (FY X Y)))))))))
This conjecture simplifies, applying CONS-CAR-CDR, CAR-NLISTP, and CDR-NLISTP,
and opening up the functions NOT, AND, IMPLIES, LESSP, OR, FY, NUMBERP, EQUAL,
and CONS, to:
(IMPLIES (AND (NUMBERP (CAR (G (CONS X (FY X Y)))))
(NUMBERP (CDR (G (CONS X (FY X Y)))))
(LESSP (CAR (G (CONS X (FY X Y)))) X)
(NOT (LISTP (G (CONS X (FY X Y)))))
(NOT (Q '(0 . 0)))
(NUMBERP X)
(NUMBERP Y)
(NOT (Q (CONS X Y))))
(NOT (EQUAL X 0))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
Q-HOLDS
(PROVE-LEMMA Q-IS-TRUE
(REWRITE)
(IMPLIES (ORDP P) (Q P)))
This formula can be simplified, using the abbreviations ORDP and IMPLIES, to:
(IMPLIES (AND (LISTP P)
(NUMBERP (CAR P))
(NUMBERP (CDR P)))
(Q P)).
Applying the lemma CAR-CDR-ELIM, replace P by (CONS X Z) to eliminate (CAR P)
and (CDR P). We thus obtain:
(IMPLIES (AND (NUMBERP X) (NUMBERP Z))
(Q (CONS X Z))),
which simplifies, applying the lemma Q-HOLDS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
Q-IS-TRUE
(DEFN RESET
(X)
(IF X (CONS (CAR X) 0) F))
Observe that (OR (FALSEP (RESET X)) (LISTP (RESET X))) is a theorem.
[ 0.0 0.0 0.0 ]
RESET
(DEFN QVAL
(TERM VA)
(RESET (V&C$ T TERM VA)))
From the definition we can conclude that:
(OR (FALSEP (QVAL TERM VA))
(LISTP (QVAL TERM VA)))
is a theorem.
[ 0.0 0.0 0.0 ]
QVAL
(DEFN QVAL-LIST
(LIST-OF-TERMS VA)
(IF (NLISTP LIST-OF-TERMS)
NIL
(CONS (QVAL (CAR LIST-OF-TERMS) VA)
(QVAL-LIST (CDR LIST-OF-TERMS) VA))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LIST-OF-TERMS)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, QVAL-LIST is accepted under the principle of definition. Note that:
(OR (LITATOM (QVAL-LIST LIST-OF-TERMS VA))
(LISTP (QVAL-LIST LIST-OF-TERMS VA)))
is a theorem.
[ 0.0 0.0 0.0 ]
QVAL-LIST
(PROVE-LEMMA QVAL-LIST-EMPTY
(REWRITE)
(IMPLIES (NLISTP LST)
(EQUAL (QVAL-LIST LST VA) NIL)))
This formula can be simplified, using the abbreviations NLISTP and IMPLIES, to:
(IMPLIES (NOT (LISTP LST))
(EQUAL (QVAL-LIST LST VA) NIL)),
which simplifies, opening up the functions QVAL-LIST and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-LIST-EMPTY
(PROVE-LEMMA QVAL-LIST-NON-EMPTY
(REWRITE)
(IMPLIES (LISTP LST)
(EQUAL (QVAL-LIST LST VA)
(CONS (QVAL (CAR LST) VA)
(QVAL-LIST (CDR LST) VA)))))
This conjecture can be simplified, using the abbreviations IMPLIES and QVAL,
to the goal:
(IMPLIES (LISTP LST)
(EQUAL (QVAL-LIST LST VA)
(CONS (RESET (V&C$ T (CAR LST) VA))
(QVAL-LIST (CDR LST) VA)))).
This simplifies, unfolding QVAL, RESET, and QVAL-LIST, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-LIST-NON-EMPTY
(PROVE-LEMMA SAME-F-MEMBERSHIP NIL
(IFF (MEMBER F (QVAL-LIST LST VA))
(MEMBER F (V&C$ 'LIST LST VA))))
This conjecture simplifies, unfolding the definition of IFF, to two new
conjectures:
Case 2. (IMPLIES (NOT (MEMBER F (QVAL-LIST LST VA)))
(NOT (MEMBER F (V&C$ 'LIST LST VA)))),
which we will name *1.
Case 1. (IMPLIES (MEMBER F (QVAL-LIST LST VA))
(MEMBER F (V&C$ 'LIST LST VA))),
which we would usually 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 consider:
(IFF (MEMBER F (QVAL-LIST LST VA))
(MEMBER F (V&C$ 'LIST LST VA))),
which we named *1 above. We will appeal to induction. There is only one
plausible induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP LST) (p LST VA))
(IMPLIES (AND (NOT (NLISTP LST))
(p (CDR LST) VA))
(p LST VA))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT LST) 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 conjectures:
Case 2. (IMPLIES (NLISTP LST)
(IFF (MEMBER F (QVAL-LIST LST VA))
(MEMBER F (V&C$ 'LIST LST VA)))).
This simplifies, applying QVAL-LIST-EMPTY, and expanding the functions
NLISTP, MEMBER, EQUAL, V&C$, and IFF, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(IFF (MEMBER F (QVAL-LIST (CDR LST) VA))
(MEMBER F
(V&C$ 'LIST (CDR LST) VA))))
(IFF (MEMBER F (QVAL-LIST LST VA))
(MEMBER F (V&C$ 'LIST LST VA)))),
which simplifies, rewriting with QVAL-LIST-NON-EMPTY, CDR-CONS, and CAR-CONS,
and expanding NLISTP, IFF, RESET, QVAL, and MEMBER, to the following three
new formulas:
Case 1.3.
(IMPLIES (AND (LISTP LST)
(NOT (MEMBER F (QVAL-LIST (CDR LST) VA)))
(NOT (MEMBER F (V&C$ 'LIST (CDR LST) VA)))
(V&C$ T (CAR LST) VA))
(NOT (MEMBER F (V&C$ 'LIST LST VA)))).
But this again simplifies, applying CDR-CONS and CAR-CONS, and expanding
the definitions of NLISTP, EQUAL, V&C$, and MEMBER, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP LST)
(NOT (MEMBER F (QVAL-LIST (CDR LST) VA)))
(NOT (MEMBER F (V&C$ 'LIST (CDR LST) VA)))
(NOT (V&C$ T (CAR LST) VA)))
(MEMBER F (V&C$ 'LIST LST VA))).
This again simplifies, applying the lemma CAR-CONS, and unfolding the
definitions of NLISTP, EQUAL, V&C$, and MEMBER, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP LST)
(MEMBER F (QVAL-LIST (CDR LST) VA))
(MEMBER F (V&C$ 'LIST (CDR LST) VA)))
(MEMBER F (V&C$ 'LIST LST VA))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
(CDR LST) and (CAR LST). This produces:
(IMPLIES (AND (MEMBER F (QVAL-LIST X VA))
(MEMBER F (V&C$ 'LIST X VA)))
(MEMBER F
(V&C$ 'LIST (CONS Z X) VA))),
which further simplifies, rewriting with CDR-CONS and CAR-CONS, and
unfolding NLISTP, EQUAL, V&C$, and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SAME-F-MEMBERSHIP
(PROVE-LEMMA SAME-STRIP-CARS NIL
(EQUAL (STRIP-CARS (QVAL-LIST LST VA))
(STRIP-CARS (V&C$ 'LIST LST VA))))
Name 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 (NLISTP LST) (p LST VA))
(IMPLIES (AND (NOT (NLISTP LST))
(p (CDR LST) VA))
(p LST VA))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT LST) 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 LST)
(EQUAL (STRIP-CARS (QVAL-LIST LST VA))
(STRIP-CARS (V&C$ 'LIST LST VA)))).
This simplifies, applying QVAL-LIST-EMPTY, and expanding the functions
NLISTP, STRIP-CARS, EQUAL, and V&C$, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(EQUAL (STRIP-CARS (QVAL-LIST (CDR LST) VA))
(STRIP-CARS (V&C$ 'LIST (CDR LST) VA))))
(EQUAL (STRIP-CARS (QVAL-LIST LST VA))
(STRIP-CARS (V&C$ 'LIST LST VA)))),
which simplifies, rewriting with QVAL-LIST-NON-EMPTY, CDR-CONS, and CAR-CONS,
and opening up the functions NLISTP, RESET, QVAL, and STRIP-CARS, to the
following two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP LST)
(EQUAL (STRIP-CARS (QVAL-LIST (CDR LST) VA))
(STRIP-CARS (V&C$ 'LIST (CDR LST) VA)))
(NOT (V&C$ T (CAR LST) VA)))
(EQUAL (CONS (CAR F)
(STRIP-CARS (QVAL-LIST (CDR LST) VA)))
(STRIP-CARS (V&C$ 'LIST LST VA)))).
But this again simplifies, applying CDR-CONS and CAR-CONS, and opening up
CAR, NLISTP, EQUAL, V&C$, and STRIP-CARS, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP LST)
(EQUAL (STRIP-CARS (QVAL-LIST (CDR LST) VA))
(STRIP-CARS (V&C$ 'LIST (CDR LST) VA)))
(V&C$ T (CAR LST) VA))
(EQUAL (CONS (CAR (CONS (CAR (V&C$ T (CAR LST) VA)) 0))
(STRIP-CARS (QVAL-LIST (CDR LST) VA)))
(STRIP-CARS (V&C$ 'LIST LST VA)))).
This again simplifies, applying the lemmas CAR-CONS and CDR-CONS, and
opening up the functions NLISTP, EQUAL, V&C$, and STRIP-CARS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SAME-STRIP-CARS
(DISABLE QVAL-LIST)
[ 0.0 0.0 0.0 ]
QVAL-LIST-OFF
(PROVE-LEMMA QVAL-LITATOM
(REWRITE)
(IMPLIES (LITATOM TERM)
(EQUAL (QVAL TERM VA)
(CONS (CDR (ASSOC TERM VA)) 0))))
WARNING: Note that the rewrite rule QVAL-LITATOM will be stored so as to
apply only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviations IMPLIES and QVAL, to:
(IMPLIES (LITATOM TERM)
(EQUAL (RESET (V&C$ T TERM VA))
(CONS (CDR (ASSOC TERM VA)) 0))),
which simplifies, rewriting with CAR-CONS, and expanding the functions EQUAL,
V&C$, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-LITATOM
(PROVE-LEMMA QVAL-CONSTANT
(REWRITE)
(IMPLIES (AND (NOT (LITATOM TERM))
(NLISTP TERM))
(EQUAL (QVAL TERM VA) (CONS TERM 0))))
WARNING: Note that the rewrite rule QVAL-CONSTANT will be stored so as to
apply only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviations NLISTP, NOT, AND,
IMPLIES, and QVAL, to the new conjecture:
(IMPLIES (AND (NOT (LITATOM TERM))
(NOT (LISTP TERM)))
(EQUAL (RESET (V&C$ T TERM VA))
(CONS TERM 0))),
which simplifies, applying CAR-CONS, and unfolding the functions NLISTP, EQUAL,
V&C$, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-CONSTANT
(PROVE-LEMMA QVAL-QUOTE
(REWRITE)
(EQUAL (QVAL (LIST 'QUOTE OBJECT) VA)
(CONS OBJECT 0)))
WARNING: Note that the rewrite rule QVAL-QUOTE will be stored so as to apply
only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviation QVAL, to:
(EQUAL (RESET (V&C$ T (LIST 'QUOTE OBJECT) VA))
(CONS OBJECT 0)),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
functions NLISTP, EQUAL, V&C$, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-QUOTE
(PROVE-LEMMA QVAL-IF
(REWRITE)
(EQUAL (QVAL (LIST 'IF TEST THENCASE ELSECASE)
VA)
(IF (QVAL TEST VA)
(IF (CAR (QVAL TEST VA))
(QVAL THENCASE VA)
(QVAL ELSECASE VA))
F)))
WARNING: Note that the rewrite rule QVAL-IF will be stored so as to apply
only to terms with the nonrecursive function symbol QVAL.
This conjecture can be simplified, using the abbreviation QVAL, to:
(EQUAL (RESET (V&C$ T
(LIST 'IF TEST THENCASE ELSECASE)
VA))
(IF (RESET (V&C$ T TEST VA))
(IF (CAR (RESET (V&C$ T TEST VA)))
(RESET (V&C$ T THENCASE VA))
(RESET (V&C$ T ELSECASE VA)))
F)).
This simplifies, rewriting with CDR-CONS, CAR-CONS, and REWRITE-CAR-V&C-APPLY$,
and opening up the functions NLISTP, EQUAL, V&C$, and RESET, to seven new
formulas:
Case 7. (IMPLIES (NOT (V&C$ T TEST VA))
(NOT (V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA))))),
which again simplifies, rewriting with the lemmas REWRITE-V&C-APPLY$ and
CAR-CONS, to:
T.
Case 6. (IMPLIES (AND (V&C$ T TEST VA)
(NOT (CAR (CONS (CAR (V&C$ T TEST VA)) 0)))
(V&C$ T ELSECASE VA))
(V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA)))),
which again simplifies, rewriting with CAR-CONS, REWRITE-V&C-APPLY$, and
CDR-CONS, to:
T.
Case 5. (IMPLIES (AND (NOT (CAR (CONS (CAR (V&C$ T TEST VA)) 0)))
(NOT (V&C$ T ELSECASE VA)))
(NOT (V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA))))).
This again simplifies, appealing to the lemmas CAR-CONS, REWRITE-V&C-APPLY$,
and CDR-CONS, and unfolding the definitions of CONS and CAR, to:
T.
Case 4. (IMPLIES (AND (V&C$ T TEST VA)
(CAR (CONS (CAR (V&C$ T TEST VA)) 0))
(V&C$ T THENCASE VA))
(V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA)))),
which again simplifies, rewriting with CAR-CONS, REWRITE-V&C-APPLY$, and
CDR-CONS, to:
T.
Case 3. (IMPLIES (AND (CAR (CONS (CAR (V&C$ T TEST VA)) 0))
(NOT (V&C$ T THENCASE VA)))
(NOT (V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA))))).
This again simplifies, applying the lemmas CAR-CONS, REWRITE-V&C-APPLY$, and
CDR-CONS, to:
T.
Case 2. (IMPLIES (AND (CAR (CONS (CAR (V&C$ T TEST VA)) 0))
(V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA)))
(NOT (CAR (V&C$ T TEST VA))))
(EQUAL (CONS (CAR (V&C$ T ELSECASE VA)) 0)
(CONS (CAR (V&C$ T THENCASE VA)) 0))),
which again simplifies, unfolding CONS and CAR, to:
T.
Case 1. (IMPLIES (AND (NOT (CAR (CONS (CAR (V&C$ T TEST VA)) 0)))
(V&C-APPLY$ 'IF
(LIST (V&C$ T TEST VA)
(V&C$ T THENCASE VA)
(V&C$ T ELSECASE VA)))
(CAR (V&C$ T TEST VA)))
(EQUAL (CONS (CAR (V&C$ T THENCASE VA)) 0)
(CONS (CAR (V&C$ T ELSECASE VA)) 0))),
which again simplifies, applying CAR-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-IF
(PROVE-LEMMA QVAL-ARGS-DONT-HALT-AUX1 NIL
(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(MEMBER F (V&C$ 'LIST ARGS VA)))
(EQUAL (V&C$ T (CONS FN ARGS) VA) F))
((USE (V&C-APPLY$ (FN FN)
(ARGS (V&C$ 'LIST ARGS VA))))))
This conjecture simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
unfolding the definitions of MEMBER, STRIP-CARS, SUM-CDRS, EQUAL, NLISTP, and
V&C$, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ARGS-DONT-HALT-AUX1
(PROVE-LEMMA QVAL-ARGS-DONT-HALT
(REWRITE)
(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(MEMBER F (QVAL-LIST ARGS VA)))
(EQUAL (QVAL (CONS FN ARGS) VA) F))
((USE (QVAL-ARGS-DONT-HALT-AUX1)
(SAME-F-MEMBERSHIP (VA VA)
(LST ARGS)))))
WARNING: Note that the rewrite rule QVAL-ARGS-DONT-HALT will be stored so as
to apply only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and
QVAL, to the new goal:
(IMPLIES (AND (IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(MEMBER F (V&C$ 'LIST ARGS VA)))
(EQUAL (V&C$ T (CONS FN ARGS) VA) F))
(IFF (MEMBER F (QVAL-LIST ARGS VA))
(MEMBER F (V&C$ 'LIST ARGS VA)))
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(MEMBER F (QVAL-LIST ARGS VA)))
(EQUAL (RESET (V&C$ T (CONS FN ARGS) VA))
F)),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding the
functions NOT, AND, NLISTP, EQUAL, V&C$, IMPLIES, IFF, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-ARGS-DONT-HALT
(PROVE-LEMMA QVAL-SUBR-AUX1 NIL
(IMPLIES (AND (NOT (MEMBER F (V&C$ 'LIST ARGS VA)))
(NOT (EQUAL FN 'IF))
(SUBRP FN))
(EQUAL (V&C$ T (CONS FN ARGS) VA)
(CONS (APPLY-SUBR FN
(STRIP-CARS (V&C$ 'LIST ARGS VA)))
(ADD1 (SUM-CDRS (V&C$ 'LIST ARGS VA))))))
((USE (V&C-APPLY$ (FN FN)
(ARGS (V&C$ 'LIST ARGS VA))))))
This simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and opening up
the definitions of MEMBER, STRIP-CARS, SUM-CDRS, EQUAL, NLISTP, V&C$, and ADD1,
to the following three new goals:
Case 3. (IMPLIES
(AND
(LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(LISTP (CDR (V&C$ 'LIST ARGS VA)))
(CADR (V&C$ 'LIST ARGS VA))
(NOT (MEMBER F
(CDDR (V&C$ 'LIST ARGS VA))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(CONS
(APPLY-SUBR FN
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA))))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
(CDADR (V&C$ 'LIST ARGS VA))
(SUM-CDRS (CDDR (V&C$ 'LIST ARGS VA)))))))
(NOT (EQUAL FN 'IF))
(SUBRP FN)
(EQUAL FN 'QUOTE))
(EQUAL (CONS (CAR ARGS) 0)
(V&C-APPLY$ FN
(V&C$ 'LIST ARGS VA)))).
But this again simplifies, applying REWRITE-APPLY-SUBR, and expanding the
functions EQUAL and SUBRP, to:
T.
Case 2. (IMPLIES
(AND (LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(NOT (LISTP (CDR (V&C$ 'LIST ARGS VA))))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(CONS (APPLY-SUBR FN
(LIST (CAAR (V&C$ 'LIST ARGS VA))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
0))))
(NOT (EQUAL FN 'IF))
(SUBRP FN)
(EQUAL FN 'QUOTE))
(EQUAL (CONS (CAR ARGS) 0)
(V&C-APPLY$ FN
(V&C$ 'LIST ARGS VA)))).
However this again simplifies, applying REWRITE-APPLY-SUBR, and opening up
EQUAL and SUBRP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP (V&C$ 'LIST ARGS VA)))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(CONS (APPLY-SUBR FN NIL) 1))
(NOT (EQUAL FN 'IF))
(SUBRP FN)
(EQUAL FN 'QUOTE))
(EQUAL (CONS (CAR ARGS) 0)
(CONS (APPLY-SUBR FN NIL) 1))).
But this again simplifies, expanding APPLY-SUBR, CONS, EQUAL, and SUBRP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-SUBR-AUX1
(PROVE-LEMMA QVAL-SUBR-AUX2
(REWRITE)
(IMPLIES (AND (EQUAL VVV (CONS UU ANYTHING))
A B C D E)
(EQUAL (CAR VVV) UU)))
WARNING: Note that QVAL-SUBR-AUX2 contains the free variables E, D, C, B, A,
ANYTHING, and UU which will be chosen by instantiating the hypotheses:
(EQUAL VVV (CONS UU ANYTHING))
A, B, C, D, and E.
This simplifies, rewriting with CAR-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-SUBR-AUX2
(PROVE-LEMMA QVAL-SUBR
(REWRITE)
(IMPLIES (AND (NOT (MEMBER F (QVAL-LIST ARGS VA)))
(NOT (EQUAL FN 'IF))
(SUBRP FN))
(EQUAL (QVAL (CONS FN ARGS) VA)
(CONS (APPLY-SUBR FN
(STRIP-CARS (QVAL-LIST ARGS VA)))
0)))
((USE (QVAL-SUBR-AUX1)
(SAME-F-MEMBERSHIP (VA VA) (LST ARGS))
(SAME-STRIP-CARS (VA VA) (LST ARGS)))
(DO-NOT-INDUCT T)
(DISABLE V&C$ SUBRP)
(HANDS-OFF V&C$ SUBRP)))
WARNING: Note that the rewrite rule QVAL-SUBR will be stored so as to apply
only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and
QVAL, to:
(IMPLIES
(AND
(IMPLIES (AND (NOT (MEMBER F (V&C$ 'LIST ARGS VA)))
(NOT (EQUAL FN 'IF))
(SUBRP FN))
(EQUAL (V&C$ T (CONS FN ARGS) VA)
(CONS (APPLY-SUBR FN
(STRIP-CARS (V&C$ 'LIST ARGS VA)))
(ADD1 (SUM-CDRS (V&C$ 'LIST ARGS VA))))))
(IFF (MEMBER F (QVAL-LIST ARGS VA))
(MEMBER F (V&C$ 'LIST ARGS VA)))
(EQUAL (STRIP-CARS (QVAL-LIST ARGS VA))
(STRIP-CARS (V&C$ 'LIST ARGS VA)))
(NOT (MEMBER F (QVAL-LIST ARGS VA)))
(NOT (EQUAL FN 'IF))
(SUBRP FN))
(EQUAL (RESET (V&C$ T (CONS FN ARGS) VA))
(CONS (APPLY-SUBR FN
(STRIP-CARS (QVAL-LIST ARGS VA)))
0))),
which simplifies, rewriting with QVAL-SUBR-AUX2, and opening up the functions
NOT, AND, IMPLIES, IFF, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-SUBR
(DISABLE QVAL-SUBR-AUX2)
[ 0.0 0.0 0.0 ]
QVAL-SUBR-AUX2-OFF
(PROVE-LEMMA QVAL-NON-SUBR-AUX1 NIL
(IMPLIES (AND (NOT (EQUAL FN 'QUOTE))
(NOT (MEMBER F (V&C$ 'LIST ARGS VA)))
(NOT (SUBRP FN)))
(EQUAL (V&C$ T (CONS FN ARGS) VA)
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(STRIP-CARS (V&C$ 'LIST ARGS VA))))
(ADD1 (SUM-CDRS (V&C$ 'LIST ARGS VA))))))
((USE (V&C-APPLY$ (FN FN)
(ARGS (V&C$ 'LIST ARGS VA))))))
This conjecture simplifies, rewriting with SUB1-ADD1, CDR-CONS, and CAR-CONS,
and unfolding PLUS, FIX-COST, MEMBER, STRIP-CARS, SUM-CDRS, ADD1, NLISTP,
EQUAL, V&C$, and SUBRP, to six new goals:
Case 6. (IMPLIES (AND (NOT (EQUAL FN 'IF))
(NOT (LISTP (V&C$ 'LIST ARGS VA)))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL))
1))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(NOT (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL))))
(EQUAL (V&C$ T (CONS FN ARGS) VA) F)),
which again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up
the definitions of FIX-COST, NLISTP, EQUAL, and V&C$, to:
T.
Case 5. (IMPLIES
(AND (NOT (EQUAL FN 'IF))
(NOT (LISTP (V&C$ 'LIST ARGS VA)))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL))
1))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL)))
(EQUAL (V&C$ T (CONS FN ARGS) VA)
(CONS (CAR (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL)))
(PLUS 1
(CDR (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN) NIL))))))).
But this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
and expanding FIX-COST, NLISTP, EQUAL, and V&C$, to:
T.
Case 4. (IMPLIES
(AND
(NOT (EQUAL FN 'IF))
(LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(NOT (LISTP (CDR (V&C$ 'LIST ARGS VA))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA)))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
0))))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(NOT (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA)))))))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
F)),
which again simplifies, expanding FIX-COST, to:
T.
Case 3. (IMPLIES
(AND
(NOT (EQUAL FN 'IF))
(LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(NOT (LISTP (CDR (V&C$ 'LIST ARGS VA))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA)))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
0))))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA))))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(CONS
(CAR (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA))))))
(ADD1
(PLUS
(PLUS (CDAR (V&C$ 'LIST ARGS VA)) 0)
(CDR (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(LIST (CAAR (V&C$ 'LIST ARGS VA))))))))))),
which again simplifies, rewriting with SUB1-ADD1, and unfolding the
functions PLUS and FIX-COST, to:
T.
Case 2. (IMPLIES
(AND
(NOT (EQUAL FN 'IF))
(LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(LISTP (CDR (V&C$ 'LIST ARGS VA)))
(CADR (V&C$ 'LIST ARGS VA))
(NOT (MEMBER F
(CDDR (V&C$ 'LIST ARGS VA))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST
(V&C$ T
(BODY FN)
(PAIRLIST
(FORMALS FN)
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA)))))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
(CDADR (V&C$ 'LIST ARGS VA))
(SUM-CDRS (CDDR (V&C$ 'LIST ARGS VA)))))))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(NOT
(V&C$ T
(BODY FN)
(PAIRLIST
(FORMALS FN)
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA)))))))))
(EQUAL (V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
F)).
This again simplifies, expanding the function FIX-COST, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EQUAL FN 'IF))
(LISTP (V&C$ 'LIST ARGS VA))
(CAR (V&C$ 'LIST ARGS VA))
(LISTP (CDR (V&C$ 'LIST ARGS VA)))
(CADR (V&C$ 'LIST ARGS VA))
(NOT (MEMBER F
(CDDR (V&C$ 'LIST ARGS VA))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(FIX-COST
(V&C$ T
(BODY FN)
(PAIRLIST
(FORMALS FN)
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA)))))))
(ADD1 (PLUS (CDAR (V&C$ 'LIST ARGS VA))
(CDADR (V&C$ 'LIST ARGS VA))
(SUM-CDRS (CDDR (V&C$ 'LIST ARGS VA)))))))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN))
(V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA))))))))
(EQUAL
(V&C-APPLY$ FN (V&C$ 'LIST ARGS VA))
(CONS
(CAR
(V&C$ T
(BODY FN)
(PAIRLIST
(FORMALS FN)
(CONS (CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA))))))))
(ADD1
(PLUS
(PLUS (CDAR (V&C$ 'LIST ARGS VA))
(CDADR (V&C$ 'LIST ARGS VA))
(SUM-CDRS (CDDR (V&C$ 'LIST ARGS VA))))
(CDR
(V&C$ T
(BODY FN)
(PAIRLIST
(FORMALS FN)
(CONS
(CAAR (V&C$ 'LIST ARGS VA))
(CONS (CAADR (V&C$ 'LIST ARGS VA))
(STRIP-CARS (CDDR (V&C$ 'LIST ARGS VA))))))))))))),
which again simplifies, applying the lemma SUB1-ADD1, and unfolding PLUS and
FIX-COST, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
QVAL-NON-SUBR-AUX1
(PROVE-LEMMA QVAL-NON-SUBR-AUX2
(REWRITE)
(IMPLIES (AND X1
(EQUAL V1 (CONS W X2))
X3 X4 X5 X6 X7)
(EQUAL (CAR V1) W)))
WARNING: Note that QVAL-NON-SUBR-AUX2 contains the free variables X7, X6, X5,
X4, X3, X2, W, and X1 which will be chosen by instantiating the hypotheses X1,
(EQUAL V1 (CONS W X2)), X3, X4, X5, X6, and X7.
This simplifies, applying CAR-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-NON-SUBR-AUX2
(PROVE-LEMMA QVAL-NON-SUBR
(REWRITE)
(IMPLIES (AND (NOT (MEMBER F (QVAL-LIST ARGS VA)))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN)))
(EQUAL (QVAL (CONS FN ARGS) VA)
(QVAL (BODY FN)
(PAIRLIST (FORMALS FN)
(STRIP-CARS (QVAL-LIST ARGS VA))))))
((USE (QVAL-NON-SUBR-AUX1)
(SAME-F-MEMBERSHIP (VA VA) (LST ARGS))
(SAME-STRIP-CARS (VA VA) (LST ARGS)))
(DO-NOT-INDUCT T)
(DISABLE V&C$ SUBRP)
(HANDS-OFF V&C$ SUBRP)))
WARNING: Note that the rewrite rule QVAL-NON-SUBR will be stored so as to
apply only to terms with the nonrecursive function symbol QVAL.
This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and
QVAL, to:
(IMPLIES
(AND
(IMPLIES
(AND (NOT (EQUAL FN 'QUOTE))
(NOT (MEMBER F (V&C$ 'LIST ARGS VA)))
(NOT (SUBRP FN)))
(EQUAL (V&C$ T (CONS FN ARGS) VA)
(FIX-COST (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(STRIP-CARS (V&C$ 'LIST ARGS VA))))
(ADD1 (SUM-CDRS (V&C$ 'LIST ARGS VA))))))
(IFF (MEMBER F (QVAL-LIST ARGS VA))
(MEMBER F (V&C$ 'LIST ARGS VA)))
(EQUAL (STRIP-CARS (QVAL-LIST ARGS VA))
(STRIP-CARS (V&C$ 'LIST ARGS VA)))
(NOT (MEMBER F (QVAL-LIST ARGS VA)))
(NOT (EQUAL FN 'QUOTE))
(NOT (SUBRP FN)))
(EQUAL (RESET (V&C$ T (CONS FN ARGS) VA))
(RESET (V&C$ T
(BODY FN)
(PAIRLIST (FORMALS FN)
(STRIP-CARS (QVAL-LIST ARGS VA))))))),
which simplifies, applying SUB1-ADD1 and QVAL-NON-SUBR-AUX2, and expanding the
definitions of NOT, AND, PLUS, FIX-COST, IMPLIES, IFF, RESET, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-NON-SUBR
(DISABLE QVAL-NON-SUBR-AUX2)
[ 0.0 0.0 0.0 ]
QVAL-NON-SUBR-AUX2-OFF
(DISABLE QVAL)
[ 0.0 0.0 0.0 ]
QVAL-OFF
(DEFN ROW0
(X)
(IF (ZEROP X)
1
(IF (EQUAL X 1) 2 (PLUS X 2))))
Observe that (NUMBERP (ROW0 X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROW0
(DEFN ROW1
(X)
(IF (ZEROP X)
1
(ROW0 (ROW1 (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, ROW1 is accepted under the
principle of definition. From the definition we can conclude that
(NUMBERP (ROW1 X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROW1
(DEFN ROW2
(X)
(IF (ZEROP X)
1
(ROW1 (ROW2 (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, ROW2 is accepted under the
principle of definition. From the definition we can conclude that
(NUMBERP (ROW2 X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROW2
(DEFN ROW3
(X)
(IF (ZEROP X)
1
(ROW2 (ROW3 (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, ROW3 is accepted under the
principle of definition. From the definition we can conclude that
(NUMBERP (ROW3 X)) is a theorem.
[ 0.0 0.0 0.0 ]
ROW3
(DEFN BASE
(X Y)
(OR (ZEROP X) (ZEROP Y)))
Note that (OR (FALSEP (BASE X Y)) (TRUEP (BASE X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
BASE
(DEFN BASE-FN
(X Y)
(IF (ZEROP Y) (ROW0 X) 1))
Note that (NUMBERP (BASE-FN X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
BASE-FN
(DEFN ACK
(X Y)
(EVAL$ T
'(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X X) (CONS 'Y Y))))
[ 0.0 0.0 0.0 ]
ACK
(DEFN ASSN
(VALX VALY)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
Note that (LISTP (ASSN VALX VALY)) is a theorem.
[ 0.0 0.0 0.0 ]
ASSN
(DEFN A
(VALX VALY)
(QVAL '(ACK X Y) (ASSN VALX VALY)))
From the definition we can conclude that:
(OR (FALSEP (A VALX VALY))
(LISTP (A VALX VALY)))
is a theorem.
[ 0.0 0.0 0.0 ]
A
(DEFN ACKERMANN
(VALX VALY)
(CAR (A VALX VALY)))
[ 0.0 0.0 0.0 ]
ACKERMANN
(PROVE-LEMMA QVAL-LIST-1
(REWRITE)
(EQUAL (QVAL-LIST (LIST TERM) VA)
(LIST (QVAL TERM VA))))
This conjecture simplifies, applying CAR-CONS, CDR-CONS, QVAL-LIST-EMPTY, and
QVAL-LIST-NON-EMPTY, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-LIST-1
(PROVE-LEMMA QVAL-LIST-2
(REWRITE)
(EQUAL (QVAL-LIST (LIST TERM1 TERM2) VA)
(LIST (QVAL TERM1 VA)
(QVAL TERM2 VA))))
This formula simplifies, rewriting with CAR-CONS, CDR-CONS, QVAL-LIST-1, and
QVAL-LIST-NON-EMPTY, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-LIST-2
(DISABLE QVAL-LIST-NON-EMPTY)
[ 0.0 0.0 0.0 ]
QVAL-LIST-NON-EMPTY-OFF
(PROVE-LEMMA QVAL-ON-X
(REWRITE)
(EQUAL (QVAL 'X (ASSN VALX VALY))
(CONS VALX 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL 'X
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS VALX 0)).
This simplifies, applying CAR-CONS, CDR-CONS, and QVAL-LITATOM, and unfolding
the definitions of EQUAL and ASSOC, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-ON-X
(PROVE-LEMMA QVAL-ON-Y
(REWRITE)
(EQUAL (QVAL 'Y (ASSN VALX VALY))
(CONS VALY 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL 'Y
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS VALY 0)).
This simplifies, applying CDR-CONS, CAR-CONS, and QVAL-LITATOM, and unfolding
the definitions of EQUAL and ASSOC, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-ON-Y
(PROVE-LEMMA QVAL-ON-SUB1-X
(REWRITE)
(EQUAL (QVAL '(SUB1 X) (ASSN VALX VALY))
(CONS (SUB1 VALX) 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL '(SUB1 X)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (SUB1 VALX) 0)).
This simplifies, applying QVAL-LIST-1, QVAL-LITATOM, CDR-CONS, CAR-CONS,
REWRITE-APPLY-SUBR, and QVAL-SUBR, and expanding SUBRP, MEMBER, ASSOC, EQUAL,
and STRIP-CARS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-ON-SUB1-X
(PROVE-LEMMA QVAL-ON-SUB1-Y
(REWRITE)
(EQUAL (QVAL '(SUB1 Y) (ASSN VALX VALY))
(CONS (SUB1 VALY) 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL '(SUB1 Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (SUB1 VALY) 0)).
This simplifies, applying QVAL-LIST-1, QVAL-LITATOM, CAR-CONS, CDR-CONS,
REWRITE-APPLY-SUBR, and QVAL-SUBR, and expanding SUBRP, MEMBER, ASSOC, EQUAL,
and STRIP-CARS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-ON-SUB1-Y
(PROVE-LEMMA QVAL-ON-BASE
(REWRITE)
(EQUAL (QVAL '(BASE X Y) (ASSN VALX VALY))
(CONS (BASE VALX VALY) 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL '(BASE X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (BASE VALX VALY) 0)).
This simplifies, applying QVAL-LIST-2, QVAL-LITATOM, CDR-CONS, CAR-CONS,
QVAL-SUBR, REWRITE-APPLY-SUBR, QVAL-LIST-1, and QVAL-NON-SUBR, and opening up
the definitions of SUBRP, MEMBER, ASSOC, EQUAL, BODY, FORMALS, STRIP-CARS, CDR,
CAR, LISTP, PAIRLIST, ZEROP, OR, and BASE, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
QVAL-ON-BASE
(PROVE-LEMMA QVAL-ON-BASE-FN
(REWRITE)
(EQUAL (QVAL '(BASE-FN X Y) (ASSN VALX VALY))
(CONS (BASE-FN VALX VALY) 0)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(EQUAL (QVAL '(BASE-FN X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (BASE-FN VALX VALY) 0)).
This simplifies, applying QVAL-LIST-2, QVAL-LITATOM, CDR-CONS, CAR-CONS,
QVAL-LIST-1, REWRITE-APPLY-SUBR, QVAL-SUBR, QVAL-QUOTE, QVAL-IF, and
QVAL-NON-SUBR, and opening up the definitions of SUBRP, MEMBER, ASSOC, EQUAL,
BODY, FORMALS, STRIP-CARS, CDR, CAR, LISTP, PAIRLIST, ZEROP, CONS, ROW0, and
BASE-FN, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
QVAL-ON-BASE-FN
(PROVE-LEMMA QVAL-ON-BODY
(REWRITE)
(EQUAL (QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(ASSN VALX VALY))
(IF (BASE VALX VALY)
(CONS (BASE-FN VALX VALY) 0)
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))))
((USE (QVAL-ON-BASE)
(QVAL-ON-BASE-FN)
(QVAL-IF (TEST '(BASE X Y))
(THENCASE '(BASE-FN X Y))
(ELSECASE '(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(VA (ASSN VALX VALY))))
(DISABLE QVAL-IF STRIP-CARS QVAL-LIST-1 QVAL-LIST-2 BASE
BASE-FN QVAL-ON-BASE QVAL-ON-BASE-FN)))
WARNING: the previously added lemma, QVAL-IF, could be applied whenever the
newly proposed QVAL-ON-BODY could!
This conjecture can be simplified, using the abbreviations AND and ASSN, to:
(IMPLIES (AND (EQUAL (QVAL '(BASE X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (BASE VALX VALY) 0))
(EQUAL (QVAL '(BASE-FN X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(CONS (BASE-FN VALX VALY) 0))
(EQUAL (QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(IF (QVAL '(BASE X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(IF (CAR (QVAL '(BASE X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))
(QVAL '(BASE-FN X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))
F)))
(EQUAL (QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(IF (BASE VALX VALY)
(CONS (BASE-FN VALX VALY) 0)
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))))).
This simplifies, rewriting with the lemma CAR-CONS, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ON-BODY
(PROVE-LEMMA QVAL-OF-ACK-OF-TERMS-AUX1
(REWRITE)
(IMPLIES (AND (QVAL TERM1 VA) (QVAL TERM2 VA))
(EQUAL (QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(ASSN (CAR (QVAL TERM1 VA))
(CAR (QVAL TERM2 VA))))))
((DO-NOT-INDUCT T)
(USE (QVAL-NON-SUBR (FN 'ACK)
(ARGS (LIST TERM1 TERM2))
(VA VA)))
(DISABLE QVAL-IF BASE BASE-FN QVAL-ON-BASE QVAL-ON-BASE-FN
QVAL-NON-SUBR)))
This formula can be simplified, using the abbreviations AND, IMPLIES, ASSN,
and PACK-EQUAL, to:
(IMPLIES
(AND
(IMPLIES
(AND (NOT (MEMBER F
(QVAL-LIST (LIST TERM1 TERM2) VA)))
(NOT (EQUAL '(65 67 75 . 0)
'(81 85 79 84 69 . 0)))
(NOT (SUBRP 'ACK)))
(EQUAL
(QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL (BODY 'ACK)
(PAIRLIST (FORMALS 'ACK)
(STRIP-CARS (QVAL-LIST (LIST TERM1 TERM2) VA))))))
(QVAL TERM1 VA)
(QVAL TERM2 VA))
(EQUAL (QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X (CAR (QVAL TERM1 VA)))
(CONS 'Y (CAR (QVAL TERM2 VA))))))),
which simplifies, applying the lemmas QVAL-LIST-2, CDR-CONS, and CAR-CONS, and
unfolding the definitions of MEMBER, NOT, EQUAL, SUBRP, AND, BODY, FORMALS,
STRIP-CARS, CDR, CAR, LISTP, PAIRLIST, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-OF-ACK-OF-TERMS-AUX1
(PROVE-LEMMA QVAL-OF-ACKXY-AUX1
(REWRITE)
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(ASSN VALX VALY)))
((DO-NOT-INDUCT T)
(USE (QVAL-OF-ACK-OF-TERMS-AUX1 (TERM1 'X)
(TERM2 'Y)
(VA (ASSN VALX VALY))))
(DISABLE QVAL-IF STRIP-CARS QVAL-OF-ACK-OF-TERMS-AUX1)))
This conjecture can be simplified, using the abbreviation ASSN, to:
(IMPLIES
(IMPLIES
(AND (QVAL 'X
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(QVAL 'Y
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))
(EQUAL (QVAL '(ACK X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X
(CAR (QVAL 'X
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))))
(CONS 'Y
(CAR (QVAL 'Y
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))))))))
(EQUAL (QVAL '(ACK X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))).
This simplifies, applying CAR-CONS, CDR-CONS, QVAL-LITATOM, QVAL-LIST-2, and
QVAL-NON-SUBR, and opening up EQUAL, ASSOC, AND, SUBRP, MEMBER, BODY, FORMALS,
CDR, CAR, LISTP, PAIRLIST, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
QVAL-OF-ACKXY-AUX1
(PROVE-LEMMA QVAL-OF-ACK-OF-TERMS
(REWRITE)
(IMPLIES (AND (QVAL TERM1 VA) (QVAL TERM2 VA))
(EQUAL (QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL TERM1 VA))
(CAR (QVAL TERM2 VA))))))
((DO-NOT-INDUCT T)
(USE (QVAL-OF-ACK-OF-TERMS-AUX1)
(QVAL-OF-ACKXY-AUX1 (VALX (CAR (QVAL TERM1 VA)))
(VALY (CAR (QVAL TERM2 VA)))))
(DISABLE QVAL-IF STRIP-CARS QVAL-OF-ACK-OF-TERMS-AUX1
QVAL-OF-ACKXY-AUX1)))
WARNING: the previously added lemma, QVAL-OF-ACK-OF-TERMS-AUX1, could be
applied whenever the newly proposed QVAL-OF-ACK-OF-TERMS could!
This conjecture can be simplified, using the abbreviations IMPLIES, AND, and
ASSN, to the conjecture:
(IMPLIES
(AND (IMPLIES (AND (QVAL TERM1 VA) (QVAL TERM2 VA))
(EQUAL (QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X (CAR (QVAL TERM1 VA)))
(CONS 'Y (CAR (QVAL TERM2 VA)))))))
(EQUAL (QVAL '(ACK X Y)
(LIST (CONS 'X (CAR (QVAL TERM1 VA)))
(CONS 'Y (CAR (QVAL TERM2 VA)))))
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X (CAR (QVAL TERM1 VA)))
(CONS 'Y (CAR (QVAL TERM2 VA))))))
(QVAL TERM1 VA)
(QVAL TERM2 VA))
(EQUAL (QVAL (LIST 'ACK TERM1 TERM2) VA)
(QVAL '(ACK X Y)
(LIST (CONS 'X (CAR (QVAL TERM1 VA)))
(CONS 'Y (CAR (QVAL TERM2 VA))))))).
This simplifies, appealing to the lemmas CAR-CONS, CDR-CONS, QVAL-LIST-2,
QVAL-NON-SUBR, and QVAL-LITATOM, and expanding the functions AND, SUBRP, EQUAL,
MEMBER, BODY, FORMALS, CDR, CAR, LISTP, PAIRLIST, ASSOC, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
QVAL-OF-ACK-OF-TERMS
(DISABLE QVAL-OF-ACK-OF-TERMS-AUX1)
[ 0.0 0.0 0.0 ]
QVAL-OF-ACK-OF-TERMS-AUX1-OFF
(PROVE-LEMMA QVAL-OF-ACKXY
(REWRITE)
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(IF (BASE VALX VALY)
(CONS (BASE-FN VALX VALY) 0)
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))))
((USE (QVAL-OF-ACKXY-AUX1)
(QVAL-ON-BODY))
(DISABLE QVAL-OF-ACKXY-AUX1 QVAL-IF QVAL-ON-BODY BASE BASE-FN
QVAL-NON-SUBR QVAL-SUBR QVAL-LIST QVAL-LIST-1)))
WARNING: the previously added lemma, QVAL-OF-ACKXY-AUX1, could be applied
whenever the newly proposed QVAL-OF-ACKXY could!
This conjecture can be simplified, using the abbreviations AND and ASSN, to:
(IMPLIES (AND (EQUAL (QVAL '(ACK X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))
(EQUAL (QVAL '(IF (BASE X Y)
(BASE-FN X Y)
(ACK (ACK (SUB1 X) Y) (SUB1 Y)))
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(IF (BASE VALX VALY)
(CONS (BASE-FN VALX VALY) 0)
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(LIST (CONS 'X VALX)
(CONS 'Y VALY))))))
(EQUAL (QVAL '(ACK X Y)
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))
(IF (BASE VALX VALY)
(CONS (BASE-FN VALX VALY) 0)
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(LIST (CONS 'X VALX)
(CONS 'Y VALY)))))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
QVAL-OF-ACKXY
(DISABLE QVAL-OF-ACKXY-AUX1)
[ 0.0 0.0 0.0 ]
QVAL-OF-ACKXY-AUX1-OFF
(PROVE-LEMMA QVAL-OF-ACKXY-BASE
(REWRITE)
(IMPLIES (BASE VALX VALY)
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(CONS (BASE-FN VALX VALY) 0)))
((DISABLE QVAL-NON-SUBR BASE BASE-FN ASSN)))
WARNING: the previously added lemma, QVAL-OF-ACKXY, could be applied whenever
the newly proposed QVAL-OF-ACKXY-BASE could!
This formula simplifies, rewriting with QVAL-OF-ACKXY, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-OF-ACKXY-BASE
(PROVE-LEMMA QVAL-OF-ACKXY-NON-BASE-AUX1
(REWRITE)
(IMPLIES (NOT (BASE VALX VALY))
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))))
((DISABLE QVAL-NON-SUBR BASE BASE-FN ASSN)))
WARNING: the previously added lemma, QVAL-OF-ACKXY, could be applied whenever
the newly proposed QVAL-OF-ACKXY-NON-BASE-AUX1 could!
This simplifies, applying QVAL-OF-ACKXY, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
QVAL-OF-ACKXY-NON-BASE-AUX1
(DISABLE QVAL-OF-ACKXY)
[ 0.0 0.0 0.0 ]
QVAL-OF-ACKXY-OFF
(PROVE-LEMMA QVAL-OF-ACK-SMALL
(REWRITE)
(EQUAL (QVAL '(ACK (SUB1 X) Y)
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
((USE (QVAL-OF-ACK-OF-TERMS (TERM1 '(SUB1 X))
(TERM2 'Y)
(VA (ASSN VALX VALY))))
(DISABLE QVAL-NON-SUBR BASE BASE-FN ASSN QVAL-OF-ACKXY
QVAL-OF-ACK-OF-TERMS)))
This conjecture can be simplified, using the abbreviations CAR-CONS, QVAL-ON-Y,
and QVAL-ON-SUB1-X, to the formula:
(IMPLIES (IMPLIES (AND (CONS (SUB1 VALX) 0)
(CONS VALY 0))
(EQUAL (QVAL '(ACK (SUB1 X) Y)
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))))
(EQUAL (QVAL '(ACK (SUB1 X) Y)
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))).
This simplifies, opening up the definitions of AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-OF-ACK-SMALL
(PROVE-LEMMA QVAL-OF-ACK-BIG
(REWRITE)
(IMPLIES (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))
(EQUAL (QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK (SUB1 X) Y)
(ASSN VALX VALY)))
(SUB1 VALY)))))
((USE (QVAL-OF-ACK-OF-TERMS (TERM1 '(ACK (SUB1 X) Y))
(TERM2 '(SUB1 Y))
(VA (ASSN VALX VALY))))
(DISABLE QVAL-NON-SUBR BASE BASE-FN ASSN QVAL-OF-ACKXY
QVAL-OF-ACK-OF-TERMS)))
This formula can be simplified, using the abbreviations IMPLIES, CAR-CONS,
QVAL-ON-SUB1-Y, and QVAL-OF-ACK-SMALL, to the new formula:
(IMPLIES
(AND (IMPLIES (AND (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))
(CONS (SUB1 VALY) 0))
(EQUAL (QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY)))))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(EQUAL (QVAL '(ACK (ACK (SUB1 X) Y) (SUB1 Y))
(ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY))))),
which simplifies, unfolding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-OF-ACK-BIG
(DISABLE QVAL-OF-ACK-OF-TERMS)
[ 0.0 0.0 0.0 ]
QVAL-OF-ACK-OF-TERMS-OFF
(PROVE-LEMMA QVAL-OF-ACKXY-NON-BASE
(REWRITE)
(IMPLIES (AND (NOT (BASE VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY)))))
((USE (QVAL-OF-ACKXY-NON-BASE-AUX1))
(DISABLE QVAL-NON-SUBR BASE BASE-FN ASSN
QVAL-OF-ACKXY-NON-BASE-AUX1)))
WARNING: the previously added lemma, QVAL-OF-ACKXY-NON-BASE-AUX1, could be
applied whenever the newly proposed QVAL-OF-ACKXY-NON-BASE could!
This formula simplifies, rewriting with QVAL-OF-ACK-SMALL and QVAL-OF-ACK-BIG,
and expanding the functions NOT and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QVAL-OF-ACKXY-NON-BASE
(DISABLE QVAL-OF-ACKXY-NON-BASE-AUX1)
[ 0.0 0.0 0.0 ]
QVAL-OF-ACKXY-NON-BASE-AUX1-OFF
(DISABLE ASSN)
[ 0.0 0.0 0.0 ]
ASSN-OFF
(PROVE-LEMMA A-IS-TRUE-AUX1
(REWRITE)
(IMPLIES (BASE VALX VALY)
(A VALX VALY)))
WARNING: Note that the rewrite rule A-IS-TRUE-AUX1 will be stored so as to
apply only to terms with the nonrecursive function symbol A.
This formula can be simplified, using the abbreviations IMPLIES and A, to:
(IMPLIES (BASE VALX VALY)
(QVAL '(ACK X Y) (ASSN VALX VALY))),
which simplifies, applying the lemma QVAL-OF-ACKXY-BASE, and expanding the
definitions of BASE, EQUAL, ROW0, BASE-FN, and CONS, to two new conjectures:
Case 2. (IMPLIES (EQUAL VALX 0) '(1 . 0)),
which again simplifies, clearly, to:
T.
Case 1. (IMPLIES (NOT (NUMBERP VALX))
'(1 . 0)).
This again simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX1
(PROVE-LEMMA A-IS-TRUE-AUX2
(REWRITE)
(IMPLIES (ZEROP VALX) (A VALX VALY)))
WARNING: Note that the rewrite rule A-IS-TRUE-AUX2 will be stored so as to
apply only to terms with the nonrecursive function symbol A.
This conjecture can be simplified, using the abbreviations IMPLIES and A, to:
(IMPLIES (ZEROP VALX)
(QVAL '(ACK X Y) (ASSN VALX VALY))).
This simplifies, rewriting with QVAL-OF-ACKXY-BASE, and expanding the
definitions of ZEROP, BASE, EQUAL, ROW0, BASE-FN, and CONS, to two new goals:
Case 2. (IMPLIES (EQUAL VALX 0) '(1 . 0)),
which again simplifies, trivially, to:
T.
Case 1. (IMPLIES (NOT (NUMBERP VALX))
'(1 . 0)).
This again simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX2
(PROVE-LEMMA A-IS-TRUE-AUX3
(REWRITE)
(IMPLIES (ZEROP VALY) (A VALX VALY)))
WARNING: Note that the rewrite rule A-IS-TRUE-AUX3 will be stored so as to
apply only to terms with the nonrecursive function symbol A.
This conjecture can be simplified, using the abbreviations IMPLIES and A, to:
(IMPLIES (ZEROP VALY)
(QVAL '(ACK X Y) (ASSN VALX VALY))).
This simplifies, rewriting with QVAL-OF-ACKXY-BASE, and expanding the
definitions of ZEROP, BASE, EQUAL, ROW0, and BASE-FN, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX3
(DEFN PREV
(VALX VALY)
(CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))))
[ 0.0 0.0 0.0 ]
PREV
(PROVE-LEMMA A-IS-TRUE-AUX4
(REWRITE)
(IMPLIES (AND (NOT (BASE VALX VALY))
(A (SUB1 VALX) VALY)
(A (PREV VALX VALY) (SUB1 VALY)))
(A VALX VALY))
((USE (QVAL-OF-ACKXY-NON-BASE))
(DISABLE BASE QVAL-OF-ACKXY-NON-BASE QVAL-NON-SUBR)))
WARNING: Note that the rewrite rule A-IS-TRUE-AUX4 will be stored so as to
apply only to terms with the nonrecursive function symbol A.
This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
PREV, and A, to the goal:
(IMPLIES
(AND (IMPLIES (AND (NOT (BASE VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY)))))
(NOT (BASE VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY))))
(QVAL '(ACK X Y) (ASSN VALX VALY))).
This simplifies, expanding the functions NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX4
(DISABLE A)
[ 0.0 0.0 0.0 ]
A-OFF
(DISABLE PREV)
[ 0.0 0.0 0.0 ]
PREV-OFF
(DEFN FX
(VALX VALY)
(IF (ZEROP VALX)
F
(IF (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY))
VALX
(FX (SUB1 VALX) VALY))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of AND,
NOT, and ZEROP inform us that the measure (COUNT VALX) decreases according to
the well-founded relation LESSP in each recursive call. Hence, FX is accepted
under the definitional principle. Note that:
(OR (FALSEP (FX VALX VALY))
(NUMBERP (FX VALX VALY)))
is a theorem.
[ 0.0 0.0 0.0 ]
FX
(PROVE-LEMMA FX-IS-FIRST-1
(REWRITE)
(IMPLIES (NOT (A VALX VALY))
(NOT (A (FX VALX VALY) VALY))))
Name 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 (ZEROP VALX) (p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p (SUB1 VALX) VALY))
(p VALX VALY))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of AND, NOT,
and ZEROP can be used to show that the measure (COUNT VALX) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following four new goals:
Case 4. (IMPLIES (AND (ZEROP VALX) (NOT (A VALX VALY)))
(NOT (A (FX VALX VALY) VALY))).
This simplifies, applying A-IS-TRUE-AUX2, and expanding the function ZEROP,
to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY))
(NOT (A VALX VALY)))
(NOT (A (FX VALX VALY) VALY))),
which simplifies, unfolding the functions ZEROP, NOT, AND, and FX, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(A (SUB1 VALX) VALY)
(NOT (A VALX VALY)))
(NOT (A (FX VALX VALY) VALY))),
which simplifies, expanding the definitions of ZEROP, NOT, and AND, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(NOT (A (FX (SUB1 VALX) VALY) VALY))
(NOT (A VALX VALY)))
(NOT (A (FX VALX VALY) VALY))),
which simplifies, expanding the functions ZEROP, NOT, AND, and FX, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FX-IS-FIRST-1
(PROVE-LEMMA FX-IS-FIRST-2
(REWRITE)
(IMPLIES (NOT (A VALX VALY))
(A (SUB1 (FX VALX VALY)) VALY)))
Name 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 (ZEROP VALX) (p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p (SUB1 VALX) VALY))
(p VALX VALY))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of AND, NOT,
and ZEROP can be used to show that the measure (COUNT VALX) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following four new goals:
Case 4. (IMPLIES (AND (ZEROP VALX) (NOT (A VALX VALY)))
(A (SUB1 (FX VALX VALY)) VALY)).
This simplifies, applying A-IS-TRUE-AUX2, and expanding the function ZEROP,
to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY))
(NOT (A VALX VALY)))
(A (SUB1 (FX VALX VALY)) VALY)),
which simplifies, unfolding the functions ZEROP, NOT, AND, and FX, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(A (SUB1 VALX) VALY)
(NOT (A VALX VALY)))
(A (SUB1 (FX VALX VALY)) VALY)),
which simplifies, expanding the definitions of ZEROP, NOT, and AND, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(A (SUB1 (FX (SUB1 VALX) VALY)) VALY)
(NOT (A VALX VALY)))
(A (SUB1 (FX VALX VALY)) VALY)),
which simplifies, expanding the functions ZEROP, NOT, AND, and FX, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FX-IS-FIRST-2
(PROVE-LEMMA A-IS-TRUE-AUX5
(REWRITE)
(IMPLIES (NOT (A VALX VALY))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))))
.
Applying the lemma SUB1-ELIM, replace VALY by (ADD1 X) to eliminate
(SUB1 VALY). We use the type restriction lemma noted when SUB1 was introduced
to restrict the new variable. This produces the following three new goals:
Case 3. (IMPLIES (AND (EQUAL VALY 0)
(NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))).
But this simplifies, applying A-IS-TRUE-AUX3, and expanding the function
ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP VALY))
(NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))).
But this simplifies, rewriting with A-IS-TRUE-AUX3, and expanding the
function ZEROP, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (A VALX (ADD1 X))))
(NOT (A (PREV (FX VALX (ADD1 X)) (ADD1 X))
X))).
This simplifies, obviously, to:
(IMPLIES (AND (NUMBERP X)
(NOT (A VALX (ADD1 X))))
(NOT (A (PREV (FX VALX (ADD1 X)) (ADD1 X))
X))),
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:
(IMPLIES (NOT (A VALX VALY))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))).
We named this *1. We will try to prove it by induction. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP VALX) (p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p VALX VALY))
(IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(p (SUB1 VALX) VALY))
(p VALX VALY))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of AND, NOT,
and ZEROP inform us that the measure (COUNT VALX) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (ZEROP VALX) (NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))),
which simplifies, applying A-IS-TRUE-AUX2, and unfolding the function ZEROP,
to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP VALX))
(AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY))
(NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))).
This simplifies, opening up the definitions of ZEROP, NOT, AND, and FX, to:
(IMPLIES (AND (NOT (EQUAL VALX 0))
(NUMBERP VALX)
(A (SUB1 VALX) VALY)
(NOT (A VALX VALY)))
(NOT (A (PREV VALX VALY) (SUB1 VALY)))).
Applying the lemma SUB1-ELIM, replace VALX by (ADD1 X) to eliminate
(SUB1 VALX). We rely upon the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. This produces:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(A X VALY)
(NOT (A (ADD1 X) VALY)))
(NOT (A (PREV (ADD1 X) VALY)
(SUB1 VALY)))),
which further simplifies, obviously, to:
(IMPLIES (AND (NUMBERP X)
(A X VALY)
(NOT (A (ADD1 X) VALY)))
(NOT (A (PREV (ADD1 X) VALY)
(SUB1 VALY)))).
Applying the lemma SUB1-ELIM, replace VALY by (ADD1 Z) to eliminate
(SUB1 VALY). We employ the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. This produces the following three
new conjectures:
Case 3.3.
(IMPLIES (AND (EQUAL VALY 0)
(NUMBERP X)
(A X VALY)
(NOT (A (ADD1 X) VALY)))
(NOT (A (PREV (ADD1 X) VALY)
(SUB1 VALY)))).
However this further simplifies, rewriting with A-IS-TRUE-AUX3, and
expanding ZEROP, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (NUMBERP VALY))
(NUMBERP X)
(A X VALY)
(NOT (A (ADD1 X) VALY)))
(NOT (A (PREV (ADD1 X) VALY)
(SUB1 VALY)))).
But this further simplifies, rewriting with the lemma A-IS-TRUE-AUX3, and
unfolding the definition of ZEROP, to:
T.
Case 3.1.
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NUMBERP X)
(A X (ADD1 Z))
(NOT (A (ADD1 X) (ADD1 Z))))
(NOT (A (PREV (ADD1 X) (ADD1 Z)) Z))),
which further simplifies, appealing to the lemmas SUB1-ADD1 and
A-IS-TRUE-AUX4, and unfolding the function BASE, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(A (SUB1 VALX) VALY)
(NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))),
which simplifies, unfolding the definitions of ZEROP, NOT, and AND, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP VALX))
(NOT (AND (NOT (A VALX VALY))
(A (SUB1 VALX) VALY)))
(NOT (A (PREV (FX (SUB1 VALX) VALY) VALY)
(SUB1 VALY)))
(NOT (A VALX VALY)))
(NOT (A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))),
which simplifies, unfolding the definitions of ZEROP, NOT, AND, and FX, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX5
(DEFN A-IS-TRUE-KLUDGE
(VALX VALY)
(IF (ZEROP VALY)
0
(A-IS-TRUE-KLUDGE (PREV (FX VALX VALY) VALY)
(SUB1 VALY))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT VALY) decreases according to the
well-founded relation LESSP in each recursive call. Hence, A-IS-TRUE-KLUDGE
is accepted under the definitional principle. From the definition we can
conclude that (NUMBERP (A-IS-TRUE-KLUDGE VALX VALY)) is a theorem.
[ 0.0 0.0 0.0 ]
A-IS-TRUE-KLUDGE
(PROVE-LEMMA A-IS-TRUE
(REWRITE)
(A VALX VALY)
((INDUCT (A-IS-TRUE-KLUDGE VALX VALY))))
WARNING: the newly proposed lemma, A-IS-TRUE, could be applied whenever the
previously added lemma FX-IS-FIRST-2 could.
WARNING: the newly proposed lemma, A-IS-TRUE, could be applied whenever the
previously added lemma A-IS-TRUE-AUX4 could.
WARNING: the newly proposed lemma, A-IS-TRUE, could be applied whenever the
previously added lemma A-IS-TRUE-AUX3 could.
WARNING: the newly proposed lemma, A-IS-TRUE, could be applied whenever the
previously added lemma A-IS-TRUE-AUX2 could.
WARNING: the newly proposed lemma, A-IS-TRUE, could be applied whenever the
previously added lemma A-IS-TRUE-AUX1 could.
This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new goals:
Case 2. (IMPLIES (ZEROP VALY) (A VALX VALY)).
This simplifies, rewriting with A-IS-TRUE-AUX3, and unfolding the function
ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL VALY 0))
(NUMBERP VALY)
(A (PREV (FX VALX VALY) VALY)
(SUB1 VALY)))
(A VALX VALY)),
which simplifies, rewriting with A-IS-TRUE-AUX5, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-IS-TRUE
(DISABLE A-IS-TRUE-AUX1)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX1-OFF
(DISABLE A-IS-TRUE-AUX2)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX2-OFF
(DISABLE A-IS-TRUE-AUX3)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX3-OFF
(DISABLE A-IS-TRUE-AUX4)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX4-OFF
(DISABLE A-IS-TRUE-AUX5)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-AUX5-OFF
(DISABLE FX)
[ 0.0 0.0 0.0 ]
FX-OFF
(DISABLE FX-IS-FIRST-1)
[ 0.0 0.0 0.0 ]
FX-IS-FIRST-1-OFF
(DISABLE FX-IS-FIRST-2)
[ 0.0 0.0 0.0 ]
FX-IS-FIRST-2-OFF
(DISABLE A-IS-TRUE-KLUDGE)
[ 0.0 0.0 0.0 ]
A-IS-TRUE-KLUDGE-OFF
(ENABLE A)
[ 0.0 0.0 0.0 ]
A-ON
(PROVE-LEMMA A-BASE
(REWRITE)
(IMPLIES (BASE VALX VALY)
(EQUAL (A VALX VALY)
(CONS (BASE-FN VALX VALY) 0))))
WARNING: Note that the rewrite rule A-BASE will be stored so as to apply only
to terms with the nonrecursive function symbol A.
This conjecture can be simplified, using the abbreviations IMPLIES and A, to:
(IMPLIES (BASE VALX VALY)
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(CONS (BASE-FN VALX VALY) 0))).
This simplifies, applying QVAL-OF-ACKXY-BASE, and expanding BASE, EQUAL, ROW0,
BASE-FN, and CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-BASE
(PROVE-LEMMA A-INDUCTION
(REWRITE)
(IMPLIES (NOT (BASE VALX VALY))
(EQUAL (A VALX VALY)
(A (CAR (A (SUB1 VALX) VALY))
(SUB1 VALY))))
((USE (A-IS-TRUE (VALX (SUB1 VALX))
(VALY VALY))
(QVAL-OF-ACKXY-NON-BASE))
(DISABLE BASE ASSN QVAL-NON-SUBR QVAL-IF A-IS-TRUE
QVAL-OF-ACKXY-NON-BASE)))
WARNING: Note that the rewrite rule A-INDUCTION will be stored so as to apply
only to terms with the nonrecursive function symbol A.
This conjecture can be simplified, using the abbreviations NOT, IMPLIES, AND,
and A, to:
(IMPLIES
(AND (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY))
(IMPLIES (AND (NOT (BASE VALX VALY))
(QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY)))))
(NOT (BASE VALX VALY)))
(EQUAL (QVAL '(ACK X Y) (ASSN VALX VALY))
(QVAL '(ACK X Y)
(ASSN (CAR (QVAL '(ACK X Y)
(ASSN (SUB1 VALX) VALY)))
(SUB1 VALY))))).
This simplifies, opening up the definitions of NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
A-INDUCTION
(DISABLE A)
[ 0.0 0.0 0.0 ]
A-OFF1
(PROVE-LEMMA ACKERMANN-WORKS
(REWRITE)
(EQUAL (ACKERMANN X Y)
(IF (ZEROP X)
1
(IF (ZEROP Y)
(IF (EQUAL X 1) 2 (PLUS X 2))
(ACKERMANN (ACKERMANN (SUB1 X) Y)
(SUB1 Y))))))
WARNING: Note that the rewrite rule ACKERMANN-WORKS will be stored so as to
apply only to terms with the nonrecursive function symbol ACKERMANN.
This conjecture can be simplified, using the abbreviation ACKERMANN, to:
(EQUAL (CAR (A X Y))
(COND ((ZEROP X) 1)
((ZEROP Y)
(IF (EQUAL X 1) 2 (PLUS X 2)))
(T (CAR (A (CAR (A (SUB1 X) Y)) (SUB1 Y)))))).
This simplifies, unfolding the functions ZEROP, NUMBERP, and PLUS, to the
following seven new formulas:
Case 7. (IMPLIES (NOT (NUMBERP X))
(EQUAL (CAR (A X Y)) 1)).
This again simplifies, rewriting with the lemma A-BASE, and expanding the
definitions of BASE, ROW0, BASE-FN, CONS, CAR, and EQUAL, to:
T.
Case 6. (IMPLIES (EQUAL X 0)
(EQUAL (CAR (A X Y)) 1)),
which again simplifies, applying A-BASE, and unfolding the functions BASE,
EQUAL, ROW0, BASE-FN, CONS, and CAR, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL (CAR (A X Y))
(CAR (A (CAR (A (SUB1 X) Y)) (SUB1 Y))))).
However this again simplifies, applying the lemma A-INDUCTION, and unfolding
the definition of BASE, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL Y 0)
(NOT (EQUAL X 1)))
(EQUAL (CAR (A X Y))
(ADD1 (PLUS (SUB1 X) 2)))),
which again simplifies, applying the lemmas A-BASE and CAR-CONS, and opening
up the definitions of BASE, EQUAL, ROW0, PLUS, and BASE-FN, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (NUMBERP Y))
(NOT (EQUAL X 1)))
(EQUAL (CAR (A X Y))
(ADD1 (PLUS (SUB1 X) 2)))),
which again simplifies, applying A-BASE and CAR-CONS, and opening up the
definitions of BASE, ROW0, PLUS, and BASE-FN, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL Y 0)
(EQUAL X 1))
(EQUAL (CAR (A X Y)) 2)).
However this again simplifies, opening up the functions EQUAL, NUMBERP, A,
and CAR, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (NUMBERP Y))
(EQUAL X 1))
(EQUAL (CAR (A X Y)) 2)),
which again simplifies, applying the lemma A-BASE, and unfolding EQUAL,
NUMBERP, BASE, ROW0, BASE-FN, CONS, and CAR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ACKERMANN-WORKS
(DEFN DIVISOR
(X TOP)
(IF (LESSP TOP 2)
F
(IF (DIVISOR X (SUB1 TOP))
(DIVISOR X (SUB1 TOP))
(IF (ZEROP (REMAINDER X TOP))
TOP F))))
Linear arithmetic and the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP can be
used to prove that the measure (COUNT TOP) decreases according to the
well-founded relation LESSP in each recursive call. Hence, DIVISOR is
accepted under the principle of definition. Observe that:
(OR (OR (FALSEP (DIVISOR X TOP))
(NUMBERP (DIVISOR X TOP)))
(EQUAL (DIVISOR X TOP) TOP))
is a theorem.
[ 0.0 0.0 0.0 ]
DIVISOR
(DEFN PRIMEP
(X)
(AND (LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))))
From the definition we can conclude that:
(OR (FALSEP (PRIMEP X))
(TRUEP (PRIMEP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
PRIMEP
(DEFN FPP
(Y)
(AND (PRIMEP Y)
(PRIMEP (ADD1 (ADD1 Y)))))
Note that (OR (FALSEP (FPP Y)) (TRUEP (FPP Y))) is a theorem.
[ 0.0 0.0 0.0 ]
FPP
(DEFN NTP
(X)
(EVAL$ T
'(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
(LIST (CONS 'X X))))
[ 0.0 0.0 0.0 ]
NTP
(DEFN N
(VALX)
(QVAL '(NTP X)
(LIST (CONS 'X VALX))))
Note that (OR (FALSEP (N VALX)) (LISTP (N VALX))) is a theorem.
[ 0.0 0.0 0.0 ]
N
(PROVE-LEMMA QVAL-ON-FPP
(REWRITE)
(IMPLIES (QVAL TERM VA)
(EQUAL (QVAL (LIST 'FPP TERM) VA)
(CONS (FPP (CAR (QVAL TERM VA))) 0)))
((ENABLE QVAL)))
This conjecture can be simplified, using the abbreviations RESET, IMPLIES, and
QVAL, to:
(IMPLIES (AND (V&C$ T TERM VA)
(CONS (CAR (V&C$ T TERM VA)) 0))
(EQUAL (RESET (V&C$ T (LIST 'FPP TERM) VA))
(CONS (FPP (CAR (RESET (V&C$ T TERM VA))))
0))).
This simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, SUB1-ADD1, and
REWRITE-CAR-V&C-APPLY$, and unfolding NLISTP, EQUAL, V&C$, FPP, PRIMEP,
DIVISOR, LESSP, NUMBERP, SUB1, MEMBER, and RESET, to:
(IMPLIES (V&C$ T TERM VA)
(V&C-APPLY$ 'FPP
(LIST (V&C$ T TERM VA)))),
which again simplifies, rewriting with REWRITE-V&C-APPLY$, CDR-CONS, and
CAR-CONS, and unfolding the functions MEMBER and NOT, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ON-FPP
(DISABLE FPP)
[ 0.0 0.0 0.0 ]
FPP-OFF
(PROVE-LEMMA QVAL-ON-NTP-TERM
(REWRITE)
(IMPLIES (QVAL TERM VA)
(EQUAL (QVAL (LIST 'NTP TERM) VA)
(QVAL '(NTP X)
(LIST (CONS 'X (CAR (QVAL TERM VA)))))))
((DISABLE QVAL-LIST QVAL-IF)))
This conjecture simplifies, appealing to the lemmas CAR-CONS, CDR-CONS,
QVAL-LIST-1, QVAL-NON-SUBR, and QVAL-LITATOM, and opening up SUBRP, EQUAL,
MEMBER, BODY, FORMALS, STRIP-CARS, PAIRLIST, CDR, CAR, LISTP, and ASSOC, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ON-NTP-TERM
(PROVE-LEMMA QVAL-ON-NTP-TERM-N
(REWRITE)
(IMPLIES (QVAL TERM VA)
(EQUAL (QVAL (LIST 'NTP TERM) VA)
(N (CAR (QVAL TERM VA)))))
((DISABLE QVAL-LIST QVAL-IF)))
WARNING: the previously added lemma, QVAL-ON-NTP-TERM, could be applied
whenever the newly proposed QVAL-ON-NTP-TERM-N could!
This formula can be simplified, using the abbreviations IMPLIES and N, to:
(IMPLIES (QVAL TERM VA)
(EQUAL (QVAL (LIST 'NTP TERM) VA)
(QVAL '(NTP X)
(LIST (CONS 'X (CAR (QVAL TERM VA))))))),
which simplifies, rewriting with QVAL-LIST-1, QVAL-LITATOM, CDR-CONS, CAR-CONS,
QVAL-NON-SUBR, and QVAL-ON-NTP-TERM, and expanding the definitions of SUBRP,
MEMBER, ASSOC, EQUAL, BODY, FORMALS, STRIP-CARS, PAIRLIST, CDR, CAR, and LISTP,
to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ON-NTP-TERM-N
(PROVE-LEMMA QVAL-ON-NTP-ADD1
(REWRITE)
(EQUAL (QVAL '(NTP (ADD1 X))
(LIST (CONS 'X VALX)))
(N (ADD1 VALX)))
((DISABLE QVAL-LIST QVAL-IF)))
This conjecture can be simplified, using the abbreviation N, to:
(EQUAL (QVAL '(NTP (ADD1 X))
(LIST (CONS 'X VALX)))
(QVAL '(NTP X)
(LIST (CONS 'X (ADD1 VALX))))).
This simplifies, rewriting with the lemmas QVAL-SUBR, REWRITE-APPLY-SUBR,
CAR-CONS, CDR-CONS, QVAL-LITATOM, QVAL-LIST-1, and QVAL-NON-SUBR, and
expanding the functions STRIP-CARS, EQUAL, ASSOC, MEMBER, SUBRP, BODY, FORMALS,
PAIRLIST, CDR, CAR, and LISTP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
QVAL-ON-NTP-ADD1
(PROVE-LEMMA UNWIND-1
(REWRITE)
(EQUAL (N VALX)
(QVAL '(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
(LIST (CONS 'X VALX))))
((DISABLE QVAL-LIST QVAL-IF)))
WARNING: Note that the rewrite rule UNWIND-1 will be stored so as to apply
only to terms with the nonrecursive function symbol N.
This conjecture can be simplified, using the abbreviation N, to:
(EQUAL (QVAL '(NTP X) (LIST (CONS 'X VALX)))
(QVAL '(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
(LIST (CONS 'X VALX)))).
This simplifies, appealing to the lemmas QVAL-LIST-1, QVAL-LITATOM, CDR-CONS,
CAR-CONS, and QVAL-NON-SUBR, and unfolding SUBRP, MEMBER, ASSOC, EQUAL, BODY,
FORMALS, STRIP-CARS, PAIRLIST, CDR, CAR, and LISTP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
UNWIND-1
(PROVE-LEMMA UNWIND-2
(REWRITE)
(EQUAL (QVAL '(FPP (ADD1 X)) VA)
(CONS (FPP (ADD1 (CDR (ASSOC 'X VA))))
0))
((USE (QVAL-ON-FPP (TERM '(ADD1 X))))
(DISABLE QVAL-LIST QVAL-NON-SUBR QVAL-ON-FPP)))
This conjecture simplifies, applying CAR-CONS, CDR-CONS, QVAL-LIST-1,
QVAL-LITATOM, REWRITE-APPLY-SUBR, and QVAL-SUBR, and expanding SUBRP, EQUAL,
MEMBER, STRIP-CARS, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
UNWIND-2
(PROVE-LEMMA UNWIND-3
(REWRITE)
(EQUAL (QVAL '(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
VA)
(IF (FPP (ADD1 (CDR (ASSOC 'X VA))))
(CONS (ADD1 (CDR (ASSOC 'X VA))) 0)
(QVAL '(NTP (ADD1 X)) VA)))
((DO-NOT-INDUCT T)
(DISABLE QVAL-LIST N QVAL-NON-SUBR)
(HANDS-OFF N)))
WARNING: the previously added lemma, QVAL-IF, could be applied whenever the
newly proposed UNWIND-3 could!
This simplifies, rewriting with UNWIND-2, CAR-CONS, CDR-CONS, QVAL-LIST-1,
QVAL-LITATOM, REWRITE-APPLY-SUBR, QVAL-SUBR, and QVAL-IF, and unfolding the
functions SUBRP, EQUAL, MEMBER, and STRIP-CARS, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
UNWIND-3
(PROVE-LEMMA UNWIND-4
(REWRITE)
(EQUAL (N VALX)
(IF (FPP (ADD1 VALX))
(CONS (ADD1 VALX) 0)
(QVAL '(NTP (ADD1 X))
(LIST (CONS 'X VALX)))))
((DO-NOT-INDUCT T)
(USE (UNWIND-1)
(UNWIND-3 (VA (LIST (CONS 'X VALX)))))
(DISABLE UNWIND-1 QVAL-LIST QVAL-NON-SUBR UNWIND-3 QVAL-IF)))
WARNING: Note that the rewrite rule UNWIND-4 will be stored so as to apply
only to terms with the nonrecursive function symbol N.
WARNING: the previously added lemma, UNWIND-1, could be applied whenever the
newly proposed UNWIND-4 could!
This conjecture can be simplified, using the abbreviations AND,
QVAL-ON-NTP-ADD1, and N, to:
(IMPLIES
(AND (EQUAL (QVAL '(NTP X) (LIST (CONS 'X VALX)))
(QVAL '(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
(LIST (CONS 'X VALX))))
(EQUAL (QVAL '(IF (FPP (ADD1 X))
(ADD1 X)
(NTP (ADD1 X)))
(LIST (CONS 'X VALX)))
(IF (FPP (ADD1 (CDR (ASSOC 'X (LIST (CONS 'X VALX))))))
(CONS (ADD1 (CDR (ASSOC 'X (LIST (CONS 'X VALX)))))
0)
(QVAL '(NTP X)
(LIST (CONS 'X (ADD1 VALX)))))))
(EQUAL (QVAL '(NTP X) (LIST (CONS 'X VALX)))
(IF (FPP (ADD1 VALX))
(CONS (ADD1 VALX) 0)
(QVAL '(NTP X)
(LIST (CONS 'X (ADD1 VALX))))))).
This simplifies, rewriting with the lemmas CAR-CONS and CDR-CONS, and
expanding the definitions of EQUAL and ASSOC, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
UNWIND-4
(PROVE-LEMMA UNWIND-5
(REWRITE)
(EQUAL (N VALX)
(IF (FPP (ADD1 VALX))
(CONS (ADD1 VALX) 0)
(N (ADD1 VALX))))
((DO-NOT-INDUCT T)
(USE (UNWIND-4))
(DISABLE N QVAL-LIST QVAL-NON-SUBR UNWIND-4 QVAL-IF)))
WARNING: Note that the rewrite rule UNWIND-5 will be stored so as to apply
only to terms with the nonrecursive function symbol N.
WARNING: the previously added lemma, UNWIND-4, could be applied whenever the
newly proposed UNWIND-5 could!
WARNING: the previously added lemma, UNWIND-1, could be applied whenever the
newly proposed UNWIND-5 could!
This formula can be simplified, using the abbreviations QVAL-ON-NTP-ADD1 and
UNWIND-1, to the new conjecture:
T,
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
UNWIND-5
(DISABLE UNWIND-1)
[ 0.0 0.0 0.0 ]
UNWIND-1-OFF
(DISABLE UNWIND-2)
[ 0.0 0.0 0.0 ]
UNWIND-2-OFF
(DISABLE UNWIND-3)
[ 0.0 0.0 0.0 ]
UNWIND-3-OFF
(DISABLE UNWIND-4)
[ 0.0 0.0 0.0 ]
UNWIND-4-OFF
(DISABLE UNWIND-5)
[ 0.0 0.0 0.0 ]
UNWIND-5-OFF
(PROVE-LEMMA N-BASIS
(REWRITE)
(IMPLIES (FPP (ADD1 X))
(EQUAL (N X) (CONS (ADD1 X) 0)))
((USE (UNWIND-5 (VALX X)))
(DISABLE N)))
WARNING: Note that the rewrite rule N-BASIS will be stored so as to apply
only to terms with the nonrecursive function symbol N.
This simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
N-BASIS
(PROVE-LEMMA N-INDUCTION
(REWRITE)
(IMPLIES (NOT (FPP (ADD1 X)))
(EQUAL (N X) (N (ADD1 X))))
((USE (UNWIND-5 (VALX X)))
(DISABLE N N-BASIS)))
WARNING: Note that the rewrite rule N-INDUCTION will be stored so as to apply
only to terms with the nonrecursive function symbol N.
This formula simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
N-INDUCTION
(PROVE-LEMMA FORM-OF-N
(REWRITE)
(IMPLIES (N X)
(EQUAL (N X) (CONS (CAR (N X)) 0)))
((ENABLE RESET QVAL)
(DISABLE QVAL-NON-SUBR)))
WARNING: Note that the rewrite rule FORM-OF-N will be stored so as to apply
only to terms with the nonrecursive function symbol N.
This formula can be simplified, using the abbreviations RESET, IMPLIES, QVAL,
and N, to:
(IMPLIES (AND (V&C$ T '(NTP X) (LIST (CONS 'X X)))
(CONS (CAR (V&C$ T '(NTP X) (LIST (CONS 'X X))))
0))
(EQUAL (RESET (V&C$ T '(NTP X) (LIST (CONS 'X X))))
(CONS (CAR (RESET (V&C$ T
'(NTP X)
(LIST (CONS 'X X)))))
0))),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
definitions of CDR, CAR, NLISTP, LITATOM, EQUAL, V&C$, ASSOC, and RESET, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
FORM-OF-N
(PROVE-LEMMA N-OF-ZERO
(REWRITE)
(IMPLIES (ZEROP X)
(EQUAL (N X) '(3 . 0))))
WARNING: Note that the rewrite rule N-OF-ZERO will be stored so as to apply
only to terms with the nonrecursive function symbol N.
This formula can be simplified, using the abbreviations IMPLIES and N, to:
(IMPLIES (ZEROP X)
(EQUAL (QVAL '(NTP X) (LIST (CONS 'X X)))
'(3 . 0))),
which simplifies, appealing to the lemmas QVAL-LIST-1, QVAL-LITATOM, CDR-CONS,
CAR-CONS, QVAL-SUBR, SUB1-TYPE-RESTRICTION, REWRITE-APPLY-SUBR, QVAL-ON-FPP,
QVAL-ON-NTP-ADD1, QVAL-IF, and QVAL-NON-SUBR, and unfolding ZEROP, CONS, QVAL,
EQUAL, SUBRP, MEMBER, ASSOC, BODY, FORMALS, STRIP-CARS, PAIRLIST, CDR, CAR,
LISTP, FPP, and N, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
N-OF-ZERO
(DEFN GOOD
(X)
(AND (FPP (CAR (N X)))
(LESSP X (CAR (N X)))))
Observe that (OR (FALSEP (GOOD X)) (TRUEP (GOOD X))) is a theorem.
[ 0.0 0.0 0.0 ]
GOOD
(DISABLE N)
[ 0.0 0.0 0.0 ]
N-OFF
(PROVE-LEMMA N-OF-FPP
(REWRITE)
(IMPLIES (FPP X)
(EQUAL (N (SUB1 X)) (CONS X 0)))
((ENABLE FPP)))
This formula can be simplified, using the abbreviations PRIMEP, FPP, and
IMPLIES, to the new conjecture:
(IMPLIES (AND (LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(LESSP 1 (ADD1 (ADD1 X)))
(NOT (DIVISOR (ADD1 (ADD1 X))
(SUB1 (ADD1 (ADD1 X))))))
(EQUAL (N (SUB1 X)) (CONS X 0))),
which simplifies, rewriting with SUB1-ADD1, ADD1-SUB1, and N-BASIS, and
opening up SUB1, NUMBERP, EQUAL, LESSP, DIVISOR, FPP, and PRIMEP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
N-OF-FPP
(PROVE-LEMMA N-OF-NON-FPP
(REWRITE)
(IMPLIES (AND (NOT (FPP X)) (NOT (ZEROP X)))
(EQUAL (N (SUB1 X)) (N X)))
((USE (N-INDUCTION (X (SUB1 X))))
(DISABLE N-INDUCTION DIVISOR PRIMEP)))
This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (NOT (FPP (ADD1 (SUB1 X))))
(EQUAL (N (SUB1 X))
(N (ADD1 (SUB1 X)))))
(NOT (FPP X))
(NOT (EQUAL X 0))
(NUMBERP X))
(EQUAL (N (SUB1 X)) (N X))),
which simplifies, applying the lemma ADD1-SUB1, and opening up the definitions
of NOT and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
N-OF-NON-FPP
(PROVE-LEMMA ZERO-IS-GOOD
(REWRITE)
(IMPLIES (ZEROP X) (GOOD X)))
WARNING: Note that the rewrite rule ZERO-IS-GOOD will be stored so as to
apply only to terms with the nonrecursive function symbol GOOD.
This simplifies, applying N-OF-ZERO, and opening up the definitions of ZEROP,
GOOD, LESSP, EQUAL, NUMBERP, FPP, and CAR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZERO-IS-GOOD
(PROVE-LEMMA GOOD-GOES-DOWN-AUX1 NIL
(IMPLIES (FPP X) (GOOD (SUB1 X)))
((ENABLE FPP)))
This formula can be simplified, using the abbreviations PRIMEP, FPP, and
IMPLIES, to:
(IMPLIES (AND (LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(LESSP 1 (ADD1 (ADD1 X)))
(NOT (DIVISOR (ADD1 (ADD1 X))
(SUB1 (ADD1 (ADD1 X))))))
(GOOD (SUB1 X))),
which simplifies, applying the lemmas SUB1-ADD1, SUB1-NNUMBERP, CAR-CONS, and
N-OF-FPP, and expanding the definitions of SUB1, NUMBERP, EQUAL, LESSP,
DIVISOR, GOOD, PRIMEP, and FPP, to two new conjectures:
Case 2. (IMPLIES (AND (LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(NUMBERP X)
(LESSP X 1))
(LESSP (SUB1 X) X)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL X 0)
(LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(NUMBERP X)
(LESSP X 1))
(LESSP (SUB1 X) X)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(NUMBERP X)
(NOT (DIVISOR (ADD1 (ADD1 X)) X))
(NOT (EQUAL (REMAINDER (ADD1 (ADD1 X)) (ADD1 X))
0)))
(LESSP (SUB1 X) X)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL X 0)
(LESSP 1 X)
(NOT (DIVISOR X (SUB1 X)))
(NUMBERP X)
(NOT (DIVISOR (ADD1 (ADD1 X)) X))
(NOT (EQUAL (REMAINDER (ADD1 (ADD1 X)) (ADD1 X))
0)))
(LESSP (SUB1 X) X)).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
GOOD-GOES-DOWN-AUX1
(PROVE-LEMMA GOOD-GOES-DOWN-AUX2 NIL
(IMPLIES (AND (NOT (FPP X))
(NOT (ZEROP X))
(GOOD X))
(GOOD (SUB1 X)))
((USE (N-OF-NON-FPP))
(DISABLE N-OF-NON-FPP N N-INDUCTION)))
This conjecture can be simplified, using the abbreviations GOOD, ZEROP, NOT,
AND, and IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (NOT (FPP X)) (NOT (ZEROP X)))
(EQUAL (N (SUB1 X)) (N X)))
(NOT (FPP X))
(NOT (EQUAL X 0))
(NUMBERP X)
(FPP (CAR (N X)))
(LESSP X (CAR (N X))))
(GOOD (SUB1 X))).
This simplifies, expanding the definitions of NOT, ZEROP, AND, IMPLIES, and
GOOD, to:
(IMPLIES (AND (EQUAL (N (SUB1 X)) (N X))
(NOT (FPP X))
(NOT (EQUAL X 0))
(NUMBERP X)
(FPP (CAR (N X)))
(LESSP X (CAR (N X))))
(LESSP (SUB1 X) (CAR (N X)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-GOES-DOWN-AUX2
(PROVE-LEMMA GOOD-GOES-DOWN
(REWRITE)
(IMPLIES (GOOD X) (GOOD (SUB1 X)))
((USE (GOOD-GOES-DOWN-AUX1)
(GOOD-GOES-DOWN-AUX2))
(DISABLE N-OF-NON-FPP N N-INDUCTION N DIVISOR GOOD)))
WARNING: Note that the rewrite rule GOOD-GOES-DOWN will be stored so as to
apply only to terms with the nonrecursive function symbol GOOD.
This conjecture simplifies, rewriting with the lemmas ZERO-IS-GOOD and
SUB1-NNUMBERP, and opening up the definitions of IMPLIES, NOT, ZEROP, AND,
GOOD, and SUB1, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
GOOD-GOES-DOWN
(DEFN GOOD-BELOW-KLUDGE
(Y Z)
(IF (ZEROP Z)
0
(GOOD-BELOW-KLUDGE Y (SUB1 Z))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT Z) decreases according to the well-founded
relation LESSP in each recursive call. Hence, GOOD-BELOW-KLUDGE is accepted
under the principle of definition. From the definition we can conclude that:
(NUMBERP (GOOD-BELOW-KLUDGE Y Z))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-BELOW-KLUDGE
(PROVE-LEMMA GOOD-BELOW-AUX1
(REWRITE)
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z))))
This conjecture simplifies, using linear arithmetic, to the following four new
formulas:
Case 4. (IMPLIES (LESSP (SUB1 Y) Z)
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
Appealing to the lemma SUB1-ELIM, we now replace Y by (ADD1 X) to eliminate
(SUB1 Y). We use the type restriction lemma noted when SUB1 was introduced
to constrain the new variable. We must thus prove three new conjectures:
Case 4.3.
(IMPLIES (AND (EQUAL Y 0) (LESSP (SUB1 Y) Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which further simplifies, expanding the definitions of SUB1, EQUAL, LESSP,
and DIFFERENCE, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP Y))
(LESSP (SUB1 Y) Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which further simplifies, appealing to the lemma SUB1-NNUMBERP, and
opening up EQUAL, LESSP, DIFFERENCE, and SUB1, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(LESSP X Z))
(EQUAL (DIFFERENCE X Z)
(SUB1 (DIFFERENCE (ADD1 X) Z)))),
which further simplifies, applying the lemma SUB1-ADD1, and opening up
DIFFERENCE, to three new goals:
Case 4.1.3.
(IMPLIES (AND (NUMBERP X)
(LESSP X Z)
(NOT (EQUAL Z 0))
(NUMBERP Z))
(EQUAL (DIFFERENCE X Z)
(SUB1 (DIFFERENCE X (SUB1 Z))))).
Applying the lemma SUB1-ELIM, replace Z by (ADD1 V) to eliminate
(SUB1 Z). We employ the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. This produces the new formula:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP X (ADD1 V))
(NOT (EQUAL (ADD1 V) 0)))
(EQUAL (DIFFERENCE X (ADD1 V))
(SUB1 (DIFFERENCE X V)))),
which further simplifies, applying SUB1-ADD1, and opening up LESSP,
EQUAL, DIFFERENCE, and SUB1, to the following two new conjectures:
Case 4.1.3.2.
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NOT (EQUAL X 0)))
(EQUAL (DIFFERENCE (SUB1 X) V)
(SUB1 (DIFFERENCE X V)))),
which we would usually 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 consider:
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z))).
We gave this the name *1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest three inductions. However, they
merge into one likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP (SUB1 Y)) (p Y Z))
(IMPLIES (AND (NOT (ZEROP (SUB1 Y))) (ZEROP Z))
(p Y Z))
(IMPLIES (AND (NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(p (SUB1 Y) (SUB1 Z)))
(p Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT Z) decreases according to the well-founded relation
LESSP in each induction step of the scheme. Note, however, the inductive
instance chosen for Y. The above induction scheme produces the following
three new goals:
Case 3. (IMPLIES (ZEROP (SUB1 Y))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
This simplifies, using linear arithmetic, to the following four new goals:
Case 3.4.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(ZEROP (SUB1 Y)))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
But this again simplifies, opening up the functions ZEROP, EQUAL, and
DIFFERENCE, to five new formulas:
Case 3.4.5.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL Z 0))
(NUMBERP Z))
(EQUAL 0
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, opening up the definitions of EQUAL, LESSP,
DIFFERENCE, and SUB1, to:
T.
Case 3.4.4.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL Z 0))
(EQUAL 0 (SUB1 Y))),
which again simplifies, trivially, to:
T.
Case 3.4.3.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (NUMBERP Z)))
(EQUAL 0 (SUB1 Y))).
This again simplifies, clearly, to:
T.
Case 3.4.2.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(EQUAL (SUB1 Y) 0)
(EQUAL Y 0))
(EQUAL 0 (SUB1 0))).
This again simplifies, clearly, to:
T.
Case 3.4.1.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(EQUAL (SUB1 Y) 0)
(NOT (NUMBERP Y)))
(EQUAL 0 (SUB1 0))).
However this again simplifies, applying the lemma SUB1-NNUMBERP, and
opening up the definitions of EQUAL, LESSP, and SUB1, to:
T.
Case 3.3.
(IMPLIES (AND (LESSP Y 1) (ZEROP (SUB1 Y)))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which again simplifies, opening up the definitions of ZEROP, EQUAL, and
DIFFERENCE, to five new goals:
Case 3.3.5.
(IMPLIES (AND (LESSP Y 1)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL Z 0))
(NUMBERP Z))
(EQUAL 0
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.3.4.
(IMPLIES (AND (LESSP Y 1)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL Z 0))
(EQUAL 0 (SUB1 Y))),
which again simplifies, clearly, to:
T.
Case 3.3.3.
(IMPLIES (AND (LESSP Y 1)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (NUMBERP Z)))
(EQUAL 0 (SUB1 Y))).
This again simplifies, clearly, to:
T.
Case 3.3.2.
(IMPLIES (AND (LESSP Y 1)
(EQUAL (SUB1 Y) 0)
(EQUAL Y 0))
(EQUAL 0 (SUB1 0))).
This again simplifies, obviously, to:
T.
Case 3.3.1.
(IMPLIES (AND (LESSP Y 1)
(EQUAL (SUB1 Y) 0)
(NOT (NUMBERP Y)))
(EQUAL 0 (SUB1 0))).
But this again simplifies, applying SUB1-NNUMBERP, and opening up the
definitions of NUMBERP, EQUAL, LESSP, and SUB1, to:
T.
Case 3.2.
(IMPLIES (AND (NOT (LESSP Z Y))
(ZEROP (SUB1 Y)))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
This again simplifies, opening up the definitions of ZEROP, EQUAL, and
DIFFERENCE, to five new conjectures:
Case 3.2.5.
(IMPLIES (AND (NOT (LESSP Z Y))
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL Z 0))
(NUMBERP Z))
(EQUAL 0
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, opening up EQUAL, DIFFERENCE, and SUB1, to:
T.
Case 3.2.4.
(IMPLIES (AND (NOT (LESSP Z Y))
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL Z 0))
(EQUAL 0 (SUB1 Y))),
which again simplifies, trivially, to:
T.
Case 3.2.3.
(IMPLIES (AND (NOT (LESSP Z Y))
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (NUMBERP Z)))
(EQUAL 0 (SUB1 Y))).
This again simplifies, obviously, to:
T.
Case 3.2.2.
(IMPLIES (AND (NOT (LESSP Z Y))
(EQUAL (SUB1 Y) 0)
(EQUAL Y 0))
(EQUAL 0 (SUB1 0))).
This again simplifies, obviously, to:
T.
Case 3.2.1.
(IMPLIES (AND (NOT (LESSP Z Y))
(EQUAL (SUB1 Y) 0)
(NOT (NUMBERP Y)))
(EQUAL 0 (SUB1 0))).
However this again simplifies, applying SUB1-NNUMBERP, and unfolding the
functions LESSP, EQUAL, and SUB1, to:
T.
Case 3.1.
(IMPLIES (AND (LESSP Y Z) (ZEROP (SUB1 Y)))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
But this again simplifies, expanding ZEROP, EQUAL, and DIFFERENCE, to five
new formulas:
Case 3.1.5.
(IMPLIES (AND (LESSP Y Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL Z 0))
(NUMBERP Z))
(EQUAL 0
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, unfolding the functions EQUAL, DIFFERENCE, and
SUB1, to:
T.
Case 3.1.4.
(IMPLIES (AND (LESSP Y Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL Z 0))
(EQUAL 0 (SUB1 Y))),
which again simplifies, trivially, to:
T.
Case 3.1.3.
(IMPLIES (AND (LESSP Y Z)
(EQUAL (SUB1 Y) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (NUMBERP Z)))
(EQUAL 0 (SUB1 Y))).
This again simplifies, clearly, to:
T.
Case 3.1.2.
(IMPLIES (AND (LESSP Y Z)
(EQUAL (SUB1 Y) 0)
(EQUAL Y 0))
(EQUAL 0 (SUB1 0))).
This again simplifies, trivially, to:
T.
Case 3.1.1.
(IMPLIES (AND (LESSP Y Z)
(EQUAL (SUB1 Y) 0)
(NOT (NUMBERP Y)))
(EQUAL 0 (SUB1 0))).
However this again simplifies, applying the lemma SUB1-NNUMBERP, and
expanding the definitions of LESSP, EQUAL, and SUB1, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP (SUB1 Y))) (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which simplifies, using linear arithmetic, to four new formulas:
Case 2.4.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (ZEROP (SUB1 Y)))
(ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which again simplifies, expanding the definitions of ZEROP, EQUAL, and
DIFFERENCE, to four new formulas:
Case 2.4.4.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, rewriting with SUB1-NNUMBERP, and unfolding the
function LESSP, to:
T.
Case 2.4.3.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, obviously, to:
T.
Case 2.4.2.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, applying SUB1-NNUMBERP, and opening up the
definition of LESSP, to:
T.
Case 2.4.1.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, clearly, to:
T.
Case 2.3.
(IMPLIES (AND (LESSP Y 1)
(NOT (ZEROP (SUB1 Y)))
(ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
But this again simplifies, expanding ZEROP, EQUAL, and DIFFERENCE, to four
new conjectures:
Case 2.3.4.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, applying SUB1-NNUMBERP, and unfolding NUMBERP,
EQUAL, and LESSP, to:
T.
Case 2.3.3.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, obviously, to:
T.
Case 2.3.2.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
opening up the functions NUMBERP, EQUAL, and LESSP, to:
T.
Case 2.3.1.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, obviously, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (ZEROP (SUB1 Y)))
(ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
This again simplifies, opening up the functions ZEROP, EQUAL, and
DIFFERENCE, to four new formulas:
Case 2.2.4.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, applying the lemma SUB1-NNUMBERP, and expanding
the definitions of LESSP and EQUAL, to:
T.
Case 2.2.3.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, clearly, to:
T.
Case 2.2.2.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))).
However this again simplifies, rewriting with SUB1-NNUMBERP, and
expanding the definitions of LESSP and EQUAL, to:
T.
Case 2.2.1.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LESSP Y Z)
(NOT (ZEROP (SUB1 Y)))
(ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
This again simplifies, unfolding the definitions of ZEROP, EQUAL, and
DIFFERENCE, to four new goals:
Case 2.1.4.
(IMPLIES (AND (LESSP Y Z)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.1.3.
(IMPLIES (AND (LESSP Y Z)
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL Z 0)
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, clearly, to:
T.
Case 2.1.2.
(IMPLIES (AND (LESSP Y Z)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(NOT (NUMBERP Y)))
(EQUAL (SUB1 Y) (SUB1 0))).
This again simplifies, unfolding the definition of LESSP, to:
T.
Case 2.1.1.
(IMPLIES (AND (LESSP Y Z)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (NUMBERP Z))
(EQUAL Y 0))
(EQUAL (SUB1 Y) (SUB1 0))),
which again simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z)))))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
This simplifies, using linear arithmetic, to the following four new
conjectures:
Case 1.4.
(IMPLIES (AND (LESSP (SUB1 Y) Z)
(NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z)))))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))).
However this again simplifies, expanding the functions LESSP, ZEROP, and
DIFFERENCE, to three new goals:
Case 1.4.3.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 (SUB1 Y)) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, obviously, to:
T.
Case 1.4.2.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 (SUB1 Y)) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(EQUAL Y 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))).
But this again simplifies, unfolding the functions SUB1, EQUAL, and
LESSP, to:
T.
Case 1.4.1.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 (SUB1 Y)) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (NUMBERP Y)))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))),
which again simplifies, applying the lemma SUB1-NNUMBERP, and unfolding
the definitions of SUB1, EQUAL, and LESSP, to:
T.
Case 1.3.
(IMPLIES (AND (LESSP Y 1)
(NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z)))))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which again simplifies, opening up the functions ZEROP and DIFFERENCE, to
three new conjectures:
Case 1.3.3.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, clearly, to:
T.
Case 1.3.2.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(EQUAL Y 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))).
But this again simplifies, unfolding LESSP, SUB1, and EQUAL, to:
T.
Case 1.3.1.
(IMPLIES (AND (LESSP Y 1)
(NOT (EQUAL (SUB1 Y) 0))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (NUMBERP Y)))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))),
which again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the functions NUMBERP, EQUAL, and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (LESSP Z Y))
(NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z)))))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which again simplifies, applying the lemma SUB1-NNUMBERP, and opening up
the definitions of LESSP, SUB1, ZEROP, and DIFFERENCE, to three new
formulas:
Case 1.2.3.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(NOT (LESSP (SUB1 Z) (SUB1 Y)))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, trivially, to:
T.
Case 1.2.2.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(NOT (LESSP (SUB1 Z) (SUB1 Y)))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(EQUAL Y 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))).
But this again simplifies, unfolding the functions SUB1, EQUAL, and
LESSP, to:
T.
Case 1.2.1.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(NOT (LESSP (SUB1 Z) (SUB1 Y)))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (NUMBERP Y)))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))),
which again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the functions EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (LESSP Y Z)
(NOT (ZEROP (SUB1 Y)))
(NOT (ZEROP Z))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z)))))
(EQUAL (DIFFERENCE (SUB1 Y) Z)
(SUB1 (DIFFERENCE Y Z)))),
which again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the definitions of LESSP, SUB1, ZEROP, and DIFFERENCE, to three
new formulas:
Case 1.1.3.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 Y) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))),
which again simplifies, clearly, to:
T.
Case 1.1.2.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 Y) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(EQUAL Y 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))).
This again simplifies, unfolding the definitions of SUB1, EQUAL, and
LESSP, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(LESSP (SUB1 Y) (SUB1 Z))
(NOT (EQUAL (SUB1 Y) 0))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 (DIFFERENCE (SUB1 Y) (SUB1 Z))))
(NOT (NUMBERP Y)))
(EQUAL (DIFFERENCE (SUB1 (SUB1 Y)) (SUB1 Z))
(SUB1 0))),
which again simplifies, applying SUB1-NNUMBERP, and unfolding EQUAL and
LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.1 ]
GOOD-BELOW-AUX1
(PROVE-LEMMA GOOD-BELOW-AUX2
(REWRITE)
(IMPLIES (FPP Y)
(GOOD (DIFFERENCE Y (ADD1 Z))))
((INDUCT (GOOD-BELOW-KLUDGE Y Z))
(DO-NOT-INDUCT T)
(USE (GOOD-GOES-DOWN-AUX1 (X Y)))
(DISABLE GOOD)))
WARNING: Note that the rewrite rule GOOD-BELOW-AUX2 will be stored so as to
apply only to terms with the nonrecursive function symbol GOOD.
This formula simplifies, rewriting with SUB1-ADD1, GOOD-BELOW-AUX1, and
ADD1-SUB1, and unfolding the definitions of IMPLIES, ZEROP, NOT, DIFFERENCE,
OR, and AND, to nine new conjectures:
Case 9. (IMPLIES (AND (GOOD (SUB1 Y))
(NOT (NUMBERP Z))
(FPP Y)
(NOT (EQUAL Y 0))
(NUMBERP Y))
(GOOD (SUB1 (DIFFERENCE Y 0)))),
which again simplifies, expanding EQUAL and DIFFERENCE, to:
T.
Case 8. (IMPLIES (AND (GOOD (SUB1 Y))
(EQUAL Z 0)
(FPP Y)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP Z))
(GOOD (SUB1 (DIFFERENCE Y Z)))),
which again simplifies, opening up NUMBERP, EQUAL, and DIFFERENCE, to:
T.
Case 7. (IMPLIES (AND (GOOD (SUB1 Y))
(EQUAL Z 0)
(FPP Y)
(NOT (NUMBERP Y)))
(GOOD 0)),
which again simplifies, rewriting with SUB1-NNUMBERP, and unfolding the
definition of GOOD, to:
T.
Case 6. (IMPLIES (AND (GOOD (SUB1 Y))
(EQUAL Z 0)
(FPP Y)
(EQUAL Y 0))
(GOOD 0)).
However this again simplifies, unfolding SUB1, GOOD, and FPP, to:
T.
Case 5. (IMPLIES (AND (GOOD (SUB1 Y))
(NOT (NUMBERP Z))
(FPP Y)
(NOT (NUMBERP Y)))
(GOOD 0)),
which again simplifies, rewriting with SUB1-NNUMBERP, and expanding the
definition of GOOD, to:
T.
Case 4. (IMPLIES (AND (GOOD (SUB1 Y))
(NOT (NUMBERP Z))
(FPP Y)
(EQUAL Y 0))
(GOOD 0)).
However this again simplifies, unfolding the functions SUB1, GOOD, and FPP,
to:
T.
Case 3. (IMPLIES (AND (GOOD (SUB1 Y))
(NUMBERP Z)
(FPP Y)
(GOOD (DIFFERENCE Y Z))
(NOT (EQUAL Y 0))
(NUMBERP Y))
(GOOD (SUB1 (DIFFERENCE Y Z)))),
which again simplifies, rewriting with the lemmas GOOD-BELOW-AUX1 and
GOOD-GOES-DOWN, and opening up the definitions of DIFFERENCE and EQUAL, to:
T.
Case 2. (IMPLIES (AND (GOOD (SUB1 Y))
(FPP Y)
(GOOD (DIFFERENCE Y Z))
(NOT (NUMBERP Y)))
(GOOD 0)),
which again simplifies, appealing to the lemma SUB1-NNUMBERP, and opening up
the functions GOOD and DIFFERENCE, to:
T.
Case 1. (IMPLIES (AND (GOOD (SUB1 Y))
(FPP Y)
(GOOD (DIFFERENCE Y Z))
(EQUAL Y 0))
(GOOD 0)),
which again simplifies, unfolding SUB1, GOOD, and FPP, to:
T.
Q.E.D.
[ 0.0 0.7 0.0 ]
GOOD-BELOW-AUX2
(DISABLE GOOD-BELOW-AUX1)
[ 0.0 0.0 0.0 ]
GOOD-BELOW-AUX1-OFF
(DISABLE GOOD-BELOW-AUX2)
[ 0.0 0.0 0.0 ]
GOOD-BELOW-AUX2-OFF
(PROVE-LEMMA GOOD-BELOW-AUX3
(REWRITE)
(IMPLIES (AND (LESSP X Y) (NUMBERP X))
(EQUAL (DIFFERENCE Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
X)))
This simplifies, using linear arithmetic, to two new goals:
Case 2. (IMPLIES (AND (LESSP Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
(LESSP X Y)
(NUMBERP X))
(EQUAL (DIFFERENCE Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
X)),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP Y X)
(LESSP Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
(LESSP X Y)
(NUMBERP X))
(EQUAL (DIFFERENCE Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
X)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP Y X)
(LESSP X Y)
(NUMBERP X))
(EQUAL (DIFFERENCE Y
(ADD1 (SUB1 (DIFFERENCE Y X))))
X)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-BELOW-AUX3
(PROVE-LEMMA GOOD-BELOW
(REWRITE)
(IMPLIES (AND (FPP Y) (LESSP X Y))
(GOOD X))
((DO-NOT-INDUCT T)
(USE (GOOD-BELOW-AUX3)
(GOOD-BELOW-AUX2 (Z (SUB1 (DIFFERENCE Y X)))))))
WARNING: Note that the rewrite rule GOOD-BELOW will be stored so as to apply
only to terms with the nonrecursive function symbol GOOD.
WARNING: Note that GOOD-BELOW contains the free variable Y which will be
chosen by instantiating the hypothesis (FPP Y).
This simplifies, rewriting with the lemmas ADD1-SUB1 and ZERO-IS-GOOD, and
expanding AND, IMPLIES, DIFFERENCE, LESSP, FPP, ZEROP, GOOD, SUB1, and ADD1,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-BELOW
(DISABLE GOOD-BELOW-AUX3)
[ 0.0 0.0 0.0 ]
GOOD-BELOW-AUX3-OFF
(PROVE-LEMMA PROPERTIES-OF-BAD-AUX1
(REWRITE)
(IMPLIES (AND (NOT (GOOD X)) (LESSP X Y))
(NOT (FPP Y)))
((DISABLE GOOD)))
WARNING: Note that PROPERTIES-OF-BAD-AUX1 contains the free variable X which
will be chosen by instantiating the hypothesis (NOT (GOOD X)).
This formula simplifies, appealing to the lemma GOOD-BELOW, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERTIES-OF-BAD-AUX1
(PROVE-LEMMA PROPERTIES-OF-GOOD-AUX1
(REWRITE)
(IMPLIES (GOOD X)
(AND (FPP (CAR (N X)))
(LESSP X (CAR (N X))))))
WARNING: Note that the proposed lemma PROPERTIES-OF-GOOD-AUX1 is to be stored
as zero type prescription rules, zero compound recognizer rules, one linear
rule, and one replacement rule.
This formula can be simplified, using the abbreviations GOOD and IMPLIES, to:
(IMPLIES (AND (FPP (CAR (N X)))
(LESSP X (CAR (N X))))
(AND (FPP (CAR (N X)))
(LESSP X (CAR (N X))))),
which simplifies, unfolding the definition of AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERTIES-OF-GOOD-AUX1
(DEFN NEXT-TWIN-PRIME
(X)
(IF (GOOD X) (CAR (N X)) F))
[ 0.0 0.0 0.0 ]
NEXT-TWIN-PRIME
(DISABLE GOOD-BELOW)
[ 0.0 0.0 0.0 ]
GOOD-BELOW-OFF
(DISABLE GOOD)
[ 0.0 0.0 0.0 ]
GOOD-OFF
(PROVE-LEMMA PROPERTIES-OF-GOOD
(REWRITE)
(IMPLIES (GOOD X)
(AND (FPP (NEXT-TWIN-PRIME X))
(LESSP X (NEXT-TWIN-PRIME X)))))
WARNING: Note that the linear lemma PROPERTIES-OF-GOOD is being stored under
the term (NEXT-TWIN-PRIME X), which is unusual because NEXT-TWIN-PRIME is a
nonrecursive function symbol.
WARNING: Note that the proposed lemma PROPERTIES-OF-GOOD is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and one replacement rule.
This formula simplifies, appealing to the lemma PROPERTIES-OF-GOOD-AUX1, and
expanding the functions NEXT-TWIN-PRIME and AND, to:
(IMPLIES (GOOD X)
(LESSP X (CAR (N X)))),
which again simplifies, using linear arithmetic and rewriting with
PROPERTIES-OF-GOOD-AUX1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERTIES-OF-GOOD
(PROVE-LEMMA PROPERTIES-OF-BAD-1
(REWRITE)
(IMPLIES (NOT (GOOD X))
(EQUAL (NEXT-TWIN-PRIME X) F)))
WARNING: Note that the rewrite rule PROPERTIES-OF-BAD-1 will be stored so as
to apply only to terms with the nonrecursive function symbol NEXT-TWIN-PRIME.
This formula simplifies, expanding the functions NEXT-TWIN-PRIME and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERTIES-OF-BAD-1
(PROVE-LEMMA PROPERTIES-OF-BAD-2
(REWRITE)
(IMPLIES (AND (NOT (GOOD X)) (LESSP X Y))
(NOT (FPP Y))))
WARNING: Note that PROPERTIES-OF-BAD-2 contains the free variable X which
will be chosen by instantiating the hypothesis (NOT (GOOD X)).
WARNING: the previously added lemma, PROPERTIES-OF-BAD-AUX1, could be applied
whenever the newly proposed PROPERTIES-OF-BAD-2 could!
This formula simplifies, appealing to the lemma PROPERTIES-OF-BAD-AUX1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERTIES-OF-BAD-2