acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / regex / regex-exec.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((30 RECORD-EXPANSION (MAKE-FLAG RUN-REGEX-FLAG RUN-REGEX) (ENCAPSULATE NIL (LOGIC) (SET-IGNORE-OK T) (FLAG::ID (DEFUN-NX RUN-REGEX-FLAG (FLAG INDEX BACKREFS REGEX STR ILIST MIN MAX) (DECLARE (XARGS :VERIFY-GUARDS NIL :NORMALIZE NIL :MEASURE (CASE FLAG (RUN-REGEX (RUN-REGEX-MEASURE REGEX STR INDEX)) (RUN-REGEX-LIST (IF (ATOM ILIST) (QUOTE 0) (RUN-REGEX-LIST-MEASURE REGEX STR ILIST))) (RUN-REPEAT (RUN-REPEAT-MEASURE REGEX STR INDEX MIN)) (OTHERWISE (IF (ATOM ILIST) (QUOTE 0) (RUN-REPEAT-LIST-MEASURE REGEX STR ILIST MIN)))) :HINTS NIL :WELL-FOUNDED-RELATION O< :MODE :LOGIC) (IGNORABLE INDEX BACKREFS REGEX STR ILIST MIN MAX)) (COND ((EQUAL FLAG (QUOTE RUN-REGEX)) (IF (R-CONCAT-P REGEX) ((LAMBDA (LEFT RIGHT BACKREFS INDEX STR) (RUN-REGEX-FLAG (QUOTE RUN-REGEX-LIST) NIL NIL RIGHT STR (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS LEFT STR NIL NIL NIL) NIL NIL)) (R-CONCAT-LEFT REGEX) (R-CONCAT-RIGHT REGEX) BACKREFS INDEX STR) (IF (R-DISJUNCT-P REGEX) ((LAMBDA (LEFT RIGHT BACKREFS INDEX STR) (BINARY-APPEND (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS LEFT STR NIL NIL NIL) (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS RIGHT STR NIL NIL NIL))) (R-DISJUNCT-LEFT REGEX) (R-DISJUNCT-RIGHT REGEX) BACKREFS INDEX STR) (IF (R-EXACT-P REGEX) ((LAMBDA (C BACKREFS STR INDEX) (IF (< INDEX (LENGTH STR)) (IF (EQUAL C (CHAR STR INDEX)) (CONS (CONS (BINARY-+ (QUOTE 1) INDEX) BACKREFS) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL))) (R-EXACT-VAL REGEX) BACKREFS STR INDEX) (IF (R-ANY-P REGEX) ((LAMBDA (BACKREFS STR INDEX) (IF (< INDEX (LENGTH STR)) (CONS (CONS (BINARY-+ (QUOTE 1) INDEX) BACKREFS) (QUOTE NIL)) (QUOTE NIL))) BACKREFS STR INDEX) (IF (R-EMPTY-P REGEX) ((LAMBDA (BACKREFS INDEX) (CONS (CONS INDEX BACKREFS) (QUOTE NIL))) BACKREFS INDEX) (IF (R-NOMATCH-P REGEX) (QUOTE NIL) (IF (R-END-P REGEX) ((LAMBDA (BACKREFS STR INDEX) (IF (EQUAL INDEX (LENGTH STR)) (CONS (CONS INDEX BACKREFS) (QUOTE NIL)) (QUOTE NIL))) BACKREFS STR INDEX) (IF (R-BEGIN-P REGEX) ((LAMBDA (BACKREFS INDEX) (IF (EQUAL INDEX (QUOTE 0)) (CONS (CONS (QUOTE 0) BACKREFS) (QUOTE NIL)) (QUOTE NIL))) BACKREFS INDEX) (IF (R-REPEAT-P REGEX) ((LAMBDA (REG MIN MAX BACKREFS INDEX STR) ((LAMBDA (REPEAT BACKREFS INDEX MIN) (IF (ZP (NFIX MIN)) (CONS (CONS INDEX BACKREFS) REPEAT) REPEAT)) (RUN-REGEX-FLAG (QUOTE RUN-REPEAT) INDEX BACKREFS REG STR NIL MIN MAX) BACKREFS INDEX MIN)) (R-REPEAT-REGEX REGEX) (R-REPEAT-MIN REGEX) (R-REPEAT-MAX REGEX) BACKREFS INDEX STR) (IF (R-CHARSET-P REGEX) ((LAMBDA (S BACKREFS STR INDEX) (IF (< INDEX (LENGTH STR)) (IF (IN-CHARSET (CHAR STR INDEX) S) (CONS (CONS (BINARY-+ (QUOTE 1) INDEX) BACKREFS) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL))) (R-CHARSET-SET REGEX) BACKREFS STR INDEX) (IF (R-GROUP-P REGEX) ((LAMBDA (REG GID BACKREFS INDEX STR) (STORE-BACKREFS (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS REG STR NIL NIL NIL) STR INDEX GID)) (R-GROUP-REGEX REGEX) (R-GROUP-INDEX REGEX) BACKREFS INDEX STR) (IF (R-BACKREF-P REGEX) ((LAMBDA (BRID STR INDEX BACKREFS) ((LAMBDA (BR BACKREFS INDEX STR) (IF BR ((LAMBDA (NEWIND BACKREFS) (IF NEWIND (CONS (CONS NEWIND BACKREFS) (QUOTE NIL)) (QUOTE NIL))) (CHECK-BACKREF STR INDEX BR) BACKREFS) (QUOTE NIL))) (NTH BRID BACKREFS) BACKREFS INDEX STR)) (R-BACKREF-INDEX REGEX) STR INDEX BACKREFS) (QUOTE (BAD-INPUT))))))))))))))) ((EQUAL FLAG (QUOTE RUN-REGEX-LIST)) (IF (REG-ILIST-GUARD REGEX STR ILIST) (IF (CONSP ILIST) (BINARY-APPEND (RUN-REGEX-FLAG (QUOTE RUN-REGEX) (CAR (CAR ILIST)) (CDR (CAR ILIST)) REGEX STR NIL NIL NIL) (RUN-REGEX-FLAG (QUOTE RUN-REGEX-LIST) NIL NIL REGEX STR (CDR ILIST) NIL NIL)) (QUOTE NIL)) (QUOTE NIL))) ((EQUAL FLAG (QUOTE RUN-REPEAT)) (IF (REG-STR-BR-GUARD REGEX STR INDEX BACKREFS) (IF (REPEAT-GUARD MIN MAX) (IF (EQUAL MAX (QUOTE 0)) (IF (ZP (NFIX MIN)) (CONS (CONS INDEX BACKREFS) (QUOTE NIL)) ((LAMBDA (SUFFIXES STR REGEX MAX INDEX MIN) (IF (ZP (NFIX MIN)) ((LAMBDA (SHORT-SUFF MAX MIN REGEX SUFFIXES STR INDEX) (IF (< INDEX (LENGTH STR)) (BINARY-APPEND SUFFIXES (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) NIL NIL REGEX STR SHORT-SUFF MIN (QUOTE -1))) SUFFIXES)) (REMOVE-ALL-LONGER-EQUAL-IL SUFFIXES INDEX) (QUOTE 0) MIN REGEX SUFFIXES STR INDEX) (IF (< (MIN-IDX-IL SUFFIXES STR) INDEX) (QUOTE NIL) ((LAMBDA (VAL SUFFIXES MIN) (IF (< (QUOTE 1) MIN) VAL (BINARY-APPEND SUFFIXES VAL))) (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) NIL NIL REGEX STR SUFFIXES (BINARY-+ (QUOTE -1) MIN) (QUOTE -1)) SUFFIXES MIN)))) (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS REGEX STR NIL NIL NIL) STR REGEX (QUOTE 0) INDEX MIN)) ((LAMBDA (SUFFIXES STR REGEX MAX INDEX MIN) (IF (ZP (NFIX MIN)) ((LAMBDA (SHORT-SUFF MAX MIN REGEX SUFFIXES STR INDEX) (IF (< INDEX (LENGTH STR)) (BINARY-APPEND SUFFIXES (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) NIL NIL REGEX STR SHORT-SUFF MIN (BINARY-+ (QUOTE -1) MAX))) SUFFIXES)) (REMOVE-ALL-LONGER-EQUAL-IL SUFFIXES INDEX) MAX MIN REGEX SUFFIXES STR INDEX) (IF (< (MIN-IDX-IL SUFFIXES STR) INDEX) (QUOTE NIL) ((LAMBDA (VAL SUFFIXES MIN) (IF (< (QUOTE 1) MIN) VAL (BINARY-APPEND SUFFIXES VAL))) (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) NIL NIL REGEX STR SUFFIXES (BINARY-+ (QUOTE -1) MIN) (BINARY-+ (QUOTE -1) MAX)) SUFFIXES MIN)))) (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS REGEX STR NIL NIL NIL) STR REGEX MAX INDEX MIN)) (QUOTE NIL)) (QUOTE NIL))) (T (IF (REG-ILIST-GUARD REGEX STR ILIST) (IF (REPEAT-GUARD MIN MAX) (IF (CONSP ILIST) (BINARY-APPEND (RUN-REGEX-FLAG (QUOTE RUN-REPEAT) (CAR (CAR ILIST)) (CDR (CAR ILIST)) REGEX STR NIL MIN MAX) (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) NIL NIL REGEX STR (CDR ILIST) MIN MAX)) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)))))) (DEFMACRO DEFTHM-RUN-REGEX-FLAG (&REST ARGS) (FLAG::MAKE-DEFTHM-MACRO-FN ARGS (QUOTE ((RUN-REGEX . RUN-REGEX) (RUN-REGEX-LIST . RUN-REGEX-LIST) (RUN-REPEAT . RUN-REPEAT) (RUN-REPEAT-LIST . RUN-REPEAT-LIST))) (QUOTE FLAG) (QUOTE (RUN-REGEX-FLAG FLAG INDEX BACKREFS REGEX STR ILIST MIN MAX)))) (FLAG::ID (WITH-OUTPUT :OFF (PROVE EVENT) (ENCAPSULATE NIL (LOGIC) (LOCAL (DEFTHM FLAG::FLAG-EQUIV-LEMMA (EQUAL (RUN-REGEX-FLAG FLAG INDEX BACKREFS REGEX STR ILIST MIN MAX) (CASE FLAG (RUN-REGEX (RUN-REGEX REGEX STR INDEX BACKREFS)) (RUN-REGEX-LIST (RUN-REGEX-LIST REGEX STR ILIST)) (RUN-REPEAT (RUN-REPEAT REGEX STR INDEX BACKREFS MIN MAX)) (OTHERWISE (RUN-REPEAT-LIST REGEX STR ILIST MIN MAX)))) :HINTS (("Goal" :INDUCT (RUN-REGEX-FLAG FLAG INDEX BACKREFS REGEX STR ILIST MIN MAX) :IN-THEORY (SET-DIFFERENCE-THEORIES (UNION-THEORIES (THEORY (QUOTE MINIMAL-THEORY)) (QUOTE ((:INDUCTION RUN-REGEX-FLAG) (:REWRITE FLAG::EXPAND-ALL-HIDES)))) (QUOTE ((:DEFINITION MV-NTH) (:EXECUTABLE-COUNTERPART FORCE))))) (FLAG::FLAG-EXPAND-COMPUTED-HINT STABLE-UNDER-SIMPLIFICATIONP CLAUSE (QUOTE (RUN-REGEX-FLAG RUN-REGEX RUN-REGEX-LIST RUN-REPEAT RUN-REPEAT-LIST)))))) (DEFTHM RUN-REGEX-FLAG-EQUIVALENCES (AND (EQUAL (RUN-REGEX-FLAG (QUOTE RUN-REGEX) INDEX BACKREFS REGEX STR ILIST MIN MAX) (RUN-REGEX REGEX STR INDEX BACKREFS)) (EQUAL (RUN-REGEX-FLAG (QUOTE RUN-REGEX-LIST) INDEX BACKREFS REGEX STR ILIST MIN MAX) (RUN-REGEX-LIST REGEX STR ILIST)) (EQUAL (RUN-REGEX-FLAG (QUOTE RUN-REPEAT) INDEX BACKREFS REGEX STR ILIST MIN MAX) (RUN-REPEAT REGEX STR INDEX BACKREFS MIN MAX)) (EQUAL (RUN-REGEX-FLAG (QUOTE RUN-REPEAT-LIST) INDEX BACKREFS REGEX STR ILIST MIN MAX) (RUN-REPEAT-LIST REGEX STR ILIST MIN MAX))))))) (PROGN (TABLE FLAG::FLAG-FNS (QUOTE RUN-REGEX) (QUOTE (RUN-REGEX-FLAG ((RUN-REGEX . RUN-REGEX) (RUN-REGEX-LIST . RUN-REGEX-LIST) (RUN-REPEAT . RUN-REPEAT) (RUN-REPEAT-LIST . RUN-REPEAT-LIST)) DEFTHM-RUN-REGEX-FLAG RUN-REGEX-FLAG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE RUN-REGEX-LIST) (QUOTE (RUN-REGEX-FLAG ((RUN-REGEX . RUN-REGEX) (RUN-REGEX-LIST . RUN-REGEX-LIST) (RUN-REPEAT . RUN-REPEAT) (RUN-REPEAT-LIST . RUN-REPEAT-LIST)) DEFTHM-RUN-REGEX-FLAG RUN-REGEX-FLAG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE RUN-REPEAT) (QUOTE (RUN-REGEX-FLAG ((RUN-REGEX . RUN-REGEX) (RUN-REGEX-LIST . RUN-REGEX-LIST) (RUN-REPEAT . RUN-REPEAT) (RUN-REPEAT-LIST . RUN-REPEAT-LIST)) DEFTHM-RUN-REGEX-FLAG RUN-REGEX-FLAG-EQUIVALENCES))) (TABLE FLAG::FLAG-FNS (QUOTE RUN-REPEAT-LIST) (QUOTE (RUN-REGEX-FLAG ((RUN-REGEX . RUN-REGEX) (RUN-REGEX-LIST . RUN-REGEX-LIST) (RUN-REPEAT . RUN-REPEAT) (RUN-REPEAT-LIST . RUN-REPEAT-LIST)) DEFTHM-RUN-REGEX-FLAG RUN-REGEX-FLAG-EQUIVALENCES)))) (FLAG::ID (IN-THEORY (DISABLE (:DEFINITION RUN-REGEX-FLAG)))))))
(("/usr/share/acl2-6.3/books/regex/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 390361791) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/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/regex/regex-exec.lisp" "regex-exec" "regex-exec" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 791395464) ("/usr/share/acl2-6.3/books/clause-processors/find-subterms.lisp" "clause-processors/find-subterms" "find-subterms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 928774552) ("/usr/share/acl2-6.3/books/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/regex/input-list.lisp" "input-list" "input-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 354450911) ("/usr/share/acl2-6.3/books/cutil/deflist.lisp" "cutil/deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857676809) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "std/osets/under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) ("/usr/share/acl2-6.3/books/cutil/maybe-defthm.lisp" "maybe-defthm" "maybe-defthm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 169275099) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/defsort/duplicated-members.lisp" "defsort/duplicated-members" "duplicated-members" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 720301003) ("/usr/share/acl2-6.3/books/defsort/uniquep.lisp" "uniquep" "uniquep" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1350027706) ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort" "defsort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 284418813) ("/usr/share/acl2-6.3/books/defsort/generic.lisp" "generic" "generic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 992283938) (LOCAL ("/usr/share/acl2-6.3/books/defsort/generic-impl.lisp" "generic-impl" "generic-impl" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 154835353)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-lemmas.lisp" "ihs/ihs-lemmas" "ihs-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1685360399)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-lemmas.lisp" "logops-lemmas" "logops-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 998280003)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/logops-definitions.lisp" "logops-definitions" "logops-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2048680937)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/basic-definitions.lisp" "basic-definitions" "basic-definitions" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1383521171)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/quotient-remainder-lemmas.lisp" "quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 603178913)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2130795727)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1617928370)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1992988803)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/utilities.lisp" "data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1536684829)) (LOCAL ("/usr/share/acl2-6.3/books/data-structures/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1486104990)) (LOCAL ("/usr/share/acl2-6.3/books/ihs/ihs-doc-topic.lisp" "ihs-doc-topic" "ihs-doc-topic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 664631734)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/no-duplicatesp.lisp" "std/lists/no-duplicatesp" "no-duplicatesp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 334869696)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "std/lists/revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "std/lists/duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854) ("/usr/share/acl2-6.3/books/std/osets/top.lisp" "std/osets/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2045504100) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/under-set-equiv.lisp" "under-set-equiv" "under-set-equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1595680367)) ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "std/lists/sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/sort.lisp" "sort" "sort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 335087178)) (LOCAL ("/usr/share/acl2-6.3/books/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/outer.lisp" "outer" "outer" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883866964)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/cardinality.lisp" "cardinality" "cardinality" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 101478632)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/difference.lisp" "difference" "difference" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1211437825)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/intersect.lisp" "intersect" "intersect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 464592124)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/union.lisp" "union" "union" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 895011797)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/delete.lisp" "delete" "delete" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 929878553)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 48714967)) (LOCAL ("/usr/share/acl2-6.3/books/std/osets/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 392002111)) ("/usr/share/acl2-6.3/books/std/osets/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 537896665) ("/usr/share/acl2-6.3/books/std/osets/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1528243117) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/misc/total-order.lisp" "misc/total-order" "total-order" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619824963) (LOCAL ("/usr/share/acl2-6.3/books/misc/total-order-bsd.lisp" "total-order-bsd" "total-order-bsd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 449327279)) ("/usr/share/acl2-6.3/books/str/cat.lisp" "str/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262) ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843) ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482) ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854) ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) ("/usr/share/acl2-6.3/books/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/misc/definline.lisp" "misc/definline" "definline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1571016648) ("/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/regex/regex-defs.lisp" "regex-defs" "regex-defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1054214948) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2140150970)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1221989523)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/nat-listp.lisp" "nat-listp" "nat-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1767896370)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1775556314)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-crg.lisp" "cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761519866)) (LOCAL ("/usr/share/acl2-6.3/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2007324914)) (LOCAL ("/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/defsum.lisp" "tools/defsum" "defsum" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1829289372) ("/usr/share/acl2-6.3/books/tools/types-misc.lisp" "types-misc" "types-misc" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 741554513) ("/usr/share/acl2-6.3/books/tools/theory-tools.lisp" "theory-tools" "theory-tools" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1192579963) ("/usr/share/acl2-6.3/books/tools/pattern-match.lisp" "pattern-match" "pattern-match" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1646398624) ("/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/regex/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 390361791) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/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))
164932189