/usr/share/acl2-6.3/books/str/suffixp.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((7 RECORD-EXPANSION (DEFSECTION STR::STRSUFFIXP :PARENTS (STR::SUBSTRINGS) :SHORT "Case-sensitive string suffix test." :LONG "<p>@(call strsuffixp) determines if the string @('x') is a suffix of
the string @('y'), in a case-sensitive manner.</p>
<p>Logically, we ask whether @('|x| < |y|'), and whether</p>
@({
(equal (nthcdr (- |y| |x|) (explode x))
(explode y))
})
<p>But we use a more efficient implementation that avoids coercing the strings
into lists; basically we ask if the last @('|x|') characters of @('y') are
equal to @('x').</p>
<p>Corner case: we regard the empty string as a suffix of every other string.
That is, @('(strsuffixp \"\" x)') is always true.</p>" (DEFINLINED STR::STRSUFFIXP (X Y) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (LET* ((STR::XCHARS (EXPLODE X)) (STR::YCHARS (EXPLODE Y)) (STR::XLEN (LEN STR::XCHARS)) (STR::YLEN (LEN STR::YCHARS))) (AND (<= STR::XLEN STR::YLEN) (EQUAL (NTHCDR (- STR::YLEN STR::XLEN) (EXPLODE Y)) (EXPLODE X)))) :EXEC (LET* ((STR::XLEN (LENGTH X)) (STR::YLEN (LENGTH Y))) (AND (<= STR::XLEN STR::YLEN) (STR::STRPREFIXP-IMPL X Y 0 (- STR::YLEN STR::XLEN) STR::XLEN STR::YLEN))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUFFIXP))) (LOCAL (DEFTHM STR::C0 (IMPLIES (AND (NATP N) (<= (LEN X) N) (TRUE-LISTP X)) (EQUAL (NTHCDR N X) NIL)))) (LOCAL (DEFTHM STR::C1 (IMPLIES (TRUE-LISTP X) (NOT (NTHCDR (LEN X) X))))) (DEFTHM STR::STRSUFFIXP-OF-EMPTY (STR::STRSUFFIXP "" Y)) (LOCAL (PROGN (ASSERT! (STR::STRSUFFIXP "" "")) (ASSERT! (STR::STRSUFFIXP "" "foo")) (ASSERT! (STR::STRSUFFIXP "o" "foo")) (ASSERT! (STR::STRSUFFIXP "oo" "foo")) (ASSERT! (NOT (STR::STRSUFFIXP "ooo" "foo"))) (ASSERT! (NOT (STR::STRSUFFIXP "fo" "foo"))) (ASSERT! (STR::STRSUFFIXP "foo" "foo")))) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 1) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUFFIXP)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STRSUFFIXP (X Y) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (LET* ((STR::XCHARS (EXPLODE X)) (STR::YCHARS (EXPLODE Y)) (STR::XLEN (LEN STR::XCHARS)) (STR::YLEN (LEN STR::YCHARS))) (AND (<= STR::XLEN STR::YLEN) (EQUAL (NTHCDR (- STR::YLEN STR::XLEN) (EXPLODE Y)) (EXPLODE X)))) :EXEC (LET* ((STR::XLEN (LENGTH X)) (STR::YLEN (LENGTH Y))) (AND (<= STR::XLEN STR::YLEN) (STR::STRPREFIXP-IMPL X Y 0 (- STR::YLEN STR::XLEN) STR::XLEN STR::YLEN))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUFFIXP))) (LOCAL (DEFTHM STR::C0 (IMPLIES (AND (NATP N) (<= (LEN X) N) (TRUE-LISTP X)) (EQUAL (NTHCDR N X) NIL)))) (LOCAL (DEFTHM STR::C1 (IMPLIES (TRUE-LISTP X) (NOT (NTHCDR (LEN X) X))))) (DEFTHM STR::STRSUFFIXP-OF-EMPTY (STR::STRSUFFIXP "" Y)) (LOCAL (PROGN (ASSERT! (STR::STRSUFFIXP "" "")) (ASSERT! (STR::STRSUFFIXP "" "foo")) (ASSERT! (STR::STRSUFFIXP "o" "foo")) (ASSERT! (STR::STRSUFFIXP "oo" "foo")) (ASSERT! (NOT (STR::STRSUFFIXP "ooo" "foo"))) (ASSERT! (NOT (STR::STRSUFFIXP "fo" "foo"))) (ASSERT! (STR::STRSUFFIXP "foo" "foo")))) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 1) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 2))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STRSUFFIXP (X Y) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (LET* ((STR::XCHARS (EXPLODE X)) (STR::YCHARS (EXPLODE Y)) (STR::XLEN (LEN STR::XCHARS)) (STR::YLEN (LEN STR::YCHARS))) (AND (<= STR::XLEN STR::YLEN) (EQUAL (NTHCDR (- STR::YLEN STR::XLEN) (EXPLODE Y)) (EXPLODE X)))) :EXEC (LET* ((STR::XLEN (LENGTH X)) (STR::YLEN (LENGTH Y))) (AND (<= STR::XLEN STR::YLEN) (STR::STRPREFIXP-IMPL X Y 0 (- STR::YLEN STR::XLEN) STR::XLEN STR::YLEN))))) (LOCAL (IN-THEORY (ENABLE STR::STRSUFFIXP))) (LOCAL (DEFTHM STR::C0 (IMPLIES (AND (NATP N) (<= (LEN X) N) (TRUE-LISTP X)) (EQUAL (NTHCDR N X) NIL)))) (LOCAL (DEFTHM STR::C1 (IMPLIES (TRUE-LISTP X) (NOT (NTHCDR (LEN X) X))))) (DEFTHM STR::STRSUFFIXP-OF-EMPTY (STR::STRSUFFIXP "" Y)) (RECORD-EXPANSION (LOCAL (PROGN (ASSERT! (STR::STRSUFFIXP "" "")) (ASSERT! (STR::STRSUFFIXP "" "foo")) (ASSERT! (STR::STRSUFFIXP "o" "foo")) (ASSERT! (STR::STRSUFFIXP "oo" "foo")) (ASSERT! (NOT (STR::STRSUFFIXP "ooo" "foo"))) (ASSERT! (NOT (STR::STRSUFFIXP "fo" "foo"))) (ASSERT! (STR::STRSUFFIXP "foo" "foo")))) (LOCAL (VALUE-TRIPLE :ELIDED))) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 1) (DEFCONG STR::STREQV EQUAL (STR::STRSUFFIXP X Y) 2)))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STRSUFFIXP)) (XDOC::PARENTS (QUOTE (STR::SUBSTRINGS))) (XDOC::SHORT (QUOTE "Case-sensitive string suffix test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STRSUFFIXP))) 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 strsuffixp) determines if the string @('x') is a suffix of
the string @('y'), in a case-sensitive manner.</p>
<p>Logically, we ask whether @('|x| < |y|'), and whether</p>
@({
(equal (nthcdr (- |y| |x|) (explode x))
(explode y))
})
<p>But we use a more efficient implementation that avoids coercing the strings
into lists; basically we ask if the last @('|x|') characters of @('y') are
equal to @('x').</p>
<p>Corner case: we regard the empty string as a suffix of every other string.
That is, @('(strsuffixp \"\" x)') is always true.</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::STRSUFFIXP) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SUBSTRINGS) (:SHORT . "Case-sensitive string suffix test.") (:LONG . "<p>@(call strsuffixp) determines if the string @('x') is a suffix of
the string @('y'), in a case-sensitive manner.</p>
<p>Logically, we ask whether @('|x| < |y|'), and whether</p>
@({
(equal (nthcdr (- |y| |x|) (explode x))
(explode y))
})
<p>But we use a more efficient implementation that avoids coercing the strings
into lists; basically we ask if the last @('|x|') characters of @('y') are
equal to @('x').</p>
<p>Corner case: we regard the empty string as a suffix of every other string.
That is, @('(strsuffixp \"\" x)') is always true.</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|STRSUFFIXP$INLINE|)
@(def |STR|::|STRSUFFIXP-OF-EMPTY|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRSUFFIXP-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRSUFFIXP-2|)") (:FROM . "[books]/str/suffixp.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STRSUFFIXP)))))) (VALUE-TRIPLE (QUOTE STR::STRSUFFIXP))))))
(("/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/suffixp.lisp" "suffixp" "suffixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1217176423) (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/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))
1990341385
|