(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