acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / serialize / serialize-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (TEST-SERIALIZE 0) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (6 RECORD-EXPANSION (TEST-SERIALIZE 1) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (7 RECORD-EXPANSION (TEST-SERIALIZE -1) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (8 RECORD-EXPANSION (TEST-SERIALIZE 128308190248190238190283901283901283901283901823901) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (9 RECORD-EXPANSION (TEST-SERIALIZE 1/2) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (10 RECORD-EXPANSION (TEST-SERIALIZE -1/2) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (11 RECORD-EXPANSION (TEST-SERIALIZE #C(0 1)) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (12 RECORD-EXPANSION (TEST-SERIALIZE #C(-1 1/3)) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (13 RECORD-EXPANSION (TEST-SERIALIZE #\a) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (14 RECORD-EXPANSION (TEST-SERIALIZE #\z) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (15 RECORD-EXPANSION (TEST-SERIALIZE "foo") (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (16 RECORD-EXPANSION (TEST-SERIALIZE "bar") (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (17 RECORD-EXPANSION (TEST-SERIALIZE "") (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (18 RECORD-EXPANSION (TEST-SERIALIZE (CODE-CHAR 0)) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (19 RECORD-EXPANSION (TEST-SERIALIZE NIL) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (20 RECORD-EXPANSION (TEST-SERIALIZE T) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (21 RECORD-EXPANSION (TEST-SERIALIZE (QUOTE (NIL))) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (22 RECORD-EXPANSION (TEST-SERIALIZE (QUOTE (T))) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (34 RECORD-EXPANSION (TEST-SERIALIZE *TEST*) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (35 RECORD-EXPANSION (MAKE-EVENT (IF (NOT (HONS-ENABLEDP STATE)) (QUOTE (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (QUOTE (LOCAL (ENCAPSULATE NIL (MAKE-EVENT (LET ((STATE (SERIALIZE-WRITE "test.sao" NIL))) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (DEFTHM LEMMA-1 (EQUAL (UNSOUND-READ "test.sao") NIL) :RULE-CLASSES NIL) (MAKE-EVENT (LET ((STATE (SERIALIZE-WRITE "test.sao" T))) (VALUE (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (DEFTHM LEMMA-2 (EQUAL (UNSOUND-READ "test.sao") T) :RULE-CLASSES NIL) (DEFTHM QED NIL :RULE-CLASSES NIL :HINTS (("Goal" :USE ((:INSTANCE LEMMA-1) (:INSTANCE LEMMA-2)) :IN-THEORY (DISABLE (UNSOUND-READ-FN)))))))))) (VALUE-TRIPLE :DOES-NOT-WORK-WITHOUT-HONS)) (36 RECORD-EXPANSION (MAKE-EVENT (QUOTE (DEFCONST *FOO* (MAKE-FAST-ALIST (PAIRLIS$ (QUOTE (1 2 3 4)) (QUOTE (A B C D))))))) (DEFCONST *FOO* (MAKE-FAST-ALIST (PAIRLIS$ (QUOTE (1 2 3 4)) (QUOTE (A B C D)))))) (37 RECORD-EXPANSION (MAKE-EVENT (QUOTE (DEFCONST *FOO2* (MAKE-FAST-ALIST (LIST (CONS "blah" 1) (CONS (CONCATENATE (QUOTE STRING) "bl" "ah") 2) (CONS "black" 3) (CONS (CONCATENATE (QUOTE STRING) "bl" "ack") 3) (CONS "sheep" 4)))))) (DEFCONST *FOO2* (MAKE-FAST-ALIST (LIST (CONS "blah" 1) (CONS (CONCATENATE (QUOTE STRING) "bl" "ah") 2) (CONS "black" 3) (CONS (CONCATENATE (QUOTE STRING) "bl" "ack") 3) (CONS "sheep" 4))))))
NIL
(("/usr/share/acl2-6.3/books/serialize/serialize-tests.lisp" "serialize-tests" "serialize-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:UNSOUND-READ "/usr/share/acl2-6.3/books/serialize/unsound-read.lisp"))) . 494735893) ("/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/serialize/unsound-read.lisp" "unsound-read" "unsound-read" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:UNSOUND-READ "/usr/share/acl2-6.3/books/serialize/unsound-read.lisp"))) . 871955740) ("/usr/share/acl2-6.3/books/tools/include-raw.lisp" "tools/include-raw" "include-raw" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 438153625) ("/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))
1137244880