(BOOT-STRAP NQTHM)
[ 0.0 0.2 0.0 ]
GROUND-ZERO
(DEFN ASCII-TABLE NIL
'((TAB . 9)
(NEWLINE . 10)
(PAGE . 12)
(SPACE . 32)
(RUBOUT . 127)
(EXCLAMATION-POINT . 33)
(DOUBLE-QUOTE . 34)
(NUMBER-SIGN . 35)
(DOLLAR-SIGN . 36)
(PERCENT-SIGN . 37)
(AMPERSAND . 38)
(SINGLE-QUOTE . 39)
(OPEN-PAREN . 40)
(CLOSE-PAREN . 41)
(ASTERISK . 42)
(PLUS-SIGN . 43)
(COMMA . 44)
(MINUS-SIGN . 45)
(DOT . 46)
(SLASH . 47)
(DIGIT-ZERO . 48)
(DIGIT-ONE . 49)
(DIGIT-TWO . 50)
(DIGIT-THREE . 51)
(DIGIT-FOUR . 52)
(DIGIT-FIVE . 53)
(DIGIT-SIX . 54)
(DIGIT-SEVEN . 55)
(DIGIT-EIGHT . 56)
(DIGIT-NINE . 57)
(COLON . 58)
(SEMICOLON . 59)
(LESS-THAN-SIGN . 60)
(EQUAL-SIGN . 61)
(GREATER-THAN-SIGN . 62)
(QUESTION-MARK . 63)
(AT-SIGN . 64)
(UPPER-A . 65)
(UPPER-B . 66)
(UPPER-C . 67)
(UPPER-D . 68)
(UPPER-E . 69)
(UPPER-F . 70)
(UPPER-G . 71)
(UPPER-H . 72)
(UPPER-I . 73)
(UPPER-J . 74)
(UPPER-K . 75)
(UPPER-L . 76)
(UPPER-M . 77)
(UPPER-N . 78)
(UPPER-O . 79)
(UPPER-P . 80)
(UPPER-Q . 81)
(UPPER-R . 82)
(UPPER-S . 83)
(UPPER-T . 84)
(UPPER-U . 85)
(UPPER-V . 86)
(UPPER-W . 87)
(UPPER-X . 88)
(UPPER-Y . 89)
(UPPER-Z . 90)
(OPEN-BRACKET . 91)
(BACKSLASH . 92)
(CLOSE-BRACKET . 93)
(UPARROW . 94)
(UNDERSCORE . 95)
(BACKQUOTE . 96)
(LOWER-A . 97)
(LOWER-B . 98)
(LOWER-C . 99)
(LOWER-D . 100)
(LOWER-E . 101)
(LOWER-F . 102)
(LOWER-G . 103)
(LOWER-H . 104)
(LOWER-I . 105)
(LOWER-J . 106)
(LOWER-K . 107)
(LOWER-L . 108)
(LOWER-M . 109)
(LOWER-N . 110)
(LOWER-O . 111)
(LOWER-P . 112)
(LOWER-Q . 113)
(LOWER-R . 114)
(LOWER-S . 115)
(LOWER-T . 116)
(LOWER-U . 117)
(LOWER-V . 118)
(LOWER-W . 119)
(LOWER-X . 120)
(LOWER-Y . 121)
(LOWER-Z . 122)
(OPEN-BRACE . 123)
(VERTICAL-BAR . 124)
(CLOSE-BRACE . 125)
(TILDE . 126)))
From the definition we can conclude that (LISTP (ASCII-TABLE)) is a
theorem.
[ 0.0 0.0 0.0 ]
ASCII-TABLE
(DEFN ASCII-LIST
(LST)
(IF (NLISTP LST)
NIL
(CONS (CDR (ASSOC (CAR LST) (ASCII-TABLE)))
(ASCII-LIST (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, ASCII-LIST is accepted under the principle of definition. Note that:
(OR (LITATOM (ASCII-LIST LST))
(LISTP (ASCII-LIST LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ASCII-LIST
(DEFN ASCII
(X)
(IF (LITATOM X)
(CDR (ASSOC X (ASCII-TABLE)))
(ASCII-LIST X)))
[ 0.0 0.0 0.0 ]
ASCII
(DEFN UPPER-DIGITS NIL
(ASCII '(DIGIT-ZERO DIGIT-ONE DIGIT-TWO DIGIT-THREE DIGIT-FOUR
DIGIT-FIVE DIGIT-SIX DIGIT-SEVEN DIGIT-EIGHT
DIGIT-NINE UPPER-A UPPER-B UPPER-C UPPER-D UPPER-E
UPPER-F)))
[ 0.0 0.0 0.0 ]
UPPER-DIGITS
(DEFN CDRN
(N LST)
(IF (ZEROP N)
LST
(CDRN (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, CDRN is accepted under the
principle of definition.
[ 0.0 0.0 0.0 ]
CDRN
(DEFN CADRN
(N LST)
(CAR (CDRN N LST)))
[ 0.0 0.0 0.0 ]
CADRN
(DEFN LIST1 (X) (CONS X NIL))
Observe that (LISTP (LIST1 X)) is a theorem.
[ 0.0 0.0 0.0 ]
LIST1
(DEFN LIST2 (X Y) (CONS X (LIST1 Y)))
Note that (LISTP (LIST2 X Y)) is a theorem.
[ 0.0 0.0 0.0 ]
LIST2
(DEFN LIST3
(X Y Z)
(CONS X (LIST2 Y Z)))
Note that (LISTP (LIST3 X Y Z)) is a theorem.
[ 0.0 0.0 0.0 ]
LIST3
(DEFN FIRST-N
(N LST)
(IF (ZEROP N)
NIL
(CONS (CAR LST)
(FIRST-N (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, FIRST-N is accepted under the
definitional principle. Note that:
(OR (LITATOM (FIRST-N N LST))
(LISTP (FIRST-N N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
FIRST-N
(DEFN BASE-N-DIGIT-CHARACTER
(N C)
(AND (LEQ N 16)
(MEMBER C
(FIRST-N N (UPPER-DIGITS)))))
Observe that:
(OR (FALSEP (BASE-N-DIGIT-CHARACTER N C))
(TRUEP (BASE-N-DIGIT-CHARACTER N C)))
is a theorem.
[ 0.0 0.0 0.0 ]
BASE-N-DIGIT-CHARACTER
(DEFN POSITION
(X LST)
(IF (NLISTP LST)
0
(IF (EQUAL X (CAR LST))
0
(ADD1 (POSITION X (CDR LST))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
POSITION is accepted under the definitional principle. From the definition we
can conclude that (NUMBERP (POSITION X LST)) is a theorem.
[ 0.0 0.0 0.0 ]
POSITION
(DEFN BASE-N-DIGIT-VALUE
(C)
(POSITION C (UPPER-DIGITS)))
From the definition we can conclude that (NUMBERP (BASE-N-DIGIT-VALUE C))
is a theorem.
[ 0.0 0.0 0.0 ]
BASE-N-DIGIT-VALUE
(DEFN ALL-BASE-N-DIGIT-CHARACTERS
(N LST)
(IF (NLISTP LST)
T
(AND (BASE-N-DIGIT-CHARACTER N (CAR LST))
(ALL-BASE-N-DIGIT-CHARACTERS N
(CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
ALL-BASE-N-DIGIT-CHARACTERS
is accepted under the principle of definition. Note that:
(OR (FALSEP (ALL-BASE-N-DIGIT-CHARACTERS N LST))
(TRUEP (ALL-BASE-N-DIGIT-CHARACTERS N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-BASE-N-DIGIT-CHARACTERS
(DEFN BASE-N-DIGIT-SEQUENCE
(N LST)
(AND (LISTP LST)
(ALL-BASE-N-DIGIT-CHARACTERS N LST)))
From the definition we can conclude that:
(OR (FALSEP (BASE-N-DIGIT-SEQUENCE N LST))
(TRUEP (BASE-N-DIGIT-SEQUENCE N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
BASE-N-DIGIT-SEQUENCE
(DEFN OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE
(N LST)
(OR (BASE-N-DIGIT-SEQUENCE N LST)
(AND (LISTP LST)
(AND (OR (EQUAL (CAR LST) (ASCII 'PLUS-SIGN))
(EQUAL (CAR LST)
(ASCII 'MINUS-SIGN)))
(BASE-N-DIGIT-SEQUENCE N
(CDR LST))))))
Observe that:
(OR (FALSEP (OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE N LST))
(TRUEP (OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE
(DEFN LENGTH
(LST)
(IF (NLISTP LST)
0
(ADD1 (LENGTH (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
LENGTH is accepted under the principle of definition. From the definition we
can conclude that (NUMBERP (LENGTH LST)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(DEFN EXP
(I J)
(IF (ZEROP J)
1
(TIMES I (EXP I (SUB1 J)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT J) decreases according to the well-founded
relation LESSP in each recursive call. Hence, EXP is accepted under the
definitional principle. From the definition we can conclude that
(NUMBERP (EXP I J)) is a theorem.
[ 0.0 0.0 0.0 ]
EXP
(DEFN BASE-N-VALUE
(N LST)
(IF (NLISTP LST)
0
(PLUS (TIMES (BASE-N-DIGIT-VALUE (CAR LST))
(EXP N (LENGTH (CDR LST))))
(BASE-N-VALUE N (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
BASE-N-VALUE is accepted under the definitional principle. Note that:
(NUMBERP (BASE-N-VALUE N LST))
is a theorem.
[ 0.0 0.0 0.0 ]
BASE-N-VALUE
(DEFN NUMERATOR-SEQUENCE
(LST)
(IF (NLISTP LST)
NIL
(IF (EQUAL (CAR LST) (ASCII 'SLASH))
NIL
(CONS (CAR LST)
(NUMERATOR-SEQUENCE (CDR LST))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of ASCII and NLISTP establish that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, NUMERATOR-SEQUENCE is accepted under the principle of definition. Note
that (OR (LITATOM (NUMERATOR-SEQUENCE LST)) (LISTP (NUMERATOR-SEQUENCE LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMERATOR-SEQUENCE
(DEFN DENOMINATOR-SEQUENCE
(LST)
(IF (NLISTP LST)
NIL
(IF (EQUAL (CAR LST) (ASCII 'SLASH))
(CDR LST)
(DENOMINATOR-SEQUENCE (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of ASCII and NLISTP establish that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, DENOMINATOR-SEQUENCE is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
DENOMINATOR-SEQUENCE
(DEFN BASE-N-SIGNED-VALUE
(N LST)
(IF (EQUAL (CAR LST) (ASCII 'MINUS-SIGN))
(MINUS (BASE-N-VALUE N (CDR LST)))
(IF (EQUAL (CAR LST) (ASCII 'PLUS-SIGN))
(BASE-N-VALUE N (CDR LST))
(BASE-N-VALUE N LST))))
Note that:
(OR (NUMBERP (BASE-N-SIGNED-VALUE N LST))
(NEGATIVEP (BASE-N-SIGNED-VALUE N LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
BASE-N-SIGNED-VALUE
(DEFN NUMBER-SIGN-SEQUENCE
(LST)
(AND
(GEQ (LENGTH LST) 3)
(EQUAL (CAR LST)
(ASCII 'NUMBER-SIGN))
(MEMBER (CADRN 1 LST)
(ASCII '(UPPER-B UPPER-O UPPER-X)))
(OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE (IF (EQUAL (CADRN 1 LST)
(ASCII 'UPPER-B))
2
(IF (EQUAL (CADRN 1 LST)
(ASCII 'UPPER-O))
8 16))
(CDR (CDR LST)))))
From the definition we can conclude that:
(OR (FALSEP (NUMBER-SIGN-SEQUENCE LST))
(TRUEP (NUMBER-SIGN-SEQUENCE LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMBER-SIGN-SEQUENCE
(DEFN LAST
(LST)
(IF (NLISTP LST)
LST
(IF (NLISTP (CDR LST))
LST
(LAST (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to prove that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, LAST is accepted under the definitional principle. Note that:
(OR (LISTP (LAST LST))
(EQUAL (LAST LST) LST))
is a theorem.
[ 0.0 0.0 0.0 ]
LAST
(DEFN ALL-BUT-LAST
(LST)
(IF (NLISTP LST)
NIL
(IF (NLISTP (CDR LST))
NIL
(CONS (CAR LST)
(ALL-BUT-LAST (CDR LST))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
ALL-BUT-LAST is accepted under the definitional principle. From the
definition we can conclude that:
(OR (LITATOM (ALL-BUT-LAST LST))
(LISTP (ALL-BUT-LAST LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-BUT-LAST
(DEFN NUMERIC-SEQUENCE
(LST)
(OR (OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE 10 LST)
(OR (AND (EQUAL (CAR (LAST LST)) (ASCII 'DOT))
(OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE 10
(ALL-BUT-LAST LST)))
(NUMBER-SIGN-SEQUENCE LST))))
From the definition we can conclude that:
(OR (FALSEP (NUMERIC-SEQUENCE LST))
(TRUEP (NUMERIC-SEQUENCE LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMERIC-SEQUENCE
(DEFN NUMERIC-VALUE
(LST)
(IF (OPTIONALLY-SIGNED-BASE-N-DIGIT-SEQUENCE 10 LST)
(BASE-N-SIGNED-VALUE 10 LST)
(IF (EQUAL (CAR (LAST LST)) (ASCII 'DOT))
(BASE-N-SIGNED-VALUE 10
(ALL-BUT-LAST LST))
(BASE-N-SIGNED-VALUE (IF (EQUAL (CADRN 1 LST)
(ASCII 'UPPER-B))
2
(IF (EQUAL (CADRN 1 LST)
(ASCII 'UPPER-O))
8 16))
(CDR (CDR LST))))))
Note that:
(OR (NUMBERP (NUMERIC-VALUE LST))
(NEGATIVEP (NUMERIC-VALUE LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMERIC-VALUE
(DEFN SINGLE-QUOTE-TOKEN NIL
(PACK (CONS (ASCII 'SINGLE-QUOTE) 0)))
Observe that (LITATOM (SINGLE-QUOTE-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
SINGLE-QUOTE-TOKEN
(DEFN BACKQUOTE-TOKEN NIL
(PACK (CONS (ASCII 'BACKQUOTE) 0)))
Observe that (LITATOM (BACKQUOTE-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
BACKQUOTE-TOKEN
(DEFN DOT-TOKEN NIL
(PACK (CONS (ASCII 'DOT) 0)))
Observe that (LITATOM (DOT-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
DOT-TOKEN
(DEFN COMMA-TOKEN NIL
(PACK (CONS (ASCII 'COMMA) 0)))
Observe that (LITATOM (COMMA-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
COMMA-TOKEN
(DEFN COMMA-AT-SIGN-TOKEN NIL
(PACK (CONS (ASCII 'COMMA)
(CONS (ASCII 'AT-SIGN) 0))))
Note that (LITATOM (COMMA-AT-SIGN-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
COMMA-AT-SIGN-TOKEN
(DEFN COMMA-DOT-TOKEN NIL
(PACK (CONS (ASCII 'COMMA)
(CONS (ASCII 'DOT) 0))))
Note that (LITATOM (COMMA-DOT-TOKEN)) is a theorem.
[ 0.0 0.0 0.0 ]
COMMA-DOT-TOKEN
(DEFN WORD-CHARACTERS NIL
(ASCII '(UPPER-A UPPER-B UPPER-C UPPER-D UPPER-E UPPER-F UPPER-G
UPPER-H UPPER-I UPPER-J UPPER-K UPPER-L UPPER-M
UPPER-N UPPER-O UPPER-P UPPER-Q UPPER-R UPPER-S
UPPER-T UPPER-U UPPER-V UPPER-W UPPER-X UPPER-Y
UPPER-Z DIGIT-ZERO DIGIT-ONE DIGIT-TWO DIGIT-THREE
DIGIT-FOUR DIGIT-FIVE DIGIT-SIX DIGIT-SEVEN
DIGIT-EIGHT DIGIT-NINE DOLLAR-SIGN UPARROW AMPERSAND
ASTERISK UNDERSCORE MINUS-SIGN PLUS-SIGN EQUAL-SIGN
TILDE OPEN-BRACE CLOSE-BRACE QUESTION-MARK
LESS-THAN-SIGN GREATER-THAN-SIGN)))
[ 0.0 0.0 0.0 ]
WORD-CHARACTERS
(DEFN SUBSETP
(X Y)
(IF (NLISTP X)
T
(IF (MEMBER (CAR X) Y)
(SUBSETP (CDR X) Y)
F)))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call. Hence, SUBSETP is
accepted under the definitional principle. Note that:
(OR (FALSEP (SUBSETP X Y))
(TRUEP (SUBSETP X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
SUBSETP
(DEFN WORD
(S)
(AND (LITATOM S)
(OR (NUMERIC-SEQUENCE (UNPACK S))
(AND (LISTP (UNPACK S))
(SUBSETP (UNPACK S)
(WORD-CHARACTERS))))))
Note that (OR (FALSEP (WORD S)) (TRUEP (WORD S))) is a theorem.
[ 0.0 0.0 0.0 ]
WORD
(DEFN NUMERIC-WORD
(S)
(AND (LITATOM S)
(NUMERIC-SEQUENCE (UNPACK S))))
From the definition we can conclude that:
(OR (FALSEP (NUMERIC-WORD S))
(TRUEP (NUMERIC-WORD S)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMERIC-WORD
(DEFN NUMERIC-WORD-VALUE
(S)
(NUMERIC-VALUE (UNPACK S)))
From the definition we can conclude that:
(OR (NUMBERP (NUMERIC-WORD-VALUE S))
(NEGATIVEP (NUMERIC-WORD-VALUE S)))
is a theorem.
[ 0.0 0.0 0.0 ]
NUMERIC-WORD-VALUE
(DEFN INTEGERP
(X)
(OR (NUMBERP X) (NEGATIVEP X)))
Observe that (OR (FALSEP (INTEGERP X)) (TRUEP (INTEGERP X))) is a theorem.
[ 0.0 0.0 0.0 ]
INTEGERP
(DEFN SPECIAL-TOKEN
(X)
(OR (EQUAL X (SINGLE-QUOTE-TOKEN))
(OR (EQUAL X (BACKQUOTE-TOKEN))
(OR (EQUAL X (COMMA-TOKEN))
(OR (EQUAL X (COMMA-AT-SIGN-TOKEN))
(EQUAL X (COMMA-DOT-TOKEN)))))))
Observe that (OR (FALSEP (SPECIAL-TOKEN X)) (TRUEP (SPECIAL-TOKEN X))) is
a theorem.
[ 0.0 0.0 0.0 ]
SPECIAL-TOKEN
(DEFN EQLEN
(LST N)
(IF (ZEROP N)
(EQUAL LST NIL)
(IF (NLISTP LST)
F
(EQLEN (CDR LST) (SUB1 N)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of NLISTP and ZEROP establish that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, EQLEN is accepted under the definitional principle. The definition of
EQLEN can be justified in another way. Linear arithmetic, the lemma
COUNT-NUMBERP, and the definitions of NLISTP and ZEROP can be used to show
that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each recursive call. Observe that:
(OR (FALSEP (EQLEN LST N))
(TRUEP (EQLEN LST N)))
is a theorem.
[ 0.0 0.0 0.0 ]
EQLEN
(DEFN DOTTED-PAIR
(X)
(AND (EQLEN X 3)
(EQUAL (CADRN 1 X) (DOT-TOKEN))))
Note that (OR (FALSEP (DOTTED-PAIR X)) (TRUEP (DOTTED-PAIR X))) is a
theorem.
[ 0.0 0.0 0.0 ]
DOTTED-PAIR
(DEFN DOTTED-S-EXPRESSION
(X)
(IF (NLISTP X)
F
(IF (DOTTED-PAIR X)
T
(DOTTED-S-EXPRESSION (CDR X)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of DOTTED-PAIR, CADRN, DOT-TOKEN, and NLISTP can be used to show
that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call. Hence, DOTTED-S-EXPRESSION is accepted under
the definitional principle. From the definition we can conclude that:
(OR (FALSEP (DOTTED-S-EXPRESSION X))
(TRUEP (DOTTED-S-EXPRESSION X)))
is a theorem.
[ 0.0 0.0 0.0 ]
DOTTED-S-EXPRESSION
(DEFN SINGLETON (X) (EQLEN X 1))
Observe that (OR (FALSEP (SINGLETON X)) (TRUEP (SINGLETON X))) is a
theorem.
[ 0.0 0.0 0.0 ]
SINGLETON
(PROVE-LEMMA CDRN-EXPANDER
(REWRITE)
(EQUAL (CDRN (ADD1 N) X)
(CDRN N (CDR X))))
This conjecture simplifies, applying SUB1-ADD1, and unfolding the function
CDRN, to the formula:
(IMPLIES (NOT (NUMBERP N))
(EQUAL (CDRN 0 (CDR X))
(CDRN N (CDR X)))).
This again simplifies, expanding EQUAL and CDRN, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CDRN-EXPANDER
(DEFN TOKEN-TREE
(X)
(IF (NLISTP X)
(OR (INTEGERP X) (WORD X))
(IF (AND (SPECIAL-TOKEN (CAR X))
(EQUAL (LENGTH X) 2))
(TOKEN-TREE (CADRN 1 X))
(IF (DOTTED-PAIR X)
(AND (TOKEN-TREE (CAR X))
(TOKEN-TREE (CADRN 2 X)))
(IF (SINGLETON X)
(TOKEN-TREE (CAR X))
(AND (TOKEN-TREE (CAR X))
(TOKEN-TREE (CDR X))))))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSP,
CDR-LESSEQP, CAR-LESSP, and ADD1-EQUAL, and the definitions of CADRN, EQUAL,
CDRN, AND, SPECIAL-TOKEN, SINGLE-QUOTE-TOKEN, BACKQUOTE-TOKEN, COMMA-TOKEN,
COMMA-AT-SIGN-TOKEN, COMMA-DOT-TOKEN, NLISTP, DOTTED-PAIR, DOT-TOKEN,
SINGLETON, SUB1, EQLEN, NUMBERP, and LENGTH can be used to show that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each recursive call. Hence, TOKEN-TREE is accepted under the principle of
definition. Note that (OR (FALSEP (TOKEN-TREE X)) (TRUEP (TOKEN-TREE X))) is
a theorem.
[ 0.0 0.1 0.0 ]
TOKEN-TREE
(DEFN SPECIAL-TOKEN-TREE
(X)
(SPECIAL-TOKEN (CAR X)))
From the definition we can conclude that:
(OR (FALSEP (SPECIAL-TOKEN-TREE X))
(TRUEP (SPECIAL-TOKEN-TREE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SPECIAL-TOKEN-TREE
(DEFN SINGLE-QUOTE-TOKEN-TREE
(X)
(EQUAL (CAR X) (SINGLE-QUOTE-TOKEN)))
Note that:
(OR (FALSEP (SINGLE-QUOTE-TOKEN-TREE X))
(TRUEP (SINGLE-QUOTE-TOKEN-TREE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SINGLE-QUOTE-TOKEN-TREE
(DEFN BACKQUOTE-TOKEN-TREE
(X)
(EQUAL (CAR X) (BACKQUOTE-TOKEN)))
Note that:
(OR (FALSEP (BACKQUOTE-TOKEN-TREE X))
(TRUEP (BACKQUOTE-TOKEN-TREE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
BACKQUOTE-TOKEN-TREE
(DEFN COMMA-ESCAPE-TOKEN-TREE
(X)
(EQUAL (CAR X) (COMMA-TOKEN)))
Note that:
(OR (FALSEP (COMMA-ESCAPE-TOKEN-TREE X))
(TRUEP (COMMA-ESCAPE-TOKEN-TREE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
COMMA-ESCAPE-TOKEN-TREE
(DEFN SPLICE-ESCAPE-TOKEN-TREE
(X)
(OR (EQUAL (CAR X) (COMMA-AT-SIGN-TOKEN))
(EQUAL (CAR X) (COMMA-DOT-TOKEN))))
From the definition we can conclude that:
(OR (FALSEP (SPLICE-ESCAPE-TOKEN-TREE X))
(TRUEP (SPLICE-ESCAPE-TOKEN-TREE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SPLICE-ESCAPE-TOKEN-TREE
(DEFN CONSTITUENT (X) (CADRN 1 X))
[ 0.0 0.0 0.0 ]
CONSTITUENT
(DEFN OPEN-PAREN NIL
(PACK (CONS (ASCII 'OPEN-PAREN) 0)))
Observe that (LITATOM (OPEN-PAREN)) is a theorem.
[ 0.0 0.0 0.0 ]
OPEN-PAREN
(DEFN CLOSE-PAREN NIL
(PACK (CONS (ASCII 'CLOSE-PAREN) 0)))
Observe that (LITATOM (CLOSE-PAREN)) is a theorem.
[ 0.0 0.0 0.0 ]
CLOSE-PAREN
(DEFN SKIP-PAST-NEWLINE
(STREAM)
(IF (NLISTP STREAM)
STREAM
(IF (EQUAL (CAR STREAM) (ASCII 'NEWLINE))
(CDR STREAM)
(SKIP-PAST-NEWLINE (CDR STREAM)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of ASCII and NLISTP inform us that the measure (COUNT STREAM)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, SKIP-PAST-NEWLINE is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
SKIP-PAST-NEWLINE
(PROVE-LEMMA LESSP-SKIP-PAST-NEWLINE
(REWRITE)
(NOT (LESSP (LENGTH STREAM)
(LENGTH (SKIP-PAST-NEWLINE STREAM)))))
WARNING: Note that the proposed lemma LESSP-SKIP-PAST-NEWLINE 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 are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP STREAM) (p STREAM))
(IMPLIES (AND (NOT (NLISTP STREAM))
(EQUAL (CAR STREAM)
(ASCII 'NEWLINE)))
(p STREAM))
(IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (EQUAL (CAR STREAM)
(ASCII 'NEWLINE)))
(p (CDR STREAM)))
(p STREAM))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions
of ASCII and NLISTP establish that the measure (COUNT STREAM) 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 (NLISTP STREAM)
(NOT (LESSP (LENGTH STREAM)
(LENGTH (SKIP-PAST-NEWLINE STREAM))))).
This simplifies, expanding NLISTP, LENGTH, SKIP-PAST-NEWLINE, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP STREAM))
(EQUAL (CAR STREAM)
(ASCII 'NEWLINE)))
(NOT (LESSP (LENGTH STREAM)
(LENGTH (SKIP-PAST-NEWLINE STREAM))))).
This simplifies, rewriting with SUB1-ADD1, and unfolding the definitions of
NLISTP, ASCII, LENGTH, SKIP-PAST-NEWLINE, EQUAL, and LESSP, to:
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 10)
(NOT (EQUAL (LENGTH (CDR STREAM)) 0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (CDR STREAM)))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (EQUAL (CAR STREAM)
(ASCII 'NEWLINE)))
(NOT (LESSP (LENGTH (CDR STREAM))
(LENGTH (SKIP-PAST-NEWLINE (CDR STREAM))))))
(NOT (LESSP (LENGTH STREAM)
(LENGTH (SKIP-PAST-NEWLINE STREAM))))),
which simplifies, rewriting with the lemma SUB1-ADD1, and unfolding NLISTP,
ASCII, LENGTH, SKIP-PAST-NEWLINE, and LESSP, to:
(IMPLIES
(AND (LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 10))
(NOT (LESSP (LENGTH (CDR STREAM))
(LENGTH (SKIP-PAST-NEWLINE (CDR STREAM)))))
(NOT (EQUAL (LENGTH (SKIP-PAST-NEWLINE (CDR STREAM)))
0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (SKIP-PAST-NEWLINE (CDR STREAM))))))).
But this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-SKIP-PAST-NEWLINE
(DEFN SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(STREAM I)
(IF
(NLISTP STREAM)
(CONS (ASCII 'OPEN-PAREN) STREAM)
(IF (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR)))
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I))
(IF (AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(IF (EQUAL I 0)
(CONS (ASCII 'OPEN-PAREN)
(CDRN 2 STREAM))
(IF (EQUAL I 1)
(CDRN 2 STREAM)
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CDR-LESSEQP, and CDR-LESSP,
and the definitions of AND, CADRN, EQUAL, CDRN, ASCII, and NLISTP establish
that the measure (COUNT STREAM) decreases according to the well-founded
relation LESSP in each recursive call. Hence,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
is accepted under the principle of definition.
[ 0.1 0.0 0.0 ]
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(PROVE-LEMMA SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN-LEMMA
(REWRITE)
(NOT (LESSP (ADD1 (LENGTH STREAM))
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))
WARNING: Note that the proposed lemma:
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN-LEMMA
is to be stored as zero type prescription rules, zero compound recognizer
rules, one linear rule, and zero replacement rules.
This formula simplifies, applying SUB1-ADD1, and opening up the function LESSP,
to:
(IMPLIES
(NOT (EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which we will name *1.
We will appeal to induction. There are three plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP STREAM) (p STREAM I))
(IMPLIES (AND (NOT (NLISTP STREAM))
(AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR)))
(p (CDRN 2 STREAM) (ADD1 I)))
(p STREAM I))
(IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(EQUAL I 0))
(p STREAM I))
(IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(NOT (EQUAL I 0))
(EQUAL I 1))
(p STREAM I))
(IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(p (CDRN 2 STREAM) (SUB1 I)))
(p STREAM I))
(IMPLIES (AND (NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN))))
(p (CDR STREAM) I))
(p STREAM I))).
Linear arithmetic, the lemmas CDRN-EXPANDER, CDR-LESSEQP, and CDR-LESSP, and
the definitions of AND, CADRN, EQUAL, CDRN, ASCII, and NLISTP inform us that
the measure (COUNT STREAM) decreases according to the well-founded relation
LESSP in each induction step of the scheme. Note, however, the inductive
instances chosen for I. The above induction scheme generates the following
nine new goals:
Case 9. (IMPLIES
(AND
(NLISTP STREAM)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))).
This simplifies, rewriting with the lemma CDR-CONS, and expanding the
functions NLISTP, SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, ASCII, ADD1,
LENGTH, EQUAL, SUB1, and LESSP, to:
T.
Case 8. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR)))
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I)))
0)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))).
This simplifies, applying CDRN-EXPANDER, and opening up NLISTP, ASCII, CDRN,
EQUAL, CADRN, AND, and SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, to:
T.
Case 7. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR)))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I))))))
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, appealing to the lemmas CDRN-EXPANDER and SUB1-ADD1, and
opening up the functions NLISTP, ASCII, CDRN, EQUAL, CADRN, AND,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, LENGTH, and LESSP, to the
conjecture:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(ADD1 I)))))))).
But this further simplifies, rewriting with CDRN-EXPANDER, and unfolding the
definitions of EQUAL and CDRN, to:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))))
(NOT
(EQUAL
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))))))),
which again simplifies, opening up the definition of LENGTH, to two new
goals:
Case 7.2.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))
0))
(NOT (LISTP (CDR STREAM))))
(NOT
(LESSP 0
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))))))),
which again simplifies, rewriting with CAR-NLISTP, and unfolding the
function EQUAL, to:
T.
Case 7.1.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I))))
0))
(LISTP (CDR STREAM)))
(NOT
(LESSP
(ADD1 (LENGTH (CDDR STREAM)))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(ADD1 I)))))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(EQUAL I 0)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, applying the lemmas CDRN-EXPANDER, CDR-CONS, and SUB1-ADD1,
and opening up the functions NLISTP, ASCII, CDRN, EQUAL, CADRN, AND,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, LENGTH, and LESSP, to two new
goals:
Case 6.2.
(IMPLIES (AND (LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 35))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (CDDR STREAM)))))),
which again simplifies, opening up EQUAL, to:
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (CDDR STREAM)))))).
This further simplifies, opening up LENGTH, to two new goals:
Case 6.2.2.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (LISTP (CDR STREAM))))
(NOT (LESSP 0
(SUB1 (LENGTH (CDDR STREAM)))))),
which again simplifies, applying the lemma CAR-NLISTP, and expanding the
definition of EQUAL, to:
T.
Case 6.2.1.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(LISTP (CDR STREAM)))
(NOT (LESSP (ADD1 (LENGTH (CDDR STREAM)))
(SUB1 (LENGTH (CDDR STREAM)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 6.1.
(IMPLIES (AND (LISTP STREAM)
(NOT (EQUAL (CADR STREAM) 124))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (CDDR STREAM)))))),
which again simplifies, opening up the function EQUAL, to the conjecture:
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (LENGTH (CDDR STREAM)))))).
This further simplifies, unfolding the function LENGTH, to two new
formulas:
Case 6.1.2.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (LISTP (CDR STREAM))))
(NOT (LESSP 0
(SUB1 (LENGTH (CDDR STREAM)))))),
which again simplifies, rewriting with CAR-NLISTP, and unfolding the
function EQUAL, to:
T.
Case 6.1.1.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(LISTP (CDR STREAM)))
(NOT (LESSP (ADD1 (LENGTH (CDDR STREAM)))
(SUB1 (LENGTH (CDDR STREAM)))))).
This again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(NOT (EQUAL I 0))
(EQUAL I 1)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, applying CDRN-EXPANDER and SUB1-ADD1, and expanding the
functions NLISTP, ASCII, CDRN, EQUAL, CADRN, AND,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, LENGTH, and LESSP, to the
following two new conjectures:
Case 5.2.
(IMPLIES (AND (LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 35))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))).
However this again simplifies, unfolding EQUAL, to:
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))).
But this further simplifies, unfolding the definition of LENGTH, to two
new goals:
Case 5.2.2.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0))
(NOT (LISTP (CDR STREAM))))
(NOT (LESSP 0
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))),
which again simplifies, applying the lemma CAR-NLISTP, and expanding the
function EQUAL, to:
T.
Case 5.2.1.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0))
(LISTP (CDR STREAM)))
(NOT (LESSP (ADD1 (LENGTH (CDDR STREAM)))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.1.
(IMPLIES (AND (LISTP STREAM)
(NOT (EQUAL (CADR STREAM) 124))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))),
which again simplifies, opening up the definition of EQUAL, to:
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0)))
(NOT (LESSP (LENGTH (CDR STREAM))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))).
But this further simplifies, opening up LENGTH, to two new conjectures:
Case 5.1.2.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0))
(NOT (LISTP (CDR STREAM))))
(NOT (LESSP 0
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))),
which again simplifies, rewriting with CAR-NLISTP, and unfolding EQUAL,
to:
T.
Case 5.1.1.
(IMPLIES (AND (LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL (LENGTH (CDDR STREAM)) 0))
(NOT (EQUAL (SUB1 (LENGTH (CDDR STREAM)))
0))
(LISTP (CDR STREAM)))
(NOT (LESSP (ADD1 (LENGTH (CDDR STREAM)))
(SUB1 (SUB1 (LENGTH (CDDR STREAM))))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))
0)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, rewriting with CDRN-EXPANDER, and opening up NLISTP, ASCII,
CDRN, EQUAL, CADRN, AND, and SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN,
to:
T.
Case 3. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN)))
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))))
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))).
This simplifies, appealing to the lemmas CDRN-EXPANDER and SUB1-ADD1, and
unfolding NLISTP, ASCII, CDRN, EQUAL, CADRN, AND,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, LENGTH, and LESSP, to the
following two new formulas:
Case 3.2.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 35))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))))))).
However this again simplifies, opening up EQUAL, to:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))))))).
But this further simplifies, rewriting with CDRN-EXPANDER, and unfolding
the functions EQUAL and CDRN, to:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))))))),
which again simplifies, unfolding LENGTH, to two new formulas:
Case 3.2.2.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0))
(NOT (LISTP (CDR STREAM))))
(NOT
(LESSP 0
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(CDDR STREAM)
(SUB1 I)))))))),
which again simplifies, rewriting with CAR-NLISTP, and opening up the
definition of EQUAL, to:
T.
Case 3.2.1.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0))
(LISTP (CDR STREAM)))
(NOT
(LESSP
(ADD1 (LENGTH (CDDR STREAM)))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(CDDR STREAM)
(SUB1 I)))))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CADR STREAM) 124))
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))))))),
which again simplifies, opening up EQUAL, to:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDRN 2 STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
(SUB1 I)))))))).
But this further simplifies, rewriting with the lemma CDRN-EXPANDER, and
expanding the functions EQUAL and CDRN, to the formula:
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))))))).
But this again simplifies, unfolding the function LENGTH, to two new
conjectures:
Case 3.1.2.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0))
(NOT (LISTP (CDR STREAM))))
(NOT
(LESSP 0
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(CDDR STREAM)
(SUB1 I)))))))),
which again simplifies, rewriting with CAR-NLISTP, and unfolding the
function EQUAL, to:
T.
Case 3.1.1.
(IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 124)
(EQUAL (CADR STREAM) 35)
(NOT (EQUAL I 0))
(NOT (EQUAL I 1))
(NOT
(LESSP
(LENGTH (CDDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I)))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
(SUB1 I))))
0))
(LISTP (CDR STREAM)))
(NOT
(LESSP
(ADD1 (LENGTH (CDDR STREAM)))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(CDDR STREAM)
(SUB1 I)))))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN))))
(EQUAL
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))
0)
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, appealing to the lemma CDRN-EXPANDER, and expanding NLISTP,
ASCII, CDRN, EQUAL, CADRN, AND, and
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, to:
T.
Case 1. (IMPLIES
(AND
(NOT (NLISTP STREAM))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(NOT (AND (EQUAL (CAR STREAM)
(ASCII 'VERTICAL-BAR))
(EQUAL (CADRN 1 STREAM)
(ASCII 'NUMBER-SIGN))))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
(NOT
(EQUAL (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I))
0)))
(NOT
(LESSP
(LENGTH STREAM)
(SUB1 (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN STREAM
I)))))),
which simplifies, rewriting with CDRN-EXPANDER and SUB1-ADD1, and opening up
the functions NLISTP, ASCII, CDRN, EQUAL, CADRN, AND,
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, LENGTH, and LESSP, to the
following four new goals:
Case 1.4.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 35))
(NOT (EQUAL (CAR STREAM) 124))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CAR STREAM) 35))
(NOT (EQUAL (CADR STREAM) 35))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CADR STREAM) 124))
(NOT (EQUAL (CAR STREAM) 124))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND
(LISTP STREAM)
(NOT (EQUAL (CADR STREAM) 124))
(NOT (EQUAL (CADR STREAM) 35))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))))
(NOT
(EQUAL
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))
0))
(NOT
(EQUAL
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I)))
0)))
(NOT
(LESSP
(LENGTH (CDR STREAM))
(SUB1
(SUB1
(LENGTH
(SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDR STREAM)
I))))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.1 ]
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN-LEMMA
(PROVE-LEMMA LESSP-SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(REWRITE)
(IMPLIES
(AND (LISTP STREAM)
(AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADR STREAM)
(ASCII 'VERTICAL-BAR))))
(LESSP (LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
1))
(LENGTH STREAM))))
WARNING: Note that the proposed lemma:
LESSP-SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
is to be stored as zero type prescription rules, zero compound recognizer
rules, one linear rule, and zero replacement rules.
This conjecture simplifies, rewriting with SUB1-ADD1, and opening up ASCII,
LENGTH, and LESSP, to two new formulas:
Case 2. (IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(EQUAL
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
1))
0))
(LISTP (CDR STREAM)))
(LESSP
(SUB1
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
1)))
(ADD1 (LENGTH (CDDR STREAM))))),
which again simplifies, using linear arithmetic and rewriting with
SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN-LEMMA, to:
T.
Case 1. (IMPLIES
(AND
(LISTP STREAM)
(EQUAL (CAR STREAM) 35)
(EQUAL (CADR STREAM) 124)
(NOT
(EQUAL
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
1))
0))
(NOT (LISTP (CDR STREAM))))
(LESSP
(SUB1
(LENGTH (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDDR STREAM)
1)))
0)).
But this again simplifies, applying CAR-NLISTP, and unfolding EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN
(DEFN WHITE-SPACEP
(C)
(MEMBER C
(ASCII '(SPACE TAB NEWLINE))))
Observe that (OR (FALSEP (WHITE-SPACEP C)) (TRUEP (WHITE-SPACEP C))) is a
theorem.
[ 0.0 0.0 0.0 ]
WHITE-SPACEP
(DEFN REV1
(LST ANS)
(IF (NLISTP LST)
ANS
(REV1 (CDR LST)
(CONS (CAR LST) ANS))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
REV1 is accepted under the definitional principle. From the definition we can
conclude that (OR (LISTP (REV1 LST ANS)) (EQUAL (REV1 LST ANS) ANS)) is a
theorem.
[ 0.0 0.0 0.0 ]
REV1
(DEFN EMIT
(PNAME LST)
(IF (EQUAL PNAME 0)
LST
(CONS (PACK (REV1 PNAME 0)) LST)))
From the definition we can conclude that:
(OR (LISTP (EMIT PNAME LST))
(EQUAL (EMIT PNAME LST) LST))
is a theorem.
[ 0.0 0.0 0.0 ]
EMIT
(DEFN UPCASE
(C)
(IF (AND (LEQ (ASCII 'LOWER-A) C)
(LEQ C (ASCII 'LOWER-Z)))
(DIFFERENCE C
(DIFFERENCE (ASCII 'LOWER-A)
(ASCII 'UPPER-A)))
C))
From the definition we can conclude that:
(OR (NUMBERP (UPCASE C))
(EQUAL (UPCASE C) C))
is a theorem.
[ 0.0 0.0 0.0 ]
UPCASE
(DEFN LEXEMES
(STREAM PNAME)
(IF
(NLISTP STREAM)
(EMIT PNAME NIL)
(IF
(EQUAL (CAR STREAM)
(ASCII 'SEMICOLON))
(EMIT PNAME
(LEXEMES (SKIP-PAST-NEWLINE (CDR STREAM))
0))
(IF
(MEMBER (CAR STREAM)
(ASCII '(BACKQUOTE SINGLE-QUOTE OPEN-PAREN CLOSE-PAREN)))
(EMIT PNAME
(EMIT (CONS (CAR STREAM) 0)
(LEXEMES (CDR STREAM) 0)))
(IF
(EQUAL (CAR STREAM) (ASCII 'COMMA))
(IF (OR (EQUAL (CADRN 1 STREAM)
(ASCII 'AT-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'DOT)))
(EMIT PNAME
(EMIT (CONS (CADRN 1 STREAM)
(CONS (CAR STREAM) 0))
(LEXEMES (CDR (CDR STREAM)) 0)))
(EMIT PNAME
(EMIT (CONS (CAR STREAM) 0)
(LEXEMES (CDR STREAM) 0))))
(IF
(WHITE-SPACEP (CAR STREAM))
(EMIT PNAME (LEXEMES (CDR STREAM) 0))
(IF
(AND (EQUAL PNAME 0)
(AND (EQUAL (CAR STREAM)
(ASCII 'NUMBER-SIGN))
(EQUAL (CADRN 1 STREAM)
(ASCII 'VERTICAL-BAR))))
(LEXEMES (SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN (CDRN 2 STREAM)
1)
0)
(LEXEMES (CDR STREAM)
(CONS (UPCASE (CAR STREAM))
PNAME))))))))
((LESSP (LENGTH STREAM))))
Linear arithmetic, the lemmas SUB1-ADD1, LESSP-SKIP-PAST-NEWLINE,
CDRN-EXPANDER, CAR-NLISTP, and
LESSP-SKIP-PAST-BALANCING-VERTICAL-BAR-NUMBER-SIGN, and the definitions of
LESSP, LENGTH, ASCII, NLISTP, MEMBER, LISTP, CAR, CDR, OR, CADRN, CDRN, EQUAL,
WHITE-SPACEP, and AND can be used to establish that the measure
(LENGTH STREAM) decreases according to the well-founded relation LESSP in each
recursive call. Hence, LEXEMES is accepted under the definitional principle.
Observe that:
(OR (LITATOM (LEXEMES STREAM PNAME))
(LISTP (LEXEMES STREAM PNAME)))
is a theorem.
[ 0.0 0.1 0.0 ]
LEXEMES
(DEFN TOP-PSTK
(STACK)
(IF (LISTP STACK) (CAR STACK) F))
[ 0.0 0.0 0.0 ]
TOP-PSTK
(DEFN POP-PSTK
(STACK)
(IF (LISTP STACK) (CDR STACK) F))
[ 0.0 0.0 0.0 ]
POP-PSTK
(DEFN PUSH-PSTK
(X STACK)
(IF (EQUAL STACK F) F (CONS X STACK)))
From the definition we can conclude that:
(OR (FALSEP (PUSH-PSTK X STACK))
(LISTP (PUSH-PSTK X STACK)))
is a theorem.
[ 0.0 0.0 0.0 ]
PUSH-PSTK
(DEFN EMPTY-PSTK (X) (NLISTP X))
Observe that (OR (FALSEP (EMPTY-PSTK X)) (TRUEP (EMPTY-PSTK X))) is a
theorem.
[ 0.0 0.0 0.0 ]
EMPTY-PSTK
(DEFN DOT-CRITERION
(I X)
(IF (NLISTP X)
T
(IF (EQUAL (CAR X) (DOT-TOKEN))
(AND (NOT (ZEROP I))
(AND (LISTP (CDR X))
(NLISTP (CDR (CDR X)))))
(DOT-CRITERION (ADD1 I) (CDR X)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of DOT-TOKEN and NLISTP establish that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, DOT-CRITERION is accepted under the principle of definition. Observe
that (OR (FALSEP (DOT-CRITERION I X)) (TRUEP (DOT-CRITERION I X))) is a
theorem.
[ 0.0 0.0 0.0 ]
DOT-CRITERION
(DEFN ADD-ELEMENT-TO-TOP
(X STACK)
(IF (EMPTY-PSTK STACK)
F
(IF (NOT (DOT-CRITERION 0 X))
F
(IF (SPECIAL-TOKEN (TOP-PSTK STACK))
(ADD-ELEMENT-TO-TOP (LIST2 (TOP-PSTK STACK) X)
(POP-PSTK STACK))
(PUSH-PSTK (APPEND (TOP-PSTK STACK) (LIST1 X))
(POP-PSTK STACK))))))
Linear arithmetic, the lemma CDR-LESSP, and the definitions of POP-PSTK,
SPECIAL-TOKEN, SINGLE-QUOTE-TOKEN, BACKQUOTE-TOKEN, COMMA-TOKEN,
COMMA-AT-SIGN-TOKEN, COMMA-DOT-TOKEN, TOP-PSTK, and EMPTY-PSTK establish that
the measure (COUNT STACK) decreases according to the well-founded relation
LESSP in each recursive call. Hence, ADD-ELEMENT-TO-TOP is accepted under the
principle of definition. Note that:
(OR (FALSEP (ADD-ELEMENT-TO-TOP X STACK))
(LISTP (ADD-ELEMENT-TO-TOP X STACK)))
is a theorem.
[ 0.0 0.0 0.0 ]
ADD-ELEMENT-TO-TOP
(DEFN STOP
(STACK)
(IF (AND (EQLEN STACK 1)
(AND (EQLEN (TOP-PSTK STACK) 1)
(NOT (EQUAL (CAR (TOP-PSTK STACK))
(DOT-TOKEN)))))
(CAR (TOP-PSTK STACK))
F))
[ 0.0 0.0 0.0 ]
STOP
(DEFN PARSE
(LEXEMES STACK)
(IF (NLISTP LEXEMES)
(STOP STACK)
(IF (EQUAL (CAR LEXEMES) (OPEN-PAREN))
(PARSE (CDR LEXEMES)
(PUSH-PSTK NIL STACK))
(IF (SPECIAL-TOKEN (CAR LEXEMES))
(PARSE (CDR LEXEMES)
(PUSH-PSTK (CAR LEXEMES) STACK))
(IF (EQUAL (CAR LEXEMES) (CLOSE-PAREN))
(PARSE (CDR LEXEMES)
(ADD-ELEMENT-TO-TOP (TOP-PSTK STACK)
(POP-PSTK STACK)))
(PARSE (CDR LEXEMES)
(ADD-ELEMENT-TO-TOP (CAR LEXEMES)
STACK)))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of OPEN-PAREN, NLISTP, SPECIAL-TOKEN, SINGLE-QUOTE-TOKEN,
BACKQUOTE-TOKEN, COMMA-TOKEN, COMMA-AT-SIGN-TOKEN, COMMA-DOT-TOKEN,
CLOSE-PAREN, and UNPACK can be used to show that the measure (COUNT LEXEMES)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, PARSE is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
PARSE
(DEFN READ-TOKEN-TREE
(STREAM)
(IF (TOKEN-TREE (PARSE (LEXEMES STREAM 0)
(CONS NIL NIL)))
(PARSE (LEXEMES STREAM 0)
(CONS NIL NIL))
F))
[ 0.0 0.0 0.0 ]
READ-TOKEN-TREE
(DEFN READABLE
(X N)
(IF (NLISTP X)
(NOT (EQUAL X F))
(IF (SINGLE-QUOTE-TOKEN-TREE X)
(READABLE (CONSTITUENT X) N)
(IF (BACKQUOTE-TOKEN-TREE X)
(AND (READABLE (CONSTITUENT X) (ADD1 N))
(NOT (SPLICE-ESCAPE-TOKEN-TREE (CONSTITUENT X))))
(IF (OR (COMMA-ESCAPE-TOKEN-TREE X)
(SPLICE-ESCAPE-TOKEN-TREE X))
(AND (LESSP 0 N)
(READABLE (CONSTITUENT X) (SUB1 N)))
(IF (DOTTED-PAIR X)
(AND (READABLE (CAR X) N)
(AND (READABLE (CADRN 2 X) N)
(NOT (SPLICE-ESCAPE-TOKEN-TREE (CADRN 2 X)))))
(IF (SINGLETON X)
(READABLE (CAR X) N)
(AND (READABLE (CAR X) N)
(READABLE (CDR X) N)))))))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSP,
CDR-LESSEQP, and CAR-LESSP, and the definitions of CONSTITUENT, CDRN, EQUAL,
CADRN, SINGLE-QUOTE-TOKEN-TREE, SINGLE-QUOTE-TOKEN, NLISTP,
BACKQUOTE-TOKEN-TREE, BACKQUOTE-TOKEN, OR, SPLICE-ESCAPE-TOKEN-TREE,
COMMA-AT-SIGN-TOKEN, COMMA-DOT-TOKEN, COMMA-ESCAPE-TOKEN-TREE, COMMA-TOKEN,
DOTTED-PAIR, DOT-TOKEN, and SINGLETON inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, READABLE is accepted under the definitional principle. From the
definition we can conclude that:
(OR (FALSEP (READABLE X N))
(TRUEP (READABLE X N)))
is a theorem.
[ 0.0 0.0 0.0 ]
READABLE
(DEFN S-EXPRESSION
(X)
(IF (NLISTP X)
(IF (EQUAL X F)
F
(NOT (NUMERIC-WORD X)))
(IF (SPECIAL-TOKEN-TREE X)
F
(IF (DOTTED-PAIR X)
(AND (S-EXPRESSION (CAR X))
(S-EXPRESSION (CADRN 2 X)))
(IF (SINGLETON X)
(S-EXPRESSION (CAR X))
(AND (S-EXPRESSION (CAR X))
(S-EXPRESSION (CDR X))))))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSEQP,
CDR-LESSP, and CAR-LESSP, and the definitions of DOTTED-PAIR, CDRN, EQUAL,
CADRN, DOT-TOKEN, SPECIAL-TOKEN-TREE, COMMA-DOT-TOKEN, COMMA-AT-SIGN-TOKEN,
COMMA-TOKEN, BACKQUOTE-TOKEN, SINGLE-QUOTE-TOKEN, SPECIAL-TOKEN, NLISTP, and
SINGLETON inform us that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each recursive call. Hence, S-EXPRESSION is
accepted under the principle of definition. From the definition we can
conclude that (OR (FALSEP (S-EXPRESSION X)) (TRUEP (S-EXPRESSION X))) is a
theorem.
[ 0.0 0.0 0.0 ]
S-EXPRESSION
(DEFN BACKQUOTE-EXPANSION
(FLG X)
(IF FLG
(IF (NLISTP X)
(LIST2 'QUOTE X)
(IF (OR (COMMA-ESCAPE-TOKEN-TREE X)
(SPLICE-ESCAPE-TOKEN-TREE X))
(CONSTITUENT X)
(BACKQUOTE-EXPANSION F X)))
(IF (NLISTP X)
'IMPOSSIBLE-IF-X-IS-A-DOTTED-OR-UNDOTTED-TOKEN-TREE
(LIST3 (IF (SPLICE-ESCAPE-TOKEN-TREE (CAR X))
'APPEND
'CONS)
(BACKQUOTE-EXPANSION T (CAR X))
(IF (SINGLETON X)
(LIST2 'QUOTE 'NIL)
(IF (DOTTED-PAIR X)
(BACKQUOTE-EXPANSION T (CADRN 2 X))
(BACKQUOTE-EXPANSION F (CDR X)))))))
((ORD-LESSP (CONS (ADD1 (COUNT X))
(IF FLG 1 0)))))
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-EQUAL,
CDR-LESSP, CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSEQP, and CAR-LESSP, and the
definitions of ORDINALP, ORD-LESSP, OR, SPLICE-ESCAPE-TOKEN-TREE,
COMMA-AT-SIGN-TOKEN, COMMA-DOT-TOKEN, COMMA-ESCAPE-TOKEN-TREE, COMMA-TOKEN,
NLISTP, LESSP, CADRN, EQUAL, and CDRN establish that the measure:
(CONS (ADD1 (COUNT X)) (IF FLG 1 0))
decreases according to the well-founded relation ORD-LESSP in each recursive
call. Hence, BACKQUOTE-EXPANSION is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
BACKQUOTE-EXPANSION
(DEFN READMACRO-EXPANSION
(X)
(IF
(NLISTP X)
(IF (NUMERIC-WORD X)
(NUMERIC-WORD-VALUE X)
X)
(IF (SINGLE-QUOTE-TOKEN-TREE X)
(LIST2 'QUOTE
(READMACRO-EXPANSION (CONSTITUENT X)))
(IF (BACKQUOTE-TOKEN-TREE X)
(BACKQUOTE-EXPANSION T
(READMACRO-EXPANSION (CONSTITUENT X)))
(IF (DOTTED-PAIR X)
(IF (OR (AND (NLISTP (READMACRO-EXPANSION (CADRN 2 X)))
(NOT (EQUAL (READMACRO-EXPANSION (CADRN 2 X))
'NIL)))
(SPECIAL-TOKEN-TREE (READMACRO-EXPANSION (CADRN 2 X))))
(LIST3 (READMACRO-EXPANSION (CAR X))
(DOT-TOKEN)
(READMACRO-EXPANSION (CADRN 2 X)))
(CONS (READMACRO-EXPANSION (CAR X))
(READMACRO-EXPANSION (CADRN 2 X))))
(IF (SINGLETON X)
(LIST1 (READMACRO-EXPANSION (CAR X)))
(CONS (READMACRO-EXPANSION (CAR X))
(READMACRO-EXPANSION (CDR X)))))))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSP,
CDR-LESSEQP, and CAR-LESSP, and the definitions of CONSTITUENT, CDRN, EQUAL,
CADRN, SINGLE-QUOTE-TOKEN-TREE, SINGLE-QUOTE-TOKEN, NLISTP,
BACKQUOTE-TOKEN-TREE, BACKQUOTE-TOKEN, DOTTED-PAIR, DOT-TOKEN, OR,
SPECIAL-TOKEN-TREE, COMMA-DOT-TOKEN, COMMA-AT-SIGN-TOKEN, COMMA-TOKEN,
SPECIAL-TOKEN, AND, NOT, and SINGLETON inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, READMACRO-EXPANSION is accepted under the definitional principle.
[ 0.0 0.1 0.0 ]
READMACRO-EXPANSION
(DEFN CORRESPONDING-NUMBERP
(N)
(IF (ZEROP N)
(LIST1 'ZERO)
(LIST2 'ADD1
(CORRESPONDING-NUMBERP (SUB1 N)))))
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, CORRESPONDING-NUMBERP is
accepted under the definitional principle. Observe that:
(LISTP (CORRESPONDING-NUMBERP N))
is a theorem.
[ 0.0 0.0 0.0 ]
CORRESPONDING-NUMBERP
(DEFN CORRESPONDING-NEGATIVEP
(N)
(LIST2 'MINUS
(CORRESPONDING-NUMBERP (NEGATIVE-GUTS N))))
From the definition we can conclude that:
(LISTP (CORRESPONDING-NEGATIVEP N))
is a theorem.
[ 0.0 0.0 0.0 ]
CORRESPONDING-NEGATIVEP
(DEFN A-D-SEQUENCEP
(LST)
(IF (NLISTP LST)
T
(IF (OR (EQUAL (CAR LST) (ASCII 'UPPER-A))
(EQUAL (CAR LST) (ASCII 'UPPER-D)))
(A-D-SEQUENCEP (CDR LST))
F)))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of OR, ASCII, and NLISTP inform us that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, A-D-SEQUENCEP is accepted under the definitional principle. Observe
that (OR (FALSEP (A-D-SEQUENCEP LST)) (TRUEP (A-D-SEQUENCEP LST))) is a
theorem.
[ 0.0 0.0 0.0 ]
A-D-SEQUENCEP
(DEFN CAR-CDR-SYMBOLP
(X)
(AND (LITATOM X)
(AND (EQUAL (CAR (UNPACK X))
(ASCII 'UPPER-C))
(AND (EQUAL (CAR (LAST (UNPACK X)))
(ASCII 'UPPER-R))
(A-D-SEQUENCEP (ALL-BUT-LAST (CDR (UNPACK X))))))))
From the definition we can conclude that:
(OR (FALSEP (CAR-CDR-SYMBOLP X))
(TRUEP (CAR-CDR-SYMBOLP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
CAR-CDR-SYMBOLP
(DEFN A-D-SEQUENCE
(X)
(ALL-BUT-LAST (CDR (UNPACK X))))
Note that (OR (LITATOM (A-D-SEQUENCE X)) (LISTP (A-D-SEQUENCE X))) is a
theorem.
[ 0.0 0.0 0.0 ]
A-D-SEQUENCE
(DEFN CAR-CDR-NEST
(LST X)
(IF (NLISTP LST)
X
(IF (EQUAL (CAR LST) (ASCII 'UPPER-A))
(LIST2 'CAR
(CAR-CDR-NEST (CDR LST) X))
(LIST2 'CDR
(CAR-CDR-NEST (CDR LST) X)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of ASCII and NLISTP can be used to show that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, CAR-CDR-NEST is accepted under the definitional
principle. From the definition we can conclude that:
(OR (LISTP (CAR-CDR-NEST LST X))
(EQUAL (CAR-CDR-NEST LST X) X))
is a theorem.
[ 0.0 0.1 0.0 ]
CAR-CDR-NEST
(DEFN FCONS
(X Y)
(IF (AND X Y) (CONS X Y) F))
Observe that (OR (FALSEP (FCONS X Y)) (LISTP (FCONS X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
FCONS
(DEFN FLIST1 (X) (FCONS X NIL))
Observe that (OR (FALSEP (FLIST1 X)) (LISTP (FLIST1 X))) is a theorem.
[ 0.0 0.0 0.0 ]
FLIST1
(DEFN FLIST2
(X Y)
(FCONS X (FLIST1 Y)))
Note that (OR (FALSEP (FLIST2 X Y)) (LISTP (FLIST2 X Y))) is a theorem.
[ 0.0 0.0 0.0 ]
FLIST2
(DEFN FLIST3
(X Y Z)
(FCONS X (FLIST2 Y Z)))
Note that (OR (FALSEP (FLIST3 X Y Z)) (LISTP (FLIST3 X Y Z))) is a
theorem.
[ 0.0 0.0 0.0 ]
FLIST3
(DEFN FLIST4
(X Y Z W)
(FCONS X (FLIST3 Y Z W)))
Observe that (OR (FALSEP (FLIST4 X Y Z W)) (LISTP (FLIST4 X Y Z W))) is a
theorem.
[ 0.0 0.0 0.0 ]
FLIST4
(DEFN FLIST5
(X Y Z W V)
(FCONS X (FLIST4 Y Z W V)))
From the definition we can conclude that:
(OR (FALSEP (FLIST5 X Y Z W V))
(LISTP (FLIST5 X Y Z W V)))
is a theorem.
[ 0.0 0.0 0.0 ]
FLIST5
(DEFN FLIST6
(X Y Z W V U)
(FCONS X (FLIST5 Y Z W V U)))
Note that (OR (FALSEP (FLIST6 X Y Z W V U)) (LISTP (FLIST6 X Y Z W V U)))
is a theorem.
[ 0.0 0.0 0.0 ]
FLIST6
(DEFN FLIST7
(X Y Z W V U R)
(FCONS X (FLIST6 Y Z W V U R)))
Observe that:
(OR (FALSEP (FLIST7 X Y Z W V U R))
(LISTP (FLIST7 X Y Z W V U R)))
is a theorem.
[ 0.0 0.0 0.0 ]
FLIST7
(DEFN FN-NEST
(FN LST X)
(IF (NLISTP LST)
X
(FLIST3 FN
(CAR LST)
(FN-NEST FN (CDR LST) X))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to show that the measure (COUNT LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, FN-NEST is accepted under the definitional principle. From the
definition we can conclude that:
(OR (OR (FALSEP (FN-NEST FN LST X))
(LISTP (FN-NEST FN LST X)))
(EQUAL (FN-NEST FN LST X) X))
is a theorem.
[ 0.0 0.0 0.0 ]
FN-NEST
(DEFN CORRESPONDING-NUMBERPS
(LST)
(IF (NLISTP LST)
NIL
(CONS (CORRESPONDING-NUMBERP (CAR LST))
(CORRESPONDING-NUMBERPS (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CORRESPONDING-NUMBERPS is accepted under the definitional principle. Observe
that:
(OR (LITATOM (CORRESPONDING-NUMBERPS LST))
(LISTP (CORRESPONDING-NUMBERPS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
CORRESPONDING-NUMBERPS
(DEFN EXPLOSION
(LST)
(FN-NEST 'CONS
(CORRESPONDING-NUMBERPS LST)
(LIST1 'ZERO)))
From the definition we can conclude that:
(OR (FALSEP (EXPLOSION LST))
(LISTP (EXPLOSION LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
EXPLOSION
(DEFN CORRESPONDING-LITATOM
(X)
(LIST2 'PACK (EXPLOSION (UNPACK X))))
From the definition we can conclude that:
(LISTP (CORRESPONDING-LITATOM X))
is a theorem.
[ 0.0 0.0 0.0 ]
CORRESPONDING-LITATOM
(DEFN STAR-ONE-STAR
(X)
(PACK (APPEND (ASCII '(ASTERISK DIGIT-ONE ASTERISK))
(UNPACK X))))
Note that (LITATOM (STAR-ONE-STAR X)) is a theorem.
[ 0.0 0.0 0.0 ]
STAR-ONE-STAR
(DEFN ASCII-UPPER-ALPHABETICS NIL
(ASCII '(UPPER-A UPPER-B UPPER-C UPPER-D UPPER-E UPPER-F UPPER-G
UPPER-H UPPER-I UPPER-J UPPER-K UPPER-L UPPER-M
UPPER-N UPPER-O UPPER-P UPPER-Q UPPER-R UPPER-S
UPPER-T UPPER-U UPPER-V UPPER-W UPPER-X UPPER-Y
UPPER-Z)))
[ 0.0 0.0 0.0 ]
ASCII-UPPER-ALPHABETICS
(DEFN ASCII-DIGITS-AND-SIGNS NIL
(ASCII '(DIGIT-ONE DIGIT-TWO DIGIT-THREE DIGIT-FOUR DIGIT-FIVE
DIGIT-SIX DIGIT-SEVEN DIGIT-EIGHT DIGIT-NINE
DOLLAR-SIGN UPARROW AMPERSAND ASTERISK UNDERSCORE
MINUS-SIGN PLUS-SIGN EQUAL-SIGN TILDE OPEN-BRACE
CLOSE-BRACE QUESTION-MARK LESS-THAN-SIGN
GREATER-THAN-SIGN)))
[ 0.0 0.0 0.0 ]
ASCII-DIGITS-AND-SIGNS
(DEFN ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS
(L)
(IF (NLISTP L)
T
(AND (OR (MEMBER (CAR L)
(ASCII-UPPER-ALPHABETICS))
(MEMBER (CAR L)
(ASCII-DIGITS-AND-SIGNS)))
(ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS (CDR L)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS
is accepted under the principle of definition. From the definition we can
conclude that:
(OR (FALSEP (ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS L))
(TRUEP (ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS L)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS
(DEFN LEGAL-CHAR-CODE-SEQ
(L)
(AND (LISTP L)
(AND (EQUAL (CDR (LAST L)) 0)
(AND (MEMBER (CAR L)
(ASCII-UPPER-ALPHABETICS))
(ALL-UPPER-ALPHABETICS-DIGITS-OR-SIGNS (CDR L))))))
Observe that:
(OR (FALSEP (LEGAL-CHAR-CODE-SEQ L))
(TRUEP (LEGAL-CHAR-CODE-SEQ L)))
is a theorem.
[ 0.0 0.0 0.0 ]
LEGAL-CHAR-CODE-SEQ
(DEFN SYMBOLP
(X)
(AND (LITATOM X)
(LEGAL-CHAR-CODE-SEQ (UNPACK X))))
From the definition we can conclude that:
(OR (FALSEP (SYMBOLP X))
(TRUEP (SYMBOLP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SYMBOLP
(ADD-SHELL PUSH EMPTY-STACK STACKP
((TOP (ONE-OF NUMBERP) ZERO)
(POP (ONE-OF STACKP) EMPTY-STACK)))
[ 0.0 0.0 0.0 ]
PUSH
(DEFN CONCAT
(X Y)
(IF (NLISTP X)
Y
(CONS (CAR X) (CONCAT (CDR X) Y))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call. Hence, CONCAT is
accepted under the definitional principle. From the definition we can
conclude that (OR (LISTP (CONCAT X Y)) (EQUAL (CONCAT X Y) Y)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT
(DEFN SHELL-BASE-FUNCTION
(X)
(IF (EQUAL X 'TRUE)
'TRUEP
(IF (EQUAL X 'FALSE)
'FALSEP
(IF (EQUAL X 'ZERO)
'NUMBERP
(IF (EQUAL X 'EMPTY-STACK)
'STACKP
F)))))
Observe that:
(OR (FALSEP (SHELL-BASE-FUNCTION X))
(LITATOM (SHELL-BASE-FUNCTION X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SHELL-BASE-FUNCTION
(DEFN SHELL-CONSTRUCTOR-FUNCTION
(X)
(IF (EQUAL X 'ADD1)
'NUMBERP
(IF (EQUAL X 'CONS)
'LISTP
(IF (EQUAL X 'PACK)
'LITATOM
(IF (EQUAL X 'MINUS)
'NEGATIVEP
(IF (EQUAL X 'PUSH) 'STACKP F))))))
From the definition we can conclude that:
(OR (FALSEP (SHELL-CONSTRUCTOR-FUNCTION X))
(LITATOM (SHELL-CONSTRUCTOR-FUNCTION X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SHELL-CONSTRUCTOR-FUNCTION
(DEFN SHELL-TYPE-RESTRICTIONS
(X)
(IF (OR (EQUAL X 'ADD1)
(EQUAL X 'MINUS))
(LIST1 (LIST2 'ONE-OF 'NUMBERP))
(IF (EQUAL X 'CONS)
(LIST2 (LIST1 'NONE-OF)
(LIST1 'NONE-OF))
(IF (EQUAL X 'PACK)
(LIST1 (LIST1 'NONE-OF))
(IF (EQUAL X 'PUSH)
(LIST2 (LIST2 'ONE-OF 'NUMBERP)
(LIST2 'ONE-OF 'STACKP))
F)))))
Note that:
(OR (FALSEP (SHELL-TYPE-RESTRICTIONS X))
(LISTP (SHELL-TYPE-RESTRICTIONS X)))
is a theorem.
[ 0.0 0.0 0.0 ]
SHELL-TYPE-RESTRICTIONS
(DEFN SATISFIES
(FN TYPE-RESTRICTION)
(IF (EQUAL (CAR TYPE-RESTRICTION)
'ONE-OF)
(MEMBER (IF (SHELL-BASE-FUNCTION FN)
(SHELL-BASE-FUNCTION FN)
(SHELL-CONSTRUCTOR-FUNCTION FN))
(CDR TYPE-RESTRICTION))
(NOT (MEMBER (IF (SHELL-BASE-FUNCTION FN)
(SHELL-BASE-FUNCTION FN)
(SHELL-CONSTRUCTOR-FUNCTION FN))
(CDR TYPE-RESTRICTION)))))
Observe that:
(OR (FALSEP (SATISFIES FN TYPE-RESTRICTION))
(TRUEP (SATISFIES FN TYPE-RESTRICTION)))
is a theorem.
[ 0.0 0.0 0.0 ]
SATISFIES
(DEFN ALL-SATISFY
(FN-LST TYPE-RESTRICTION-LST)
(IF (NLISTP FN-LST)
T
(AND (SATISFIES (CAR FN-LST)
(CAR TYPE-RESTRICTION-LST))
(ALL-SATISFY (CDR FN-LST)
(CDR TYPE-RESTRICTION-LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to show that the measure (COUNT FN-LST)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, ALL-SATISFY is accepted under the definitional principle. Observe that:
(OR (FALSEP (ALL-SATISFY FN-LST TYPE-RESTRICTION-LST))
(TRUEP (ALL-SATISFY FN-LST TYPE-RESTRICTION-LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-SATISFY
(DEFN ARITY-ALIST NIL
'((IF . 3)
(EQUAL . 2)
(COUNT . 1)
(FALSE . 0)
(FALSEP . 1)
(TRUE . 0)
(TRUEP . 1)
(NOT . 1)
(AND . 2)
(OR . 2)
(IMPLIES . 2)
(ADD1 . 1)
(NUMBERP . 1)
(SUB1 . 1)
(ZERO . 0)
(LESSP . 2)
(GREATERP . 2)
(LEQ . 2)
(GEQ . 2)
(ZEROP . 1)
(FIX . 1)
(PLUS . 2)
(PACK . 1)
(LITATOM . 1)
(UNPACK . 1)
(CONS . 2)
(LISTP . 1)
(CAR . 1)
(CDR . 1)
(NLISTP . 1)
(MINUS . 1)
(NEGATIVEP . 1)
(NEGATIVE-GUTS . 1)
(DIFFERENCE . 2)
(TIMES . 2)
(QUOTIENT . 2)
(REMAINDER . 2)
(MEMBER . 2)
(IFF . 2)
(ORD-LESSP . 2)
(ORDINALP . 1)
(ASSOC . 2)
(PAIRLIST . 2)
(SUBRP . 1)
(APPLY-SUBR . 2)
(FORMALS . 1)
(BODY . 1)
(FIX-COST . 2)
(STRIP-CARS . 1)
(SUM-CDRS . 1)
(V&C$ . 3)
(V&C-APPLY$ . 2)
(APPLY$ . 2)
(EVAL$ . 3)
(QUANTIFIER-INITIAL-VALUE . 1)
(ADD-TO-SET . 2)
(APPEND . 2)
(MAX . 2)
(UNION . 2)
(QUANTIFIER-OPERATION . 3)
(FOR . 6)
(PUSH . 2)
(EMPTY-STACK . 0)
(STACKP . 1)
(TOP . 1)
(POP . 2)
(CONCAT . 2)))
From the definition we can conclude that (LISTP (ARITY-ALIST)) is a
theorem.
[ 0.0 0.0 0.0 ]
ARITY-ALIST
(DEFN ARITY
(FN)
(IF (ASSOC FN (ARITY-ALIST))
(CDR (ASSOC FN (ARITY-ALIST)))
F))
[ 0.0 0.0 0.0 ]
ARITY
(SET-STATUS PRE-EXPLICIT-VALUE-DESCRIPTOR T
((DEFN DISABLE) (OTHERWISE AS-IS)))
[ 0.0 0.0 0.0 ]
PRE-EXPLICIT-VALUE-DESCRIPTOR
(ENABLE CADRN)
[ 0.0 0.0 0.0 ]
CADRN-ON
(ENABLE CDRN)
[ 0.0 0.0 0.0 ]
CDRN-ON
(DEFN EXPLICIT-VALUE-DESCRIPTOR
(FLG X)
(IF FLG
(IF
(NLISTP X)
(IF (INTEGERP X)
(IF (NUMBERP X)
(CORRESPONDING-NUMBERP X)
(CORRESPONDING-NEGATIVEP X))
(IF (EQUAL X (STAR-ONE-STAR 'TRUE))
(LIST1 'TRUE)
(IF (EQUAL X (STAR-ONE-STAR 'FALSE))
(LIST1 'FALSE)
(IF (SYMBOLP X)
(CORRESPONDING-LITATOM X)
F))))
(IF
(EQUAL (CAR X)
(STAR-ONE-STAR 'QUOTE))
(IF
(AND
(OR (SHELL-CONSTRUCTOR-FUNCTION (CADRN 1 X))
(SHELL-BASE-FUNCTION (CADRN 1 X)))
(AND
(EQLEN (CDRN 2 X) (ARITY (CADRN 1 X)))
(AND
(EQUAL (CDR (LAST X)) NIL)
(AND
(NOT (EQUAL (CADRN 1 X) 'ADD1))
(AND
(NOT (EQUAL (CADRN 1 X) 'ZERO))
(AND
(NOT (EQUAL (CADRN 1 X) 'CONS))
(AND
(EXPLICIT-VALUE-DESCRIPTOR F
(CDRN 2 X))
(AND
(IF
(SHELL-CONSTRUCTOR-FUNCTION (CADRN 1 X))
(ALL-SATISFY (STRIP-CARS (EXPLICIT-VALUE-DESCRIPTOR F
(CDRN 2 X)))
(SHELL-TYPE-RESTRICTIONS (CADRN 1 X)))
T)
(IF (EQUAL (CADRN 1 X) 'PACK)
(NOT (LEGAL-CHAR-CODE-SEQ (CADRN 2 X)))
(IF (EQUAL (CADRN 1 X) 'MINUS)
(EQUAL (CADRN 2 X) (ZERO))
T))))))))))
(CONS (CADRN 1 X)
(EXPLICIT-VALUE-DESCRIPTOR F
(CDRN 2 X)))
F)
(IF (DOTTED-PAIR X)
(FLIST3 'CONS
(EXPLICIT-VALUE-DESCRIPTOR T (CAR X))
(EXPLICIT-VALUE-DESCRIPTOR T
(CADRN 2 X)))
(IF (SINGLETON X)
(FLIST3 'CONS
(EXPLICIT-VALUE-DESCRIPTOR T (CAR X))
(CORRESPONDING-LITATOM NIL))
(FLIST3 'CONS
(EXPLICIT-VALUE-DESCRIPTOR T (CAR X))
(EXPLICIT-VALUE-DESCRIPTOR T
(CDR X)))))))
(IF (NLISTP X)
NIL
(FCONS (EXPLICIT-VALUE-DESCRIPTOR T (CAR X))
(EXPLICIT-VALUE-DESCRIPTOR F
(CDR X))))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CDR-LESSEQP, CDR-LESSP,
CAR-LESSEQP, and CAR-LESSP, and the definitions of CDRN, EQUAL, STAR-ONE-STAR,
NLISTP, AND, NOT, OR, and CADRN can be used to establish that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, EXPLICIT-VALUE-DESCRIPTOR is accepted under the
definitional principle. From the definition we can conclude that:
(OR (FALSEP (EXPLICIT-VALUE-DESCRIPTOR FLG X))
(LITATOM (EXPLICIT-VALUE-DESCRIPTOR FLG X))
(LISTP (EXPLICIT-VALUE-DESCRIPTOR FLG X)))
is a theorem.
[ 0.0 0.1 0.0 ]
EXPLICIT-VALUE-DESCRIPTOR
(SET-STATUS POST-EXPLICIT-VALUE-DESCRIPTOR T
((DEFN ENABLE) (OTHERWISE AS-IS)))
[ 0.0 0.0 0.0 ]
POST-EXPLICIT-VALUE-DESCRIPTOR
(DEFN QT
(X)
(EXPLICIT-VALUE-DESCRIPTOR T X))
Observe that (OR (FALSEP (QT X)) (LITATOM (QT X)) (LISTP (QT X))) is a
theorem.
[ 0.0 0.0 0.0 ]
QT
(DEFN DOUBLETS
(LST)
(IF (NLISTP LST)
(EQUAL LST NIL)
(AND (EQLEN (CAR LST) 2)
(DOUBLETS (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
DOUBLETS is accepted under the definitional principle. Note that:
(OR (FALSEP (DOUBLETS LST))
(TRUEP (DOUBLETS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
DOUBLETS
(DEFN DUPLICATESP
(LST)
(IF (NLISTP LST)
F
(IF (MEMBER (CAR LST) (CDR LST))
T
(DUPLICATESP (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
DUPLICATESP is accepted under the definitional principle. Note that:
(OR (FALSEP (DUPLICATESP LST))
(TRUEP (DUPLICATESP LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
DUPLICATESP
(DEFN STRIP-CADRS
(LST)
(IF (NLISTP LST)
NIL
(CONS (CADRN 1 (CAR LST))
(STRIP-CADRS (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
STRIP-CADRS is accepted under the principle of definition. Note that:
(OR (LITATOM (STRIP-CADRS LST))
(LISTP (STRIP-CADRS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
STRIP-CADRS
(DEFN SYMBOLPS
(LST)
(IF (NLISTP LST)
T
(AND (SYMBOLP (CAR LST))
(SYMBOLPS (CDR LST)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT LST) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
SYMBOLPS is accepted under the definitional principle. Observe that:
(OR (FALSEP (SYMBOLPS LST))
(TRUEP (SYMBOLPS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
SYMBOLPS
(DEFN SUBLIS-VAR
(FLG ALIST TERM)
(IF FLG
(IF (NLISTP TERM)
(IF (ASSOC TERM ALIST)
(CDR (ASSOC TERM ALIST))
TERM)
(IF (EQUAL (CAR TERM) 'QUOTE)
TERM
(CONS (CAR TERM)
(SUBLIS-VAR F ALIST (CDR TERM)))))
(IF (NLISTP TERM)
NIL
(CONS (SUBLIS-VAR T ALIST (CAR TERM))
(SUBLIS-VAR F ALIST (CDR TERM)))))
((LESSP (COUNT TERM))))
Linear arithmetic, the lemmas CDR-LESSEQP, CDR-LESSP, CAR-LESSEQP, and
CAR-LESSP, and the definition of NLISTP establish that the measure
(COUNT TERM) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SUBLIS-VAR is accepted under the principle of
definition.
[ 0.0 0.0 0.0 ]
SUBLIS-VAR
(DEFN ABBREVIATED-FOR-VAR
(X)
(CADRN 1 X))
[ 0.0 0.0 0.0 ]
ABBREVIATED-FOR-VAR
(DEFN ABBREVIATED-FOR-RANGE
(X)
(CADRN 3 X))
[ 0.0 0.0 0.0 ]
ABBREVIATED-FOR-RANGE
(DEFN ABBREVIATED-FOR-WHEN
(X)
(IF (EQLEN X 8) (CADRN 5 X) 'T))
[ 0.0 0.0 0.0 ]
ABBREVIATED-FOR-WHEN
(DEFN ABBREVIATED-FOR-OP
(X)
(IF (EQLEN X 8)
(CADRN 6 X)
(CADRN 4 X)))
[ 0.0 0.0 0.0 ]
ABBREVIATED-FOR-OP
(DEFN ABBREVIATED-FOR-BODY
(X)
(CAR (LAST X)))
[ 0.0 0.0 0.0 ]
ABBREVIATED-FOR-BODY
(DEFN FOR-OPERATIONP
(X)
(OR (EQUAL X 'ADD-TO-SET)
(OR (EQUAL X 'ALWAYS)
(OR (EQUAL X 'APPEND)
(OR (EQUAL X 'COLLECT)
(OR (EQUAL X 'COUNT)
(OR (EQUAL X 'DO-RETURN)
(OR (EQUAL X 'EXISTS)
(OR (EQUAL X 'MAX)
(OR (EQUAL X 'SUM)
(OR (EQUAL X 'MULTIPLY)
(EQUAL X 'UNION))))))))))))
Observe that (OR (FALSEP (FOR-OPERATIONP X)) (TRUEP (FOR-OPERATIONP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
FOR-OPERATIONP
(DEFN ABBREVIATED-FORP
(X)
(AND
(LISTP X)
(AND
(EQUAL (CAR X) 'FOR)
(AND
(OR (EQLEN X 8) (EQLEN X 6))
(AND
(SYMBOLP (ABBREVIATED-FOR-VAR X))
(AND (NOT (EQUAL (ABBREVIATED-FOR-VAR X) NIL))
(AND (NOT (EQUAL (ABBREVIATED-FOR-VAR X) 'T))
(AND (NOT (EQUAL (ABBREVIATED-FOR-VAR X) 'F))
(AND (EQUAL (CADRN 2 X) 'IN)
(AND (OR (EQLEN X 6)
(EQUAL (CADRN 4 X) 'WHEN))
(FOR-OPERATIONP (ABBREVIATED-FOR-OP X))))))))))))
From the definition we can conclude that:
(OR (FALSEP (ABBREVIATED-FORP X))
(TRUEP (ABBREVIATED-FORP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
ABBREVIATED-FORP
(DEFN ALPHABETIC-LESSP1
(L1 L2)
(IF (NLISTP L1)
T
(IF (NLISTP L2)
F
(IF (LESSP (CAR L1) (CAR L2))
T
(IF (EQUAL (CAR L1) (CAR L2))
(ALPHABETIC-LESSP1 (CDR L1) (CDR L2))
F)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L1) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
ALPHABETIC-LESSP1 is accepted under the principle of definition. The
definition of ALPHABETIC-LESSP1 can be justified in another way. Linear
arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP
can be used to establish that the measure (COUNT L2) decreases according to
the well-founded relation LESSP in each recursive call. Observe that:
(OR (FALSEP (ALPHABETIC-LESSP1 L1 L2))
(TRUEP (ALPHABETIC-LESSP1 L1 L2)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALPHABETIC-LESSP1
(DEFN ALPHABETIC-LESSP
(X Y)
(ALPHABETIC-LESSP1 (UNPACK X)
(UNPACK Y)))
Note that:
(OR (FALSEP (ALPHABETIC-LESSP X Y))
(TRUEP (ALPHABETIC-LESSP X Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALPHABETIC-LESSP
(DEFN ALPHABETIC-INSERT
(X L)
(IF (NLISTP L)
(LIST1 X)
(IF (ALPHABETIC-LESSP X (CAR L))
(CONS X L)
(CONS (CAR L)
(ALPHABETIC-INSERT X (CDR L))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definitions of ALPHABETIC-LESSP and NLISTP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, ALPHABETIC-INSERT is accepted under the definitional
principle. Note that (LISTP (ALPHABETIC-INSERT X L)) is a theorem.
[ 0.0 0.0 0.0 ]
ALPHABETIC-INSERT
(DEFN ALPHABETIZE
(L)
(IF (NLISTP L)
L
(ALPHABETIC-INSERT (CAR L)
(ALPHABETIZE (CDR L)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP can be used to establish that the measure (COUNT L)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, ALPHABETIZE is accepted under the principle of definition. From the
definition we can conclude that:
(OR (LISTP (ALPHABETIZE L))
(EQUAL (ALPHABETIZE L) L))
is a theorem.
[ 0.0 0.0 0.0 ]
ALPHABETIZE
(DEFN ALL-VARS
(FLG X)
(IF FLG
(IF (NLISTP X)
(CONS X NIL)
(ALL-VARS F (CDR X)))
(IF (NLISTP X)
NIL
(UNION (ALL-VARS T (CAR X))
(ALL-VARS F (CDR X))))))
Linear arithmetic, the lemmas CDR-LESSEQP, CDR-LESSP, CAR-LESSEQP, and
CAR-LESSP, and the definition of NLISTP can be used to establish that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each recursive call. Hence, ALL-VARS is accepted under the definitional
principle. Note that (OR (LITATOM (ALL-VARS FLG X)) (LISTP (ALL-VARS FLG X)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-VARS
(DEFN STANDARD-ALIST
(VARS)
(IF (NLISTP VARS)
(QT NIL)
(LIST3 'CONS
(LIST3 'CONS
(QT (CAR VARS))
(CAR VARS))
(STANDARD-ALIST (CDR VARS)))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT VARS) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
STANDARD-ALIST is accepted under the principle of definition. Note that:
(OR (FALSEP (STANDARD-ALIST VARS))
(LITATOM (STANDARD-ALIST VARS))
(LISTP (STANDARD-ALIST VARS)))
is a theorem.
[ 0.0 0.0 0.0 ]
STANDARD-ALIST
(DEFN DELETE
(X L)
(IF (NLISTP L)
L
(IF (EQUAL X (CAR L))
(CDR L)
(CONS (CAR L) (DELETE X (CDR L))))))
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call. Hence, DELETE is
accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
DELETE
(DEFN MAKE-ALIST
(VAR WHEN BODY)
(STANDARD-ALIST (ALPHABETIZE (DELETE VAR
(UNION (ALL-VARS T WHEN)
(ALL-VARS T BODY))))))
Note that:
(OR (FALSEP (MAKE-ALIST VAR WHEN BODY))
(LITATOM (MAKE-ALIST VAR WHEN BODY))
(LISTP (MAKE-ALIST VAR WHEN BODY)))
is a theorem.
[ 0.1 0.0 0.0 ]
MAKE-ALIST
(PROVE-LEMMA LESSP-ABBREVIATED-FOR-RANGE
(REWRITE)
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (ABBREVIATED-FOR-RANGE X))
(COUNT X))))
WARNING: Note that the proposed lemma LESSP-ABBREVIATED-FOR-RANGE is to be
stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.
This formula can be simplified, using the abbreviations IMPLIES, CDRN-EXPANDER,
CADRN, and ABBREVIATED-FOR-RANGE, to:
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (CAR (CDRN 0 (CDDDR X))))
(COUNT X))),
which simplifies, unfolding the definitions of EQUAL and CDRN, to:
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (CADDDR X)) (COUNT X))).
This again simplifies, using linear arithmetic and rewriting with CDR-LESSEQP
and CAR-LESSEQP, to the new formula:
(IMPLIES (AND (EQUAL (COUNT (CDR X)) (COUNT X))
(EQUAL (CAR X) 'FOR))
(LESSP (COUNT (CADDDR X)) (COUNT X))).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X)
and (CAR X), Z by (CONS D W) to eliminate (CDR Z) and (CAR Z), W by (CONS C Z)
to eliminate (CDR W) and (CAR W), and Z by (CONS W X1) to eliminate (CAR Z)
and (CDR Z). We thus obtain the following five new formulas:
Case 5. (IMPLIES (AND (NOT (LISTP X))
(EQUAL (COUNT (CDR X)) (COUNT X))
(EQUAL (CAR X) 'FOR))
(LESSP (COUNT (CADDDR X)) (COUNT X))).
However this further simplifies, applying the lemmas CDR-NLISTP and
CAR-NLISTP, and expanding COUNT and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (LISTP Z))
(EQUAL (COUNT Z) (COUNT (CONS V Z)))
(EQUAL V 'FOR))
(LESSP (COUNT (CADDR Z))
(COUNT (CONS V Z)))),
which further simplifies, applying COUNT-CONS and CDR-NLISTP, and opening up
the functions COUNT, CDR, CAR, EQUAL, and LESSP, to:
(IMPLIES (AND (NOT (LISTP Z))
(EQUAL (COUNT Z)
(ADD1 (PLUS 235 (COUNT Z)))))
(NOT (EQUAL (COUNT Z) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (LISTP W))
(EQUAL (COUNT (CONS D W))
(COUNT (CONS V (CONS D W))))
(EQUAL V 'FOR))
(LESSP (COUNT (CADR W))
(COUNT (CONS V (CONS D W))))),
which further simplifies, rewriting with COUNT-CONS, ADD1-EQUAL, and
CDR-NLISTP, and expanding the functions COUNT, CAR, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP Z))
(EQUAL (COUNT (CONS D (CONS C Z)))
(COUNT (CONS V (CONS D (CONS C Z)))))
(EQUAL V 'FOR))
(LESSP (COUNT (CAR Z))
(COUNT (CONS V (CONS D (CONS C Z)))))).
This further simplifies, applying COUNT-CONS, ADD1-EQUAL, and CAR-NLISTP,
and opening up COUNT, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (EQUAL (COUNT (CONS D (CONS C (CONS W X1))))
(COUNT (CONS V
(CONS D (CONS C (CONS W X1))))))
(EQUAL V 'FOR))
(LESSP (COUNT W)
(COUNT (CONS V
(CONS D (CONS C (CONS W X1))))))).
But this further simplifies, applying COUNT-CONS, ADD1-EQUAL, and SUB1-ADD1,
and opening up COUNT and LESSP, to the new formula:
(IMPLIES
(AND
(EQUAL
(PLUS (COUNT D)
(ADD1 (PLUS (COUNT C)
(ADD1 (PLUS (COUNT W) (COUNT X1))))))
(PLUS 235
(ADD1 (PLUS (COUNT D)
(ADD1 (PLUS (COUNT C)
(ADD1 (PLUS (COUNT W) (COUNT X1)))))))))
(NOT (EQUAL (COUNT W) 0)))
(LESSP (SUB1 (COUNT W))
(PLUS (COUNT D)
(ADD1 (PLUS (COUNT C)
(ADD1 (PLUS (COUNT W) (COUNT X1)))))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-ABBREVIATED-FOR-RANGE
(PROVE-LEMMA LESSP-ABBREVIATED-FOR-WHEN
(REWRITE)
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (ABBREVIATED-FOR-WHEN X))
(COUNT X))))
WARNING: Note that the proposed lemma LESSP-ABBREVIATED-FOR-WHEN is to be
stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.
This conjecture simplifies, applying CDRN-EXPANDER, and expanding the
functions CADRN, EQUAL, CDRN, and ABBREVIATED-FOR-WHEN, to two new conjectures:
Case 2. (IMPLIES (AND (EQUAL (CAR X) 'FOR)
(NOT (EQLEN X 8)))
(LESSP (COUNT 'T) (COUNT X))),
which again simplifies, expanding the function COUNT, to:
(IMPLIES (AND (EQUAL (CAR X) 'FOR)
(NOT (EQLEN X 8)))
(LESSP 86 (COUNT X))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to
eliminate (CAR X) and (CDR X). We must thus prove two new goals:
Case 2.2.
(IMPLIES (AND (NOT (LISTP X))
(EQUAL (CAR X) 'FOR)
(NOT (EQLEN X 8)))
(LESSP 86 (COUNT X))),
which further simplifies, rewriting with CAR-NLISTP, and unfolding EQUAL,
to:
T.
Case 2.1.
(IMPLIES (AND (EQUAL Z 'FOR)
(NOT (EQLEN (CONS Z V) 8)))
(LESSP 86 (COUNT (CONS Z V)))).
But this further simplifies, applying CDR-CONS, COUNT-CONS, and SUB1-ADD1,
and unfolding SUB1, NUMBERP, EQUAL, EQLEN, COUNT, and LESSP, to:
(IMPLIES (NOT (EQLEN V 7))
(LESSP 85 (PLUS 235 (COUNT V)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (CAR X) 'FOR)
(EQLEN X 8))
(LESSP (COUNT (CADDDDDR X))
(COUNT X))),
which again simplifies, using linear arithmetic and rewriting with the
lemmas CDR-LESSEQP and CAR-LESSEQP, to the formula:
(IMPLIES (AND (EQUAL (COUNT (CDR X)) (COUNT X))
(EQUAL (CAR X) 'FOR)
(EQLEN X 8))
(LESSP (COUNT (CADDDDDR X))
(COUNT X))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to
eliminate (CDR X) and (CAR X), Z by (CONS D W) to eliminate (CDR Z) and
(CAR Z), W by (CONS C Z) to eliminate (CDR W) and (CAR W), Z by (CONS X1 W)
to eliminate (CDR Z) and (CAR Z), W by (CONS Z1 Z) to eliminate (CDR W) and
(CAR W), and Z by (CONS W V1) to eliminate (CAR Z) and (CDR Z). This
generates seven new formulas:
Case 1.7.
(IMPLIES (AND (NOT (LISTP X))
(EQUAL (COUNT (CDR X)) (COUNT X))
(EQUAL (CAR X) 'FOR)
(EQLEN X 8))
(LESSP (COUNT (CADDDDDR X))
(COUNT X))),
which further simplifies, rewriting with CDR-NLISTP and CAR-NLISTP, and
unfolding the functions COUNT and EQUAL, to:
T.
Case 1.6.
(IMPLIES (AND (NOT (LISTP Z))
(EQUAL (COUNT Z) (COUNT (CONS V Z)))
(EQUAL V 'FOR)
(EQLEN (CONS V Z) 8))
(LESSP (COUNT (CADDDDR Z))
(COUNT (CONS V Z)))).
This further simplifies, rewriting with COUNT-CONS and CDR-CONS, and
opening up the functions COUNT, SUB1, NUMBERP, EQUAL, and EQLEN, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (LISTP W))
(EQUAL (COUNT (CONS D W))
(COUNT (CONS V (CONS D W))))
(EQUAL V 'FOR)
(EQLEN (CONS V (CONS D W)) 8))
(LESSP (COUNT (CADDDR W))
(COUNT (CONS V (CONS D W))))).
This further simplifies, rewriting with COUNT-CONS, ADD1-EQUAL, and
CDR-CONS, and unfolding the functions COUNT, SUB1, NUMBERP, EQUAL, and
EQLEN, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (LISTP Z))
(EQUAL (COUNT (CONS D (CONS C Z)))
(COUNT (CONS V (CONS D (CONS C Z)))))
(EQUAL V 'FOR)
(EQLEN (CONS V (CONS D (CONS C Z)))
8))
(LESSP (COUNT (CADDR Z))
(COUNT (CONS V (CONS D (CONS C Z)))))).
But this further simplifies, applying COUNT-CONS, ADD1-EQUAL, and CDR-CONS,
and opening up COUNT, SUB1, NUMBERP, EQUAL, and EQLEN, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (LISTP W))
(EQUAL (COUNT (CONS D (CONS C (CONS X1 W))))
(COUNT (CONS V
(CONS D (CONS C (CONS X1 W))))))
(EQUAL V 'FOR)
(EQLEN (CONS V (CONS D (CONS C (CONS X1 W))))
8))
(LESSP (COUNT (CADR W))
(COUNT (CONS V
(CONS D (CONS C (CONS X1 W))))))).
However this further simplifies, applying COUNT-CONS, ADD1-EQUAL, and
CDR-CONS, and expanding COUNT, SUB1, NUMBERP, EQUAL, and EQLEN, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (LISTP Z))
(EQUAL (COUNT (CONS D
(CONS C (CONS X1 (CONS Z1 Z)))))
(COUNT (CONS V
(CONS D
(CONS C (CONS X1 (CONS Z1 Z)))))))
(EQUAL V 'FOR)
(EQLEN (CONS V
(CONS D
(CONS C (CONS X1 (CONS Z1 Z)))))
8))
(LESSP (COUNT (CAR Z))
(COUNT (CONS V
(CONS D
(CONS C (CONS X1 (CONS Z1 Z)))))))).
This further simplifies, applying the lemmas COUNT-CONS, ADD1-EQUAL, and
CDR-CONS, and unfolding the functions COUNT, SUB1, NUMBERP, EQUAL, and
EQLEN, to:
T.
Case 1.1.
(IMPLIES
(AND
(EQUAL
(COUNT (CONS D
(CONS C
(CONS X1 (CONS Z1 (CONS W V1))))))
(COUNT (CONS V
(CONS D
(CONS C
(CONS X1 (CONS Z1 (CONS W V1))))))))
(EQUAL V 'FOR)
(EQLEN (CONS V
(CONS D
(CONS C
(CONS X1 (CONS Z1 (CONS W V1))))))
8))
(LESSP
(COUNT W)
(COUNT (CONS V
(CONS D
(CONS C
(CONS X1 (CONS Z1 (CONS W V1))))))))),
which further simplifies, rewriting with COUNT-CONS, ADD1-EQUAL, CDR-CONS,
and SUB1-ADD1, and opening up COUNT, SUB1, NUMBERP, EQUAL, EQLEN, and
LESSP, to:
(IMPLIES
(AND
(EQUAL
(PLUS
(COUNT D)
(ADD1
(PLUS
(COUNT C)
(ADD1
(PLUS (COUNT X1)
(ADD1 (PLUS (COUNT Z1)
(ADD1 (PLUS (COUNT W) (COUNT V1))))))))))
(PLUS 235
(ADD1
(PLUS
(COUNT D)
(ADD1
(PLUS
(COUNT C)
(ADD1
(PLUS
(COUNT X1)
(ADD1 (PLUS (COUNT Z1)
(ADD1 (PLUS (COUNT W) (COUNT V1)))))))))))))
(EQLEN V1 2)
(NOT (EQUAL (COUNT W) 0)))
(LESSP
(SUB1 (COUNT W))
(PLUS
(COUNT D)
(ADD1
(PLUS
(COUNT C)
(ADD1
(PLUS (COUNT X1)
(ADD1 (PLUS (COUNT Z1)
(ADD1 (PLUS (COUNT W) (COUNT V1)))))))))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
LESSP-ABBREVIATED-FOR-WHEN
(PROVE-LEMMA LESSP-LAST
(REWRITE)
(NOT (LESSP (COUNT X) (COUNT (LAST X)))))
WARNING: Note that the proposed lemma LESSP-LAST 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 (NLISTP X) (p X))
(IMPLIES (AND (NOT (NLISTP X))
(NLISTP (CDR X)))
(p X))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (NLISTP (CDR X)))
(p (CDR X)))
(p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP 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 produces the following three new goals:
Case 3. (IMPLIES (NLISTP X)
(NOT (LESSP (COUNT X) (COUNT (LAST X))))).
This simplifies, expanding NLISTP and LAST, to:
(IMPLIES (NOT (LISTP X))
(NOT (LESSP (COUNT X) (COUNT X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NLISTP (CDR X)))
(NOT (LESSP (COUNT X) (COUNT (LAST X))))),
which simplifies, expanding the functions NLISTP and LAST, to:
(IMPLIES (AND (LISTP X) (NOT (LISTP (CDR X))))
(NOT (LESSP (COUNT X) (COUNT X)))).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (NLISTP (CDR X)))
(NOT (LESSP (COUNT (CDR X))
(COUNT (LAST (CDR X))))))
(NOT (LESSP (COUNT X) (COUNT (LAST X))))),
which simplifies, unfolding NLISTP and LAST, to:
(IMPLIES (AND (LISTP X)
(LISTP (CDR X))
(NOT (LESSP (COUNT (CDR X))
(COUNT (LAST (CDR X))))))
(NOT (LESSP (COUNT X)
(COUNT (LAST (CDR X)))))).
But this again simplifies, using linear arithmetic and rewriting with
CDR-LESSEQP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-LAST
(PROVE-LEMMA LESSP-ABBREVIATED-FOR-BODY
(REWRITE)
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (ABBREVIATED-FOR-BODY X))
(COUNT X))))
WARNING: Note that the proposed lemma LESSP-ABBREVIATED-FOR-BODY is to be
stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.
This formula can be simplified, using the abbreviations IMPLIES and
ABBREVIATED-FOR-BODY, to:
(IMPLIES (EQUAL (CAR X) 'FOR)
(LESSP (COUNT (CAR (LAST X)))
(COUNT X))),
which simplifies, using linear arithmetic and rewriting with LESSP-LAST and
CAR-LESSEQP, to:
(IMPLIES (AND (EQUAL (COUNT (LAST X)) (COUNT X))
(EQUAL (CAR X) 'FOR))
(LESSP (COUNT (CAR (LAST X)))
(COUNT X))).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate (CAR X)
and (CDR X). We would thus like to prove the following two new formulas:
Case 2. (IMPLIES (AND (NOT (LISTP X))
(EQUAL (COUNT (LAST X)) (COUNT X))
(EQUAL (CAR X) 'FOR))
(LESSP (COUNT (CAR (LAST X)))
(COUNT X))).
This further simplifies, applying CAR-NLISTP, and opening up the functions
LAST and EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (COUNT (LAST (CONS Z V)))
(COUNT (CONS Z V)))
(EQUAL Z 'FOR))
(LESSP (COUNT (CAR (LAST (CONS Z V))))
(COUNT (CONS Z V)))).
However this further simplifies, using linear arithmetic and rewriting with
CAR-LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-ABBREVIATED-FOR-BODY
(PROVE-LEMMA LESSP-COUNT-STRIP-CARS
(REWRITE)
(IMPLIES (DOUBLETS LST)
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CARS LST))))))
WARNING: Note that the proposed lemma LESSP-COUNT-STRIP-CARS is to be stored
as zero type prescription rules, zero compound recognizer rules, one linear
rule, and zero replacement rules.
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP LST) (p LST))
(IMPLIES (AND (NOT (NLISTP LST)) (p (CDR LST)))
(p LST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT LST) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to the following three new goals:
Case 3. (IMPLIES (AND (NLISTP LST) (DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CARS LST))))).
This simplifies, expanding the definitions of NLISTP, DOUBLETS, COUNT,
STRIP-CARS, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (DOUBLETS (CDR LST)))
(DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CARS LST))))).
This simplifies, unfolding NLISTP and DOUBLETS, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CARS (CDR LST)))))
(DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CARS LST))))).
This simplifies, rewriting with COUNT-CONS and SUB1-ADD1, and expanding the
definitions of NLISTP, DOUBLETS, STRIP-CARS, and LESSP, to two new
conjectures:
Case 1.2.
(IMPLIES (AND (LISTP LST)
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CARS (CDR LST)))))
(EQLEN (CAR LST) 2)
(DOUBLETS (CDR LST)))
(NOT (EQUAL (COUNT LST) 0))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
(CDR LST) and (CAR LST). This produces:
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CARS X))))
(EQLEN Z 2)
(DOUBLETS X))
(NOT (EQUAL (COUNT (CONS Z X)) 0))),
which further simplifies, applying the lemma COUNT-CONS, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP LST)
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CARS (CDR LST)))))
(EQLEN (CAR LST) 2)
(DOUBLETS (CDR LST)))
(NOT (LESSP (SUB1 (COUNT LST))
(PLUS (COUNT (CAAR LST))
(COUNT (STRIP-CARS (CDR LST))))))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
(CDR LST) and (CAR LST) and Z by (CONS V W) to eliminate (CAR Z) and
(CDR Z). This produces the following two new conjectures:
Case 1.1.2.
(IMPLIES (AND (NOT (LISTP Z))
(NOT (LESSP (COUNT X)
(COUNT (STRIP-CARS X))))
(EQLEN Z 2)
(DOUBLETS X))
(NOT (LESSP (SUB1 (COUNT (CONS Z X)))
(PLUS (COUNT (CAR Z))
(COUNT (STRIP-CARS X)))))).
However this further simplifies, opening up NUMBERP, EQUAL, and EQLEN,
to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CARS X))))
(EQLEN (CONS V W) 2)
(DOUBLETS X))
(NOT (LESSP (SUB1 (COUNT (CONS (CONS V W) X)))
(PLUS (COUNT V)
(COUNT (STRIP-CARS X)))))),
which further simplifies, applying CDR-CONS, COUNT-CONS, and SUB1-ADD1,
and expanding the functions SUB1, NUMBERP, EQUAL, EQLEN, PLUS, and LESSP,
to:
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CARS X))))
(EQLEN W 1)
(DOUBLETS X)
(NOT (EQUAL (PLUS (COUNT V)
(COUNT (STRIP-CARS X)))
0)))
(NOT (LESSP (PLUS (PLUS (COUNT V) (COUNT W))
(COUNT X))
(SUB1 (PLUS (COUNT V)
(COUNT (STRIP-CARS X))))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-COUNT-STRIP-CARS
(PROVE-LEMMA LESSP-COUNT-STRIP-CADRS
(REWRITE)
(IMPLIES (DOUBLETS LST)
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CADRS LST))))))
WARNING: Note that the proposed lemma LESSP-COUNT-STRIP-CADRS is to be stored
as zero type prescription rules, zero compound recognizer rules, one linear
rule, and zero replacement rules.
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP LST) (p LST))
(IMPLIES (AND (NOT (NLISTP LST)) (p (CDR LST)))
(p LST))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT LST) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to the following three new goals:
Case 3. (IMPLIES (AND (NLISTP LST) (DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CADRS LST))))).
This simplifies, expanding the definitions of NLISTP, DOUBLETS, COUNT,
STRIP-CADRS, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (DOUBLETS (CDR LST)))
(DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CADRS LST))))).
This simplifies, unfolding NLISTP and DOUBLETS, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP LST))
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CADRS (CDR LST)))))
(DOUBLETS LST))
(NOT (LESSP (COUNT LST)
(COUNT (STRIP-CADRS LST))))).
This simplifies, rewriting with CDRN-EXPANDER, COUNT-CONS, and SUB1-ADD1,
and expanding the definitions of NLISTP, DOUBLETS, STRIP-CADRS, CDRN, EQUAL,
CADRN, and LESSP, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP LST)
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CADRS (CDR LST)))))
(EQLEN (CAR LST) 2)
(DOUBLETS (CDR LST)))
(NOT (EQUAL (COUNT LST) 0))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
(CDR LST) and (CAR LST). This produces:
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CADRS X))))
(EQLEN Z 2)
(DOUBLETS X))
(NOT (EQUAL (COUNT (CONS Z X)) 0))),
which further simplifies, applying the lemma COUNT-CONS, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP LST)
(NOT (LESSP (COUNT (CDR LST))
(COUNT (STRIP-CADRS (CDR LST)))))
(EQLEN (CAR LST) 2)
(DOUBLETS (CDR LST)))
(NOT (LESSP (SUB1 (COUNT LST))
(PLUS (COUNT (CADAR LST))
(COUNT (STRIP-CADRS (CDR LST))))))).
Applying the lemma CAR-CDR-ELIM, replace LST by (CONS Z X) to eliminate
(CDR LST) and (CAR LST), Z by (CONS W V) to eliminate (CDR Z) and (CAR Z),
and V by (CONS Z D) to eliminate (CAR V) and (CDR V). This produces the
following three new conjectures:
Case 1.1.3.
(IMPLIES (AND (NOT (LISTP Z))
(NOT (LESSP (COUNT X)
(COUNT (STRIP-CADRS X))))
(EQLEN Z 2)
(DOUBLETS X))
(NOT (LESSP (SUB1 (COUNT (CONS Z X)))
(PLUS (COUNT (CADR Z))
(COUNT (STRIP-CADRS X)))))).
However this further simplifies, opening up NUMBERP, EQUAL, and EQLEN,
to:
T.
Case 1.1.2.
(IMPLIES (AND (NOT (LISTP V))
(NOT (LESSP (COUNT X)
(COUNT (STRIP-CADRS X))))
(EQLEN (CONS W V) 2)
(DOUBLETS X))
(NOT (LESSP (SUB1 (COUNT (CONS (CONS W V) X)))
(PLUS (COUNT (CAR V))
(COUNT (STRIP-CADRS X)))))),
which further simplifies, applying CDR-CONS, and expanding the functions
SUB1, NUMBERP, EQUAL, and EQLEN, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CADRS X))))
(EQLEN (CONS W (CONS Z D)) 2)
(DOUBLETS X))
(NOT (LESSP (SUB1 (COUNT (CONS (CONS W (CONS Z D)) X)))
(PLUS (COUNT Z)
(COUNT (STRIP-CADRS X)))))).
But this further simplifies, rewriting with CDR-CONS, COUNT-CONS, and
SUB1-ADD1, and unfolding SUB1, NUMBERP, EQUAL, EQLEN, COUNT, PLUS, and
LESSP, to the new goal:
(IMPLIES (AND (NOT (LESSP (COUNT X)
(COUNT (STRIP-CADRS X))))
(EQUAL D NIL)
(DOUBLETS X)
(NOT (EQUAL (PLUS (COUNT Z)
(COUNT (STRIP-CADRS X)))
0)))
(NOT (LESSP (PLUS (PLUS (COUNT W)
(ADD1 (PLUS (COUNT Z) 231)))
(COUNT X))
(SUB1 (PLUS (COUNT Z)
(COUNT (STRIP-CADRS X))))))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-COUNT-STRIP-CADRS
(PROVE-LEMMA LISTP-CDDR-X-COUNT-X
(REWRITE)
(IMPLIES (LISTP (CDDR X))
(EQUAL (COUNT X)
(ADD1 (ADD1 (PLUS (COUNT (CAR X))
(PLUS (COUNT (CADR X))
(COUNT (CDDR X)))))))))
.
Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS V Z) to
eliminate (CDR X) and (CAR X) and Z by (CONS D W) to eliminate (CDR Z) and
(CAR Z). We must thus prove three new formulas:
Case 3. (IMPLIES (AND (NOT (LISTP X)) (LISTP (CDDR X)))
(EQUAL (COUNT X)
(ADD1 (ADD1 (PLUS (COUNT (CAR X))
(COUNT (CADR X))
(COUNT (CDDR X))))))),
which simplifies, applying CDR-NLISTP, and unfolding CDR and LISTP, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP Z)) (LISTP (CDR Z)))
(EQUAL (COUNT (CONS V Z))
(ADD1 (ADD1 (PLUS (COUNT V)
(COUNT (CAR Z))
(COUNT (CDR Z))))))).
But this simplifies, rewriting with the lemma CDR-NLISTP, and opening up the
definition of LISTP, to:
T.
Case 1. (IMPLIES (LISTP W)
(EQUAL (COUNT (CONS V (CONS D W)))
(ADD1 (ADD1 (PLUS (COUNT V)
(COUNT D)
(COUNT W)))))),
which simplifies, rewriting with the lemmas COUNT-CONS and ADD1-EQUAL, to:
(IMPLIES (LISTP W)
(EQUAL (PLUS (COUNT V)
(ADD1 (PLUS (COUNT D) (COUNT W))))
(ADD1 (PLUS (COUNT V)
(COUNT D)
(COUNT W))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LISTP-CDDR-X-COUNT-X
(PROVE-LEMMA LISTP-CDDDR-X-COUNT-X
(REWRITE)
(IMPLIES (LISTP (CDDDR X))
(EQUAL (COUNT X)
(ADD1 (ADD1 (ADD1 (PLUS (COUNT (CAR X))
(PLUS (COUNT (CADR X))
(PLUS (COUNT (CADDR X))
(COUNT (CDDDR X)))))))))))
.
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate (CDR X)
and (CAR X), Z by (CONS D W) to eliminate (CDR Z) and (CAR Z), and W by
(CONS C Z) to eliminate (CDR W) and (CAR W). This produces the following four
new formulas:
Case 4. (IMPLIES (AND (NOT (LISTP X))
(LISTP (CDDDR X)))
(EQUAL (COUNT X)
(ADD1 (ADD1 (ADD1 (PLUS (COUNT (CAR X))
(COUNT (CADR X))
(COUNT (CADDR X))
(COUNT (CDDDR X)))))))).
This simplifies, applying CDR-NLISTP, and opening up the definitions of CDR
and LISTP, to:
T.
Case 3. (IMPLIES (AND (NOT (LISTP Z)) (LISTP (CDDR Z)))
(EQUAL (COUNT (CONS V Z))
(ADD1 (ADD1 (ADD1 (PLUS (COUNT V)
(COUNT (CAR Z))
(COUNT (CADR Z))
(COUNT (CDDR Z)))))))).
However this simplifies, applying CDR-NLISTP, and unfolding the functions
CDR and LISTP, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP W)) (LISTP (CDR W)))
(EQUAL (COUNT (CONS V (CONS D W)))
(ADD1 (ADD1 (ADD1 (PLUS (COUNT V)
(COUNT D)
(COUNT (CAR W))
(COUNT (CDR W)))))))).
This simplifies, rewriting with CDR-NLISTP, and opening up the function
LISTP, to:
T.
Case 1. (IMPLIES (LISTP Z)
(EQUAL (COUNT (CONS V (CONS D (CONS C Z))))
(ADD1 (ADD1 (ADD1 (PLUS (COUNT V)
(COUNT D)
(COUNT C)
(COUNT Z))))))).
But this simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, COUNT-CONS,
LISTP-CDDR-X-COUNT-X, and ADD1-EQUAL, to the goal:
(IMPLIES (LISTP Z)
(EQUAL (PLUS (COUNT V)
(COUNT D)
(ADD1 (PLUS (COUNT C) (COUNT Z))))
(ADD1 (PLUS (COUNT V)
(COUNT D)
(COUNT C)
(COUNT Z))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LISTP-CDDDR-X-COUNT-X
(SET-STATUS PRE-TRANSLATE T
((DEFN DISABLE) (OTHERWISE AS-IS)))
[ 0.0 0.0 0.0 ]
PRE-TRANSLATE
(ENABLE CADRN)
[ 0.0 0.0 0.0 ]
CADRN-ON1
(ENABLE CDRN)
[ 0.0 0.0 0.0 ]
CDRN-ON1
(DEFN TRANSLATE
(FLG X)
(IF FLG
(IF
(NLISTP X)
(IF (INTEGERP X)
(QT X)
(IF (SYMBOLP X)
(IF (EQUAL X 'T)
(LIST1 'TRUE)
(IF (EQUAL X 'F)
(LIST1 'FALSE)
(IF (EQUAL X NIL) (QT NIL) X)))
F))
(IF
(DOTTED-S-EXPRESSION X)
F
(IF
(EQUAL (CAR X) 'QUOTE)
(IF (EQLEN X 2) (QT (CADRN 1 X)) F)
(IF
(EQUAL (CAR X) 'COND)
(IF (AND (EQLEN X 2)
(AND (EQLEN (CADRN 1 X) 2)
(EQUAL (CAR (CADRN 1 X)) 'T)))
(TRANSLATE T (CADRN 1 (CADRN 1 X)))
(IF (AND (EQLEN (CADRN 1 X) 2)
(AND (NOT (EQUAL (CAR (CADRN 1 X)) 'T))
(LISTP (CDRN 2 X))))
(FLIST4 'IF
(TRANSLATE T (CAR (CADRN 1 X)))
(TRANSLATE T (CADRN 1 (CADRN 1 X)))
(TRANSLATE T
(CONS 'COND (CDRN 2 X))))
F))
(IF
(EQUAL (CAR X) 'CASE)
(IF (AND (EQLEN X 3)
(AND (EQLEN (CADRN 2 X) 2)
(AND (EQUAL (CAR (CADRN 2 X)) 'OTHERWISE)
(TRANSLATE T (CADRN 1 X)))))
(TRANSLATE T (CADRN 1 (CADRN 2 X)))
(IF (AND (EQLEN (CADRN 2 X) 2)
(AND (LISTP (CDRN 3 X))
(NOT (MEMBER (CAR (CADRN 2 X))
(STRIP-CARS (CDRN 3 X))))))
(FLIST4 'IF
(FLIST3 'EQUAL
(TRANSLATE T (CADRN 1 X))
(QT (CAR (CADRN 2 X))))
(TRANSLATE T (CADRN 1 (CADRN 2 X)))
(TRANSLATE T
(CONS 'CASE
(CONS (CADRN 1 X) (CDRN 3 X)))))
F))
(IF
(EQUAL (CAR X) 'LET)
(IF
(DOUBLETS (CADRN 1 X))
(IF
(AND
(EQLEN X 3)
(AND
(TRANSLATE F (STRIP-CARS (CADRN 1 X)))
(AND
(TRANSLATE F
(STRIP-CADRS (CADRN 1 X)))
(AND
(TRANSLATE T (CADRN 2 X))
(AND
(SYMBOLPS (TRANSLATE F
(STRIP-CARS (CADRN 1 X))))
(NOT (DUPLICATESP (TRANSLATE F
(STRIP-CARS (CADRN 1 X))))))))))
(SUBLIS-VAR T
(PAIRLIST (TRANSLATE F (STRIP-CARS (CADRN 1 X)))
(TRANSLATE F
(STRIP-CADRS (CADRN 1 X))))
(TRANSLATE T (CADRN 2 X)))
F)
F)
(IF
(NOT (TRANSLATE F (CDR X)))
F
(IF
(OR (EQUAL (CAR X) NIL)
(OR (EQUAL (CAR X) 'T)
(EQUAL (CAR X) 'F)))
F
(IF
(EQUAL (CAR X) 'LIST)
(FN-NEST 'CONS
(TRANSLATE F (CDR X))
(QT NIL))
(IF
(EQUAL (CAR X) 'LIST*)
(IF (EQLEN X 1)
F
(FN-NEST 'CONS
(ALL-BUT-LAST (TRANSLATE F (CDR X)))
(CAR (LAST (TRANSLATE F (CDR X))))))
(IF
(CAR-CDR-SYMBOLP (CAR X))
(IF (EQLEN X 2)
(CAR-CDR-NEST (A-D-SEQUENCE (CAR X))
(TRANSLATE T (CADRN 1 X)))
F)
(IF
(EQLEN (CDR X) (ARITY (CAR X)))
(FCONS (CAR X) (TRANSLATE F (CDR X)))
(IF
(EQUAL (CAR X) 'FOR)
(IF (ABBREVIATED-FORP X)
(FLIST7 'FOR
(QT (ABBREVIATED-FOR-VAR X))
(TRANSLATE T
(ABBREVIATED-FOR-RANGE X))
(QT (TRANSLATE T
(ABBREVIATED-FOR-WHEN X)))
(QT (ABBREVIATED-FOR-OP X))
(QT (TRANSLATE T
(ABBREVIATED-FOR-BODY X)))
(MAKE-ALIST (ABBREVIATED-FOR-VAR X)
(TRANSLATE T (ABBREVIATED-FOR-WHEN X))
(TRANSLATE T
(ABBREVIATED-FOR-BODY X))))
F)
(IF (AND (LESSP 2 (LENGTH (CDR X)))
(OR (EQUAL (CAR X) 'AND)
(OR (EQUAL (CAR X) 'OR)
(OR (EQUAL (CAR X) 'PLUS)
(EQUAL (CAR X) 'TIMES)))))
(FN-NEST (CAR X)
(ALL-BUT-LAST (TRANSLATE F (CDR X)))
(CAR (LAST (TRANSLATE F (CDR X)))))
F))))))))))))))
(IF (NLISTP X)
NIL
(FCONS (TRANSLATE T (CAR X))
(TRANSLATE F (CDR X)))))
((LESSP (COUNT X))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSEQP,
CDR-LESSP, SUB1-ADD1, LISTP-CDDR-X-COUNT-X, COUNT-CONS, LISTP-CDDDR-X-COUNT-X,
CAR-CONS, CDR-CONS, LESSP-COUNT-STRIP-CADRS, LESSP-COUNT-STRIP-CARS,
LESSP-ABBREVIATED-FOR-BODY, LESSP-ABBREVIATED-FOR-WHEN,
LESSP-ABBREVIATED-FOR-RANGE, and CAR-LESSP, and the definitions of AND, CADRN,
CDRN, EQUAL, NLISTP, LESSP, COUNT, NOT, and OR can be used to establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, TRANSLATE is accepted under the principle of
definition.
[ 0.0 0.5 0.0 ]
TRANSLATE
(SET-STATUS POST-TRANSLATE T
((DEFN ENABLE) (OTHERWISE AS-IS)))
[ 0.0 0.0 0.0 ]
POST-TRANSLATE
(DEFN EXSYN
(STREAM)
(IF (READABLE (READ-TOKEN-TREE STREAM) 0)
(TRANSLATE T
(READMACRO-EXPANSION (READ-TOKEN-TREE STREAM)))
F))
[ 0.0 0.0 0.0 ]
EXSYN
(DEFN ADD1-NESTP
(X I)
(IF (NLISTP X)
F
(IF (AND (EQUAL (CAR X) 'ZERO)
(EQLEN X 1))
I
(IF (AND (EQUAL (CAR X) 'ADD1)
(EQLEN X 2))
(ADD1-NESTP (CADRN 1 X) (ADD1 I))
F))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, and CDR-LESSP,
and the definitions of CADRN, EQUAL, CDRN, AND, and NLISTP can be used to show
that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each recursive call. Hence, ADD1-NESTP is accepted under the
principle of definition. Note that:
(OR (OR (FALSEP (ADD1-NESTP X I))
(NUMBERP (ADD1-NESTP X I)))
(EQUAL (ADD1-NESTP X I) I))
is a theorem.
[ 0.0 0.0 0.0 ]
ADD1-NESTP
(DEFN CONS-ADD1-NESTP
(X)
(IF (NLISTP X)
F
(IF (AND (EQUAL (CAR X) 'ZERO)
(EQLEN X 1))
0
(IF (AND (EQUAL (CAR X) 'CONS)
(EQLEN X 3))
(FCONS (ADD1-NESTP (CADRN 1 X) 0)
(CONS-ADD1-NESTP (CADRN 2 X)))
F))))
Linear arithmetic, the lemmas CDRN-EXPANDER, CAR-LESSEQP, CDR-LESSEQP,
and CDR-LESSP, and the definitions of CADRN, EQUAL, CDRN, AND, and NLISTP
inform us that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each recursive call. Hence, CONS-ADD1-NESTP is accepted
under the principle of definition. From the definition we can conclude that:
(OR (FALSEP (CONS-ADD1-NESTP X))
(NUMBERP (CONS-ADD1-NESTP X))
(LISTP (CONS-ADD1-NESTP X)))
is a theorem.
[ 0.0 0.0 0.0 ]
CONS-ADD1-NESTP
(DEFN EXPLODED-LITATOM
(X)
(IF (AND (EQLEN X 2)
(AND (EQUAL (CAR X) 'PACK)
(CONS-ADD1-NESTP (CADRN 1 X))))
(LIST2 'QUOTE
(PACK (CONS-ADD1-NESTP (CADRN 1 X))))
F))
From the definition we can conclude that:
(OR (FALSEP (EXPLODED-LITATOM X))
(LISTP (EXPLODED-LITATOM X)))
is a theorem.
[ 0.0 0.0 0.0 ]
EXPLODED-LITATOM
(DEFN ABBREV
(FLG X)
(IF FLG
(IF (NLISTP X)
X
(IF (ADD1-NESTP X 0)
(ADD1-NESTP X 0)
(IF (EXPLODED-LITATOM X)
(EXPLODED-LITATOM X)
(CONS (CAR X) (ABBREV F (CDR X))))))
(IF (NLISTP X)
NIL
(CONS (ABBREV T (CAR X))
(ABBREV F (CDR X))))))
Linear arithmetic, the lemmas CDR-LESSEQP, CDRN-EXPANDER, CDR-LESSP,
CAR-LESSEQP, and CAR-LESSP, and the definitions of EXPLODED-LITATOM, CDRN,
EQUAL, CADRN, LIST1, LIST2, and NLISTP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, ABBREV is accepted under the principle of definition. From the
definition we can conclude that:
(OR (OR (NUMBERP (ABBREV FLG X))
(LITATOM (ABBREV FLG X))
(LISTP (ABBREV FLG X)))
(EQUAL (ABBREV FLG X) X))
is a theorem.
[ 0.0 0.1 0.0 ]
ABBREV
(DEFN AEXSYN
(STREAM)
(IF (READABLE (READ-TOKEN-TREE STREAM) 0)
(ABBREV T
(TRANSLATE T
(READMACRO-EXPANSION (READ-TOKEN-TREE STREAM))))
F))
[ 0.0 0.0 0.0 ]
AEXSYN
(MAKE-LIB "parser" T)
Making the lib for "parser".
Compiling the lib for "parser".
Loading ./basic/parser.o
Finished loading ./basic/parser.o
Finished compiling the lib for "parser".
Finished making the lib for "parser".
(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/parser.lib
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/parser.lisp)