acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / pad.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (DEFSECTION STR::PAD-TRIM :PARENTS (STR) :SHORT "Functions for trimming whitespace and padding with spaces.") (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::PAD-TRIM)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::PAD-TRIM)) (XDOC::PARENTS (QUOTE (STR))) (XDOC::SHORT (QUOTE "Functions for trimming whitespace and padding with spaces.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::PAD-TRIM))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::PAD-TRIM) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR) (:SHORT . "Functions for trimming whitespace and padding with spaces.") (:LONG . "

") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::PAD-TRIM)))))) (VALUE-TRIPLE (QUOTE STR::PAD-TRIM))))) (7 RECORD-EXPANSION (DEFSECTION STR::RPADCHARS :PARENTS (STR::PAD-TRIM) :SHORT "Pad a character-list with spaces on the right." :LONG "<p>@(call rpadchars) extends the character list @('x') to length
@('len') by adding spaces on the right.  For instance,</p>

@({
  (rpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\f #\\o #\\o #\\Space #\\Space)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>" (DEFUND STR::RPADCHARS (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::RPADCHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-RPADCHARS (CHARACTER-LISTP (STR::RPADCHARS X LEN))) (DEFTHM STR::LEN-OF-RPADCHARS (EQUAL (LEN (STR::RPADCHARS X LEN)) (MAX (LEN X) (NFIX LEN)))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::RPADCHARS X LEN) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::RPADCHARS X LEN) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::RPADCHARS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::RPADCHARS (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::RPADCHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-RPADCHARS (CHARACTER-LISTP (STR::RPADCHARS X LEN))) (DEFTHM STR::LEN-OF-RPADCHARS (EQUAL (LEN (STR::RPADCHARS X LEN)) (MAX (LEN X) (NFIX LEN)))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::RPADCHARS X LEN) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::RPADCHARS X LEN) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::RPADCHARS)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Pad a character-list with spaces on the right.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::RPADCHARS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call rpadchars) extends the character list @('x') to length
@('len') by adding spaces on the right.  For instance,</p>

@({
  (rpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\f #\\o #\\o #\\Space #\\Space)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::RPADCHARS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Pad a character-list with spaces on the right.") (:LONG . "<p>@(call rpadchars) extends the character list @('x') to length
@('len') by adding spaces on the right.  For instance,</p>

@({
  (rpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\f #\\o #\\o #\\Space #\\Space)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|RPADCHARS|)
@(def |STR|::|CHARACTER-LISTP-OF-RPADCHARS|)
@(def |STR|::|LEN-OF-RPADCHARS|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-RPADCHARS-1|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-RPADCHARS-1|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::RPADCHARS)))))) (VALUE-TRIPLE (QUOTE STR::RPADCHARS))))) (8 RECORD-EXPANSION (DEFSECTION STR::RPADSTR :PARENTS (STR::PAD-TRIM) :SHORT "Pad a string with spaces on the right." :LONG "<p>@(call rpadstr) extends the string @('x') to length @('len') by
adding spaces on the right.  For instance,</p>

@({
  (rpadchars \"foo\" 5)
     -->
  \"foo  \"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing or
coercion is performed.</p>" (LOCAL (IN-THEORY (ENABLE STR::RPADCHARS STR::APPEND-CHARS))) (DEFUND STR::RPADSTR (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::RPADSTR))) (DEFTHM STR::STRINGP-OF-RPADSTR (STRINGP (STR::RPADSTR X LEN)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::LEN-OF-EXPLODE-OF-RPADSTR (IMPLIES (FORCE (STRINGP X)) (EQUAL (LEN (EXPLODE (STR::RPADSTR X LEN))) (MAX (LENGTH X) (NFIX LEN))))) (DEFCONG STR::STREQV EQUAL (STR::RPADSTR X LEN) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::RPADSTR X LEN) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::RPADSTR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE STR::RPADCHARS STR::APPEND-CHARS))) (DEFUND STR::RPADSTR (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::RPADSTR))) (DEFTHM STR::STRINGP-OF-RPADSTR (STRINGP (STR::RPADSTR X LEN)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::LEN-OF-EXPLODE-OF-RPADSTR (IMPLIES (FORCE (STRINGP X)) (EQUAL (LEN (EXPLODE (STR::RPADSTR X LEN))) (MAX (LENGTH X) (NFIX LEN))))) (DEFCONG STR::STREQV EQUAL (STR::RPADSTR X LEN) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::RPADSTR X LEN) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::RPADSTR)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Pad a string with spaces on the right.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::RPADSTR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call rpadstr) extends the string @('x') to length @('len') by
adding spaces on the right.  For instance,</p>

@({
  (rpadchars \"foo\" 5)
     -->
  \"foo  \"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing or
coercion is performed.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::RPADSTR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Pad a string with spaces on the right.") (:LONG . "<p>@(call rpadstr) extends the string @('x') to length @('len') by
adding spaces on the right.  For instance,</p>

@({
  (rpadchars \"foo\" 5)
     -->
  \"foo  \"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing or
coercion is performed.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|RPADSTR|)
@(def |STR|::|STRINGP-OF-RPADSTR|)
@(def |STR|::|LEN-OF-EXPLODE-OF-RPADSTR|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-RPADSTR-1|)
@(def |STR|::|ISTREQV-IMPLIES-ISTREQV-RPADSTR-1|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::RPADSTR)))))) (VALUE-TRIPLE (QUOTE STR::RPADSTR))))) (9 RECORD-EXPANSION (DEFSECTION STR::LPADCHARS :PARENTS (STR::PAD-TRIM) :SHORT "Pad a character-list with spaces on the left." :LONG "<p>@(call lpadchars) extends the character list @('x') to length
@('len') by adding spaces on the left.  For instance,</p>

@({
  (lpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\Space #\\Space #\\f #\\o #\\o)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>" (DEFUND STR::LPADCHARS (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::LPADCHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-LPADCHARS (CHARACTER-LISTP (STR::LPADCHARS X LEN))) (DEFTHM STR::LEN-OF-LPADCHARS (EQUAL (LEN (STR::LPADCHARS X LEN)) (MAX (LEN X) (NFIX LEN)))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::LPADCHARS X LEN) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::LPADCHARS X LEN) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::LPADCHARS)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::LPADCHARS (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::LPADCHARS))) (DEFTHM STR::CHARACTER-LISTP-OF-LPADCHARS (CHARACTER-LISTP (STR::LPADCHARS X LEN))) (DEFTHM STR::LEN-OF-LPADCHARS (EQUAL (LEN (STR::LPADCHARS X LEN)) (MAX (LEN X) (NFIX LEN)))) (DEFCONG STR::CHARLISTEQV EQUAL (STR::LPADCHARS X LEN) 1) (DEFCONG STR::ICHARLISTEQV STR::ICHARLISTEQV (STR::LPADCHARS X LEN) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::LPADCHARS)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Pad a character-list with spaces on the left.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::LPADCHARS))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call lpadchars) extends the character list @('x') to length
@('len') by adding spaces on the left.  For instance,</p>

@({
  (lpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\Space #\\Space #\\f #\\o #\\o)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::LPADCHARS) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Pad a character-list with spaces on the left.") (:LONG . "<p>@(call lpadchars) extends the character list @('x') to length
@('len') by adding spaces on the left.  For instance,</p>

@({
  (lpadchars '(#\\f #\\o #\\o) 5)
     -->
  '(#\\Space #\\Space #\\f #\\o #\\o)
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|LPADCHARS|)
@(def |STR|::|CHARACTER-LISTP-OF-LPADCHARS|)
@(def |STR|::|LEN-OF-LPADCHARS|)
@(def |STR|::|CHARLISTEQV-IMPLIES-EQUAL-LPADCHARS-1|)
@(def |STR|::|ICHARLISTEQV-IMPLIES-ICHARLISTEQV-LPADCHARS-1|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::LPADCHARS)))))) (VALUE-TRIPLE (QUOTE STR::LPADCHARS))))) (10 RECORD-EXPANSION (DEFSECTION STR::LPADSTR :PARENTS (STR::PAD-TRIM) :SHORT "Pad a string with spaces on the left." :LONG "<p>@(call lpadstr) extends the string @('x') to length @('len') by
adding spaces on the left.  For instance,</p>

@({
  (lpadstr \"foo\" 5)
     -->
  \"  foo\"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>" (LOCAL (IN-THEORY (ENABLE STR::LPADCHARS))) (DEFUND STR::LPADSTR (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::LPADSTR))) (DEFTHM STR::STRINGP-OF-LPADSTR (STRINGP (STR::LPADSTR X LEN)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::LEN-OF-EXPLODE-OF-LPADSTR (IMPLIES (FORCE (STRINGP X)) (EQUAL (LEN (EXPLODE (STR::LPADSTR X LEN))) (MAX (LENGTH X) (NFIX LEN))))) (DEFCONG STR::STREQV EQUAL (STR::LPADSTR X LEN) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::LPADSTR X LEN) 1)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::LPADSTR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE STR::LPADCHARS))) (DEFUND STR::LPADSTR (X LEN) (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)))) (LOCAL (IN-THEORY (ENABLE STR::LPADSTR))) (DEFTHM STR::STRINGP-OF-LPADSTR (STRINGP (STR::LPADSTR X LEN)) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::LEN-OF-EXPLODE-OF-LPADSTR (IMPLIES (FORCE (STRINGP X)) (EQUAL (LEN (EXPLODE (STR::LPADSTR X LEN))) (MAX (LENGTH X) (NFIX LEN))))) (DEFCONG STR::STREQV EQUAL (STR::LPADSTR X LEN) 1) (DEFCONG STR::ISTREQV STR::ISTREQV (STR::LPADSTR X LEN) 1))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::LPADSTR)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Pad a string with spaces on the left.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::LPADSTR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call lpadstr) extends the string @('x') to length @('len') by
adding spaces on the left.  For instance,</p>

@({
  (lpadstr \"foo\" 5)
     -->
  \"  foo\"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::LPADSTR) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Pad a string with spaces on the left.") (:LONG . "<p>@(call lpadstr) extends the string @('x') to length @('len') by
adding spaces on the left.  For instance,</p>

@({
  (lpadstr \"foo\" 5)
     -->
  \"  foo\"
})

<p>This is completely dumb: we don't try to account for newlines, tabs, or
anything like that, and just add @('#\\Space') characters until reaching the
desired width.</p>

<p>If no new spaces are needed, @('x') is returned unchanged and no consing is
performed.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|LPADSTR|)
@(def |STR|::|STRINGP-OF-LPADSTR|)
@(def |STR|::|LEN-OF-EXPLODE-OF-LPADSTR|)
@(def |STR|::|STREQV-IMPLIES-EQUAL-LPADSTR-1|)
@(def |STR|::|ISTREQV-IMPLIES-ISTREQV-LPADSTR-1|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::LPADSTR)))))) (VALUE-TRIPLE (QUOTE STR::LPADSTR))))) (11 RECORD-EXPANSION (DEFSECTION STR::TRIM-BAG :PARENTS (STR::PAD-TRIM) :SHORT "Remove particular characters from the front and end of a string." :LONG "<p>@(call trim-bag) removes the characters in @('bag') from the
front and end of the string @('x').</p>

<p>BOZO eventually make this efficient.</p>" (DEFUND STR::TRIM-AUX (X STR::BAG) (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)) (LOCAL (IN-THEORY (ENABLE STR::TRIM-AUX))) (DEFTHM STR::CHARACTER-LISTP-OF-TRIM-AUX (IMPLIES (FORCE (CHARACTER-LISTP X)) (CHARACTER-LISTP (STR::TRIM-AUX X STR::BAG)))) (LOCAL (DEFTHM STR::TRUE-LISTP-WHEN-CHARACTER-LISTP (IMPLIES (CHARACTER-LISTP X) (TRUE-LISTP X)))) (DEFUND STR::TRIM-BAG (X STR::BAG) (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))) (LOCAL (IN-THEORY (ENABLE STR::TRIM-BAG))) (DEFTHM STR::STRINGP-OF-TRIM-BAG (STRINGP (STR::TRIM-BAG X STR::BAG)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::TRIM-BAG)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::TRIM-AUX (X STR::BAG) (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)) (LOCAL (IN-THEORY (ENABLE STR::TRIM-AUX))) (DEFTHM STR::CHARACTER-LISTP-OF-TRIM-AUX (IMPLIES (FORCE (CHARACTER-LISTP X)) (CHARACTER-LISTP (STR::TRIM-AUX X STR::BAG)))) (LOCAL (DEFTHM STR::TRUE-LISTP-WHEN-CHARACTER-LISTP (IMPLIES (CHARACTER-LISTP X) (TRUE-LISTP X)))) (DEFUND STR::TRIM-BAG (X STR::BAG) (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))) (LOCAL (IN-THEORY (ENABLE STR::TRIM-BAG))) (DEFTHM STR::STRINGP-OF-TRIM-BAG (STRINGP (STR::TRIM-BAG X STR::BAG)) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::TRIM-BAG)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Remove particular characters from the front and end of a string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::TRIM-BAG))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call trim-bag) removes the characters in @('bag') from the
front and end of the string @('x').</p>

<p>BOZO eventually make this efficient.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::TRIM-BAG) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Remove particular characters from the front and end of a string.") (:LONG . "<p>@(call trim-bag) removes the characters in @('bag') from the
front and end of the string @('x').</p>

<p>BOZO eventually make this efficient.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|TRIM-AUX|)
@(def |STR|::|CHARACTER-LISTP-OF-TRIM-AUX|)
@(def |STR|::|TRIM-BAG|)
@(def |STR|::|STRINGP-OF-TRIM-BAG|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::TRIM-BAG)))))) (VALUE-TRIPLE (QUOTE STR::TRIM-BAG))))) (12 RECORD-EXPANSION (DEFSECTION STR::TRIM :PARENTS (STR::PAD-TRIM) :SHORT "Remove whitespace characters from the front and end of a string." :LONG "<p>@(call trim) removes whitespace characters from the
front and end of the string @('x').</p>" (DEFUND STR::TRIM (X) (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))) (LOCAL (IN-THEORY (ENABLE STR::TRIM))) (DEFTHM STR::STRINGP-OF-TRIM (STRINGP (STR::TRIM X)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::TRIM)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::TRIM (X) (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))) (LOCAL (IN-THEORY (ENABLE STR::TRIM))) (DEFTHM STR::STRINGP-OF-TRIM (STRINGP (STR::TRIM X)) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::TRIM)) (XDOC::PARENTS (QUOTE (STR::PAD-TRIM))) (XDOC::SHORT (QUOTE "Remove whitespace characters from the front and end of a string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::TRIM))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call trim) removes whitespace characters from the
front and end of the string @('x').</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::TRIM) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::PAD-TRIM) (:SHORT . "Remove whitespace characters from the front and end of a string.") (:LONG . "<p>@(call trim) removes whitespace characters from the
front and end of the string @('x').</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|TRIM|)
@(def |STR|::|STRINGP-OF-TRIM|)") (:FROM . "[books]/str/pad.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::TRIM)))))) (VALUE-TRIPLE (QUOTE STR::TRIM))))))
(("/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/pad.lisp" "pad" "pad" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 724548430) ("/usr/share/acl2-6.3/books/str/cat.lisp" "cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1403689963)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1072446698