(BOOT-STRAP NQTHM)
[ 0.0 0.1 0.0 ]
GROUND-ZERO
(DEFN LENGTH
(X)
(IF (LISTP X)
(ADD1 (LENGTH (CDR X)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, LENGTH is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (LENGTH X)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN PLISTP
(X)
(IF (LISTP X)
(PLISTP (CDR X))
(EQUAL X NIL)))
Linear arithmetic and the lemma CDR-LESSP can be used to establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, PLISTP is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (PLISTP X))
(TRUEP (PLISTP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
PLISTP
(DEFN EXP-P
(EXP)
(COND ((NUMBERP EXP) T)
((NOT (PLISTP EXP)) F)
((EQUAL (LENGTH EXP) 3)
(COND ((EQUAL (CAR EXP) 'PLUS)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
((EQUAL (CAR EXP) 'TIMES)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
((EQUAL (CAR EXP) 'SUBTRACT)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
(T F)))
(T F)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, ADD1-EQUAL, and
CDR-LESSP, and the definitions of ADD1, NUMBERP, EQUAL, LENGTH, and PLISTP
inform us that the measure (COUNT EXP) decreases according to the well-founded
relation LESSP in each recursive call. Hence, EXP-P is accepted under the
definitional principle. From the definition we can conclude that:
(OR (FALSEP (EXP-P EXP))
(TRUEP (EXP-P EXP)))
is a theorem.
[ 0.0 0.1 0.0 ]
EXP-P
(PROVE-LEMMA EXP-P-OPENER
(REWRITE)
(IMPLIES (NOT (NUMBERP EXP))
(EQUAL (EXP-P EXP)
(COND ((NOT (PLISTP EXP)) F)
((EQUAL (LENGTH EXP) 3)
(COND ((EQUAL (CAR EXP) 'PLUS)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
((EQUAL (CAR EXP) 'TIMES)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
((EQUAL (CAR EXP) 'SUBTRACT)
(AND (EXP-P (CADR EXP))
(EXP-P (CADDR EXP))))
(T F)))
(T F)))))
This simplifies, opening up the functions LENGTH, PLISTP, EXP-P, NOT, and AND,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EXP-P-OPENER
(DEFN EVAL-S
(EXP)
(COND ((NOT (EXP-P EXP)) 0)
((NUMBERP EXP) EXP)
((EQUAL (CAR EXP) 'PLUS)
(PLUS (EVAL-S (CADR EXP))
(EVAL-S (CADDR EXP))))
((EQUAL (CAR EXP) 'TIMES)
(TIMES (EVAL-S (CADR EXP))
(EVAL-S (CADDR EXP))))
((EQUAL (CAR EXP) 'SUBTRACT)
(DIFFERENCE (EVAL-S (CADR EXP))
(EVAL-S (CADDR EXP))))
(T 0)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, EXP-P-OPENER, and
CDR-LESSP, and the definitions of EQUAL, LENGTH, and PLISTP establish that the
measure (COUNT EXP) decreases according to the well-founded relation LESSP in
each recursive call. Hence, EVAL-S is accepted under the principle of
definition. Note that (NUMBERP (EVAL-S EXP)) is a theorem.
[ 0.0 0.1 0.0 ]
EVAL-S
(DISABLE EXP-P-OPENER)
[ 0.0 0.0 0.0 ]
EXP-P-OPENER-OFF
(DEFN TARGET-INST-P
(EXP)
(IF (NLISTP EXP)
(MEMBER EXP '(ADD MULT SUB))
(AND (PLISTP EXP)
(EQUAL (LENGTH EXP) 2)
(EQUAL (CAR EXP) 'PUSHC)
(NUMBERP (CADR EXP)))))
From the definition we can conclude that:
(OR (FALSEP (TARGET-INST-P EXP))
(TRUEP (TARGET-INST-P EXP)))
is a theorem.
[ 0.0 0.0 0.0 ]
TARGET-INST-P
(DEFN TARGET-INST-LIST-P
(EXP)
(IF (LISTP EXP)
(AND (TARGET-INST-P (CAR EXP))
(TARGET-INST-LIST-P (CDR EXP)))
(EQUAL EXP NIL)))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT EXP) decreases according to the well-founded relation LESSP in each
recursive call. Hence, TARGET-INST-LIST-P is accepted under the principle of
definition. Note that:
(OR (FALSEP (TARGET-INST-LIST-P EXP))
(TRUEP (TARGET-INST-LIST-P EXP)))
is a theorem.
[ 0.0 0.0 0.0 ]
TARGET-INST-LIST-P
(DEFN SINGLE-STEP
(INST S)
(CASE INST
(ADD (CONS (PLUS (CADR S) (CAR S))
(CDDR S)))
(MULT (CONS (TIMES (CADR S) (CAR S))
(CDDR S)))
(SUB (CONS (DIFFERENCE (CADR S) (CAR S))
(CDDR S)))
(OTHERWISE (CONS (CADR INST) S))))
Observe that (LISTP (SINGLE-STEP INST S)) is a theorem.
[ 0.0 0.0 0.0 ]
SINGLE-STEP
(DEFN INTERPRETER-TARGET
(INST-LIST S)
(IF (LISTP INST-LIST)
(INTERPRETER-TARGET (CDR INST-LIST)
(SINGLE-STEP (CAR INST-LIST) S))
S))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT INST-LIST) decreases according to the well-founded relation LESSP in
each recursive call. Hence, INTERPRETER-TARGET is accepted under the
definitional principle. From the definition we can conclude that:
(OR (LISTP (INTERPRETER-TARGET INST-LIST S))
(EQUAL (INTERPRETER-TARGET INST-LIST S)
S))
is a theorem.
[ 0.0 0.0 0.0 ]
INTERPRETER-TARGET
(ENABLE EXP-P-OPENER)
[ 0.0 0.0 0.0 ]
EXP-P-OPENER-ON
(DEFN COMPILE
(EXP)
(COND ((NOT (EXP-P EXP)) NIL)
((NUMBERP EXP)
(LIST (LIST 'PUSHC EXP)))
((EQUAL (CAR EXP) 'PLUS)
(APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
(LIST 'ADD))))
((EQUAL (CAR EXP) 'TIMES)
(APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
(LIST 'MULT))))
((EQUAL (CAR EXP) 'SUBTRACT)
(APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
(LIST 'SUB))))
(T NIL)))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, EXP-P-OPENER, and
CDR-LESSP, and the definitions of EQUAL, LENGTH, and PLISTP can be used to
show that the measure (COUNT EXP) decreases according to the well-founded
relation LESSP in each recursive call. Hence, COMPILE is accepted under the
principle of definition. Observe that:
(OR (LITATOM (COMPILE EXP))
(LISTP (COMPILE EXP)))
is a theorem.
[ 0.0 0.1 0.0 ]
COMPILE
(DISABLE EXP-P-OPENER)
[ 0.0 0.0 0.0 ]
EXP-P-OPENER-OFF1
(PROVE-LEMMA COMPILE-PRESERVES-LEGALITY
(REWRITE)
(IMPLIES (EXP-P EXP)
(TARGET-INST-LIST-P (COMPILE EXP))))
Give the conjecture the name *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture. However, they merge into one likely candidate induction. We
will induct according to the following scheme:
(AND (IMPLIES (NUMBERP EXP) (p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(NOT (PLISTP EXP)))
(p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(EQUAL (CAR EXP) 'PLUS)
(p (CADR EXP))
(p (CADDR EXP)))
(p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(EQUAL (CAR EXP) 'TIMES)
(p (CADR EXP))
(p (CADDR EXP)))
(p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(EQUAL (CAR EXP) 'SUBTRACT)
(p (CADR EXP))
(p (CADDR EXP)))
(p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(NOT (EQUAL (CAR EXP) 'SUBTRACT)))
(p EXP))
(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(NOT (EQUAL (LENGTH EXP) 3)))
(p EXP))).
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, ADD1-EQUAL, and
CDR-LESSP, and the definitions of ADD1, NUMBERP, EQUAL, LENGTH, and PLISTP
inform us that the measure (COUNT EXP) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme produces the following 16 new conjectures:
Case 16.(IMPLIES (AND (NUMBERP EXP) (EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
functions EXP-P, COMPILE, TARGET-INST-LIST-P, TARGET-INST-P, PLISTP, LENGTH,
ADD1, and EQUAL, to:
T.
Case 15.(IMPLIES (AND (NOT (NUMBERP EXP))
(NOT (PLISTP EXP))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, unfolding the function EXP-P, to:
T.
Case 14.(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(EQUAL (CAR EXP) 'PLUS)
(NOT (EXP-P (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, applying ADD1-EQUAL, and unfolding the definitions of
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 13.(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(EQUAL (CAR EXP) 'PLUS)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, rewriting with the lemma ADD1-EQUAL, and opening up the
functions PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 12.(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(EQUAL (CAR EXP) 'PLUS)
(NOT (EXP-P (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, rewriting with the lemma ADD1-EQUAL, and opening up PLISTP,
LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 11.(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(EQUAL (CAR EXP) 'PLUS)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, applying ADD1-EQUAL, and opening up the definitions of
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, ADD1, and COMPILE, to:
(IMPLIES (AND (NOT (NUMBERP EXP))
(LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'PLUS)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(ADD))))).
This again simplifies, clearly, to the new conjecture:
(IMPLIES (AND (LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'PLUS)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(ADD))))).
Applying the lemma CAR-CDR-ELIM, replace EXP by (CONS Z X) to eliminate
(CDR EXP) and (CAR EXP), X by (CONS W V) to eliminate (CDR X) and (CAR X),
and V by (CONS X D) to eliminate (CAR V) and (CDR V). This produces the
following two new formulas:
Case 11.2.
(IMPLIES
(AND (NOT (LISTP V))
(PLISTP V)
(EQUAL (LENGTH V) 1)
(EQUAL Z 'PLUS)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE (CAR V)))
(EXP-P W)
(EXP-P (CAR V)))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE (CAR V)) '(ADD))))).
However this further simplifies, opening up PLISTP, LENGTH, and EQUAL, to:
T.
Case 11.1.
(IMPLIES (AND (PLISTP (CONS X D))
(EQUAL (LENGTH (CONS X D)) 1)
(EQUAL Z 'PLUS)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(ADD))))),
which further simplifies, rewriting with the lemmas CDR-CONS and
ADD1-EQUAL, and opening up the functions PLISTP, LENGTH, and NUMBERP, to:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(ADD))))).
We will try to prove the above formula by generalizing it, replacing
(COMPILE X) by Y and (COMPILE W) by A. We must thus prove:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y)
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))).
Eliminate irrelevant terms. This produces:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
which we will finally name *1.1.
Case 10.(IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(EQUAL (CAR EXP) 'TIMES)
(NOT (EXP-P (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, rewriting with ADD1-EQUAL, and unfolding PLISTP, LENGTH,
EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 9. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(EQUAL (CAR EXP) 'TIMES)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, applying ADD1-EQUAL, and opening up the functions PLISTP,
LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 8. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(EQUAL (CAR EXP) 'TIMES)
(NOT (EXP-P (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, rewriting with ADD1-EQUAL, and opening up the functions
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 7. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(EQUAL (CAR EXP) 'TIMES)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, applying ADD1-EQUAL, and unfolding PLISTP, LENGTH, EQUAL,
NUMBERP, EXP-P, ADD1, and COMPILE, to the new goal:
(IMPLIES (AND (NOT (NUMBERP EXP))
(LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'TIMES)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(MULT))))),
which again simplifies, trivially, to:
(IMPLIES (AND (LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'TIMES)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(MULT))))).
Applying the lemma CAR-CDR-ELIM, replace EXP by (CONS Z X) to eliminate
(CDR EXP) and (CAR EXP), X by (CONS W V) to eliminate (CDR X) and (CAR X),
and V by (CONS X D) to eliminate (CAR V) and (CDR V). We would thus like to
prove the following two new formulas:
Case 7.2.
(IMPLIES
(AND (NOT (LISTP V))
(PLISTP V)
(EQUAL (LENGTH V) 1)
(EQUAL Z 'TIMES)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE (CAR V)))
(EXP-P W)
(EXP-P (CAR V)))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE (CAR V)) '(MULT))))).
This further simplifies, unfolding PLISTP, LENGTH, and EQUAL, to:
T.
Case 7.1.
(IMPLIES (AND (PLISTP (CONS X D))
(EQUAL (LENGTH (CONS X D)) 1)
(EQUAL Z 'TIMES)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(MULT))))),
which further simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and
expanding the functions PLISTP, LENGTH, and NUMBERP, to:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(MULT))))),
which we generalize by replacing (COMPILE X) by Y and (COMPILE W) by A.
We must thus prove:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y)
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))).
Eliminate irrelevant terms. We would thus like to prove the new goal:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which we will finally name *1.2.
Case 6. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(EQUAL (CAR EXP) 'SUBTRACT)
(NOT (EXP-P (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, rewriting with ADD1-EQUAL, and expanding the functions
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 5. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(EQUAL (CAR EXP) 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(NOT (EXP-P (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, applying ADD1-EQUAL, and expanding the definitions of
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 4. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(EQUAL (CAR EXP) 'SUBTRACT)
(NOT (EXP-P (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, applying ADD1-EQUAL, and expanding the definitions of
PLISTP, LENGTH, EQUAL, NUMBERP, EXP-P, and ADD1, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(EQUAL (CAR EXP) 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))),
which simplifies, applying ADD1-EQUAL, and unfolding the functions PLISTP,
LENGTH, EQUAL, NUMBERP, EXP-P, ADD1, and COMPILE, to:
(IMPLIES (AND (NOT (NUMBERP EXP))
(LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(SUB))))),
which again simplifies, clearly, to:
(IMPLIES (AND (LISTP EXP)
(LISTP (CDR EXP))
(PLISTP (CDDR EXP))
(EQUAL (LENGTH (CDDR EXP)) 1)
(EQUAL (CAR EXP) 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE (CADR EXP)))
(TARGET-INST-LIST-P (COMPILE (CADDR EXP)))
(EXP-P (CADR EXP))
(EXP-P (CADDR EXP)))
(TARGET-INST-LIST-P (APPEND (COMPILE (CADR EXP))
(APPEND (COMPILE (CADDR EXP))
'(SUB))))).
Applying the lemma CAR-CDR-ELIM, replace EXP by (CONS Z X) to eliminate
(CDR EXP) and (CAR EXP), X by (CONS W V) to eliminate (CDR X) and (CAR X),
and V by (CONS X D) to eliminate (CAR V) and (CDR V). This produces the
following two new conjectures:
Case 3.2.
(IMPLIES
(AND (NOT (LISTP V))
(PLISTP V)
(EQUAL (LENGTH V) 1)
(EQUAL Z 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE (CAR V)))
(EXP-P W)
(EXP-P (CAR V)))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE (CAR V)) '(SUB))))).
But this further simplifies, unfolding PLISTP, LENGTH, and EQUAL, to:
T.
Case 3.1.
(IMPLIES (AND (PLISTP (CONS X D))
(EQUAL (LENGTH (CONS X D)) 1)
(EQUAL Z 'SUBTRACT)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(SUB))))),
which further simplifies, applying CDR-CONS and ADD1-EQUAL, and expanding
the definitions of PLISTP, LENGTH, and NUMBERP, to:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P (COMPILE W))
(TARGET-INST-LIST-P (COMPILE X))
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND (COMPILE W)
(APPEND (COMPILE X) '(SUB))))),
which we generalize by replacing (COMPILE X) by Y and (COMPILE W) by A.
This generates the conjecture:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y)
(EXP-P W)
(EXP-P X))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
Eliminate irrelevant terms. We would thus like to prove the new goal:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))),
which we will finally name *1.3.
Case 2. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(EQUAL (LENGTH EXP) 3)
(NOT (EQUAL (CAR EXP) 'PLUS))
(NOT (EQUAL (CAR EXP) 'TIMES))
(NOT (EQUAL (CAR EXP) 'SUBTRACT))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, unfolding EXP-P and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP EXP))
(PLISTP EXP)
(NOT (EQUAL (LENGTH EXP) 3))
(EXP-P EXP))
(TARGET-INST-LIST-P (COMPILE EXP))).
This simplifies, opening up the definition of EXP-P, to:
T.
So let us turn our attention to:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))),
which is formula *1.3 above. We will appeal to induction. The recursive
terms in the conjecture suggest six inductions. They merge into three likely
candidate inductions, all of which are unflawed. However, one of these is
more likely than the others. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP D) (p A Y (CDR D)))
(p A Y D))
(IMPLIES (NOT (LISTP D)) (p A Y D))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT D)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following three new
goals:
Case 3. (IMPLIES (AND (LISTP D)
(NOT (PLISTP (CDR D)))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
This simplifies, unfolding the definition of PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP D)
(NOT (EQUAL (LENGTH (CDR D)) 0))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
This simplifies, opening up the functions PLISTP and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP D))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
This simplifies, opening up the definitions of PLISTP, LENGTH, and EQUAL, to
the new conjecture:
(IMPLIES (AND (NOT (LISTP D))
(EQUAL D NIL)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))),
which again simplifies, unfolding LISTP, to:
(IMPLIES (AND (TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
Give the above formula the name *1.3.1.
We will appeal to induction. There are four plausible inductions. They
merge into two likely candidate inductions, both of which are unflawed. Since
both of these are equally likely, we will choose arbitrarily. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) Y))
(p A Y))
(IMPLIES (NOT (LISTP A)) (p A Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
conjectures:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (TARGET-INST-LIST-P (CDR A)))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
This simplifies, expanding TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, and
TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(TARGET-INST-LIST-P (APPEND (CDR A) (APPEND Y '(SUB))))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))).
This simplifies, applying CDR-CONS and CAR-CONS, and expanding the functions
TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P, APPEND, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(SUB))))),
which simplifies, expanding TARGET-INST-LIST-P, LISTP, and APPEND, to the
formula:
(IMPLIES (AND (NOT (LISTP A))
(EQUAL A NIL)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(SUB)))).
This again simplifies, opening up the function LISTP, to:
(IMPLIES (TARGET-INST-LIST-P Y)
(TARGET-INST-LIST-P (APPEND Y '(SUB)))).
Call the above conjecture *1.3.1.1.
Perhaps we can prove it by induction. Two inductions are suggested by
terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (p (CDR Y)))
(p Y))
(IMPLIES (NOT (LISTP Y)) (p Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to the following three new
conjectures:
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (TARGET-INST-LIST-P (CDR Y)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(SUB)))).
This simplifies, unfolding the definitions of TARGET-INST-LIST-P, MEMBER,
LISTP, CAR, CDR, and TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(TARGET-INST-LIST-P (APPEND (CDR Y) '(SUB)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(SUB)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding
TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P, APPEND, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(SUB)))),
which simplifies, expanding the definitions of TARGET-INST-LIST-P and APPEND,
to:
T.
That finishes the proof of *1.3.1.1, which, consequently, finishes the
proof of *1.3.1, which, in turn, finishes the proof of *1.3.
So next consider:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which is formula *1.2 above. We will try to prove it by induction. There are
six plausible inductions. They merge into three likely candidate inductions,
all of which are unflawed. However, one of these is more likely than the
others. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP D) (p A Y (CDR D)))
(p A Y D))
(IMPLIES (NOT (LISTP D)) (p A Y D))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT D)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to three new goals:
Case 3. (IMPLIES (AND (LISTP D)
(NOT (PLISTP (CDR D)))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which simplifies, unfolding PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP D)
(NOT (EQUAL (LENGTH (CDR D)) 0))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which simplifies, opening up the functions PLISTP and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP D))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which simplifies, opening up the definitions of PLISTP, LENGTH, and EQUAL,
to:
(IMPLIES (AND (NOT (LISTP D))
(EQUAL D NIL)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))).
But this again simplifies, expanding the function LISTP, to:
(IMPLIES (AND (TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))).
Name the above subgoal *1.2.1.
Perhaps we can prove it by induction. There are four plausible
inductions. They merge into two likely candidate inductions, both of which
are unflawed. Since both of these are equally likely, we will choose
arbitrarily. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) Y))
(p A Y))
(IMPLIES (NOT (LISTP A)) (p A Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
formulas:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (TARGET-INST-LIST-P (CDR A)))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))).
This simplifies, opening up the functions TARGET-INST-LIST-P, MEMBER, LISTP,
CAR, CDR, and TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(TARGET-INST-LIST-P (APPEND (CDR A) (APPEND Y '(MULT))))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))).
This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
definitions of TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P,
APPEND, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(MULT))))),
which simplifies, expanding the definitions of TARGET-INST-LIST-P, LISTP,
and APPEND, to:
(IMPLIES (AND (NOT (LISTP A))
(EQUAL A NIL)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(MULT)))).
This again simplifies, expanding LISTP, to:
(IMPLIES (TARGET-INST-LIST-P Y)
(TARGET-INST-LIST-P (APPEND Y '(MULT)))).
Name the above subgoal *1.2.1.1.
Perhaps we can prove it by induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (p (CDR Y)))
(p Y))
(IMPLIES (NOT (LISTP Y)) (p Y))).
Linear arithmetic and the lemma CDR-LESSP 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 three new
goals:
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (TARGET-INST-LIST-P (CDR Y)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(MULT)))),
which simplifies, unfolding the functions TARGET-INST-LIST-P, MEMBER, LISTP,
CAR, CDR, and TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(TARGET-INST-LIST-P (APPEND (CDR Y) '(MULT)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(MULT)))),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
functions TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P, APPEND,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(MULT)))).
This simplifies, opening up the definitions of TARGET-INST-LIST-P and APPEND,
to:
T.
That finishes the proof of *1.2.1.1, which, in turn, also finishes the
proof of *1.2.1, which also finishes the proof of *1.2.
So we now return to:
(IMPLIES (AND (PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
named *1.1 above. We will appeal to induction. Six inductions are suggested
by terms in the conjecture. They merge into three likely candidate inductions,
all of which are unflawed. However, one of these is more likely than the
others. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP D) (p A Y (CDR D)))
(p A Y D))
(IMPLIES (NOT (LISTP D)) (p A Y D))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT D) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates three new
goals:
Case 3. (IMPLIES (AND (LISTP D)
(NOT (PLISTP (CDR D)))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
which simplifies, unfolding PLISTP, to:
T.
Case 2. (IMPLIES (AND (LISTP D)
(NOT (EQUAL (LENGTH (CDR D)) 0))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
which simplifies, unfolding the functions PLISTP and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP D))
(PLISTP D)
(EQUAL (LENGTH D) 0)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
which simplifies, unfolding the functions PLISTP, LENGTH, and EQUAL, to:
(IMPLIES (AND (NOT (LISTP D))
(EQUAL D NIL)
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))).
However this again simplifies, unfolding LISTP, to the goal:
(IMPLIES (AND (TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))).
Give the above formula the name *1.1.1.
Perhaps we can prove it by induction. Four inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions,
both of which are unflawed. Since both of these are equally likely, we will
choose arbitrarily. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) Y))
(p A Y))
(IMPLIES (NOT (LISTP A)) (p A Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
goals:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (TARGET-INST-LIST-P (CDR A)))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))).
This simplifies, unfolding TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, and
TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(TARGET-INST-LIST-P (APPEND (CDR A) (APPEND Y '(ADD))))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding the
definitions of TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P,
APPEND, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(TARGET-INST-LIST-P A)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND A (APPEND Y '(ADD))))),
which simplifies, unfolding TARGET-INST-LIST-P, LISTP, and APPEND, to the
formula:
(IMPLIES (AND (NOT (LISTP A))
(EQUAL A NIL)
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(ADD)))).
But this again simplifies, unfolding the definition of LISTP, to:
(IMPLIES (TARGET-INST-LIST-P Y)
(TARGET-INST-LIST-P (APPEND Y '(ADD)))).
Call the above conjecture *1.1.1.1.
We will appeal to induction. The recursive terms in the conjecture
suggest two inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP Y) (p (CDR Y)))
(p Y))
(IMPLIES (NOT (LISTP Y)) (p Y))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
goals:
Case 3. (IMPLIES (AND (LISTP Y)
(NOT (TARGET-INST-LIST-P (CDR Y)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(ADD)))).
This simplifies, expanding the definitions of TARGET-INST-LIST-P, MEMBER,
LISTP, CAR, CDR, and TARGET-INST-P, to:
T.
Case 2. (IMPLIES (AND (LISTP Y)
(TARGET-INST-LIST-P (APPEND (CDR Y) '(ADD)))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(ADD)))).
This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
opening up TARGET-INST-LIST-P, MEMBER, LISTP, CAR, CDR, TARGET-INST-P,
APPEND, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Y))
(TARGET-INST-LIST-P Y))
(TARGET-INST-LIST-P (APPEND Y '(ADD)))).
This simplifies, unfolding TARGET-INST-LIST-P and APPEND, to:
T.
That finishes the proof of *1.1.1.1, which, in turn, also finishes the
proof of *1.1.1, which also finishes the proof of *1.1, which, in turn, also
finishes the proof of *1. Q.E.D.
[ 0.0 1.4 0.1 ]
COMPILE-PRESERVES-LEGALITY
(PROVE-LEMMA INTERPRETER-TARGET-APPEND
(REWRITE)
(EQUAL (INTERPRETER-TARGET (APPEND INST-LIST1 INST-LIST2)
S)
(INTERPRETER-TARGET INST-LIST2
(INTERPRETER-TARGET INST-LIST1 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 INST-LIST1)
(p (CDR INST-LIST1)
INST-LIST2
(SINGLE-STEP (CAR INST-LIST1) S)))
(p INST-LIST1 INST-LIST2 S))
(IMPLIES (NOT (LISTP INST-LIST1))
(p INST-LIST1 INST-LIST2 S))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT INST-LIST1) decreases according to the well-founded relation
LESSP in each induction step of the scheme. Note, however, the inductive
instance chosen for S. The above induction scheme leads to two new goals:
Case 2. (IMPLIES
(AND
(LISTP INST-LIST1)
(EQUAL
(INTERPRETER-TARGET (APPEND (CDR INST-LIST1) INST-LIST2)
(SINGLE-STEP (CAR INST-LIST1) S))
(INTERPRETER-TARGET INST-LIST2
(INTERPRETER-TARGET (CDR INST-LIST1)
(SINGLE-STEP (CAR INST-LIST1) S)))))
(EQUAL (INTERPRETER-TARGET (APPEND INST-LIST1 INST-LIST2)
S)
(INTERPRETER-TARGET INST-LIST2
(INTERPRETER-TARGET INST-LIST1 S)))),
which simplifies, applying the lemmas CAR-CONS and CDR-CONS, and opening up
the definitions of SINGLE-STEP, APPEND, EQUAL, and INTERPRETER-TARGET, to:
T.
Case 1. (IMPLIES
(NOT (LISTP INST-LIST1))
(EQUAL (INTERPRETER-TARGET (APPEND INST-LIST1 INST-LIST2)
S)
(INTERPRETER-TARGET INST-LIST2
(INTERPRETER-TARGET INST-LIST1 S)))),
which simplifies, unfolding the functions APPEND and INTERPRETER-TARGET, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
INTERPRETER-TARGET-APPEND
(DEFN COMPILER-CORRECTNESS-INDUCT
(EXP S)
(IF (EQUAL (LENGTH EXP) 3)
(AND (COMPILER-CORRECTNESS-INDUCT (CADR EXP)
S)
(COMPILER-CORRECTNESS-INDUCT (CADDR EXP)
(CONS (EVAL-S (CADR EXP)) S)))
T))
Linear arithmetic, the lemmas CAR-LESSEQP, CDR-LESSEQP, and CDR-LESSP,
and the definition of LENGTH inform us that the measure (COUNT EXP) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
COMPILER-CORRECTNESS-INDUCT
is accepted under the principle of definition. Note that:
(TRUEP (COMPILER-CORRECTNESS-INDUCT EXP S))
is a theorem.
[ 0.0 0.0 0.0 ]
COMPILER-CORRECTNESS-INDUCT
(PROVE-LEMMA COMPILER-CORRECTNESS-PLUS
(REWRITE)
(IMPLIES (EXP-P EXP)
(EQUAL (INTERPRETER-TARGET (COMPILE EXP) S)
(CONS (EVAL-S EXP) S)))
((INDUCT (COMPILER-CORRECTNESS-INDUCT EXP S))))
This formula can be simplified, using the abbreviations IMPLIES, NOT, OR, and
AND, to the following two new goals:
Case 2. (IMPLIES
(AND (EQUAL (LENGTH EXP) 3)
(IMPLIES (EXP-P (CADDR EXP))
(EQUAL (INTERPRETER-TARGET (COMPILE (CADDR EXP))
(CONS (EVAL-S (CADR EXP)) S))
(CONS (EVAL-S (CADDR EXP))
(CONS (EVAL-S (CADR EXP)) S))))
(IMPLIES (EXP-P (CADR EXP))
(EQUAL (INTERPRETER-TARGET (COMPILE (CADR EXP))
S)
(CONS (EVAL-S (CADR EXP)) S)))
(EXP-P EXP))
(EQUAL (INTERPRETER-TARGET (COMPILE EXP) S)
(CONS (EVAL-S EXP) S))).
This simplifies, applying the lemmas CAR-CONS, CDR-CONS, and
INTERPRETER-TARGET-APPEND, and unfolding the definitions of LENGTH, IMPLIES,
EQUAL, PLISTP, EXP-P, COMPILE, SINGLE-STEP, CAR, CDR, LISTP,
INTERPRETER-TARGET, and EVAL-S, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (LENGTH EXP) 3))
(EXP-P EXP))
(EQUAL (INTERPRETER-TARGET (COMPILE EXP) S)
(CONS (EVAL-S EXP) S))).
This simplifies, rewriting with CAR-CONS and CDR-CONS, and unfolding the
functions EXP-P, COMPILE, SINGLE-STEP, INTERPRETER-TARGET, LISTP, and EVAL-S,
to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
COMPILER-CORRECTNESS-PLUS
(PROVE-LEMMA COMPILER-CORRECTNESS
(REWRITE)
(IMPLIES (EXP-P EXP)
(EQUAL (EVAL-S EXP)
(CAR (INTERPRETER-TARGET (COMPILE EXP)
S)))))
This formula simplifies, appealing to the lemmas COMPILER-CORRECTNESS-PLUS and
CAR-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.3 ]
COMPILER-CORRECTNESS