/usr/share/acl2-6.3/books/quadratic-reciprocity/mersenne.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/quadratic-reciprocity/mersenne.lisp" "mersenne" "mersenne" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 66668430) ("/usr/share/acl2-6.3/books/quadratic-reciprocity/gauss.lisp" "gauss" "gauss" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 45722765) ("/usr/share/acl2-6.3/books/quadratic-reciprocity/euler.lisp" "euler" "euler" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 891629868) ("/usr/share/acl2-6.3/books/quadratic-reciprocity/fermat.lisp" "fermat" "fermat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1426911910) ("/usr/share/acl2-6.3/books/quadratic-reciprocity/euclid.lisp" "euclid" "euclid" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 980824336) ("/usr/share/acl2-6.3/books/rtl/rel8/lib/basic.lisp" "rtl/rel8/lib/basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 536850909) ("/usr/share/acl2-6.3/books/rtl/rel8/lib/arith.lisp" "rtl/rel8/lib/arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2084481173) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/top/top.lisp" "../support/top/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1449316243)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn2log.lisp" "../lib2.delta1/logn2log" "logn2log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1007811297)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn2log-proofs.lisp" "logn2log-proofs" "logn2log-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1716535080)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simplify-model-helpers.lisp" "../lib2.delta1/simplify-model-helpers" "simplify-model-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 582099186)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simplify-model-helpers-proofs.lisp" "simplify-model-helpers-proofs" "simplify-model-helpers-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1730083723)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simplify-model-helpers-new.lisp" "simplify-model-helpers-new" "simplify-model-helpers-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 722120777)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simplify-model-helpers-new-proofs.lisp" "simplify-model-helpers-new-proofs" "simplify-model-helpers-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1279817244)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/simplify-model-helpers.lisp" "../lib2/simplify-model-helpers" "simplify-model-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1736427016)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/simplify-model-helpers.lisp" "../support/simplify-model-helpers" "simplify-model-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 990148787)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/arith.lisp" "arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1968567520)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn.lisp" "../lib2.delta1/logn" "logn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 780116553)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bvecp-helpers.lisp" "../lib2.delta1/bvecp-helpers" "bvecp-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 993348470)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bvecp-raw-helpers.lisp" "bvecp-raw-helpers" "bvecp-raw-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 751728833)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/rom-helpers.lisp" "../lib2/rom-helpers" "rom-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1208766449)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rom-helpers.lisp" "../support/rom-helpers" "rom-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 534396735)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simple-loop-helpers.lisp" "../lib2.delta1/simple-loop-helpers" "simple-loop-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1468300159)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/simple-loop-helpers-proofs.lisp" "simple-loop-helpers-proofs" "simple-loop-helpers-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 638926174)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bvecp-raw-helpers.lisp" "../lib2.delta1/bvecp-raw-helpers" "bvecp-raw-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 751728833)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bvecp-raw-helpers-proofs.lisp" "bvecp-raw-helpers-proofs" "bvecp-raw-helpers-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1483388363)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn.lisp" "logn" "logn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 780116553)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn-proofs.lisp" "logn-proofs" "logn-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1802650154)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn-new.lisp" "logn-new" "logn-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1531039306)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/logn-new-proofs.lisp" "logn-new-proofs" "logn-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 83004331)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtlarr.lisp" "rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653525586)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta2/add.lisp" "../lib2.delta2/add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1503590111)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta2/log.lisp" "../lib2.delta2/log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 882207266)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta2/bits.lisp" "../lib2.delta2/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1922039883)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta2/add-lib.lisp" "add-lib" "add-lib" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 520809976)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/arith.lisp" "../lib2.delta1/arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1968567520)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta2/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 176438422)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/util.lisp" "../lib2.delta1/util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 163164940)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/mult.lisp" "../lib2.delta1/mult" "mult" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1307954051)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/mult-proofs.lisp" "mult-proofs" "mult-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1725691863)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/mult-new.lisp" "mult-new" "mult-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449491365)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/mult-new-proofs.lisp" "mult-new-proofs" "mult-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1610258629)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/add.lisp" "add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 455189055)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/add.lisp" "../lib2.delta1/add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 455189055)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/add-proofs.lisp" "add-proofs" "add-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2002026313)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/add-new.lisp" "add-new" "add-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1250459532)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/add-new-proofs.lisp" "add-new-proofs" "add-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1122252122)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/round.lisp" "round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1597848129)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/round.lisp" "../lib2.delta1/round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1597848129)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/round-proofs.lisp" "round-proofs" "round-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1812269390)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/round-new.lisp" "round-new" "round-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 851320487)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/round-new-proofs.lisp" "round-new-proofs" "round-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 592459445)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/reps.lisp" "../lib2.delta1/reps" "reps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1681979650)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/reps-proofs.lisp" "reps-proofs" "reps-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 88755262)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/reps-new.lisp" "reps-new" "reps-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1147246048)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/reps-new-proofs.lisp" "reps-new-proofs" "reps-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1964607655)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log-support.lisp" "log-support" "log-support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2036235392)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log-support-proofs.lisp" "log-support-proofs" "log-support-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 439527557)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/float.lisp" "float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 601757649)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/float.lisp" "../lib2.delta1/float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 601757649)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/float-proofs.lisp" "float-proofs" "float-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915401860)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/float-new.lisp" "float-new" "float-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1334285191)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/float-new-proofs.lisp" "float-new-proofs" "float-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2050604625)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log.lisp" "log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1840097837)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log.lisp" "../lib2.delta1/log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1840097837)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log-proofs.lisp" "log-proofs" "log-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1381564038)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bits.lisp" "../lib2.delta1/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 159164042)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtlarr.lisp" "../lib2.delta1/rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653525586)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtl.lisp" "rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 571016967)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtlarr-new.lisp" "rtlarr-new" "rtlarr-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 731167846)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtl.lisp" "../lib2.delta1/rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 571016967)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtl-proofs.lisp" "rtl-proofs" "rtl-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 716616276)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bits.lisp" "bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 159164042)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bits-proofs.lisp" "bits-proofs" "bits-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 716050146)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtl-new.lisp" "rtl-new" "rtl-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 309294410)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/rtl-new-proofs.lisp" "rtl-new-proofs" "rtl-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1524308242)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log-new.lisp" "log-new" "log-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1438482707)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/log-new-proofs.lisp" "log-new-proofs" "log-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 854083575)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lognot.lisp" "../support/lognot" "lognot" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327888594)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logxor.lisp" "../support/logxor" "logxor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 22449149)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logior.lisp" "../support/logior" "logior" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948519876)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bits-new.lisp" "bits-new" "bits-new" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 276807307)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/basic.lisp" "../lib2/basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 225659118)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2.delta1/bits-new-proofs.lisp" "bits-new-proofs" "bits-new-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1872164667)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/badguys.lisp" "../support/badguys" "badguys" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2027003241)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logand.lisp" "../support/logand" "logand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 193497260)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/merge.lisp" "../support/merge" "merge" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1388042792)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/log.lisp" "../support/log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 568865953)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/top.lisp" "../lib2/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1777199538)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/util.lisp" "util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1245101938)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/arith.lisp" "arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1120066331)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/mult.lisp" "mult" "mult" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1031828771)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/add.lisp" "add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 323536447)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/round.lisp" "round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 812212847)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/reps.lisp" "reps" "reps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 913757202)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/float.lisp" "float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1286105915)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/log.lisp" "log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 553707208)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/bits.lisp" "bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1869893009)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/rtlarr.lisp" "rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260305174)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/rtl.lisp" "rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 421843971)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/bits.lisp" "../lib2/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1869893009)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 225659118)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib2/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1121118647)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/simple-loop-helpers.lisp" "../lib1.delta1/simple-loop-helpers" "simple-loop-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 623042885)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/simple-loop-helpers-extra.lisp" "simple-loop-helpers-extra" "simple-loop-helpers-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1062078462)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/simple-loop-helpers.lisp" "../lib1/simple-loop-helpers" "simple-loop-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 598608571)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/simple-loop-helpers.lisp" "../support/simple-loop-helpers" "simple-loop-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1960059434)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/arith.lisp" "arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 315766257)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/bvecp-raw-helpers.lisp" "../lib1.delta1/bvecp-raw-helpers" "bvecp-raw-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1757878700)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/bvecp-raw-helpers-extra.lisp" "bvecp-raw-helpers-extra" "bvecp-raw-helpers-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1309131955)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/bvecp-raw-helpers.lisp" "../lib1/bvecp-raw-helpers" "bvecp-raw-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1808600197)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/decode.lisp" "../support/decode" "decode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1294090937)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/encode.lisp" "../support/encode" "encode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1081048419)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/mulcat.lisp" "../support/mulcat" "mulcat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 281231437)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/shft.lisp" "../support/shft" "shft" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2075005662)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lnot.lisp" "../support/lnot" "lnot" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1475228708)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logs.lisp" "../support/logs" "logs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 824187868)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbitn.lisp" "../support/setbitn" "setbitn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 73211283)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbits.lisp" "../support/setbits" "setbits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685120556)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bitn.lisp" "../support/bitn" "bitn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482090031)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bits.lisp" "../support/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1370009319)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/util.lisp" "../lib1/util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2004088401)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/arith.lisp" "../lib1.delta1/arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 315766257)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/arith-extra.lisp" "arith-extra" "arith-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 482331627)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/arith.lisp" "../lib1/arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797309786)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/mult.lisp" "../lib1.delta1/mult" "mult" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1169854356)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/mult-proofs.lisp" "mult-proofs" "mult-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 306809640)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/cat.lisp" "../support/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 795157675)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lxor.lisp" "../support/lxor" "lxor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 651029821)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/land.lisp" "../support/land" "land" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 190868162)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lior.lisp" "../support/lior" "lior" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1958592902)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/sumbits.lisp" "../support/sumbits" "sumbits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 9708740)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rtl.lisp" "../support/rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1638971093)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/add.lisp" "../lib1/add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1645824547)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/round.lisp" "../lib1.delta1/round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1428340704)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/round-extra2.lisp" "round-extra2" "round-extra2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 348748665)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/away.lisp" "../support/away" "away" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 710865809)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/even-odd.lisp" "../../arithmetic/even-odd" "even-odd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 540341452)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/trunc.lisp" "../support/trunc" "trunc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1713711045)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/round.lisp" "../lib1/round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 116477925)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/float.lisp" "float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1831232415)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/reps.lisp" "../lib1/reps" "reps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1459033708)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta2/float.lisp" "../lib1.delta2/float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2119265235)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta2/float-extra.lisp" "float-extra" "float-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 429387506)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/float.lisp" "../lib1.delta1/float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1831232415)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/float-extra2.lisp" "float-extra2" "float-extra2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 734738236)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/float.lisp" "../lib1/float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1717498776)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/log.lisp" "../lib1/log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1241286897)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/bits.lisp" "../lib1.delta1/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1333052710)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/bits-extra.lisp" "bits-extra" "bits-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2100846756)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/top.lisp" "../lib1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1893377935)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/util.lisp" "util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2004088401)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/util.lisp" "../support/util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878410565)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/arith.lisp" "arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797309786)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ash.lisp" "../support/ash" "ash" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1250610944)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/extra-rules.lisp" "../../arithmetic/extra-rules" "extra-rules" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496638615)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fp2.lisp" "../../arithmetic/fp2" "fp2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1001657670)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/add.lisp" "add" "add" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1645824547)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/round.lisp" "round" "round" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 116477925)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/reps.lisp" "reps" "reps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1459033708)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ireps.lisp" "../support/ireps" "ireps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 925367279)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ereps.lisp" "../support/ereps" "ereps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1205992813)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/float.lisp" "float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1717498776)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/log.lisp" "log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1241286897)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/bits.lisp" "bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 919497265)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/rtlarr.lisp" "rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 230074667)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/bits.lisp" "../lib1/bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 919497265)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1548353641)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/basic.lisp" "../lib1.delta1/basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 785836430)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1.delta1/basic-extra.lisp" "basic-extra" "basic-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 437266771)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/floor.lisp" "../../arithmetic/floor" "floor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 309404600)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/basic.lisp" "../lib1/basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1548353641)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/rtlarr.lisp" "../lib1/rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 230074667)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/rtl.lisp" "rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2134923781)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/guards.lisp" "../support/guards" "guards" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 518042679)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bvecp-helpers.lisp" "../support/bvecp-helpers" "bvecp-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1281349629)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rtlarr.lisp" "../support/rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 166211276)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/lib1/rtl.lisp" "../lib1/rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2134923781)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/top.lisp" "../support/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 160926708)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/badguys.lisp" "badguys" "badguys" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2027003241)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/guards.lisp" "guards" "guards" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 518042679)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/round-extra.lisp" "round-extra" "round-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 838634521)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/float-extra.lisp" "float-extra" "float-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1200376914)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "arithmetic/inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/fadd-extra.lisp" "fadd-extra" "fadd-extra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 189711229)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/fadd-extra0.lisp" "fadd-extra0" "fadd-extra0" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1961349187)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lextra.lisp" "lextra" "lextra" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 842579911)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lxor.lisp" "lxor" "lxor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 651029821)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lior.lisp" "lior" "lior" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1958592902)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/land.lisp" "land" "land" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 190868162)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/top1.lisp" "top1" "top1" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 276946246)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/fadd.lisp" "fadd" "fadd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 614567302)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fp.lisp" "../../arithmetic/fp" "fp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 184220419)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/simplify-model-helpers.lisp" "simplify-model-helpers" "simplify-model-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 990148787)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/package-defs.lisp" "package-defs" "package-defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 565831662)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/openers.lisp" "openers" "openers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1943184146)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/clocks.lisp" "clocks" "clocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1982779065)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/even-odd2.lisp" "../../arithmetic/even-odd2" "even-odd2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920150912)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/mod4.lisp" "mod4" "mod4" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1880547303)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/simple-loop-helpers.lisp" "simple-loop-helpers" "simple-loop-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1960059434)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rom-helpers.lisp" "rom-helpers" "rom-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 534396735)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/model-helpers.lisp" "model-helpers" "model-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 213177292)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bvecp-helpers.lisp" "bvecp-helpers" "bvecp-helpers" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1281349629)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/stick.lisp" "stick" "stick" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 579397023)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/stick-proofs.lisp" "stick-proofs" "stick-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1047150939)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop3.lisp" "lop3" "lop3" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 700601866)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop3-proofs.lisp" "lop3-proofs" "lop3-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1454066278)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop2.lisp" "lop2" "lop2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1345104715)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop2-proofs.lisp" "lop2-proofs" "lop2-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 391404246)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop1.lisp" "lop1" "lop1" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1585524932)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lop1-proofs.lisp" "lop1-proofs" "lop1-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1086636844)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/add3.lisp" "add3" "add3" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1283940703)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/add3-proofs.lisp" "add3-proofs" "add3-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1234029808)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/drnd-original.lisp" "drnd-original" "drnd-original" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 894044752)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/sgn.lisp" "sgn" "sgn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1569069310)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rnd.lisp" "rnd" "rnd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1255570385)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bits-trunc.lisp" "bits-trunc" "bits-trunc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 61931730)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bits-trunc-proofs.lisp" "bits-trunc-proofs" "bits-trunc-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 4575482)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/sticky.lisp" "sticky" "sticky" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1848398916)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/sticky-proofs.lisp" "sticky-proofs" "sticky-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 26465685)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/oddr.lisp" "oddr" "oddr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1539682331)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/oddr-proofs.lisp" "oddr-proofs" "oddr-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013013497)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/near+.lisp" "near+" "near+" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1598583829)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/near+-proofs.lisp" "near+-proofs" "near+-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1524281015)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/cg.lisp" "../../arithmetic/cg" "cg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1861436219)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/predicate.lisp" "../../arithmetic/predicate" "predicate" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1760934274)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/near.lisp" "near" "near" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1868892361)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/near-proofs.lisp" "near-proofs" "near-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 961688087)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/away.lisp" "away" "away" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 710865809)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/away-proofs.lisp" "away-proofs" "away-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 650675966)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/trunc.lisp" "trunc" "trunc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1713711045)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/trunc-proofs.lisp" "trunc-proofs" "trunc-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 151129358)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lextra0.lisp" "lextra0" "lextra0" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1676673031)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lextra-proofs.lisp" "lextra-proofs" "lextra-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 500860574)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ireps.lisp" "ireps" "ireps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 925367279)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ereps.lisp" "ereps" "ereps" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1205992813)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ereps-proofs.lisp" "ereps-proofs" "ereps-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1367803045)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bias.lisp" "bias" "bias" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 129204844)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bias-proofs.lisp" "bias-proofs" "bias-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 766783327)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logior1.lisp" "logior1" "logior1" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 594828147)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logior1-proofs.lisp" "logior1-proofs" "logior1-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2061804194)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/merge2.lisp" "merge2" "merge2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 185558580)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bvecp-lemmas.lisp" "bvecp-lemmas" "bvecp-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2079468651)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lxor0.lisp" "lxor0" "lxor0" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1172533893)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lxor0-proofs.lisp" "lxor0-proofs" "lxor0-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1057504888)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lior0.lisp" "lior0" "lior0" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 545016676)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lior0-proofs.lisp" "lior0-proofs" "lior0-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1842889706)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/land0.lisp" "land0" "land0" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 496240836)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/land0-proofs.lisp" "land0-proofs" "land0-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1923025965)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/all-ones.lisp" "all-ones" "all-ones" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2003285740)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/mulcat.lisp" "mulcat" "mulcat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 281231437)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/mulcat-proofs.lisp" "mulcat-proofs" "mulcat-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 627721641)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/merge.lisp" "merge" "merge" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1388042792)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ocat.lisp" "ocat" "ocat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2073475867)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/sumbits.lisp" "sumbits" "sumbits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 9708740)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/basic.lisp" "../../arithmetic/basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 16479620)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/log.lisp" "log" "log" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 568865953)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/log-proofs.lisp" "log-proofs" "log-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 342136678)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logxor.lisp" "logxor" "logxor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 22449149)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logeqv.lisp" "logeqv" "logeqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1270937634)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logorc1.lisp" "logorc1" "logorc1" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 667126046)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logior.lisp" "logior" "logior" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948519876)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logior-proofs.lisp" "logior-proofs" "logior-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 679383796)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logand.lisp" "logand" "logand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 193497260)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logand-proofs.lisp" "logand-proofs" "logand-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 424647565)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lognot.lisp" "lognot" "lognot" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327888594)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/induct.lisp" "../../arithmetic/induct" "induct" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1068651620)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/shft.lisp" "shft" "shft" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2075005662)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lnot.lisp" "lnot" "lnot" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1475228708)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/lnot-proofs.lisp" "lnot-proofs" "lnot-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1961923577)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/integerp.lisp" "../../arithmetic/integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1274355872)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/arith2.lisp" "../../arithmetic/arith2" "arith2" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1321734032)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/arith.lisp" "../../arithmetic/arith" "arith" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1942063469)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/mod.lisp" "../../arithmetic/mod" "mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 792040810)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/logs.lisp" "logs" "logs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 824187868)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/decode.lisp" "decode" "decode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1294090937)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/decode-proofs.lisp" "decode-proofs" "decode-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 205806501)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/encode.lisp" "encode" "encode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1081048419)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/float.lisp" "float" "float" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1667671003)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ash.lisp" "ash" "ash" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1250610944)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expt.lisp" "../../arithmetic/expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 397311293)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/fl.lisp" "../../arithmetic/fl" "fl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1643208654)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbitn.lisp" "setbitn" "setbitn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 73211283)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbitn-proofs.lisp" "setbitn-proofs" "setbitn-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1687079699)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbits.lisp" "setbits" "setbits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685120556)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/setbits-proofs.lisp" "setbits-proofs" "setbits-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 128935254)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/cat.lisp" "cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 795157675)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/cat-proofs.lisp" "cat-proofs" "cat-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 88932913)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bitn.lisp" "bitn" "bitn" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482090031)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bitn-proofs.lisp" "bitn-proofs" "bitn-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1278320087)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bits.lisp" "bits" "bits" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1370009319)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bits-proofs.lisp" "bits-proofs" "bits-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 662211535)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bvecp.lisp" "bvecp" "bvecp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1967435644)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/bvecp-proofs.lisp" "bvecp-proofs" "bvecp-proofs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 906971511)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/top.lisp" "../../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/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/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/power2p.lisp" "../../arithmetic/power2p" "power2p" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 651335974)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/negative-syntaxp.lisp" "../../arithmetic/negative-syntaxp" "negative-syntaxp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1540911563)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/expo.lisp" "../../arithmetic/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/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/rtl/rel8/arithmetic/even-odd.lisp" "even-odd" "even-odd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 540341452)) (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/power2p.lisp" "power2p" "power2p" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 651335974)) (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/rtl/rel8/arithmetic/inverted-factor.lisp" "inverted-factor" "inverted-factor" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 357645011)) ("/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/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/rtl/rel8/support/support/rtl.lisp" "rtl" "rtl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1638971093)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/cat-def.lisp" "cat-def" "cat-def" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1254054176)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rtlarr.lisp" "rtlarr" "rtlarr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 166211276)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/rewrite-theory.lisp" "rewrite-theory" "rewrite-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1118210542)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/ground-zero.lisp" "ground-zero" "ground-zero" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 635436423)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/arithmetic/ground-zero.lisp" "../../arithmetic/ground-zero" "ground-zero" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 403163111)) (LOCAL ("/usr/share/acl2-6.3/books/rtl/rel8/support/support/util.lisp" "util" "util" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878410565)) ("/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/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)) (LOCAL ("/usr/share/acl2-6.3/books/ordinals/ordinal-total-order.lisp" "ordinal-total-order" "ordinal-total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 757763360)) ("/usr/share/acl2-6.3/books/ordinals/ordinal-definitions.lisp" "ordinal-definitions" "ordinal-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1478376100))
1588584069
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / quadratic-reciprocity / mersenne.cert
