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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (DEFSECTION STR::HTML-ENCODING :PARENTS (STR) :SHORT "Routines to encode HTML entities, e.g., @('<') becomes @('&lt;')." :LONG "<p>In principle, our conversion routines may not be entirely
legitimate in the sense of some precise HTML specification, because we do not
account for non-printable characters or other similarly unlikely garbage in the
input.  But it seems like what we implement is pretty reasonable, and handles
most ordinary characters.</p>

<p>Note that we convert @('#\\Newline') characters into the sequence
@('<br/>#\\Newline').  This may not be the desired behavior in certain
applications, but seems basically reasonable for converting plain text into
HTML.</p>") (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HTML-ENCODING)) (XDOC::PARENTS (QUOTE (STR))) (XDOC::SHORT (QUOTE "Routines to encode HTML entities, e.g., @('<') becomes @('&lt;').")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODING))) 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>In principle, our conversion routines may not be entirely
legitimate in the sense of some precise HTML specification, because we do not
account for non-printable characters or other similarly unlikely garbage in the
input.  But it seems like what we implement is pretty reasonable, and handles
most ordinary characters.</p>

<p>Note that we convert @('#\\Newline') characters into the sequence
@('<br/>#\\Newline').  This may not be the desired behavior in certain
applications, but seems basically reasonable for converting plain text into
HTML.</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::HTML-ENCODING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR) (:SHORT . "Routines to encode HTML entities, e.g., @('<') becomes @('&lt;').") (:LONG . "<p>In principle, our conversion routines may not be entirely
legitimate in the sense of some precise HTML specification, because we do not
account for non-printable characters or other similarly unlikely garbage in the
input.  But it seems like what we implement is pretty reasonable, and handles
most ordinary characters.</p>

<p>Note that we convert @('#\\Newline') characters into the sequence
@('<br/>#\\Newline').  This may not be the desired behavior in certain
applications, but seems basically reasonable for converting plain text into
HTML.</p>

") (:FROM . "[books]/str/html-encode.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HTML-ENCODING)))))) (VALUE-TRIPLE (QUOTE STR::HTML-ENCODING))))) (14 RECORD-EXPANSION (DEFSECTION STR::HTML-ENCODE-CHARS-AUX :PARENTS (STR::HTML-ENCODING) :SHORT "Convert a character list into HTML." :LONG "<p>@(call html-encode-chars-aux) converts the character-list @('x')
into HTML, producing new characters which are accumulated onto @('acc') in
reverse order.</p>

<p>As inputs:</p>
<ul>
 <li>X is a list of characters which we are currently transforming into HTML.</li>
 <li>Col is the current column number</li>
 <li>Acc is an ordinary character list, onto which we accumulate the encoded
     HTML characters, in reverse order.</li>
</ul>

<p>We return @('(mv col' acc')'), where @('col'') is the new column number and
@('acc'') is the updated accumulator, which includes the HTML encoding of
@('X') in reverse.</p>" (DEFUND STR::HTML-ENCODE-CHARS-AUX (X STR::COL STR::TABSIZE STR::ACC) (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))))))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-CHARS-AUX))) (DEFTHM STR::NATP-OF-HTML-ENCODE-CHARS-AUX (NATP (MV-NTH 0 (STR::HTML-ENCODE-CHARS-AUX X STR::COL STR::TABSIZE STR::ACC))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-HTML-ENCODE-CHARS-AUX (IMPLIES (AND (CHARACTER-LISTP X) (NATP STR::COL) (CHARACTER-LISTP STR::ACC)) (CHARACTER-LISTP (MV-NTH 1 (STR::HTML-ENCODE-CHARS-AUX X STR::COL STR::TABSIZE STR::ACC)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-CHARS-AUX)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::HTML-ENCODE-CHARS-AUX (X STR::COL STR::TABSIZE STR::ACC) (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))))))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-CHARS-AUX))) (DEFTHM STR::NATP-OF-HTML-ENCODE-CHARS-AUX (NATP (MV-NTH 0 (STR::HTML-ENCODE-CHARS-AUX X STR::COL STR::TABSIZE STR::ACC))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-HTML-ENCODE-CHARS-AUX (IMPLIES (AND (CHARACTER-LISTP X) (NATP STR::COL) (CHARACTER-LISTP STR::ACC)) (CHARACTER-LISTP (MV-NTH 1 (STR::HTML-ENCODE-CHARS-AUX X STR::COL STR::TABSIZE STR::ACC))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HTML-ENCODE-CHARS-AUX)) (XDOC::PARENTS (QUOTE (STR::HTML-ENCODING))) (XDOC::SHORT (QUOTE "Convert a character list into HTML.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-CHARS-AUX))) 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 html-encode-chars-aux) converts the character-list @('x')
into HTML, producing new characters which are accumulated onto @('acc') in
reverse order.</p>

<p>As inputs:</p>
<ul>
 <li>X is a list of characters which we are currently transforming into HTML.</li>
 <li>Col is the current column number</li>
 <li>Acc is an ordinary character list, onto which we accumulate the encoded
     HTML characters, in reverse order.</li>
</ul>

<p>We return @('(mv col' acc')'), where @('col'') is the new column number and
@('acc'') is the updated accumulator, which includes the HTML encoding of
@('X') in reverse.</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::HTML-ENCODE-CHARS-AUX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::HTML-ENCODING) (:SHORT . "Convert a character list into HTML.") (:LONG . "<p>@(call html-encode-chars-aux) converts the character-list @('x')
into HTML, producing new characters which are accumulated onto @('acc') in
reverse order.</p>

<p>As inputs:</p>
<ul>
 <li>X is a list of characters which we are currently transforming into HTML.</li>
 <li>Col is the current column number</li>
 <li>Acc is an ordinary character list, onto which we accumulate the encoded
     HTML characters, in reverse order.</li>
</ul>

<p>We return @('(mv col' acc')'), where @('col'') is the new column number and
@('acc'') is the updated accumulator, which includes the HTML encoding of
@('X') in reverse.</p>

<h3>Definitions and Theorems</h3>@(def |STR|::|HTML-ENCODE-CHARS-AUX|)
@(def |STR|::|NATP-OF-HTML-ENCODE-CHARS-AUX|)
@(def |STR|::|CHARACTER-LISTP-OF-HTML-ENCODE-CHARS-AUX|)") (:FROM . "[books]/str/html-encode.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HTML-ENCODE-CHARS-AUX)))))) (VALUE-TRIPLE (QUOTE STR::HTML-ENCODE-CHARS-AUX))))) (15 RECORD-EXPANSION (DEFSECTION STR::HTML-ENCODE-STRING-AUX :PARENTS (STR::HTML-ENCODING) :SHORT "Convert a string into HTML." :LONG "<p>@(call html-encode-string-aux) returns @('(mv col acc)').</p>

<p>This is similar to @(see html-encode-chars-aux), but encodes part of a the
string @('x') instead of a character list.  The additional arguments are as
follows:</p>

<ul>

<li>@('xl') - the pre-computed length of the string</li>

<li>@('n') - current position in the string where we are encoding; this should
typically be 0 to begin with.</li>

</ul>" (DEFUND STR::HTML-ENCODE-STRING-AUX (X N STR::XL STR::COL STR::TABSIZE STR::ACC) (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))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N)))) (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))))))) (LOCAL (ASSERT! (B* ((X "blah
tab:	  <boo> & \"foo\" blah blah") ((MV STR::STR-COL STR::STR-ANS) (STR::HTML-ENCODE-STRING-AUX X 0 (LENGTH X) 0 8 NIL)) ((MV STR::CHAR-COL STR::CHAR-ANS) (STR::HTML-ENCODE-CHARS-AUX (COERCE X (QUOTE LIST)) 0 8 NIL)) (- (CW "~s0~%" (COERCE (REVERSE STR::STR-ANS) (QUOTE STRING))))) (AND (EQUAL STR::STR-COL STR::CHAR-COL) (EQUAL STR::STR-ANS STR::CHAR-ANS))))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-STRING-AUX))) (DEFTHM STR::NATP-OF-HTML-ENCODE-STRING-AUX (NATP (MV-NTH 0 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-HTML-ENCODE-STRING-AUX (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (NATP STR::COL) (CHARACTER-LISTP STR::ACC) (<= N STR::XL) (= STR::XL (LENGTH X))) (CHARACTER-LISTP (MV-NTH 1 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC)))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-STRING-AUX)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::HTML-ENCODE-STRING-AUX (X N STR::XL STR::COL STR::TABSIZE STR::ACC) (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))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N)))) (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))))))) (LOCAL (ASSERT! (B* ((X "blah
tab:	  <boo> & \"foo\" blah blah") ((MV STR::STR-COL STR::STR-ANS) (STR::HTML-ENCODE-STRING-AUX X 0 (LENGTH X) 0 8 NIL)) ((MV STR::CHAR-COL STR::CHAR-ANS) (STR::HTML-ENCODE-CHARS-AUX (COERCE X (QUOTE LIST)) 0 8 NIL)) (- (CW "~s0~%" (COERCE (REVERSE STR::STR-ANS) (QUOTE STRING))))) (AND (EQUAL STR::STR-COL STR::CHAR-COL) (EQUAL STR::STR-ANS STR::CHAR-ANS))))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-STRING-AUX))) (DEFTHM STR::NATP-OF-HTML-ENCODE-STRING-AUX (NATP (MV-NTH 0 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-HTML-ENCODE-STRING-AUX (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (NATP STR::COL) (CHARACTER-LISTP STR::ACC) (<= N STR::XL) (= STR::XL (LENGTH X))) (CHARACTER-LISTP (MV-NTH 1 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::HTML-ENCODE-STRING-AUX (X N STR::XL STR::COL STR::TABSIZE STR::ACC) (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))) :MEASURE (NFIX (- (NFIX STR::XL) (NFIX N)))) (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))))))) (RECORD-EXPANSION (LOCAL (ASSERT! (B* ((X "blah
tab:	  <boo> & \"foo\" blah blah") ((MV STR::STR-COL STR::STR-ANS) (STR::HTML-ENCODE-STRING-AUX X 0 (LENGTH X) 0 8 NIL)) ((MV STR::CHAR-COL STR::CHAR-ANS) (STR::HTML-ENCODE-CHARS-AUX (COERCE X (QUOTE LIST)) 0 8 NIL)) (- (CW "~s0~%" (COERCE (REVERSE STR::STR-ANS) (QUOTE STRING))))) (AND (EQUAL STR::STR-COL STR::CHAR-COL) (EQUAL STR::STR-ANS STR::CHAR-ANS))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-STRING-AUX))) (DEFTHM STR::NATP-OF-HTML-ENCODE-STRING-AUX (NATP (MV-NTH 0 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC))) :RULE-CLASSES :TYPE-PRESCRIPTION) (DEFTHM STR::CHARACTER-LISTP-OF-HTML-ENCODE-STRING-AUX (IMPLIES (AND (STRINGP X) (NATP N) (NATP STR::XL) (NATP STR::COL) (CHARACTER-LISTP STR::ACC) (<= N STR::XL) (= STR::XL (LENGTH X))) (CHARACTER-LISTP (MV-NTH 1 (STR::HTML-ENCODE-STRING-AUX X N STR::XL STR::COL STR::TABSIZE STR::ACC)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HTML-ENCODE-STRING-AUX)) (XDOC::PARENTS (QUOTE (STR::HTML-ENCODING))) (XDOC::SHORT (QUOTE "Convert a string into HTML.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-STRING-AUX))) 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 html-encode-string-aux) returns @('(mv col acc)').</p>

<p>This is similar to @(see html-encode-chars-aux), but encodes part of a the
string @('x') instead of a character list.  The additional arguments are as
follows:</p>

<ul>

<li>@('xl') - the pre-computed length of the string</li>

<li>@('n') - current position in the string where we are encoding; this should
typically be 0 to begin with.</li>

</ul>") (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::HTML-ENCODE-STRING-AUX) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::HTML-ENCODING) (:SHORT . "Convert a string into HTML.") (:LONG . "<p>@(call html-encode-string-aux) returns @('(mv col acc)').</p>

<p>This is similar to @(see html-encode-chars-aux), but encodes part of a the
string @('x') instead of a character list.  The additional arguments are as
follows:</p>

<ul>

<li>@('xl') - the pre-computed length of the string</li>

<li>@('n') - current position in the string where we are encoding; this should
typically be 0 to begin with.</li>

</ul>

<h3>Definitions and Theorems</h3>@(def |STR|::|HTML-ENCODE-STRING-AUX|)
@(def |STR|::|NATP-OF-HTML-ENCODE-STRING-AUX|)
@(def |STR|::|CHARACTER-LISTP-OF-HTML-ENCODE-STRING-AUX|)") (:FROM . "[books]/str/html-encode.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HTML-ENCODE-STRING-AUX)))))) (VALUE-TRIPLE (QUOTE STR::HTML-ENCODE-STRING-AUX))))) (16 RECORD-EXPANSION (DEFSECTION STR::HTML-ENCODE-STRING :PARENTS (STR::HTML-ENCODING) :SHORT "@(call html-encode-string) converts the string @('x') into HTML, and
returns the result as a new string." (DEFUND STR::HTML-ENCODE-STRING (X STR::TABSIZE) (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))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-STRING))) (DEFTHM STR::STRINGP-OF-HTML-ENCODE-STRING (STRINGP (STR::HTML-ENCODE-STRING X STR::TABSIZE)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-STRING)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::HTML-ENCODE-STRING (X STR::TABSIZE) (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))) (LOCAL (IN-THEORY (ENABLE STR::HTML-ENCODE-STRING))) (DEFTHM STR::STRINGP-OF-HTML-ENCODE-STRING (STRINGP (STR::HTML-ENCODE-STRING X STR::TABSIZE)) :RULE-CLASSES :TYPE-PRESCRIPTION))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::HTML-ENCODE-STRING)) (XDOC::PARENTS (QUOTE (STR::HTML-ENCODING))) (XDOC::SHORT (QUOTE "@(call html-encode-string) converts the string @('x') into HTML, and
returns the result as a new string.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::HTML-ENCODE-STRING))) 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::HTML-ENCODE-STRING) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::HTML-ENCODING) (:SHORT . "@(call html-encode-string) converts the string @('x') into HTML, and
returns the result as a new string.") (:LONG . "

<h3>Definitions and Theorems</h3>@(def |STR|::|HTML-ENCODE-STRING|)
@(def |STR|::|STRINGP-OF-HTML-ENCODE-STRING|)") (:FROM . "[books]/str/html-encode.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::HTML-ENCODE-STRING)))))) (VALUE-TRIPLE (QUOTE STR::HTML-ENCODE-STRING))))))
(("/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/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)) ("/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))
1573846993