acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / paco / utilities.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFMACRO PACO NIL (QUOTE (COND ((ASSOC-EQUAL "PACO" (KNOWN-PACKAGE-ALIST STATE)) (IN-PACKAGE "PACO")) (T (ER-PROGN (INCLUDE-BOOK "paco") (COMP T) (VALUE (CW "~%~%Note:  For ptrace and faster output, :q and ~%~
                           (load \"raw.lisp\").~%~%")) (IN-PACKAGE "PACO"))))))
(DEFPKG "PACO" (QUOTE (ACL2-NUMBERP BAD-ATOM BAD-ATOM<= BINARY-* BINARY-+ UNARY-- UNARY-/ < CAR CDR CHAR-CODE CHARACTERP CODE-CHAR COMPLEX COMPLEX-RATIONALP COERCE CONS CONSP DENOMINATOR EQUAL IF IMAGPART INTEGERP INTERN-IN-PACKAGE-OF-SYMBOL NUMERATOR RATIONALP REALPART STRINGP SYMBOL-NAME SYMBOL-PACKAGE-NAME SYMBOLP NOT EQ LENGTH ATOM ACONS ENDP NULL = /= ZP ZIP NTH CHAR CONJUGATE STANDARD-CHAR-P STRING ALPHA-CHAR-P UPPER-CASE-P LOWER-CASE-P CHAR-UPCASE CHAR-DOWNCASE STRING-DOWNCASE STRING-UPCASE CHAR-EQUAL STRING-EQUAL KEYWORDP IDENTITY REVAPPEND REVERSE EQL MEMBER ASSOC RASSOC REMOVE REMOVE-DUPLICATES POSITION SUBSTITUTE SUBSETP SUBLIS SUBST FLOOR CEILING TRUNCATE ROUND MOD REM EVENP ODDP ZEROP PLUSP MINUSP MIN MAX ABS SIGNUM LOGNOT EXPT BINARY-APPEND NFIX E0-ORDINALP E0-ORD-< CHAR< CHAR> CHAR<= CHAR>= STRING< STRING> STRING<= STRING>= ZPF INTEGER-LENGTH LOGNAND LOGORC1 LOGORC2 LOGANDC1 LOGANDC2 LOGNOR LOGTEST SUBSEQ BUTLAST ACL2-COUNT IMPLIES IFF TRUE-LISTP LEN SYNP LISTP PROG2$ FORCE CASE-SPLIT QUOTE NIL T LAMBDA DECLARE IGNORE XARGS OTHERWISE INT= DIGIT-CHAR-P INTERN APPEND CONCATENATE FIRST SECOND THIRD FOURTH FIFTH SIXTH SEVENTH EIGHTH NINTH TENTH REST LIST* THE-FIXNUM MAKE-LIST THE-MV THE2S I-LIMITED GC$ + * - / > >= <= 1- 1+ LOGAND LOGEQV LOGIOR LOGXOR LET LET* LIST COND CASE CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR MV MV-LET MV-NTH AND OR &REST PROGN THE INTEGER TRACE UNTRACE LP *MAIN-LISP-PACKAGE-NAME* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *COMMON-LISP-SPECIALS-AND-CONSTANTS* MUTUAL-RECURSION DEFUN DEFTHM DEFCONST DEFMACRO DEFLABEL IN-PACKAGE VERIFY-GUARDS IN-THEORY DISABLE ENABLE PREPROCESS SIMPLIFY ELIMINATE-DESTRUCTORS FERTILIZE GENERALIZE ELIMINATE-IRRELEVANCE LD VALUE INCLUDE-BOOK THM LOCAL ENCAPSULATE WORMHOLE WORMHOLE-EVAL WORMHOLE-INPUT WORMHOLE-STATUS MAKE-WORMHOLE-STATUS WORMHOLE-DATA SET-WORMHOLE-DATA ER-PROGN ASSIGN @ CW MSG)))
(SET-VERIFY-GUARDS-EAGERNESS 0)
(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")) T)
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp") (:SYSTEM . "arithmetic/nat-listp.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp")) T)
(DEFPKG "ACL2-CRG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp")) T)
(DEFPKG "ACL2-AGP" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp")) T)
(DEFPKG "ACL2-ASG" (SET-DIFFERENCE-EQUAL (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (ZERO))) NIL ((:SYSTEM . "arithmetic/equalities.lisp") (:SYSTEM . "arithmetic/top.lisp") (:SYSTEM . "ihs/math-lemmas.lisp") (:SYSTEM . "ihs/ihs-lemmas.lisp")) T)
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/paco/utilities.lisp" "utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 364667623) (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/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/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148)) (LOCAL ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573)) (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)))
627203307