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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (DEFSECTION STR::ICHAR< :PARENTS (STR::ORDERING) :SHORT "Case-insensitive character less-than test." :LONG "<p>@(call ichar<) determines if @('x') is \"smaller\" than @('y'), but
ignoring case.  Our approach is basically to downcase upper-case letters and
then compare the resulting character codes.</p>

<p>Something subtle about this is that, in the ASCII character ordering, the
upper-case characters do not immediately preceede the lower-case ones.  That
is, upper-case Z is at 90, but lower-case a does not start until 97.  So, in
our approach, the 6 intervening characters (the square brackets, backslash,
hat, underscore, and backtick) are considered \"smaller\" than letters, even
though in regular ASCII ordering they are \"larger\" than the upper-case
letters.</p>" (DEFINLINED STR::ICHAR< (X Y) (DECLARE (TYPE CHARACTER X) (TYPE CHARACTER Y) (XARGS :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-CHAR))))) (MBE :LOGIC (< (CHAR-CODE (STR::DOWNCASE-CHAR X)) (CHAR-CODE (STR::DOWNCASE-CHAR Y))) :EXEC (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X)))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER Y)))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX))))) (LOCAL (IN-THEORY (ENABLE STR::ICHAR<))) (DEFTHM STR::ICHAR<-IRREFLEXIVE (NOT (STR::ICHAR< X X))) (DEFTHM STR::ICHAR<-ANTISYMMETRIC (IMPLIES (STR::ICHAR< X Y) (NOT (STR::ICHAR< Y X)))) (DEFTHM STR::ICHAR<-TRANSITIVE (IMPLIES (AND (STR::ICHAR< X Y) (STR::ICHAR< Y Z)) (STR::ICHAR< X Z))) (DEFTHM STR::ICHAR<-TRANSITIVE-TWO (IMPLIES (AND (STR::ICHAR< Y Z) (STR::ICHAR< X Y)) (STR::ICHAR< X Z))) (DEFTHM STR::ICHAR<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::ICHAR< X Y)) (NOT (STR::ICHAR< Y X))) (EQUAL (STR::ICHAREQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFCONG STR::ICHAREQV EQUAL (STR::ICHAR< X Y) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFCONG STR::ICHAREQV EQUAL (STR::ICHAR< X Y) 2 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::ICHAR<-TRICHOTOMY-STRONG (EQUAL (STR::ICHAR< X Y) (AND (NOT (STR::ICHAREQV X Y)) (NOT (STR::ICHAR< Y X)))) :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX) (STR::ICHAR<-TRICHOTOMY-WEAK)) :USE ((:INSTANCE STR::ICHAR<-TRICHOTOMY-WEAK)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::ICHAR<)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFINLINED STR::ICHAR< (X Y) (DECLARE (TYPE CHARACTER X) (TYPE CHARACTER Y) (XARGS :GUARD-HINTS (("Goal" :IN-THEORY (ENABLE STR::DOWNCASE-CHAR))))) (MBE :LOGIC (< (CHAR-CODE (STR::DOWNCASE-CHAR X)) (CHAR-CODE (STR::DOWNCASE-CHAR Y))) :EXEC (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X)))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER Y)))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX))))) (LOCAL (IN-THEORY (ENABLE STR::ICHAR<))) (DEFTHM STR::ICHAR<-IRREFLEXIVE (NOT (STR::ICHAR< X X))) (DEFTHM STR::ICHAR<-ANTISYMMETRIC (IMPLIES (STR::ICHAR< X Y) (NOT (STR::ICHAR< Y X)))) (DEFTHM STR::ICHAR<-TRANSITIVE (IMPLIES (AND (STR::ICHAR< X Y) (STR::ICHAR< Y Z)) (STR::ICHAR< X Z))) (DEFTHM STR::ICHAR<-TRANSITIVE-TWO (IMPLIES (AND (STR::ICHAR< Y Z) (STR::ICHAR< X Y)) (STR::ICHAR< X Z))) (DEFTHM STR::ICHAR<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::ICHAR< X Y)) (NOT (STR::ICHAR< Y X))) (EQUAL (STR::ICHAREQV X Y) T)) :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFCONG STR::ICHAREQV EQUAL (STR::ICHAR< X Y) 1 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFCONG STR::ICHAREQV EQUAL (STR::ICHAR< X Y) 2 :HINTS (("Goal" :IN-THEORY (ENABLE STR::ICHAR< STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX)))) (DEFTHM STR::ICHAR<-TRICHOTOMY-STRONG (EQUAL (STR::ICHAR< X Y) (AND (NOT (STR::ICHAREQV X Y)) (NOT (STR::ICHAR< Y X)))) :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAREQV STR::DOWNCASE-CHAR STR::CHAR-FIX) (STR::ICHAR<-TRICHOTOMY-WEAK)) :USE ((:INSTANCE STR::ICHAR<-TRICHOTOMY-WEAK)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::ICHAR<)) (XDOC::PARENTS (QUOTE (STR::ORDERING))) (XDOC::SHORT (QUOTE "Case-insensitive character less-than test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::ICHAR<))) 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 ichar<) determines if @('x') is \"smaller\" than @('y'), but
ignoring case.  Our approach is basically to downcase upper-case letters and
then compare the resulting character codes.</p>

<p>Something subtle about this is that, in the ASCII character ordering, the
upper-case characters do not immediately preceede the lower-case ones.  That
is, upper-case Z is at 90, but lower-case a does not start until 97.  So, in
our approach, the 6 intervening characters (the square brackets, backslash,
hat, underscore, and backtick) are considered \"smaller\" than letters, even
though in regular ASCII ordering they are \"larger\" than the upper-case
letters.</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::ICHAR<) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::ORDERING) (:SHORT . "Case-insensitive character less-than test.") (:LONG . "<p>@(call ichar<) determines if @('x') is \"smaller\" than @('y'), but
ignoring case.  Our approach is basically to downcase upper-case letters and
then compare the resulting character codes.</p>

<p>Something subtle about this is that, in the ASCII character ordering, the
upper-case characters do not immediately preceede the lower-case ones.  That
is, upper-case Z is at 90, but lower-case a does not start until 97.  So, in
our approach, the 6 intervening characters (the square brackets, backslash,
hat, underscore, and backtick) are considered \"smaller\" than letters, even
though in regular ASCII ordering they are \"larger\" than the upper-case
letters.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|ICHAR<$INLINE|)
@(def |STR|::|ICHAR<-IRREFLEXIVE|)
@(def |STR|::|ICHAR<-ANTISYMMETRIC|)
@(def |STR|::|ICHAR<-TRANSITIVE|)
@(def |STR|::|ICHAR<-TRANSITIVE-TWO|)
@(def |STR|::|ICHAR<-TRICHOTOMY-WEAK|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-ICHAR<-1|)
@(def |STR|::|ICHAREQV-IMPLIES-EQUAL-ICHAR<-2|)
@(def |STR|::|ICHAR<-TRICHOTOMY-STRONG|)") (:FROM . "[books]/str/iless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::ICHAR<)))))) (VALUE-TRIPLE (QUOTE STR::ICHAR<))))) (5 RECORD-EXPANSION (DEFSECTION STR::ICHARLIST< :PARENTS (STR::ORDERING) :SHORT "Case-insensitive character-list less-than test." :LONG "<p>@(call icharlist<) determines whether the character list @('x')
preceeds @('y') in alphabetical order without regards to case.  The characters
are compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</p>" (DEFUND STR::ICHARLIST< (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM Y) NIL) ((ATOM X) T) ((STR::ICHAR< (CAR X) (CAR Y)) T) ((STR::ICHAR< (CAR Y) (CAR X)) NIL) (T (STR::ICHARLIST< (CDR X) (CDR Y)))) :EXEC (COND ((ATOM Y) NIL) ((ATOM X) T) (T (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X))))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR Y))))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (COND ((< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX)) T) ((< (THE (UNSIGNED-BYTE 8) STR::YC-FIX) (THE (UNSIGNED-BYTE 8) STR::XC-FIX)) NIL) (T (STR::ICHARLIST< (CDR X) (CDR Y))))))))) (LOCAL (IN-THEORY (ENABLE STR::ICHARLIST<))) (VERIFY-GUARDS STR::ICHARLIST< :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAR< STR::DOWNCASE-CHAR) (STR::ICHAR<-TRICHOTOMY-STRONG))))) (DEFTHM STR::ICHARLIST<-IRREFLEXIVE (EQUAL (STR::ICHARLIST< X X) NIL)) (DEFTHM STR::ICHARLIST<-ANTISYMMETRIC (IMPLIES (STR::ICHARLIST< X Y) (NOT (STR::ICHARLIST< Y X)))) (DEFTHM STR::ICHARLIST<-TRANSITIVE (IMPLIES (AND (STR::ICHARLIST< X Y) (STR::ICHARLIST< Y Z)) (STR::ICHARLIST< X Z))) (DEFTHM STR::ICHARLIST<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::ICHARLIST< X Y)) (NOT (STR::ICHARLIST< Y X))) (EQUAL (STR::ICHARLISTEQV X Y) T))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::ICHARLIST< X Y) 1) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::ICHARLIST< X Y) 2) (DEFTHM STR::ICHARLIST<-TRICHOTOMY-STRONG (EQUAL (STR::ICHARLIST< X Y) (AND (NOT (STR::ICHARLISTEQV X Y)) (NOT (STR::ICHARLIST< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::ICHARLIST<)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::ICHARLIST< (X Y) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)) :VERIFY-GUARDS NIL)) (MBE :LOGIC (COND ((ATOM Y) NIL) ((ATOM X) T) ((STR::ICHAR< (CAR X) (CAR Y)) T) ((STR::ICHAR< (CAR Y) (CAR X)) NIL) (T (STR::ICHARLIST< (CDR X) (CDR Y)))) :EXEC (COND ((ATOM Y) NIL) ((ATOM X) T) (T (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X))))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR Y))))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (COND ((< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX)) T) ((< (THE (UNSIGNED-BYTE 8) STR::YC-FIX) (THE (UNSIGNED-BYTE 8) STR::XC-FIX)) NIL) (T (STR::ICHARLIST< (CDR X) (CDR Y))))))))) (LOCAL (IN-THEORY (ENABLE STR::ICHARLIST<))) (VERIFY-GUARDS STR::ICHARLIST< :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAR< STR::DOWNCASE-CHAR) (STR::ICHAR<-TRICHOTOMY-STRONG))))) (DEFTHM STR::ICHARLIST<-IRREFLEXIVE (EQUAL (STR::ICHARLIST< X X) NIL)) (DEFTHM STR::ICHARLIST<-ANTISYMMETRIC (IMPLIES (STR::ICHARLIST< X Y) (NOT (STR::ICHARLIST< Y X)))) (DEFTHM STR::ICHARLIST<-TRANSITIVE (IMPLIES (AND (STR::ICHARLIST< X Y) (STR::ICHARLIST< Y Z)) (STR::ICHARLIST< X Z))) (DEFTHM STR::ICHARLIST<-TRICHOTOMY-WEAK (IMPLIES (AND (NOT (STR::ICHARLIST< X Y)) (NOT (STR::ICHARLIST< Y X))) (EQUAL (STR::ICHARLISTEQV X Y) T))) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::ICHARLIST< X Y) 1) (DEFCONG STR::ICHARLISTEQV EQUAL (STR::ICHARLIST< X Y) 2) (DEFTHM STR::ICHARLIST<-TRICHOTOMY-STRONG (EQUAL (STR::ICHARLIST< X Y) (AND (NOT (STR::ICHARLISTEQV X Y)) (NOT (STR::ICHARLIST< Y X)))) :RULE-CLASSES ((:REWRITE :LOOP-STOPPER ((X Y))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::ICHARLIST<)) (XDOC::PARENTS (QUOTE (STR::ORDERING))) (XDOC::SHORT (QUOTE "Case-insensitive character-list less-than test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::ICHARLIST<))) 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 icharlist<) determines whether the character list @('x')
preceeds @('y') in alphabetical order without regards to case.  The characters
are compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</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::ICHARLIST<) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::ORDERING) (:SHORT . "Case-insensitive character-list less-than test.") (:LONG . "<p>@(call icharlist<) determines whether the character list @('x')
preceeds @('y') in alphabetical order without regards to case.  The characters
are compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|ICHARLIST<|)
@(def |STR|::|ICHARLIST<-IRREFLEXIVE|)
@(def |STR|::|ICHARLIST<-ANTISYMMETRIC|)
@(def |STR|::|ICHARLIST<-TRANSITIVE|)
@(def |STR|::|ICHARLIST<-TRICHOTOMY-WEAK|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-ICHARLIST<-1|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-EQUAL-ICHARLIST<-2|)
@(def |STR|::|ICHARLIST<-TRICHOTOMY-STRONG|)") (:FROM . "[books]/str/iless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::ICHARLIST<)))))) (VALUE-TRIPLE (QUOTE STR::ICHARLIST<))))) (6 RECORD-EXPANSION (DEFSECTION STR::ISTR< :PARENTS (STR::ORDERING) :SHORT "Case-insensitive string less-than test." :LONG "<p>@(call icharlist<) determines whether the string @('x') preceeds
@('y') in alphabetical order without regards to case.  The characters are
compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</p>

<p>Logically, this is identical to:</p>

@({
  (icharlist< (explode x) (explode y))
})

<p>But we use a more efficient implementation which avoids coercing the strings
into lists.</p>

<p>NOTE: for reasoning, we leave this function enabled and prefer to work with
@(see icharlist<) of the explodes as our normal form.</p>" (DEFUND STR::ISTR<-AUX (X Y N STR::XL STR::YL) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP N) (<= N (LENGTH X)) (<= N (LENGTH Y)) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y))) :VERIFY-GUARDS NIL :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (MBE :LOGIC (COND ((ZP (- (NFIX STR::YL) (NFIX N))) NIL) ((ZP (- (NFIX STR::XL) (NFIX N))) T) ((STR::ICHAR< (CHAR X N) (CHAR Y N)) T) ((STR::ICHAR< (CHAR Y N) (CHAR X N)) NIL) (T (STR::ISTR<-AUX X Y (+ (NFIX N) 1) STR::XL STR::YL))) :EXEC (COND ((= (THE INTEGER N) (THE INTEGER STR::YL)) NIL) ((= (THE INTEGER N) (THE INTEGER STR::XL)) T) (T (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING X) (THE INTEGER N)))))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING Y) (THE INTEGER N)))))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (COND ((< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX)) T) ((< (THE (UNSIGNED-BYTE 8) STR::YC-FIX) (THE (UNSIGNED-BYTE 8) STR::XC-FIX)) NIL) (T (STR::ISTR<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER N) 1)) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))))))) (DEFINLINE STR::ISTR< (X Y) (DECLARE (TYPE STRING X) (TYPE STRING Y) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (STR::ICHARLIST< (EXPLODE X) (EXPLODE Y)) :EXEC (STR::ISTR<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (LOCAL (DEFTHM STR::CROCK (EQUAL (< A A) NIL))) (LOCAL (DEFTHM STR::CROCK2 (IMPLIES (< A B) (EQUAL (< B A) NIL)))) (VERIFY-GUARDS STR::ISTR<-AUX :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAR< STR::DOWNCASE-CHAR))))) (DEFTHM STR::ISTR<-AUX-CORRECT (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP N) (<= N (LENGTH X)) (<= N (LENGTH Y)) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y))) (EQUAL (STR::ISTR<-AUX X Y N STR::XL STR::YL) (STR::ICHARLIST< (NTHCDR N (COERCE X (QUOTE LIST))) (NTHCDR N (COERCE Y (QUOTE LIST)))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::ISTR<-AUX STR::ICHARLIST<)))) (VERIFY-GUARDS STR::ISTR<$INLINE) (DEFCONG STR::ISTREQV EQUAL (STR::ISTR< X Y) 1) (DEFCONG STR::ISTREQV EQUAL (STR::ISTR< X Y) 2)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::ISTR<)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::ISTR<-AUX (X Y N STR::XL STR::YL) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP N) (<= N (LENGTH X)) (<= N (LENGTH Y)) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y))) :VERIFY-GUARDS NIL :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N))))) (MBE :LOGIC (COND ((ZP (- (NFIX STR::YL) (NFIX N))) NIL) ((ZP (- (NFIX STR::XL) (NFIX N))) T) ((STR::ICHAR< (CHAR X N) (CHAR Y N)) T) ((STR::ICHAR< (CHAR Y N) (CHAR X N)) NIL) (T (STR::ISTR<-AUX X Y (+ (NFIX N) 1) STR::XL STR::YL))) :EXEC (COND ((= (THE INTEGER N) (THE INTEGER STR::YL)) NIL) ((= (THE INTEGER N) (THE INTEGER STR::XL)) T) (T (LET* ((STR::XC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING X) (THE INTEGER N)))))) (STR::YC (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING Y) (THE INTEGER N)))))) (STR::XC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::XC)) (<= (THE (UNSIGNED-BYTE 8) STR::XC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::XC) 32)) (THE (UNSIGNED-BYTE 8) STR::XC))) (STR::YC-FIX (IF (AND (<= (STR::BIG-A) (THE (UNSIGNED-BYTE 8) STR::YC)) (<= (THE (UNSIGNED-BYTE 8) STR::YC) (STR::BIG-Z))) (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) STR::YC) 32)) (THE (UNSIGNED-BYTE 8) STR::YC)))) (COND ((< (THE (UNSIGNED-BYTE 8) STR::XC-FIX) (THE (UNSIGNED-BYTE 8) STR::YC-FIX)) T) ((< (THE (UNSIGNED-BYTE 8) STR::YC-FIX) (THE (UNSIGNED-BYTE 8) STR::XC-FIX)) NIL) (T (STR::ISTR<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER N) 1)) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))))))) (DEFINLINE STR::ISTR< (X Y) (DECLARE (TYPE STRING X) (TYPE STRING Y) (XARGS :VERIFY-GUARDS NIL)) (MBE :LOGIC (STR::ICHARLIST< (EXPLODE X) (EXPLODE Y)) :EXEC (STR::ISTR<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (LOCAL (DEFTHM STR::CROCK (EQUAL (< A A) NIL))) (LOCAL (DEFTHM STR::CROCK2 (IMPLIES (< A B) (EQUAL (< B A) NIL)))) (VERIFY-GUARDS STR::ISTR<-AUX :HINTS (("Goal" :IN-THEORY (E/D (STR::ICHAR< STR::DOWNCASE-CHAR))))) (DEFTHM STR::ISTR<-AUX-CORRECT (IMPLIES (AND (STRINGP X) (STRINGP Y) (NATP N) (<= N (LENGTH X)) (<= N (LENGTH Y)) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y))) (EQUAL (STR::ISTR<-AUX X Y N STR::XL STR::YL) (STR::ICHARLIST< (NTHCDR N (COERCE X (QUOTE LIST))) (NTHCDR N (COERCE Y (QUOTE LIST)))))) :HINTS (("Goal" :IN-THEORY (ENABLE STR::ISTR<-AUX STR::ICHARLIST<)))) (VERIFY-GUARDS STR::ISTR<$INLINE) (DEFCONG STR::ISTREQV EQUAL (STR::ISTR< X Y) 1) (DEFCONG STR::ISTREQV EQUAL (STR::ISTR< X Y) 2))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::ISTR<)) (XDOC::PARENTS (QUOTE (STR::ORDERING))) (XDOC::SHORT (QUOTE "Case-insensitive string less-than test.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::ISTR<))) 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 icharlist<) determines whether the string @('x') preceeds
@('y') in alphabetical order without regards to case.  The characters are
compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</p>

<p>Logically, this is identical to:</p>

@({
  (icharlist< (explode x) (explode y))
})

<p>But we use a more efficient implementation which avoids coercing the strings
into lists.</p>

<p>NOTE: for reasoning, we leave this function enabled and prefer to work with
@(see icharlist<) of the explodes as our normal form.</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::ISTR<) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::ORDERING) (:SHORT . "Case-insensitive string less-than test.") (:LONG . "<p>@(call icharlist<) determines whether the string @('x') preceeds
@('y') in alphabetical order without regards to case.  The characters are
compared with @(see ichar<) and shorter strings are considered smaller than
longer strings.</p>

<p>Logically, this is identical to:</p>

@({
  (icharlist< (explode x) (explode y))
})

<p>But we use a more efficient implementation which avoids coercing the strings
into lists.</p>

<p>NOTE: for reasoning, we leave this function enabled and prefer to work with
@(see icharlist<) of the explodes as our normal form.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|ISTR<-AUX|)
@(def |STR|::|ISTR<$INLINE|)
@(def |STR|::|ISTR<-AUX-CORRECT|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-ISTR<-1|)
@(def |STR|::|ISTREQV-IMPLIES-EQUAL-ISTR<-2|)") (:FROM . "[books]/str/iless.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::ISTR<)))))) (VALUE-TRIPLE (QUOTE STR::ISTR<))))))
(("/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/iless.lisp" "iless" "iless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 267906057) ("/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))
104162687
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / iless.cert
