(BOOT-STRAP NQTHM)
[ 0.0 0.1 0.0 ]
GROUND-ZERO
(DEFN ROTATE
(N LST)
(IF (ZEROP N)
LST
(ROTATE (SUB1 N)
(APPEND (CDR LST) (LIST (CAR LST))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, ROTATE is accepted under the
principle of definition. From the definition we can conclude that:
(OR (LISTP (ROTATE N LST))
(EQUAL (ROTATE N LST) LST))
is a theorem.
[ 0.0 0.0 0.0 ]
ROTATE
(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 PROPERP
(X)
(IF (LISTP X)
(PROPERP (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, PROPERP is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (PROPERP X))
(TRUEP (PROPERP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
PROPERP
(DEFN FIRSTN
(N LST)
(IF (ZEROP N)
NIL
(CONS (CAR LST)
(FIRSTN (SUB1 N) (CDR LST)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, FIRSTN is accepted under the
definitional principle. Note that:
(OR (LITATOM (FIRSTN N LST))
(LISTP (FIRSTN N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
FIRSTN
(DEFN NTHCDR
(N LST)
(IF (ZEROP N)
LST
(NTHCDR (SUB1 N) (CDR LST))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, NTHCDR is accepted under the
principle of definition.
[ 0.0 0.0 0.0 ]
NTHCDR
(PROVE-LEMMA ASSOCIATIVITY-OF-APPEND
(REWRITE)
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z))))
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 X) (p (CDR X) Y Z))
(p X Y Z))
(IMPLIES (NOT (LISTP X)) (p X Y Z))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to two
new goals:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (APPEND (APPEND (CDR X) Y) Z)
(APPEND (CDR X) (APPEND Y Z))))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, applying the lemmas CDR-CONS and CAR-CONS, and opening up
the definition of APPEND, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (APPEND (APPEND X Y) Z)
(APPEND X (APPEND Y Z)))),
which simplifies, unfolding the function APPEND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ASSOCIATIVITY-OF-APPEND
(PROVE-LEMMA APPEND-NIL
(REWRITE)
(IMPLIES (PROPERP X)
(EQUAL (APPEND X NIL) X)))
Name the conjecture *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 X) (p (CDR X)))
(p X))
(IMPLIES (NOT (LISTP X)) (p X))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following three new
formulas:
Case 3. (IMPLIES (AND (LISTP X)
(NOT (PROPERP (CDR X)))
(PROPERP X))
(EQUAL (APPEND X NIL) X)).
This simplifies, expanding the definition of PROPERP, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (APPEND (CDR X) NIL) (CDR X))
(PROPERP X))
(EQUAL (APPEND X NIL) X)).
This simplifies, applying CONS-CAR-CDR, and expanding the definitions of
PROPERP and APPEND, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X)) (PROPERP X))
(EQUAL (APPEND X NIL) X)),
which simplifies, opening up PROPERP, APPEND, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.2 0.0 ]
APPEND-NIL
(DEFN ROTATE-APPEND-INDUCTION
(N LST EXTRA)
(IF (OR (EQUAL N 0) (NOT (NUMBERP N)))
T
(IF (NLISTP LST)
T
(ROTATE-APPEND-INDUCTION (SUB1 N)
(CDR LST)
(APPEND EXTRA (LIST (CAR LST)))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of NLISTP,
OR, and NOT establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence,
ROTATE-APPEND-INDUCTION is accepted under the principle of definition. The
definition of ROTATE-APPEND-INDUCTION can be justified in another way. Linear
arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of
NLISTP, OR, and NOT establish that the measure (COUNT LST) decreases according
to the well-founded relation LESSP in each recursive call. From the
definition we can conclude that (TRUEP (ROTATE-APPEND-INDUCTION N LST EXTRA))
is a theorem.
[ 0.0 0.0 0.0 ]
ROTATE-APPEND-INDUCTION
(PROVE-LEMMA PROPERP-APPEND
(REWRITE)
(EQUAL (PROPERP (APPEND X Y))
(PROPERP Y)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest two inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X) (p (CDR X) Y))
(p X Y))
(IMPLIES (NOT (LISTP X)) (p X Y))).
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 induction step of the scheme. The above induction scheme generates the
following two new formulas:
Case 2. (IMPLIES (AND (LISTP X)
(EQUAL (PROPERP (APPEND (CDR X) Y))
(PROPERP Y)))
(EQUAL (PROPERP (APPEND X Y))
(PROPERP Y))).
This simplifies, applying CDR-CONS, and expanding the functions APPEND and
PROPERP, to:
T.
Case 1. (IMPLIES (NOT (LISTP X))
(EQUAL (PROPERP (APPEND X Y))
(PROPERP Y))),
which simplifies, opening up the function APPEND, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PROPERP-APPEND
(PROVE-LEMMA ROTATE-APPEND NIL
(IMPLIES (AND (PROPERP EXTRA)
(NOT (LESSP (LENGTH LST) N)))
(EQUAL (ROTATE N (APPEND LST EXTRA))
(APPEND (NTHCDR N LST)
(APPEND EXTRA (FIRSTN N LST)))))
((INDUCT (ROTATE-APPEND-INDUCTION N LST EXTRA))))
This conjecture can be simplified, using the abbreviations NLISTP, IMPLIES,
NOT, OR, AND, ASSOCIATIVITY-OF-APPEND, and PROPERP-APPEND, to three new
formulas:
Case 3. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(PROPERP EXTRA)
(NOT (LESSP (LENGTH LST) N)))
(EQUAL (ROTATE N (APPEND LST EXTRA))
(APPEND (NTHCDR N LST)
(APPEND EXTRA (FIRSTN N LST))))),
which simplifies, rewriting with APPEND-NIL, and unfolding the definitions
of NOT, OR, EQUAL, LESSP, ROTATE, NTHCDR, and FIRSTN, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LISTP LST))
(PROPERP EXTRA)
(NOT (LESSP (LENGTH LST) N)))
(EQUAL (ROTATE N (APPEND LST EXTRA))
(APPEND (NTHCDR N LST)
(APPEND EXTRA (FIRSTN N LST))))).
This simplifies, opening up the definitions of LENGTH, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(LISTP LST)
(IMPLIES
(AND (PROPERP (LIST (CAR LST)))
(NOT (LESSP (LENGTH (CDR LST)) (SUB1 N))))
(EQUAL (ROTATE (SUB1 N)
(APPEND (CDR LST)
(APPEND EXTRA (LIST (CAR LST)))))
(APPEND (NTHCDR (SUB1 N) (CDR LST))
(APPEND EXTRA
(APPEND (LIST (CAR LST))
(FIRSTN (SUB1 N) (CDR LST)))))))
(PROPERP EXTRA)
(NOT (LESSP (LENGTH LST) N)))
(EQUAL (ROTATE N (APPEND LST EXTRA))
(APPEND (NTHCDR N LST)
(APPEND EXTRA (FIRSTN N LST))))).
This simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, SUB1-ADD1,
and ASSOCIATIVITY-OF-APPEND, and opening up the definitions of PROPERP, NOT,
AND, APPEND, LISTP, IMPLIES, LENGTH, LESSP, ROTATE, NTHCDR, and FIRSTN, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ROTATE-APPEND
(PROVE-LEMMA NTHCDR-LENGTH
(REWRITE)
(IMPLIES (PROPERP LST)
(EQUAL (NTHCDR (LENGTH LST) LST)
NIL)))
Call the conjecture *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 LST) (p (CDR LST)))
(p LST))
(IMPLIES (NOT (LISTP LST)) (p LST))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove 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 three
new goals:
Case 3. (IMPLIES (AND (LISTP LST)
(NOT (PROPERP (CDR LST)))
(PROPERP LST))
(EQUAL (NTHCDR (LENGTH LST) LST)
NIL)),
which simplifies, opening up the definition of PROPERP, to:
T.
Case 2. (IMPLIES (AND (LISTP LST)
(EQUAL (NTHCDR (LENGTH (CDR LST)) (CDR LST))
NIL)
(PROPERP LST))
(EQUAL (NTHCDR (LENGTH LST) LST)
NIL)),
which simplifies, applying SUB1-ADD1, and unfolding PROPERP, LENGTH, NTHCDR,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP LST)) (PROPERP LST))
(EQUAL (NTHCDR (LENGTH LST) LST)
NIL)).
This simplifies, expanding the functions PROPERP, LENGTH, NTHCDR, and EQUAL,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
NTHCDR-LENGTH
(PROVE-LEMMA FIRSTN-LENGTH
(REWRITE)
(IMPLIES (PROPERP LST)
(EQUAL (FIRSTN (LENGTH LST) LST)
LST)))
Name the conjecture *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 LST) (p (CDR LST)))
(p LST))
(IMPLIES (NOT (LISTP LST)) (p LST))).
Linear arithmetic and the lemma CDR-LESSP 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 produces the
following three new formulas:
Case 3. (IMPLIES (AND (LISTP LST)
(NOT (PROPERP (CDR LST)))
(PROPERP LST))
(EQUAL (FIRSTN (LENGTH LST) LST)
LST)).
This simplifies, expanding the definition of PROPERP, to:
T.
Case 2. (IMPLIES (AND (LISTP LST)
(EQUAL (FIRSTN (LENGTH (CDR LST)) (CDR LST))
(CDR LST))
(PROPERP LST))
(EQUAL (FIRSTN (LENGTH LST) LST)
LST)).
This simplifies, applying CONS-CAR-CDR and SUB1-ADD1, and expanding the
definitions of PROPERP, LENGTH, and FIRSTN, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP LST)) (PROPERP LST))
(EQUAL (FIRSTN (LENGTH LST) LST)
LST)),
which simplifies, opening up PROPERP, LENGTH, FIRSTN, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FIRSTN-LENGTH
(PROVE-LEMMA ROTATE-LENGTH NIL
(IMPLIES (PROPERP LST)
(EQUAL (ROTATE (LENGTH LST) LST) LST))
((USE (ROTATE-APPEND (EXTRA NIL)
(N (LENGTH LST))))))
This conjecture simplifies, applying the lemmas APPEND-NIL, NTHCDR-LENGTH, and
FIRSTN-LENGTH, and expanding the definitions of PROPERP, NOT, AND, LISTP,
APPEND, and IMPLIES, to:
(IMPLIES (AND (LESSP (LENGTH LST) (LENGTH LST))
(PROPERP LST))
(EQUAL (ROTATE (LENGTH LST) LST)
LST)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ROTATE-LENGTH