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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFSECTION STR::DIGITP :PARENTS (STR::NUMBERS) :SHORT "Recognizer for numeric characters (0-9)." :LONG "<p>ACL2 provides @(see digit-char-p) which is more flexible and can
recognize numeric characters in other bases.  @(call digitp) only recognizes
base-10 digits, but is roughly twice as fast as @('digit-char-p'), at least on
CCL.  Here is an experiment you can run in raw lisp, with times reported in CCL
on the machine Lisp2.</p>

@({
  (defconstant *chars*
    (loop for i from 0 to 256 collect (code-char i)))

  ;; 21.876 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digit-char-p c))))

  ;; 10.819 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digitp c))))
})" (DEFINLINED STR::DIGITP (X) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (LOCAL (IN-THEORY (ENABLE STR::DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::CHARACTERP-WHEN-DIGITP (IMPLIES (STR::DIGITP CHAR) (CHARACTERP CHAR)) :RULE-CLASSES :COMPOUND-RECOGNIZER)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DIGITP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::DIGITP (X) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (LOCAL (IN-THEORY (ENABLE STR::DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::CHARACTERP-WHEN-DIGITP (IMPLIES (STR::DIGITP CHAR) (CHARACTERP CHAR)) :RULE-CLASSES :COMPOUND-RECOGNIZER))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DIGITP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizer for numeric characters (0-9).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::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>ACL2 provides @(see digit-char-p) which is more flexible and can
recognize numeric characters in other bases.  @(call digitp) only recognizes
base-10 digits, but is roughly twice as fast as @('digit-char-p'), at least on
CCL.  Here is an experiment you can run in raw lisp, with times reported in CCL
on the machine Lisp2.</p>

@({
  (defconstant *chars*
    (loop for i from 0 to 256 collect (code-char i)))

  ;; 21.876 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digit-char-p c))))

  ;; 10.819 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digitp c))))
})") (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::DIGITP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizer for numeric characters (0-9).") (:LONG . "<p>ACL2 provides @(see digit-char-p) which is more flexible and can
recognize numeric characters in other bases.  @(call digitp) only recognizes
base-10 digits, but is roughly twice as fast as @('digit-char-p'), at least on
CCL.  Here is an experiment you can run in raw lisp, with times reported in CCL
on the machine Lisp2.</p>

@({
  (defconstant *chars*
    (loop for i from 0 to 256 collect (code-char i)))

  ;; 21.876 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digit-char-p c))))

  ;; 10.819 seconds, no garbage
  (time (loop for i fixnum from 1 to 10000000 do
              (loop for c in *chars* do (digitp c))))
})

<h3>Definitions and Theorems</h3>@(def |STR|::|DIGITP$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-DIGITP-1|)
@(def |STR|::|CHARACTERP-WHEN-DIGITP|)") (:FROM . "[books]/str/digitp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DIGITP)))))) (VALUE-TRIPLE (QUOTE STR::DIGITP))))) (6 RECORD-EXPANSION (DEFSECTION STR::NONZERO-DIGITP :PARENTS (STR::NUMBERS) :SHORT "Recognizer for non-zero numeric characters (1-9)." (DEFINLINED STR::NONZERO-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\1) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 49) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (LOCAL (IN-THEORY (ENABLE STR::NONZERO-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::NONZERO-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::DIGITP-WHEN-NONZERO-DIGITP (IMPLIES (STR::NONZERO-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::NONZERO-DIGITP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::NONZERO-DIGITP (X) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\1) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 49) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (LOCAL (IN-THEORY (ENABLE STR::NONZERO-DIGITP))) (DEFCONG STR::ICHAREQV EQUAL (STR::NONZERO-DIGITP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::DIGITP-WHEN-NONZERO-DIGITP (IMPLIES (STR::NONZERO-DIGITP X) (STR::DIGITP X)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::NONZERO-DIGITP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizer for non-zero numeric characters (1-9).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::NONZERO-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 "") (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::NONZERO-DIGITP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizer for non-zero numeric characters (1-9).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|NONZERO-DIGITP$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-NONZERO-DIGITP-1|)
@(def |STR|::|DIGITP-WHEN-NONZERO-DIGITP|)") (:FROM . "[books]/str/digitp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::NONZERO-DIGITP)))))) (VALUE-TRIPLE (QUOTE STR::NONZERO-DIGITP))))) (7 RECORD-EXPANSION (DEFSECTION STR::DIGIT-VAL :PARENTS (STR::NUMBERS) :SHORT "Coerces a @(see digitp) character into an integer." :LONG "<p>For instance, @('(digit-val #\\3)') is 3.  For any non-@('digitp'),
0 is returned.</p>" (DEFINLINED STR::DIGIT-VAL (X) (DECLARE (TYPE CHARACTER X) (XARGS :GUARD (STR::DIGITP X) :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP))))) (MBE :LOGIC (IF (STR::DIGITP X) (- (CHAR-CODE (STR::CHAR-FIX X)) (CHAR-CODE #\0)) 0) :EXEC (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))) (THE (UNSIGNED-BYTE 8) 48))))) (LOCAL (IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX))) (DEFCONG STR::ICHAREQV EQUAL (STR::DIGIT-VAL X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::NATP-OF-DIGIT-VAL (AND (INTEGERP (STR::DIGIT-VAL X)) (<= 0 (STR::DIGIT-VAL X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::DIGIT-VAL-UPPER-BOUND (< (STR::DIGIT-VAL X) 10) :RULE-CLASSES ((:REWRITE) (:LINEAR))) (DEFTHM STR::EQUAL-OF-DIGIT-VAL-AND-DIGIT-VAL (IMPLIES (AND (STR::DIGITP X) (STR::DIGITP Y)) (EQUAL (EQUAL (STR::DIGIT-VAL X) (STR::DIGIT-VAL Y)) (EQUAL X Y)))) (DEFTHM STR::DIGIT-VAL-OF-DIGIT-TO-CHAR (IMPLIES (AND (NATP N) (< N 10)) (EQUAL (STR::DIGIT-VAL (DIGIT-TO-CHAR N)) N)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DIGIT-VAL)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::DIGIT-VAL (X) (DECLARE (TYPE CHARACTER X) (XARGS :GUARD (STR::DIGITP X) :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGITP))))) (MBE :LOGIC (IF (STR::DIGITP X) (- (CHAR-CODE (STR::CHAR-FIX X)) (CHAR-CODE #\0)) 0) :EXEC (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))) (THE (UNSIGNED-BYTE 8) 48))))) (LOCAL (IN-THEORY (ENABLE STR::DIGITP STR::DIGIT-VAL STR::CHAR-FIX))) (DEFCONG STR::ICHAREQV EQUAL (STR::DIGIT-VAL X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::NATP-OF-DIGIT-VAL (AND (INTEGERP (STR::DIGIT-VAL X)) (<= 0 (STR::DIGIT-VAL X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::DIGIT-VAL-UPPER-BOUND (< (STR::DIGIT-VAL X) 10) :RULE-CLASSES ((:REWRITE) (:LINEAR))) (DEFTHM STR::EQUAL-OF-DIGIT-VAL-AND-DIGIT-VAL (IMPLIES (AND (STR::DIGITP X) (STR::DIGITP Y)) (EQUAL (EQUAL (STR::DIGIT-VAL X) (STR::DIGIT-VAL Y)) (EQUAL X Y)))) (DEFTHM STR::DIGIT-VAL-OF-DIGIT-TO-CHAR (IMPLIES (AND (NATP N) (< N 10)) (EQUAL (STR::DIGIT-VAL (DIGIT-TO-CHAR N)) N))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DIGIT-VAL)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a @(see 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::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>For instance, @('(digit-val #\\3)') is 3.  For any non-@('digitp'),
0 is returned.</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::DIGIT-VAL) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a @(see digitp) character into an integer.") (:LONG . "<p>For instance, @('(digit-val #\\3)') is 3.  For any non-@('digitp'),
0 is returned.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|DIGIT-VAL$INLINE|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-DIGIT-VAL-1|)
@(def |STR|::|NATP-OF-DIGIT-VAL|)
@(def |STR|::|DIGIT-VAL-UPPER-BOUND|)
@(def |STR|::|EQUAL-OF-DIGIT-VAL-AND-DIGIT-VAL|)
@(def |STR|::|DIGIT-VAL-OF-DIGIT-TO-CHAR|)") (:FROM . "[books]/str/digitp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DIGIT-VAL)))))) (VALUE-TRIPLE (QUOTE STR::DIGIT-VAL))))) (8 RECORD-EXPANSION (DEFSECTION STR::DIGIT-LISTP :PARENTS (STR::NUMBERS) :SHORT "Recognizes lists of @(see digitp) characters." (DEFUND STR::DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (CONSP X) (AND (STR::DIGITP (CAR X)) (STR::DIGIT-LISTP (CDR X))) T)) (LOCAL (IN-THEORY (ENABLE STR::DIGIT-LISTP))) (DEFTHM STR::DIGIT-LISTP-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-CONS (EQUAL (STR::DIGIT-LISTP (CONS A X)) (AND (STR::DIGITP A) (STR::DIGIT-LISTP X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::DIGIT-LISTP-OF-LIST-FIX (EQUAL (STR::DIGIT-LISTP (LIST-FIX X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-APPEND (EQUAL (STR::DIGIT-LISTP (APPEND X Y)) (AND (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)))) (DEFTHM STR::DIGIT-LISTP-OF-REVAPPEND (EQUAL (STR::DIGIT-LISTP (REVAPPEND X Y)) (AND (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)))) (DEFTHM STR::DIGIT-LISTP-OF-REV (EQUAL (STR::DIGIT-LISTP (REV X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-NTHCDR (IMPLIES (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP (NTHCDR N X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DIGIT-LISTP)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::DIGIT-LISTP (X) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (CONSP X) (AND (STR::DIGITP (CAR X)) (STR::DIGIT-LISTP (CDR X))) T)) (LOCAL (IN-THEORY (ENABLE STR::DIGIT-LISTP))) (DEFTHM STR::DIGIT-LISTP-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-CONS (EQUAL (STR::DIGIT-LISTP (CONS A X)) (AND (STR::DIGITP A) (STR::DIGIT-LISTP X)))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DIGIT-LISTP X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::DIGIT-LISTP-OF-LIST-FIX (EQUAL (STR::DIGIT-LISTP (LIST-FIX X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-APPEND (EQUAL (STR::DIGIT-LISTP (APPEND X Y)) (AND (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)))) (DEFTHM STR::DIGIT-LISTP-OF-REVAPPEND (EQUAL (STR::DIGIT-LISTP (REVAPPEND X Y)) (AND (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP Y)))) (DEFTHM STR::DIGIT-LISTP-OF-REV (EQUAL (STR::DIGIT-LISTP (REV X)) (STR::DIGIT-LISTP X))) (DEFTHM STR::DIGIT-LISTP-OF-NTHCDR (IMPLIES (STR::DIGIT-LISTP X) (STR::DIGIT-LISTP (NTHCDR N X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DIGIT-LISTP)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Recognizes lists of @(see 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::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::DIGIT-LISTP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Recognizes lists of @(see digitp) characters.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|DIGIT-LISTP|)
@(def |STR|::|DIGIT-LISTP-WHEN-NOT-CONSP|)
@(def |STR|::|DIGIT-LISTP-OF-CONS|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-DIGIT-LISTP-1|)
@(def |STR|::|DIGIT-LISTP-OF-LIST-FIX|)
@(def |STR|::|DIGIT-LISTP-OF-APPEND|)
@(def |STR|::|DIGIT-LISTP-OF-REVAPPEND|)
@(def |STR|::|DIGIT-LISTP-OF-REV|)
@(def |STR|::|DIGIT-LISTP-OF-NTHCDR|)") (:FROM . "[books]/str/digitp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DIGIT-LISTP)))))) (VALUE-TRIPLE (QUOTE STR::DIGIT-LISTP))))) (9 RECORD-EXPANSION (DEFSECTION STR::DIGIT-LIST-VALUE :PARENTS (STR::NUMBERS) :SHORT "Coerces a @(see digit-listp) into a natural number." :LONG "<p>For instance, @('(digit-list-value '(#1 #0 #3))') is 103.</p>

<p>See also @(see parse-nat-from-charlist) for a more flexible function that
can tolerate non-numeric characters after the number.</p>" (DEFUND STR::DIGIT-LIST-VALUE1 (X STR::VAL) (DECLARE (TYPE (INTEGER 0 *) STR::VAL) (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::DIGIT-LISTP X)) :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-VAL STR::DIGITP))))) (MBE :LOGIC (IF (CONSP X) (STR::DIGIT-LIST-VALUE1 (CDR X) (+ (STR::DIGIT-VAL (CAR X)) (* 10 (NFIX STR::VAL)))) (NFIX STR::VAL)) :EXEC (IF (CONSP X) (STR::DIGIT-LIST-VALUE1 (CDR X) (THE (INTEGER 0 *) (+ (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X)))) (THE (UNSIGNED-BYTE 8) 48))) (* (THE (INTEGER 0 *) 10) (THE (INTEGER 0 *) STR::VAL))))) (THE (INTEGER 0 *) STR::VAL)))) (DEFINLINED STR::DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::DIGIT-LISTP X)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (CONSP X) (+ (* (EXPT 10 (1- (LEN X))) (STR::DIGIT-VAL (CAR X))) (STR::DIGIT-LIST-VALUE (CDR X))) 0) :EXEC (STR::DIGIT-LIST-VALUE1 X 0))) (LOCAL (IN-THEORY (ENABLE STR::DIGIT-LIST-VALUE))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::NATP-OF-DIGIT-LIST-VALUE (NATP (STR::DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (ENCAPSULATE NIL (SET-NON-LINEARP T) (DEFTHM STR::DIGIT-LIST-VALUE-UPPER-BOUND (< (STR::DIGIT-LIST-VALUE X) (EXPT 10 (LEN X))))) (DEFTHM STR::DIGIT-LIST-VALUE-UPPER-BOUND-FREE (IMPLIES (EQUAL N (LEN X)) (< (STR::DIGIT-LIST-VALUE X) (EXPT 10 N)))) (DEFTHM STR::DIGIT-LIST-VALUE1-REMOVAL (EQUAL (STR::DIGIT-LIST-VALUE1 X STR::VAL) (+ (STR::DIGIT-LIST-VALUE X) (* (NFIX STR::VAL) (EXPT 10 (LEN X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-LIST-VALUE1) :INDUCT (STR::DIGIT-LIST-VALUE1 X STR::VAL)))) (VERIFY-GUARDS STR::DIGIT-LIST-VALUE$INLINE) (DEFTHM STR::DIGIT-LIST-VALUE-OF-APPEND (EQUAL (STR::DIGIT-LIST-VALUE (APPEND X (LIST A))) (+ (* 10 (STR::DIGIT-LIST-VALUE X)) (STR::DIGIT-VAL A))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::DIGIT-LIST-VALUE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::DIGIT-LIST-VALUE1 (X STR::VAL) (DECLARE (TYPE (INTEGER 0 *) STR::VAL) (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::DIGIT-LISTP X)) :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-VAL STR::DIGITP))))) (MBE :LOGIC (IF (CONSP X) (STR::DIGIT-LIST-VALUE1 (CDR X) (+ (STR::DIGIT-VAL (CAR X)) (* 10 (NFIX STR::VAL)))) (NFIX STR::VAL)) :EXEC (IF (CONSP X) (STR::DIGIT-LIST-VALUE1 (CDR X) (THE (INTEGER 0 *) (+ (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X)))) (THE (UNSIGNED-BYTE 8) 48))) (* (THE (INTEGER 0 *) 10) (THE (INTEGER 0 *) STR::VAL))))) (THE (INTEGER 0 *) STR::VAL)))) (DEFINLINED STR::DIGIT-LIST-VALUE (X) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::DIGIT-LISTP X)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (IF (CONSP X) (+ (* (EXPT 10 (1- (LEN X))) (STR::DIGIT-VAL (CAR X))) (STR::DIGIT-LIST-VALUE (CDR X))) 0) :EXEC (STR::DIGIT-LIST-VALUE1 X 0))) (LOCAL (IN-THEORY (ENABLE STR::DIGIT-LIST-VALUE))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::DIGIT-LIST-VALUE X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHARLISTEQV)))) (DEFTHM STR::NATP-OF-DIGIT-LIST-VALUE (NATP (STR::DIGIT-LIST-VALUE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (ENCAPSULATE NIL (SET-NON-LINEARP T) (DEFTHM STR::DIGIT-LIST-VALUE-UPPER-BOUND (< (STR::DIGIT-LIST-VALUE X) (EXPT 10 (LEN X))))) (DEFTHM STR::DIGIT-LIST-VALUE-UPPER-BOUND-FREE (IMPLIES (EQUAL N (LEN X)) (< (STR::DIGIT-LIST-VALUE X) (EXPT 10 N)))) (DEFTHM STR::DIGIT-LIST-VALUE1-REMOVAL (EQUAL (STR::DIGIT-LIST-VALUE1 X STR::VAL) (+ (STR::DIGIT-LIST-VALUE X) (* (NFIX STR::VAL) (EXPT 10 (LEN X))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::DIGIT-LIST-VALUE1) :INDUCT (STR::DIGIT-LIST-VALUE1 X STR::VAL)))) (VERIFY-GUARDS STR::DIGIT-LIST-VALUE$INLINE) (DEFTHM STR::DIGIT-LIST-VALUE-OF-APPEND (EQUAL (STR::DIGIT-LIST-VALUE (APPEND X (LIST A))) (+ (* 10 (STR::DIGIT-LIST-VALUE X)) (STR::DIGIT-VAL A)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::DIGIT-LIST-VALUE)) (XDOC::PARENTS (QUOTE (STR::NUMBERS))) (XDOC::SHORT (QUOTE "Coerces a @(see digit-listp) 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::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>For instance, @('(digit-list-value '(#1 #0 #3))') is 103.</p>

<p>See also @(see parse-nat-from-charlist) for a more flexible function that
can tolerate non-numeric characters 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::DIGIT-LIST-VALUE) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::NUMBERS) (:SHORT . "Coerces a @(see digit-listp) into a natural number.") (:LONG . "<p>For instance, @('(digit-list-value '(#1 #0 #3))') is 103.</p>

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

<h3>Definitions and Theorems</h3>@(def |STR|::|DIGIT-LIST-VALUE1|)
@(def |STR|::|DIGIT-LIST-VALUE$INLINE|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-DIGIT-LIST-VALUE-1|)
@(def |STR|::|NATP-OF-DIGIT-LIST-VALUE|)
@(def |STR|::|DIGIT-LIST-VALUE-UPPER-BOUND|)
@(def |STR|::|DIGIT-LIST-VALUE-UPPER-BOUND-FREE|)
@(def |STR|::|DIGIT-LIST-VALUE1-REMOVAL|)
@(def |STR|::|DIGIT-LIST-VALUE-OF-APPEND|)") (:FROM . "[books]/str/digitp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::DIGIT-LIST-VALUE)))))) (VALUE-TRIPLE (QUOTE STR::DIGIT-LIST-VALUE))))))
(("/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/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))
376990158