/usr/share/acl2-6.3/books/system/top.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 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/system/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1691385109) ("/usr/share/acl2-6.3/books/system/legal-variablep.lisp" "legal-variablep" "legal-variablep" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 717920099) ("/usr/share/acl2-6.3/books/system/meta-extract.lisp" "meta-extract" "meta-extract" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1275181980) ("/usr/share/acl2-6.3/books/system/gather-dcls.lisp" "gather-dcls" "gather-dcls" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 377228105) ("/usr/share/acl2-6.3/books/system/convert-normalized-term-to-pairs.lisp" "convert-normalized-term-to-pairs" "convert-normalized-term-to-pairs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 918037690) ("/usr/share/acl2-6.3/books/system/subst-expr.lisp" "subst-expr" "subst-expr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1670444963) ("/usr/share/acl2-6.3/books/system/subst-var.lisp" "subst-var" "subst-var" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 407675406) ("/usr/share/acl2-6.3/books/system/subcor-var.lisp" "subcor-var" "subcor-var" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1958820302) (LOCAL ("/usr/share/acl2-6.3/books/system/pseudo-termp-lemmas.lisp" "pseudo-termp-lemmas" "pseudo-termp-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 617312428)) ("/usr/share/acl2-6.3/books/system/sublis-var.lisp" "sublis-var" "sublis-var" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 625848762) ("/usr/share/acl2-6.3/books/system/verified-termination-and-guards.lisp" "verified-termination-and-guards" "verified-termination-and-guards" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 452407258) ("/usr/share/acl2-6.3/books/system/too-many-ifs.lisp" "too-many-ifs" "too-many-ifs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1919958005) ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499) ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577) ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479) ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595) ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372) ("/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)) ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295) ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966) ("/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)) ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970) ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523) ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370) ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314) ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595) ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866) ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914) ("/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/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/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/system/extend-pathname.lisp" "extend-pathname" "extend-pathname" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479638026) ("/usr/share/acl2-6.3/books/system/hl-addr-combine.lisp" "hl-addr-combine" "hl-addr-combine" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1840548645) (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)))
234782293
|