/usr/share/acl2-6.3/books/make-event/proof-by-arith.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 10 11 12 13 14 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "U" (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) NIL ((:SYSTEM . "ihs/ihs-init.lisp") (:SYSTEM . "ihs/ihs-definitions.lisp") (:SYSTEM . "rtl/rel8/arithmetic/fp2.lisp") (:SYSTEM . "rtl/rel8/arithmetic/numerator.lisp") (:SYSTEM . "rtl/rel8/arithmetic/fl-proofs.lisp") (:SYSTEM . "rtl/rel8/arithmetic/fl.lisp") (:SYSTEM . "rtl/rel8/arithmetic/induct.lisp") (:SYSTEM . "rtl/rel8/arithmetic/top.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 . "arithmetic/top-with-meta.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 . "arithmetic/top-with-meta.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 . "arithmetic/top-with-meta.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 . "arithmetic/top-with-meta.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((5 RECORD-EXPANSION (PROOF-BY-ARITH (DEFTHM NNID (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL)) (ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "arithmetic/top-with-meta" :DIR :SYSTEM)) (DEFTHM NNID (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL))) (6 RECORD-EXPANSION (PROOF-BY-ARITH (DEFTHM NNID2 (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL) T) (WITH-OUTPUT :OFF (PROVE PROOF-TREE WARNING OBSERVATION EVENT EXPANSION SUMMARY) (ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "arithmetic/top-with-meta" :DIR :SYSTEM)) (DEFTHM NNID2 (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL)))) (7 RECORD-EXPANSION (PROOF-BY-ARITH (DEFTHM NNID3 (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL) NIL (("arithmetic-3/floor-mod/floor-mod" (SET-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))))) ("rtl/rel8/arithmetic/top") ("arithmetic-3/bind-free/top" (SET-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))))))) (ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "rtl/rel8/arithmetic/top" :DIR :SYSTEM)) (DEFTHM NNID3 (IMPLIES (AND (INTEGERP N) (< 0 N)) (EQUAL (DENOMINATOR (+ 1 (* 1/2 N))) (DENOMINATOR (* 1/2 N)))) :RULE-CLASSES NIL))) (8 RECORD-EXPANSION (PROOF-BY-ARITH (DEFTHM |proof-by-arith.lisp easy| (EQUAL (+ X Y (- X)) (FIX Y)) :RULE-CLASSES NIL) NIL (("arithmetic-3/floor-mod/floor-mod" (SET-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))))))) (ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "arithmetic-3/floor-mod/floor-mod" :DIR :SYSTEM)) (SET-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV)))) (DEFTHM |proof-by-arith.lisp easy| (EQUAL (+ X Y (- X)) (FIX Y)) :RULE-CLASSES NIL))) (9 RECORD-EXPANSION (PROOF-BY-ARITH (DEFTHM |proof-by-arith.lisp harder| (IMPLIES (AND (RATIONALP A) (RATIONALP B) (<= 0 A) (< A B)) (< (* A A) (* B B))))) (ENCAPSULATE NIL (LOCAL (INCLUDE-BOOK "arithmetic-3/top" :DIR :SYSTEM)) (SET-DEFAULT-HINTS (QUOTE ((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV)))) (DEFTHM |proof-by-arith.lisp harder| (IMPLIES (AND (RATIONALP A) (RATIONALP B) (<= 0 A) (< A B)) (< (* A A) (* B B)))))))
NIL
(("/usr/share/acl2-6.3/books/make-event/proof-by-arith.lisp" "proof-by-arith" "proof-by-arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1706060895) (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/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)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/top.lisp" "rtl/rel8/arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 756292945)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/mod-expt.lisp" "mod-expt" "mod-expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1942725880)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fl-expt.lisp" "fl-expt" "fl-expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1327162425)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/cg.lisp" "cg" "cg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1861436219)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/even-odd2.lisp" "even-odd2" "even-odd2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920150912)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/even-odd2-proofs.lisp" "even-odd2-proofs" "even-odd2-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2056004266)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fl-hacks.lisp" "fl-hacks" "fl-hacks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 737542075)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/mod.lisp" "mod" "mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 792040810)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/mod-proofs.lisp" "mod-proofs" "mod-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 853860481)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expo.lisp" "expo" "expo" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1547736526)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expo-proofs.lisp" "expo-proofs" "expo-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 240658463)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/power2p.lisp" "power2p" "power2p" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 651335974)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/x-2xx.lisp" "x-2xx" "x-2xx" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1832736645)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 16479620)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 397311293)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expt-proofs.lisp" "expt-proofs" "expt-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1808256733)) (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/rtl/rel8/arithmetic/even-odd.lisp" "even-odd" "even-odd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 540341452)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/complex-rationalp.lisp" "complex-rationalp" "complex-rationalp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1058200408)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/induct.lisp" "induct" "induct" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1068651620)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fl.lisp" "fl" "fl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1643208654)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fl-proofs.lisp" "fl-proofs" "fl-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2089095811)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/common-factor.lisp" "common-factor" "common-factor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 473235775)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/common-factor-defuns.lisp" "common-factor-defuns" "common-factor-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2122260756)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/floor.lisp" "floor" "floor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 309404600)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/floor-proofs.lisp" "floor-proofs" "floor-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 812673590)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/rationalp.lisp" "rationalp" "rationalp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 381475482)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/nniq.lisp" "nniq" "nniq" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 272033343)) (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/arithmetic/idiv.lisp" "../../../arithmetic/idiv" "idiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1789056792)) (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/rtl/rel8/arithmetic/arith.lisp" "arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1942063469)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/arith2.lisp" "arith2" "arith2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1321734032)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "../../../meta/meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "../../../meta/meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "../../../meta/meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1274355872)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/product.lisp" "product" "product" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661649302)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/product-proofs.lisp" "product-proofs" "product-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1224254738)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/unary-divide.lisp" "unary-divide" "unary-divide" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1659376686)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/numerator.lisp" "numerator" "numerator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 450678502)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/predicate.lisp" "predicate" "predicate" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1760934274)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/denominator.lisp" "denominator" "denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 571895333)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/mod-gcd.lisp" "../../../arithmetic/mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1629957550)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fp2.lisp" "fp2" "fp2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1001657670)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-2/meta/non-linear.lisp" "../../../arithmetic-2/meta/non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1703948508)) (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/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)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-lemmas.lisp" "../../../ihs/ihs-lemmas" "ihs-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685360399)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-lemmas.lisp" "logops-lemmas" "logops-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 998280003)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-definitions.lisp" "../../../ihs/ihs-definitions" "ihs-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 418368132)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-definitions.lisp" "logops-definitions" "logops-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2048680937)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/basic-definitions.lisp" "basic-definitions" "basic-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1383521171)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "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/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/ordinals/e0-ordinal.lisp" "../../../ordinals/e0-ordinal" "e0-ordinal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1020737716)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-isomorphism.lisp" "ordinal-isomorphism" "ordinal-isomorphism" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1519046782)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-addition.lisp" "ordinal-addition" "ordinal-addition" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 348288899)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-basic-thms.lisp" "ordinal-basic-thms" "ordinal-basic-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 770752119)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/top-with-meta.lisp" "top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 532658826)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-total-order.lisp" "ordinal-total-order" "ordinal-total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 757763360)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-definitions.lisp" "ordinal-definitions" "ordinal-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1478376100)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/inverted-factor.lisp" "inverted-factor" "inverted-factor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 357645011)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/negative-syntaxp.lisp" "negative-syntaxp" "negative-syntaxp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1540911563)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/ground-zero.lisp" "ground-zero" "ground-zero" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 403163111)) (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/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)))
95988968
|