acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / misc / radix.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "RADIX" (UNION-EQ (QUOTE (FMX)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
(DEFPKG "U" (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) NIL ((:SYSTEM . "ihs/ihs-init.lisp") (:SYSTEM . "ihs/quotient-remainder-lemmas.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod-helper.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod.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/quotient-remainder-lemmas.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod-helper.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod.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/quotient-remainder-lemmas.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod-helper.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod.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/quotient-remainder-lemmas.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod-helper.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod.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/quotient-remainder-lemmas.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod-helper.lisp") (:SYSTEM . "arithmetic-2/floor-mod/floor-mod.lisp")) T)
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/misc/radix.lisp" "radix" "radix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 545956865) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/floor-mod/floor-mod.lisp" "arithmetic-2/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1714686173)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "floor-mod-helper" "floor-mod-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1895560764)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "ihs/quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 603178913)) (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/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)) (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/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-2/meta/top.lisp" "../meta/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 232468655)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/top.lisp" "arithmetic-2/meta/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 232468655)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/post.lisp" "post" "post" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 756560553)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 410240007)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1703948508)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1816787487)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1329840539)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1498669602)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/collect-terms-meta.lisp" "collect-terms-meta" "collect-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 815322349)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/cancel-terms-meta.lisp" "cancel-terms-meta" "cancel-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1454902718)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/cancel-terms-helper.lisp" "cancel-terms-helper" "cancel-terms-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1911183526)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/common-meta.lisp" "common-meta" "common-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 676684688)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 472043675)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 191999018)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/pre.lisp" "pre" "pre" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069370462)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 578758519)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 879141259)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp" "numerator-and-denominator-helper" "numerator-and-denominator-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 418530727)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1752567041)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1176064317)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 987706591)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 204952285)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 298400249)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1773867232)))
324238923