acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / leftist-trees / leftist-tree-defthms.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/leftist-trees/leftist-tree-defthms.lisp" "leftist-tree-defthms" "leftist-tree-defthms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 559063720) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/top.lisp" "arithmetic-5/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 414221999)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/top.lisp" "lib/floor-mod/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2036487313)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/mod-expt-fast.lisp" "mod-expt-fast" "mod-expt-fast" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 8474989)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/logand.lisp" "logand" "logand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 477689935)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/logand-helper.lisp" "logand-helper" "logand-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1567870466)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/truncate-rem.lisp" "truncate-rem" "truncate-rem" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1222339411)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/more-floor-mod.lisp" "more-floor-mod" "more-floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1054313738)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/if-normalization.lisp" "if-normalization" "if-normalization" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 478555307)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod.lisp" "floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1117227810)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-helper.lisp" "floor-mod-helper" "floor-mod-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 383675918)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-basic.lisp" "floor-mod-basic" "floor-mod-basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1868400972)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/floor-mod-basic-helper.lisp" "floor-mod-basic-helper" "floor-mod-basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122255223)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/floor-mod/forcing-types.lisp" "forcing-types" "forcing-types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2092136594)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/common.lisp" "../basic-ops/common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2005694427)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/top.lisp" "../basic-ops/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 227046385)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks.lisp" "../basic-ops/building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 3355516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/top.lisp" "lib/basic-ops/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 227046385)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 322732972)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/forcing-types.lisp" "forcing-types" "forcing-types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 176314612)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/if-normalization.lisp" "if-normalization" "if-normalization" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2119667687)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 586482828)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities.lisp" "simple-equalities-and-inequalities" "simple-equalities-and-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 869088724)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simple-equalities-and-inequalities-helper.lisp" "simple-equalities-and-inequalities-helper" "simple-equalities-and-inequalities-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 21977321)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2009755655)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1042653498)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/types.lisp" "types" "types" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1952837234)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/types-helper.lisp" "types-helper" "types-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308711892)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 414495578)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1484950306)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2103891710)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp-helper.lisp" "integerp-helper" "integerp-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1650787804)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1666343128)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1658521281)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 475372159)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1950245832)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1441743781)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2047460336)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 668797475)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1040308974)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2005694427)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 3355516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/building-blocks-helper.lisp" "building-blocks-helper" "building-blocks-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1904099973)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/top.lisp" "../../support/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1197165143)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/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-5/support/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2058266018)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1097318215)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 628802930)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1078019670)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 806765711)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/support/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153952210)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/dynamic-e-d.lisp" "dynamic-e-d" "dynamic-e-d" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689130045)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/distributivity.lisp" "distributivity" "distributivity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1422342520)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-5/lib/basic-ops/we-are-here.lisp" "we-are-here" "we-are-here" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1006471420)) ("/usr/share/acl2-6.3/books/leftist-trees/leftist-tree-defuns.lisp" "leftist-tree-defuns" "leftist-tree-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 241936917))
2106512374