(IN-PACKAGE "ACL2") "ACL2 Version 2.7" :BEGIN-PORTCULLIS-CMDS (INCLUDE-BOOK "/v/net2/v2/users/prof/moore/publications/trecia/support/utilities") :END-PORTCULLIS-CMDS (("/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp" "utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 67149996) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/quotient-remainder-lemmas.lisp" "/projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 92839301) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 24321978) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 115970970) ("/v/filer1b/v0q004/acl2/v2-7/books/data-structures/utilities.lisp" "../data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 72444240) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top-with-meta.lisp" "/projects/acl2/v2-7/books/arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 175638983) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta.lisp" "../meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 146179060) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 69450866) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 113270299) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 220828626) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 5165141) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 263462730) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 192778911) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 130234613) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 64148425) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143723605) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 260688904) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 106260818) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 44566077) ("/v/net2/v2/users/prof/moore/publications/trecia/support/m5.lisp" "/v/net2/v2/users/prof/moore/publications/trecia/support/m5" "m5" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 234757449)) (("/v/net2/v2/users/prof/moore/publications/trecia/support/vcg-examples.lisp" "vcg-examples" "vcg-examples" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 58822494) ("/v/net2/v2/users/prof/moore/publications/trecia/support/demo.lisp" "demo" "demo" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 58567155) ("/v/net2/v2/users/prof/moore/publications/trecia/support/defpun.lisp" "defpun" "defpun" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143438860) ("/v/net2/v2/users/prof/moore/publications/trecia/support/utilities.lisp" "utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 67149996) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/quotient-remainder-lemmas.lisp" "/projects/acl2/v2-7/books/ihs/quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 92839301) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 223551077)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top.lisp" "../arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 263462730)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 192778911)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 64148425)) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 24321978) ("/v/filer1b/v0q004/acl2/v2-7/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 115970970) ("/v/filer1b/v0q004/acl2/v2-7/books/data-structures/utilities.lisp" "../data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 72444240) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top-with-meta.lisp" "/projects/acl2/v2-7/books/arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 175638983) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta.lisp" "../meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 146179060) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 69450866) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/equalities.lisp" "../arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143723605)) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 113270299) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 220828626) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 185835692)) ("/v/filer1b/v0q004/acl2/v2-7/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 5165141) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 263462730) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 192778911) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 49344105)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 130234613)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143723605)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 260688904)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 106260818)) (LOCAL ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 44566077)) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 130234613) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 64148425) ("/v/filer1b/v0q004/acl2/v2-7/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 143723605) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 260688904) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 106260818) ("/v/filer1b/v0q004/acl2/v2-7/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 44566077) ("/v/net2/v2/users/prof/moore/publications/trecia/support/m5.lisp" "m5" "m5" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 234757449)) 247753012