(IN-PACKAGE "ACL2")
"ACL2 Version 3.2"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/Users/cce/plt/research/dracula/trunk/src/teachpacks/list-utilities.lisp" "list-utilities" "list-utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 180354812) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp" "arithmetic-2/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 230207184) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "floor-mod-helper" "floor-mod-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 250164037)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "../../ihs/quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 75580058)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 41383250)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "../arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 51353441)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 192778911)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 77763855)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 64148425)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 88130948)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 115970970)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/data-structures/utilities.lisp" "../data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 58465099)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/top.lisp" "../meta/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 112844677)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/post.lisp" "post" "post" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 111875395)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 159968747)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 236109322)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82194709)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 249242356)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 254673040)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/collect-terms-meta.lisp" "collect-terms-meta" "collect-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 86943081)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/cancel-terms-meta.lisp" "cancel-terms-meta" "cancel-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 201143376)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/cancel-terms-helper.lisp" "cancel-terms-helper" "cancel-terms-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 59403007)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/common-meta.lisp" "common-meta" "common-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18424879)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 23974661)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 27882705)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/pre.lisp" "pre" "pre" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 217072582)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 228875392)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130872758)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp" "numerator-and-denominator-helper" "numerator-and-denominator-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 41852482)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 208853457)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 244408932)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 244408932)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 136146365)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 239360158)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 239360158)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 51473664)) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 51353441) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 192778911) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 49344105)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130234613)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 103475026)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260688904)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 106260818)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 44566077)) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 77763855) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130234613) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 64148425) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 103475026) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260688904) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 106260818) ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 44566077))
133910724