/usr/share/acl2-6.3/books/cgen/splitnat.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/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/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557))
193287441
|