/usr/share/acl2-6.3/books/str/char-case.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((9 RECORD-EXPANSION (DEFSECTION STR::UP-ALPHA-P :PARENTS (STR::CASES UPPER-CASE-P) :SHORT "Determine if a character is an upper-case letter (A-Z)." :LONG "<p>@(call up-alpha-p) determines if @('x') is an upper-case alphabetic
character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::upper-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('up-alpha-p') works on arbitrary characters.</p>" (DEFINLINED STR::UP-ALPHA-P (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))))) (LOCAL (IN-THEORY (ENABLE STR::UP-ALPHA-P))) (DEFCONG STR::CHAREQV EQUAL (STR::UP-ALPHA-P X) 1) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (NOT (UPPER-CASE-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE UPPER-CASE-P))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z)))) :HINTS (("Goal" :CASES ((CHARACTERP X)))))) (DEFTHM STR::UPPER-CASE-P-IS-UP-ALPHA-P (EQUAL (UPPER-CASE-P X) (STR::UP-ALPHA-P (DOUBLE-REWRITE X)))) (IN-THEORY (DISABLE UPPER-CASE-P-CHAR-UPCASE))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UP-ALPHA-P)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::UP-ALPHA-P (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))))) (LOCAL (IN-THEORY (ENABLE STR::UP-ALPHA-P))) (DEFCONG STR::CHAREQV EQUAL (STR::UP-ALPHA-P X) 1) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (NOT (UPPER-CASE-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE UPPER-CASE-P))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (UPPER-CASE-P X) (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z)))) :HINTS (("Goal" :CASES ((CHARACTERP X)))))) (DEFTHM STR::UPPER-CASE-P-IS-UP-ALPHA-P (EQUAL (UPPER-CASE-P X) (STR::UP-ALPHA-P (DOUBLE-REWRITE X)))) (IN-THEORY (DISABLE UPPER-CASE-P-CHAR-UPCASE)))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UP-ALPHA-P)) (XDOC::PARENTS (QUOTE (STR::CASES UPPER-CASE-P))) (XDOC::SHORT (QUOTE "Determine if a character is an upper-case letter (A-Z).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UP-ALPHA-P))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call up-alpha-p) determines if @('x') is an upper-case alphabetic
character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::upper-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('up-alpha-p') works on arbitrary characters.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UP-ALPHA-P) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES UPPER-CASE-P) (:SHORT . "Determine if a character is an upper-case letter (A-Z).") (:LONG . "<p>@(call up-alpha-p) determines if @('x') is an upper-case alphabetic
character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::upper-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('up-alpha-p') works on arbitrary characters.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|UP-ALPHA-P$INLINE|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-UP-ALPHA-P-1|)
@(def |STR|::|UPPER-CASE-P-IS-UP-ALPHA-P|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UP-ALPHA-P)))))) (VALUE-TRIPLE (QUOTE STR::UP-ALPHA-P))))) (10 RECORD-EXPANSION (DEFSECTION STR::DOWN-ALPHA-P :PARENTS (STR::CASES LOWER-CASE-P) :SHORT "Determine if a character is a lower-case letter (a-z)." :LONG "<p>@(call down-alpha-p) determines if @('x') is an lower-case
alphabetic character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::lower-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('down-alpha-p') works on arbitrary characters.</p>" (DEFINLINED STR::DOWN-ALPHA-P (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))))) (LOCAL (IN-THEORY (ENABLE STR::DOWN-ALPHA-P))) (DEFCONG STR::CHAREQV EQUAL (STR::DOWN-ALPHA-P X) 1) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (NOT (LOWER-CASE-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE LOWER-CASE-P))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z)))) :HINTS (("Goal" :CASES ((CHARACTERP X)))))) (DEFTHM STR::LOWER-CASE-P-IS-DOWN-ALPHA-P (EQUAL (LOWER-CASE-P X) (STR::DOWN-ALPHA-P (DOUBLE-REWRITE X)))) (IN-THEORY (DISABLE LOWER-CASE-P-CHAR-DOWNCASE)) (DEFTHM STR::DOWN-ALPHA-P-WHEN-UP-ALPHA-P (IMPLIES (STR::UP-ALPHA-P X) (NOT (STR::DOWN-ALPHA-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UP-ALPHA-P STR::DOWN-ALPHA-P))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWN-ALPHA-P)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::DOWN-ALPHA-P (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))))) (LOCAL (IN-THEORY (ENABLE STR::DOWN-ALPHA-P))) (DEFCONG STR::CHAREQV EQUAL (STR::DOWN-ALPHA-P X) 1) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (NOT (LOWER-CASE-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE LOWER-CASE-P))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (LOWER-CASE-P X) (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z)))) :HINTS (("Goal" :CASES ((CHARACTERP X)))))) (DEFTHM STR::LOWER-CASE-P-IS-DOWN-ALPHA-P (EQUAL (LOWER-CASE-P X) (STR::DOWN-ALPHA-P (DOUBLE-REWRITE X)))) (IN-THEORY (DISABLE LOWER-CASE-P-CHAR-DOWNCASE)) (DEFTHM STR::DOWN-ALPHA-P-WHEN-UP-ALPHA-P (IMPLIES (STR::UP-ALPHA-P X) (NOT (STR::DOWN-ALPHA-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UP-ALPHA-P STR::DOWN-ALPHA-P)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWN-ALPHA-P)) (XDOC::PARENTS (QUOTE (STR::CASES LOWER-CASE-P))) (XDOC::SHORT (QUOTE "Determine if a character is a lower-case letter (a-z).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWN-ALPHA-P))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call down-alpha-p) determines if @('x') is an lower-case
alphabetic character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::lower-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('down-alpha-p') works on arbitrary characters.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWN-ALPHA-P) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES LOWER-CASE-P) (:SHORT . "Determine if a character is a lower-case letter (a-z).") (:LONG . "<p>@(call down-alpha-p) determines if @('x') is an lower-case
alphabetic character.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::lower-case-p),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('down-alpha-p') works on arbitrary characters.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|DOWN-ALPHA-P$INLINE|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-DOWN-ALPHA-P-1|)
@(def |STR|::|LOWER-CASE-P-IS-DOWN-ALPHA-P|)
@(def |STR|::|DOWN-ALPHA-P-WHEN-UP-ALPHA-P|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWN-ALPHA-P)))))) (VALUE-TRIPLE (QUOTE STR::DOWN-ALPHA-P))))) (11 RECORD-EXPANSION (DEFSECTION STR::UPCASE-CHAR :PARENTS (STR::CASES CHAR-UPCASE) :SHORT "Convert a character to upper-case." :LONG "<p>@(call upcase-char) converts lower-case characters into their
upper-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::char-upcase),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-char') works on arbitrary characters.</p>" (DEFINLINED STR::UPCASE-CHAR (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (- STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-CHAR))) (DEFCONG STR::CHAREQV EQUAL (STR::UPCASE-CHAR X) 1) (DEFTHM STR::UPCASE-CHAR-DOES-NOTHING-UNLESS-DOWN-ALPHA-P (IMPLIES (NOT (STR::DOWN-ALPHA-P X)) (EQUAL (STR::UPCASE-CHAR X) (STR::CHAR-FIX X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWN-ALPHA-P)))) (DEFTHM STR::UPCASE-CHAR-OF-UPCASE-CHAR (EQUAL (STR::UPCASE-CHAR (STR::UPCASE-CHAR X)) (STR::UPCASE-CHAR X))) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (EQUAL (CHAR-UPCASE X) (CODE-CHAR 0))) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR-UPCASE))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (CHAR-UPCASE X) (IF (CHARACTERP X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X) (CODE-CHAR 0))))) (DEFTHM STR::CHAR-UPCASE-IS-UPCASE-CHAR (EQUAL (CHAR-UPCASE X) (STR::UPCASE-CHAR (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHAR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::UPCASE-CHAR (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (- STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (LOCAL (IN-THEORY (ENABLE STR::UPCASE-CHAR))) (DEFCONG STR::CHAREQV EQUAL (STR::UPCASE-CHAR X) 1) (DEFTHM STR::UPCASE-CHAR-DOES-NOTHING-UNLESS-DOWN-ALPHA-P (IMPLIES (NOT (STR::DOWN-ALPHA-P X)) (EQUAL (STR::UPCASE-CHAR X) (STR::CHAR-FIX X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWN-ALPHA-P)))) (DEFTHM STR::UPCASE-CHAR-OF-UPCASE-CHAR (EQUAL (STR::UPCASE-CHAR (STR::UPCASE-CHAR X)) (STR::UPCASE-CHAR X))) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (CHAR-UPCASE X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (EQUAL (CHAR-UPCASE X) (CODE-CHAR 0))) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR-UPCASE))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (CHAR-UPCASE X) (IF (CHARACTERP X) (IF (AND (<= (STR::LITTLE-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::LITTLE-Z))) (CODE-CHAR (- (CHAR-CODE X) (STR::CASE-DELTA))) X) (CODE-CHAR 0))))) (DEFTHM STR::CHAR-UPCASE-IS-UPCASE-CHAR (EQUAL (CHAR-UPCASE X) (STR::UPCASE-CHAR (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-CHAR)) (XDOC::PARENTS (QUOTE (STR::CASES CHAR-UPCASE))) (XDOC::SHORT (QUOTE "Convert a character to upper-case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHAR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call upcase-char) converts lower-case characters into their
upper-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::char-upcase),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-char') works on arbitrary characters.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-CHAR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES CHAR-UPCASE) (:SHORT . "Convert a character to upper-case.") (:LONG . "<p>@(call upcase-char) converts lower-case characters into their
upper-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see acl2::char-upcase),
but it is irritating to use because it has @(see standard-char-p) guards.  In
contrast, @('upcase-char') works on arbitrary characters.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|UPCASE-CHAR$INLINE|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-UPCASE-CHAR-1|)
@(def |STR|::|UPCASE-CHAR-DOES-NOTHING-UNLESS-DOWN-ALPHA-P|)
@(def |STR|::|UPCASE-CHAR-OF-UPCASE-CHAR|)
@(def |STR|::|CHAR-UPCASE-IS-UPCASE-CHAR|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-CHAR)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-CHAR))))) (12 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-CHAR :PARENTS (STR::CASES CHAR-DOWNCASE) :SHORT "Convert a character to lower-case." :LONG "<p>@(call downcase-char) converts upper-case characters into their
lower-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::char-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-char') works on arbitrary
characters.</p>" (DEFINLINED STR::DOWNCASE-CHAR (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (+ STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-CHAR))) (DEFCONG STR::CHAREQV EQUAL (STR::DOWNCASE-CHAR X) 1) (DEFTHM STR::DOWNCASE-CHAR-DOES-NOTHING-UNLESS-UP-ALPHA-P (IMPLIES (NOT (STR::UP-ALPHA-P X)) (EQUAL (STR::DOWNCASE-CHAR X) (STR::CHAR-FIX X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UP-ALPHA-P)))) (DEFTHM STR::DOWNCASE-CHAR-OF-DOWNCASE-CHAR (EQUAL (STR::DOWNCASE-CHAR (STR::DOWNCASE-CHAR X)) (STR::DOWNCASE-CHAR X))) (DEFTHM STR::DOWNCASE-CHAR-OF-UPCASE-CHAR (EQUAL (STR::DOWNCASE-CHAR (STR::UPCASE-CHAR X)) (STR::DOWNCASE-CHAR X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::UPCASE-CHAR-OF-DOWNCASE-CHAR (EQUAL (STR::UPCASE-CHAR (STR::DOWNCASE-CHAR X)) (STR::UPCASE-CHAR X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHAR STR::CHAR-FIX)))) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (EQUAL (CHAR-DOWNCASE X) (CODE-CHAR 0))) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR-DOWNCASE))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (CHAR-DOWNCASE X) (IF (CHARACTERP X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X) (CODE-CHAR 0))))) (DEFTHM STR::CHAR-DOWNCASE-IS-DOWNCASE-CHAR (EQUAL (CHAR-DOWNCASE X) (STR::DOWNCASE-CHAR (DOUBLE-REWRITE X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHAR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::DOWNCASE-CHAR (X) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (+ STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (LOCAL (IN-THEORY (ENABLE STR::DOWNCASE-CHAR))) (DEFCONG STR::CHAREQV EQUAL (STR::DOWNCASE-CHAR X) 1) (DEFTHM STR::DOWNCASE-CHAR-DOES-NOTHING-UNLESS-UP-ALPHA-P (IMPLIES (NOT (STR::UP-ALPHA-P X)) (EQUAL (STR::DOWNCASE-CHAR X) (STR::CHAR-FIX X))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UP-ALPHA-P)))) (DEFTHM STR::DOWNCASE-CHAR-OF-DOWNCASE-CHAR (EQUAL (STR::DOWNCASE-CHAR (STR::DOWNCASE-CHAR X)) (STR::DOWNCASE-CHAR X))) (DEFTHM STR::DOWNCASE-CHAR-OF-UPCASE-CHAR (EQUAL (STR::DOWNCASE-CHAR (STR::UPCASE-CHAR X)) (STR::DOWNCASE-CHAR X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::UPCASE-CHAR-OF-DOWNCASE-CHAR (EQUAL (STR::UPCASE-CHAR (STR::DOWNCASE-CHAR X)) (STR::UPCASE-CHAR X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::UPCASE-CHAR STR::CHAR-FIX)))) (LOCAL (DEFUND STR::EXHAUSTIVE-TEST (N) (AND (LET ((X (CODE-CHAR N))) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) (OR (ZP N) (STR::EXHAUSTIVE-TEST (- N 1)))))) (LOCAL (DEFTHM STR::LEMMA1 (IMPLIES (AND (NATP N) (<= N 255)) (EQUAL (CHAR-CODE (CODE-CHAR N)) N)))) (LOCAL (DEFTHM STR::LEMMA2 (IMPLIES (AND (NATP N) (NATP M) (STR::EXHAUSTIVE-TEST N) (= X (CODE-CHAR M)) (<= M N) (<= N 255)) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :INDUCT (STR::EXHAUSTIVE-TEST N) :IN-THEORY (ENABLE STR::EXHAUSTIVE-TEST))))) (LOCAL (DEFTHM STR::LEMMA3 (IMPLIES (CHARACTERP X) (EQUAL (CHAR-DOWNCASE X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X))) :HINTS (("Goal" :IN-THEORY (DISABLE STR::LEMMA2) :USE ((:INSTANCE STR::LEMMA2 (N 255) (M (CHAR-CODE X)))))))) (LOCAL (DEFTHM STR::LEMMA4 (IMPLIES (NOT (CHARACTERP X)) (EQUAL (CHAR-DOWNCASE X) (CODE-CHAR 0))) :HINTS (("Goal" :IN-THEORY (ENABLE CHAR-DOWNCASE))))) (LOCAL (DEFTHM STR::LEMMA5 (EQUAL (CHAR-DOWNCASE X) (IF (CHARACTERP X) (IF (AND (<= (STR::BIG-A) (CHAR-CODE X)) (<= (CHAR-CODE X) (STR::BIG-Z))) (CODE-CHAR (+ (CHAR-CODE X) (STR::CASE-DELTA))) X) (CODE-CHAR 0))))) (DEFTHM STR::CHAR-DOWNCASE-IS-DOWNCASE-CHAR (EQUAL (CHAR-DOWNCASE X) (STR::DOWNCASE-CHAR (DOUBLE-REWRITE X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-CHAR)) (XDOC::PARENTS (QUOTE (STR::CASES CHAR-DOWNCASE))) (XDOC::SHORT (QUOTE "Convert a character to lower-case.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHAR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call downcase-char) converts upper-case characters into their
lower-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::char-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-char') works on arbitrary
characters.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-CHAR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES CHAR-DOWNCASE) (:SHORT . "Convert a character to lower-case.") (:LONG . "<p>@(call downcase-char) converts upper-case characters into their
lower-case equivalents, and returns other characters unchanged.</p>

<p>ACL2 has a built-in alternative to this function, @(see
acl2::char-downcase), but it is irritating to use because it has @(see
standard-char-p) guards.  In contrast, @('downcase-char') works on arbitrary
characters.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|DOWNCASE-CHAR$INLINE|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-DOWNCASE-CHAR-1|)
@(def |STR|::|DOWNCASE-CHAR-DOES-NOTHING-UNLESS-UP-ALPHA-P|)
@(def |STR|::|DOWNCASE-CHAR-OF-DOWNCASE-CHAR|)
@(def |STR|::|DOWNCASE-CHAR-OF-UPCASE-CHAR|)
@(def |STR|::|UPCASE-CHAR-OF-DOWNCASE-CHAR|)
@(def |STR|::|CHAR-DOWNCASE-IS-DOWNCASE-CHAR|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-CHAR)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-CHAR))))) (13 RECORD-EXPANSION (DEFSECTION STR::UPCASE-CHAR-STR :PARENTS (STR::CASES) :SHORT "Convert a character into an upper-case one-element string." :LONG "<p>@(call upcase-char-str) is logically equal to:</p>

@({
 (implode (list (upcase-char c)))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see upcase-first).</p>" (DEFUN STR::MAKE-UPCASE-FIRST-STRTBL (N) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-UPCASE-FIRST-STRTBL (- N 1))))) (DEFCONST STR::*UPCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-UPCASE-FIRST-STRTBL 255)))) (LOCAL (IN-THEORY (DISABLE AREF1))) (LOCAL (DEFUN STR::TEST (N) (DECLARE (XARGS :RULER-EXTENDERS :ALL)) (AND (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* N) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) T (STR::TEST (- N 1)))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (NATP I) (NATP N) (<= I N) (<= N 255) (STR::TEST N)) (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :INDUCT (STR::TEST N))))) (LOCAL (DEFTHM STR::L1 (IMPLIES (AND (NATP I) (<= I 255)) (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (N 255))))))) (DEFINLINE STR::UPCASE-CHAR-STR (C) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::UPCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* (CHAR-CODE C))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHAR-STR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN STR::MAKE-UPCASE-FIRST-STRTBL (N) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-UPCASE-FIRST-STRTBL (- N 1))))) (DEFCONST STR::*UPCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-UPCASE-FIRST-STRTBL 255)))) (LOCAL (IN-THEORY (DISABLE AREF1))) (LOCAL (DEFUN STR::TEST (N) (DECLARE (XARGS :RULER-EXTENDERS :ALL)) (AND (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* N) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) T (STR::TEST (- N 1)))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (NATP I) (NATP N) (<= I N) (<= N 255) (STR::TEST N)) (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :INDUCT (STR::TEST N))))) (LOCAL (DEFTHM STR::L1 (IMPLIES (AND (NATP I) (<= I 255)) (EQUAL (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (N 255))))))) (DEFINLINE STR::UPCASE-CHAR-STR (C) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::UPCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* (CHAR-CODE C)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::UPCASE-CHAR-STR)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert a character into an upper-case one-element string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::UPCASE-CHAR-STR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call upcase-char-str) is logically equal to:</p>

@({
 (implode (list (upcase-char c)))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see upcase-first).</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::UPCASE-CHAR-STR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert a character into an upper-case one-element string.") (:LONG . "<p>@(call upcase-char-str) is logically equal to:</p>

@({
 (implode (list (upcase-char c)))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see upcase-first).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|MAKE-UPCASE-FIRST-STRTBL|)
@(def |STR|::|UPCASE-CHAR-STR$INLINE|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::UPCASE-CHAR-STR)))))) (VALUE-TRIPLE (QUOTE STR::UPCASE-CHAR-STR))))) (14 RECORD-EXPANSION (DEFSECTION STR::DOWNCASE-CHAR-STR :PARENTS (STR::CASES) :SHORT "Convert a character into a lower-case one-element string." :LONG "<p>@(call downcase-char-str) is logically equal to:</p>

@({
 (implode (downcase-char c))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see downcase-first).</p>" (DEFUN STR::MAKE-DOWNCASE-FIRST-STRTBL (N) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-DOWNCASE-FIRST-STRTBL (- N 1))))) (DEFCONST STR::*DOWNCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-DOWNCASE-FIRST-STRTBL 255)))) (LOCAL (IN-THEORY (DISABLE AREF1))) (LOCAL (DEFUN STR::TEST (N) (DECLARE (XARGS :RULER-EXTENDERS :ALL)) (AND (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* N) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) T (STR::TEST (- N 1)))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (NATP I) (NATP N) (<= I N) (<= N 255) (STR::TEST N)) (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :INDUCT (STR::TEST N))))) (LOCAL (DEFTHM STR::L1 (IMPLIES (AND (NATP I) (<= I 255)) (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (N 255))))))) (DEFINLINE STR::DOWNCASE-CHAR-STR (C) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::DOWNCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* (CHAR-CODE C))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHAR-STR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN STR::MAKE-DOWNCASE-FIRST-STRTBL (N) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-DOWNCASE-FIRST-STRTBL (- N 1))))) (DEFCONST STR::*DOWNCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-DOWNCASE-FIRST-STRTBL 255)))) (LOCAL (IN-THEORY (DISABLE AREF1))) (LOCAL (DEFUN STR::TEST (N) (DECLARE (XARGS :RULER-EXTENDERS :ALL)) (AND (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* N) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) T (STR::TEST (- N 1)))))) (LOCAL (DEFTHM STR::L0 (IMPLIES (AND (NATP I) (NATP N) (<= I N) (<= N 255) (STR::TEST N)) (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :INDUCT (STR::TEST N))))) (LOCAL (DEFTHM STR::L1 (IMPLIES (AND (NATP I) (<= I 255)) (EQUAL (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* I) (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR I)))))) :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (N 255))))))) (DEFINLINE STR::DOWNCASE-CHAR-STR (C) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::DOWNCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* (CHAR-CODE C)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DOWNCASE-CHAR-STR)) (XDOC::PARENTS (QUOTE (STR::CASES))) (XDOC::SHORT (QUOTE "Convert a character into a lower-case one-element string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::DOWNCASE-CHAR-STR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call downcase-char-str) is logically equal to:</p>

@({
 (implode (downcase-char c))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see downcase-first).</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::DOWNCASE-CHAR-STR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::CASES) (:SHORT . "Convert a character into a lower-case one-element string.") (:LONG . "<p>@(call downcase-char-str) is logically equal to:</p>

@({
 (implode (downcase-char c))
})

<p>But we store these strings in a table so that they don't have to be
recomputed.  This is mainly useful to reduce the creation of temporary strings
during @(see downcase-first).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|MAKE-DOWNCASE-FIRST-STRTBL|)
@(def |STR|::|DOWNCASE-CHAR-STR$INLINE|)") (:FROM . "[books]/str/char-case.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DOWNCASE-CHAR-STR)))))) (VALUE-TRIPLE (QUOTE STR::DOWNCASE-CHAR-STR))))))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1418171271
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / char-case.cert
