acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / strval.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (DEFSECTION STR::OCTAL-DIGITP :PARENTS (STR::NUMBERS) :SHORT "Recognizer for characters #\\0 through #\\7." :LONG "<p>@(call octal-digitp) is the octal alternative to @(see digitp).</p>" (DEFINLINED STR::OCTAL-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\7))))) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::OCTAL-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::OCTAL-DIGITP STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::DIGITP-WHEN-OCTAL-DIGITP (IMPLIES (STR::OCTAL-DIGITP X) (STR::DIGITP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGITP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::OCTAL-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\7))))) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::OCTAL-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::OCTAL-DIGITP STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::DIGITP-WHEN-OCTAL-DIGITP (IMPLIES (STR::OCTAL-DIGITP X) (STR::DIGITP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::OCTAL-DIGITP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizer for characters #\\0 through #\\7.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGITP))) 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 octal-digitp) is the octal alternative to @(see digitp).</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::OCTAL-DIGITP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizer for characters #\\0 through #\\7.") (:LONG . "<p>@(call octal-digitp) is the octal alternative to @(see digitp).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|OCTAL-DIGITP$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-OCTAL-DIGITP-1|)
@(def |STR|::|DIGITP-WHEN-OCTAL-DIGITP|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::OCTAL-DIGITP)))))) (VALUE-TRIPLE (QUOTE STR::OCTAL-DIGITP))))) (5 RECORD-EXPANSION (DEFSECTION STR::OCTAL-DIGIT-LISTP :PARENTS (STR::NUMBERS) :SHORT "Recognizes lists of @(see octal-digitp) characters." (DEFUND STR::OCTAL-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::OCTAL-DIGITP (CAR X)) (STR::OCTAL-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGIT-LISTP))) (DEFTHM STR::DIGIT-LISTP-WHEN-OCTAL-DIGIT-LISTP (IMPLIES (STR::OCTAL-DIGIT-LISTP X) (STR::DIGIT-LISTP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-LISTP)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::OCTAL-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGIT-LISTP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::OCTAL-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::OCTAL-DIGITP (CAR X)) (STR::OCTAL-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGIT-LISTP))) (DEFTHM STR::DIGIT-LISTP-WHEN-OCTAL-DIGIT-LISTP (IMPLIES (STR::OCTAL-DIGIT-LISTP X) (STR::DIGIT-LISTP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-LISTP)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::OCTAL-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::OCTAL-DIGIT-LISTP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizes lists of @(see octal-digitp) characters.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGIT-LISTP))) 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 "") (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::OCTAL-DIGIT-LISTP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizes lists of @(see octal-digitp) characters.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|OCTAL-DIGIT-LISTP|)
@(def |STR|::|DIGIT-LISTP-WHEN-OCTAL-DIGIT-LISTP|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-OCTAL-DIGIT-LISTP-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::OCTAL-DIGIT-LISTP)))))) (VALUE-TRIPLE (QUOTE STR::OCTAL-DIGIT-LISTP))))) (6 RECORD-EXPANSION (DEFSECTION STR::PARSE-OCTAL-FROM-CHARLIST :PARENTS (STR::NUMBERS) :SHORT "Parse an octal number from the beginning of a character list." :LONG "<p>This is like @(call parse-nat-from-charlist), but deals with octal
digits and returns their octal value.</p>" (DEFUND STR::PARSE-OCTAL-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::OCTAL-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-OCTAL-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 8 (LNFIX STR::VAL))) (+ 1 (LNFIX LEN))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-OCTAL-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-OCTAL-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-OCTAL-FROM-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::PARSE-OCTAL-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::OCTAL-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-OCTAL-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 8 (LNFIX STR::VAL))) (+ 1 (LNFIX LEN))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-OCTAL-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-OCTAL-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PARSE-OCTAL-FROM-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Parse an octal number from the beginning of a character list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-OCTAL-FROM-CHARLIST))) 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>This is like @(call parse-nat-from-charlist), but deals with octal
digits and returns their octal value.</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::PARSE-OCTAL-FROM-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Parse an octal number from the beginning of a character list.") (:LONG . "<p>This is like @(call parse-nat-from-charlist), but deals with octal
digits and returns their octal value.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PARSE-OCTAL-FROM-CHARLIST|)
@(def |STR|::|NATP-OF-PARSE-OCTAL-FROM-CHARLIST|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PARSE-OCTAL-FROM-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::PARSE-OCTAL-FROM-CHARLIST))))) (7 RECORD-EXPANSION (DEFSECTION STR::OCTAL-DIGIT-LIST-VALUE :PARENTS (STR::NUMBERS) :SHORT "Coerces a list of octal digits into a natural number." :LONG "<p>@(call octal-digit-list-value) is like @(see digit-list-value) but
for octal numbers.</p>

<p>See also @(see parse-octal-from-charlist) for a more flexible function that
can tolerate non-octal digits after the number.</p>" (DEFINLINED STR::OCTAL-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::OCTAL-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-OCTAL-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-OCTAL-DIGIT-LIST-VALUE (NATP (STR::OCTAL-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-OCTAL-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::OCTAL-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 10) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 668))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGIT-LIST-VALUE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::OCTAL-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::OCTAL-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-OCTAL-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-OCTAL-DIGIT-LIST-VALUE (NATP (STR::OCTAL-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-OCTAL-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::OCTAL-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 10) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 668)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::OCTAL-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::OCTAL-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-OCTAL-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::OCTAL-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-OCTAL-DIGIT-LIST-VALUE (NATP (STR::OCTAL-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-OCTAL-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-OCTAL-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::OCTAL-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (RECORD-EXPANSION (LOCAL (ASSERT! (AND (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 10) (EQUAL (STR::OCTAL-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 668)))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::OCTAL-DIGIT-LIST-VALUE)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a list of octal digits into a natural number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::OCTAL-DIGIT-LIST-VALUE))) 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 octal-digit-list-value) is like @(see digit-list-value) but
for octal numbers.</p>

<p>See also @(see parse-octal-from-charlist) for a more flexible function that
can tolerate non-octal digits after the number.</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::OCTAL-DIGIT-LIST-VALUE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a list of octal digits into a natural number.") (:LONG . "<p>@(call octal-digit-list-value) is like @(see digit-list-value) but
for octal numbers.</p>

<p>See also @(see parse-octal-from-charlist) for a more flexible function that
can tolerate non-octal digits after the number.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|OCTAL-DIGIT-LIST-VALUE$INLINE|)
@(def |STR|::|NATP-OF-OCTAL-DIGIT-LIST-VALUE|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-OCTAL-DIGIT-LIST-VALUE-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::OCTAL-DIGIT-LIST-VALUE)))))) (VALUE-TRIPLE (QUOTE STR::OCTAL-DIGIT-LIST-VALUE))))) (8 RECORD-EXPANSION (DEFSECTION STR::HEX-DIGITP :PARENTS (STR::NUMBERS) :SHORT "Recognizer for characters 0-9, A-F, and a-f." :LONG "<p>@(call hex-digitp) is the hexadecimal alternative to @(see digitp).</p>" (DEFINLINED STR::HEX-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (OR (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9))) (AND (<= (CHAR-CODE #\a) STR::CODE) (<= STR::CODE (CHAR-CODE #\f))) (AND (<= (CHAR-CODE #\A) STR::CODE) (<= STR::CODE (CHAR-CODE #\F)))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::HEX-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::HEX-DIGITP STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGITP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::HEX-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (OR (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9))) (AND (<= (CHAR-CODE #\a) STR::CODE) (<= STR::CODE (CHAR-CODE #\f))) (AND (<= (CHAR-CODE #\A) STR::CODE) (<= STR::CODE (CHAR-CODE #\F)))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::HEX-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::HEX-DIGITP STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HEX-DIGITP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizer for characters 0-9, A-F, and a-f.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGITP))) 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 hex-digitp) is the hexadecimal alternative to @(see digitp).</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::HEX-DIGITP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizer for characters 0-9, A-F, and a-f.") (:LONG . "<p>@(call hex-digitp) is the hexadecimal alternative to @(see digitp).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|HEX-DIGITP$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-HEX-DIGITP-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HEX-DIGITP)))))) (VALUE-TRIPLE (QUOTE STR::HEX-DIGITP))))) (9 RECORD-EXPANSION (DEFSECTION STR::HEX-DIGIT-LISTP :PARENTS (STR::NUMBERS) :SHORT "Recognizes lists of @(see hex-digitp) characters." (DEFUND STR::HEX-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::HEX-DIGITP (CAR X)) (STR::HEX-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-LISTP))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::HEX-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-LISTP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::HEX-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::HEX-DIGITP (CAR X)) (STR::HEX-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-LISTP))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::HEX-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HEX-DIGIT-LISTP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizes lists of @(see hex-digitp) characters.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-LISTP))) 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 "") (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::HEX-DIGIT-LISTP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizes lists of @(see hex-digitp) characters.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|HEX-DIGIT-LISTP|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-HEX-DIGIT-LISTP-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HEX-DIGIT-LISTP)))))) (VALUE-TRIPLE (QUOTE STR::HEX-DIGIT-LISTP))))) (10 RECORD-EXPANSION (DEFSECTION STR::HEX-DIGIT-VAL :PARENTS (STR::NUMBERS) :SHORT "Coerces a @(see hex-digitp) character into an integer." :LONG "<p>@(call hex-digit-val) is the hexadecimal version of @(see
digit-val).</p>" (DEFINLINED STR::HEX-DIGIT-VAL (X) (DECLARE (XARGS :GUARD (AND (CHARACTERP X) (STR::HEX-DIGITP X)))) (IF (MBE :LOGIC (NOT (STR::HEX-DIGITP X)) :EXEC NIL) 0 (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (COND ((<= (CHAR-CODE #\a) STR::CODE) (- STR::CODE (- (CHAR-CODE #\a) 10))) ((<= (CHAR-CODE #\A) STR::CODE) (- STR::CODE (- (CHAR-CODE #\A) 10))) (T (- STR::CODE (CHAR-CODE #\0))))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-VAL STR::HEX-DIGITP))) (DEFTHM STR::NATP-OF-HEX-DIGIT-VAL (NATP (STR::HEX-DIGIT-VAL X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ICHAREQV EQUAL (STR::HEX-DIGIT-VAL X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-VAL #\A) 10) (EQUAL (STR::HEX-DIGIT-VAL #\B) 11) (EQUAL (STR::HEX-DIGIT-VAL #\C) 12) (EQUAL (STR::HEX-DIGIT-VAL #\D) 13) (EQUAL (STR::HEX-DIGIT-VAL #\E) 14) (EQUAL (STR::HEX-DIGIT-VAL #\F) 15) (EQUAL (STR::HEX-DIGIT-VAL #\a) 10) (EQUAL (STR::HEX-DIGIT-VAL #\b) 11) (EQUAL (STR::HEX-DIGIT-VAL #\c) 12) (EQUAL (STR::HEX-DIGIT-VAL #\d) 13) (EQUAL (STR::HEX-DIGIT-VAL #\e) 14) (EQUAL (STR::HEX-DIGIT-VAL #\f) 15) (EQUAL (STR::HEX-DIGIT-VAL #\0) 0) (EQUAL (STR::HEX-DIGIT-VAL #\1) 1) (EQUAL (STR::HEX-DIGIT-VAL #\2) 2) (EQUAL (STR::HEX-DIGIT-VAL #\3) 3) (EQUAL (STR::HEX-DIGIT-VAL #\4) 4) (EQUAL (STR::HEX-DIGIT-VAL #\5) 5) (EQUAL (STR::HEX-DIGIT-VAL #\6) 6) (EQUAL (STR::HEX-DIGIT-VAL #\7) 7) (EQUAL (STR::HEX-DIGIT-VAL #\8) 8) (EQUAL (STR::HEX-DIGIT-VAL #\9) 9))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-VAL)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::HEX-DIGIT-VAL (X) (DECLARE (XARGS :GUARD (AND (CHARACTERP X) (STR::HEX-DIGITP X)))) (IF (MBE :LOGIC (NOT (STR::HEX-DIGITP X)) :EXEC NIL) 0 (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (COND ((<= (CHAR-CODE #\a) STR::CODE) (- STR::CODE (- (CHAR-CODE #\a) 10))) ((<= (CHAR-CODE #\A) STR::CODE) (- STR::CODE (- (CHAR-CODE #\A) 10))) (T (- STR::CODE (CHAR-CODE #\0))))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-VAL STR::HEX-DIGITP))) (DEFTHM STR::NATP-OF-HEX-DIGIT-VAL (NATP (STR::HEX-DIGIT-VAL X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ICHAREQV EQUAL (STR::HEX-DIGIT-VAL X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-VAL #\A) 10) (EQUAL (STR::HEX-DIGIT-VAL #\B) 11) (EQUAL (STR::HEX-DIGIT-VAL #\C) 12) (EQUAL (STR::HEX-DIGIT-VAL #\D) 13) (EQUAL (STR::HEX-DIGIT-VAL #\E) 14) (EQUAL (STR::HEX-DIGIT-VAL #\F) 15) (EQUAL (STR::HEX-DIGIT-VAL #\a) 10) (EQUAL (STR::HEX-DIGIT-VAL #\b) 11) (EQUAL (STR::HEX-DIGIT-VAL #\c) 12) (EQUAL (STR::HEX-DIGIT-VAL #\d) 13) (EQUAL (STR::HEX-DIGIT-VAL #\e) 14) (EQUAL (STR::HEX-DIGIT-VAL #\f) 15) (EQUAL (STR::HEX-DIGIT-VAL #\0) 0) (EQUAL (STR::HEX-DIGIT-VAL #\1) 1) (EQUAL (STR::HEX-DIGIT-VAL #\2) 2) (EQUAL (STR::HEX-DIGIT-VAL #\3) 3) (EQUAL (STR::HEX-DIGIT-VAL #\4) 4) (EQUAL (STR::HEX-DIGIT-VAL #\5) 5) (EQUAL (STR::HEX-DIGIT-VAL #\6) 6) (EQUAL (STR::HEX-DIGIT-VAL #\7) 7) (EQUAL (STR::HEX-DIGIT-VAL #\8) 8) (EQUAL (STR::HEX-DIGIT-VAL #\9) 9)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::HEX-DIGIT-VAL (X) (DECLARE (XARGS :GUARD (AND (CHARACTERP X) (STR::HEX-DIGITP X)))) (IF (MBE :LOGIC (NOT (STR::HEX-DIGITP X)) :EXEC NIL) 0 (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (COND ((<= (CHAR-CODE #\a) STR::CODE) (- STR::CODE (- (CHAR-CODE #\a) 10))) ((<= (CHAR-CODE #\A) STR::CODE) (- STR::CODE (- (CHAR-CODE #\A) 10))) (T (- STR::CODE (CHAR-CODE #\0))))))) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-VAL STR::HEX-DIGITP))) (DEFTHM STR::NATP-OF-HEX-DIGIT-VAL (NATP (STR::HEX-DIGIT-VAL X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ICHAREQV EQUAL (STR::HEX-DIGIT-VAL X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (RECORD-EXPANSION (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-VAL #\A) 10) (EQUAL (STR::HEX-DIGIT-VAL #\B) 11) (EQUAL (STR::HEX-DIGIT-VAL #\C) 12) (EQUAL (STR::HEX-DIGIT-VAL #\D) 13) (EQUAL (STR::HEX-DIGIT-VAL #\E) 14) (EQUAL (STR::HEX-DIGIT-VAL #\F) 15) (EQUAL (STR::HEX-DIGIT-VAL #\a) 10) (EQUAL (STR::HEX-DIGIT-VAL #\b) 11) (EQUAL (STR::HEX-DIGIT-VAL #\c) 12) (EQUAL (STR::HEX-DIGIT-VAL #\d) 13) (EQUAL (STR::HEX-DIGIT-VAL #\e) 14) (EQUAL (STR::HEX-DIGIT-VAL #\f) 15) (EQUAL (STR::HEX-DIGIT-VAL #\0) 0) (EQUAL (STR::HEX-DIGIT-VAL #\1) 1) (EQUAL (STR::HEX-DIGIT-VAL #\2) 2) (EQUAL (STR::HEX-DIGIT-VAL #\3) 3) (EQUAL (STR::HEX-DIGIT-VAL #\4) 4) (EQUAL (STR::HEX-DIGIT-VAL #\5) 5) (EQUAL (STR::HEX-DIGIT-VAL #\6) 6) (EQUAL (STR::HEX-DIGIT-VAL #\7) 7) (EQUAL (STR::HEX-DIGIT-VAL #\8) 8) (EQUAL (STR::HEX-DIGIT-VAL #\9) 9)))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HEX-DIGIT-VAL)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a @(see hex-digitp) character into an integer.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-VAL))) 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 hex-digit-val) is the hexadecimal version of @(see
digit-val).</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::HEX-DIGIT-VAL) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a @(see hex-digitp) character into an integer.") (:LONG . "<p>@(call hex-digit-val) is the hexadecimal version of @(see
digit-val).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|HEX-DIGIT-VAL$INLINE|)
@(def |STR|::|NATP-OF-HEX-DIGIT-VAL|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-HEX-DIGIT-VAL-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HEX-DIGIT-VAL)))))) (VALUE-TRIPLE (QUOTE STR::HEX-DIGIT-VAL))))) (11 RECORD-EXPANSION (DEFSECTION STR::PARSE-HEX-FROM-CHARLIST :PARENTS (STR::NUMBERS) :SHORT "Parse a hexadecimal number from the beginning of a character list." :LONG "<p>This is like @(call parse-nat-from-charlist), but deals with
hex digits and returns their hexadecimal value.</p>" (DEFUND STR::PARSE-HEX-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::HEX-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::HEX-DIGIT-VAL (CAR X)))) (STR::PARSE-HEX-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ (THE (INTEGER 0 *) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 16 (THE (INTEGER 0 *) (LNFIX STR::VAL)))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN))))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-HEX-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-HEX-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-HEX-FROM-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::PARSE-HEX-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::HEX-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::HEX-DIGIT-VAL (CAR X)))) (STR::PARSE-HEX-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ (THE (INTEGER 0 *) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 16 (THE (INTEGER 0 *) (LNFIX STR::VAL)))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN))))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-HEX-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-HEX-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PARSE-HEX-FROM-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Parse a hexadecimal number from the beginning of a character list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-HEX-FROM-CHARLIST))) 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>This is like @(call parse-nat-from-charlist), but deals with
hex digits and returns their hexadecimal value.</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::PARSE-HEX-FROM-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Parse a hexadecimal number from the beginning of a character list.") (:LONG . "<p>This is like @(call parse-nat-from-charlist), but deals with
hex digits and returns their hexadecimal value.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PARSE-HEX-FROM-CHARLIST|)
@(def |STR|::|NATP-OF-PARSE-HEX-FROM-CHARLIST|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PARSE-HEX-FROM-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::PARSE-HEX-FROM-CHARLIST))))) (12 RECORD-EXPANSION (DEFSECTION STR::HEX-DIGIT-LIST-VALUE :PARENTS (STR::NUMBERS) :SHORT "Coerces a list of hex digits into a natural number." :LONG "<p>@(call hex-digit-list-value) is like @(see digit-list-value) but
for hex numbers.</p>

<p>See also @(see parse-hex-from-charlist) for a more flexible function that
can tolerate non-hex digits after the number.</p>" (DEFINLINED STR::HEX-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::HEX-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-HEX-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-HEX-DIGIT-LIST-VALUE (NATP (STR::HEX-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-HEX-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::HEX-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 18) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 4660))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-LIST-VALUE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::HEX-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::HEX-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-HEX-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-HEX-DIGIT-LIST-VALUE (NATP (STR::HEX-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-HEX-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::HEX-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 18) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 4660)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::HEX-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::HEX-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-HEX-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::HEX-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-HEX-DIGIT-LIST-VALUE (NATP (STR::HEX-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-HEX-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-HEX-FROM-CHARLIST STR::ICHARLISTEQV))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::HEX-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (RECORD-EXPANSION (LOCAL (ASSERT! (AND (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "6" (QUOTE LIST))) 6) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "12" (QUOTE LIST))) 18) (EQUAL (STR::HEX-DIGIT-LIST-VALUE (COERCE "1234" (QUOTE LIST))) 4660)))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HEX-DIGIT-LIST-VALUE)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a list of hex digits into a natural number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HEX-DIGIT-LIST-VALUE))) 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 hex-digit-list-value) is like @(see digit-list-value) but
for hex numbers.</p>

<p>See also @(see parse-hex-from-charlist) for a more flexible function that
can tolerate non-hex digits after the number.</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::HEX-DIGIT-LIST-VALUE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a list of hex digits into a natural number.") (:LONG . "<p>@(call hex-digit-list-value) is like @(see digit-list-value) but
for hex numbers.</p>

<p>See also @(see parse-hex-from-charlist) for a more flexible function that
can tolerate non-hex digits after the number.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|HEX-DIGIT-LIST-VALUE$INLINE|)
@(def |STR|::|NATP-OF-HEX-DIGIT-LIST-VALUE|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-HEX-DIGIT-LIST-VALUE-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HEX-DIGIT-LIST-VALUE)))))) (VALUE-TRIPLE (QUOTE STR::HEX-DIGIT-LIST-VALUE))))) (13 RECORD-EXPANSION (DEFSECTION STR::BIT-DIGITP :PARENTS (STR::NUMBERS) :SHORT "Recognizer for characters #\\0 and #\\1." :LONG "<p>@(call bit-digitp) is the binary alternative to @(see digitp).</p>" (DEFINLINED STR::BIT-DIGITP (X) (DECLARE (XARGS :GUARD T)) (OR (EQL X #\0) (EQL X #\1))) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::BIT-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGITP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::BIT-DIGITP (X) (DECLARE (XARGS :GUARD T)) (OR (EQL X #\0) (EQL X #\1))) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::BIT-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::BIT-DIGITP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizer for characters #\\0 and #\\1.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGITP))) 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 bit-digitp) is the binary alternative to @(see digitp).</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::BIT-DIGITP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizer for characters #\\0 and #\\1.") (:LONG . "<p>@(call bit-digitp) is the binary alternative to @(see digitp).</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|BIT-DIGITP$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-BIT-DIGITP-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::BIT-DIGITP)))))) (VALUE-TRIPLE (QUOTE STR::BIT-DIGITP))))) (14 RECORD-EXPANSION (DEFSECTION STR::BIT-DIGIT-LISTP :PARENTS (STR::NUMBERS) :SHORT "Recognizes lists of @(see bit-digitp) characters." (DEFUND STR::BIT-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD T)) (IF (ATOM X) T (AND (STR::BIT-DIGITP (CAR X)) (STR::BIT-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGIT-LISTP))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::BIT-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGIT-LISTP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::BIT-DIGIT-LISTP (X) (DECLARE (XARGS :GUARD T)) (IF (ATOM X) T (AND (STR::BIT-DIGITP (CAR X)) (STR::BIT-DIGIT-LISTP (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGIT-LISTP))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::BIT-DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::BIT-DIGIT-LISTP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizes lists of @(see bit-digitp) characters.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGIT-LISTP))) 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 "") (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::BIT-DIGIT-LISTP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizes lists of @(see bit-digitp) characters.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|BIT-DIGIT-LISTP|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-BIT-DIGIT-LISTP-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::BIT-DIGIT-LISTP)))))) (VALUE-TRIPLE (QUOTE STR::BIT-DIGIT-LISTP))))) (15 RECORD-EXPANSION (DEFSECTION STR::BITSTRING-P :PARENTS (STR::NUMBERS) :SHORT "Recognizes strings with only @(see bit-digitp) characters." (DEFUND STR::BITSTRING-P (X) (DECLARE (XARGS :GUARD T)) (AND (STRINGP X) (STR::BIT-DIGIT-LISTP (EXPLODE X)))) (LOCAL (IN-THEORY (ENABLE STR::BITSTRING-P)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::BITSTRING-P)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::BITSTRING-P (X) (DECLARE (XARGS :GUARD T)) (AND (STRINGP X) (STR::BIT-DIGIT-LISTP (EXPLODE X)))) (LOCAL (IN-THEORY (ENABLE STR::BITSTRING-P))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::BITSTRING-P)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizes strings with only @(see bit-digitp) characters.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::BITSTRING-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 "") (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::BITSTRING-P) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizes strings with only @(see bit-digitp) characters.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|BITSTRING-P|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::BITSTRING-P)))))) (VALUE-TRIPLE (QUOTE STR::BITSTRING-P))))) (16 RECORD-EXPANSION (DEFSECTION STR::PARSE-BITS-FROM-CHARLIST :PARENTS (STR::NUMBERS) :SHORT "Parse a binary number from the beginning of a character list." :LONG "<p>This is like @(call parse-nat-from-charlist), but deals with binary
digits (#\\0 and #\\1) and returns their binary value.</p>" (DEFUND STR::PARSE-BITS-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((EQL (CAR X) #\0) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) ((EQL (CAR X) #\1) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ 1 (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-BITS-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-BITS-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-BITS-FROM-CHARLIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::PARSE-BITS-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((EQL (CAR X) #\0) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) ((EQL (CAR X) #\1) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ 1 (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (LOCAL (IN-THEORY (ENABLE STR::PARSE-BITS-FROM-CHARLIST))) (DEFTHM STR::NATP-OF-PARSE-BITS-FROM-CHARLIST (IMPLIES (NATP STR::VAL) (NATP (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST X STR::VAL LEN)))) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PARSE-BITS-FROM-CHARLIST)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Parse a binary number from the beginning of a character list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PARSE-BITS-FROM-CHARLIST))) 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>This is like @(call parse-nat-from-charlist), but deals with binary
digits (#\\0 and #\\1) and returns their binary value.</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::PARSE-BITS-FROM-CHARLIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Parse a binary number from the beginning of a character list.") (:LONG . "<p>This is like @(call parse-nat-from-charlist), but deals with binary
digits (#\\0 and #\\1) and returns their binary value.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|PARSE-BITS-FROM-CHARLIST|)
@(def |STR|::|NATP-OF-PARSE-BITS-FROM-CHARLIST|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PARSE-BITS-FROM-CHARLIST)))))) (VALUE-TRIPLE (QUOTE STR::PARSE-BITS-FROM-CHARLIST))))) (17 RECORD-EXPANSION (DEFSECTION STR::BIT-DIGIT-LIST-VALUE :PARENTS (STR::NUMBERS) :SHORT "Coerces a list of bit digits into a natural number." :LONG "<p>@(call bit-digit-list-value) is like @(see digit-list-value) but
for bit numbers.</p>

<p>See also @(see parse-bits-from-charlist) for a more flexible function that
can tolerate non-bit digits after the number.</p>" (DEFINLINED STR::BIT-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::BIT-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-BITS-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-BIT-DIGIT-LIST-VALUE (NATP (STR::BIT-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-BITS-FROM-CHARLIST STR::ICHARLISTEQV STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::BIT-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "1" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "01" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0101011101" (QUOTE LIST))) 349))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGIT-LIST-VALUE)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::BIT-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::BIT-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-BITS-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-BIT-DIGIT-LIST-VALUE (NATP (STR::BIT-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-BITS-FROM-CHARLIST STR::ICHARLISTEQV STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::BIT-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (LOCAL (ASSERT! (AND (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "1" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "01" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0101011101" (QUOTE LIST))) 349)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::BIT-DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::BIT-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-BITS-FROM-CHARLIST X 0 0))) STR::VAL)) (LOCAL (IN-THEORY (ENABLE STR::BIT-DIGIT-LIST-VALUE))) (DEFTHM STR::NATP-OF-BIT-DIGIT-LIST-VALUE (NATP (STR::BIT-DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (LOCAL (DEFTHMD STR::L0 (IMPLIES (STR::ICHARLISTEQV X STR::X-EQUIV) (EQUAL (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST X STR::VAL LEN)) (MV-NTH 0 (STR::PARSE-BITS-FROM-CHARLIST STR::X-EQUIV STR::VAL LEN)))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::PARSE-BITS-FROM-CHARLIST STR::ICHARLISTEQV STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX))))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::BIT-DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :USE ((:INSTANCE STR::L0 (STR::VAL 0) (LEN 0)))))) (RECORD-EXPANSION (LOCAL (ASSERT! (AND (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0" (QUOTE LIST))) 0) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "1" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "01" (QUOTE LIST))) 1) (EQUAL (STR::BIT-DIGIT-LIST-VALUE (COERCE "0101011101" (QUOTE LIST))) 349)))) (LOCAL (VALUE-TRIPLE :ELIDED)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::BIT-DIGIT-LIST-VALUE)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a list of bit digits into a natural number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::BIT-DIGIT-LIST-VALUE))) 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 bit-digit-list-value) is like @(see digit-list-value) but
for bit numbers.</p>

<p>See also @(see parse-bits-from-charlist) for a more flexible function that
can tolerate non-bit digits after the number.</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::BIT-DIGIT-LIST-VALUE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a list of bit digits into a natural number.") (:LONG . "<p>@(call bit-digit-list-value) is like @(see digit-list-value) but
for bit numbers.</p>

<p>See also @(see parse-bits-from-charlist) for a more flexible function that
can tolerate non-bit digits after the number.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|BIT-DIGIT-LIST-VALUE$INLINE|)
@(def |STR|::|NATP-OF-BIT-DIGIT-LIST-VALUE|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-BIT-DIGIT-LIST-VALUE-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::BIT-DIGIT-LIST-VALUE)))))) (VALUE-TRIPLE (QUOTE STR::BIT-DIGIT-LIST-VALUE))))) (18 RECORD-EXPANSION (DEFSECTION STR::STRVAL :PARENTS (STR::NUMBERS) :SHORT "Interpret a string as a decimal number." :LONG "<p>@(call strval) tries to interpret a string as a base-10 natural
number.  For example, @('(strval \"35\")') is 35.  If the string has any
non-decimal digit characters or is empty, we return @('nil').</p>" (DEFUND STR::STRVAL (X) (DECLARE (TYPE STRING X)) (B* (((THE (INTEGER 0 *) STR::XL) (MBE :LOGIC (LEN (EXPLODE X)) :EXEC (LENGTH X))) ((MV (THE (INTEGER 0 *) STR::VAL) (THE (INTEGER 0 *) LEN)) (STR::PARSE-NAT-FROM-STRING X 0 0 0 STR::XL))) (AND (< 0 LEN) (INT= LEN STR::XL) STR::VAL))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL))) (DEFTHM STR::TYPE-OF-STRVAL (OR (NATP (STR::STRVAL X)) (NOT (STR::STRVAL X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRVAL (X) (DECLARE (TYPE STRING X)) (B* (((THE (INTEGER 0 *) STR::XL) (MBE :LOGIC (LEN (EXPLODE X)) :EXEC (LENGTH X))) ((MV (THE (INTEGER 0 *) STR::VAL) (THE (INTEGER 0 *) LEN)) (STR::PARSE-NAT-FROM-STRING X 0 0 0 STR::XL))) (AND (< 0 LEN) (INT= LEN STR::XL) STR::VAL))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL))) (DEFTHM STR::TYPE-OF-STRVAL (OR (NATP (STR::STRVAL X)) (NOT (STR::STRVAL X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRVAL)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Interpret a string as a decimal number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL))) 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 strval) tries to interpret a string as a base-10 natural
number.  For example, @('(strval \"35\")') is 35.  If the string has any
non-decimal digit characters or is empty, we return @('nil').</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::STRVAL) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Interpret a string as a decimal number.") (:LONG . "<p>@(call strval) tries to interpret a string as a base-10 natural
number.  For example, @('(strval \"35\")') is 35.  If the string has any
non-decimal digit characters or is empty, we return @('nil').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRVAL|)
@(def |STR|::|TYPE-OF-STRVAL|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-STRVAL-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRVAL)))))) (VALUE-TRIPLE (QUOTE STR::STRVAL))))) (19 RECORD-EXPANSION (DEFSECTION STR::STRVAL8 :PARENTS (STR::NUMBERS) :SHORT "Interpret a string as an octal number." :LONG "<p>@(call strval8) is like @(see strval) but for octal instead of
decimal numbers.  For example, @('(strval8 \"10\")') is 8.  If the string is
empty or has any non-octal digit characters, we return @('nil').</p>" (DEFUND STR::STRVAL8 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::OCTAL-DIGIT-LISTP STR::CHARS) (STR::OCTAL-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL8))) (DEFTHM STR::TYPE-OF-STRVAL8 (OR (NATP (STR::STRVAL8 X)) (NOT (STR::STRVAL8 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL8 X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL8)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRVAL8 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::OCTAL-DIGIT-LISTP STR::CHARS) (STR::OCTAL-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL8))) (DEFTHM STR::TYPE-OF-STRVAL8 (OR (NATP (STR::STRVAL8 X)) (NOT (STR::STRVAL8 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL8 X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRVAL8)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Interpret a string as an octal number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL8))) 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 strval8) is like @(see strval) but for octal instead of
decimal numbers.  For example, @('(strval8 \"10\")') is 8.  If the string is
empty or has any non-octal digit characters, we return @('nil').</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::STRVAL8) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Interpret a string as an octal number.") (:LONG . "<p>@(call strval8) is like @(see strval) but for octal instead of
decimal numbers.  For example, @('(strval8 \"10\")') is 8.  If the string is
empty or has any non-octal digit characters, we return @('nil').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRVAL8|)
@(def |STR|::|TYPE-OF-STRVAL8|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-STRVAL8-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRVAL8)))))) (VALUE-TRIPLE (QUOTE STR::STRVAL8))))) (20 RECORD-EXPANSION (DEFSECTION STR::STRVAL16 :PARENTS (STR::NUMBERS) :SHORT "Interpret a string as a hexadecimal number." :LONG "<p>@(call strval16) is like @(see strval) but for hexadecimal instead
of decimal numbers.  For example, @('(strval16 \"10\")') is 16.  If the string
is empty or has any non-hex digit characters, we return @('nil').</p>" (DEFUND STR::STRVAL16 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::HEX-DIGIT-LISTP STR::CHARS) (STR::HEX-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL16))) (DEFTHM STR::TYPE-OF-STRVAL16 (OR (NATP (STR::STRVAL16 X)) (NOT (STR::STRVAL16 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL16 X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL16)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRVAL16 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::HEX-DIGIT-LISTP STR::CHARS) (STR::HEX-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL16))) (DEFTHM STR::TYPE-OF-STRVAL16 (OR (NATP (STR::STRVAL16 X)) (NOT (STR::STRVAL16 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL16 X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRVAL16)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Interpret a string as a hexadecimal number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL16))) 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 strval16) is like @(see strval) but for hexadecimal instead
of decimal numbers.  For example, @('(strval16 \"10\")') is 16.  If the string
is empty or has any non-hex digit characters, we return @('nil').</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::STRVAL16) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Interpret a string as a hexadecimal number.") (:LONG . "<p>@(call strval16) is like @(see strval) but for hexadecimal instead
of decimal numbers.  For example, @('(strval16 \"10\")') is 16.  If the string
is empty or has any non-hex digit characters, we return @('nil').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRVAL16|)
@(def |STR|::|TYPE-OF-STRVAL16|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-STRVAL16-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRVAL16)))))) (VALUE-TRIPLE (QUOTE STR::STRVAL16))))) (21 RECORD-EXPANSION (DEFSECTION STR::STRVAL2 :PARENTS (STR::NUMBERS) :SHORT "Interpret a string as a binary number." :LONG "<p>@(call strval2) is like @(see strval) but for binary instead of
decimal numbers.  For example, @('(strval16 \"10\")') is 2.  If the string is
empty or has any non-binary digit characters, we return @('nil').</p>" (DEFUND STR::STRVAL2 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::BIT-DIGIT-LISTP STR::CHARS) (STR::BIT-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL2))) (DEFTHM STR::TYPE-OF-STRVAL2 (OR (NATP (STR::STRVAL2 X)) (NOT (STR::STRVAL2 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL2 X) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL2)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRVAL2 (X) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::BIT-DIGIT-LISTP STR::CHARS) (STR::BIT-DIGIT-LIST-VALUE STR::CHARS)))) (LOCAL (IN-THEORY (ENABLE STR::STRVAL2))) (DEFTHM STR::TYPE-OF-STRVAL2 (OR (NATP (STR::STRVAL2 X)) (NOT (STR::STRVAL2 X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFCONG STR::ISTREQV EQUAL (STR::STRVAL2 X) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRVAL2)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Interpret a string as a binary number.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRVAL2))) 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 strval2) is like @(see strval) but for binary instead of
decimal numbers.  For example, @('(strval16 \"10\")') is 2.  If the string is
empty or has any non-binary digit characters, we return @('nil').</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::STRVAL2) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Interpret a string as a binary number.") (:LONG . "<p>@(call strval2) is like @(see strval) but for binary instead of
decimal numbers.  For example, @('(strval16 \"10\")') is 2.  If the string is
empty or has any non-binary digit characters, we return @('nil').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRVAL2|)
@(def |STR|::|TYPE-OF-STRVAL2|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-STRVAL2-1|)") (:FROM . "[books]/str/strval.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRVAL2)))))) (VALUE-TRIPLE (QUOTE STR::STRVAL2))))) (22 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL "") NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (23 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL2 "") NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (24 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL8 "") NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (25 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL16 "") NIL))) (LOCAL (VALUE-TRIPLE :ELIDED))) (26 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL "0") 0))) (LOCAL (VALUE-TRIPLE :ELIDED))) (27 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL2 "0") 0))) (LOCAL (VALUE-TRIPLE :ELIDED))) (28 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL8 "0") 0))) (LOCAL (VALUE-TRIPLE :ELIDED))) (29 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL16 "0") 0))) (LOCAL (VALUE-TRIPLE :ELIDED))) (30 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL "1234") 1234))) (LOCAL (VALUE-TRIPLE :ELIDED))) (31 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL2 "0101") 5))) (LOCAL (VALUE-TRIPLE :ELIDED))) (32 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL8 "1234") 668))) (LOCAL (VALUE-TRIPLE :ELIDED))) (33 RECORD-EXPANSION (LOCAL (ASSERT! (EQUAL (STR::STRVAL16 "1234") 4660))) (LOCAL (VALUE-TRIPLE :ELIDED))))
(("/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/strval.lisp" "strval" "strval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1981642498) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) ("/usr/share/acl2-6.3/books/str/strnatless.lisp" "strnatless" "strnatless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797808730) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 248299501)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915259697)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 732116275)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105657945)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 864029516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 750113408)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1374753694)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122664565)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013733040)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061645425)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619080936)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 972646001)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 384804126)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1113724693)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 483566967)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 457663279)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134470975)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 784695287)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2126151702)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653127144)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1661395704)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1273493319)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 508744284)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061889192)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153949377)) ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140) ("/usr/share/acl2-6.3/books/str/digitp.lisp" "digitp" "digitp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479290421) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/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))
2105863970