acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / cutil / defredundant-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (ENCAPSULATE NIL (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) (DECLARE (XARGS :NORMALIZE NIL)) (+ 1 CUTIL::X)) (DEFTHM CUTIL::NATP-OF-F1 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F1 CUTIL::X)))) (DEFUND CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (+ 1 CUTIL::X)) (DEFTHMD CUTIL::NATP-OF-F2 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F2 CUTIL::X))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::F2)))) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X) :VERIFY-GUARDS T)) (+ 1 CUTIL::X)) (IN-THEORY (DISABLE (:E CUTIL::F3))) (MUTUAL-RECURSION (DEFUN CUTIL::F4-TERM (CUTIL::X) (DECLARE (XARGS :GUARD (PSEUDO-TERMP CUTIL::X))) (IF (ATOM CUTIL::X) 1 (IF (QUOTEP CUTIL::X) 2 (CONS (CAR CUTIL::X) (CUTIL::F4-LIST (CDR CUTIL::X)))))) (DEFUN CUTIL::F4-LIST (CUTIL::X) (DECLARE (XARGS :GUARD (PSEUDO-TERM-LISTP CUTIL::X))) (IF (ATOM CUTIL::X) NIL (CONS (CUTIL::F4-TERM (CAR CUTIL::X)) (CUTIL::F4-LIST (CDR CUTIL::X)))))) (DEFINLINE CUTIL::F5 (CUTIL::X) (DECLARE (XARGS :GUARD T)) CUTIL::X) (DEFINLINED CUTIL::F6 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (+ 1 CUTIL::X)) (DEFUN CUTIL::F7 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 1 CUTIL::X)) (DEFINLINE CUTIL::F8 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM :GUARD (NATP CUTIL::X))) (+ 1 CUTIL::X)) (DEFUN CUTIL::M (CUTIL::X CUTIL::Y) (+ (ACL2-COUNT CUTIL::X) (ACL2-COUNT CUTIL::Y))) (DEFUND CUTIL::F9 (CUTIL::X CUTIL::Y) (DECLARE (XARGS :MEASURE (CUTIL::M CUTIL::X CUTIL::Y))) (IF (AND (ATOM CUTIL::X) (ATOM CUTIL::Y)) 0 (+ (CUTIL::F9 (CDR CUTIL::X) (CDR CUTIL::Y))))))) (CUTIL::DEFREDUNDANT CUTIL::F1 CUTIL::NATP-OF-F1 CUTIL::F2 CUTIL::NATP-OF-F2 CUTIL::F3 CUTIL::F9)) (ENCAPSULATE NIL (LOCAL (PROGN (DEFUN CUTIL::F1 (CUTIL::X) (DECLARE (XARGS :NORMALIZE NIL)) (+ 1 CUTIL::X)) (DEFTHM CUTIL::NATP-OF-F1 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F1 CUTIL::X)))) (DEFUND CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :VERIFY-GUARDS NIL)) (+ 1 CUTIL::X)) (DEFTHMD CUTIL::NATP-OF-F2 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F2 CUTIL::X))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::F2)))) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X) :VERIFY-GUARDS T)) (+ 1 CUTIL::X)) (IN-THEORY (DISABLE (:E CUTIL::F3))) (MUTUAL-RECURSION (DEFUN CUTIL::F4-TERM (CUTIL::X) (DECLARE (XARGS :GUARD (PSEUDO-TERMP CUTIL::X))) (IF (ATOM CUTIL::X) 1 (IF (QUOTEP CUTIL::X) 2 (CONS (CAR CUTIL::X) (CUTIL::F4-LIST (CDR CUTIL::X)))))) (DEFUN CUTIL::F4-LIST (CUTIL::X) (DECLARE (XARGS :GUARD (PSEUDO-TERM-LISTP CUTIL::X))) (IF (ATOM CUTIL::X) NIL (CONS (CUTIL::F4-TERM (CAR CUTIL::X)) (CUTIL::F4-LIST (CDR CUTIL::X)))))) (DEFINLINE CUTIL::F5 (CUTIL::X) (DECLARE (XARGS :GUARD T)) CUTIL::X) (DEFINLINED CUTIL::F6 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (+ 1 CUTIL::X)) (DEFUN CUTIL::F7 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 1 CUTIL::X)) (DEFINLINE CUTIL::F8 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM :GUARD (NATP CUTIL::X))) (+ 1 CUTIL::X)) (DEFUN CUTIL::M (CUTIL::X CUTIL::Y) (+ (ACL2-COUNT CUTIL::X) (ACL2-COUNT CUTIL::Y))) (DEFUND CUTIL::F9 (CUTIL::X CUTIL::Y) (DECLARE (XARGS :MEASURE (CUTIL::M CUTIL::X CUTIL::Y))) (IF (AND (ATOM CUTIL::X) (ATOM CUTIL::Y)) 0 (+ (CUTIL::F9 (CDR CUTIL::X) (CDR CUTIL::Y))))))) (RECORD-EXPANSION (CUTIL::DEFREDUNDANT CUTIL::F1 CUTIL::NATP-OF-F1 CUTIL::F2 CUTIL::NATP-OF-F2 CUTIL::F3 CUTIL::F9) (ENCAPSULATE NIL (SET-ENFORCE-REDUNDANCY T) (LOGIC) (DEFUN CUTIL::F1 (CUTIL::X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS NIL)) (DECLARE (XARGS :NORMALIZE NIL)) (+ 1 CUTIL::X)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION CUTIL::F1) (:EXECUTABLE-COUNTERPART CUTIL::F1) (:DEFINITION CUTIL::F1)) NIL)) (DEFTHM CUTIL::NATP-OF-F1 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F1 CUTIL::X)))) (IN-THEORY (E/D ((:REWRITE CUTIL::NATP-OF-F1)) NIL)) (DEFUN CUTIL::F2 (CUTIL::X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS NIL)) (DECLARE (XARGS)) (+ 1 CUTIL::X)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION CUTIL::F2) (:EXECUTABLE-COUNTERPART CUTIL::F2)) ((:DEFINITION CUTIL::F2)))) (DEFTHM CUTIL::NATP-OF-F2 (IMPLIES (NATP CUTIL::X) (NATP (CUTIL::F2 CUTIL::X))) :RULE-CLASSES :TYPE-PRESCRIPTION) (IN-THEORY (E/D NIL ((:TYPE-PRESCRIPTION CUTIL::NATP-OF-F2)))) (DEFUN CUTIL::F3 (CUTIL::X) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS T)) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (+ 1 CUTIL::X)) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION CUTIL::F3) (:DEFINITION CUTIL::F3)) ((:EXECUTABLE-COUNTERPART CUTIL::F3)))) (DEFUN CUTIL::F9 (CUTIL::X CUTIL::Y) (DECLARE (XARGS :MODE :LOGIC :VERIFY-GUARDS NIL)) (DECLARE (XARGS :MEASURE (:? CUTIL::Y CUTIL::X))) (DECLARE (XARGS)) (IF (AND (ATOM CUTIL::X) (ATOM CUTIL::Y)) 0 (+ (CUTIL::F9 (CDR CUTIL::X) (CDR CUTIL::Y))))) (IN-THEORY (E/D ((:TYPE-PRESCRIPTION CUTIL::F9) (:EXECUTABLE-COUNTERPART CUTIL::F9)) ((:INDUCTION CUTIL::F9) (:DEFINITION CUTIL::F9)))))))) (6 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:DEFINITION CUTIL::F1) T) (VALUE-TRIPLE :SUCCESS)) (7 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:DEFINITION CUTIL::F2) NIL) (VALUE-TRIPLE :SUCCESS)) (8 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:DEFINITION CUTIL::F3) T) (VALUE-TRIPLE :SUCCESS)) (9 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:DEFINITION CUTIL::F9) NIL) (VALUE-TRIPLE :SUCCESS)) (10 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:REWRITE CUTIL::NATP-OF-F1) T) (VALUE-TRIPLE :SUCCESS)) (11 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:TYPE-PRESCRIPTION CUTIL::NATP-OF-F2) NIL) (VALUE-TRIPLE :SUCCESS)) (12 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:EXECUTABLE-COUNTERPART CUTIL::F1) T) (VALUE-TRIPLE :SUCCESS)) (13 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:EXECUTABLE-COUNTERPART CUTIL::F2) T) (VALUE-TRIPLE :SUCCESS)) (14 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:EXECUTABLE-COUNTERPART CUTIL::F3) NIL) (VALUE-TRIPLE :SUCCESS)) (15 RECORD-EXPANSION (CUTIL::ASSERT-ENABLED (:EXECUTABLE-COUNTERPART CUTIL::F9) T) (VALUE-TRIPLE :SUCCESS)))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/cutil/defredundant-tests.lisp" "defredundant-tests" "defredundant-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1776646794) ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718) ("/usr/share/acl2-6.3/books/cutil/defredundant.lisp" "defredundant" "defredundant" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1198380940) ("/usr/share/acl2-6.3/books/cutil/support.lisp" "support" "support" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1180314020) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/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/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
409826519