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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
(DEFPKG "U" (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) NIL ((:SYSTEM . "ihs/ihs-init.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp") (:SYSTEM . "defsort/generic-impl.lisp") (:SYSTEM . "defsort/generic.lisp") (:SYSTEM . "defsort/defsort.lisp") (:SYSTEM . "str/isort.lisp") (:SYSTEM . "str/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (MAKE-EVENT (CUTIL::DEFREDUNDANT-FN (QUOTE (EXPLODE$INLINE EXPLODE IMPLODE$INLINE IMPLODE STR::STRINGP-OF-IMPLODE STR::CHAR-FIX$INLINE STR::CHAR-FIX STR::CHAREQV$INLINE STR::CHAREQV STR::CHAREQV-IS-AN-EQUIVALENCE STR::CHARLISTEQV STR::CHARLISTEQV-IS-AN-EQUIVALENCE STR::STR-FIX$INLINE STR::STR-FIX STR::STREQV$INLINE STR::STREQV STR::STREQV-IS-AN-EQUIVALENCE STR::FAST-STRING-APPEND STR::FAST-STRING-APPEND-LST STR::FAST-CONCATENATE STR::CAT STR::APPEND-CHARS-AUX STR::APPEND-CHARS$INLINE STR::APPEND-CHARS STR::REVAPPEND-CHARS-AUX STR::REVAPPEND-CHARS$INLINE STR::REVAPPEND-CHARS STR::PREFIX-STRINGS STR::RCHARS-TO-STRING STR::JOIN-AUX STR::JOIN STR::LITTLE-A STR::LITTLE-Z STR::BIG-A STR::BIG-Z STR::CASE-DELTA STR::UP-ALPHA-P$INLINE STR::UP-ALPHA-P STR::DOWN-ALPHA-P$INLINE STR::DOWN-ALPHA-P STR::UPCASE-CHAR$INLINE STR::UPCASE-CHAR STR::DOWNCASE-CHAR$INLINE STR::DOWNCASE-CHAR STR::MAKE-UPCASE-FIRST-STRTBL STR::*UPCASE-FIRST-STRTBL* STR::UPCASE-CHAR-STR$INLINE STR::UPCASE-CHAR-STR STR::MAKE-DOWNCASE-FIRST-STRTBL STR::*DOWNCASE-FIRST-STRTBL* STR::DOWNCASE-CHAR-STR$INLINE STR::DOWNCASE-CHAR-STR STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P STR::UPCASE-CHARLIST-AUX STR::UPCASE-CHARLIST STR::CHARLIST-HAS-SOME-UP-ALPHA-P STR::DOWNCASE-CHARLIST-AUX STR::DOWNCASE-CHARLIST STR::STRING-HAS-SOME-DOWN-ALPHA-P STR::UPCASE-STRING-AUX STR::UPCASE-STRING STR::STRING-HAS-SOME-UP-ALPHA-P STR::DOWNCASE-STRING-AUX STR::DOWNCASE-STRING STR::UPCASE-STRING-LIST-AUX STR::UPCASE-STRING-LIST STR::DOWNCASE-STRING-LIST-AUX STR::DOWNCASE-STRING-LIST STR::UPCASE-FIRST-CHARLIST STR::UPCASE-FIRST STR::DOWNCASE-FIRST-CHARLIST STR::DOWNCASE-FIRST STR::ICHAREQV$INLINE STR::ICHAREQV STR::ICHAREQV-IS-AN-EQUIVALENCE STR::ICHARLISTEQV STR::ICHARLISTEQV-IS-AN-EQUIVALENCE STR::ISTREQV-AUX STR::ISTREQV$INLINE STR::ISTREQV STR::ISTREQV-IS-AN-EQUIVALENCE STR::DIGITP$INLINE STR::DIGITP STR::NONZERO-DIGITP$INLINE STR::NONZERO-DIGITP STR::DIGIT-VAL$INLINE STR::DIGIT-VAL STR::DIGIT-LISTP STR::DIGIT-LIST-VALUE STR::SKIP-LEADING-DIGITS STR::TAKE-LEADING-DIGITS STR::DIGIT-STRING-P-AUX STR::DIGIT-STRING-P$INLINE STR::DIGIT-STRING-P STR::FIRSTN-CHARS-AUX STR::FIRSTN-CHARS STR::APPEND-FIRSTN-CHARS STR::HTML-SPACE STR::HTML-NEWLINE STR::HTML-LESS STR::HTML-GREATER STR::HTML-AMP STR::HTML-QUOTE STR::REPEATED-REVAPPEND STR::DISTANCE-TO-TAB$INLINE STR::DISTANCE-TO-TAB STR::HTML-ENCODE-CHARS-AUX STR::HTML-ENCODE-STRING-AUX STR::HTML-ENCODE-STRING STR::ICHAR<$INLINE STR::ICHAR< STR::ICHARLIST< STR::ISTR<-AUX STR::ISTR<$INLINE STR::ISTR< STR::IPREFIXP STR::ISTRPREFIXP-IMPL STR::ISTRPREFIXP$INLINE STR::ISTRPREFIXP STR::ISTRPOS-IMPL STR::ISTRPOS$INLINE STR::ISTRPOS STR::ISUBSTRP$INLINE STR::ISUBSTRP STR::COLLECT-STRS-WITH-ISUBSTR STR::COLLECT-SYMS-WITH-ISUBSTR MERGESORT-FIXNUM-THRESHOLD STR::ISTR-LIST-P STR::ISTR-MERGE-TR STR::ISTR-MERGESORT-FIXNUM STR::ISTR-MERGESORT-INTEGERS STR::ISTR-SORT STR::ISTRSORT STR::BASIC-NATCHARS STR::NATCHARS-AUX STR::NATCHARS$INLINE STR::NATCHARS STR::NATSTR$INLINE STR::NATSTR STR::NATSTR-LIST STR::REVAPPEND-NATCHARS-AUX STR::REVAPPEND-NATCHARS$INLINE STR::REVAPPEND-NATCHARS STR::RPADCHARS STR::RPADSTR STR::LPADCHARS STR::LPADSTR STR::TRIM-AUX STR::TRIM-BAG STR::TRIM STR::PREFIX-LINES-AUX STR::PREFIX-LINES STR::CHARPOS-AUX STR::GO-TO-LINE STR::STRLINE STR::STRLINES STR::PARSE-NAT-FROM-CHARLIST STR::PARSE-NAT-FROM-STRING STR::CHARLISTNAT< STR::STRNAT<-AUX STR::STRNAT<$INLINE STR::STRNAT< STR::STRPREFIXP-IMPL STR::STRPREFIXP$INLINE STR::STRPREFIXP STR::STRPOS-FAST STR::STRPOS$INLINE STR::STRPOS STR::STRRPOS-FAST STR::STRRPOS$INLINE STR::STRRPOS STR::SPLIT-LIST-1 STR::SPLIT-LIST* STR::CHARACTER-LIST-LISTP STR::COERCE-LIST-TO-STRINGS STR::STRSPLIT STR::STRSUBST-AUX STR::STRSUBST STR::STRSUBST-LIST STR::STRTOK-AUX STR::STRTOK$INLINE STR::STRTOK STR::OCTAL-DIGITP$INLINE STR::OCTAL-DIGITP STR::OCTAL-DIGIT-LISTP STR::PARSE-OCTAL-FROM-CHARLIST STR::OCTAL-DIGIT-LIST-VALUE$INLINE STR::OCTAL-DIGIT-LIST-VALUE STR::HEX-DIGITP$INLINE STR::HEX-DIGITP STR::HEX-DIGIT-LISTP STR::HEX-DIGIT-VAL$INLINE STR::HEX-DIGIT-VAL STR::PARSE-HEX-FROM-CHARLIST STR::HEX-DIGIT-LIST-VALUE$INLINE STR::HEX-DIGIT-LIST-VALUE STR::BIT-DIGITP$INLINE STR::BIT-DIGITP STR::BIT-DIGIT-LISTP STR::BITSTRING-P STR::PARSE-BITS-FROM-CHARLIST STR::BIT-DIGIT-LIST-VALUE$INLINE STR::BIT-DIGIT-LIST-VALUE STR::STRVAL STR::STRVAL8 STR::STRVAL16 STR::STRVAL2 STR::SUBSTRP$INLINE STR::SUBSTRP STR::STRSUFFIXP$INLINE STR::STRSUFFIXP STR::SYMBOL-LIST-NAMES STR::INTERN-LIST-FN STR::INTERN-LIST)) STATE)) (ENCAPSULATE NIL (SET-ENFORCE-REDUNDANCY T) (LOGIC) (DEFUN EXPLODE$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (COERCE X (QUOTE LIST))) (IN-THEORY (E/D ((:EXECUTABLE-COUNTERPART EXPLODE$INLINE)) ((:TYPE-PRESCRIPTION EXPLODE$INLINE) (:DEFINITION EXPLODE$INLINE)))) (DEFMACRO EXPLODE (X) (LIST (QUOTE EXPLODE$INLINE) X)) (DEFUN IMPLODE$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (COERCE X (QUOTE STRING))) (IN-THEORY (E/D ((:EXECUTABLE-COUNTERPART IMPLODE$INLINE)) ((:TYPE-PRESCRIPTION IMPLODE$INLINE) (:DEFINITION IMPLODE$INLINE)))) (DEFMACRO IMPLODE (X) (LIST (QUOTE IMPLODE$INLINE) X)) (DEFTHM STR::STRINGP-OF-IMPLODE (STRINGP (IMPLODE X)) :RULE-CLASSES :TYPE-PRESCRIPTION) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRINGP-OF-IMPLODE)) NIL)) (DEFUN STR::CHAR-FIX$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (IF (CHARACTERP X) X (CODE-CHAR 0))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHAR-FIX$INLINE) (:EXECUTABLE-COUNTERPART STR::CHAR-FIX$INLINE)) ((:DEFINITION STR::CHAR-FIX$INLINE)))) (DEFMACRO STR::CHAR-FIX (X) (LIST (QUOTE STR::CHAR-FIX$INLINE) X)) (DEFUN STR::CHAREQV$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (EQL (STR::CHAR-FIX X) (STR::CHAR-FIX Y))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHAREQV$INLINE) (:EXECUTABLE-COUNTERPART STR::CHAREQV$INLINE)) ((:DEFINITION STR::CHAREQV$INLINE)))) (DEFMACRO STR::CHAREQV (X Y) (LIST (QUOTE STR::CHAREQV$INLINE) X Y)) (DEFTHM STR::CHAREQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::CHAREQV X Y)) (STR::CHAREQV X X) (IMPLIES (STR::CHAREQV X Y) (STR::CHAREQV Y X)) (IMPLIES (AND (STR::CHAREQV X Y) (STR::CHAREQV Y Z)) (STR::CHAREQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::CHAREQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::CHARLISTEQV (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (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))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARLISTEQV) (:EXECUTABLE-COUNTERPART STR::CHARLISTEQV)) ((:INDUCTION STR::CHARLISTEQV) (:DEFINITION STR::CHARLISTEQV)))) (DEFTHM STR::CHARLISTEQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::CHARLISTEQV X Y)) (STR::CHARLISTEQV X X) (IMPLIES (STR::CHARLISTEQV X Y) (STR::CHARLISTEQV Y X)) (IMPLIES (AND (STR::CHARLISTEQV X Y) (STR::CHARLISTEQV Y Z)) (STR::CHARLISTEQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::CHARLISTEQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::STR-FIX$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (IF (STRINGP X) X "")) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STR-FIX$INLINE) (:EXECUTABLE-COUNTERPART STR::STR-FIX$INLINE)) ((:DEFINITION STR::STR-FIX$INLINE)))) (DEFMACRO STR::STR-FIX (X) (LIST (QUOTE STR::STR-FIX$INLINE) X)) (DEFUN STR::STREQV$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (EQUAL (STR::STR-FIX X) (STR::STR-FIX Y))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STREQV$INLINE) (:EXECUTABLE-COUNTERPART STR::STREQV$INLINE)) ((:DEFINITION STR::STREQV$INLINE)))) (DEFMACRO STR::STREQV (X Y) (LIST (QUOTE STR::STREQV$INLINE) X Y)) (DEFTHM STR::STREQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::STREQV X Y)) (STR::STREQV X X) (IMPLIES (STR::STREQV X Y) (STR::STREQV Y X)) (IMPLIES (AND (STR::STREQV X Y) (STR::STREQV Y Z)) (STR::STREQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::STREQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::FAST-STRING-APPEND (STR::STR1 STR::STR2) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING STR::STR1 STR::STR2)) (STRING-APPEND STR::STR1 STR::STR2)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::FAST-STRING-APPEND) (:EXECUTABLE-COUNTERPART STR::FAST-STRING-APPEND) (:DEFINITION STR::FAST-STRING-APPEND)) NIL)) (DEFUN STR::FAST-STRING-APPEND-LST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (STRING-LISTP X))) (STRING-APPEND-LST X)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::FAST-STRING-APPEND-LST) (:EXECUTABLE-COUNTERPART STR::FAST-STRING-APPEND-LST) (:DEFINITION STR::FAST-STRING-APPEND-LST)) NIL)) (DEFMACRO STR::FAST-CONCATENATE (STR::RESULT-TYPE &REST STR::SEQUENCES) (DECLARE (XARGS :GUARD (MEMBER-EQUAL STR::RESULT-TYPE (QUOTE ((QUOTE STRING) (QUOTE LIST)))))) (COND ((EQUAL STR::RESULT-TYPE (QUOTE (QUOTE STRING))) (COND ((AND STR::SEQUENCES (CDR STR::SEQUENCES) (NULL (CDDR STR::SEQUENCES))) (LIST (QUOTE STR::FAST-STRING-APPEND) (CAR STR::SEQUENCES) (CADR STR::SEQUENCES))) (T (LIST (QUOTE STR::FAST-STRING-APPEND-LST) (CONS (QUOTE LIST) STR::SEQUENCES))))) (T (CONS (QUOTE APPEND) (CONS (CONS (QUOTE LIST) STR::SEQUENCES) (QUOTE NIL)))))) (DEFMACRO STR::CAT (&REST ARGS) (CONS (QUOTE STR::FAST-CONCATENATE) (CONS (CONS (QUOTE QUOTE) (CONS (QUOTE STRING) (QUOTE NIL))) ARGS))) (DEFUN STR::APPEND-CHARS-AUX (X N Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N) (XARGS :GUARD (< N (LENGTH X)))) (IF (ZP N) (CONS (CHAR X 0) Y) (STR::APPEND-CHARS-AUX X (THE (INTEGER 0 *) (- N 1)) (CONS (CHAR X N) Y)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::APPEND-CHARS-AUX) (:EXECUTABLE-COUNTERPART STR::APPEND-CHARS-AUX)) ((:INDUCTION STR::APPEND-CHARS-AUX) (:DEFINITION STR::APPEND-CHARS-AUX)))) (DEFUN STR::APPEND-CHARS$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (MBE :LOGIC (APPEND (EXPLODE X) Y) :EXEC (B* (((THE (INTEGER 0 *) STR::XL) (LENGTH X)) ((WHEN (EQL STR::XL 0)) Y) ((THE (INTEGER 0 *) N) (- STR::XL 1))) (STR::APPEND-CHARS-AUX X N Y)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::APPEND-CHARS$INLINE) (:EXECUTABLE-COUNTERPART STR::APPEND-CHARS$INLINE)) ((:DEFINITION STR::APPEND-CHARS$INLINE)))) (DEFMACRO STR::APPEND-CHARS (X Y) (LIST (QUOTE STR::APPEND-CHARS$INLINE) X Y)) (DEFUN STR::REVAPPEND-CHARS-AUX (X N STR::XL Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N STR::XL) (XARGS :GUARD (AND (<= N STR::XL) (EQUAL STR::XL (LENGTH X))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (EQL N STR::XL)) Y (STR::REVAPPEND-CHARS-AUX X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL (CONS (CHAR X N) Y)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::REVAPPEND-CHARS-AUX) (:EXECUTABLE-COUNTERPART STR::REVAPPEND-CHARS-AUX)) ((:INDUCTION STR::REVAPPEND-CHARS-AUX) (:DEFINITION STR::REVAPPEND-CHARS-AUX)))) (DEFUN STR::REVAPPEND-CHARS$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (STRINGP X)) (TYPE STRING X)) (MBE :LOGIC (REVAPPEND (EXPLODE X) Y) :EXEC (STR::REVAPPEND-CHARS-AUX X 0 (LENGTH X) Y))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::REVAPPEND-CHARS$INLINE) (:EXECUTABLE-COUNTERPART STR::REVAPPEND-CHARS$INLINE)) ((:DEFINITION STR::REVAPPEND-CHARS$INLINE)))) (DEFMACRO STR::REVAPPEND-CHARS (X Y) (LIST (QUOTE STR::REVAPPEND-CHARS$INLINE) X Y)) (DEFUN STR::PREFIX-STRINGS (STR::PREFIX X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE STRING STR::PREFIX) (XARGS :GUARD (STRING-LISTP X))) (IF (ATOM X) NIL (CONS (STR::CAT STR::PREFIX (CAR X)) (STR::PREFIX-STRINGS STR::PREFIX (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PREFIX-STRINGS) (:EXECUTABLE-COUNTERPART STR::PREFIX-STRINGS)) ((:INDUCTION STR::PREFIX-STRINGS) (:DEFINITION STR::PREFIX-STRINGS)))) (DEFUN STR::RCHARS-TO-STRING (STR::RCHARS) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (CHARACTER-LISTP STR::RCHARS))) (THE STRING (REVERSE (THE STRING (COERCE (THE LIST STR::RCHARS) (QUOTE STRING)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::RCHARS-TO-STRING) (:EXECUTABLE-COUNTERPART STR::RCHARS-TO-STRING) (:DEFINITION STR::RCHARS-TO-STRING)) NIL)) (DEFUN STR::JOIN-AUX (X STR::SEPARATOR STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (STRING-LISTP X)) (TYPE STRING STR::SEPARATOR)) (COND ((ATOM X) STR::ACC) ((ATOM (CDR X)) (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (T (LET* ((STR::ACC (STR::REVAPPEND-CHARS (CAR X) STR::ACC)) (STR::ACC (STR::REVAPPEND-CHARS STR::SEPARATOR STR::ACC))) (STR::JOIN-AUX (CDR X) STR::SEPARATOR STR::ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::JOIN-AUX) (:EXECUTABLE-COUNTERPART STR::JOIN-AUX)) ((:INDUCTION STR::JOIN-AUX) (:DEFINITION STR::JOIN-AUX)))) (DEFUN STR::JOIN (X STR::SEPARATOR) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE STRING STR::SEPARATOR)) (DECLARE (XARGS :GUARD (STRING-LISTP X))) (MBE :LOGIC (COND ((ATOM X) "") ((ATOM (CDR X)) (IF (STRINGP (CAR X)) (CAR X) "")) (T (STR::CAT (CAR X) STR::SEPARATOR (STR::JOIN (CDR X) STR::SEPARATOR)))) :EXEC (STR::RCHARS-TO-STRING (STR::JOIN-AUX X STR::SEPARATOR NIL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::JOIN) (:EXECUTABLE-COUNTERPART STR::JOIN)) ((:INDUCTION STR::JOIN) (:DEFINITION STR::JOIN)))) (DEFMACRO STR::LITTLE-A NIL (CHAR-CODE #\a)) (DEFMACRO STR::LITTLE-Z NIL (CHAR-CODE #\z)) (DEFMACRO STR::BIG-A NIL (CHAR-CODE #\A)) (DEFMACRO STR::BIG-Z NIL (CHAR-CODE #\Z)) (DEFMACRO STR::CASE-DELTA NIL (- (STR::LITTLE-A) (STR::BIG-A))) (DEFUN STR::UP-ALPHA-P$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UP-ALPHA-P$INLINE) (:EXECUTABLE-COUNTERPART STR::UP-ALPHA-P$INLINE)) ((:DEFINITION STR::UP-ALPHA-P$INLINE)))) (DEFMACRO STR::UP-ALPHA-P (X) (LIST (QUOTE STR::UP-ALPHA-P$INLINE) X)) (DEFUN STR::DOWN-ALPHA-P$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWN-ALPHA-P$INLINE) (:EXECUTABLE-COUNTERPART STR::DOWN-ALPHA-P$INLINE)) ((:DEFINITION STR::DOWN-ALPHA-P$INLINE)))) (DEFMACRO STR::DOWN-ALPHA-P (X) (LIST (QUOTE STR::DOWN-ALPHA-P$INLINE) X)) (DEFUN STR::UPCASE-CHAR$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::LITTLE-A) STR::CODE) (<= STR::CODE (STR::LITTLE-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (- STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-CHAR$INLINE) (:EXECUTABLE-COUNTERPART STR::UPCASE-CHAR$INLINE)) ((:DEFINITION STR::UPCASE-CHAR$INLINE)))) (DEFMACRO STR::UPCASE-CHAR (X) (LIST (QUOTE STR::UPCASE-CHAR$INLINE) X)) (DEFUN STR::DOWNCASE-CHAR$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (B* (((THE (UNSIGNED-BYTE 8) STR::CODE) (CHAR-CODE X))) (IF (AND (<= (STR::BIG-A) STR::CODE) (<= STR::CODE (STR::BIG-Z))) (CODE-CHAR (THE (UNSIGNED-BYTE 8) (+ STR::CODE (STR::CASE-DELTA)))) (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-CHAR$INLINE) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-CHAR$INLINE)) ((:DEFINITION STR::DOWNCASE-CHAR$INLINE)))) (DEFMACRO STR::DOWNCASE-CHAR (X) (LIST (QUOTE STR::DOWNCASE-CHAR$INLINE) X)) (DEFUN STR::MAKE-UPCASE-FIRST-STRTBL (N) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::UPCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-UPCASE-FIRST-STRTBL (- N 1))))) (IN-THEORY (E/D ((:INDUCTION STR::MAKE-UPCASE-FIRST-STRTBL) (:TYPE-PRESCRIPTION STR::MAKE-UPCASE-FIRST-STRTBL) (:EXECUTABLE-COUNTERPART STR::MAKE-UPCASE-FIRST-STRTBL) (:DEFINITION STR::MAKE-UPCASE-FIRST-STRTBL)) NIL)) (DEFCONST STR::*UPCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-UPCASE-FIRST-STRTBL 255)))) (DEFUN STR::UPCASE-CHAR-STR$INLINE (C) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::UPCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*UPCASE-FIRST-STRTBL*) STR::*UPCASE-FIRST-STRTBL* (CHAR-CODE C)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-CHAR-STR$INLINE) (:EXECUTABLE-COUNTERPART STR::UPCASE-CHAR-STR$INLINE) (:DEFINITION STR::UPCASE-CHAR-STR$INLINE)) NIL)) (DEFMACRO STR::UPCASE-CHAR-STR (C) (LIST (QUOTE STR::UPCASE-CHAR-STR$INLINE) C)) (DEFUN STR::MAKE-DOWNCASE-FIRST-STRTBL (N) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (XARGS :GUARD (AND (NATP N) (<= N 255)) :RULER-EXTENDERS :ALL)) (CONS (CONS N (IMPLODE (LIST (STR::DOWNCASE-CHAR (CODE-CHAR N))))) (IF (ZP N) NIL (STR::MAKE-DOWNCASE-FIRST-STRTBL (- N 1))))) (IN-THEORY (E/D ((:INDUCTION STR::MAKE-DOWNCASE-FIRST-STRTBL) (:TYPE-PRESCRIPTION STR::MAKE-DOWNCASE-FIRST-STRTBL) (:EXECUTABLE-COUNTERPART STR::MAKE-DOWNCASE-FIRST-STRTBL) (:DEFINITION STR::MAKE-DOWNCASE-FIRST-STRTBL)) NIL)) (DEFCONST STR::*DOWNCASE-FIRST-STRTBL* (COMPRESS1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) (CONS (QUOTE (:HEADER :DIMENSIONS (256) :MAXIMUM-LENGTH 257)) (STR::MAKE-DOWNCASE-FIRST-STRTBL 255)))) (DEFUN STR::DOWNCASE-CHAR-STR$INLINE (C) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER C)) (MBE :LOGIC (IMPLODE (LIST (STR::DOWNCASE-CHAR C))) :EXEC (AREF1 (QUOTE STR::*DOWNCASE-FIRST-STRTBL*) STR::*DOWNCASE-FIRST-STRTBL* (CHAR-CODE C)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-CHAR-STR$INLINE) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-CHAR-STR$INLINE) (:DEFINITION STR::DOWNCASE-CHAR-STR$INLINE)) NIL)) (DEFMACRO STR::DOWNCASE-CHAR-STR (C) (LIST (QUOTE STR::DOWNCASE-CHAR-STR$INLINE) C)) (DEFUN STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::DOWN-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P) (:EXECUTABLE-COUNTERPART STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P)) ((:INDUCTION STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P) (:DEFINITION STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P)))) (DEFUN STR::UPCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-CHARLIST-AUX (CDR X) (CONS (STR::UPCASE-CHAR (CAR X)) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-CHARLIST-AUX) (:EXECUTABLE-COUNTERPART STR::UPCASE-CHARLIST-AUX)) ((:INDUCTION STR::UPCASE-CHARLIST-AUX) (:DEFINITION STR::UPCASE-CHARLIST-AUX)))) (DEFUN STR::UPCASE-CHARLIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (STR::UPCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-DOWN-ALPHA-P X) (REVERSE (STR::UPCASE-CHARLIST-AUX X NIL)) X))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-CHARLIST) (:EXECUTABLE-COUNTERPART STR::UPCASE-CHARLIST)) ((:INDUCTION STR::UPCASE-CHARLIST) (:DEFINITION STR::UPCASE-CHARLIST)))) (DEFUN STR::CHARLIST-HAS-SOME-UP-ALPHA-P (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) NIL (OR (STR::UP-ALPHA-P (CAR X)) (STR::CHARLIST-HAS-SOME-UP-ALPHA-P (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARLIST-HAS-SOME-UP-ALPHA-P) (:EXECUTABLE-COUNTERPART STR::CHARLIST-HAS-SOME-UP-ALPHA-P)) ((:INDUCTION STR::CHARLIST-HAS-SOME-UP-ALPHA-P) (:DEFINITION STR::CHARLIST-HAS-SOME-UP-ALPHA-P)))) (DEFUN STR::DOWNCASE-CHARLIST-AUX (X STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-CHARLIST-AUX (CDR X) (CONS (STR::DOWNCASE-CHAR (CAR X)) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-CHARLIST-AUX) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-CHARLIST-AUX)) ((:INDUCTION STR::DOWNCASE-CHARLIST-AUX) (:DEFINITION STR::DOWNCASE-CHARLIST-AUX)))) (DEFUN STR::DOWNCASE-CHARLIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (STR::DOWNCASE-CHARLIST (CDR X)))) :EXEC (IF (STR::CHARLIST-HAS-SOME-UP-ALPHA-P X) (REVERSE (STR::DOWNCASE-CHARLIST-AUX X NIL)) X))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-CHARLIST) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-CHARLIST)) ((:INDUCTION STR::DOWNCASE-CHARLIST) (:DEFINITION STR::DOWNCASE-CHARLIST)))) (DEFUN STR::STRING-HAS-SOME-DOWN-ALPHA-P (X N STR::XL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::DOWN-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-DOWN-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRING-HAS-SOME-DOWN-ALPHA-P) (:EXECUTABLE-COUNTERPART STR::STRING-HAS-SOME-DOWN-ALPHA-P)) ((:INDUCTION STR::STRING-HAS-SOME-DOWN-ALPHA-P) (:DEFINITION STR::STRING-HAS-SOME-DOWN-ALPHA-P)))) (DEFUN STR::UPCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::UPCHAR (STR::UPCASE-CHAR CHAR))) (STR::UPCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::UPCHAR STR::ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-STRING-AUX) (:EXECUTABLE-COUNTERPART STR::UPCASE-STRING-AUX)) ((:INDUCTION STR::UPCASE-STRING-AUX) (:DEFINITION STR::UPCASE-STRING-AUX)))) (DEFUN STR::UPCASE-STRING (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (XARGS)) (MBE :LOGIC (IMPLODE (STR::UPCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-DOWN-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::UPCASE-STRING-AUX X 0 STR::XL NIL)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-STRING) (:EXECUTABLE-COUNTERPART STR::UPCASE-STRING)) ((:DEFINITION STR::UPCASE-STRING)))) (DEFUN STR::STRING-HAS-SOME-UP-ALPHA-P (X N STR::XL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL (OR (STR::UP-ALPHA-P (CHAR X N)) (STR::STRING-HAS-SOME-UP-ALPHA-P X (+ 1 (LNFIX N)) STR::XL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRING-HAS-SOME-UP-ALPHA-P) (:EXECUTABLE-COUNTERPART STR::STRING-HAS-SOME-UP-ALPHA-P)) ((:INDUCTION STR::STRING-HAS-SOME-UP-ALPHA-P) (:DEFINITION STR::STRING-HAS-SOME-UP-ALPHA-P)))) (DEFUN STR::DOWNCASE-STRING-AUX (X N STR::XL STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (= STR::XL (LENGTH X)) (<= N STR::XL)))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::DOWNCHAR (STR::DOWNCASE-CHAR CHAR))) (STR::DOWNCASE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (CONS STR::DOWNCHAR STR::ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-STRING-AUX) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-STRING-AUX)) ((:INDUCTION STR::DOWNCASE-STRING-AUX) (:DEFINITION STR::DOWNCASE-STRING-AUX)))) (DEFUN STR::DOWNCASE-STRING (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (XARGS)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-CHARLIST (EXPLODE X))) :EXEC (LET ((STR::XL (LENGTH X))) (IF (NOT (STR::STRING-HAS-SOME-UP-ALPHA-P X 0 STR::XL)) X (STR::RCHARS-TO-STRING (STR::DOWNCASE-STRING-AUX X 0 STR::XL NIL)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-STRING) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-STRING)) ((:DEFINITION STR::DOWNCASE-STRING)))) (DEFUN STR::UPCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::UPCASE-STRING-LIST-AUX (CDR X) (CONS (STR::UPCASE-STRING (CAR X)) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-STRING-LIST-AUX) (:EXECUTABLE-COUNTERPART STR::UPCASE-STRING-LIST-AUX)) ((:INDUCTION STR::UPCASE-STRING-LIST-AUX) (:DEFINITION STR::UPCASE-STRING-LIST-AUX)))) (DEFUN STR::UPCASE-STRING-LIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (STRING-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-STRING (CAR X)) (STR::UPCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::UPCASE-STRING-LIST-AUX X NIL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-STRING-LIST) (:EXECUTABLE-COUNTERPART STR::UPCASE-STRING-LIST)) ((:INDUCTION STR::UPCASE-STRING-LIST) (:DEFINITION STR::UPCASE-STRING-LIST)))) (DEFUN STR::DOWNCASE-STRING-LIST-AUX (X STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (STRING-LISTP STR::ACC)))) (IF (ATOM X) STR::ACC (STR::DOWNCASE-STRING-LIST-AUX (CDR X) (CONS (STR::DOWNCASE-STRING (CAR X)) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-STRING-LIST-AUX) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-STRING-LIST-AUX)) ((:INDUCTION STR::DOWNCASE-STRING-LIST-AUX) (:DEFINITION STR::DOWNCASE-STRING-LIST-AUX)))) (DEFUN STR::DOWNCASE-STRING-LIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (STRING-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-STRING (CAR X)) (STR::DOWNCASE-STRING-LIST (CDR X)))) :EXEC (REVERSE (STR::DOWNCASE-STRING-LIST-AUX X NIL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-STRING-LIST) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-STRING-LIST)) ((:INDUCTION STR::DOWNCASE-STRING-LIST) (:DEFINITION STR::DOWNCASE-STRING-LIST)))) (DEFUN STR::UPCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::UPCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::DOWN-ALPHA-P (CAR X)) (CONS (STR::UPCASE-CHAR (CAR X)) (CDR X))) (T X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-FIRST-CHARLIST) (:EXECUTABLE-COUNTERPART STR::UPCASE-FIRST-CHARLIST)) ((:DEFINITION STR::UPCASE-FIRST-CHARLIST)))) (DEFUN STR::UPCASE-FIRST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (XARGS)) (MBE :LOGIC (IMPLODE (STR::UPCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::DOWN-ALPHA-P C) (STR::CAT (STR::UPCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::UPCASE-FIRST) (:EXECUTABLE-COUNTERPART STR::UPCASE-FIRST)) ((:DEFINITION STR::UPCASE-FIRST)))) (DEFUN STR::DOWNCASE-FIRST-CHARLIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (MBE :LOGIC (IF (ATOM X) NIL (CONS (STR::DOWNCASE-CHAR (CAR X)) (MAKE-CHARACTER-LIST (CDR X)))) :EXEC (COND ((ATOM X) NIL) ((STR::UP-ALPHA-P (CAR X)) (CONS (STR::DOWNCASE-CHAR (CAR X)) (CDR X))) (T X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-FIRST-CHARLIST) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-FIRST-CHARLIST)) ((:DEFINITION STR::DOWNCASE-FIRST-CHARLIST)))) (DEFUN STR::DOWNCASE-FIRST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (XARGS)) (MBE :LOGIC (IMPLODE (STR::DOWNCASE-FIRST-CHARLIST (EXPLODE X))) :EXEC (IF (EQL (LENGTH X) 0) X (LET ((C (CHAR X 0))) (IF (STR::UP-ALPHA-P C) (STR::CAT (STR::DOWNCASE-CHAR-STR C) (SUBSEQ X 1 NIL)) X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DOWNCASE-FIRST) (:EXECUTABLE-COUNTERPART STR::DOWNCASE-FIRST)) ((:DEFINITION STR::DOWNCASE-FIRST)))) (DEFUN STR::ICHAREQV$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X) (TYPE CHARACTER Y)) (EQUAL (STR::DOWNCASE-CHAR X) (STR::DOWNCASE-CHAR Y))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ICHAREQV$INLINE) (:EXECUTABLE-COUNTERPART STR::ICHAREQV$INLINE)) ((:DEFINITION STR::ICHAREQV$INLINE)))) (DEFMACRO STR::ICHAREQV (X Y) (LIST (QUOTE STR::ICHAREQV$INLINE) X Y)) (DEFTHM STR::ICHAREQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::ICHAREQV X Y)) (STR::ICHAREQV X X) (IMPLIES (STR::ICHAREQV X Y) (STR::ICHAREQV Y X)) (IMPLIES (AND (STR::ICHAREQV X Y) (STR::ICHAREQV Y Z)) (STR::ICHAREQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::ICHAREQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::ICHARLISTEQV (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (IF (CONSP X) (AND (CONSP Y) (STR::ICHAREQV (CAR X) (CAR Y)) (STR::ICHARLISTEQV (CDR X) (CDR Y))) (ATOM Y))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ICHARLISTEQV) (:EXECUTABLE-COUNTERPART STR::ICHARLISTEQV)) ((:INDUCTION STR::ICHARLISTEQV) (:DEFINITION STR::ICHARLISTEQV)))) (DEFTHM STR::ICHARLISTEQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::ICHARLISTEQV X Y)) (STR::ICHARLISTEQV X X) (IMPLIES (STR::ICHARLISTEQV X Y) (STR::ICHARLISTEQV Y X)) (IMPLIES (AND (STR::ICHARLISTEQV X Y) (STR::ICHARLISTEQV Y Z)) (STR::ICHARLISTEQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::ICHARLISTEQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::ISTREQV-AUX (X Y N L) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N L))) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE (INTEGER 0 *) N) (TYPE (INTEGER 0 *) L) (XARGS :GUARD (AND (NATP N) (NATP L) (EQUAL (LENGTH X) L) (EQUAL (LENGTH Y) L) (<= N L)))) (MBE :LOGIC (IF (ZP (- (NFIX L) (NFIX N))) T (AND (STR::ICHAREQV (CHAR X N) (CHAR Y N)) (STR::ISTREQV-AUX X Y (+ (NFIX N) 1) L))) :EXEC (IF (EQL N L) T (AND (STR::ICHAREQV (THE CHARACTER (CHAR X N)) (THE CHARACTER (CHAR Y N))) (STR::ISTREQV-AUX X Y (THE (INTEGER 0 *) (+ 1 N)) L))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTREQV-AUX) (:EXECUTABLE-COUNTERPART STR::ISTREQV-AUX)) ((:INDUCTION STR::ISTREQV-AUX) (:DEFINITION STR::ISTREQV-AUX)))) (DEFUN STR::ISTREQV$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (TYPE STRING Y) (XARGS)) (MBE :LOGIC (STR::ICHARLISTEQV (EXPLODE X) (EXPLODE Y)) :EXEC (B* (((THE (INTEGER 0 *) STR::XL) (LENGTH X)) ((THE (INTEGER 0 *) STR::YL) (LENGTH Y))) (AND (EQL STR::XL STR::YL) (STR::ISTREQV-AUX X Y 0 STR::XL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTREQV$INLINE) (:EXECUTABLE-COUNTERPART STR::ISTREQV$INLINE) (:DEFINITION STR::ISTREQV$INLINE)) NIL)) (DEFMACRO STR::ISTREQV (X Y) (LIST (QUOTE STR::ISTREQV$INLINE) X Y)) (DEFTHM STR::ISTREQV-IS-AN-EQUIVALENCE (AND (BOOLEANP (STR::ISTREQV X Y)) (STR::ISTREQV X X) (IMPLIES (STR::ISTREQV X Y) (STR::ISTREQV Y X)) (IMPLIES (AND (STR::ISTREQV X Y) (STR::ISTREQV Y Z)) (STR::ISTREQV X Z))) :RULE-CLASSES (:EQUIVALENCE)) (IN-THEORY (E/D ((:EQUIVALENCE STR::ISTREQV-IS-AN-EQUIVALENCE)) NIL)) (DEFUN STR::DIGITP$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DIGITP$INLINE) (:EXECUTABLE-COUNTERPART STR::DIGITP$INLINE)) ((:DEFINITION STR::DIGITP$INLINE)))) (DEFMACRO STR::DIGITP (X) (LIST (QUOTE STR::DIGITP$INLINE) X)) (DEFUN STR::NONZERO-DIGITP$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (MBE :LOGIC (LET ((STR::CODE (CHAR-CODE (STR::CHAR-FIX X)))) (AND (<= (CHAR-CODE #\1) STR::CODE) (<= STR::CODE (CHAR-CODE #\9)))) :EXEC (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (THE (UNSIGNED-BYTE 8) 49) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::NONZERO-DIGITP$INLINE) (:EXECUTABLE-COUNTERPART STR::NONZERO-DIGITP$INLINE)) ((:DEFINITION STR::NONZERO-DIGITP$INLINE)))) (DEFMACRO STR::NONZERO-DIGITP (X) (LIST (QUOTE STR::NONZERO-DIGITP$INLINE) X)) (DEFUN STR::DIGIT-VAL$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X) (XARGS :GUARD (STR::DIGITP X))) (MBE :LOGIC (IF (STR::DIGITP X) (- (CHAR-CODE (STR::CHAR-FIX X)) (CHAR-CODE #\0)) 0) :EXEC (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER X))) (THE (UNSIGNED-BYTE 8) 48))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DIGIT-VAL$INLINE) (:EXECUTABLE-COUNTERPART STR::DIGIT-VAL$INLINE)) ((:DEFINITION STR::DIGIT-VAL$INLINE)))) (DEFMACRO STR::DIGIT-VAL (X) (LIST (QUOTE STR::DIGIT-VAL$INLINE) X)) (DEFUN STR::DIGIT-LISTP (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (CONSP X) (AND (STR::DIGITP (CAR X)) (STR::DIGIT-LISTP (CDR X))) T)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DIGIT-LISTP) (:EXECUTABLE-COUNTERPART STR::DIGIT-LISTP)) ((:INDUCTION STR::DIGIT-LISTP) (:DEFINITION STR::DIGIT-LISTP)))) (DEFMACRO STR::DIGIT-LIST-VALUE (X) (LIST (QUOTE STR::DIGIT-LIST-VALUE$INLINE) X)) (DEFUN STR::SKIP-LEADING-DIGITS (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (STR::SKIP-LEADING-DIGITS (CDR X)) X) NIL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::SKIP-LEADING-DIGITS) (:EXECUTABLE-COUNTERPART STR::SKIP-LEADING-DIGITS)) ((:INDUCTION STR::SKIP-LEADING-DIGITS) (:DEFINITION STR::SKIP-LEADING-DIGITS)))) (DEFUN STR::TAKE-LEADING-DIGITS (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (CONSP X) (IF (STR::DIGITP (CAR X)) (CONS (CAR X) (STR::TAKE-LEADING-DIGITS (CDR X))) NIL) NIL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::TAKE-LEADING-DIGITS) (:EXECUTABLE-COUNTERPART STR::TAKE-LEADING-DIGITS)) ((:INDUCTION STR::TAKE-LEADING-DIGITS) (:DEFINITION STR::TAKE-LEADING-DIGITS)))) (DEFUN STR::DIGIT-STRING-P-AUX (X N STR::XL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N) (TYPE (INTEGER 0 *) STR::XL) (XARGS :GUARD (AND (<= N STR::XL) (= STR::XL (LENGTH X))))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (EQL N STR::XL)) T (AND (STR::DIGITP (CHAR X N)) (STR::DIGIT-STRING-P-AUX X (MBE :LOGIC (+ 1 (NFIX N)) :EXEC (THE (INTEGER 0 *) (+ 1 N))) STR::XL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DIGIT-STRING-P-AUX) (:EXECUTABLE-COUNTERPART STR::DIGIT-STRING-P-AUX)) ((:INDUCTION STR::DIGIT-STRING-P-AUX) (:DEFINITION STR::DIGIT-STRING-P-AUX)))) (DEFUN STR::DIGIT-STRING-P$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (MBE :LOGIC (STR::DIGIT-LISTP (EXPLODE X)) :EXEC (STR::DIGIT-STRING-P-AUX X 0 (LENGTH X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DIGIT-STRING-P$INLINE) (:EXECUTABLE-COUNTERPART STR::DIGIT-STRING-P$INLINE) (:DEFINITION STR::DIGIT-STRING-P$INLINE)) NIL)) (DEFMACRO STR::DIGIT-STRING-P (X) (LIST (QUOTE STR::DIGIT-STRING-P$INLINE) X)) (DEFUN STR::FIRSTN-CHARS-AUX (X N STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP N) (< N (LENGTH X)))) (TYPE STRING X) (TYPE (INTEGER 0 *) N)) (IF (ZP N) (CONS (CHAR X 0) STR::ACC) (STR::FIRSTN-CHARS-AUX X (THE (INTEGER 0 *) (- N 1)) (CONS (CHAR X N) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::FIRSTN-CHARS-AUX) (:EXECUTABLE-COUNTERPART STR::FIRSTN-CHARS-AUX)) ((:INDUCTION STR::FIRSTN-CHARS-AUX) (:DEFINITION STR::FIRSTN-CHARS-AUX)))) (DEFUN STR::FIRSTN-CHARS (N X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP N))) (TYPE STRING X) (TYPE (INTEGER 0 *) N)) (MBE :LOGIC (TAKE (MIN (NFIX N) (LEN (EXPLODE X))) (EXPLODE X)) :EXEC (LET ((N (MIN N (LENGTH X)))) (IF (ZP N) NIL (STR::FIRSTN-CHARS-AUX X (THE (INTEGER 0 *) (- N 1)) NIL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::FIRSTN-CHARS) (:EXECUTABLE-COUNTERPART STR::FIRSTN-CHARS)) ((:DEFINITION STR::FIRSTN-CHARS)))) (DEFUN STR::APPEND-FIRSTN-CHARS (N X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (NATP N) (STRINGP X)))) (MBE :LOGIC (APPEND (STR::FIRSTN-CHARS N X) Y) :EXEC (LET ((N (MIN N (LENGTH X)))) (IF (ZP N) Y (STR::FIRSTN-CHARS-AUX X (- N 1) Y))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::APPEND-FIRSTN-CHARS) (:EXECUTABLE-COUNTERPART STR::APPEND-FIRSTN-CHARS)) ((:DEFINITION STR::APPEND-FIRSTN-CHARS)))) (DEFMACRO STR::HTML-SPACE NIL (LIST (QUOTE QUOTE) (COERCE "&nbsp;" (QUOTE LIST)))) (DEFMACRO STR::HTML-NEWLINE NIL (LIST (QUOTE QUOTE) (APPEND (COERCE "<br/>" (QUOTE LIST)) (LIST #\Newline)))) (DEFMACRO STR::HTML-LESS NIL (LIST (QUOTE QUOTE) (COERCE "&lt;" (QUOTE LIST)))) (DEFMACRO STR::HTML-GREATER NIL (LIST (QUOTE QUOTE) (COERCE "&gt;" (QUOTE LIST)))) (DEFMACRO STR::HTML-AMP NIL (LIST (QUOTE QUOTE) (COERCE "&amp;" (QUOTE LIST)))) (DEFMACRO STR::HTML-QUOTE NIL (LIST (QUOTE QUOTE) (COERCE "&quot;" (QUOTE LIST)))) (DEFUN STR::REPEATED-REVAPPEND (N X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (XARGS :GUARD (AND (NATP N) (TRUE-LISTP X)))) (IF (ZP N) Y (STR::REPEATED-REVAPPEND (- N 1) X (REVAPPEND X Y)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::REPEATED-REVAPPEND) (:EXECUTABLE-COUNTERPART STR::REPEATED-REVAPPEND)) ((:INDUCTION STR::REPEATED-REVAPPEND) (:DEFINITION STR::REPEATED-REVAPPEND)))) (DEFUN STR::DISTANCE-TO-TAB$INLINE (STR::COL STR::TABSIZE) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (NATP STR::COL) (POSP STR::TABSIZE)))) (MBE :LOGIC (NFIX (- STR::TABSIZE (REM STR::COL STR::TABSIZE))) :EXEC (- STR::TABSIZE (REM STR::COL STR::TABSIZE)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::DISTANCE-TO-TAB$INLINE) (:EXECUTABLE-COUNTERPART STR::DISTANCE-TO-TAB$INLINE)) ((:DEFINITION STR::DISTANCE-TO-TAB$INLINE)))) (DEFMACRO STR::DISTANCE-TO-TAB (STR::COL STR::TABSIZE) (LIST (QUOTE STR::DISTANCE-TO-TAB$INLINE) STR::COL STR::TABSIZE)) (DEFUN STR::HTML-ENCODE-CHARS-AUX (X STR::COL STR::TABSIZE STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::COL) (POSP STR::TABSIZE) (CHARACTER-LISTP STR::ACC)))) (IF (ATOM X) (MV (LNFIX STR::COL) STR::ACC) (LET ((STR::CHAR1 (CAR X))) (STR::HTML-ENCODE-CHARS-AUX (CDR X) (COND ((EQL STR::CHAR1 #\Newline) 0) ((EQL STR::CHAR1 #\Tab) (+ STR::COL (STR::DISTANCE-TO-TAB STR::COL STR::TABSIZE))) (T (+ 1 STR::COL))) STR::TABSIZE (CASE STR::CHAR1 (#\Space (IF (OR (ATOM STR::ACC) (EQL (CAR STR::ACC) #\Space) (EQL (CAR STR::ACC) #\Newline)) (REVAPPEND (STR::HTML-SPACE) STR::ACC) (CONS #\Space STR::ACC))) (#\Newline (REVAPPEND (STR::HTML-NEWLINE) STR::ACC)) (#\< (REVAPPEND (STR::HTML-LESS) STR::ACC)) (#\> (REVAPPEND (STR::HTML-GREATER) STR::ACC)) (#\& (REVAPPEND (STR::HTML-AMP) STR::ACC)) (#\" (REVAPPEND (STR::HTML-QUOTE) STR::ACC)) (#\Tab (STR::REPEATED-REVAPPEND (STR::DISTANCE-TO-TAB STR::COL STR::TABSIZE) (STR::HTML-SPACE) STR::ACC)) (OTHERWISE (CONS STR::CHAR1 STR::ACC))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HTML-ENCODE-CHARS-AUX) (:EXECUTABLE-COUNTERPART STR::HTML-ENCODE-CHARS-AUX)) ((:INDUCTION STR::HTML-ENCODE-CHARS-AUX) (:DEFINITION STR::HTML-ENCODE-CHARS-AUX)))) (DEFUN STR::HTML-ENCODE-STRING-AUX (X N STR::XL STR::COL STR::TABSIZE STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (NATP STR::COL) (POSP STR::TABSIZE) (CHARACTER-LISTP STR::ACC) (<= N STR::XL) (= STR::XL (LENGTH X)))) (TYPE STRING X) (TYPE INTEGER N STR::XL STR::COL STR::TABSIZE)) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) (MV (LNFIX STR::COL) STR::ACC) (LET ((STR::CHAR1 (CHAR X N))) (STR::HTML-ENCODE-STRING-AUX X (+ 1 (LNFIX N)) STR::XL (COND ((EQL STR::CHAR1 #\Newline) 0) ((EQL STR::CHAR1 #\Tab) (+ STR::COL (STR::DISTANCE-TO-TAB STR::COL STR::TABSIZE))) (T (+ 1 STR::COL))) STR::TABSIZE (CASE STR::CHAR1 (#\Space (IF (OR (ATOM STR::ACC) (EQL (CAR STR::ACC) #\Space) (EQL (CAR STR::ACC) #\Newline)) (REVAPPEND (STR::HTML-SPACE) STR::ACC) (CONS #\Space STR::ACC))) (#\Newline (REVAPPEND (STR::HTML-NEWLINE) STR::ACC)) (#\< (REVAPPEND (STR::HTML-LESS) STR::ACC)) (#\> (REVAPPEND (STR::HTML-GREATER) STR::ACC)) (#\& (REVAPPEND (STR::HTML-AMP) STR::ACC)) (#\" (REVAPPEND (STR::HTML-QUOTE) STR::ACC)) (#\Tab (STR::REPEATED-REVAPPEND (STR::DISTANCE-TO-TAB STR::COL STR::TABSIZE) (STR::HTML-SPACE) STR::ACC)) (OTHERWISE (CONS STR::CHAR1 STR::ACC))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HTML-ENCODE-STRING-AUX) (:EXECUTABLE-COUNTERPART STR::HTML-ENCODE-STRING-AUX)) ((:INDUCTION STR::HTML-ENCODE-STRING-AUX) (:DEFINITION STR::HTML-ENCODE-STRING-AUX)))) (DEFUN STR::HTML-ENCODE-STRING (X STR::TABSIZE) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (POSP STR::TABSIZE))) (TYPE STRING X) (TYPE INTEGER STR::TABSIZE)) (B* (((MV STR::?COL STR::ACC) (STR::HTML-ENCODE-STRING-AUX X 0 (LENGTH X) 0 STR::TABSIZE NIL))) (STR::RCHARS-TO-STRING STR::ACC))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HTML-ENCODE-STRING) (:EXECUTABLE-COUNTERPART STR::HTML-ENCODE-STRING)) ((:DEFINITION STR::HTML-ENCODE-STRING)))) (DEFUN STR::ICHAR<$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X) (TYPE CHARACTER Y) (XARGS)) (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))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ICHAR<$INLINE) (:EXECUTABLE-COUNTERPART STR::ICHAR<$INLINE)) ((:DEFINITION STR::ICHAR<$INLINE)))) (DEFMACRO STR::ICHAR< (X Y) (LIST (QUOTE STR::ICHAR<$INLINE) X Y)) (DEFUN STR::ICHARLIST< (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (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))))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ICHARLIST<) (:EXECUTABLE-COUNTERPART STR::ICHARLIST<)) ((:INDUCTION STR::ICHARLIST<) (:DEFINITION STR::ICHARLIST<)))) (DEFUN STR::ISTR<-AUX (X Y N STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (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))))) (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))))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR<-AUX) (:EXECUTABLE-COUNTERPART STR::ISTR<-AUX)) ((:INDUCTION STR::ISTR<-AUX) (:DEFINITION STR::ISTR<-AUX)))) (DEFUN STR::ISTR<$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (TYPE STRING Y) (XARGS)) (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)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR<$INLINE) (:EXECUTABLE-COUNTERPART STR::ISTR<$INLINE) (:DEFINITION STR::ISTR<$INLINE)) NIL)) (DEFMACRO STR::ISTR< (X Y) (LIST (QUOTE STR::ISTR<$INLINE) X Y)) (DEFUN STR::IPREFIXP (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (IF (CONSP X) (AND (CONSP Y) (STR::ICHAREQV (CAR X) (CAR Y)) (STR::IPREFIXP (CDR X) (CDR Y))) T)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::IPREFIXP) (:EXECUTABLE-COUNTERPART STR::IPREFIXP)) ((:INDUCTION STR::IPREFIXP) (:DEFINITION STR::IPREFIXP)))) (DEFUN STR::ISTRPREFIXP-IMPL (X Y STR::XN STR::YN STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? STR::YN STR::YL STR::XN STR::XL))) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER STR::XN) (TYPE INTEGER STR::YN) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (NATP STR::XL) (NATP STR::YL) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (<= STR::XN (LENGTH X)) (<= STR::YN (LENGTH Y))))) (COND ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX STR::XN))) :EXEC (INT= STR::XN STR::XL)) T) ((MBE :LOGIC (ZP (- (NFIX STR::YL) (NFIX STR::YN))) :EXEC (INT= STR::YN STR::YL)) NIL) ((STR::ICHAREQV (CHAR X STR::XN) (CHAR Y STR::YN)) (STR::ISTRPREFIXP-IMPL X Y (+ 1 (LNFIX STR::XN)) (+ 1 (LNFIX STR::YN)) STR::XL STR::YL)) (T NIL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTRPREFIXP-IMPL) (:EXECUTABLE-COUNTERPART STR::ISTRPREFIXP-IMPL)) ((:INDUCTION STR::ISTRPREFIXP-IMPL) (:DEFINITION STR::ISTRPREFIXP-IMPL)))) (DEFUN STR::ISTRPREFIXP$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (TYPE STRING Y) (XARGS)) (MBE :LOGIC (STR::IPREFIXP (EXPLODE X) (EXPLODE Y)) :EXEC (STR::ISTRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTRPREFIXP$INLINE) (:EXECUTABLE-COUNTERPART STR::ISTRPREFIXP$INLINE) (:DEFINITION STR::ISTRPREFIXP$INLINE)) NIL)) (DEFMACRO STR::ISTRPREFIXP (X Y) (LIST (QUOTE STR::ISTRPREFIXP$INLINE) X Y)) (DEFUN STR::ISTRPOS-IMPL (X Y N STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N 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))))) (COND ((MBE :LOGIC (STR::IPREFIXP (EXPLODE X) (NTHCDR N (EXPLODE Y))) :EXEC (STR::ISTRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) 0) (THE (INTEGER 0 *) N) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))) (LNFIX N)) ((MBE :LOGIC (ZP (- (NFIX STR::YL) (NFIX N))) :EXEC (INT= N STR::YL)) NIL) (T (STR::ISTRPOS-IMPL (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) (THE (INTEGER 0 *) STR::XL) (THE (INTEGER 0 *) STR::YL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTRPOS-IMPL) (:EXECUTABLE-COUNTERPART STR::ISTRPOS-IMPL)) ((:INDUCTION STR::ISTRPOS-IMPL) (:DEFINITION STR::ISTRPOS-IMPL)))) (DEFUN STR::ISTRPOS$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X Y)) (LET* ((STR::XL (MBE :LOGIC (LEN (EXPLODE X)) :EXEC (LENGTH (THE STRING X)))) (STR::YL (MBE :LOGIC (LEN (EXPLODE Y)) :EXEC (LENGTH (THE STRING Y))))) (DECLARE (TYPE (INTEGER 0 *) STR::XL STR::YL)) (STR::ISTRPOS-IMPL (THE STRING X) (THE STRING Y) (THE (INTEGER 0 *) 0) STR::XL STR::YL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTRPOS$INLINE) (:EXECUTABLE-COUNTERPART STR::ISTRPOS$INLINE)) ((:DEFINITION STR::ISTRPOS$INLINE)))) (DEFMACRO STR::ISTRPOS (X Y) (LIST (QUOTE STR::ISTRPOS$INLINE) X Y)) (DEFUN STR::ISUBSTRP$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X Y)) (IF (STR::ISTRPOS X Y) T NIL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISUBSTRP$INLINE) (:EXECUTABLE-COUNTERPART STR::ISUBSTRP$INLINE)) ((:DEFINITION STR::ISUBSTRP$INLINE)))) (DEFMACRO STR::ISUBSTRP (X Y) (LIST (QUOTE STR::ISUBSTRP$INLINE) X Y)) (DEFUN STR::COLLECT-STRS-WITH-ISUBSTR (A X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRINGP A) (STRING-LISTP X)))) (COND ((ATOM X) NIL) ((STR::ISUBSTRP A (CAR X)) (CONS (CAR X) (STR::COLLECT-STRS-WITH-ISUBSTR A (CDR X)))) (T (STR::COLLECT-STRS-WITH-ISUBSTR A (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::COLLECT-STRS-WITH-ISUBSTR) (:EXECUTABLE-COUNTERPART STR::COLLECT-STRS-WITH-ISUBSTR)) ((:INDUCTION STR::COLLECT-STRS-WITH-ISUBSTR) (:DEFINITION STR::COLLECT-STRS-WITH-ISUBSTR)))) (DEFUN STR::COLLECT-SYMS-WITH-ISUBSTR (A X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRINGP A) (SYMBOL-LISTP X)))) (COND ((ATOM X) NIL) ((STR::ISUBSTRP A (SYMBOL-NAME (CAR X))) (CONS (CAR X) (STR::COLLECT-SYMS-WITH-ISUBSTR A (CDR X)))) (T (STR::COLLECT-SYMS-WITH-ISUBSTR A (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::COLLECT-SYMS-WITH-ISUBSTR) (:EXECUTABLE-COUNTERPART STR::COLLECT-SYMS-WITH-ISUBSTR)) ((:INDUCTION STR::COLLECT-SYMS-WITH-ISUBSTR) (:DEFINITION STR::COLLECT-SYMS-WITH-ISUBSTR)))) (DEFMACRO MERGESORT-FIXNUM-THRESHOLD NIL 536870912) (DEFUN STR::ISTR-LIST-P (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD T)) (IF (CONSP X) (AND (STRINGP (CAR X)) (STR::ISTR-LIST-P (CDR X))) T)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR-LIST-P) (:EXECUTABLE-COUNTERPART STR::ISTR-LIST-P)) ((:INDUCTION STR::ISTR-LIST-P) (:DEFINITION STR::ISTR-LIST-P)))) (DEFUN STR::ISTR-MERGE-TR (X Y ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? Y X))) (DECLARE (XARGS :GUARD (AND (STR::ISTR-LIST-P X) (STR::ISTR-LIST-P Y)))) (COND ((ATOM X) (REVAPPEND-WITHOUT-GUARD ACC Y)) ((ATOM Y) (REVAPPEND-WITHOUT-GUARD ACC X)) ((STR::ISTR< (CAR Y) (CAR X)) (STR::ISTR-MERGE-TR X (CDR Y) (CONS (CAR Y) ACC))) (T (STR::ISTR-MERGE-TR (CDR X) Y (CONS (CAR X) ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR-MERGE-TR) (:EXECUTABLE-COUNTERPART STR::ISTR-MERGE-TR)) ((:INDUCTION STR::ISTR-MERGE-TR) (:DEFINITION STR::ISTR-MERGE-TR)))) (DEFUN STR::ISTR-MERGESORT-FIXNUM (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? LEN))) (DECLARE (XARGS :GUARD (AND (STR::ISTR-LIST-P X) (NATP LEN) (<= LEN (LEN X)))) (TYPE (SIGNED-BYTE 30) LEN)) (COND ((MBE :LOGIC (ZP LEN) :EXEC (EQL (THE (SIGNED-BYTE 30) LEN) 0)) NIL) ((EQL (THE (SIGNED-BYTE 30) LEN) 1) (LIST (CAR X))) (T (LET* ((LEN1 (THE (SIGNED-BYTE 30) (ASH (THE (SIGNED-BYTE 30) LEN) -1))) (LEN2 (THE (SIGNED-BYTE 30) (+ (THE (SIGNED-BYTE 30) LEN1) (THE (SIGNED-BYTE 30) (LOGAND (THE (SIGNED-BYTE 30) LEN) 1))))) (PART1 (STR::ISTR-MERGESORT-FIXNUM X LEN1)) (PART2 (STR::ISTR-MERGESORT-FIXNUM (REST-N LEN1 X) LEN2))) (STR::ISTR-MERGE-TR PART1 PART2 NIL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR-MERGESORT-FIXNUM) (:EXECUTABLE-COUNTERPART STR::ISTR-MERGESORT-FIXNUM)) ((:INDUCTION STR::ISTR-MERGESORT-FIXNUM) (:DEFINITION STR::ISTR-MERGESORT-FIXNUM)))) (DEFUN STR::ISTR-MERGESORT-INTEGERS (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? LEN))) (DECLARE (XARGS :GUARD (AND (STR::ISTR-LIST-P X) (NATP LEN) (<= LEN (LEN X)))) (TYPE INTEGER LEN)) (COND ((MBE :LOGIC (ZP LEN) :EXEC (EQL (THE INTEGER LEN) 0)) NIL) ((EQL (THE INTEGER LEN) 1) (LIST (CAR X))) (T (LET* ((LEN1 (THE INTEGER (ASH (THE INTEGER LEN) -1))) (LEN2 (THE INTEGER (+ (THE INTEGER LEN1) (THE INTEGER (LOGAND (THE INTEGER LEN) 1))))) (PART1 (IF (< (THE INTEGER LEN1) (MERGESORT-FIXNUM-THRESHOLD)) (STR::ISTR-MERGESORT-FIXNUM X LEN1) (STR::ISTR-MERGESORT-INTEGERS X LEN1))) (PART2 (IF (< (THE INTEGER LEN2) (MERGESORT-FIXNUM-THRESHOLD)) (STR::ISTR-MERGESORT-FIXNUM (REST-N LEN1 X) LEN2) (STR::ISTR-MERGESORT-INTEGERS (REST-N LEN1 X) LEN2)))) (STR::ISTR-MERGE-TR PART1 PART2 NIL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR-MERGESORT-INTEGERS) (:EXECUTABLE-COUNTERPART STR::ISTR-MERGESORT-INTEGERS)) ((:INDUCTION STR::ISTR-MERGESORT-INTEGERS) (:DEFINITION STR::ISTR-MERGESORT-INTEGERS)))) (DEFUN STR::ISTR-SORT (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (STR::ISTR-LIST-P X))) (LET ((LEN (LEN X))) (IF (< LEN (MERGESORT-FIXNUM-THRESHOLD)) (STR::ISTR-MERGESORT-FIXNUM X LEN) (STR::ISTR-MERGESORT-INTEGERS X LEN)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::ISTR-SORT) (:EXECUTABLE-COUNTERPART STR::ISTR-SORT)) ((:DEFINITION STR::ISTR-SORT)))) (DEFMACRO STR::ISTRSORT (X) (CONS (QUOTE STR::ISTR-SORT) (CONS X (QUOTE NIL)))) (DEFUN STR::BASIC-NATCHARS (N) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (XARGS :GUARD (NATP N))) (IF (ZP N) NIL (CONS (DIGIT-TO-CHAR (MOD N 10)) (STR::BASIC-NATCHARS (FLOOR N 10))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::BASIC-NATCHARS) (:EXECUTABLE-COUNTERPART STR::BASIC-NATCHARS)) ((:INDUCTION STR::BASIC-NATCHARS) (:DEFINITION STR::BASIC-NATCHARS)))) (DEFUN STR::NATCHARS-AUX (N STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (TYPE INTEGER N) (XARGS :GUARD (NATP N))) (IF (ZP N) STR::ACC (STR::NATCHARS-AUX (THE INTEGER (TRUNCATE (THE INTEGER N) 10)) (CONS (THE CHARACTER (CODE-CHAR (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) (REM (THE INTEGER N) 10)))))) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::NATCHARS-AUX) (:EXECUTABLE-COUNTERPART STR::NATCHARS-AUX)) ((:INDUCTION STR::NATCHARS-AUX) (:DEFINITION STR::NATCHARS-AUX)))) (DEFUN STR::NATCHARS$INLINE (N) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE INTEGER N) (XARGS :GUARD (NATP N))) (OR (STR::NATCHARS-AUX N NIL) (QUOTE (#\0)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::NATCHARS$INLINE) (:EXECUTABLE-COUNTERPART STR::NATCHARS$INLINE)) ((:DEFINITION STR::NATCHARS$INLINE)))) (DEFMACRO STR::NATCHARS (N) (LIST (QUOTE STR::NATCHARS$INLINE) N)) (DEFUN STR::NATSTR$INLINE (N) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE INTEGER N) (XARGS :GUARD (NATP N))) (IMPLODE (STR::NATCHARS N))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::NATSTR$INLINE) (:EXECUTABLE-COUNTERPART STR::NATSTR$INLINE)) ((:DEFINITION STR::NATSTR$INLINE)))) (DEFMACRO STR::NATSTR (N) (LIST (QUOTE STR::NATSTR$INLINE) N)) (DEFUN STR::NATSTR-LIST (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (NAT-LISTP X))) (IF (ATOM X) NIL (CONS (STR::NATSTR (CAR X)) (STR::NATSTR-LIST (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::NATSTR-LIST) (:EXECUTABLE-COUNTERPART STR::NATSTR-LIST)) ((:INDUCTION STR::NATSTR-LIST) (:DEFINITION STR::NATSTR-LIST)))) (DEFUN STR::REVAPPEND-NATCHARS-AUX (N STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (DECLARE (TYPE INTEGER N) (XARGS :GUARD (AND (NATP N)))) (IF (ZP N) STR::ACC (CONS (THE CHARACTER (CODE-CHAR (THE (UNSIGNED-BYTE 8) (+ (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) (REM (THE INTEGER N) 10)))))) (STR::REVAPPEND-NATCHARS-AUX (THE INTEGER (TRUNCATE (THE INTEGER N) 10)) STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::REVAPPEND-NATCHARS-AUX) (:EXECUTABLE-COUNTERPART STR::REVAPPEND-NATCHARS-AUX)) ((:INDUCTION STR::REVAPPEND-NATCHARS-AUX) (:DEFINITION STR::REVAPPEND-NATCHARS-AUX)))) (DEFUN STR::REVAPPEND-NATCHARS$INLINE (N STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE INTEGER N) (XARGS :GUARD (NATP N))) (MBE :LOGIC (REVAPPEND (STR::NATCHARS N) STR::ACC) :EXEC (IF (ZP N) (CONS #\0 STR::ACC) (STR::REVAPPEND-NATCHARS-AUX N STR::ACC)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::REVAPPEND-NATCHARS$INLINE) (:EXECUTABLE-COUNTERPART STR::REVAPPEND-NATCHARS$INLINE) (:DEFINITION STR::REVAPPEND-NATCHARS$INLINE)) NIL)) (DEFMACRO STR::REVAPPEND-NATCHARS (N STR::ACC) (LIST (QUOTE STR::REVAPPEND-NATCHARS$INLINE) N STR::ACC)) (DEFUN STR::RPADCHARS (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP LEN))) (TYPE INTEGER LEN)) (MBE :LOGIC (APPEND (MAKE-CHARACTER-LIST X) (REPEAT #\Space (NFIX (- (NFIX LEN) (LEN X))))) :EXEC (LET* ((STR::X-LEN (LENGTH (THE LIST X))) (STR::DIFF (- LEN STR::X-LEN))) (IF (> STR::DIFF 0) (APPEND X (REPEAT #\Space STR::DIFF)) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::RPADCHARS) (:EXECUTABLE-COUNTERPART STR::RPADCHARS)) ((:DEFINITION STR::RPADCHARS)))) (DEFUN STR::RPADSTR (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP LEN))) (TYPE STRING X) (TYPE INTEGER LEN)) (MBE :LOGIC (IMPLODE (STR::RPADCHARS (EXPLODE X) LEN)) :EXEC (LET* ((STR::X-LEN (LENGTH (THE STRING X))) (STR::DIFF (- LEN STR::X-LEN))) (IF (> STR::DIFF 0) (LET ((STR::SPACES (REPEAT #\Space STR::DIFF))) (IMPLODE (MBE :LOGIC (STR::APPEND-CHARS X STR::SPACES) :EXEC (IF (ZP STR::X-LEN) STR::SPACES (STR::APPEND-CHARS-AUX X (- STR::X-LEN 1) STR::SPACES))))) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::RPADSTR) (:EXECUTABLE-COUNTERPART STR::RPADSTR)) ((:DEFINITION STR::RPADSTR)))) (DEFUN STR::LPADCHARS (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP LEN))) (TYPE INTEGER LEN)) (MBE :LOGIC (APPEND (REPEAT #\Space (NFIX (- (NFIX LEN) (LEN X)))) (MAKE-CHARACTER-LIST X)) :EXEC (LET* ((STR::X-LEN (LENGTH X)) (STR::DIFF (- LEN STR::X-LEN))) (IF (< 0 STR::DIFF) (MAKE-LIST-AC STR::DIFF #\Space X) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::LPADCHARS) (:EXECUTABLE-COUNTERPART STR::LPADCHARS)) ((:DEFINITION STR::LPADCHARS)))) (DEFUN STR::LPADSTR (X LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP LEN))) (TYPE STRING X) (TYPE INTEGER LEN)) (MBE :LOGIC (IMPLODE (STR::LPADCHARS (EXPLODE X) LEN)) :EXEC (LET* ((STR::X-LEN (LENGTH X)) (STR::DIFF (- LEN STR::X-LEN))) (IF (< 0 STR::DIFF) (IMPLODE (MAKE-LIST-AC STR::DIFF #\Space (EXPLODE X))) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::LPADSTR) (:EXECUTABLE-COUNTERPART STR::LPADSTR)) ((:DEFINITION STR::LPADSTR)))) (DEFUN STR::TRIM-AUX (X STR::BAG) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP STR::BAG)))) (IF (CONSP X) (IF (MEMBER (CAR X) STR::BAG) (STR::TRIM-AUX (CDR X) STR::BAG) X) NIL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::TRIM-AUX) (:EXECUTABLE-COUNTERPART STR::TRIM-AUX)) ((:INDUCTION STR::TRIM-AUX) (:DEFINITION STR::TRIM-AUX)))) (DEFUN STR::TRIM-BAG (X STR::BAG) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (CHARACTER-LISTP STR::BAG)))) (LET* ((STR::CHARS (EXPLODE X)) (STR::CHARS (STR::TRIM-AUX STR::CHARS STR::BAG)) (STR::CHARS (REVERSE STR::CHARS)) (STR::CHARS (STR::TRIM-AUX STR::CHARS STR::BAG)) (STR::CHARS (REVERSE STR::CHARS))) (IMPLODE STR::CHARS))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::TRIM-BAG) (:EXECUTABLE-COUNTERPART STR::TRIM-BAG)) ((:DEFINITION STR::TRIM-BAG)))) (DEFUN STR::TRIM (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (STRINGP X))) (LET* ((STR::BAG (LIST #\Space #\Tab #\Newline #\Page (CODE-CHAR 13) (CODE-CHAR 11)))) (STR::TRIM-BAG X STR::BAG))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::TRIM) (:EXECUTABLE-COUNTERPART STR::TRIM)) ((:DEFINITION STR::TRIM)))) (DEFUN STR::PREFIX-LINES-AUX (N X STR::XL STR::ACC STR::PREFIX) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (XARGS :GUARD (AND (NATP N) (STRINGP X) (NATP STR::XL) (<= N STR::XL) (= STR::XL (LENGTH X)) (STRINGP STR::PREFIX)))) (LET ((N (LNFIX N)) (STR::XL (LNFIX STR::XL))) (IF (MBE :LOGIC (ZP (- STR::XL N)) :EXEC (INT= N STR::XL)) STR::ACC (LET* ((CHAR (CHAR X N)) (STR::ACC (CONS CHAR STR::ACC)) (STR::ACC (IF (EQL CHAR #\Newline) (STR::REVAPPEND-CHARS STR::PREFIX STR::ACC) STR::ACC))) (STR::PREFIX-LINES-AUX (+ 1 N) X STR::XL STR::ACC STR::PREFIX))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PREFIX-LINES-AUX) (:EXECUTABLE-COUNTERPART STR::PREFIX-LINES-AUX)) ((:INDUCTION STR::PREFIX-LINES-AUX) (:DEFINITION STR::PREFIX-LINES-AUX)))) (DEFUN STR::PREFIX-LINES (X STR::PREFIX) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (STRINGP STR::PREFIX)))) (LET* ((STR::ACC (STR::REVAPPEND-CHARS STR::PREFIX NIL)) (STR::RCHARS (STR::PREFIX-LINES-AUX 0 X (LENGTH X) STR::ACC STR::PREFIX))) (STR::RCHARS-TO-STRING STR::RCHARS))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PREFIX-LINES) (:EXECUTABLE-COUNTERPART STR::PREFIX-LINES)) ((:DEFINITION STR::PREFIX-LINES)))) (DEFUN STR::CHARPOS-AUX (X N STR::XL CHAR) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (TYPE INTEGER N) (TYPE INTEGER STR::XL) (TYPE CHARACTER CHAR) (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (<= N STR::XL) (= STR::XL (LENGTH X))))) (MBE :LOGIC (POSITION-AC CHAR (NTHCDR N (EXPLODE X)) (NFIX N)) :EXEC (COND ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL) ((EQL (CHAR X N) CHAR) (LNFIX N)) (T (STR::CHARPOS-AUX X (+ 1 (LNFIX N)) STR::XL CHAR))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARPOS-AUX) (:EXECUTABLE-COUNTERPART STR::CHARPOS-AUX)) ((:DEFINITION STR::CHARPOS-AUX)))) (DEFUN STR::GO-TO-LINE (X N STR::XL STR::CURR STR::GOAL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (XARGS :GUARD (AND (STRINGP X) (NATP N) (NATP STR::XL) (<= N STR::XL) (= STR::XL (LENGTH X)) (NATP STR::CURR) (NATP STR::GOAL))) (TYPE STRING X) (TYPE INTEGER N STR::XL STR::CURR STR::GOAL)) (COND ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) NIL) ((INT= STR::CURR STR::GOAL) (LNFIX N)) (T (STR::GO-TO-LINE X (+ 1 (LNFIX N)) STR::XL (IF (EQL (CHAR X N) #\Newline) (+ 1 STR::CURR) STR::CURR) STR::GOAL)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::GO-TO-LINE) (:EXECUTABLE-COUNTERPART STR::GO-TO-LINE)) ((:INDUCTION STR::GO-TO-LINE) (:DEFINITION STR::GO-TO-LINE)))) (DEFUN STR::STRLINE (N X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (POSP N) (STRINGP X)))) (LET* ((X (MBE :LOGIC (IF (STRINGP X) X "") :EXEC X)) (STR::XL (LENGTH X)) (STR::START (STR::GO-TO-LINE X 0 STR::XL 1 N))) (IF (NOT STR::START) "" (LET ((STR::END (STR::CHARPOS-AUX X STR::START STR::XL #\Newline))) (SUBSEQ X STR::START STR::END))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRLINE) (:EXECUTABLE-COUNTERPART STR::STRLINE)) ((:DEFINITION STR::STRLINE)))) (DEFUN STR::STRLINES (A B X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE INTEGER A) (TYPE INTEGER B) (TYPE STRING X) (XARGS :GUARD (AND (POSP A) (POSP B) (STRINGP X)))) (LET* ((X (MBE :LOGIC (IF (STRINGP X) X "") :EXEC X)) (STR::XL (LENGTH X))) (MV-LET (A B) (IF (<= A B) (MV A B) (MV B A)) (LET ((STR::START (STR::GO-TO-LINE X 0 STR::XL 1 A))) (IF (NOT STR::START) "" (LET ((STR::END (STR::GO-TO-LINE X STR::START STR::XL A (+ 1 B)))) (SUBSEQ X STR::START STR::END))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRLINES) (:EXECUTABLE-COUNTERPART STR::STRLINES)) ((:DEFINITION STR::STRLINES)))) (DEFUN STR::PARSE-NAT-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE INTEGER STR::VAL) (TYPE INTEGER LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (MBE :LOGIC (COND ((ATOM X) (MV (NFIX STR::VAL) (NFIX LEN) NIL)) ((STR::DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN))))) (T (MV (NFIX STR::VAL) (NFIX LEN) X))) :EXEC (COND ((ATOM X) (MV STR::VAL LEN NIL)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CAR X)))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-CHARLIST (CDR X) (THE INTEGER (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE INTEGER (* 10 (THE INTEGER STR::VAL))))) (THE INTEGER (+ 1 (THE INTEGER LEN))))) (MV STR::VAL LEN X))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PARSE-NAT-FROM-CHARLIST) (:EXECUTABLE-COUNTERPART STR::PARSE-NAT-FROM-CHARLIST)) ((:INDUCTION STR::PARSE-NAT-FROM-CHARLIST) (:DEFINITION STR::PARSE-NAT-FROM-CHARLIST)))) (DEFUN STR::PARSE-NAT-FROM-STRING (X STR::VAL LEN N STR::XL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) STR::VAL LEN N STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP STR::VAL) (NATP LEN) (NATP N) (EQUAL STR::XL (LENGTH X)) (<= N STR::XL)))) (MBE :LOGIC (COND ((ZP (- (NFIX STR::XL) (NFIX N))) (MV (NFIX STR::VAL) (NFIX LEN))) ((STR::DIGITP (CHAR X N)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CHAR X N)))) (STR::PARSE-NAT-FROM-STRING X (+ STR::DIGIT-VAL (* 10 (NFIX STR::VAL))) (+ 1 (NFIX LEN)) (+ 1 (NFIX N)) (NFIX STR::XL)))) (T (MV (NFIX STR::VAL) (NFIX LEN)))) :EXEC (COND ((INT= N STR::XL) (MV STR::VAL LEN)) (T (LET ((STR::CODE (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER (CHAR (THE STRING X) (THE (INTEGER 0 *) N))))))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (IF (AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 57))) (LET ((STR::DIGIT-VAL (THE (UNSIGNED-BYTE 8) (- (THE (UNSIGNED-BYTE 8) STR::CODE) (THE (UNSIGNED-BYTE 8) 48))))) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE (INTEGER 0 *) (+ (THE (UNSIGNED-BYTE 8) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 10 (THE (INTEGER 0 *) STR::VAL))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) LEN))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) N))) (THE (INTEGER 0 *) STR::XL))) (MV STR::VAL LEN))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PARSE-NAT-FROM-STRING) (:EXECUTABLE-COUNTERPART STR::PARSE-NAT-FROM-STRING)) ((:INDUCTION STR::PARSE-NAT-FROM-STRING) (:DEFINITION STR::PARSE-NAT-FROM-STRING)))) (DEFUN STR::CHARLISTNAT< (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (CHARACTER-LISTP Y)))) (COND ((ATOM Y) NIL) ((ATOM X) T) ((AND (STR::DIGITP (CAR X)) (STR::DIGITP (CAR Y))) (B* (((MV STR::V1 STR::L1 STR::REST-X) (STR::PARSE-NAT-FROM-CHARLIST X 0 0)) ((MV STR::V2 STR::L2 STR::REST-Y) (STR::PARSE-NAT-FROM-CHARLIST Y 0 0))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::CHARLISTNAT< STR::REST-X STR::REST-Y))))) ((CHAR< (CAR X) (CAR Y)) T) ((CHAR< (CAR Y) (CAR X)) NIL) (T (STR::CHARLISTNAT< (CDR X) (CDR Y))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARLISTNAT<) (:EXECUTABLE-COUNTERPART STR::CHARLISTNAT<)) ((:INDUCTION STR::CHARLISTNAT<) (:DEFINITION STR::CHARLISTNAT<)))) (DEFUN STR::STRNAT<-AUX (X Y STR::XN STR::YN STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? Y STR::YN STR::XN X))) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER STR::XN) (TYPE INTEGER STR::YN) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (EQUAL STR::XL (LENGTH X)) (EQUAL STR::YL (LENGTH Y)) (<= STR::XN STR::XL) (<= STR::YN STR::YL))) (IGNORABLE STR::XL STR::YL)) (MBE :LOGIC (LET* ((X (IF (STRINGP X) X "")) (Y (IF (STRINGP Y) Y "")) (STR::XN (NFIX STR::XN)) (STR::YN (NFIX STR::YN)) (STR::XL (LENGTH X)) (STR::YL (LENGTH Y))) (COND ((ZP (- STR::YL STR::YN)) NIL) ((ZP (- STR::XL STR::XN)) T) ((AND (STR::DIGITP (CHAR X STR::XN)) (STR::DIGITP (CHAR Y STR::YN))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING X 0 0 STR::XN STR::XL)) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING Y 0 0 STR::YN STR::YL))) (COND ((OR (< STR::V1 STR::V2) (AND (INT= STR::V1 STR::V2) (< STR::L1 STR::L2))) T) ((OR (< STR::V2 STR::V1) (AND (INT= STR::V1 STR::V2) (< STR::L2 STR::L1))) NIL) (T (STR::STRNAT<-AUX X Y (+ STR::XN STR::L1) (+ STR::YN STR::L2) STR::XL STR::YL))))) ((CHAR< (CHAR X STR::XN) (CHAR Y STR::YN)) T) ((CHAR< (CHAR Y STR::YN) (CHAR X STR::XN)) NIL) (T (STR::STRNAT<-AUX X Y (+ 1 STR::XN) (+ 1 STR::YN) STR::XL STR::YL)))) :EXEC (COND ((INT= STR::YN STR::YL) NIL) ((INT= STR::XN STR::XL) T) (T (LET* ((STR::CHAR-X (THE CHARACTER (CHAR (THE STRING X) (THE INTEGER STR::XN)))) (STR::CHAR-Y (THE CHARACTER (CHAR (THE STRING Y) (THE INTEGER STR::YN)))) (STR::CODE-X (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-X)))) (STR::CODE-Y (THE (UNSIGNED-BYTE 8) (CHAR-CODE (THE CHARACTER STR::CHAR-Y))))) (DECLARE (TYPE CHARACTER STR::CHAR-X) (TYPE CHARACTER STR::CHAR-Y) (TYPE (UNSIGNED-BYTE 8) STR::CODE-X) (TYPE (UNSIGNED-BYTE 8) STR::CODE-Y)) (COND ((AND (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) 57)) (<= (THE (UNSIGNED-BYTE 8) 48) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) (<= (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) 57))) (B* (((MV STR::V1 STR::L1) (STR::PARSE-NAT-FROM-STRING (THE STRING X) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::XN) (THE INTEGER STR::XL))) ((MV STR::V2 STR::L2) (STR::PARSE-NAT-FROM-STRING (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER STR::YN) (THE INTEGER STR::YL)))) (COND ((OR (< (THE INTEGER STR::V1) (THE INTEGER STR::V2)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L1) (THE INTEGER STR::L2)))) T) ((OR (< (THE INTEGER STR::V2) (THE INTEGER STR::V1)) (AND (INT= STR::V1 STR::V2) (< (THE INTEGER STR::L2) (THE INTEGER STR::L1)))) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER STR::XN) (THE INTEGER STR::L1))) (THE INTEGER (+ (THE INTEGER STR::YN) (THE INTEGER STR::L2))) (THE INTEGER STR::XL) (THE INTEGER STR::YL)))))) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-X) (THE (UNSIGNED-BYTE 8) STR::CODE-Y)) T) ((< (THE (UNSIGNED-BYTE 8) STR::CODE-Y) (THE (UNSIGNED-BYTE 8) STR::CODE-X)) NIL) (T (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::XN))) (THE INTEGER (+ (THE INTEGER 1) (THE INTEGER STR::YN))) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRNAT<-AUX) (:EXECUTABLE-COUNTERPART STR::STRNAT<-AUX)) ((:INDUCTION STR::STRNAT<-AUX) (:DEFINITION STR::STRNAT<-AUX)))) (DEFUN STR::STRNAT<$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (STR::CHARLISTNAT< (EXPLODE X) (EXPLODE Y)) :EXEC (STR::STRNAT<-AUX (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRNAT<$INLINE) (:EXECUTABLE-COUNTERPART STR::STRNAT<$INLINE)) ((:DEFINITION STR::STRNAT<$INLINE)))) (DEFMACRO STR::STRNAT< (X Y) (LIST (QUOTE STR::STRNAT<$INLINE) X Y)) (DEFUN STR::STRPREFIXP-IMPL (X Y STR::XN STR::YN STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? STR::YN STR::YL STR::XN STR::XL))) (DECLARE (TYPE STRING X) (TYPE STRING Y) (TYPE INTEGER STR::XN) (TYPE INTEGER STR::YN) (TYPE INTEGER STR::XL) (TYPE INTEGER STR::YL) (XARGS :GUARD (AND (STRINGP X) (STRINGP Y) (NATP STR::XN) (NATP STR::YN) (NATP STR::XL) (NATP STR::YL) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y)) (<= STR::XN (LENGTH X)) (<= STR::YN (LENGTH Y))))) (COND ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX STR::XN))) :EXEC (INT= STR::XN STR::XL)) T) ((MBE :LOGIC (ZP (- (NFIX STR::YL) (NFIX STR::YN))) :EXEC (INT= STR::YN STR::YL)) NIL) ((EQL (THE CHARACTER (CHAR X STR::XN)) (THE CHARACTER (CHAR Y STR::YN))) (MBE :LOGIC (STR::STRPREFIXP-IMPL X Y (+ (NFIX STR::XN) 1) (+ (NFIX STR::YN) 1) STR::XL STR::YL) :EXEC (STR::STRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE INTEGER (+ (THE INTEGER STR::XN) 1)) (THE INTEGER (+ (THE INTEGER STR::YN) 1)) (THE INTEGER STR::XL) (THE INTEGER STR::YL)))) (T NIL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRPREFIXP-IMPL) (:EXECUTABLE-COUNTERPART STR::STRPREFIXP-IMPL)) ((:INDUCTION STR::STRPREFIXP-IMPL) (:DEFINITION STR::STRPREFIXP-IMPL)))) (DEFUN STR::STRPREFIXP$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X) (TYPE STRING Y)) (MBE :LOGIC (PREFIXP (EXPLODE X) (EXPLODE Y)) :EXEC (STR::STRPREFIXP-IMPL (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRPREFIXP$INLINE) (:EXECUTABLE-COUNTERPART STR::STRPREFIXP$INLINE) (:DEFINITION STR::STRPREFIXP$INLINE)) NIL)) (DEFMACRO STR::STRPREFIXP (X Y) (LIST (QUOTE STR::STRPREFIXP$INLINE) X Y)) (DEFUN STR::STRPOS-FAST (X Y N STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N 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 STR::XL) (NATP STR::YL) (NATP N) (<= N (LENGTH Y)) (= STR::XL (LENGTH X)) (= STR::YL (LENGTH Y))))) (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 N) (THE INTEGER STR::XL) (THE INTEGER STR::YL))) (LNFIX N)) ((MBE :LOGIC (ZP (- (NFIX STR::YL) (NFIX N))) :EXEC (INT= N STR::YL)) NIL) (T (STR::STRPOS-FAST (THE STRING X) (THE STRING Y) (+ 1 (LNFIX N)) (THE INTEGER STR::XL) (THE INTEGER STR::YL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRPOS-FAST) (:EXECUTABLE-COUNTERPART STR::STRPOS-FAST)) ((:INDUCTION STR::STRPOS-FAST) (:DEFINITION STR::STRPOS-FAST)))) (DEFUN STR::STRPOS$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (LISTPOS (EXPLODE X) (EXPLODE Y)) :EXEC (STR::STRPOS-FAST (THE STRING X) (THE STRING Y) (THE INTEGER 0) (THE INTEGER (LENGTH (THE STRING X))) (THE INTEGER (LENGTH (THE STRING Y)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRPOS$INLINE) (:EXECUTABLE-COUNTERPART STR::STRPOS$INLINE) (:DEFINITION STR::STRPOS$INLINE)) NIL)) (DEFMACRO STR::STRPOS (X Y) (LIST (QUOTE STR::STRPOS$INLINE) X Y)) (DEFUN STR::STRRPOS-FAST (X Y N STR::XL STR::YL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N))) (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))))) (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))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRRPOS-FAST) (:EXECUTABLE-COUNTERPART STR::STRRPOS-FAST)) ((:INDUCTION STR::STRRPOS-FAST) (:DEFINITION STR::STRRPOS-FAST)))) (DEFUN STR::STRRPOS$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (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)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRRPOS$INLINE) (:EXECUTABLE-COUNTERPART STR::STRRPOS$INLINE)) ((:DEFINITION STR::STRRPOS$INLINE)))) (DEFMACRO STR::STRRPOS (X Y) (LIST (QUOTE STR::STRRPOS$INLINE) X Y)) (DEFUN STR::SPLIT-LIST-1 (X STR::DEL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD T)) (COND ((ATOM X) (MV NIL NIL)) ((EQUAL (CAR X) STR::DEL) (MV NIL (CDR X))) (T (MV-LET (STR::PART1 STR::PART2) (STR::SPLIT-LIST-1 (CDR X) STR::DEL) (MV (CONS (CAR X) STR::PART1) STR::PART2))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::SPLIT-LIST-1) (:EXECUTABLE-COUNTERPART STR::SPLIT-LIST-1)) ((:INDUCTION STR::SPLIT-LIST-1) (:DEFINITION STR::SPLIT-LIST-1)))) (DEFUN STR::SPLIT-LIST* (X STR::DEL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD T)) (IF (ATOM X) NIL (MV-LET (STR::FIRST1 X) (STR::SPLIT-LIST-1 X STR::DEL) (IF STR::FIRST1 (CONS STR::FIRST1 (STR::SPLIT-LIST* X STR::DEL)) (STR::SPLIT-LIST* X STR::DEL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::SPLIT-LIST*) (:EXECUTABLE-COUNTERPART STR::SPLIT-LIST*)) ((:INDUCTION STR::SPLIT-LIST*) (:DEFINITION STR::SPLIT-LIST*)))) (DEFUN STR::CHARACTER-LIST-LISTP (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD T)) (IF (CONSP X) (AND (CHARACTER-LISTP (CAR X)) (STR::CHARACTER-LIST-LISTP (CDR X))) T)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::CHARACTER-LIST-LISTP) (:EXECUTABLE-COUNTERPART STR::CHARACTER-LIST-LISTP)) ((:INDUCTION STR::CHARACTER-LIST-LISTP) (:DEFINITION STR::CHARACTER-LIST-LISTP)))) (DEFUN STR::COERCE-LIST-TO-STRINGS (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (STR::CHARACTER-LIST-LISTP X))) (IF (CONSP X) (CONS (COERCE (CAR X) (QUOTE STRING)) (STR::COERCE-LIST-TO-STRINGS (CDR X))) NIL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::COERCE-LIST-TO-STRINGS) (:EXECUTABLE-COUNTERPART STR::COERCE-LIST-TO-STRINGS)) ((:INDUCTION STR::COERCE-LIST-TO-STRINGS) (:DEFINITION STR::COERCE-LIST-TO-STRINGS)))) (DEFUN STR::STRSPLIT (X STR::DEL) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (CHARACTERP STR::DEL)))) (STR::COERCE-LIST-TO-STRINGS (STR::SPLIT-LIST* (COERCE X (QUOTE LIST)) STR::DEL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRSPLIT) (:EXECUTABLE-COUNTERPART STR::STRSPLIT)) ((:DEFINITION STR::STRSPLIT)))) (DEFUN STR::STRSUBST-AUX (STR::OLD STR::NEW X N STR::XL STR::OLDL STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING STR::OLD STR::NEW X) (TYPE (INTEGER 0 *) N STR::XL STR::OLDL) (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X) (NATP N) (NATP STR::XL) (POSP STR::OLDL) (= STR::OLDL (LENGTH STR::OLD)) (= STR::XL (LENGTH X))))) (COND ((MBE :LOGIC (ZP STR::OLDL) :EXEC NIL) STR::ACC) ((MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (>= N STR::XL)) STR::ACC) ((STR::STRPREFIXP-IMPL STR::OLD X 0 N STR::OLDL STR::XL) (LET ((STR::ACC (STR::REVAPPEND-CHARS STR::NEW STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ STR::OLDL (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))) (T (LET ((STR::ACC (CONS (CHAR X N) STR::ACC))) (STR::STRSUBST-AUX STR::OLD STR::NEW X (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX N)))) STR::XL STR::OLDL STR::ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRSUBST-AUX) (:EXECUTABLE-COUNTERPART STR::STRSUBST-AUX)) ((:INDUCTION STR::STRSUBST-AUX) (:DEFINITION STR::STRSUBST-AUX)))) (DEFUN STR::STRSUBST (STR::OLD STR::NEW X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRINGP X)))) (LET ((STR::OLDL (MBE :LOGIC (LEN (EXPLODE STR::OLD)) :EXEC (LENGTH STR::OLD)))) (IF (ZP STR::OLDL) (MBE :LOGIC (STR::STR-FIX X) :EXEC X) (STR::RCHARS-TO-STRING (STR::STRSUBST-AUX STR::OLD STR::NEW X 0 (LENGTH X) STR::OLDL NIL))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRSUBST) (:EXECUTABLE-COUNTERPART STR::STRSUBST)) ((:DEFINITION STR::STRSUBST)))) (DEFUN STR::STRSUBST-LIST (STR::OLD STR::NEW X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRINGP STR::OLD) (STRINGP STR::NEW) (STRING-LISTP X)))) (IF (ATOM X) NIL (CONS (STR::STRSUBST STR::OLD STR::NEW (CAR X)) (STR::STRSUBST-LIST STR::OLD STR::NEW (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRSUBST-LIST) (:EXECUTABLE-COUNTERPART STR::STRSUBST-LIST)) ((:INDUCTION STR::STRSUBST-LIST) (:DEFINITION STR::STRSUBST-LIST)))) (DEFUN STR::STRTOK-AUX (X N STR::XL STR::DELIMITERS STR::CURR STR::ACC) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? N STR::XL))) (DECLARE (TYPE STRING X) (TYPE (INTEGER 0 *) N STR::XL) (XARGS :GUARD (AND (STRINGP X) (NATP STR::XL) (NATP N) (= STR::XL (LENGTH X)) (<= N STR::XL) (CHARACTER-LISTP STR::DELIMITERS) (CHARACTER-LISTP STR::CURR) (STRING-LISTP STR::ACC)))) (IF (MBE :LOGIC (ZP (- (NFIX STR::XL) (NFIX N))) :EXEC (INT= N STR::XL)) (IF STR::CURR (CONS (STR::RCHARS-TO-STRING STR::CURR) STR::ACC) STR::ACC) (LET* ((STR::CHAR1 (CHAR X N)) (STR::MATCHP (MEMBER STR::CHAR1 STR::DELIMITERS))) (STR::STRTOK-AUX (THE STRING X) (THE (INTEGER 0 *) (+ 1 (LNFIX N))) (THE INTEGER STR::XL) STR::DELIMITERS (IF STR::MATCHP NIL (CONS STR::CHAR1 STR::CURR)) (IF (AND STR::MATCHP STR::CURR) (CONS (STR::RCHARS-TO-STRING STR::CURR) STR::ACC) STR::ACC))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRTOK-AUX) (:EXECUTABLE-COUNTERPART STR::STRTOK-AUX)) ((:INDUCTION STR::STRTOK-AUX) (:DEFINITION STR::STRTOK-AUX)))) (DEFUN STR::STRTOK$INLINE (X STR::DELIMITERS) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (STRINGP X) (CHARACTER-LISTP STR::DELIMITERS)))) (LET ((STR::RTOKENS (STR::STRTOK-AUX X 0 (MBE :LOGIC (LEN (EXPLODE X)) :EXEC (LENGTH X)) STR::DELIMITERS NIL NIL))) (MBE :LOGIC (REV STR::RTOKENS) :EXEC (REVERSE STR::RTOKENS)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRTOK$INLINE) (:EXECUTABLE-COUNTERPART STR::STRTOK$INLINE)) ((:DEFINITION STR::STRTOK$INLINE)))) (DEFMACRO STR::STRTOK (X STR::DELIMITERS) (LIST (QUOTE STR::STRTOK$INLINE) X STR::DELIMITERS)) (DEFUN STR::OCTAL-DIGITP$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\7))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::OCTAL-DIGITP$INLINE) (:EXECUTABLE-COUNTERPART STR::OCTAL-DIGITP$INLINE)) ((:DEFINITION STR::OCTAL-DIGITP$INLINE)))) (DEFMACRO STR::OCTAL-DIGITP (X) (LIST (QUOTE STR::OCTAL-DIGITP$INLINE) X)) (DEFUN STR::OCTAL-DIGIT-LISTP (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::OCTAL-DIGITP (CAR X)) (STR::OCTAL-DIGIT-LISTP (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::OCTAL-DIGIT-LISTP) (:EXECUTABLE-COUNTERPART STR::OCTAL-DIGIT-LISTP)) ((:INDUCTION STR::OCTAL-DIGIT-LISTP) (:DEFINITION STR::OCTAL-DIGIT-LISTP)))) (DEFUN STR::PARSE-OCTAL-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::OCTAL-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::DIGIT-VAL (CAR X)))) (STR::PARSE-OCTAL-FROM-CHARLIST (CDR X) (+ STR::DIGIT-VAL (* 8 (LNFIX STR::VAL))) (+ 1 (LNFIX LEN))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PARSE-OCTAL-FROM-CHARLIST) (:EXECUTABLE-COUNTERPART STR::PARSE-OCTAL-FROM-CHARLIST)) ((:INDUCTION STR::PARSE-OCTAL-FROM-CHARLIST) (:DEFINITION STR::PARSE-OCTAL-FROM-CHARLIST)))) (DEFUN STR::OCTAL-DIGIT-LIST-VALUE$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::OCTAL-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-OCTAL-FROM-CHARLIST X 0 0))) STR::VAL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::OCTAL-DIGIT-LIST-VALUE$INLINE) (:EXECUTABLE-COUNTERPART STR::OCTAL-DIGIT-LIST-VALUE$INLINE)) ((:DEFINITION STR::OCTAL-DIGIT-LIST-VALUE$INLINE)))) (DEFMACRO STR::OCTAL-DIGIT-LIST-VALUE (X) (LIST (QUOTE STR::OCTAL-DIGIT-LIST-VALUE$INLINE) X)) (DEFUN STR::HEX-DIGITP$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE CHARACTER X)) (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (OR (AND (<= (CHAR-CODE #\0) STR::CODE) (<= STR::CODE (CHAR-CODE #\9))) (AND (<= (CHAR-CODE #\a) STR::CODE) (<= STR::CODE (CHAR-CODE #\f))) (AND (<= (CHAR-CODE #\A) STR::CODE) (<= STR::CODE (CHAR-CODE #\F)))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HEX-DIGITP$INLINE) (:EXECUTABLE-COUNTERPART STR::HEX-DIGITP$INLINE)) ((:DEFINITION STR::HEX-DIGITP$INLINE)))) (DEFMACRO STR::HEX-DIGITP (X) (LIST (QUOTE STR::HEX-DIGITP$INLINE) X)) (DEFUN STR::HEX-DIGIT-LISTP (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (CHARACTER-LISTP X))) (IF (ATOM X) T (AND (STR::HEX-DIGITP (CAR X)) (STR::HEX-DIGIT-LISTP (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HEX-DIGIT-LISTP) (:EXECUTABLE-COUNTERPART STR::HEX-DIGIT-LISTP)) ((:INDUCTION STR::HEX-DIGIT-LISTP) (:DEFINITION STR::HEX-DIGIT-LISTP)))) (DEFUN STR::HEX-DIGIT-VAL$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTERP X) (STR::HEX-DIGITP X)))) (IF (MBE :LOGIC (NOT (STR::HEX-DIGITP X)) :EXEC NIL) 0 (LET ((STR::CODE (CHAR-CODE (MBE :LOGIC (STR::CHAR-FIX X) :EXEC X)))) (DECLARE (TYPE (UNSIGNED-BYTE 8) STR::CODE)) (COND ((<= (CHAR-CODE #\a) STR::CODE) (- STR::CODE (- (CHAR-CODE #\a) 10))) ((<= (CHAR-CODE #\A) STR::CODE) (- STR::CODE (- (CHAR-CODE #\A) 10))) (T (- STR::CODE (CHAR-CODE #\0))))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HEX-DIGIT-VAL$INLINE) (:EXECUTABLE-COUNTERPART STR::HEX-DIGIT-VAL$INLINE)) ((:DEFINITION STR::HEX-DIGIT-VAL$INLINE)))) (DEFMACRO STR::HEX-DIGIT-VAL (X) (LIST (QUOTE STR::HEX-DIGIT-VAL$INLINE) X)) (DEFUN STR::PARSE-HEX-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((STR::HEX-DIGITP (CAR X)) (LET ((STR::DIGIT-VAL (STR::HEX-DIGIT-VAL (CAR X)))) (STR::PARSE-HEX-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ (THE (INTEGER 0 *) STR::DIGIT-VAL) (THE (INTEGER 0 *) (* 16 (THE (INTEGER 0 *) (LNFIX STR::VAL)))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN))))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PARSE-HEX-FROM-CHARLIST) (:EXECUTABLE-COUNTERPART STR::PARSE-HEX-FROM-CHARLIST)) ((:INDUCTION STR::PARSE-HEX-FROM-CHARLIST) (:DEFINITION STR::PARSE-HEX-FROM-CHARLIST)))) (DEFUN STR::HEX-DIGIT-LIST-VALUE$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::HEX-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-HEX-FROM-CHARLIST X 0 0))) STR::VAL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::HEX-DIGIT-LIST-VALUE$INLINE) (:EXECUTABLE-COUNTERPART STR::HEX-DIGIT-LIST-VALUE$INLINE)) ((:DEFINITION STR::HEX-DIGIT-LIST-VALUE$INLINE)))) (DEFMACRO STR::HEX-DIGIT-LIST-VALUE (X) (LIST (QUOTE STR::HEX-DIGIT-LIST-VALUE$INLINE) X)) (DEFUN STR::BIT-DIGITP$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (OR (EQL X #\0) (EQL X #\1))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::BIT-DIGITP$INLINE) (:EXECUTABLE-COUNTERPART STR::BIT-DIGITP$INLINE)) ((:DEFINITION STR::BIT-DIGITP$INLINE)))) (DEFMACRO STR::BIT-DIGITP (X) (LIST (QUOTE STR::BIT-DIGITP$INLINE) X)) (DEFUN STR::BIT-DIGIT-LISTP (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD T)) (IF (ATOM X) T (AND (STR::BIT-DIGITP (CAR X)) (STR::BIT-DIGIT-LISTP (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::BIT-DIGIT-LISTP) (:EXECUTABLE-COUNTERPART STR::BIT-DIGIT-LISTP)) ((:INDUCTION STR::BIT-DIGIT-LISTP) (:DEFINITION STR::BIT-DIGIT-LISTP)))) (DEFUN STR::BITSTRING-P (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD T)) (AND (STRINGP X) (STR::BIT-DIGIT-LISTP (EXPLODE X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::BITSTRING-P) (:EXECUTABLE-COUNTERPART STR::BITSTRING-P)) ((:DEFINITION STR::BITSTRING-P)))) (DEFUN STR::PARSE-BITS-FROM-CHARLIST (X STR::VAL LEN) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (TYPE (INTEGER 0 *) STR::VAL LEN) (XARGS :GUARD (AND (CHARACTER-LISTP X) (NATP STR::VAL) (NATP LEN)))) (COND ((ATOM X) (MV (LNFIX STR::VAL) (LNFIX LEN) NIL)) ((EQL (CAR X) #\0) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) ((EQL (CAR X) #\1) (STR::PARSE-BITS-FROM-CHARLIST (CDR X) (THE (INTEGER 0 *) (+ 1 (MBE :LOGIC (* 2 (NFIX STR::VAL)) :EXEC (THE (INTEGER 0 *) (ASH STR::VAL 1))))) (THE (INTEGER 0 *) (+ 1 (THE (INTEGER 0 *) (LNFIX LEN)))))) (T (MV (LNFIX STR::VAL) (LNFIX LEN) X)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::PARSE-BITS-FROM-CHARLIST) (:EXECUTABLE-COUNTERPART STR::PARSE-BITS-FROM-CHARLIST)) ((:INDUCTION STR::PARSE-BITS-FROM-CHARLIST) (:DEFINITION STR::PARSE-BITS-FROM-CHARLIST)))) (DEFUN STR::BIT-DIGIT-LIST-VALUE$INLINE (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (AND (CHARACTER-LISTP X) (STR::BIT-DIGIT-LISTP X)))) (B* (((MV STR::VAL STR::?LEN STR::?REST) (STR::PARSE-BITS-FROM-CHARLIST X 0 0))) STR::VAL)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::BIT-DIGIT-LIST-VALUE$INLINE) (:EXECUTABLE-COUNTERPART STR::BIT-DIGIT-LIST-VALUE$INLINE)) ((:DEFINITION STR::BIT-DIGIT-LIST-VALUE$INLINE)))) (DEFMACRO STR::BIT-DIGIT-LIST-VALUE (X) (LIST (QUOTE STR::BIT-DIGIT-LIST-VALUE$INLINE) X)) (DEFUN STR::STRVAL (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (B* (((THE (INTEGER 0 *) STR::XL) (MBE :LOGIC (LEN (EXPLODE X)) :EXEC (LENGTH X))) ((MV (THE (INTEGER 0 *) STR::VAL) (THE (INTEGER 0 *) LEN)) (STR::PARSE-NAT-FROM-STRING X 0 0 0 STR::XL))) (AND (< 0 LEN) (INT= LEN STR::XL) STR::VAL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRVAL) (:EXECUTABLE-COUNTERPART STR::STRVAL)) ((:DEFINITION STR::STRVAL)))) (DEFUN STR::STRVAL8 (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::OCTAL-DIGIT-LISTP STR::CHARS) (STR::OCTAL-DIGIT-LIST-VALUE STR::CHARS)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRVAL8) (:EXECUTABLE-COUNTERPART STR::STRVAL8)) ((:DEFINITION STR::STRVAL8)))) (DEFUN STR::STRVAL16 (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::HEX-DIGIT-LISTP STR::CHARS) (STR::HEX-DIGIT-LIST-VALUE STR::CHARS)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRVAL16) (:EXECUTABLE-COUNTERPART STR::STRVAL16)) ((:DEFINITION STR::STRVAL16)))) (DEFUN STR::STRVAL2 (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X)) (LET ((STR::CHARS (EXPLODE X))) (AND (CONSP STR::CHARS) (STR::BIT-DIGIT-LISTP STR::CHARS) (STR::BIT-DIGIT-LIST-VALUE STR::CHARS)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRVAL2) (:EXECUTABLE-COUNTERPART STR::STRVAL2)) ((:DEFINITION STR::STRVAL2)))) (DEFUN STR::SUBSTRP$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (TYPE STRING X Y)) (MBE :LOGIC (SUBLISTP (EXPLODE X) (EXPLODE Y)) :EXEC (IF (STR::STRPOS X Y) T NIL))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::SUBSTRP$INLINE) (:EXECUTABLE-COUNTERPART STR::SUBSTRP$INLINE) (:DEFINITION STR::SUBSTRP$INLINE)) NIL)) (DEFMACRO STR::SUBSTRP (X Y) (LIST (QUOTE STR::SUBSTRP$INLINE) X Y)) (DEFUN STR::STRSUFFIXP$INLINE (X Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (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))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::STRSUFFIXP$INLINE) (:EXECUTABLE-COUNTERPART STR::STRSUFFIXP$INLINE)) ((:DEFINITION STR::STRSUFFIXP$INLINE)))) (DEFMACRO STR::STRSUFFIXP (X Y) (LIST (QUOTE STR::STRSUFFIXP$INLINE) X Y)) (DEFUN STR::SYMBOL-LIST-NAMES (X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (SYMBOL-LISTP X))) (IF (ATOM X) NIL (CONS (SYMBOL-NAME (CAR X)) (STR::SYMBOL-LIST-NAMES (CDR X))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::SYMBOL-LIST-NAMES) (:EXECUTABLE-COUNTERPART STR::SYMBOL-LIST-NAMES)) ((:INDUCTION STR::SYMBOL-LIST-NAMES) (:DEFINITION STR::SYMBOL-LIST-NAMES)))) (DEFUN STR::INTERN-LIST-FN (X STR::PKG) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :MEASURE (:? X))) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (SYMBOLP STR::PKG)))) (IF (ATOM X) NIL (CONS (INTERN-IN-PACKAGE-OF-SYMBOL (CAR X) STR::PKG) (STR::INTERN-LIST-FN (CDR X) STR::PKG)))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION STR::INTERN-LIST-FN) (:EXECUTABLE-COUNTERPART STR::INTERN-LIST-FN)) ((:INDUCTION STR::INTERN-LIST-FN) (:DEFINITION STR::INTERN-LIST-FN)))) (DEFMACRO STR::INTERN-LIST (X &OPTIONAL (STR::PKG (QUOTE (QUOTE ACL2-PKG-WITNESS)))) (CONS (QUOTE STR::INTERN-LIST-FN) (CONS X (CONS STR::PKG (QUOTE NIL))))))))
(("/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/defs.lisp" "defs" "defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1131369726) (LOCAL ("/usr/share/acl2-6.3/books/cutil/defredundant.lisp" "cutil/defredundant" "defredundant" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1198380940)) (LOCAL ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020)) (LOCAL ("/usr/share/acl2-6.3/books/str/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1717362461)) (LOCAL ("/usr/share/acl2-6.3/books/str/symbols.lisp" "symbols" "symbols" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 811693364)) (LOCAL ("/usr/share/acl2-6.3/books/str/suffixp.lisp" "suffixp" "suffixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1217176423)) (LOCAL ("/usr/share/acl2-6.3/books/str/substrp.lisp" "substrp" "substrp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 139343620)) (LOCAL ("/usr/share/acl2-6.3/books/str/strval.lisp" "strval" "strval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1981642498)) (LOCAL ("/usr/share/acl2-6.3/books/str/strtok.lisp" "strtok" "strtok" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1082657979)) (LOCAL ("/usr/share/acl2-6.3/books/str/strsubst.lisp" "strsubst" "strsubst" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1100185597)) (LOCAL ("/usr/share/acl2-6.3/books/str/strsplit.lisp" "strsplit" "strsplit" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1851472056)) (LOCAL ("/usr/share/acl2-6.3/books/str/strnatless.lisp" "strnatless" "strnatless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797808730)) (LOCAL ("/usr/share/acl2-6.3/books/str/strrpos.lisp" "strrpos" "strrpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1502347794)) (LOCAL ("/usr/share/acl2-6.3/books/str/strpos.lisp" "strpos" "strpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 35435295)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "std/lists/sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/str/strprefixp.lisp" "strprefixp" "strprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2141614236)) (LOCAL ("/usr/share/acl2-6.3/books/str/prefix-lines.lisp" "prefix-lines" "prefix-lines" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 747083898)) (LOCAL ("/usr/share/acl2-6.3/books/str/pad.lisp" "pad" "pad" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 724548430)) (LOCAL ("/usr/share/acl2-6.3/books/str/strline.lisp" "strline" "strline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 771995942)) (LOCAL ("/usr/share/acl2-6.3/books/str/natstr.lisp" "natstr" "natstr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1696407817)) (LOCAL ("/usr/share/acl2-6.3/books/str/isubstrp.lisp" "isubstrp" "isubstrp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 536022649)) (LOCAL ("/usr/share/acl2-6.3/books/str/istrpos.lisp" "istrpos" "istrpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 683068330)) (LOCAL ("/usr/share/acl2-6.3/books/str/istrprefixp.lisp" "istrprefixp" "istrprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1923285590)) (LOCAL ("/usr/share/acl2-6.3/books/str/isort.lisp" "isort" "isort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053063794)) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/string-listp.lisp" "std/typed-lists/string-listp" "string-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 988699164)) (LOCAL ("/usr/share/acl2-6.3/books/cutil/deflist.lisp" "cutil/deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857676809)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "std/osets/under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) (LOCAL ("/usr/share/acl2-6.3/books/cutil/maybe-defthm.lisp" "maybe-defthm" "maybe-defthm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 169275099)) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) (LOCAL ("/usr/share/acl2-6.3/books/defsort/duplicated-members.lisp" "defsort/duplicated-members" "duplicated-members" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720301003)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/uniquep.lisp" "uniquep" "uniquep" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1350027706)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort" "defsort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 284418813)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/top.lisp" "std/osets/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2045504100)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "std/lists/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/sort.lisp" "sort" "sort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 335087178)) (LOCAL ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/outer.lisp" "outer" "outer" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883866964)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/cardinality.lisp" "cardinality" "cardinality" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 101478632)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/difference.lisp" "difference" "difference" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1211437825)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/intersect.lisp" "intersect" "intersect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 464592124)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/union.lisp" "union" "union" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 895011797)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/delete.lisp" "delete" "delete" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 929878553)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48714967)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392002111)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 537896665)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1528243117)) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order.lisp" "misc/total-order" "total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619824963)) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order-bsd.lisp" "total-order-bsd" "total-order-bsd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449327279)) (LOCAL ("/usr/share/acl2-6.3/books/str/cat.lisp" "str/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912)) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 285905462)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort/defsort" "defsort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 284418813)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic.lisp" "generic" "generic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 992283938)) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic-impl.lisp" "generic-impl" "generic-impl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 154835353)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-lemmas.lisp" "ihs/ihs-lemmas" "ihs-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685360399)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-lemmas.lisp" "logops-lemmas" "logops-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 998280003)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-definitions.lisp" "logops-definitions" "logops-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2048680937)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/basic-definitions.lisp" "basic-definitions" "basic-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1383521171)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 603178913)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2130795727)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1617928370)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1992988803)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/utilities.lisp" "data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1536684829)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1486104990)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-doc-topic.lisp" "ihs-doc-topic" "ihs-doc-topic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 664631734)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/no-duplicatesp.lisp" "std/lists/no-duplicatesp" "no-duplicatesp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 334869696)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "std/lists/revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "std/lists/duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/str/iless.lisp" "iless" "iless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 267906057)) (LOCAL ("/usr/share/acl2-6.3/books/str/iprefixp.lisp" "iprefixp" "iprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1865764102)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "std/lists/prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/str/html-encode.lisp" "html-encode" "html-encode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1014597130)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 248299501)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915259697)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 732116275)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105657945)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 864029516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 750113408)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1374753694)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122664565)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013733040)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061645425)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619080936)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 972646001)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 384804126)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1113724693)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 483566967)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 457663279)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134470975)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 784695287)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2126151702)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653127144)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1661395704)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1273493319)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 508744284)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061889192)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153949377)) (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)) (LOCAL ("/usr/share/acl2-6.3/books/str/firstn-chars.lisp" "firstn-chars" "firstn-chars" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2075748192)) (LOCAL ("/usr/share/acl2-6.3/books/str/digitp.lisp" "digitp" "digitp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479290421)) (LOCAL ("/usr/share/acl2-6.3/books/str/case-conversion.lisp" "case-conversion" "case-conversion" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 646818128)) (LOCAL ("/usr/share/acl2-6.3/books/str/subseq.lisp" "subseq" "subseq" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1507065012)) (LOCAL ("/usr/share/acl2-6.3/books/str/cat.lisp" "cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912)) (LOCAL ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362)) (LOCAL ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298)) (LOCAL ("/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" "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)) (LOCAL ("/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/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556)) (LOCAL ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851)) (LOCAL ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648)) ("/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/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (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)) (LOCAL ("/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/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "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)) (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/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/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/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/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))
1821912046
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / defs.cert
