/usr/share/acl2-6.3/books/str/strrpos.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (DEFSECTION STR::STRRPOS-FAST :PARENTS (STR::STRRPOS) :SHORT "Fast implementation of @(see strrpos)." (DEFUND STR::STRRPOS-FAST (X Y N STR::XL STR::YL) (DECLARE (TYPE STRING X Y) (TYPE (INTEGER 0 *) N STR::XL STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y))) :MEASURE (NFIX N))) (COND ((MBE :LOGIC (PREFIXP (EXPLODE X) (NTHCDR N (EXPLODE Y))) :EXEC (STR::STRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE (INTEGER 0 *) N) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))) (LNFIX N)) ((ZP N) NIL) (T (STR::STRRPOS-FAST (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) (+ -1 (LNFIX N))) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))))) (LOCAL (IN-THEORY (ENABLE STR::STRRPOS-FAST))) (DEFTHM STR::STRRPOS-FAST-TYPE (OR (AND (INTEGERP (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (<= 0 (STR::STRRPOS-FAST X Y N STR::XL STR::YL))) (NOT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::STRRPOS-FAST-UPPER-BOUND (IMPLIES (FORCE (NATP N)) (<= (STR::STRRPOS-FAST X Y N STR::XL STR::YL) N)) :RULE-CLASSES :LINEAR) (DEFTHM STR::STRRPOS-FAST-WHEN-EMPTY (IMPLIES (AND (NOT (CONSP (EXPLODE X))) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (NATP N)) (EQUAL (STR::STRRPOS-FAST X Y N STR::XL STR::YL) N)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRRPOS-FAST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::STRRPOS-FAST (X Y N STR::XL STR::YL) (DECLARE (TYPE STRING X Y) (TYPE (INTEGER 0 *) N STR::XL STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y))) :MEASURE (NFIX N))) (COND ((MBE :LOGIC (PREFIXP (EXPLODE X) (NTHCDR N (EXPLODE Y))) :EXEC (STR::STRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE (INTEGER 0 *) N) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))) (LNFIX N)) ((ZP N) NIL) (T (STR::STRRPOS-FAST (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) (+ -1 (LNFIX N))) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))))) (LOCAL (IN-THEORY (ENABLE STR::STRRPOS-FAST))) (DEFTHM STR::STRRPOS-FAST-TYPE (OR (AND (INTEGERP (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (<= 0 (STR::STRRPOS-FAST X Y N STR::XL STR::YL))) (NOT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::STRRPOS-FAST-UPPER-BOUND (IMPLIES (FORCE (NATP N)) (<= (STR::STRRPOS-FAST X Y N STR::XL STR::YL) N)) :RULE-CLASSES :LINEAR) (DEFTHM STR::STRRPOS-FAST-WHEN-EMPTY (IMPLIES (AND (NOT (CONSP (EXPLODE X))) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (NATP N)) (EQUAL (STR::STRRPOS-FAST X Y N STR::XL STR::YL) N))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRRPOS-FAST)) (XDOC::PARENTS (QUOTE (STR::STRRPOS))) (XDOC::SHORT (QUOTE "Fast implementation of @(see strrpos).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRRPOS-FAST))) 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::STRRPOS-FAST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::STRRPOS) (:SHORT . "Fast implementation of @(see strrpos).") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|STRRPOS-FAST|)
@(def |STR|::|STRRPOS-FAST-TYPE|)
@(def |STR|::|STRRPOS-FAST-UPPER-BOUND|)
@(def |STR|::|STRRPOS-FAST-WHEN-EMPTY|)") (:FROM . "[books]/str/strrpos.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRRPOS-FAST)))))) (VALUE-TRIPLE (QUOTE STR::STRRPOS-FAST))))) (4 RECORD-EXPANSION (DEFSECTION STR::STRRPOS :PARENTS (STR::SUBSTRINGS) :SHORT "Locate the last occurrence of a substring." :LONG "<p>@(call strrpos) searches through the string @('y') for the last
occurrence of the substring @('x').  If @('x') occurs somewhere in @('y'), it
returns the starting index of the last occurrence.  Otherwise, it returns
@('nil') to indicate that @('x') never occurs in @('y').</p>

<p>The function is \"efficient\" in the sense that it does not coerce its
arguments into lists, but rather traverses both strings with @(see char).  On
the other hand, it is a naive string search which operates by repeatedly
calling @(see strprefixp), rather than some better algorithm.</p>

<p>Corner case: we say that the empty string <b>is</b> an prefix of any other
string.  As a consequence, @('(strrpos \"\" x)') is (length x) for all
@('x').</p>" (DEFINLINED STR::STRRPOS (X Y) (DECLARE (TYPE STRING X Y)) (LET ((STR::YL (LENGTH (THE STRING Y)))) (DECLARE (TYPE (INTEGER 0 *) STR::YL)) (STR::STRRPOS-FAST (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) STR::YL) (THE (INTEGER 0 *) (LENGTH (THE STRING X))) (THE (INTEGER 0 *) STR::YL)))) (LOCAL (IN-THEORY (ENABLE STR::STRRPOS STR::STRRPOS-FAST))) (DEFTHM STR::STRRPOS-TYPE (OR (AND (INTEGERP (STR::STRRPOS X Y)) (<= 0 (STR::STRRPOS X Y))) (NOT (STR::STRRPOS X Y))) :RULE-CLASSES :TYPE-PRESCRIPTION) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (PREFIXP (EXPLODE X) (NTHCDR (STR::STRRPOS-FAST X Y N STR::XL STR::YL) (EXPLODE Y)))) :HINTS (("Goal" :INDUCT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))))) (DEFTHM STR::PREFIXP-OF-STRRPOS (IMPLIES (AND (STR::STRRPOS X Y) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (PREFIXP (EXPLODE X) (NTHCDR (STR::STRRPOS X Y) (EXPLODE Y)))))) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCTION (X Y N M STR::XL STR::YL) (DECLARE (XARGS :MEASURE (NFIX N))) (COND ((PREFIXP (EXPLODE X) (NTHCDR N (EXPLODE Y))) NIL) ((ZP N) (LIST X Y N M STR::XL STR::YL)) (T (STR::MY-INDUCTION X Y (- (NFIX N) 1) (IF (= (NFIX N) (NFIX M)) (- (NFIX M) 1) M) STR::XL STR::YL))))) (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (NATP M) (>= N M) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (PREFIXP (EXPLODE X) (NTHCDR M (EXPLODE Y)))) (AND (NATP (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (>= (STR::STRRPOS-FAST X Y N STR::XL STR::YL) M))) :HINTS (("Goal" :INDUCT (STR::MY-INDUCTION X Y N M STR::XL STR::YL) :DO-NOT (QUOTE (GENERALIZE FERTILIZE)))))) (DEFTHM STR::COMPLETENESS-OF-STRRPOS (IMPLIES (AND (PREFIXP (EXPLODE X) (NTHCDR M (EXPLODE Y))) (<= M (LEN Y)) (FORCE (NATP M)) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (AND (NATP (STR::STRRPOS X Y)) (>= (STR::STRRPOS X Y) M))))) (DEFTHM STR::STRRPOS-UPPER-BOUND-WEAK (IMPLIES (AND (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (<= (STR::STRRPOS X Y) (LEN (EXPLODE Y)))) :RULE-CLASSES ((:REWRITE) (:LINEAR))) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (POSP STR::XL) (POSP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y))) (< (STR::STRRPOS-FAST X Y N STR::XL STR::YL) STR::YL)) :HINTS (("Goal" :INDUCT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))))) (DEFTHM STR::STRRPOS-UPPER-BOUND-STRONG (IMPLIES (AND (NOT (EQUAL Y "")) (NOT (EQUAL X "")) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (< (STR::STRRPOS X Y) (LEN (EXPLODE Y)))) :RULE-CLASSES ((:REWRITE) (:LINEAR))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRRPOS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STRRPOS (X Y) (DECLARE (TYPE STRING X Y)) (LET ((STR::YL (LENGTH (THE STRING Y)))) (DECLARE (TYPE (INTEGER 0 *) STR::YL)) (STR::STRRPOS-FAST (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) STR::YL) (THE (INTEGER 0 *) (LENGTH (THE STRING X))) (THE (INTEGER 0 *) STR::YL)))) (LOCAL (IN-THEORY (ENABLE STR::STRRPOS STR::STRRPOS-FAST))) (DEFTHM STR::STRRPOS-TYPE (OR (AND (INTEGERP (STR::STRRPOS X Y)) (<= 0 (STR::STRRPOS X Y))) (NOT (STR::STRRPOS X Y))) :RULE-CLASSES :TYPE-PRESCRIPTION) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (PREFIXP (EXPLODE X) (NTHCDR (STR::STRRPOS-FAST X Y N STR::XL STR::YL) (EXPLODE Y)))) :HINTS (("Goal" :INDUCT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))))) (DEFTHM STR::PREFIXP-OF-STRRPOS (IMPLIES (AND (STR::STRRPOS X Y) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (PREFIXP (EXPLODE X) (NTHCDR (STR::STRRPOS X Y) (EXPLODE Y)))))) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCTION (X Y N M STR::XL STR::YL) (DECLARE (XARGS :MEASURE (NFIX N))) (COND ((PREFIXP (EXPLODE X) (NTHCDR N (EXPLODE Y))) NIL) ((ZP N) (LIST X Y N M STR::XL STR::YL)) (T (STR::MY-INDUCTION X Y (- (NFIX N) 1) (IF (= (NFIX N) (NFIX M)) (- (NFIX M) 1) M) STR::XL STR::YL))))) (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP STR::XL) (NATP STR::YL) (NATP N) (NATP M) (>= N M) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (PREFIXP (EXPLODE X) (NTHCDR M (EXPLODE Y)))) (AND (NATP (STR::STRRPOS-FAST X Y N STR::XL STR::YL)) (>= (STR::STRRPOS-FAST X Y N STR::XL STR::YL) M))) :HINTS (("Goal" :INDUCT (STR::MY-INDUCTION X Y N M STR::XL STR::YL) :DO-NOT (QUOTE (GENERALIZE FERTILIZE)))))) (DEFTHM STR::COMPLETENESS-OF-STRRPOS (IMPLIES (AND (PREFIXP (EXPLODE X) (NTHCDR M (EXPLODE Y))) (<= M (LEN Y)) (FORCE (NATP M)) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (AND (NATP (STR::STRRPOS X Y)) (>= (STR::STRRPOS X Y) M))))) (DEFTHM STR::STRRPOS-UPPER-BOUND-WEAK (IMPLIES (AND (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (<= (STR::STRRPOS X Y) (LEN (EXPLODE Y)))) :RULE-CLASSES ((:REWRITE) (:LINEAR))) (ENCAPSULATE NIL (LOCAL (DEFTHM STR::LEMMA (IMPLIES (AND (STRINGP X) (STRINGP Y) (POSP STR::XL) (POSP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y))) (< (STR::STRRPOS-FAST X Y N STR::XL STR::YL) STR::YL)) :HINTS (("Goal" :INDUCT (STR::STRRPOS-FAST X Y N STR::XL STR::YL))))) (DEFTHM STR::STRRPOS-UPPER-BOUND-STRONG (IMPLIES (AND (NOT (EQUAL Y "")) (NOT (EQUAL X "")) (FORCE (STRINGP X)) (FORCE (STRINGP Y))) (< (STR::STRRPOS X Y) (LEN (EXPLODE Y)))) :RULE-CLASSES ((:REWRITE) (:LINEAR)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRRPOS)) (XDOC::PARENTS (QUOTE (STR::SUBSTRINGS))) (XDOC::SHORT (QUOTE "Locate the last occurrence of a substring.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRRPOS))) 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 strrpos) searches through the string @('y') for the last
occurrence of the substring @('x').  If @('x') occurs somewhere in @('y'), it
returns the starting index of the last occurrence.  Otherwise, it returns
@('nil') to indicate that @('x') never occurs in @('y').</p>

<p>The function is \"efficient\" in the sense that it does not coerce its
arguments into lists, but rather traverses both strings with @(see char).  On
the other hand, it is a naive string search which operates by repeatedly
calling @(see strprefixp), rather than some better algorithm.</p>

<p>Corner case: we say that the empty string <b>is</b> an prefix of any other
string.  As a consequence, @('(strrpos \"\" x)') is (length x) for all
@('x').</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::STRRPOS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SUBSTRINGS) (:SHORT . "Locate the last occurrence of a substring.") (:LONG . "<p>@(call strrpos) searches through the string @('y') for the last
occurrence of the substring @('x').  If @('x') occurs somewhere in @('y'), it
returns the starting index of the last occurrence.  Otherwise, it returns
@('nil') to indicate that @('x') never occurs in @('y').</p>

<p>The function is \"efficient\" in the sense that it does not coerce its
arguments into lists, but rather traverses both strings with @(see char).  On
the other hand, it is a naive string search which operates by repeatedly
calling @(see strprefixp), rather than some better algorithm.</p>

<p>Corner case: we say that the empty string <b>is</b> an prefix of any other
string.  As a consequence, @('(strrpos \"\" x)') is (length x) for all
@('x').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|STRRPOS$INLINE|)
@(def |STR|::|STRRPOS-TYPE|)
@(def |STR|::|PREFIXP-OF-STRRPOS|)
@(def |STR|::|COMPLETENESS-OF-STRRPOS|)
@(def |STR|::|STRRPOS-UPPER-BOUND-WEAK|)
@(def |STR|::|STRRPOS-UPPER-BOUND-STRONG|)") (:FROM . "[books]/str/strrpos.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRRPOS)))))) (VALUE-TRIPLE (QUOTE STR::STRRPOS))))))
(("/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/strrpos.lisp" "strrpos" "strrpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1502347794) ("/usr/share/acl2-6.3/books/str/strprefixp.lisp" "strprefixp" "strprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2141614236) ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "std/lists/prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/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))
1394831211
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / strrpos.cert
