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

This file is indexed.

/usr/share/acl2-6.3/books/cutil/wizard.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((4 RECORD-EXPANSION (CUTIL::DEFAGGREGATE WIZADVICE (PATTERN RESTRICT MSG ARGS) :TAG :ADVICE-FORM) (WITH-OUTPUT :STACK :PUSH :GAG-MODE T :OFF (SUMMARY OBSERVATION PROVE PROOF-TREE EVENT) (PROGN (SET-INHIBIT-WARNINGS "theory") (CUTIL::DA-EXTEND-AGGINFO-TABLE (QUOTE (:AGGINFO (TAG . :ADVICE-FORM) (CUTIL::NAME . WIZADVICE) (CUTIL::FIELDS PATTERN RESTRICT MSG ARGS) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . PATTERN) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . RESTRICT) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . MSG) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . ARGS) (GUARD . T) (DOC . "") (CUTIL::OPTS)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE-P :PARENTS (UNDOCUMENTED) :SHORT NIL :LONG "<p>@(call ACL2::WIZADVICE-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>pattern</tt></li>
<li><tt>restrict</tt></li>
<li><tt>msg</tt></li>
<li><tt>args</tt></li>
</ul><p>Source link: @(srclink wizadvice)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE-P) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT) (:LONG . "<p>@(call ACL2::WIZADVICE-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>pattern</tt></li>
<li><tt>restrict</tt></li>
<li><tt>msg</tt></li>
<li><tt>args</tt></li>
</ul><p>Source link: @(srclink wizadvice)</p>") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE-P)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE :PARENTS (WIZADVICE-P) :SHORT "Raw constructor for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures." :LONG "<p>Syntax:</p>@(ccall ACL2::WIZADVICE)<p>This is the lowest-level constructor for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p><b>Note:</b> It's generally better to use macros like <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see> or <see topic=\"ACL2____CHANGE-WIZADVICE\">change-wizadvice</see> instead.  These macros
                lead to more readable and robust code, because you don't have
                to remember the order of the fields.</p><p>The <tt>wizadvice-p</tt> structures we create here
                             are just constructed with ordinary @(see acl2::cons).
                             If you want to create @(see acl2::hons)ed structures,
                             see <see topic=\"ACL2____HONSED-WIZADVICE\">honsed-wizadvice</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::WIZADVICE)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Raw constructor for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall ACL2::WIZADVICE)<p>This is the lowest-level constructor for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p><b>Note:</b> It's generally better to use macros like <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see> or <see topic=\"ACL2____CHANGE-WIZADVICE\">change-wizadvice</see> instead.  These macros
                lead to more readable and robust code, because you don't have
                to remember the order of the fields.</p><p>The <tt>wizadvice-p</tt> structures we create here
                             are just constructed with ordinary @(see acl2::cons).
                             If you want to create @(see acl2::hons)ed structures,
                             see <see topic=\"ACL2____HONSED-WIZADVICE\">honsed-wizadvice</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::WIZADVICE)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE)))))) (RECORD-EXPANSION (DEFXDOC HONSED-WIZADVICE :PARENTS (WIZADVICE-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures." :LONG "<p>Syntax:</p> @(ccall ACL2::HONSED-WIZADVICE)<p>This is identical to <see topic=\"ACL2____WIZADVICE\">wizadvice</see>, except that
                            we @(see acl2::hons) the structure we are
                            creating.</p><h3>Definition</h3>

                <p>This is an ordinary honsing constructor introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::HONSED-WIZADVICE)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . HONSED-WIZADVICE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall ACL2::HONSED-WIZADVICE)<p>This is identical to <see topic=\"ACL2____WIZADVICE\">wizadvice</see>, except that
                            we @(see acl2::hons) the structure we are
                            creating.</p><h3>Definition</h3>

                <p>This is an ordinary honsing constructor introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::HONSED-WIZADVICE)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC HONSED-WIZADVICE)))))) (RECORD-EXPANSION (DEFXDOC MAKE-WIZADVICE :PARENTS (WIZADVICE-P) :SHORT "Constructor macro for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-wizadvice [:pattern &lt;pattern&gt;]
                [:restrict &lt;restrict&gt;]
                [:msg &lt;msg&gt;]
                [:args &lt;args&gt;])
</code><p>This is our preferred way to construct <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>wizadvice-p</tt> structure from
                scratch.  See also <see topic=\"ACL2____CHANGE-WIZADVICE\">change-wizadvice</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>wizadvice-p</tt> structures we create here
                             are just constructed with ordinary @(see acl2::cons).
                             If you want to create @(see acl2::hons)ed structures,
                             see <see topic=\"ACL2____MAKE-HONSED-WIZADVICE\">make-honsed-wizadvice</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::MAKE-WIZADVICE)@(def ACL2::MAKE-WIZADVICE-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . MAKE-WIZADVICE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Constructor macro for <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-wizadvice [:pattern &lt;pattern&gt;]
                [:restrict &lt;restrict&gt;]
                [:msg &lt;msg&gt;]
                [:args &lt;args&gt;])
</code><p>This is our preferred way to construct <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>wizadvice-p</tt> structure from
                scratch.  See also <see topic=\"ACL2____CHANGE-WIZADVICE\">change-wizadvice</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>wizadvice-p</tt> structures we create here
                             are just constructed with ordinary @(see acl2::cons).
                             If you want to create @(see acl2::hons)ed structures,
                             see <see topic=\"ACL2____MAKE-HONSED-WIZADVICE\">make-honsed-wizadvice</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::MAKE-WIZADVICE)@(def ACL2::MAKE-WIZADVICE-FN)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC MAKE-WIZADVICE)))))) (RECORD-EXPANSION (DEFXDOC MAKE-HONSED-WIZADVICE :PARENTS (WIZADVICE-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-wizadvice [:pattern &lt;pattern&gt;]
                       [:restrict &lt;restrict&gt;]
                       [:msg &lt;msg&gt;]
                       [:args &lt;args&gt;])
</code><p>This is identical to <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see>, except
                            that we @(see acl2::hons) the structure we are
                            creating.</p><h3>Definition</h3>

                <p>This is an ordinary honsing @('make-') macro introduced by
                @(see cutil::defaggregate).</p>@(def ACL2::MAKE-HONSED-WIZADVICE)@(def ACL2::MAKE-HONSED-WIZADVICE-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . MAKE-HONSED-WIZADVICE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-wizadvice [:pattern &lt;pattern&gt;]
                       [:restrict &lt;restrict&gt;]
                       [:msg &lt;msg&gt;]
                       [:args &lt;args&gt;])
</code><p>This is identical to <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see>, except
                            that we @(see acl2::hons) the structure we are
                            creating.</p><h3>Definition</h3>

                <p>This is an ordinary honsing @('make-') macro introduced by
                @(see cutil::defaggregate).</p>@(def ACL2::MAKE-HONSED-WIZADVICE)@(def ACL2::MAKE-HONSED-WIZADVICE-FN)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC MAKE-HONSED-WIZADVICE)))))) (RECORD-EXPANSION (DEFXDOC CHANGE-WIZADVICE :PARENTS (WIZADVICE-P) :SHORT "A copying macro that lets you create new <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-wizadvice x
                  [:pattern &lt;pattern&gt;]
                  [:restrict &lt;restrict&gt;]
                  [:msg &lt;msg&gt;]
                  [:args &lt;args&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see>.
                It constructs a new <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structure that is a copy of
                @('x'), except that you can explicitly change some particular
                fields.  Any fields you don't mention just keep their values
                from @('x').</p>

                <h3>Definition</h3>

                <p>This is an ordinary @('change-') macro introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::CHANGE-WIZADVICE)@(def ACL2::CHANGE-WIZADVICE-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CHANGE-WIZADVICE) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "A copying macro that lets you create new <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-wizadvice x
                  [:pattern &lt;pattern&gt;]
                  [:restrict &lt;restrict&gt;]
                  [:msg &lt;msg&gt;]
                  [:args &lt;args&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"ACL2____MAKE-WIZADVICE\">make-wizadvice</see>.
                It constructs a new <see topic=\"ACL2____WIZADVICE-P\">wizadvice-p</see> structure that is a copy of
                @('x'), except that you can explicitly change some particular
                fields.  Any fields you don't mention just keep their values
                from @('x').</p>

                <h3>Definition</h3>

                <p>This is an ordinary @('change-') macro introduced by @(see
                cutil::defaggregate).</p>@(def ACL2::CHANGE-WIZADVICE)@(def ACL2::CHANGE-WIZADVICE-FN)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CHANGE-WIZADVICE)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE->PATTERN :PARENTS (WIZADVICE-P) :SHORT "Access the <tt>pattern</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE->PATTERN) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Access the <tt>pattern</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (:LONG) (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE->PATTERN)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE->RESTRICT :PARENTS (WIZADVICE-P) :SHORT "Access the <tt>restrict</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE->RESTRICT) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Access the <tt>restrict</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (:LONG) (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE->RESTRICT)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE->MSG :PARENTS (WIZADVICE-P) :SHORT "Access the <tt>msg</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE->MSG) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Access the <tt>msg</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (:LONG) (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE->MSG)))))) (RECORD-EXPANSION (DEFXDOC WIZADVICE->ARGS :PARENTS (WIZADVICE-P) :SHORT "Access the <tt>args</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . WIZADVICE->ARGS) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS WIZADVICE-P) (:SHORT . "Access the <tt>args</tt> field of a @(see ACL2::WIZADVICE-P) structure.") (:LONG) (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICE->ARGS)))))) (LOGIC) (DEFUND WIZADVICE-P (X) (DECLARE (XARGS :GUARD T :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE ((:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (AND (CONSP X) (EQ (CAR X) :ADVICE-FORM) (ALISTP (CDR X)) (CONSP (CDR X)) (LET ((PATTERN (CDR (ASSOC (QUOTE PATTERN) (CDR X)))) (RESTRICT (CDR (ASSOC (QUOTE RESTRICT) (CDR X)))) (MSG (CDR (ASSOC (QUOTE MSG) (CDR X)))) (ARGS (CDR (ASSOC (QUOTE ARGS) (CDR X))))) (DECLARE (IGNORABLE PATTERN RESTRICT MSG ARGS)) (AND)))) (DEFUND WIZADVICE (PATTERN RESTRICT MSG ARGS) (DECLARE (XARGS :GUARD (AND) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :ADVICE-FORM (CONS (CONS (QUOTE PATTERN) PATTERN) (CONS (CONS (QUOTE RESTRICT) RESTRICT) (CONS (CONS (QUOTE MSG) MSG) (CONS (CONS (QUOTE ARGS) ARGS) NIL)))))) (DEFUN HONSED-WIZADVICE (PATTERN RESTRICT MSG ARGS) (DECLARE (XARGS :GUARD (AND) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (WIZADVICE PATTERN RESTRICT MSG ARGS) :EXEC (HONS :ADVICE-FORM (HONS (HONS (QUOTE PATTERN) PATTERN) (HONS (HONS (QUOTE RESTRICT) RESTRICT) (HONS (HONS (QUOTE MSG) MSG) (HONS (HONS (QUOTE ARGS) ARGS) NIL))))))) (DEFUND-INLINE WIZADVICE->PATTERN (X) (DECLARE (XARGS :GUARD (WIZADVICE-P X) :GUARD-HINTS (("Goal" :EXPAND (WIZADVICE-P X) :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE PATTERN) (CDR X)))) (DEFUND-INLINE WIZADVICE->RESTRICT (X) (DECLARE (XARGS :GUARD (WIZADVICE-P X) :GUARD-HINTS (("Goal" :EXPAND (WIZADVICE-P X) :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE RESTRICT) (CDR X)))) (DEFUND-INLINE WIZADVICE->MSG (X) (DECLARE (XARGS :GUARD (WIZADVICE-P X) :GUARD-HINTS (("Goal" :EXPAND (WIZADVICE-P X) :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE MSG) (CDR X)))) (DEFUND-INLINE WIZADVICE->ARGS (X) (DECLARE (XARGS :GUARD (WIZADVICE-P X) :GUARD-HINTS (("Goal" :EXPAND (WIZADVICE-P X) :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE ARGS) (CDR X)))) (DEFTHM CONSP-OF-WIZADVICE (CONSP (WIZADVICE PATTERN RESTRICT MSG ARGS)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICE)))) (DEFTHM BOOLEANP-OF-WIZADVICE-P (BOOLEANP (WIZADVICE-P X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICE-P)))) (DEFTHM WIZADVICE-P-OF-WIZADVICE (EQUAL (WIZADVICE-P (WIZADVICE PATTERN RESTRICT MSG ARGS)) T) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE BOOLEANP-OF-WIZADVICE-P (X (WIZADVICE PATTERN RESTRICT MSG ARGS))))))) (DEFTHM TAG-OF-WIZADVICE (EQUAL (TAG (WIZADVICE PATTERN RESTRICT MSG ARGS)) :ADVICE-FORM) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM TAG-WHEN-WIZADVICE-P (IMPLIES (WIZADVICE-P X) (EQUAL (TAG X) :ADVICE-FORM)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM WIZADVICE-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG X) :ADVICE-FORM)) (EQUAL (WIZADVICE-P X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (TAG-WHEN-WIZADVICE-P WIZADVICE-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (TAG-WHEN-WIZADVICE-P WIZADVICE-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CONSP-WHEN-WIZADVICE-P (IMPLIES (WIZADVICE-P X) (CONSP X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM WIZADVICE->PATTERN-OF-WIZADVICE (EQUAL (WIZADVICE->PATTERN (WIZADVICE PATTERN RESTRICT MSG ARGS)) PATTERN) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE->PATTERN WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM WIZADVICE->RESTRICT-OF-WIZADVICE (EQUAL (WIZADVICE->RESTRICT (WIZADVICE PATTERN RESTRICT MSG ARGS)) RESTRICT) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE->RESTRICT WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM WIZADVICE->MSG-OF-WIZADVICE (EQUAL (WIZADVICE->MSG (WIZADVICE PATTERN RESTRICT MSG ARGS)) MSG) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE->MSG WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM WIZADVICE->ARGS-OF-WIZADVICE (EQUAL (WIZADVICE->ARGS (WIZADVICE PATTERN RESTRICT MSG ARGS)) ARGS) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (WIZADVICE->ARGS WIZADVICE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO PATBIND-WIZADVICE (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE WIZADVICE) (QUOTE (PATTERN RESTRICT MSG ARGS)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CHANGE-WIZADVICE-FN (X ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE WIZADVICE) (LIST (IF (ASSOC :PATTERN ALIST) (CDR (ASSOC :PATTERN ALIST)) (LIST (QUOTE WIZADVICE->PATTERN) X)) (IF (ASSOC :RESTRICT ALIST) (CDR (ASSOC :RESTRICT ALIST)) (LIST (QUOTE WIZADVICE->RESTRICT) X)) (IF (ASSOC :MSG ALIST) (CDR (ASSOC :MSG ALIST)) (LIST (QUOTE WIZADVICE->MSG) X)) (IF (ASSOC :ARGS ALIST) (CDR (ASSOC :ARGS ALIST)) (LIST (QUOTE WIZADVICE->ARGS) X))))) (DEFMACRO CHANGE-WIZADVICE (X &REST ARGS) (CHANGE-WIZADVICE-FN X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:PATTERN :RESTRICT :MSG :ARGS))))) (DEFUN MAKE-WIZADVICE-FN (ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE WIZADVICE) (LIST (IF (ASSOC :PATTERN ALIST) (CDR (ASSOC :PATTERN ALIST)) (QUOTE NIL)) (IF (ASSOC :RESTRICT ALIST) (CDR (ASSOC :RESTRICT ALIST)) (QUOTE NIL)) (IF (ASSOC :MSG ALIST) (CDR (ASSOC :MSG ALIST)) (QUOTE NIL)) (IF (ASSOC :ARGS ALIST) (CDR (ASSOC :ARGS ALIST)) (QUOTE NIL))))) (DEFMACRO MAKE-WIZADVICE (&REST ARGS) (MAKE-WIZADVICE-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:PATTERN :RESTRICT :MSG :ARGS))))) (DEFUN MAKE-HONSED-WIZADVICE-FN (ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE HONSED-WIZADVICE) (LIST (IF (ASSOC :PATTERN ALIST) (CDR (ASSOC :PATTERN ALIST)) (QUOTE NIL)) (IF (ASSOC :RESTRICT ALIST) (CDR (ASSOC :RESTRICT ALIST)) (QUOTE NIL)) (IF (ASSOC :MSG ALIST) (CDR (ASSOC :MSG ALIST)) (QUOTE NIL)) (IF (ASSOC :ARGS ALIST) (CDR (ASSOC :ARGS ALIST)) (QUOTE NIL))))) (DEFMACRO MAKE-HONSED-WIZADVICE (&REST ARGS) (MAKE-HONSED-WIZADVICE-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:PATTERN :RESTRICT :MSG :ARGS))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE WIZADVICE)))))) (5 RECORD-EXPANSION (CUTIL::DEFLIST WIZADVICELIST-P (X) (WIZADVICE-P X) :GUARD T) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE WIZADVICELIST-P)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (ENCAPSULATE NIL (LOGIC) (SET-INHIBIT-WARNINGS "theory" "free" "non-rec" "double-rewrite") (LOCAL (DEFTHM CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM (OR (EQUAL (WIZADVICE-P X) T) (EQUAL (WIZADVICE-P X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (DEFUND WIZADVICELIST-P (X) (DECLARE (XARGS :GUARD T :NORMALIZE NIL :VERIFY-GUARDS T :GUARD-DEBUG NIL :GUARD-HINTS NIL)) (IF (CONSP X) (AND (WIZADVICE-P (CAR X)) (WIZADVICELIST-P (CDR X))) T)) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS WIZADVICELIST-P (:TYPE-PRESCRIPTION WIZADVICELIST-P) CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM))) (LOCAL (CUTIL::ENABLE-IF-THEOREM CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM)) (DEFTHM WIZADVICELIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP X)) (EQUAL (WIZADVICELIST-P X) T)) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (DEFTHM WIZADVICELIST-P-OF-CONS (EQUAL (WIZADVICELIST-P (CONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (LOCAL (IN-THEORY (ENABLE WIZADVICELIST-P-WHEN-NOT-CONSP WIZADVICELIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE WIZADVICELIST-P))) (DEFTHM WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (IMPLIES (AND (WIZADVICELIST-P X) (MEMBER-EQUAL A X)) (EQUAL (WIZADVICE-P A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL A X) (WIZADVICELIST-P X)) (EQUAL (WIZADVICE-P A) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM WIZADVICELIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (WIZADVICELIST-P Y) (SUBSETP-EQUAL X Y)) (EQUAL (WIZADVICELIST-P X) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL X Y) (WIZADVICELIST-P Y)) (EQUAL (WIZADVICELIST-P X) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE SUBSETP-EQUAL WIZADVICELIST-P) :EXPAND (TRUE-LISTP X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (A (CAR X)) (X Y)))))))) (DEFTHM WIZADVICELIST-P-PRESERVES-SET-EQUIV (IMPLIES (SET-EQUIV X Y) (EQUAL (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :RULE-CLASSES :CONGRUENCE :HINTS (("Goal" :IN-THEORY (ENABLE SET-EQUIV) :CASES ((WIZADVICELIST-P X)) :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-APPEND (EQUAL (WIZADVICELIST-P (APPEND X Y)) (AND (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :HINTS (("Goal" :INDUCT (LEN X) :EXPAND (LIST-FIX X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM WIZADVICE-P-OF-CAR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (CAR X)) (IF (CONSP X) T (WIZADVICE-P NIL)))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((WIZADVICELIST-P X))))) (DEFTHM WIZADVICELIST-P-OF-CDR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (CDR X)) T))) (DEFTHM WIZADVICE-P-OF-NTH-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (NTH N X)) (OR (WIZADVICE-P NIL) (< (NFIX N) (LEN X))))) :HINTS (("Goal" :INDUCT (NTH N X)))) (DEFTHM WIZADVICELIST-P-OF-UPDATE-NTH-WHEN-WIZADVICE-P (IMPLIES (AND (<= (NFIX N) (LEN X)) (WIZADVICELIST-P (DOUBLE-REWRITE X))) (EQUAL (WIZADVICELIST-P (UPDATE-NTH N Y X)) (WIZADVICE-P Y)))) (DEFTHM WIZADVICELIST-P-OF-NTHCDR (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (NTHCDR N X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-TAKE (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (TAKE N X)) (OR (WIZADVICE-P NIL) (<= (NFIX N) (LEN X))))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE N X) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-REPEAT (EQUAL (WIZADVICELIST-P (REPEAT X N)) (OR (WIZADVICE-P X) (ZP N))) :HINTS (("Goal" :INDUCT (REPEAT X N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-LAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (LAST X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-BUTLAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (BUTLAST X N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-RCONS (EQUAL (WIZADVICELIST-P (RCONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM WIZADVICELIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (DUPLICATED-MEMBERS X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SET-DIFFERENCE-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE Y)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SFIX (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SETS::SFIX X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP X)))))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (RECORD-EXPANSION (ENCAPSULATE NIL (LOGIC) (SET-INHIBIT-WARNINGS "theory" "free" "non-rec" "double-rewrite") (LOCAL (DEFTHM CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM (OR (EQUAL (WIZADVICE-P X) T) (EQUAL (WIZADVICE-P X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (DEFUND WIZADVICELIST-P (X) (DECLARE (XARGS :GUARD T :NORMALIZE NIL :VERIFY-GUARDS T :GUARD-DEBUG NIL :GUARD-HINTS NIL)) (IF (CONSP X) (AND (WIZADVICE-P (CAR X)) (WIZADVICELIST-P (CDR X))) T)) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS WIZADVICELIST-P (:TYPE-PRESCRIPTION WIZADVICELIST-P) CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM))) (LOCAL (CUTIL::ENABLE-IF-THEOREM CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM)) (DEFTHM WIZADVICELIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP X)) (EQUAL (WIZADVICELIST-P X) T)) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (DEFTHM WIZADVICELIST-P-OF-CONS (EQUAL (WIZADVICELIST-P (CONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (LOCAL (IN-THEORY (ENABLE WIZADVICELIST-P-WHEN-NOT-CONSP WIZADVICELIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE WIZADVICELIST-P))) (DEFTHM WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (IMPLIES (AND (WIZADVICELIST-P X) (MEMBER-EQUAL A X)) (EQUAL (WIZADVICE-P A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL A X) (WIZADVICELIST-P X)) (EQUAL (WIZADVICE-P A) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM WIZADVICELIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (WIZADVICELIST-P Y) (SUBSETP-EQUAL X Y)) (EQUAL (WIZADVICELIST-P X) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL X Y) (WIZADVICELIST-P Y)) (EQUAL (WIZADVICELIST-P X) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE SUBSETP-EQUAL WIZADVICELIST-P) :EXPAND (TRUE-LISTP X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (A (CAR X)) (X Y)))))))) (DEFTHM WIZADVICELIST-P-PRESERVES-SET-EQUIV (IMPLIES (SET-EQUIV X Y) (EQUAL (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :RULE-CLASSES :CONGRUENCE :HINTS (("Goal" :IN-THEORY (ENABLE SET-EQUIV) :CASES ((WIZADVICELIST-P X)) :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-APPEND (EQUAL (WIZADVICELIST-P (APPEND X Y)) (AND (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :HINTS (("Goal" :INDUCT (LEN X) :EXPAND (LIST-FIX X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM WIZADVICE-P-OF-CAR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (CAR X)) (IF (CONSP X) T (WIZADVICE-P NIL)))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((WIZADVICELIST-P X))))) (DEFTHM WIZADVICELIST-P-OF-CDR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (CDR X)) T))) (DEFTHM WIZADVICE-P-OF-NTH-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (NTH N X)) (OR (WIZADVICE-P NIL) (< (NFIX N) (LEN X))))) :HINTS (("Goal" :INDUCT (NTH N X)))) (DEFTHM WIZADVICELIST-P-OF-UPDATE-NTH-WHEN-WIZADVICE-P (IMPLIES (AND (<= (NFIX N) (LEN X)) (WIZADVICELIST-P (DOUBLE-REWRITE X))) (EQUAL (WIZADVICELIST-P (UPDATE-NTH N Y X)) (WIZADVICE-P Y)))) (DEFTHM WIZADVICELIST-P-OF-NTHCDR (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (NTHCDR N X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-TAKE (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (TAKE N X)) (OR (WIZADVICE-P NIL) (<= (NFIX N) (LEN X))))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE N X) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-REPEAT (EQUAL (WIZADVICELIST-P (REPEAT X N)) (OR (WIZADVICE-P X) (ZP N))) :HINTS (("Goal" :INDUCT (REPEAT X N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-LAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (LAST X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-BUTLAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (BUTLAST X N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-RCONS (EQUAL (WIZADVICELIST-P (RCONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM WIZADVICELIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (DUPLICATED-MEMBERS X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SET-DIFFERENCE-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE Y)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SFIX (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SETS::SFIX X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP X)))))) (ENCAPSULATE NIL (LOGIC) (SET-INHIBIT-WARNINGS "theory" "free" "non-rec" "double-rewrite") (LOCAL (DEFTHM CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM (OR (EQUAL (WIZADVICE-P X) T) (EQUAL (WIZADVICE-P X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (DEFUND WIZADVICELIST-P (X) (DECLARE (XARGS :GUARD T :NORMALIZE NIL :VERIFY-GUARDS T :GUARD-DEBUG NIL :GUARD-HINTS NIL)) (IF (CONSP X) (AND (WIZADVICE-P (CAR X)) (WIZADVICELIST-P (CDR X))) T)) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS WIZADVICELIST-P (:TYPE-PRESCRIPTION WIZADVICELIST-P) CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM))) (RECORD-EXPANSION (LOCAL (CUTIL::ENABLE-IF-THEOREM CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM)) (LOCAL (VALUE-TRIPLE :ELIDED))) (DEFTHM WIZADVICELIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP X)) (EQUAL (WIZADVICELIST-P X) T)) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (DEFTHM WIZADVICELIST-P-OF-CONS (EQUAL (WIZADVICELIST-P (CONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE WIZADVICELIST-P)))) (LOCAL (IN-THEORY (ENABLE WIZADVICELIST-P-WHEN-NOT-CONSP WIZADVICELIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE WIZADVICELIST-P))) (DEFTHM WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (IMPLIES (AND (WIZADVICELIST-P X) (MEMBER-EQUAL A X)) (EQUAL (WIZADVICE-P A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL A X) (WIZADVICELIST-P X)) (EQUAL (WIZADVICE-P A) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM WIZADVICELIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (WIZADVICELIST-P Y) (SUBSETP-EQUAL X Y)) (EQUAL (WIZADVICELIST-P X) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL X Y) (WIZADVICELIST-P Y)) (EQUAL (WIZADVICELIST-P X) T)))) :HINTS (("Goal" :INDUCT (LEN X) :IN-THEORY (ENABLE SUBSETP-EQUAL WIZADVICELIST-P) :EXPAND (TRUE-LISTP X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P (A (CAR X)) (X Y)))))))) (DEFTHM WIZADVICELIST-P-PRESERVES-SET-EQUIV (IMPLIES (SET-EQUIV X Y) (EQUAL (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :RULE-CLASSES :CONGRUENCE :HINTS (("Goal" :IN-THEORY (ENABLE SET-EQUIV) :CASES ((WIZADVICELIST-P X)) :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-APPEND (EQUAL (WIZADVICELIST-P (APPEND X Y)) (AND (WIZADVICELIST-P X) (WIZADVICELIST-P Y))) :HINTS (("Goal" :INDUCT (LEN X) :EXPAND (LIST-FIX X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM WIZADVICE-P-OF-CAR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (CAR X)) (IF (CONSP X) T (WIZADVICE-P NIL)))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((WIZADVICELIST-P X))))) (DEFTHM WIZADVICELIST-P-OF-CDR-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (CDR X)) T))) (DEFTHM WIZADVICE-P-OF-NTH-WHEN-WIZADVICELIST-P (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICE-P (NTH N X)) (OR (WIZADVICE-P NIL) (< (NFIX N) (LEN X))))) :HINTS (("Goal" :INDUCT (NTH N X)))) (DEFTHM WIZADVICELIST-P-OF-UPDATE-NTH-WHEN-WIZADVICE-P (IMPLIES (AND (<= (NFIX N) (LEN X)) (WIZADVICELIST-P (DOUBLE-REWRITE X))) (EQUAL (WIZADVICELIST-P (UPDATE-NTH N Y X)) (WIZADVICE-P Y)))) (DEFTHM WIZADVICELIST-P-OF-NTHCDR (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (NTHCDR N X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-TAKE (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (TAKE N X)) (OR (WIZADVICE-P NIL) (<= (NFIX N) (LEN X))))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE N X) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-REPEAT (EQUAL (WIZADVICELIST-P (REPEAT X N)) (OR (WIZADVICE-P X) (ZP N))) :HINTS (("Goal" :INDUCT (REPEAT X N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((WIZADVICELIST-P X) (:FREE (X Y) (WIZADVICELIST-P (CONS X Y))))))) (DEFTHM WIZADVICELIST-P-OF-LAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (LAST X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-BUTLAST (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (BUTLAST X N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-RCONS (EQUAL (WIZADVICELIST-P (RCONS A X)) (AND (WIZADVICE-P A) (WIZADVICELIST-P X))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM WIZADVICELIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (DUPLICATED-MEMBERS X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SET-DIFFERENCE-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE Y)) (EQUAL (WIZADVICELIST-P (INTERSECTION-EQUAL X Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM WIZADVICELIST-P-OF-SFIX (IMPLIES (WIZADVICELIST-P (DOUBLE-REWRITE X)) (EQUAL (WIZADVICELIST-P (SETS::SFIX X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP X)))))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE WIZADVICELIST-P)) (XDOC::PARENTS (QUOTE (UNDOCUMENTED))) (XDOC::SHORT (QUOTE "@(call WIZADVICELIST-P) recognizes lists where every element satisfies @(see WIZADVICE-P).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE WIZADVICELIST-P))) 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>This is an ordinary @(see cutil::deflist).  It is
\"loose\" in that it does not care whether @('x') is nil-terminated.</p>") (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 . WIZADVICELIST-P) (:BASE-PKG . ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT . "@(call WIZADVICELIST-P) recognizes lists where every element satisfies @(see WIZADVICE-P).") (:LONG . "<p>This is an ordinary @(see cutil::deflist).  It is
\"loose\" in that it does not care whether @('x') is nil-terminated.</p>

<h3>Definitions and Theorems</h3>@(def |ACL2|::|WIZADVICELIST-P|)
@(def |ACL2|::|WIZADVICELIST-P-WHEN-NOT-CONSP|)
@(def |ACL2|::|WIZADVICELIST-P-OF-CONS|)
@(def |ACL2|::|WIZADVICE-P-WHEN-MEMBER-EQUAL-OF-WIZADVICELIST-P|)
@(def |ACL2|::|WIZADVICELIST-P-WHEN-SUBSETP-EQUAL|)
@(def |ACL2|::|WIZADVICELIST-P-PRESERVES-SET-EQUIV|)
@(def |ACL2|::|WIZADVICELIST-P-OF-APPEND|)
@(def |ACL2|::|WIZADVICE-P-OF-CAR-WHEN-WIZADVICELIST-P|)
@(def |ACL2|::|WIZADVICELIST-P-OF-CDR-WHEN-WIZADVICELIST-P|)
@(def |ACL2|::|WIZADVICE-P-OF-NTH-WHEN-WIZADVICELIST-P|)
@(def |ACL2|::|WIZADVICELIST-P-OF-UPDATE-NTH-WHEN-WIZADVICE-P|)
@(def |ACL2|::|WIZADVICELIST-P-OF-NTHCDR|)
@(def |ACL2|::|WIZADVICELIST-P-OF-TAKE|)
@(def |ACL2|::|WIZADVICELIST-P-OF-REPEAT|)
@(def |ACL2|::|WIZADVICELIST-P-OF-LAST|)
@(def |ACL2|::|WIZADVICELIST-P-OF-BUTLAST|)
@(def |ACL2|::|WIZADVICELIST-P-OF-RCONS|)
@(def |ACL2|::|WIZADVICELIST-P-OF-DUPLICATED-MEMBERS|)
@(def |ACL2|::|WIZADVICELIST-P-OF-SET-DIFFERENCE-EQUAL|)
@(def |ACL2|::|WIZADVICELIST-P-OF-INTERSECTION-EQUAL-1|)
@(def |ACL2|::|WIZADVICELIST-P-OF-INTERSECTION-EQUAL-2|)
@(def |ACL2|::|WIZADVICELIST-P-OF-SFIX|)") (:FROM . "[books]/cutil/wizard.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC WIZADVICELIST-P)))))) (VALUE-TRIPLE (QUOTE WIZADVICELIST-P))))))
(("/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/wizard.lisp" "wizard" "wizard" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1145161384) ("/usr/share/acl2-6.3/books/clause-processors/unify-subst.lisp" "clause-processors/unify-subst" "unify-subst" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 152550313) ("/usr/share/acl2-6.3/books/clause-processors/ev-find-rules.lisp" "ev-find-rules" "ev-find-rules" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 413299260) ("/usr/share/acl2-6.3/books/tools/def-functional-instance.lisp" "tools/def-functional-instance" "def-functional-instance" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 156665620) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/flag.lisp" "tools/flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/cutil/deflist.lisp" "deflist" "deflist" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857676809) ("/usr/share/acl2-6.3/books/cutil/defaggregate.lisp" "defaggregate" "defaggregate" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2084462154) ("/usr/share/acl2-6.3/books/xdoc/names.lisp" "xdoc/names" "names" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 323283374) ("/usr/share/acl2-6.3/books/str/defs.lisp" "str/defs" "defs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1131369726) (LOCAL ("/usr/share/acl2-6.3/books/cutil/defredundant.lisp" "cutil/defredundant" "defredundant" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1198380940)) (LOCAL ("/usr/share/acl2-6.3/books/str/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1717362461)) (LOCAL ("/usr/share/acl2-6.3/books/str/symbols.lisp" "symbols" "symbols" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 811693364)) (LOCAL ("/usr/share/acl2-6.3/books/str/suffixp.lisp" "suffixp" "suffixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1217176423)) (LOCAL ("/usr/share/acl2-6.3/books/str/substrp.lisp" "substrp" "substrp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 139343620)) (LOCAL ("/usr/share/acl2-6.3/books/str/strval.lisp" "strval" "strval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1981642498)) (LOCAL ("/usr/share/acl2-6.3/books/str/strtok.lisp" "strtok" "strtok" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1082657979)) (LOCAL ("/usr/share/acl2-6.3/books/str/strsubst.lisp" "strsubst" "strsubst" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1100185597)) (LOCAL ("/usr/share/acl2-6.3/books/str/strsplit.lisp" "strsplit" "strsplit" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1851472056)) (LOCAL ("/usr/share/acl2-6.3/books/str/strnatless.lisp" "strnatless" "strnatless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797808730)) (LOCAL ("/usr/share/acl2-6.3/books/str/strrpos.lisp" "strrpos" "strrpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1502347794)) (LOCAL ("/usr/share/acl2-6.3/books/str/strpos.lisp" "strpos" "strpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 35435295)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "std/lists/sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/str/strprefixp.lisp" "strprefixp" "strprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2141614236)) (LOCAL ("/usr/share/acl2-6.3/books/str/prefix-lines.lisp" "prefix-lines" "prefix-lines" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 747083898)) (LOCAL ("/usr/share/acl2-6.3/books/str/pad.lisp" "pad" "pad" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 724548430)) (LOCAL ("/usr/share/acl2-6.3/books/str/strline.lisp" "strline" "strline" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 771995942)) (LOCAL ("/usr/share/acl2-6.3/books/str/natstr.lisp" "natstr" "natstr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1696407817)) (LOCAL ("/usr/share/acl2-6.3/books/str/isubstrp.lisp" "isubstrp" "isubstrp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 536022649)) (LOCAL ("/usr/share/acl2-6.3/books/str/istrpos.lisp" "istrpos" "istrpos" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 683068330)) (LOCAL ("/usr/share/acl2-6.3/books/str/istrprefixp.lisp" "istrprefixp" "istrprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1923285590)) (LOCAL ("/usr/share/acl2-6.3/books/str/isort.lisp" "isort" "isort" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053063794)) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/string-listp.lisp" "std/typed-lists/string-listp" "string-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 988699164)) ("/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) ("/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/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)) ("/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) (LOCAL ("/usr/share/acl2-6.3/books/std/typed-lists/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 285905462)) ("/usr/share/acl2-6.3/books/defsort/defsort.lisp" "defsort/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) (LOCAL ("/usr/share/acl2-6.3/books/str/iless.lisp" "iless" "iless" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 267906057)) (LOCAL ("/usr/share/acl2-6.3/books/str/iprefixp.lisp" "iprefixp" "iprefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1865764102)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "std/lists/prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/str/html-encode.lisp" "html-encode" "html-encode" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1014597130)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 14631641)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 248299501)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 915259697)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 732116275)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105657945)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 864029516)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 750113408)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1374753694)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 122664565)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2013733040)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061645425)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1619080936)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 972646001)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 384804126)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1113724693)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 483566967)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 457663279)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 513558315)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134470975)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/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-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2126151702)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1504975778)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 653127144)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1661395704)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1273493319)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 508744284)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1246647817)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376534638)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1061889192)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1153949377)) (LOCAL ("/usr/share/acl2-6.3/books/str/firstn-chars.lisp" "firstn-chars" "firstn-chars" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2075748192)) (LOCAL ("/usr/share/acl2-6.3/books/str/digitp.lisp" "digitp" "digitp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 479290421)) (LOCAL ("/usr/share/acl2-6.3/books/str/case-conversion.lisp" "case-conversion" "case-conversion" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 646818128)) (LOCAL ("/usr/share/acl2-6.3/books/str/subseq.lisp" "subseq" "subseq" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1507065012)) ("/usr/share/acl2-6.3/books/str/cat.lisp" "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/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" "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) ("/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/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/str/char-fix.lisp" "char-fix" "char-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 70055851) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "cutil/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/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)) ("/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)) (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/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/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)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/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)) ("/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/xdoc/fmt-to-str.lisp" "xdoc/fmt-to-str" "fmt-to-str" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 717243077) ("/usr/share/acl2-6.3/books/centaur/bridge/portcullis.lisp" "centaur/bridge/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661758845) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "oslib/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/usr/share/acl2-6.3/books/cutil/formals.lisp" "formals" "formals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 606017704) ("/usr/share/acl2-6.3/books/cutil/look-up.lisp" "look-up" "look-up" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1505505915) ("/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/da-base.lisp" "da-base" "da-base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 517345789) ("/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))
1860125608

APT Browse - Built by Thomas Orozco.