(BOOT-STRAP NQTHM)
[ 0.0 0.1 0.0 ]
GROUND-ZERO
(DEFN LENGTH
(L)
(IF (LISTP L)
(ADD1 (LENGTH (CDR L)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, LENGTH is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (LENGTH L)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN OP1 NIL '(SUC))
Observe that (LISTP (OP1)) is a theorem.
[ 0.0 0.0 0.0 ]
OP1
(DEFN OP2 NIL '(ADD MUL DIV MOD))
Observe that (LISTP (OP2)) is a theorem.
[ 0.0 0.0 0.0 ]
OP2
(DEFN OP1-FORM-P
(E)
(AND (LISTP E)
(LISTP (CDR E))
(EQUAL (CDDR E) NIL)
(MEMBER (CAR E) (OP1))))
Observe that (OR (FALSEP (OP1-FORM-P E)) (TRUEP (OP1-FORM-P E))) is a
theorem.
[ 0.0 0.0 0.0 ]
OP1-FORM-P
(DEFN OP2-FORM-P
(E)
(AND (LISTP E)
(LISTP (CDR E))
(LISTP (CDDR E))
(EQUAL (CDDDR E) NIL)
(MEMBER (CAR E) (OP2))))
Observe that (OR (FALSEP (OP2-FORM-P E)) (TRUEP (OP2-FORM-P E))) is a
theorem.
[ 0.0 0.0 0.0 ]
OP2-FORM-P
(DEFN EXP-P
(E)
(COND ((NUMBERP E) T)
((OP1-FORM-P E) (EXP-P (CADR E)))
((OP2-FORM-P E)
(AND (EXP-P (CADR E))
(EXP-P (CADDR E))))
(T F)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, and CDR-LESSP,
and the definitions of OP1-FORM-P, OP1, CDR, CAR, LISTP, MEMBER, OP2, and
OP2-FORM-P can be used to show that the measure (COUNT E) decreases according
to the well-founded relation LESSP in each recursive call. Hence, EXP-P is
accepted under the principle of definition. From the definition we can
conclude that (OR (FALSEP (EXP-P E)) (TRUEP (EXP-P E))) is a theorem.
[ 0.0 0.1 0.0 ]
EXP-P
(DEFN EVAL-EXP
(E)
(COND ((NUMBERP E) E)
((AND (OP1-FORM-P E)
(EQUAL (CAR E) 'SUC))
(ADD1 (EVAL-EXP (CADR E))))
((AND (OP2-FORM-P E)
(EQUAL (CAR E) 'ADD))
(PLUS (EVAL-EXP (CADR E))
(EVAL-EXP (CADDR E))))
((AND (OP2-FORM-P E)
(EQUAL (CAR E) 'MUL))
(TIMES (EVAL-EXP (CADR E))
(EVAL-EXP (CADDR E))))
((AND (OP2-FORM-P E)
(EQUAL (CAR E) 'DIV))
(QUOTIENT (EVAL-EXP (CADR E))
(EVAL-EXP (CADDR E))))
((AND (OP2-FORM-P E)
(EQUAL (CAR E) 'MOD))
(REMAINDER (EVAL-EXP (CADR E))
(EVAL-EXP (CADDR E))))
(T F)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, CDR-LESSP, and
CAR-NLISTP, and the definitions of AND, OP1-FORM-P, OP1, CDR, CAR, LISTP,
MEMBER, OP2, EQUAL, and OP2-FORM-P inform us that the measure (COUNT E)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, EVAL-EXP is accepted under the principle of definition. From the
definition we can conclude that:
(OR (FALSEP (EVAL-EXP E))
(NUMBERP (EVAL-EXP E)))
is a theorem.
[ 0.0 0.2 0.0 ]
EVAL-EXP
(DEFN EXP-TO-RPN
(E)
(COND ((NUMBERP E) (LIST E))
((OP1-FORM-P E)
(APPEND (EXP-TO-RPN (CADR E))
(LIST (CAR E))))
((OP2-FORM-P E)
(APPEND (EXP-TO-RPN (CADDR E))
(APPEND (EXP-TO-RPN (CADR E))
(LIST (CAR E)))))
(T NIL)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, and CDR-LESSP,
and the definitions of OP1-FORM-P, OP1, CDR, CAR, LISTP, MEMBER, OP2, and
OP2-FORM-P can be used to establish that the measure (COUNT E) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
EXP-TO-RPN is accepted under the definitional principle. Observe that:
(OR (LITATOM (EXP-TO-RPN E))
(LISTP (EXP-TO-RPN E)))
is a theorem.
[ 0.0 0.0 0.0 ]
EXP-TO-RPN
(DEFN EVAL-RPN
(R S)
(IF (LISTP R)
(COND ((NUMBERP (CAR R))
(EVAL-RPN (CDR R) (CONS (CAR R) S)))
((EQUAL (CAR R) 'SUC)
(EVAL-RPN (CDR R)
(CONS (ADD1 (CAR S)) (CDR S))))
((EQUAL (CAR R) 'ADD)
(EVAL-RPN (CDR R)
(CONS (PLUS (CAR S) (CADR S))
(CDDR S))))
((EQUAL (CAR R) 'MUL)
(EVAL-RPN (CDR R)
(CONS (TIMES (CAR S) (CADR S))
(CDDR S))))
((EQUAL (CAR R) 'DIV)
(EVAL-RPN (CDR R)
(CONS (QUOTIENT (CAR S) (CADR S))
(CDDR S))))
((EQUAL (CAR R) 'MOD)
(EVAL-RPN (CDR R)
(CONS (REMAINDER (CAR S) (CADR S))
(CDDR S))))
(T (EVAL-RPN (CDR R) S)))
S))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT R) decreases according to the well-founded relation LESSP in each
recursive call. Hence, EVAL-RPN is accepted under the definitional principle.
Observe that (OR (LISTP (EVAL-RPN R S)) (EQUAL (EVAL-RPN R S) S)) is a theorem.
[ 0.0 0.0 0.0 ]
EVAL-RPN
(PROVE-LEMMA EVAL-RPN-APPEND
(REWRITE)
(EQUAL (EVAL-RPN (APPEND R1 R2) S)
(EVAL-RPN R2 (EVAL-RPN R1 S))))
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP R1)
(p (CDR R1) R2 S)
(p (CDR R1)
R2
(CONS (REMAINDER (CAR S) (CADR S))
(CDDR S)))
(p (CDR R1)
R2
(CONS (QUOTIENT (CAR S) (CADR S))
(CDDR S)))
(p (CDR R1)
R2
(CONS (TIMES (CAR S) (CADR S))
(CDDR S)))
(p (CDR R1)
R2
(CONS (PLUS (CAR S) (CADR S))
(CDDR S)))
(p (CDR R1)
R2
(CONS (ADD1 (CAR S)) (CDR S)))
(p (CDR R1) R2 (CONS (CAR R1) S)))
(p R1 R2 S))
(IMPLIES (NOT (LISTP R1))
(p R1 R2 S))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT R1) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive instances
chosen for S. The above induction scheme leads to two new goals:
Case 2. (IMPLIES
(AND (LISTP R1)
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2) S)
(EVAL-RPN R2 (EVAL-RPN (CDR R1) S)))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (REMAINDER (CAR S) (CADR S))
(CDDR S)))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (REMAINDER (CAR S) (CADR S))
(CDDR S)))))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (QUOTIENT (CAR S) (CADR S))
(CDDR S)))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (QUOTIENT (CAR S) (CADR S))
(CDDR S)))))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (TIMES (CAR S) (CADR S))
(CDDR S)))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (TIMES (CAR S) (CADR S))
(CDDR S)))))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (PLUS (CAR S) (CADR S))
(CDDR S)))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (PLUS (CAR S) (CADR S))
(CDDR S)))))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (ADD1 (CAR S)) (CDR S)))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (ADD1 (CAR S)) (CDR S)))))
(EQUAL (EVAL-RPN (APPEND (CDR R1) R2)
(CONS (CAR R1) S))
(EVAL-RPN R2
(EVAL-RPN (CDR R1)
(CONS (CAR R1) S)))))
(EQUAL (EVAL-RPN (APPEND R1 R2) S)
(EVAL-RPN R2 (EVAL-RPN R1 S)))),
which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
the definitions of APPEND and EVAL-RPN, to:
T.
Case 1. (IMPLIES (NOT (LISTP R1))
(EQUAL (EVAL-RPN (APPEND R1 R2) S)
(EVAL-RPN R2 (EVAL-RPN R1 S)))),
which simplifies, unfolding the functions APPEND and EVAL-RPN, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
EVAL-RPN-APPEND
(DEFN L1-IND
(E S)
(COND ((NUMBERP E) T)
((OP1-FORM-P E) (L1-IND (CADR E) S))
((OP2-FORM-P E)
(AND (L1-IND (CADDR E) S)
(L1-IND (CADR E)
(CONS (EVAL-EXP (CADDR E)) S))))
(T T)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, and CDR-LESSP,
and the definitions of OP1-FORM-P, OP1, CDR, CAR, LISTP, MEMBER, OP2, and
OP2-FORM-P establish that the measure (COUNT E) decreases according to the
well-founded relation LESSP in each recursive call. Hence, L1-IND is accepted
under the principle of definition. From the definition we can conclude that
(TRUEP (L1-IND E S)) is a theorem.
[ 0.0 0.1 0.0 ]
L1-IND
(PROVE-LEMMA L1 NIL
(IMPLIES (EXP-P E)
(EQUAL (CONS (EVAL-EXP E) S)
(EVAL-RPN (EXP-TO-RPN E) S)))
((INDUCT (L1-IND E S))))
This formula can be simplified, using the abbreviations OP2, OP2-FORM-P, OP1,
OP1-FORM-P, IMPLIES, NOT, OR, and AND, to the following four new goals:
Case 4. (IMPLIES (AND (NUMBERP E) (EXP-P E))
(EQUAL (CONS (EVAL-EXP E) S)
(EVAL-RPN (EXP-TO-RPN E) S))).
This simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
unfolding EXP-P, EVAL-EXP, EXP-TO-RPN, EVAL-RPN, and LISTP, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP E))
(LISTP E)
(LISTP (CDR E))
(EQUAL (CDDR E) NIL)
(MEMBER (CAR E) '(SUC))
(IMPLIES (EXP-P (CADR E))
(EQUAL (CONS (EVAL-EXP (CADR E)) S)
(EVAL-RPN (EXP-TO-RPN (CADR E)) S)))
(EXP-P E))
(EQUAL (CONS (EVAL-EXP E) S)
(EVAL-RPN (EXP-TO-RPN E) S))).
This simplifies, applying CDR-CONS, CAR-CONS, and EVAL-RPN-APPEND, and
expanding the functions CDR, CAR, LISTP, MEMBER, IMPLIES, OP1-FORM-P, EQUAL,
OP1, EXP-P, EVAL-EXP, CONS, EXP-TO-RPN, NUMBERP, and EVAL-RPN, to:
T.
Case 2. (IMPLIES
(AND (NOT (NUMBERP E))
(NOT (OP1-FORM-P E))
(LISTP E)
(LISTP (CDR E))
(LISTP (CDDR E))
(EQUAL (CDDDR E) NIL)
(MEMBER (CAR E) '(ADD MUL DIV MOD))
(IMPLIES (EXP-P (CADR E))
(EQUAL (CONS (EVAL-EXP (CADR E))
(CONS (EVAL-EXP (CADDR E)) S))
(EVAL-RPN (EXP-TO-RPN (CADR E))
(CONS (EVAL-EXP (CADDR E)) S))))
(IMPLIES (EXP-P (CADDR E))
(EQUAL (CONS (EVAL-EXP (CADDR E)) S)
(EVAL-RPN (EXP-TO-RPN (CADDR E)) S)))
(EXP-P E))
(EQUAL (CONS (EVAL-EXP E) S)
(EVAL-RPN (EXP-TO-RPN E) S))),
which simplifies, rewriting with CAR-CONS, CDR-CONS, and EVAL-RPN-APPEND,
and unfolding the functions OP1-FORM-P, CDR, CAR, LISTP, MEMBER, IMPLIES,
OP2-FORM-P, EQUAL, OP2, EXP-P, EVAL-EXP, CONS, EXP-TO-RPN, NUMBERP, and
EVAL-RPN, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP E))
(NOT (OP1-FORM-P E))
(NOT (OP2-FORM-P E))
(EXP-P E))
(EQUAL (CONS (EVAL-EXP E) S)
(EVAL-RPN (EXP-TO-RPN E) S))).
This simplifies, unfolding the functions MEMBER, LISTP, CAR, CDR, OP1,
OP1-FORM-P, OP2-FORM-P, EXP-P, and OP2, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
L1