acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / str / symbols.cert

This file is indexed.

/usr/share/acl2-6.3/books/str/symbols.cert is in acl2-books-certs 6.3-5.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "cutil/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (DEFSECTION STR::SYMBOL-LIST-NAMES :PARENTS (STR::SYMBOLS SYMBOL-NAME SYMBOL-LISTP) :SHORT "Extract the name of every symbol in a list." :LONG "<p>@(call symbol-list-names) just maps @(see symbol-name) across the
list @('x'), returning a new list that has the names of all the symbols in
@('x').</p>

<p>Example:</p>
@({
    (symbol-list-names '(:foo acl2::bar str::baz))
      -->
    (\"foo\" \"bar\" \"baz\")
})" (DEFUND STR::SYMBOL-LIST-NAMES (X) (DECLARE (XARGS :GUARD (SYMBOL-LISTP X))) (IF (ATOM X) NIL (CONS (SYMBOL-NAME (CAR X)) (STR::SYMBOL-LIST-NAMES (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::SYMBOL-LIST-NAMES))) (DEFTHM STR::SYMBOL-LIST-NAMES-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::SYMBOL-LIST-NAMES X) NIL))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-CONS (EQUAL (STR::SYMBOL-LIST-NAMES (CONS A X)) (CONS (SYMBOL-NAME A) (STR::SYMBOL-LIST-NAMES X)))) (DEFTHM STR::STRING-LISTP-OF-SYMBOL-LIST-NAMES (STRING-LISTP (STR::SYMBOL-LIST-NAMES X))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::SYMBOL-LIST-NAMES (LIST-FIX X)) (STR::SYMBOL-LIST-NAMES X)))) (DEFCONG LIST-EQUIV EQUAL (STR::SYMBOL-LIST-NAMES X) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-APPEND (EQUAL (STR::SYMBOL-LIST-NAMES (APPEND X Y)) (APPEND (STR::SYMBOL-LIST-NAMES X) (STR::SYMBOL-LIST-NAMES Y)))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-REVAPPEND (EQUAL (STR::SYMBOL-LIST-NAMES (REVAPPEND X Y)) (REVAPPEND (STR::SYMBOL-LIST-NAMES X) (STR::SYMBOL-LIST-NAMES Y)))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-REV (EQUAL (STR::SYMBOL-LIST-NAMES (REV X)) (REV (STR::SYMBOL-LIST-NAMES X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::SYMBOL-LIST-NAMES)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::SYMBOL-LIST-NAMES (X) (DECLARE (XARGS :GUARD (SYMBOL-LISTP X))) (IF (ATOM X) NIL (CONS (SYMBOL-NAME (CAR X)) (STR::SYMBOL-LIST-NAMES (CDR X))))) (LOCAL (IN-THEORY (ENABLE STR::SYMBOL-LIST-NAMES))) (DEFTHM STR::SYMBOL-LIST-NAMES-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::SYMBOL-LIST-NAMES X) NIL))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-CONS (EQUAL (STR::SYMBOL-LIST-NAMES (CONS A X)) (CONS (SYMBOL-NAME A) (STR::SYMBOL-LIST-NAMES X)))) (DEFTHM STR::STRING-LISTP-OF-SYMBOL-LIST-NAMES (STRING-LISTP (STR::SYMBOL-LIST-NAMES X))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::SYMBOL-LIST-NAMES (LIST-FIX X)) (STR::SYMBOL-LIST-NAMES X)))) (DEFCONG LIST-EQUIV EQUAL (STR::SYMBOL-LIST-NAMES X) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-APPEND (EQUAL (STR::SYMBOL-LIST-NAMES (APPEND X Y)) (APPEND (STR::SYMBOL-LIST-NAMES X) (STR::SYMBOL-LIST-NAMES Y)))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-REVAPPEND (EQUAL (STR::SYMBOL-LIST-NAMES (REVAPPEND X Y)) (REVAPPEND (STR::SYMBOL-LIST-NAMES X) (STR::SYMBOL-LIST-NAMES Y)))) (DEFTHM STR::SYMBOL-LIST-NAMES-OF-REV (EQUAL (STR::SYMBOL-LIST-NAMES (REV X)) (REV (STR::SYMBOL-LIST-NAMES X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::SYMBOL-LIST-NAMES)) (XDOC::PARENTS (QUOTE (STR::SYMBOLS SYMBOL-NAME SYMBOL-LISTP))) (XDOC::SHORT (QUOTE "Extract the name of every symbol in a list.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::SYMBOL-LIST-NAMES))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>@(call symbol-list-names) just maps @(see symbol-name) across the
list @('x'), returning a new list that has the names of all the symbols in
@('x').</p>

<p>Example:</p>
@({
    (symbol-list-names '(:foo acl2::bar str::baz))
      -->
    (\"foo\" \"bar\" \"baz\")
})") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::SYMBOL-LIST-NAMES) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SYMBOLS SYMBOL-NAME SYMBOL-LISTP) (:SHORT . "Extract the name of every symbol in a list.") (:LONG . "<p>@(call symbol-list-names) just maps @(see symbol-name) across the
list @('x'), returning a new list that has the names of all the symbols in
@('x').</p>

<p>Example:</p>
@({
    (symbol-list-names '(:foo acl2::bar str::baz))
      -->
    (\"foo\" \"bar\" \"baz\")
})

<h3>Definitions and Theorems</h3>@(def |STR|::|SYMBOL-LIST-NAMES|)
@(def |STR|::|SYMBOL-LIST-NAMES-WHEN-ATOM|)
@(def |STR|::|SYMBOL-LIST-NAMES-OF-CONS|)
@(def |STR|::|STRING-LISTP-OF-SYMBOL-LIST-NAMES|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-EQUAL-SYMBOL-LIST-NAMES-1|)
@(def |STR|::|SYMBOL-LIST-NAMES-OF-APPEND|)
@(def |STR|::|SYMBOL-LIST-NAMES-OF-REVAPPEND|)
@(def |STR|::|SYMBOL-LIST-NAMES-OF-REV|)") (:FROM . "[books]/str/symbols.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::SYMBOL-LIST-NAMES)))))) (VALUE-TRIPLE (QUOTE STR::SYMBOL-LIST-NAMES))))) (7 RECORD-EXPANSION (DEFSECTION STR::INTERN-LIST :PARENTS (STR::SYMBOLS INTERN-IN-PACKAGE-OF-SYMBOL INTERN$ SYMBOL-LISTP) :SHORT "Generate a list of symbols in some package." :LONG "<p>Examples:</p>

@({
 (intern-list '(\"FOO\" \"BAR\"))           --> (acl2::foo acl2::bar)
 (intern-list '(\"FOO\" \"BAR\") 'str::foo) --> (str::foo str::bar)
})

<p>@(call intern-list) is a macro that takes</p>

<ul>

<li>@('names'), a list of strings that will become the @(see symbol-name)s of
the new symbols, and optionally</li>

<li>@('pkg'), a symbol that is used as a package indicator, as in @(see
intern-in-package-of-symbol).</li>

</ul>" (DEFUND STR::INTERN-LIST-FN (X STR::PKG) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (SYMBOLP STR::PKG)))) (IF (ATOM X) NIL (CONS (INTERN-IN-PACKAGE-OF-SYMBOL (CAR X) STR::PKG) (STR::INTERN-LIST-FN (CDR X) STR::PKG)))) (DEFMACRO STR::INTERN-LIST (X &OPTIONAL (STR::PKG (QUOTE (QUOTE ACL2-PKG-WITNESS)))) (CONS (QUOTE STR::INTERN-LIST-FN) (CONS X (CONS STR::PKG (QUOTE NIL))))) (LOCAL (DEFTHM STR::INTERN-LIST-EXAMPLES (AND (EQUAL (STR::INTERN-LIST (QUOTE ("FOO" "BAR" "BAZ"))) (QUOTE (FOO BAR BAZ))) (EQUAL (STR::INTERN-LIST (QUOTE ("FOO" "BAR" "BAZ")) (QUOTE STR::FOO)) (QUOTE (STR::FOO STR::BAR STR::BAZ)))))) (ADD-MACRO-ALIAS STR::INTERN-LIST STR::INTERN-LIST-FN) (LOCAL (IN-THEORY (ENABLE STR::INTERN-LIST))) (DEFTHM STR::INTERN-LIST-FN-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::INTERN-LIST-FN X STR::PKG) NIL))) (DEFTHM STR::INTERN-LIST-FN-OF-CONS (EQUAL (STR::INTERN-LIST-FN (CONS A X) STR::PKG) (CONS (INTERN-IN-PACKAGE-OF-SYMBOL A STR::PKG) (STR::INTERN-LIST-FN X STR::PKG)))) (DEFTHM STR::SYMBOL-LISTP-OF-INTERN-LIST-FN (SYMBOL-LISTP (STR::INTERN-LIST-FN X STR::PKG))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::INTERN-LIST-FN (LIST-FIX X) STR::PKG) (STR::INTERN-LIST-FN X STR::PKG)))) (DEFCONG LIST-EQUIV EQUAL (STR::INTERN-LIST-FN X STR::PKG) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::INTERN-LIST-FN-OF-APPEND (EQUAL (STR::INTERN-LIST-FN (APPEND X Y) STR::PKG) (APPEND (STR::INTERN-LIST-FN X STR::PKG) (STR::INTERN-LIST-FN Y STR::PKG)))) (DEFTHM STR::INTERN-LIST-FN-OF-REVAPPEND (EQUAL (STR::INTERN-LIST-FN (REVAPPEND X Y) STR::PKG) (REVAPPEND (STR::INTERN-LIST-FN X STR::PKG) (STR::INTERN-LIST-FN Y STR::PKG)))) (DEFTHM STR::INTERN-LIST-FN-OF-REV (EQUAL (STR::INTERN-LIST-FN (REV X) STR::PKG) (REV (STR::INTERN-LIST-FN X STR::PKG))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE STR::INTERN-LIST)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND STR::INTERN-LIST-FN (X STR::PKG) (DECLARE (XARGS :GUARD (AND (STRING-LISTP X) (SYMBOLP STR::PKG)))) (IF (ATOM X) NIL (CONS (INTERN-IN-PACKAGE-OF-SYMBOL (CAR X) STR::PKG) (STR::INTERN-LIST-FN (CDR X) STR::PKG)))) (DEFMACRO STR::INTERN-LIST (X &OPTIONAL (STR::PKG (QUOTE (QUOTE ACL2-PKG-WITNESS)))) (CONS (QUOTE STR::INTERN-LIST-FN) (CONS X (CONS STR::PKG (QUOTE NIL))))) (LOCAL (DEFTHM STR::INTERN-LIST-EXAMPLES (AND (EQUAL (STR::INTERN-LIST (QUOTE ("FOO" "BAR" "BAZ"))) (QUOTE (FOO BAR BAZ))) (EQUAL (STR::INTERN-LIST (QUOTE ("FOO" "BAR" "BAZ")) (QUOTE STR::FOO)) (QUOTE (STR::FOO STR::BAR STR::BAZ)))))) (ADD-MACRO-ALIAS STR::INTERN-LIST STR::INTERN-LIST-FN) (LOCAL (IN-THEORY (ENABLE STR::INTERN-LIST))) (DEFTHM STR::INTERN-LIST-FN-WHEN-ATOM (IMPLIES (ATOM X) (EQUAL (STR::INTERN-LIST-FN X STR::PKG) NIL))) (DEFTHM STR::INTERN-LIST-FN-OF-CONS (EQUAL (STR::INTERN-LIST-FN (CONS A X) STR::PKG) (CONS (INTERN-IN-PACKAGE-OF-SYMBOL A STR::PKG) (STR::INTERN-LIST-FN X STR::PKG)))) (DEFTHM STR::SYMBOL-LISTP-OF-INTERN-LIST-FN (SYMBOL-LISTP (STR::INTERN-LIST-FN X STR::PKG))) (LOCAL (DEFTHM STR::L0 (EQUAL (STR::INTERN-LIST-FN (LIST-FIX X) STR::PKG) (STR::INTERN-LIST-FN X STR::PKG)))) (DEFCONG LIST-EQUIV EQUAL (STR::INTERN-LIST-FN X STR::PKG) 1 :HINTS (("Goal" :IN-THEORY (DISABLE STR::L0) :USE ((:INSTANCE STR::L0 (X X)) (:INSTANCE STR::L0 (X X-EQUIV)))))) (DEFTHM STR::INTERN-LIST-FN-OF-APPEND (EQUAL (STR::INTERN-LIST-FN (APPEND X Y) STR::PKG) (APPEND (STR::INTERN-LIST-FN X STR::PKG) (STR::INTERN-LIST-FN Y STR::PKG)))) (DEFTHM STR::INTERN-LIST-FN-OF-REVAPPEND (EQUAL (STR::INTERN-LIST-FN (REVAPPEND X Y) STR::PKG) (REVAPPEND (STR::INTERN-LIST-FN X STR::PKG) (STR::INTERN-LIST-FN Y STR::PKG)))) (DEFTHM STR::INTERN-LIST-FN-OF-REV (EQUAL (STR::INTERN-LIST-FN (REV X) STR::PKG) (REV (STR::INTERN-LIST-FN X STR::PKG)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE STR::INTERN-LIST)) (XDOC::PARENTS (QUOTE (STR::SYMBOLS INTERN-IN-PACKAGE-OF-SYMBOL INTERN$ SYMBOL-LISTP))) (XDOC::SHORT (QUOTE "Generate a list of symbols in some package.")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE STR::INTERN-LIST))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Examples:</p>

@({
 (intern-list '(\"FOO\" \"BAR\"))           --> (acl2::foo acl2::bar)
 (intern-list '(\"FOO\" \"BAR\") 'str::foo) --> (str::foo str::bar)
})

<p>@(call intern-list) is a macro that takes</p>

<ul>

<li>@('names'), a list of strings that will become the @(see symbol-name)s of
the new symbols, and optionally</li>

<li>@('pkg'), a symbol that is used as a package indicator, as in @(see
intern-in-package-of-symbol).</li>

</ul>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . STR::INTERN-LIST) (:BASE-PKG . STR::ACL2-PKG-WITNESS) (:PARENTS STR::SYMBOLS INTERN-IN-PACKAGE-OF-SYMBOL INTERN$ SYMBOL-LISTP) (:SHORT . "Generate a list of symbols in some package.") (:LONG . "<p>Examples:</p>

@({
 (intern-list '(\"FOO\" \"BAR\"))           --> (acl2::foo acl2::bar)
 (intern-list '(\"FOO\" \"BAR\") 'str::foo) --> (str::foo str::bar)
})

<p>@(call intern-list) is a macro that takes</p>

<ul>

<li>@('names'), a list of strings that will become the @(see symbol-name)s of
the new symbols, and optionally</li>

<li>@('pkg'), a symbol that is used as a package indicator, as in @(see
intern-in-package-of-symbol).</li>

</ul>

<h3>Definitions and Theorems</h3>@(def |STR|::|INTERN-LIST-FN|)
@(def |STR|::|INTERN-LIST-FN-WHEN-ATOM|)
@(def |STR|::|INTERN-LIST-FN-OF-CONS|)
@(def |STR|::|SYMBOL-LISTP-OF-INTERN-LIST-FN|)
@(def |ACL2|::|LIST-EQUIV-IMPLIES-EQUAL-INTERN-LIST-FN-1|)
@(def |STR|::|INTERN-LIST-FN-OF-APPEND|)
@(def |STR|::|INTERN-LIST-FN-OF-REVAPPEND|)
@(def |STR|::|INTERN-LIST-FN-OF-REV|)") (:FROM . "[books]/str/symbols.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC STR::INTERN-LIST)))))) (VALUE-TRIPLE (QUOTE STR::INTERN-LIST))))))
(("/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/str/symbols.lisp" "symbols" "symbols" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 811693364) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/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/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556)) ("/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/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/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/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)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) (LOCAL ("/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/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) (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/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)) (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/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/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/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" "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))
1214402837

APT Browse - Built by Thomas Orozco.