(IN-PACKAGE "ACL2")
"ACL2 Version 3.4"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/Users/cce/plt/research/dracula/release/src/teachpacks/rand.lisp" "rand" "rand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 77426194) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 93892613)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 133270042)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 38204680)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 236153598)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 55850522)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 149346625)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 55850522)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 228612478)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48983854)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 257416865)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 5684246)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 143445080)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 111091463)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 164506980)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 228612478)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 200161728)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 50450762)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 143892352)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18126647)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 153572399)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 186483675)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 125584907)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 31546954)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 73654194)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 125584907)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 125584907)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 208853457)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 42791120)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 158421296)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 42791120)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 110727519)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 158421296)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 158421296)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18224623)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18224623)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18224623)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 170738169)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 170738169)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 207476124)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 102604516)) (LOCAL ("/Users/cce/Local/ACL2/3.4/openmcl64/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 153572399)))
151053034