acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / cgen / random.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "DEFDATA" (APPEND (QUOTE (GETPROP KEY VAL FORMALS MACRO-ARGS CONST DECODE-LOGICAL-NAME VALUE LEGAL-CONSTANTP ER-LET* B* MACROEXPAND1 TRANS-EVAL SIMPLE-TRANSLATE-AND-EVAL ASSERT-EVENT LEGAL-VARIABLE-OR-CONSTANT-NAMEP F-BOUNDP-GLOBAL F-GET-GLOBAL F-PUT-GLOBAL PROOF-CHECKER EXPANSION EQUIVALENCE-RELATIONP 1+F 1-F +F -F DEFXDOC CURRENT-ACL2-WORLD E/D UNSIGNED-BYTE-P DEFREC VARIABLEP FQUOTEP FFN-SYMB FLAMBDAP FARGS LAMBDA-BODY LAMBDA-FORMALS SUBCOR-VAR DUMB-NEGATE-LIT IS-SUBTYPE IS-DISJOINT NAT-LISTP ALLP ACL2-NUMBER-LISTP NATURALS-LISTP POS-LISTP ONEOF ANYOF DATA-CONSTRUCTORS X N V INFXLST FINXLST LISTOF ENUM RECORD MAP SET NFIXG SET-ACL2S-DEFDATA-VERBOSE GET-ACL2S-DEFDATA-VERBOSE MGET MSET C REGISTER-DATA-CONSTRUCTOR DEFINE-ENUMERATION-TYPE DEFDATA-SUBTYPE DEFDATA-DISJOINT REGISTER-CUSTOM-TYPE DEFDATA DEFDATA-TESTING TEST? TOP-LEVEL-TEST? ACL2S-DEFAULTS SET-ACL2S-RANDOM-TESTING-ENABLED GET-ACL2S-RANDOM-TESTING-ENABLED DONT-PRINT-THANKS-MESSAGE-OVERRIDE-HINT NUM-TRIALS VERBOSITY-LEVEL SHOW-TESTING-OUTPUT NUM-WITNESSES NUM-COUNTEREXAMPLES SHOW-TOP-LEVEL-COUNTEREXAMPLE SAMPLING-METHOD BACKTRACK-LIMIT SUBGOAL-TIMEOUT SEARCH-STRATEGY STOPPING-CONDITION TESTING-ENABLED SYSTEM-DEBUG-FLAG INHIBIT-OUTPUT-FLAG NORMAL-OUTPUT-FLAG VERBOSE-FLAG DEBUG-FLAG)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
(INCLUDE-BOOK "std/osets/portcullis" :DIR :SYSTEM)
(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/inequalities.lisp") (:SYSTEM . "arithmetic/rationals.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/inequalities.lisp") (:SYSTEM . "arithmetic/rationals.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/inequalities.lisp") (:SYSTEM . "arithmetic/rationals.lisp")) T)
:END-PORTCULLIS-CMDS
(("/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/cgen/random.lisp" "random" "random" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1805741846) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/top.lisp" "arithmetic-3/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1644102178)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/mod-expt-fast.lisp" "floor-mod/mod-expt-fast" "mod-expt-fast" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70679366)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "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/rationals.lisp" "arithmetic/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/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (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/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)) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557))
301436108