acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / system / too-many-ifs.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "tools/flag" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (MAKE-FLAG PSEUDO-TERMP-FLG PSEUDO-TERMP :FLAG-VAR FLG :FLAG-MAPPING ((PSEUDO-TERMP . TERM) (PSEUDO-TERM-LISTP . LIST)) :DEFTHM-MACRO-NAME DEFTHM-PSEUDO-TERMP :LOCAL T) (PROGN (LOGIC) (LOCAL (VALUE-TRIPLE :ELIDED)) (DEFMACRO DEFTHM-PSEUDO-TERMP (&REST ARGS) (FLAG::MAKE-DEFTHM-MACRO-FN ARGS (QUOTE ((PSEUDO-TERMP . TERM) (PSEUDO-TERM-LISTP . LIST))) (QUOTE FLG) (QUOTE (PSEUDO-TERMP-FLG FLG X LST)))) (LOCAL (VALUE-TRIPLE :ELIDED)) (PROGN (TABLE FLAG::FLAG-FNS (QUOTE PSEUDO-TERMP) (QUOTE (PSEUDO-TERMP-FLG ((PSEUDO-TERMP . TERM) (PSEUDO-TERM-LISTP . LIST)) DEFTHM-PSEUDO-TERMP PSEUDO-TERMP-FLG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE PSEUDO-TERM-LISTP) (QUOTE (PSEUDO-TERMP-FLG ((PSEUDO-TERMP . TERM) (PSEUDO-TERM-LISTP . LIST)) DEFTHM-PSEUDO-TERMP PSEUDO-TERMP-FLG-EQUIVALENCES)))) (LOCAL (VALUE-TRIPLE :ELIDED)))) (4 RECORD-EXPANSION (VERIFY-TERMINATION VAR-COUNTS1) (VALUE-TRIPLE :REDUNDANT)) (5 RECORD-EXPANSION (MAKE-FLAG VAR-COUNTS1-FLG VAR-COUNTS1 :FLAG-VAR FLG :FLAG-MAPPING ((VAR-COUNTS1 . TERM) (VAR-COUNTS1-LST . LIST)) :DEFTHM-MACRO-NAME DEFTHM-VAR-COUNTS1 :LOCAL T) (PROGN (LOGIC) (LOCAL (VALUE-TRIPLE :ELIDED)) (DEFMACRO DEFTHM-VAR-COUNTS1 (&REST ARGS) (FLAG::MAKE-DEFTHM-MACRO-FN ARGS (QUOTE ((VAR-COUNTS1 . TERM) (VAR-COUNTS1-LST . LIST))) (QUOTE FLG) (QUOTE (VAR-COUNTS1-FLG FLG RHS ARG LST ACC)))) (LOCAL (VALUE-TRIPLE :ELIDED)) (PROGN (TABLE FLAG::FLAG-FNS (QUOTE VAR-COUNTS1) (QUOTE (VAR-COUNTS1-FLG ((VAR-COUNTS1 . TERM) (VAR-COUNTS1-LST . LIST)) DEFTHM-VAR-COUNTS1 VAR-COUNTS1-FLG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE VAR-COUNTS1-LST) (QUOTE (VAR-COUNTS1-FLG ((VAR-COUNTS1 . TERM) (VAR-COUNTS1-LST . LIST)) DEFTHM-VAR-COUNTS1 VAR-COUNTS1-FLG-EQUIVALENCES)))) (LOCAL (VALUE-TRIPLE :ELIDED)))) (8 RECORD-EXPANSION (VERIFY-TERMINATION VAR-COUNTS) (VALUE-TRIPLE :REDUNDANT)) (11 RECORD-EXPANSION (VERIFY-TERMINATION COUNT-IFS) (VALUE-TRIPLE :REDUNDANT)) (12 RECORD-EXPANSION (VERIFY-TERMINATION TOO-MANY-IFS0) (VALUE-TRIPLE :REDUNDANT)) (13 RECORD-EXPANSION (VERIFY-TERMINATION TOO-MANY-IFS-PRE-REWRITE-BUILTIN) (VALUE-TRIPLE :REDUNDANT)) (14 RECORD-EXPANSION (VERIFY-TERMINATION OCCUR-CNT-BOUNDED) (VALUE-TRIPLE :REDUNDANT)) (15 RECORD-EXPANSION (MAKE-FLAG OCCUR-CNT-BOUNDED-FLG OCCUR-CNT-BOUNDED :FLAG-VAR FLG :FLAG-MAPPING ((OCCUR-CNT-BOUNDED . TERM) (OCCUR-CNT-BOUNDED-LST . LIST)) :DEFTHM-MACRO-NAME DEFTHM-OCCUR-CNT-BOUNDED :LOCAL T) (PROGN (LOGIC) (LOCAL (VALUE-TRIPLE :ELIDED)) (DEFMACRO DEFTHM-OCCUR-CNT-BOUNDED (&REST ARGS) (FLAG::MAKE-DEFTHM-MACRO-FN ARGS (QUOTE ((OCCUR-CNT-BOUNDED . TERM) (OCCUR-CNT-BOUNDED-LST . LIST))) (QUOTE FLG) (QUOTE (OCCUR-CNT-BOUNDED-FLG FLG TERM2 TERM1 LST A M BOUND-M)))) (LOCAL (VALUE-TRIPLE :ELIDED)) (PROGN (TABLE FLAG::FLAG-FNS (QUOTE OCCUR-CNT-BOUNDED) (QUOTE (OCCUR-CNT-BOUNDED-FLG ((OCCUR-CNT-BOUNDED . TERM) (OCCUR-CNT-BOUNDED-LST . LIST)) DEFTHM-OCCUR-CNT-BOUNDED OCCUR-CNT-BOUNDED-FLG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE OCCUR-CNT-BOUNDED-LST) (QUOTE (OCCUR-CNT-BOUNDED-FLG ((OCCUR-CNT-BOUNDED . TERM) (OCCUR-CNT-BOUNDED-LST . LIST)) DEFTHM-OCCUR-CNT-BOUNDED OCCUR-CNT-BOUNDED-FLG-EQUIVALENCES)))) (LOCAL (VALUE-TRIPLE :ELIDED)))) (19 RECORD-EXPANSION (VERIFY-TERMINATION TOO-MANY-IFS1) (VALUE-TRIPLE :REDUNDANT)) (20 RECORD-EXPANSION (VERIFY-TERMINATION TOO-MANY-IFS-POST-REWRITE-BUILTIN) (VALUE-TRIPLE :REDUNDANT)))
(("/usr/share/acl2-6.3/books/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573))
(("/usr/share/acl2-6.3/books/system/too-many-ifs.lisp" "too-many-ifs" "too-many-ifs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1919958005) ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499) ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577) ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479) ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595) ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372) ("/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)) ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295) ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966) ("/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)) ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970) ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523) ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370) ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314) ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595) ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866) ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914) ("/usr/share/acl2-6.3/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1939433116) ("/usr/share/acl2-6.3/books/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573))
660783717