/usr/share/acl2-6.3/books/cgen/defdata.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 | (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)
: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/defdata.lisp" "defdata" "defdata" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:HASH-STOBJS "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp") (:REDEF+ "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp"))) . 1945337037) ("/usr/share/acl2-6.3/books/cgen/graph-tc.lisp" "graph-tc" "graph-tc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:HASH-STOBJS "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp") (:REDEF+ "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp"))) . 1209117067) ("/usr/share/acl2-6.3/books/cgen/library-support.lisp" "library-support" "library-support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 635686251) ("/usr/share/acl2-6.3/books/finite-set-theory/osets/sets.lisp" "finite-set-theory/osets/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1410988217) ("/usr/share/acl2-6.3/books/std/osets/top.lisp" "std/osets/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2045504100) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "std/lists/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/sort.lisp" "sort" "sort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 335087178)) (LOCAL ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140)) (LOCAL ("/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" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/outer.lisp" "outer" "outer" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883866964)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/cardinality.lisp" "cardinality" "cardinality" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 101478632)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/difference.lisp" "difference" "difference" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1211437825)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/intersect.lisp" "intersect" "intersect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 464592124)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/union.lisp" "union" "union" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 895011797)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/delete.lisp" "delete" "delete" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 929878553)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48714967)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392002111)) ("/usr/share/acl2-6.3/books/std/osets/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 537896665) ("/usr/share/acl2-6.3/books/std/osets/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1528243117) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "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/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/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/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (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)) (LOCAL ("/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/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "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)) (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/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)) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/defexec/other-apps/records/records.lisp" "defexec/other-apps/records/records" "records" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 681429738) ("/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp" "add-ons/hash-stobjs" "hash-stobjs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS (:HASH-STOBJS "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp") (:REDEF+ "/usr/share/acl2-6.3/books/add-ons/hash-stobjs.lisp"))) . 1257498041) (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)) (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/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/cgen/switchnat.lisp" "switchnat" "switchnat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 999627028) ("/usr/share/acl2-6.3/books/cgen/mv-proof.lisp" "mv-proof" "mv-proof" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 40342183) ("/usr/share/acl2-6.3/books/cgen/splitnat.lisp" "splitnat" "splitnat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 940480607) (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-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/cgen/rem-and-floor.lisp" "rem-and-floor" "rem-and-floor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1227219523)) (LOCAL ("/usr/share/acl2-6.3/books/cgen/num-list-thms.lisp" "num-list-thms" "num-list-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1052180754)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/top.lisp" "arithmetic-5/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 414221999)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/top.lisp" "lib/floor-mod/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2036487313)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/mod-expt-fast.lisp" "mod-expt-fast" "mod-expt-fast" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 8474989)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/logand.lisp" "logand" "logand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 477689935)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/logand-helper.lisp" "logand-helper" "logand-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1567870466)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/truncate-rem.lisp" "truncate-rem" "truncate-rem" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1222339411)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/more-floor-mod.lisp" "more-floor-mod" "more-floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1054313738)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/if-normalization.lisp" "if-normalization" "if-normalization" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 478555307)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod.lisp" "floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1117227810)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-helper.lisp" "floor-mod-helper" "floor-mod-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 383675918)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-basic.lisp" "floor-mod-basic" "floor-mod-basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1868400972)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-basic-helper.lisp" "floor-mod-basic-helper" "floor-mod-basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122255223)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/forcing-types.lisp" "forcing-types" "forcing-types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2092136594)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/common.lisp" "../basic-ops/common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2005694427)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/top.lisp" "../basic-ops/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 227046385)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks.lisp" "../basic-ops/building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 3355516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/top.lisp" "lib/basic-ops/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 227046385)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 322732972)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/forcing-types.lisp" "forcing-types" "forcing-types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 176314612)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/if-normalization.lisp" "if-normalization" "if-normalization" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2119667687)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 586482828)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities.lisp" "simple-equalities-and-inequalities" "simple-equalities-and-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 869088724)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities-helper.lisp" "simple-equalities-and-inequalities-helper" "simple-equalities-and-inequalities-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 21977321)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2009755655)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1042653498)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/types.lisp" "types" "types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1952837234)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/types-helper.lisp" "types-helper" "types-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308711892)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 414495578)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1484950306)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2103891710)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp-helper.lisp" "integerp-helper" "integerp-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1650787804)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1666343128)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1658521281)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 475372159)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1950245832)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1441743781)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2047460336)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 668797475)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1040308974)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2005694427)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 3355516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks-helper.lisp" "building-blocks-helper" "building-blocks-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1904099973)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/top.lisp" "../../support/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1197165143)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/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-5/support/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2058266018)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1097318215)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 628802930)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1078019670)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 806765711)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153952210)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/dynamic-e-d.lisp" "dynamic-e-d" "dynamic-e-d" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689130045)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/distributivity.lisp" "distributivity" "distributivity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1422342520)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/we-are-here.lisp" "we-are-here" "we-are-here" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1006471420)) ("/usr/share/acl2-6.3/books/cgen/num-list-fns.lisp" "num-list-fns" "num-list-fns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 41485979) ("/usr/share/acl2-6.3/books/cgen/acl2s-parameter.lisp" "acl2s-parameter" "acl2s-parameter" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1259392589) ("/usr/share/acl2-6.3/books/cgen/basis.lisp" "basis" "basis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 829677440) ("/usr/share/acl2-6.3/books/cgen/utilities.lisp" "utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1459061217) ("/usr/share/acl2-6.3/books/misc/total-order.lisp" "misc/total-order" "total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619824963) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order-bsd.lisp" "total-order-bsd" "total-order-bsd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449327279)) ("/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/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/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557))
1444011635
|