/usr/share/acl2-6.3/books/str/eqv.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 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (DEFSECTION STR::CHAREQV :PARENTS (STR::EQUIVALENCES) :SHORT "Case-sensitive character equivalence test." :LONG "<p>@(call chareqv) determines if @('x') and @('y') are equivalent when
interpreted as characters. That is, non-characters are first coerced to be the
NUL character (via @(see char-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see ichareqv) for a case-insensitive alternative.</p>" (DEFINLINED STR::CHAREQV (X Y) (DECLARE (XARGS :GUARD T)) (EQL (STR::CHAR-FIX X) (STR::CHAR-FIX Y))) (LOCAL (IN-THEORY (ENABLE STR::CHAREQV STR::CHAR-FIX CHAR<))) (DEFEQUIV STR::CHAREQV) (DEFTHM STR::CHAREQV-OF-CHAR-FIX (STR::CHAREQV (STR::CHAR-FIX X) X)) (DEFCONG STR::CHAREQV EQUAL (STR::CHAR-FIX X) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR-CODE X) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR< X Y) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR< X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAREQV)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::CHAREQV (X Y) (DECLARE (XARGS :GUARD T)) (EQL (STR::CHAR-FIX X) (STR::CHAR-FIX Y))) (LOCAL (IN-THEORY (ENABLE STR::CHAREQV STR::CHAR-FIX CHAR<))) (DEFEQUIV STR::CHAREQV) (DEFTHM STR::CHAREQV-OF-CHAR-FIX (STR::CHAREQV (STR::CHAR-FIX X) X)) (DEFCONG STR::CHAREQV EQUAL (STR::CHAR-FIX X) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR-CODE X) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR< X Y) 1) (DEFCONG STR::CHAREQV EQUAL (CHAR< X Y) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHAREQV)) (XDOC::PARENTS (QUOTE (STR::EQUIVALENCES))) (XDOC::SHORT (QUOTE "Case-sensitive character equivalence test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAREQV))) 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 chareqv) determines if @('x') and @('y') are equivalent when
interpreted as characters. That is, non-characters are first coerced to be the
NUL character (via @(see char-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see ichareqv) for a case-insensitive alternative.</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::CHAREQV) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::EQUIVALENCES) (:SHORT . "Case-sensitive character equivalence test.") (:LONG . "<p>@(call chareqv) determines if @('x') and @('y') are equivalent when
interpreted as characters. That is, non-characters are first coerced to be the
NUL character (via @(see char-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see ichareqv) for a case-insensitive alternative.</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|CHAREQV$INLINE|)
@(def |STR|::|CHAREQV-IS-AN-EQUIVALENCE|)
@(def |STR|::|CHAREQV-OF-CHAR-FIX|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-CHAR-FIX-1|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-CHAR-CODE-1|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-CHAR<-1|)
@(def |STR|::|CHAREQV-IMPLIES-EQUAL-CHAR<-2|)") (:FROM . "[books]/str/eqv.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHAREQV)))))) (VALUE-TRIPLE (QUOTE STR::CHAREQV))))) (7 RECORD-EXPANSION (DEFSECTION STR::CHAR<-ORDER-THMS :PARENTS (CHAR<) :SHORT "Basic ordering facts about @('char<')." (LOCAL (IN-THEORY (ENABLE CHAR<))) (DEFTHM STR::CHAR<-IRREFLEXIVE (EQUAL (CHAR< X X) NIL)) (DEFTHM STR::CHAR<-ANTISYMMETRIC (IMPLIES (CHAR< X Y) (NOT (CHAR< Y X)))) (DEFTHM STR::CHAR<-TRANSITIVE (IMPLIES (AND (CHAR< X Y) (CHAR< Y Z)) (CHAR< X Z))) (DEFTHM STR::CHAR<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (CHAR< X Y)) (NOT (CHAR< Y X))) (EQUAL (STR::CHAREQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV)))) (DEFTHM STR::CHAR<-TRICHOTOMY-STRONG (EQUAL (CHAR< X Y) (AND (NOT (STR::CHAREQV X Y)) (NOT (CHAR< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAR<-ORDER-THMS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE CHAR<))) (DEFTHM STR::CHAR<-IRREFLEXIVE (EQUAL (CHAR< X X) NIL)) (DEFTHM STR::CHAR<-ANTISYMMETRIC (IMPLIES (CHAR< X Y) (NOT (CHAR< Y X)))) (DEFTHM STR::CHAR<-TRANSITIVE (IMPLIES (AND (CHAR< X Y) (CHAR< Y Z)) (CHAR< X Z))) (DEFTHM STR::CHAR<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (CHAR< X Y)) (NOT (CHAR< Y X))) (EQUAL (STR::CHAREQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV)))) (DEFTHM STR::CHAR<-TRICHOTOMY-STRONG (EQUAL (CHAR< X Y) (AND (NOT (STR::CHAREQV X Y)) (NOT (CHAR< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHAR<-ORDER-THMS)) (XDOC::PARENTS (QUOTE (CHAR<))) (XDOC::SHORT (QUOTE "Basic ordering facts about @('char<').")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CHAR<-ORDER-THMS))) 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::CHAR<-ORDER-THMS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS CHAR<) (:SHORT . "Basic ordering facts about @('char<').") (:LONG . "
<h3>Definitions and Theorems</h3>@(def |STR|::|CHAR<-IRREFLEXIVE|)
@(def |STR|::|CHAR<-ANTISYMMETRIC|)
@(def |STR|::|CHAR<-TRANSITIVE|)
@(def |STR|::|CHAR<-TRICHOTOMY-WEAK|)
@(def |STR|::|CHAR<-TRICHOTOMY-STRONG|)") (:FROM . "[books]/str/eqv.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHAR<-ORDER-THMS)))))) (VALUE-TRIPLE (QUOTE STR::CHAR<-ORDER-THMS))))) (8 RECORD-EXPANSION (DEFSECTION STR::CHARLISTEQV :PARENTS (STR::EQUIVALENCES) :SHORT "Case-sensitive character-list equivalence test." :LONG "<p>@(call charlisteqv) determines if @('x') and @('y') are equivalent
when interpreted as character lists. That is, @('x') and @('y') must have the
same length and their elements must be @(see chareqv) to one another.</p>
<p>See also @(see icharlisteqv) for a case-insensitive alternative.</p>" (DEFUND STR::CHARLISTEQV (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (IF (CONSP X) (AND (CONSP Y) (STR::CHAREQV (CAR X) (CAR Y)) (STR::CHARLISTEQV (CDR X) (CDR Y))) (ATOM Y))) (LOCAL (IN-THEORY (ENABLE STR::CHARLISTEQV))) (DEFEQUIV STR::CHARLISTEQV) (DEFREFINEMENT LIST-EQUIV STR::CHARLISTEQV :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV)))) (DEFCONG STR::CHARLISTEQV STR::CHAREQV (CAR X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (CDR X) 1) (DEFCONG STR::CHAREQV STR::CHARLISTEQV (CONS A X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (CONS A X) 2) (DEFCONG STR::CHARLISTEQV EQUAL (LEN X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (LIST-FIX X) 1) (DEFCONG STR::CHARLISTEQV STR::CHAREQV (NTH N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (TAKE N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (NTHCDR N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (APPEND X Y) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (APPEND X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REV X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REVAPPEND X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REVAPPEND X Y) 1) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCT (X Y) (IF (ATOM X) (LIST X Y) (STR::MY-INDUCT (CDR X) (CDR Y))))) (DEFCONG STR::CHARLISTEQV EQUAL (MAKE-CHARACTER-LIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV) :INDUCT (STR::MY-INDUCT X STR::X-EQUIV))))) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCT (X Y) (IF (ATOM X) (LIST X Y) (STR::MY-INDUCT (CDR X) (CDR Y))))) (LOCAL (DEFTHM STR::CROCK (EQUAL (STR::CHARLISTEQV X Y) (EQUAL (MAKE-CHARACTER-LIST X) (MAKE-CHARACTER-LIST Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV) :INDUCT (STR::MY-INDUCT X Y))))) (DEFCONG STR::CHARLISTEQV EQUAL (IMPLODE X) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::IMPLODE-OF-MAKE-CHARACTER-LIST) :USE ((:INSTANCE STR::IMPLODE-OF-MAKE-CHARACTER-LIST (X X)) (:INSTANCE STR::IMPLODE-OF-MAKE-CHARACTER-LIST (X STR::X-EQUIV))))))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-CONSP-LEFT (IMPLIES (NOT (CONSP X)) (EQUAL (STR::CHARLISTEQV X Y) (ATOM Y)))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-CONSP-RIGHT (IMPLIES (NOT (CONSP Y)) (EQUAL (STR::CHARLISTEQV X Y) (ATOM X)))) (DEFTHM STR::CHARLISTEQV-OF-CONS-RIGHT (EQUAL (STR::CHARLISTEQV X (CONS A Y)) (AND (CONSP X) (STR::CHAREQV (CAR X) (DOUBLE-REWRITE A)) (STR::CHARLISTEQV (CDR X) (DOUBLE-REWRITE Y))))) (DEFTHM STR::CHARLISTEQV-OF-CONS-LEFT (EQUAL (STR::CHARLISTEQV (CONS A X) Y) (AND (CONSP Y) (STR::CHAREQV (DOUBLE-REWRITE A) (CAR Y)) (STR::CHARLISTEQV (DOUBLE-REWRITE X) (CDR Y))))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-SAME-LENS (IMPLIES (NOT (EQUAL (LEN X) (LEN Y))) (NOT (STR::CHARLISTEQV X Y))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::CHARLISTEQV)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::CHARLISTEQV (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (IF (CONSP X) (AND (CONSP Y) (STR::CHAREQV (CAR X) (CAR Y)) (STR::CHARLISTEQV (CDR X) (CDR Y))) (ATOM Y))) (LOCAL (IN-THEORY (ENABLE STR::CHARLISTEQV))) (DEFEQUIV STR::CHARLISTEQV) (DEFREFINEMENT LIST-EQUIV STR::CHARLISTEQV :HINTS (("Goal" :IN-THEORY (ENABLE LIST-EQUIV)))) (DEFCONG STR::CHARLISTEQV STR::CHAREQV (CAR X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (CDR X) 1) (DEFCONG STR::CHAREQV STR::CHARLISTEQV (CONS A X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (CONS A X) 2) (DEFCONG STR::CHARLISTEQV EQUAL (LEN X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (LIST-FIX X) 1) (DEFCONG STR::CHARLISTEQV STR::CHAREQV (NTH N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (TAKE N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (NTHCDR N X) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (APPEND X Y) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (APPEND X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REV X) 1) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REVAPPEND X Y) 2) (DEFCONG STR::CHARLISTEQV STR::CHARLISTEQV (REVAPPEND X Y) 1) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCT (X Y) (IF (ATOM X) (LIST X Y) (STR::MY-INDUCT (CDR X) (CDR Y))))) (DEFCONG STR::CHARLISTEQV EQUAL (MAKE-CHARACTER-LIST X) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV) :INDUCT (STR::MY-INDUCT X STR::X-EQUIV))))) (ENCAPSULATE NIL (LOCAL (DEFUN STR::MY-INDUCT (X Y) (IF (ATOM X) (LIST X Y) (STR::MY-INDUCT (CDR X) (CDR Y))))) (LOCAL (DEFTHM STR::CROCK (EQUAL (STR::CHARLISTEQV X Y) (EQUAL (MAKE-CHARACTER-LIST X) (MAKE-CHARACTER-LIST Y))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::CHAREQV) :INDUCT (STR::MY-INDUCT X Y))))) (DEFCONG STR::CHARLISTEQV EQUAL (IMPLODE X) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::IMPLODE-OF-MAKE-CHARACTER-LIST) :USE ((:INSTANCE STR::IMPLODE-OF-MAKE-CHARACTER-LIST (X X)) (:INSTANCE STR::IMPLODE-OF-MAKE-CHARACTER-LIST (X STR::X-EQUIV))))))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-CONSP-LEFT (IMPLIES (NOT (CONSP X)) (EQUAL (STR::CHARLISTEQV X Y) (ATOM Y)))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-CONSP-RIGHT (IMPLIES (NOT (CONSP Y)) (EQUAL (STR::CHARLISTEQV X Y) (ATOM X)))) (DEFTHM STR::CHARLISTEQV-OF-CONS-RIGHT (EQUAL (STR::CHARLISTEQV X (CONS A Y)) (AND (CONSP X) (STR::CHAREQV (CAR X) (DOUBLE-REWRITE A)) (STR::CHARLISTEQV (CDR X) (DOUBLE-REWRITE Y))))) (DEFTHM STR::CHARLISTEQV-OF-CONS-LEFT (EQUAL (STR::CHARLISTEQV (CONS A X) Y) (AND (CONSP Y) (STR::CHAREQV (DOUBLE-REWRITE A) (CAR Y)) (STR::CHARLISTEQV (DOUBLE-REWRITE X) (CDR Y))))) (DEFTHM STR::CHARLISTEQV-WHEN-NOT-SAME-LENS (IMPLIES (NOT (EQUAL (LEN X) (LEN Y))) (NOT (STR::CHARLISTEQV X Y)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::CHARLISTEQV)) (XDOC::PARENTS (QUOTE (STR::EQUIVALENCES))) (XDOC::SHORT (QUOTE "Case-sensitive character-list equivalence test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::CHARLISTEQV))) 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 charlisteqv) determines if @('x') and @('y') are equivalent
when interpreted as character lists. That is, @('x') and @('y') must have the
same length and their elements must be @(see chareqv) to one another.</p>
<p>See also @(see icharlisteqv) for a case-insensitive alternative.</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::CHARLISTEQV) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::EQUIVALENCES) (:SHORT . "Case-sensitive character-list equivalence test.") (:LONG . "<p>@(call charlisteqv) determines if @('x') and @('y') are equivalent
when interpreted as character lists. That is, @('x') and @('y') must have the
same length and their elements must be @(see chareqv) to one another.</p>
<p>See also @(see icharlisteqv) for a case-insensitive alternative.</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|CHARLISTEQV|)
@(def |STR|::|CHARLISTEQV-IS-AN-EQUIVALENCE|)
@(def |ACL2|::|LIST-EQUIV-REFINES-CHARLISTEQV|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHAREQV-CAR-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-CDR-1|)
@(def |STR|::|CHAREQV-IMPLIES-CHARLISTEQV-CONS-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-CONS-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-LEN-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-LIST-FIX-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHAREQV-NTH-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-TAKE-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-NTHCDR-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-APPEND-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-APPEND-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-REV-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-REVAPPEND-2|)
@(def |STR|::|CHARLISTEQV-IMPLIES-CHARLISTEQV-REVAPPEND-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-MAKE-CHARACTER-LIST-1|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-IMPLODE-1|)
@(def |STR|::|CHARLISTEQV-WHEN-NOT-CONSP-LEFT|)
@(def |STR|::|CHARLISTEQV-WHEN-NOT-CONSP-RIGHT|)
@(def |STR|::|CHARLISTEQV-OF-CONS-RIGHT|)
@(def |STR|::|CHARLISTEQV-OF-CONS-LEFT|)
@(def |STR|::|CHARLISTEQV-WHEN-NOT-SAME-LENS|)") (:FROM . "[books]/str/eqv.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::CHARLISTEQV)))))) (VALUE-TRIPLE (QUOTE STR::CHARLISTEQV))))) (9 RECORD-EXPANSION (DEFSECTION STR::STR-FIX :PARENTS (STR::EQUIVALENCES) :SHORT "Coerce to a string." :LONG "<p>@(call str-fix) is the identity on @(see acl2::stringp)s, or
returns the empty string, @('\"\"'), for any non-string.</p>
<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see streqv).</p>" (DEFINLINED STR::STR-FIX (X) (DECLARE (XARGS :GUARD T)) (IF (STRINGP X) X "")) (LOCAL (IN-THEORY (ENABLE STR::STR-FIX))) (DEFTHM STR::STR-FIX-DEFAULT (IMPLIES (NOT (STRINGP X)) (EQUAL (STR::STR-FIX X) ""))) (DEFTHM STR::STR-FIX-WHEN-STRINGP (IMPLIES (STRINGP X) (EQUAL (STR::STR-FIX X) X)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STR-FIX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STR-FIX (X) (DECLARE (XARGS :GUARD T)) (IF (STRINGP X) X "")) (LOCAL (IN-THEORY (ENABLE STR::STR-FIX))) (DEFTHM STR::STR-FIX-DEFAULT (IMPLIES (NOT (STRINGP X)) (EQUAL (STR::STR-FIX X) ""))) (DEFTHM STR::STR-FIX-WHEN-STRINGP (IMPLIES (STRINGP X) (EQUAL (STR::STR-FIX X) X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STR-FIX)) (XDOC::PARENTS (QUOTE (STR::EQUIVALENCES))) (XDOC::SHORT (QUOTE "Coerce to a string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STR-FIX))) 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 str-fix) is the identity on @(see acl2::stringp)s, or
returns the empty string, @('\"\"'), for any non-string.</p>
<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see streqv).</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::STR-FIX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::EQUIVALENCES) (:SHORT . "Coerce to a string.") (:LONG . "<p>@(call str-fix) is the identity on @(see acl2::stringp)s, or
returns the empty string, @('\"\"'), for any non-string.</p>
<p>This is similar to other fixing functions like @(see fix) and @(see nfix).
See also @(see streqv).</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|STR-FIX$INLINE|)
@(def |STR|::|STR-FIX-DEFAULT|)
@(def |STR|::|STR-FIX-WHEN-STRINGP|)") (:FROM . "[books]/str/eqv.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STR-FIX)))))) (VALUE-TRIPLE (QUOTE STR::STR-FIX))))) (10 RECORD-EXPANSION (DEFSECTION STR::STREQV :PARENTS (STR::EQUIVALENCES) :SHORT "Case-sensitive string equivalence test." :LONG "<p>@(call streqv) determines if @('x') and @('y') are equivalent when
interpreted as strings. That is, non-strings are first coerced to be the empty
string (via @(see str-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see istreqv) for a case-insensitive alternative.</p>" (DEFINLINED STR::STREQV (X Y) (DECLARE (XARGS :GUARD T)) (EQUAL (STR::STR-FIX X) (STR::STR-FIX Y))) (LOCAL (IN-THEORY (ENABLE STR::STREQV STR::STR-FIX))) (DEFEQUIV STR::STREQV) (DEFTHM STR::STREQV-OF-STR-FIX (STR::STREQV (STR::STR-FIX X) X)) (DEFCONG STR::STREQV EQUAL (CHAR X N) 1) (DEFCONG STR::STREQV EQUAL (EXPLODE X) 1) (DEFCONG STR::STREQV EQUAL (STRING-APPEND X Y) 1) (DEFCONG STR::STREQV EQUAL (STRING-APPEND X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::STREQV)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::STREQV (X Y) (DECLARE (XARGS :GUARD T)) (EQUAL (STR::STR-FIX X) (STR::STR-FIX Y))) (LOCAL (IN-THEORY (ENABLE STR::STREQV STR::STR-FIX))) (DEFEQUIV STR::STREQV) (DEFTHM STR::STREQV-OF-STR-FIX (STR::STREQV (STR::STR-FIX X) X)) (DEFCONG STR::STREQV EQUAL (CHAR X N) 1) (DEFCONG STR::STREQV EQUAL (EXPLODE X) 1) (DEFCONG STR::STREQV EQUAL (STRING-APPEND X Y) 1) (DEFCONG STR::STREQV EQUAL (STRING-APPEND X Y) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::STREQV)) (XDOC::PARENTS (QUOTE (STR::EQUIVALENCES))) (XDOC::SHORT (QUOTE "Case-sensitive string equivalence test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::STREQV))) 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 streqv) determines if @('x') and @('y') are equivalent when
interpreted as strings. That is, non-strings are first coerced to be the empty
string (via @(see str-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see istreqv) for a case-insensitive alternative.</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::STREQV) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::EQUIVALENCES) (:SHORT . "Case-sensitive string equivalence test.") (:LONG . "<p>@(call streqv) determines if @('x') and @('y') are equivalent when
interpreted as strings. That is, non-strings are first coerced to be the empty
string (via @(see str-fix)), then we see if these coerced arguments are
equal.</p>
<p>See also @(see istreqv) for a case-insensitive alternative.</p>
<h3>Definitions and Theorems</h3>@(def |STR|::|STREQV$INLINE|)
@(def |STR|::|STREQV-IS-AN-EQUIVALENCE|)
@(def |STR|::|STREQV-OF-STR-FIX|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-CHAR-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-EXPLODE-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRING-APPEND-1|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-STRING-APPEND-2|)") (:FROM . "[books]/str/eqv.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::STREQV)))))) (VALUE-TRIPLE (QUOTE STR::STREQV))))))
(("/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/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))
104748885
|