(BOOT-STRAP NQTHM)
[ 0.0 0.1 0.0 ]
GROUND-ZERO
(ADD-SHELL CONS-SEQ-FIRST EMPTY-SEQ SEQ-P
((FIRST (NONE-OF) EMPTY-SEQ)
(FINAL (ONE-OF SEQ-P) EMPTY-SEQ)))
[ 0.0 0.0 0.0 ]
CONS-SEQ-FIRST
(DEFN EMPTY-SEQ-P
(S)
(OR (EQUAL S (EMPTY-SEQ))
(NOT (SEQ-P S))))
Note that (OR (FALSEP (EMPTY-SEQ-P S)) (TRUEP (EMPTY-SEQ-P S))) is a
theorem.
[ 0.0 0.0 0.0 ]
EMPTY-SEQ-P
(DEFN COERCE-SEQ
(S)
(IF (SEQ-P S) S (EMPTY-SEQ)))
Observe that (SEQ-P (COERCE-SEQ S)) is a theorem.
[ 0.0 0.0 0.0 ]
COERCE-SEQ
(DEFN CONS-SEQ-LAST
(S C)
(IF (EMPTY-SEQ-P S)
(CONS-SEQ-FIRST C S)
(CONS-SEQ-FIRST (FIRST S)
(CONS-SEQ-LAST (FINAL S) C))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to show that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, CONS-SEQ-LAST is accepted under the definitional principle. From the
definition we can conclude that (SEQ-P (CONS-SEQ-LAST S C)) is a theorem.
[ 0.0 0.0 0.0 ]
CONS-SEQ-LAST
(DEFN INITIAL
(S)
(IF (EMPTY-SEQ-P S)
(EMPTY-SEQ)
(IF (EQUAL (FINAL S) (EMPTY-SEQ))
(EMPTY-SEQ)
(CONS-SEQ-FIRST (FIRST S)
(INITIAL (FINAL S))))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
INITIAL is accepted under the principle of definition. Observe that
(SEQ-P (INITIAL S)) is a theorem.
[ 0.0 0.0 0.0 ]
INITIAL
(DEFN LAST
(S)
(IF (EMPTY-SEQ-P S)
(EMPTY-SEQ)
(IF (EQUAL (FINAL S) (EMPTY-SEQ))
(FIRST S)
(LAST (FINAL S)))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, LAST is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
LAST
(PROVE-LEMMA INITIAL-CONS-SEQ-LAST
(REWRITE)
(EQUAL (INITIAL (CONS-SEQ-LAST S C))
(IF (SEQ-P S) S (EMPTY-SEQ))))
This simplifies, trivially, to the following two new goals:
Case 2. (IMPLIES (NOT (SEQ-P S))
(EQUAL (INITIAL (CONS-SEQ-LAST S C))
(EMPTY-SEQ))).
This again simplifies, applying FINAL-TYPE-RESTRICTION and
FINAL-CONS-SEQ-FIRST, and unfolding the functions EMPTY-SEQ-P, CONS-SEQ-LAST,
EQUAL, SEQ-P, and INITIAL, to:
T.
Case 1. (IMPLIES (SEQ-P S)
(EQUAL (INITIAL (CONS-SEQ-LAST S C))
S)).
Call the above conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P S) (p S C))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(p (FINAL S) C))
(p S C))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S)
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 (EMPTY-SEQ-P S) (SEQ-P S))
(EQUAL (INITIAL (CONS-SEQ-LAST S C))
S)),
which simplifies, applying the lemma FINAL-CONS-SEQ-FIRST, and opening up
the definitions of EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST, EQUAL, and INITIAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (INITIAL (CONS-SEQ-LAST (FINAL S) C))
(FINAL S))
(SEQ-P S))
(EQUAL (INITIAL (CONS-SEQ-LAST S C))
S)),
which simplifies, rewriting with CONS-SEQ-FIRST-FIRST-FINAL,
FIRST-CONS-SEQ-FIRST, and FINAL-CONS-SEQ-FIRST, and opening up the functions
EMPTY-SEQ-P, CONS-SEQ-LAST, and INITIAL, to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(EQUAL (INITIAL (CONS-SEQ-LAST (FINAL S) C))
(FINAL S))
(SEQ-P S))
(NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C)
(EMPTY-SEQ)))),
which again simplifies, unfolding the function INITIAL, to the goal:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(EQUAL (EMPTY-SEQ) (FINAL S))
(SEQ-P S))
(NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C)
(EMPTY-SEQ)))).
This again simplifies, opening up the definitions of EMPTY-SEQ-P and
CONS-SEQ-LAST, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-CONS-SEQ-LAST
(PROVE-LEMMA INITIAL-NSEQ-P
(REWRITE)
(IMPLIES (NOT (SEQ-P S))
(EQUAL (INITIAL S) (EMPTY-SEQ))))
This conjecture simplifies, unfolding EMPTY-SEQ-P, INITIAL, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-NSEQ-P
(PROVE-LEMMA INITIAL-TYPE-RESTRICTION
(REWRITE)
(IMPLIES (NOT (SEQ-P S))
(EQUAL (CONS-SEQ-LAST S C)
(CONS-SEQ-LAST (EMPTY-SEQ) C))))
This formula simplifies, applying FINAL-TYPE-RESTRICTION, and unfolding
EMPTY-SEQ-P and CONS-SEQ-LAST, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-TYPE-RESTRICTION
(PROVE-LEMMA INITIAL-LESSP
(REWRITE)
(IMPLIES (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (INITIAL S))
(COUNT S))))
WARNING: Note that the proposed lemma INITIAL-LESSP is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
Call the conjecture *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 (EMPTY-SEQ-P S) (p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(p (FINAL S)))
(p S))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S)
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
goals:
Case 3. (IMPLIES (AND (EMPTY-SEQ-P S)
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (INITIAL S))
(COUNT S))).
This simplifies, opening up the definition of EMPTY-SEQ-P, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (INITIAL S))
(COUNT S))).
This simplifies, expanding EMPTY-SEQ-P, INITIAL, EQUAL, COUNT, and LESSP, to:
(IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(NOT (EQUAL (COUNT S) 0))).
Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to
eliminate (FINAL S) and (FIRST S). We employ the type restriction lemma
noted when FINAL was introduced to restrict the new variables. This
produces the new formula:
(IMPLIES (AND (SEQ-P X)
(EQUAL X (EMPTY-SEQ))
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ))))
(NOT (EQUAL (COUNT (CONS-SEQ-FIRST Z X))
0))),
which further simplifies, applying COUNT-CONS-SEQ-FIRST, and expanding the
functions SEQ-P and COUNT, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(LESSP (COUNT (INITIAL (FINAL S)))
(COUNT (FINAL S)))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (INITIAL S))
(COUNT S))).
This simplifies, applying COUNT-CONS-SEQ-FIRST and SUB1-ADD1, and opening up
EMPTY-SEQ-P, INITIAL, and LESSP, to two new conjectures:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(LESSP (COUNT (INITIAL (FINAL S)))
(COUNT (FINAL S)))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(NOT (EQUAL (COUNT S) 0))),
which again simplifies, using linear arithmetic and applying FINAL-LESSEQP,
to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(LESSP (COUNT (INITIAL (FINAL S)))
(COUNT (FINAL S)))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (PLUS (COUNT (FIRST S))
(COUNT (INITIAL (FINAL S))))
(SUB1 (COUNT S)))).
Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by
(CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We rely upon
the type restriction lemma noted when FINAL was introduced to constrain
the new variables. We must thus prove:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL X (EMPTY-SEQ)))
(LESSP (COUNT (INITIAL X)) (COUNT X))
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ))))
(LESSP (PLUS (COUNT Z) (COUNT (INITIAL X)))
(SUB1 (COUNT (CONS-SEQ-FIRST Z X))))).
This further simplifies, rewriting with the lemmas COUNT-CONS-SEQ-FIRST
and SUB1-ADD1, to the goal:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL X (EMPTY-SEQ)))
(LESSP (COUNT (INITIAL X)) (COUNT X)))
(LESSP (PLUS (COUNT Z) (COUNT (INITIAL X)))
(PLUS (COUNT Z) (COUNT X)))).
However this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-LESSP
(PROVE-LEMMA INITIAL-LESSEQP
(REWRITE)
(NOT (LESSP (COUNT S)
(COUNT (INITIAL S)))))
WARNING: Note that the proposed lemma INITIAL-LESSEQP is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
Name the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P S) (p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(p (FINAL S)))
(p S))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S)
(NOT (LESSP (COUNT S)
(COUNT (INITIAL S))))).
This simplifies, applying INITIAL-NSEQ-P, and unfolding the definitions of
EMPTY-SEQ-P, COUNT, INITIAL, LESSP, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT S)
(COUNT (INITIAL S))))),
which simplifies, unfolding the definitions of EMPTY-SEQ-P, INITIAL, EQUAL,
COUNT, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT (FINAL S))
(COUNT (INITIAL (FINAL S))))))
(NOT (LESSP (COUNT S)
(COUNT (INITIAL S))))),
which simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1, and
expanding the definitions of EMPTY-SEQ-P, INITIAL, and LESSP, to the
following two new goals:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT (FINAL S))
(COUNT (INITIAL (FINAL S))))))
(NOT (EQUAL (COUNT S) 0))).
However this again simplifies, using linear arithmetic and applying
FINAL-LESSEQP and INITIAL-LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT (FINAL S))
(COUNT (INITIAL (FINAL S))))))
(NOT (LESSP (SUB1 (COUNT S))
(PLUS (COUNT (FIRST S))
(COUNT (INITIAL (FINAL S))))))).
Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by
(CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We use the
type restriction lemma noted when FINAL was introduced to constrain the
new variables. This generates:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ)))
(NOT (EQUAL X (EMPTY-SEQ)))
(NOT (LESSP (COUNT X)
(COUNT (INITIAL X)))))
(NOT (LESSP (SUB1 (COUNT (CONS-SEQ-FIRST Z X)))
(PLUS (COUNT Z)
(COUNT (INITIAL X)))))).
This further simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1,
to:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL X (EMPTY-SEQ)))
(NOT (LESSP (COUNT X)
(COUNT (INITIAL X)))))
(NOT (LESSP (PLUS (COUNT Z) (COUNT X))
(PLUS (COUNT Z)
(COUNT (INITIAL X)))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-LESSEQP
(PROVE-LEMMA LAST-CONS-SEQ-LAST
(REWRITE)
(EQUAL (LAST (CONS-SEQ-LAST S C)) C))
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 (EMPTY-SEQ-P S) (p S C))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(p (FINAL S) C))
(p S C))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to two new conjectures:
Case 2. (IMPLIES (EMPTY-SEQ-P S)
(EQUAL (LAST (CONS-SEQ-LAST S C)) C)),
which simplifies, applying FIRST-CONS-SEQ-FIRST, FINAL-CONS-SEQ-FIRST, and
INITIAL-TYPE-RESTRICTION, and unfolding the functions EMPTY-SEQ-P,
CONS-SEQ-LAST, EQUAL, SEQ-P, and LAST, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (LAST (CONS-SEQ-LAST (FINAL S) C))
C))
(EQUAL (LAST (CONS-SEQ-LAST S C)) C)).
This simplifies, applying FIRST-CONS-SEQ-FIRST and FINAL-CONS-SEQ-FIRST, and
opening up the definitions of EMPTY-SEQ-P, CONS-SEQ-LAST, and LAST, to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(EQUAL (LAST (CONS-SEQ-LAST (FINAL S) C))
C)
(EQUAL (CONS-SEQ-LAST (FINAL S) C)
(EMPTY-SEQ)))
(EQUAL (FIRST S) C)).
However this again simplifies, unfolding LAST, to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(EQUAL (EMPTY-SEQ) C)
(EQUAL (CONS-SEQ-LAST (FINAL S) C)
(EMPTY-SEQ)))
(EQUAL (FIRST S) (EMPTY-SEQ))).
This again simplifies, obviously, to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(EQUAL (CONS-SEQ-LAST (FINAL S) (EMPTY-SEQ))
(EMPTY-SEQ)))
(EQUAL (FIRST S) (EMPTY-SEQ))).
Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to
eliminate (FINAL S) and (FIRST S). We rely upon the type restriction lemma
noted when FINAL was introduced to restrict the new variables. We would
thus like to prove:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ)))
(EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ))
(EMPTY-SEQ)))
(EQUAL Z (EMPTY-SEQ))),
which further simplifies, clearly, to the new conjecture:
(IMPLIES (AND (SEQ-P X)
(EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ))
(EMPTY-SEQ)))
(EQUAL Z (EMPTY-SEQ))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (SEQ-P X)
(NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ))
(EMPTY-SEQ)))),
which we will finally name *1.1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P X) (p X))
(IMPLIES (AND (NOT (EMPTY-SEQ-P X))
(p (FINAL X)))
(p X))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P 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 leads to the following two new goals:
Case 2. (IMPLIES (AND (EMPTY-SEQ-P X) (SEQ-P X))
(NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ))
(EMPTY-SEQ)))).
This simplifies, expanding the functions EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P X))
(NOT (EQUAL (CONS-SEQ-LAST (FINAL X) (EMPTY-SEQ))
(EMPTY-SEQ)))
(SEQ-P X))
(NOT (EQUAL (CONS-SEQ-LAST X (EMPTY-SEQ))
(EMPTY-SEQ)))).
This simplifies, unfolding the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST,
to:
T.
That finishes the proof of *1.1, which, in turn, also finishes the proof
of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LAST-CONS-SEQ-LAST
(PROVE-LEMMA LAST-NSEQ-P
(REWRITE)
(IMPLIES (NOT (SEQ-P S))
(EQUAL (LAST S) (EMPTY-SEQ))))
This conjecture simplifies, unfolding EMPTY-SEQ-P, LAST, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LAST-NSEQ-P
(PROVE-LEMMA LAST-LESSP
(REWRITE)
(IMPLIES (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (LAST S)) (COUNT S))))
WARNING: Note that the proposed lemma LAST-LESSP is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
Call the conjecture *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 (EMPTY-SEQ-P S) (p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(p (FINAL S)))
(p S))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to prove that the measure (COUNT S)
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
goals:
Case 3. (IMPLIES (AND (EMPTY-SEQ-P S)
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (LAST S)) (COUNT S))).
This simplifies, opening up the definition of EMPTY-SEQ-P, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (LAST S)) (COUNT S))).
This simplifies, expanding EMPTY-SEQ-P, LAST, and EQUAL, to:
(IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (FIRST S)) (COUNT S))),
which again simplifies, using linear arithmetic and rewriting with
FIRST-LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(LESSP (COUNT (LAST (FINAL S)))
(COUNT (FINAL S)))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (LAST S)) (COUNT S))).
This simplifies, opening up the functions EMPTY-SEQ-P and LAST, to:
(IMPLIES (AND (NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(LESSP (COUNT (LAST (FINAL S)))
(COUNT (FINAL S)))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(LESSP (COUNT (LAST (FINAL S)))
(COUNT S))),
which again simplifies, using linear arithmetic and applying FINAL-LESSEQP,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LAST-LESSP
(PROVE-LEMMA LAST-LESSEQP
(REWRITE)
(NOT (LESSP (COUNT S) (COUNT (LAST S)))))
WARNING: Note that the proposed lemma LAST-LESSEQP is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
Name the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P S) (p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(p (FINAL S)))
(p S))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S)
(NOT (LESSP (COUNT S) (COUNT (LAST S))))).
This simplifies, applying LAST-NSEQ-P, and unfolding the definitions of
EMPTY-SEQ-P, COUNT, LAST, LESSP, and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT S) (COUNT (LAST S))))),
which simplifies, unfolding the definitions of EMPTY-SEQ-P, LAST, and EQUAL,
to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT S) (COUNT (FIRST S))))).
However this again simplifies, using linear arithmetic and applying
FIRST-LESSEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT (FINAL S))
(COUNT (LAST (FINAL S))))))
(NOT (LESSP (COUNT S) (COUNT (LAST S))))).
This simplifies, unfolding EMPTY-SEQ-P and LAST, to:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(SEQ-P S)
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(NOT (LESSP (COUNT (FINAL S))
(COUNT (LAST (FINAL S))))))
(NOT (LESSP (COUNT S)
(COUNT (LAST (FINAL S)))))),
which again simplifies, using linear arithmetic and appealing to the lemma
FINAL-LESSEQP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
LAST-LESSEQP
(PROVE-LEMMA INITIAL-APPLY-EQUALS NIL
(IMPLIES (EQUAL X Y)
(EQUAL (INITIAL X) (INITIAL Y))))
This conjecture simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-APPLY-EQUALS
(PROVE-LEMMA LAST-APPLY-EQUALS NIL
(IMPLIES (EQUAL X Y)
(EQUAL (LAST X) (LAST Y))))
This conjecture simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LAST-APPLY-EQUALS
(PROVE-LEMMA CONS-SEQ-LAST-EQUAL
(REWRITE)
(EQUAL (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2))
(AND (IF (SEQ-P S1)
(IF (SEQ-P S2)
(EQUAL S1 S2)
(EQUAL S1 (EMPTY-SEQ)))
(IF (SEQ-P S2)
(EQUAL (EMPTY-SEQ) S2)
T))
(EQUAL C1 C2)))
((USE (INITIAL-APPLY-EQUALS (X (CONS-SEQ-LAST S1 C1))
(Y (CONS-SEQ-LAST S2 C2)))
(LAST-APPLY-EQUALS (X (CONS-SEQ-LAST S1 C1))
(Y (CONS-SEQ-LAST S2 C2))))))
This conjecture can be simplified, using the abbreviations AND and
LAST-CONS-SEQ-LAST, to the formula:
(IMPLIES (AND (IMPLIES (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2))
(EQUAL (INITIAL (CONS-SEQ-LAST S1 C1))
(INITIAL (CONS-SEQ-LAST S2 C2))))
(IMPLIES (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2))
(EQUAL C1 C2)))
(EQUAL (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2))
(AND (COND ((SEQ-P S1)
(IF (SEQ-P S2)
(EQUAL S1 S2)
(EQUAL S1 (EMPTY-SEQ))))
((SEQ-P S2) (EQUAL (EMPTY-SEQ) S2))
(T T))
(EQUAL C1 C2)))).
This simplifies, rewriting with INITIAL-CONS-SEQ-LAST,
INITIAL-TYPE-RESTRICTION, and CONS-SEQ-FIRST-EQUAL, and opening up IMPLIES,
AND, EQUAL, EMPTY-SEQ-P, CONS-SEQ-LAST, and SEQ-P, to five new formulas:
Case 5. (IMPLIES (AND (SEQ-P S2)
(SEQ-P S1)
(EQUAL S1 S2)
(NOT (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S1 C2))))
(NOT (EQUAL C1 C2))),
which again simplifies, clearly, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2)))
(NOT (SEQ-P S1))
(EQUAL (EMPTY-SEQ) S2))
(NOT (EQUAL C1 C2))).
This again simplifies, rewriting with INITIAL-TYPE-RESTRICTION, and
expanding EMPTY-SEQ-P and CONS-SEQ-LAST, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2)))
(SEQ-P S1)
(SEQ-P S2)
(EQUAL S1 S2))
(NOT (EQUAL C1 C2))).
This again simplifies, clearly, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2)))
(NOT (SEQ-P S2))
(EQUAL S1 (EMPTY-SEQ)))
(NOT (EQUAL C1 C2))).
However this again simplifies, applying INITIAL-TYPE-RESTRICTION, and
unfolding EMPTY-SEQ-P and CONS-SEQ-LAST, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (CONS-SEQ-LAST S1 C1)
(CONS-SEQ-LAST S2 C2)))
(NOT (SEQ-P S1))
(NOT (SEQ-P S2)))
(NOT (EQUAL C1 C2))).
But this again simplifies, rewriting with INITIAL-TYPE-RESTRICTION, and
unfolding the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CONS-SEQ-LAST-EQUAL
(PROVE-LEMMA CONS-SEQ-LAST-INITIAL-LAST
(REWRITE)
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
(IF (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
S
(CONS-SEQ-LAST (EMPTY-SEQ)
(EMPTY-SEQ)))))
This formula simplifies, expanding the definitions of NOT, AND, and
CONS-SEQ-LAST, to the following three new conjectures:
Case 3. (IMPLIES (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)).
Give the above formula the name *1.
Case 2. (IMPLIES (NOT (SEQ-P S))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
(CONS-SEQ-FIRST (EMPTY-SEQ)
(EMPTY-SEQ)))).
However this again simplifies, applying INITIAL-NSEQ-P and LAST-NSEQ-P, and
unfolding the functions CONS-SEQ-LAST and EQUAL, to:
T.
Case 1. (IMPLIES (EQUAL S (EMPTY-SEQ))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
(CONS-SEQ-FIRST (EMPTY-SEQ)
(EMPTY-SEQ)))).
This again simplifies, opening up the definitions of INITIAL, LAST,
CONS-SEQ-LAST, and EQUAL, to:
T.
So next consider:
(IMPLIES (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)),
which we named *1 above. Let us appeal to the induction principle. 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 (EMPTY-SEQ-P S) (p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ)))
(p S))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(p (FINAL S)))
(p S))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P establish that the measure (COUNT S) 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 (EMPTY-SEQ-P S)
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)),
which simplifies, opening up the function EMPTY-SEQ-P, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)),
which simplifies, opening up the definitions of EMPTY-SEQ-P, INITIAL, EQUAL,
LAST, and CONS-SEQ-LAST, to the conjecture:
(IMPLIES (AND (EQUAL (FINAL S) (EMPTY-SEQ))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-FIRST (FIRST S) (EMPTY-SEQ))
S)).
Appealing to the lemma FIRST-FINAL-ELIM, we now replace S by
(CONS-SEQ-FIRST Z X) to eliminate (FINAL S) and (FIRST S). We rely upon the
type restriction lemma noted when FINAL was introduced to constrain the new
variables. We must thus prove:
(IMPLIES (AND (SEQ-P X)
(EQUAL X (EMPTY-SEQ))
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ))))
(EQUAL (CONS-SEQ-FIRST Z (EMPTY-SEQ))
(CONS-SEQ-FIRST Z X))).
This further simplifies, clearly, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (FINAL S) (EMPTY-SEQ)))
(EQUAL (CONS-SEQ-LAST (INITIAL (FINAL S))
(LAST (FINAL S)))
(FINAL S))
(SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)).
This simplifies, rewriting with CONS-SEQ-FIRST-FIRST-FINAL,
FINAL-CONS-SEQ-FIRST, and FIRST-CONS-SEQ-FIRST, and expanding the
definitions of EMPTY-SEQ-P, INITIAL, LAST, and CONS-SEQ-LAST, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CONS-SEQ-LAST-INITIAL-LAST
(PROVE-LEMMA INITIAL-LAST-ELIM
(ELIM)
(IMPLIES (AND (SEQ-P S)
(NOT (EQUAL S (EMPTY-SEQ))))
(EQUAL (CONS-SEQ-LAST (INITIAL S) (LAST S))
S)))
This conjecture simplifies, applying CONS-SEQ-LAST-INITIAL-LAST, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INITIAL-LAST-ELIM
(PROVE-LEMMA COUNT-CONS-SEQ-LAST
(REWRITE)
(EQUAL (COUNT (CONS-SEQ-LAST S C))
(ADD1 (PLUS (IF (SEQ-P S) (COUNT S) 0)
(COUNT C)))))
This formula simplifies, trivially, to two new formulas:
Case 2. (IMPLIES (NOT (SEQ-P S))
(EQUAL (COUNT (CONS-SEQ-LAST S C))
(ADD1 (PLUS 0 (COUNT C))))),
which again simplifies, appealing to the lemmas INITIAL-TYPE-RESTRICTION,
COUNT-CONS-SEQ-FIRST, and ADD1-EQUAL, and unfolding the functions
EMPTY-SEQ-P, CONS-SEQ-LAST, SEQ-P, COUNT, EQUAL, and PLUS, to:
(IMPLIES (NOT (SEQ-P S))
(EQUAL (PLUS (COUNT C) 0) (COUNT C))).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (SEQ-P S)
(EQUAL (COUNT (CONS-SEQ-LAST S C))
(ADD1 (PLUS (COUNT S) (COUNT C))))),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P S) (p S C))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(p (FINAL S) C))
(p S C))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to show that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to two new formulas:
Case 2. (IMPLIES (AND (EMPTY-SEQ-P S) (SEQ-P S))
(EQUAL (COUNT (CONS-SEQ-LAST S C))
(ADD1 (PLUS (COUNT S) (COUNT C))))),
which simplifies, rewriting with COUNT-CONS-SEQ-FIRST and ADD1-EQUAL, and
opening up EMPTY-SEQ-P, SEQ-P, CONS-SEQ-LAST, COUNT, EQUAL, and PLUS, to:
(IMPLIES (EQUAL S (EMPTY-SEQ))
(EQUAL (PLUS (COUNT C) 0) (COUNT C))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(EQUAL (COUNT (CONS-SEQ-LAST (FINAL S) C))
(ADD1 (PLUS (COUNT (FINAL S)) (COUNT C))))
(SEQ-P S))
(EQUAL (COUNT (CONS-SEQ-LAST S C))
(ADD1 (PLUS (COUNT S) (COUNT C))))),
which simplifies, applying COUNT-CONS-SEQ-FIRST and ADD1-EQUAL, and opening
up EMPTY-SEQ-P and CONS-SEQ-LAST, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL S (EMPTY-SEQ)))
(EQUAL (COUNT (CONS-SEQ-LAST (FINAL S) C))
(ADD1 (PLUS (COUNT (FINAL S)) (COUNT C))))
(SEQ-P S))
(EQUAL (PLUS (COUNT (FIRST S))
(COUNT (CONS-SEQ-LAST (FINAL S) C)))
(PLUS (COUNT S) (COUNT C)))).
Applying the lemma FIRST-FINAL-ELIM, replace S by (CONS-SEQ-FIRST Z X) to
eliminate (FINAL S) and (FIRST S). We use the type restriction lemma noted
when FINAL was introduced to restrict the new variables. We would thus like
to prove:
(IMPLIES (AND (SEQ-P X)
(NOT (EQUAL (CONS-SEQ-FIRST Z X)
(EMPTY-SEQ)))
(EQUAL (COUNT (CONS-SEQ-LAST X C))
(ADD1 (PLUS (COUNT X) (COUNT C)))))
(EQUAL (PLUS (COUNT Z)
(COUNT (CONS-SEQ-LAST X C)))
(PLUS (COUNT (CONS-SEQ-FIRST Z X))
(COUNT C)))),
which further simplifies, rewriting with COUNT-CONS-SEQ-FIRST and SUB1-ADD1,
and unfolding PLUS, to the new conjecture:
(IMPLIES (AND (SEQ-P X)
(EQUAL (COUNT (CONS-SEQ-LAST X C))
(ADD1 (PLUS (COUNT X) (COUNT C)))))
(EQUAL (PLUS (COUNT Z)
(COUNT (CONS-SEQ-LAST X C)))
(ADD1 (PLUS (PLUS (COUNT Z) (COUNT X))
(COUNT C))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
COUNT-CONS-SEQ-LAST
(PROVE-LEMMA CONS-SEQ-LAST-NOT-EMPTY-SEQ
(REWRITE)
(NOT (EQUAL (CONS-SEQ-LAST S C)
(EMPTY-SEQ))))
Give the conjecture the name *1.
Let us appeal to the induction principle. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY-SEQ-P S) (p S C))
(IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(p (FINAL S) C))
(p S C))).
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P establish that the measure (COUNT S) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme generates two new conjectures:
Case 2. (IMPLIES (EMPTY-SEQ-P S)
(NOT (EQUAL (CONS-SEQ-LAST S C)
(EMPTY-SEQ)))),
which simplifies, applying INITIAL-TYPE-RESTRICTION, and opening up
EMPTY-SEQ-P and CONS-SEQ-LAST, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY-SEQ-P S))
(NOT (EQUAL (CONS-SEQ-LAST (FINAL S) C)
(EMPTY-SEQ))))
(NOT (EQUAL (CONS-SEQ-LAST S C)
(EMPTY-SEQ)))).
This simplifies, opening up the definitions of EMPTY-SEQ-P and CONS-SEQ-LAST,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CONS-SEQ-LAST-NOT-EMPTY-SEQ
(DEFN REVERSE1
(S)
(IF (EMPTY-SEQ-P S)
S
(CONS-SEQ-LAST (REVERSE1 (FINAL S))
(FIRST S))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, REVERSE1 is accepted under the principle of definition. From the
definition we can conclude that:
(OR (SEQ-P (REVERSE1 S))
(EQUAL (REVERSE1 S) S))
is a theorem.
[ 0.0 0.0 0.0 ]
REVERSE1
(DEFN REVERSE2
(S)
(IF (EMPTY-SEQ-P S)
S
(CONS-SEQ-FIRST (LAST S)
(REVERSE2 (INITIAL S)))))
Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the
definition of EMPTY-SEQ-P can be used to establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, REVERSE2 is accepted under the principle of definition. From the
definition we can conclude that:
(OR (SEQ-P (REVERSE2 S))
(EQUAL (REVERSE2 S) S))
is a theorem.
[ 0.0 0.0 0.0 ]
REVERSE2
(DEFN CONCAT1
(S1 S2)
(IF (EMPTY-SEQ-P S1)
(COERCE-SEQ S2)
(CONS-SEQ-FIRST (FIRST S1)
(CONCAT1 (FINAL S1) S2))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S1) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CONCAT1 is accepted under the definitional principle. Observe that
(SEQ-P (CONCAT1 S1 S2)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT1
(DEFN CONCAT2
(S1 S2)
(IF (EMPTY-SEQ-P S2)
(COERCE-SEQ S1)
(CONCAT2 (CONS-SEQ-LAST S1 (FIRST S2))
(FINAL S2))))
Linear arithmetic, the lemmas FINAL-LESSEQP and FINAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S2) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CONCAT2 is accepted under the definitional principle. Observe that
(SEQ-P (CONCAT2 S1 S2)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT2
(DEFN CONCAT3
(S1 S2)
(IF (EMPTY-SEQ-P S2)
(COERCE-SEQ S1)
(CONS-SEQ-LAST (CONCAT3 S1 (INITIAL S2))
(LAST S2))))
Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S2) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CONCAT3 is accepted under the definitional principle. Observe that
(SEQ-P (CONCAT3 S1 S2)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT3
(DEFN CONCAT4
(S1 S2)
(IF (EMPTY-SEQ-P S1)
(COERCE-SEQ S2)
(CONCAT4 (INITIAL S1)
(CONS-SEQ-FIRST (LAST S1) S2))))
Linear arithmetic, the lemmas INITIAL-LESSEQP and INITIAL-LESSP, and the
definition of EMPTY-SEQ-P inform us that the measure (COUNT S1) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CONCAT4 is accepted under the definitional principle. Observe that
(SEQ-P (CONCAT4 S1 S2)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT4