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

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (ENCAPSULATE NIL (DEFUN CUTIL::FOOF-P (CUTIL::X) (DECLARE (XARGS :GUARD T)) (KEYWORDP CUTIL::X)) (DEFMACRO CUTIL::FOOM-P (CUTIL::X) (CONS (QUOTE KEYWORDP) (CONS CUTIL::X (QUOTE NIL)))) (CUTIL::DEFAGGREGATE CUTIL::CONTAINERF (CUTIL::THING) :REQUIRE ((CUTIL::FOOF-P-OF-CONTAINERF->THING (CUTIL::FOOF-P CUTIL::THING))) :TAG :CONTAINERF) (CUTIL::DEFAGGREGATE CUTIL::CONTAINERM (CUTIL::THING) :REQUIRE ((CUTIL::FOOM-P-OF-CONTAINERM->THING (CUTIL::FOOM-P CUTIL::THING))) :TAG :CONTAINERM)) (ENCAPSULATE NIL (DEFUN CUTIL::FOOF-P (CUTIL::X) (DECLARE (XARGS :GUARD T)) (KEYWORDP CUTIL::X)) (DEFMACRO CUTIL::FOOM-P (CUTIL::X) (CONS (QUOTE KEYWORDP) (CONS CUTIL::X (QUOTE NIL)))) (RECORD-EXPANSION (CUTIL::DEFAGGREGATE CUTIL::CONTAINERF (CUTIL::THING) :REQUIRE ((CUTIL::FOOF-P-OF-CONTAINERF->THING (CUTIL::FOOF-P CUTIL::THING))) :TAG :CONTAINERF) (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 . :CONTAINERF) (CUTIL::NAME . CUTIL::CONTAINERF) (CUTIL::FIELDS CUTIL::THING) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . CUTIL::THING) (GUARD . T) (DOC . "") (CUTIL::OPTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERF-P :PARENTS (UNDOCUMENTED) :SHORT NIL :LONG "<p>@(call CUTIL::CONTAINERF-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>thing</tt></li>
</ul><p>Source link: @(srclink containerf)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERF-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT) (:LONG . "<p>@(call CUTIL::CONTAINERF-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>thing</tt></li>
</ul><p>Source link: @(srclink containerf)</p>") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERF-P)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERF :PARENTS (CUTIL::CONTAINERF-P) :SHORT "Raw constructor for <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures." :LONG "<p>Syntax:</p>@(ccall CUTIL::CONTAINERF)<p>This is the lowest-level constructor for <see topic=\"CUTIL____CONTAINERF-P\">containerf-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=\"CUTIL____MAKE-CONTAINERF\">make-containerf</see> or <see topic=\"CUTIL____CHANGE-CONTAINERF\">change-containerf</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>containerf-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=\"CUTIL____HONSED-CONTAINERF\">honsed-containerf</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::CONTAINERF)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERF) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERF-P) (:SHORT . "Raw constructor for <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall CUTIL::CONTAINERF)<p>This is the lowest-level constructor for <see topic=\"CUTIL____CONTAINERF-P\">containerf-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=\"CUTIL____MAKE-CONTAINERF\">make-containerf</see> or <see topic=\"CUTIL____CHANGE-CONTAINERF\">change-containerf</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>containerf-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=\"CUTIL____HONSED-CONTAINERF\">honsed-containerf</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::CONTAINERF)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERF)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::HONSED-CONTAINERF :PARENTS (CUTIL::CONTAINERF-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures." :LONG "<p>Syntax:</p> @(ccall CUTIL::HONSED-CONTAINERF)<p>This is identical to <see topic=\"CUTIL____CONTAINERF\">containerf</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 CUTIL::HONSED-CONTAINERF)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::HONSED-CONTAINERF) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERF-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall CUTIL::HONSED-CONTAINERF)<p>This is identical to <see topic=\"CUTIL____CONTAINERF\">containerf</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 CUTIL::HONSED-CONTAINERF)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::HONSED-CONTAINERF)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-CONTAINERF :PARENTS (CUTIL::CONTAINERF-P) :SHORT "Constructor macro for <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-containerf [:thing &lt;thing&gt;])
</code><p>This is our preferred way to construct <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>containerf-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-CONTAINERF\">change-containerf</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>containerf-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=\"CUTIL____MAKE-HONSED-CONTAINERF\">make-honsed-containerf</see> instead.</p><h3>Definition</h3>

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

                <p>This macro generates a new <tt>containerf-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-CONTAINERF\">change-containerf</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>containerf-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=\"CUTIL____MAKE-HONSED-CONTAINERF\">make-honsed-containerf</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::MAKE-CONTAINERF)@(def CUTIL::MAKE-CONTAINERF-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-CONTAINERF)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-HONSED-CONTAINERF :PARENTS (CUTIL::CONTAINERF-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-containerf [:thing &lt;thing&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-CONTAINERF\">make-containerf</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 CUTIL::MAKE-HONSED-CONTAINERF)@(def CUTIL::MAKE-HONSED-CONTAINERF-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::MAKE-HONSED-CONTAINERF) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERF-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-containerf [:thing &lt;thing&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-CONTAINERF\">make-containerf</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 CUTIL::MAKE-HONSED-CONTAINERF)@(def CUTIL::MAKE-HONSED-CONTAINERF-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-HONSED-CONTAINERF)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CHANGE-CONTAINERF :PARENTS (CUTIL::CONTAINERF-P) :SHORT "A copying macro that lets you create new <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-containerf x
                   [:thing &lt;thing&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-CONTAINERF\">make-containerf</see>.
                It constructs a new <see topic=\"CUTIL____CONTAINERF-P\">containerf-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 CUTIL::CHANGE-CONTAINERF)@(def CUTIL::CHANGE-CONTAINERF-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CHANGE-CONTAINERF) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERF-P) (:SHORT . "A copying macro that lets you create new <see topic=\"CUTIL____CONTAINERF-P\">containerf-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-containerf x
                   [:thing &lt;thing&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-CONTAINERF\">make-containerf</see>.
                It constructs a new <see topic=\"CUTIL____CONTAINERF-P\">containerf-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 CUTIL::CHANGE-CONTAINERF)@(def CUTIL::CHANGE-CONTAINERF-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CHANGE-CONTAINERF)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERF->THING :PARENTS (CUTIL::CONTAINERF-P) :SHORT "Access the <tt>thing</tt> field of a @(see CUTIL::CONTAINERF-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERF->THING) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERF-P) (:SHORT . "Access the <tt>thing</tt> field of a @(see CUTIL::CONTAINERF-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERF->THING)))))) (LOGIC) (DEFUND CUTIL::CONTAINERF-P (CUTIL::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 CUTIL::X) (EQ (CAR CUTIL::X) :CONTAINERF) (ALISTP (CDR CUTIL::X)) (CONSP (CDR CUTIL::X)) (LET ((CUTIL::THING (CDR (ASSOC (QUOTE CUTIL::THING) (CDR CUTIL::X))))) (DECLARE (IGNORABLE CUTIL::THING)) (AND (CUTIL::FOOF-P CUTIL::THING))))) (DEFUND CUTIL::CONTAINERF (CUTIL::THING) (DECLARE (XARGS :GUARD (AND (CUTIL::FOOF-P CUTIL::THING)) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :CONTAINERF (CONS (CONS (QUOTE CUTIL::THING) CUTIL::THING) NIL))) (DEFUN CUTIL::HONSED-CONTAINERF (CUTIL::THING) (DECLARE (XARGS :GUARD (AND (CUTIL::FOOF-P CUTIL::THING)) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (CUTIL::CONTAINERF CUTIL::THING) :EXEC (HONS :CONTAINERF (HONS (HONS (QUOTE CUTIL::THING) CUTIL::THING) NIL)))) (DEFUND-INLINE CUTIL::CONTAINERF->THING (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::CONTAINERF-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::CONTAINERF-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE CUTIL::THING) (CDR CUTIL::X)))) (DEFTHM CUTIL::CONSP-OF-CONTAINERF (CONSP (CUTIL::CONTAINERF CUTIL::THING)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::CONTAINERF)))) (DEFTHM CUTIL::BOOLEANP-OF-CONTAINERF-P (BOOLEANP (CUTIL::CONTAINERF-P CUTIL::X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::CONTAINERF-P)))) (DEFTHM CUTIL::CONTAINERF-P-OF-CONTAINERF (IMPLIES (FORCE (AND (CUTIL::FOOF-P CUTIL::THING))) (EQUAL (CUTIL::CONTAINERF-P (CUTIL::CONTAINERF CUTIL::THING)) T)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P CUTIL::CONTAINERF)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE CUTIL::BOOLEANP-OF-CONTAINERF-P (CUTIL::X (CUTIL::CONTAINERF CUTIL::THING))))))) (DEFTHM CUTIL::TAG-OF-CONTAINERF (EQUAL (TAG (CUTIL::CONTAINERF CUTIL::THING)) :CONTAINERF) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::TAG-WHEN-CONTAINERF-P (IMPLIES (CUTIL::CONTAINERF-P CUTIL::X) (EQUAL (TAG CUTIL::X) :CONTAINERF)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::CONTAINERF-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG CUTIL::X) :CONTAINERF)) (EQUAL (CUTIL::CONTAINERF-P CUTIL::X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (CUTIL::TAG-WHEN-CONTAINERF-P CUTIL::CONTAINERF-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (CUTIL::TAG-WHEN-CONTAINERF-P CUTIL::CONTAINERF-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CUTIL::CONSP-WHEN-CONTAINERF-P (IMPLIES (CUTIL::CONTAINERF-P CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::CONTAINERF->THING-OF-CONTAINERF (EQUAL (CUTIL::CONTAINERF->THING (CUTIL::CONTAINERF CUTIL::THING)) CUTIL::THING) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF->THING CUTIL::CONTAINERF)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::FOOF-P-OF-CONTAINERF->THING (IMPLIES (FORCE (CUTIL::CONTAINERF-P CUTIL::X)) (CUTIL::FOOF-P (CUTIL::CONTAINERF->THING CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERF-P CUTIL::CONTAINERF->THING)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO CUTIL::PATBIND-CONTAINERF (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE CUTIL::CONTAINERF) (QUOTE (CUTIL::THING)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CUTIL::CHANGE-CONTAINERF-FN (CUTIL::X CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::CONTAINERF) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (LIST (QUOTE CUTIL::CONTAINERF->THING) CUTIL::X))))) (DEFMACRO CUTIL::CHANGE-CONTAINERF (CUTIL::X &REST ARGS) (CUTIL::CHANGE-CONTAINERF-FN CUTIL::X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (DEFUN CUTIL::MAKE-CONTAINERF-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::CONTAINERF) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-CONTAINERF (&REST ARGS) (CUTIL::MAKE-CONTAINERF-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (DEFUN CUTIL::MAKE-HONSED-CONTAINERF-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::HONSED-CONTAINERF) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-HONSED-CONTAINERF (&REST ARGS) (CUTIL::MAKE-HONSED-CONTAINERF-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE CUTIL::CONTAINERF)))))) (RECORD-EXPANSION (CUTIL::DEFAGGREGATE CUTIL::CONTAINERM (CUTIL::THING) :REQUIRE ((CUTIL::FOOM-P-OF-CONTAINERM->THING (CUTIL::FOOM-P CUTIL::THING))) :TAG :CONTAINERM) (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 . :CONTAINERM) (CUTIL::NAME . CUTIL::CONTAINERM) (CUTIL::FIELDS CUTIL::THING) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . CUTIL::THING) (GUARD . T) (DOC . "") (CUTIL::OPTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERM-P :PARENTS (UNDOCUMENTED) :SHORT NIL :LONG "<p>@(call CUTIL::CONTAINERM-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>thing</tt></li>
</ul><p>Source link: @(srclink containerm)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERM-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT) (:LONG . "<p>@(call CUTIL::CONTAINERM-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>thing</tt></li>
</ul><p>Source link: @(srclink containerm)</p>") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERM-P)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERM :PARENTS (CUTIL::CONTAINERM-P) :SHORT "Raw constructor for <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures." :LONG "<p>Syntax:</p>@(ccall CUTIL::CONTAINERM)<p>This is the lowest-level constructor for <see topic=\"CUTIL____CONTAINERM-P\">containerm-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=\"CUTIL____MAKE-CONTAINERM\">make-containerm</see> or <see topic=\"CUTIL____CHANGE-CONTAINERM\">change-containerm</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>containerm-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=\"CUTIL____HONSED-CONTAINERM\">honsed-containerm</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::CONTAINERM)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERM) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERM-P) (:SHORT . "Raw constructor for <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall CUTIL::CONTAINERM)<p>This is the lowest-level constructor for <see topic=\"CUTIL____CONTAINERM-P\">containerm-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=\"CUTIL____MAKE-CONTAINERM\">make-containerm</see> or <see topic=\"CUTIL____CHANGE-CONTAINERM\">change-containerm</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>containerm-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=\"CUTIL____HONSED-CONTAINERM\">honsed-containerm</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::CONTAINERM)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERM)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::HONSED-CONTAINERM :PARENTS (CUTIL::CONTAINERM-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures." :LONG "<p>Syntax:</p> @(ccall CUTIL::HONSED-CONTAINERM)<p>This is identical to <see topic=\"CUTIL____CONTAINERM\">containerm</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 CUTIL::HONSED-CONTAINERM)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::HONSED-CONTAINERM) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERM-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall CUTIL::HONSED-CONTAINERM)<p>This is identical to <see topic=\"CUTIL____CONTAINERM\">containerm</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 CUTIL::HONSED-CONTAINERM)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::HONSED-CONTAINERM)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-CONTAINERM :PARENTS (CUTIL::CONTAINERM-P) :SHORT "Constructor macro for <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-containerm [:thing &lt;thing&gt;])
</code><p>This is our preferred way to construct <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>containerm-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-CONTAINERM\">change-containerm</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>containerm-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=\"CUTIL____MAKE-HONSED-CONTAINERM\">make-honsed-containerm</see> instead.</p><h3>Definition</h3>

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

                <p>This macro generates a new <tt>containerm-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-CONTAINERM\">change-containerm</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>containerm-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=\"CUTIL____MAKE-HONSED-CONTAINERM\">make-honsed-containerm</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::MAKE-CONTAINERM)@(def CUTIL::MAKE-CONTAINERM-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-CONTAINERM)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-HONSED-CONTAINERM :PARENTS (CUTIL::CONTAINERM-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-containerm [:thing &lt;thing&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-CONTAINERM\">make-containerm</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 CUTIL::MAKE-HONSED-CONTAINERM)@(def CUTIL::MAKE-HONSED-CONTAINERM-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::MAKE-HONSED-CONTAINERM) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERM-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-containerm [:thing &lt;thing&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-CONTAINERM\">make-containerm</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 CUTIL::MAKE-HONSED-CONTAINERM)@(def CUTIL::MAKE-HONSED-CONTAINERM-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-HONSED-CONTAINERM)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CHANGE-CONTAINERM :PARENTS (CUTIL::CONTAINERM-P) :SHORT "A copying macro that lets you create new <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-containerm x
                   [:thing &lt;thing&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-CONTAINERM\">make-containerm</see>.
                It constructs a new <see topic=\"CUTIL____CONTAINERM-P\">containerm-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 CUTIL::CHANGE-CONTAINERM)@(def CUTIL::CHANGE-CONTAINERM-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CHANGE-CONTAINERM) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERM-P) (:SHORT . "A copying macro that lets you create new <see topic=\"CUTIL____CONTAINERM-P\">containerm-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-containerm x
                   [:thing &lt;thing&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-CONTAINERM\">make-containerm</see>.
                It constructs a new <see topic=\"CUTIL____CONTAINERM-P\">containerm-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 CUTIL::CHANGE-CONTAINERM)@(def CUTIL::CHANGE-CONTAINERM-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CHANGE-CONTAINERM)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CONTAINERM->THING :PARENTS (CUTIL::CONTAINERM-P) :SHORT "Access the <tt>thing</tt> field of a @(see CUTIL::CONTAINERM-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CONTAINERM->THING) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::CONTAINERM-P) (:SHORT . "Access the <tt>thing</tt> field of a @(see CUTIL::CONTAINERM-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CONTAINERM->THING)))))) (LOGIC) (DEFUND CUTIL::CONTAINERM-P (CUTIL::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 CUTIL::X) (EQ (CAR CUTIL::X) :CONTAINERM) (ALISTP (CDR CUTIL::X)) (CONSP (CDR CUTIL::X)) (LET ((CUTIL::THING (CDR (ASSOC (QUOTE CUTIL::THING) (CDR CUTIL::X))))) (DECLARE (IGNORABLE CUTIL::THING)) (AND (CUTIL::FOOM-P CUTIL::THING))))) (DEFUND CUTIL::CONTAINERM (CUTIL::THING) (DECLARE (XARGS :GUARD (AND (CUTIL::FOOM-P CUTIL::THING)) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :CONTAINERM (CONS (CONS (QUOTE CUTIL::THING) CUTIL::THING) NIL))) (DEFUN CUTIL::HONSED-CONTAINERM (CUTIL::THING) (DECLARE (XARGS :GUARD (AND (CUTIL::FOOM-P CUTIL::THING)) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (CUTIL::CONTAINERM CUTIL::THING) :EXEC (HONS :CONTAINERM (HONS (HONS (QUOTE CUTIL::THING) CUTIL::THING) NIL)))) (DEFUND-INLINE CUTIL::CONTAINERM->THING (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::CONTAINERM-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::CONTAINERM-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE CUTIL::THING) (CDR CUTIL::X)))) (DEFTHM CUTIL::CONSP-OF-CONTAINERM (CONSP (CUTIL::CONTAINERM CUTIL::THING)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::CONTAINERM)))) (DEFTHM CUTIL::BOOLEANP-OF-CONTAINERM-P (BOOLEANP (CUTIL::CONTAINERM-P CUTIL::X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::CONTAINERM-P)))) (DEFTHM CUTIL::CONTAINERM-P-OF-CONTAINERM (IMPLIES (FORCE (AND (CUTIL::FOOM-P CUTIL::THING))) (EQUAL (CUTIL::CONTAINERM-P (CUTIL::CONTAINERM CUTIL::THING)) T)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P CUTIL::CONTAINERM)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE CUTIL::BOOLEANP-OF-CONTAINERM-P (CUTIL::X (CUTIL::CONTAINERM CUTIL::THING))))))) (DEFTHM CUTIL::TAG-OF-CONTAINERM (EQUAL (TAG (CUTIL::CONTAINERM CUTIL::THING)) :CONTAINERM) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::TAG-WHEN-CONTAINERM-P (IMPLIES (CUTIL::CONTAINERM-P CUTIL::X) (EQUAL (TAG CUTIL::X) :CONTAINERM)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::CONTAINERM-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG CUTIL::X) :CONTAINERM)) (EQUAL (CUTIL::CONTAINERM-P CUTIL::X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (CUTIL::TAG-WHEN-CONTAINERM-P CUTIL::CONTAINERM-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (CUTIL::TAG-WHEN-CONTAINERM-P CUTIL::CONTAINERM-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CUTIL::CONSP-WHEN-CONTAINERM-P (IMPLIES (CUTIL::CONTAINERM-P CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::CONTAINERM->THING-OF-CONTAINERM (EQUAL (CUTIL::CONTAINERM->THING (CUTIL::CONTAINERM CUTIL::THING)) CUTIL::THING) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM->THING CUTIL::CONTAINERM)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::FOOM-P-OF-CONTAINERM->THING (IMPLIES (FORCE (CUTIL::CONTAINERM-P CUTIL::X)) (CUTIL::FOOM-P (CUTIL::CONTAINERM->THING CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::CONTAINERM-P CUTIL::CONTAINERM->THING)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO CUTIL::PATBIND-CONTAINERM (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE CUTIL::CONTAINERM) (QUOTE (CUTIL::THING)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CUTIL::CHANGE-CONTAINERM-FN (CUTIL::X CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::CONTAINERM) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (LIST (QUOTE CUTIL::CONTAINERM->THING) CUTIL::X))))) (DEFMACRO CUTIL::CHANGE-CONTAINERM (CUTIL::X &REST ARGS) (CUTIL::CHANGE-CONTAINERM-FN CUTIL::X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (DEFUN CUTIL::MAKE-CONTAINERM-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::CONTAINERM) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-CONTAINERM (&REST ARGS) (CUTIL::MAKE-CONTAINERM-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (DEFUN CUTIL::MAKE-HONSED-CONTAINERM-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::HONSED-CONTAINERM) (LIST (IF (ASSOC :THING CUTIL::ALIST) (CDR (ASSOC :THING CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-HONSED-CONTAINERM (&REST ARGS) (CUTIL::MAKE-HONSED-CONTAINERM-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:THING))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE CUTIL::CONTAINERM)))))))) (5 RECORD-EXPANSION (CUTIL::DEFAGGREGATE CUTIL::FOO (CUTIL::BAR) :REQUIRE ((CUTIL::FOO-LIST-P-OF-FOO->BAR (CUTIL::FOO-LIST-P CUTIL::BAR))) :ALREADY-DEFINEDP T :TAG :FOO) (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 . :FOO) (CUTIL::NAME . CUTIL::FOO) (CUTIL::FIELDS CUTIL::BAR) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . CUTIL::BAR) (GUARD . T) (DOC . "") (CUTIL::OPTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::FOO-P :PARENTS (UNDOCUMENTED) :SHORT NIL :LONG "<p>@(call CUTIL::FOO-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>bar</tt></li>
</ul><p>Source link: @(srclink foo)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::FOO-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT) (:LONG . "<p>@(call CUTIL::FOO-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>bar</tt></li>
</ul><p>Source link: @(srclink foo)</p>") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::FOO-P)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::FOO :PARENTS (CUTIL::FOO-P) :SHORT "Raw constructor for <see topic=\"CUTIL____FOO-P\">foo-p</see> structures." :LONG "<p>Syntax:</p>@(ccall CUTIL::FOO)<p>This is the lowest-level constructor for <see topic=\"CUTIL____FOO-P\">foo-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=\"CUTIL____MAKE-FOO\">make-foo</see> or <see topic=\"CUTIL____CHANGE-FOO\">change-foo</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>foo-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=\"CUTIL____HONSED-FOO\">honsed-foo</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::FOO)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::FOO) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::FOO-P) (:SHORT . "Raw constructor for <see topic=\"CUTIL____FOO-P\">foo-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall CUTIL::FOO)<p>This is the lowest-level constructor for <see topic=\"CUTIL____FOO-P\">foo-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=\"CUTIL____MAKE-FOO\">make-foo</see> or <see topic=\"CUTIL____CHANGE-FOO\">change-foo</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>foo-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=\"CUTIL____HONSED-FOO\">honsed-foo</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::FOO)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::FOO)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::HONSED-FOO :PARENTS (CUTIL::FOO-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____FOO-P\">foo-p</see> structures." :LONG "<p>Syntax:</p> @(ccall CUTIL::HONSED-FOO)<p>This is identical to <see topic=\"CUTIL____FOO\">foo</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 CUTIL::HONSED-FOO)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::HONSED-FOO) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::FOO-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____FOO-P\">foo-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall CUTIL::HONSED-FOO)<p>This is identical to <see topic=\"CUTIL____FOO\">foo</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 CUTIL::HONSED-FOO)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::HONSED-FOO)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-FOO :PARENTS (CUTIL::FOO-P) :SHORT "Constructor macro for <see topic=\"CUTIL____FOO-P\">foo-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-foo [:bar &lt;bar&gt;])
</code><p>This is our preferred way to construct <see topic=\"CUTIL____FOO-P\">foo-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>foo-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-FOO\">change-foo</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>foo-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=\"CUTIL____MAKE-HONSED-FOO\">make-honsed-foo</see> instead.</p><h3>Definition</h3>

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

                <p>This macro generates a new <tt>foo-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-FOO\">change-foo</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>foo-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=\"CUTIL____MAKE-HONSED-FOO\">make-honsed-foo</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::MAKE-FOO)@(def CUTIL::MAKE-FOO-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-FOO)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-HONSED-FOO :PARENTS (CUTIL::FOO-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____FOO-P\">foo-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-foo [:bar &lt;bar&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-FOO\">make-foo</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 CUTIL::MAKE-HONSED-FOO)@(def CUTIL::MAKE-HONSED-FOO-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::MAKE-HONSED-FOO) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::FOO-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____FOO-P\">foo-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-foo [:bar &lt;bar&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-FOO\">make-foo</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 CUTIL::MAKE-HONSED-FOO)@(def CUTIL::MAKE-HONSED-FOO-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-HONSED-FOO)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CHANGE-FOO :PARENTS (CUTIL::FOO-P) :SHORT "A copying macro that lets you create new <see topic=\"CUTIL____FOO-P\">foo-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-foo x
            [:bar &lt;bar&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-FOO\">make-foo</see>.
                It constructs a new <see topic=\"CUTIL____FOO-P\">foo-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 CUTIL::CHANGE-FOO)@(def CUTIL::CHANGE-FOO-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CHANGE-FOO) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::FOO-P) (:SHORT . "A copying macro that lets you create new <see topic=\"CUTIL____FOO-P\">foo-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-foo x
            [:bar &lt;bar&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-FOO\">make-foo</see>.
                It constructs a new <see topic=\"CUTIL____FOO-P\">foo-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 CUTIL::CHANGE-FOO)@(def CUTIL::CHANGE-FOO-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CHANGE-FOO)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::FOO->BAR :PARENTS (CUTIL::FOO-P) :SHORT "Access the <tt>bar</tt> field of a @(see CUTIL::FOO-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::FOO->BAR) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::FOO-P) (:SHORT . "Access the <tt>bar</tt> field of a @(see CUTIL::FOO-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::FOO->BAR)))))) (LOGIC) (DEFUND CUTIL::FOO (CUTIL::BAR) (DECLARE (XARGS :GUARD (AND (CUTIL::FOO-LIST-P CUTIL::BAR)) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :FOO (CONS (CONS (QUOTE CUTIL::BAR) CUTIL::BAR) NIL))) (DEFUN CUTIL::HONSED-FOO (CUTIL::BAR) (DECLARE (XARGS :GUARD (AND (CUTIL::FOO-LIST-P CUTIL::BAR)) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (CUTIL::FOO CUTIL::BAR) :EXEC (HONS :FOO (HONS (HONS (QUOTE CUTIL::BAR) CUTIL::BAR) NIL)))) (DEFUND-INLINE CUTIL::FOO->BAR (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::FOO-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::FOO-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE CUTIL::BAR) (CDR CUTIL::X)))) (DEFTHM CUTIL::CONSP-OF-FOO (CONSP (CUTIL::FOO CUTIL::BAR)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO)))) (DEFTHM CUTIL::BOOLEANP-OF-FOO-P (BOOLEANP (CUTIL::FOO-P CUTIL::X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-P)))) (DEFTHM CUTIL::FOO-P-OF-FOO (IMPLIES (FORCE (AND (CUTIL::FOO-LIST-P CUTIL::BAR))) (EQUAL (CUTIL::FOO-P (CUTIL::FOO CUTIL::BAR)) T)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P CUTIL::FOO)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE CUTIL::BOOLEANP-OF-FOO-P (CUTIL::X (CUTIL::FOO CUTIL::BAR))))))) (DEFTHM CUTIL::TAG-OF-FOO (EQUAL (TAG (CUTIL::FOO CUTIL::BAR)) :FOO) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::TAG-WHEN-FOO-P (IMPLIES (CUTIL::FOO-P CUTIL::X) (EQUAL (TAG CUTIL::X) :FOO)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::FOO-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG CUTIL::X) :FOO)) (EQUAL (CUTIL::FOO-P CUTIL::X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (CUTIL::TAG-WHEN-FOO-P CUTIL::FOO-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (CUTIL::TAG-WHEN-FOO-P CUTIL::FOO-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CUTIL::CONSP-WHEN-FOO-P (IMPLIES (CUTIL::FOO-P CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::FOO->BAR-OF-FOO (EQUAL (CUTIL::FOO->BAR (CUTIL::FOO CUTIL::BAR)) CUTIL::BAR) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO->BAR CUTIL::FOO)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::FOO-LIST-P-OF-FOO->BAR (IMPLIES (FORCE (CUTIL::FOO-P CUTIL::X)) (CUTIL::FOO-LIST-P (CUTIL::FOO->BAR CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::FOO-P CUTIL::FOO->BAR)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO CUTIL::PATBIND-FOO (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE CUTIL::FOO) (QUOTE (CUTIL::BAR)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CUTIL::CHANGE-FOO-FN (CUTIL::X CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::FOO) (LIST (IF (ASSOC :BAR CUTIL::ALIST) (CDR (ASSOC :BAR CUTIL::ALIST)) (LIST (QUOTE CUTIL::FOO->BAR) CUTIL::X))))) (DEFMACRO CUTIL::CHANGE-FOO (CUTIL::X &REST ARGS) (CUTIL::CHANGE-FOO-FN CUTIL::X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:BAR))))) (DEFUN CUTIL::MAKE-FOO-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::FOO) (LIST (IF (ASSOC :BAR CUTIL::ALIST) (CDR (ASSOC :BAR CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-FOO (&REST ARGS) (CUTIL::MAKE-FOO-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:BAR))))) (DEFUN CUTIL::MAKE-HONSED-FOO-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::HONSED-FOO) (LIST (IF (ASSOC :BAR CUTIL::ALIST) (CDR (ASSOC :BAR CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-HONSED-FOO (&REST ARGS) (CUTIL::MAKE-HONSED-FOO-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:BAR))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE CUTIL::FOO)))))) (6 RECORD-EXPANSION (CUTIL::DEFLIST CUTIL::FOO-LIST-P (CUTIL::X) (CUTIL::FOO-P CUTIL::X) :ELEMENTP-OF-NIL NIL :ALREADY-DEFINEDP T :TRUE-LISTP T) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::FOO-LIST-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 (CUTIL::FOO-P CUTIL::X) T) (EQUAL (CUTIL::FOO-P CUTIL::X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (LOCAL (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM (EQUAL (CUTIL::FOO-P (QUOTE NIL)) (QUOTE NIL)))) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS CUTIL::FOO-LIST-P (:TYPE-PRESCRIPTION CUTIL::FOO-LIST-P) CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM))) (LOCAL (CUTIL::ENABLE-IF-THEOREM CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM)) (DEFTHM CUTIL::FOO-LIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (NOT CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (DEFTHM CUTIL::FOO-LIST-P-OF-CONS (EQUAL (CUTIL::FOO-LIST-P (CONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (LOCAL (IN-THEORY (ENABLE CUTIL::FOO-LIST-P-WHEN-NOT-CONSP CUTIL::FOO-LIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE CUTIL::FOO-LIST-P))) (DEFTHM CUTIL::TRUE-LISTP-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :INDUCT (LEN CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-LIST-FIX (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) (DEFTHM CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::X) (MEMBER-EQUAL CUTIL::A CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL CUTIL::A CUTIL::X) (CUTIL::FOO-LIST-P CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::Y) (SUBSETP-EQUAL CUTIL::X CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE SUBSETP-EQUAL CUTIL::FOO-LIST-P) :EXPAND (TRUE-LISTP CUTIL::X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (CUTIL::A (CAR CUTIL::X)) (CUTIL::X CUTIL::Y)))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-APPEND (EQUAL (CUTIL::FOO-LIST-P (APPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REV (EQUAL (CUTIL::FOO-LIST-P (REV CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE REV)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REVAPPEND (EQUAL (CUTIL::FOO-LIST-P (REVAPPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (REVAPPEND CUTIL::X CUTIL::Y) :IN-THEORY (ENABLE REVAPPEND)))) (DEFTHM CUTIL::FOO-P-OF-CAR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (CAR CUTIL::X)) (CONSP CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-CDR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (CDR CUTIL::X)) T))) (DEFTHM CUTIL::FOO-P-OF-NTH-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (NTH CUTIL::N CUTIL::X)) (< (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :INDUCT (NTH CUTIL::N CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-UPDATE-NTH-WHEN-FOO-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (UPDATE-NTH CUTIL::N CUTIL::Y CUTIL::X)) (AND (<= (NFIX CUTIL::N) (LEN CUTIL::X)) (CUTIL::FOO-P CUTIL::Y))))) (DEFTHM CUTIL::FOO-LIST-P-OF-NTHCDR (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (NTHCDR CUTIL::N CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-TAKE (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (TAKE CUTIL::N CUTIL::X)) (<= (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE CUTIL::N CUTIL::X) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-REPEAT (EQUAL (CUTIL::FOO-LIST-P (REPEAT CUTIL::X CUTIL::N)) (OR (CUTIL::FOO-P CUTIL::X) (ZP CUTIL::N))) :HINTS (("Goal" :INDUCT (REPEAT CUTIL::X CUTIL::N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-LAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (LAST CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-BUTLAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (BUTLAST CUTIL::X CUTIL::N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-RCONS (EQUAL (CUTIL::FOO-LIST-P (RCONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (DUPLICATED-MEMBERS CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SET-DIFFERENCE-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SFIX (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-EQUAL (EQUAL (CUTIL::FOO-LIST-P (UNION-EQUAL CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE UNION-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DIFFERENCE (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::DIFFERENCE CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-1 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-2 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::Y) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-MERGESORT (EQUAL (CUTIL::FOO-LIST-P (SETS::MERGESORT CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :DO-NOT-INDUCT T :USE ((:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::X (SETS::MERGESORT CUTIL::X)) (CUTIL::Y (LIST-FIX CUTIL::X))) (:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::Y (SETS::MERGESORT CUTIL::X)) (CUTIL::X (LIST-FIX CUTIL::X))))))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-1 (IMPLIES (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :DO-NOT-INDUCT T)))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-2 (IMPLIES (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y))) (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :HINTS (("Goal" :DO-NOT-INDUCT T :IN-THEORY (DISABLE SETS::UNION-UNDER-SET-EQUIV CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION) :USE ((:INSTANCE CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION (CUTIL::X CUTIL::X) (CUTIL::Y CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION (EQUAL (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :CASES ((CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :DO-NOT-INDUCT T)))))) (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 (CUTIL::FOO-P CUTIL::X) T) (EQUAL (CUTIL::FOO-P CUTIL::X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (LOCAL (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM (EQUAL (CUTIL::FOO-P (QUOTE NIL)) (QUOTE NIL)))) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS CUTIL::FOO-LIST-P (:TYPE-PRESCRIPTION CUTIL::FOO-LIST-P) CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM))) (LOCAL (CUTIL::ENABLE-IF-THEOREM CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM)) (DEFTHM CUTIL::FOO-LIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (NOT CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (DEFTHM CUTIL::FOO-LIST-P-OF-CONS (EQUAL (CUTIL::FOO-LIST-P (CONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (LOCAL (IN-THEORY (ENABLE CUTIL::FOO-LIST-P-WHEN-NOT-CONSP CUTIL::FOO-LIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE CUTIL::FOO-LIST-P))) (DEFTHM CUTIL::TRUE-LISTP-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :INDUCT (LEN CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-LIST-FIX (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) (DEFTHM CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::X) (MEMBER-EQUAL CUTIL::A CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL CUTIL::A CUTIL::X) (CUTIL::FOO-LIST-P CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::Y) (SUBSETP-EQUAL CUTIL::X CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE SUBSETP-EQUAL CUTIL::FOO-LIST-P) :EXPAND (TRUE-LISTP CUTIL::X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (CUTIL::A (CAR CUTIL::X)) (CUTIL::X CUTIL::Y)))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-APPEND (EQUAL (CUTIL::FOO-LIST-P (APPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REV (EQUAL (CUTIL::FOO-LIST-P (REV CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE REV)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REVAPPEND (EQUAL (CUTIL::FOO-LIST-P (REVAPPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (REVAPPEND CUTIL::X CUTIL::Y) :IN-THEORY (ENABLE REVAPPEND)))) (DEFTHM CUTIL::FOO-P-OF-CAR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (CAR CUTIL::X)) (CONSP CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-CDR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (CDR CUTIL::X)) T))) (DEFTHM CUTIL::FOO-P-OF-NTH-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (NTH CUTIL::N CUTIL::X)) (< (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :INDUCT (NTH CUTIL::N CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-UPDATE-NTH-WHEN-FOO-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (UPDATE-NTH CUTIL::N CUTIL::Y CUTIL::X)) (AND (<= (NFIX CUTIL::N) (LEN CUTIL::X)) (CUTIL::FOO-P CUTIL::Y))))) (DEFTHM CUTIL::FOO-LIST-P-OF-NTHCDR (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (NTHCDR CUTIL::N CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-TAKE (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (TAKE CUTIL::N CUTIL::X)) (<= (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE CUTIL::N CUTIL::X) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-REPEAT (EQUAL (CUTIL::FOO-LIST-P (REPEAT CUTIL::X CUTIL::N)) (OR (CUTIL::FOO-P CUTIL::X) (ZP CUTIL::N))) :HINTS (("Goal" :INDUCT (REPEAT CUTIL::X CUTIL::N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-LAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (LAST CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-BUTLAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (BUTLAST CUTIL::X CUTIL::N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-RCONS (EQUAL (CUTIL::FOO-LIST-P (RCONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (DUPLICATED-MEMBERS CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SET-DIFFERENCE-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SFIX (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-EQUAL (EQUAL (CUTIL::FOO-LIST-P (UNION-EQUAL CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE UNION-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DIFFERENCE (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::DIFFERENCE CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-1 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-2 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::Y) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-MERGESORT (EQUAL (CUTIL::FOO-LIST-P (SETS::MERGESORT CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :DO-NOT-INDUCT T :USE ((:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::X (SETS::MERGESORT CUTIL::X)) (CUTIL::Y (LIST-FIX CUTIL::X))) (:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::Y (SETS::MERGESORT CUTIL::X)) (CUTIL::X (LIST-FIX CUTIL::X))))))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-1 (IMPLIES (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :DO-NOT-INDUCT T)))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-2 (IMPLIES (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y))) (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :HINTS (("Goal" :DO-NOT-INDUCT T :IN-THEORY (DISABLE SETS::UNION-UNDER-SET-EQUIV CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION) :USE ((:INSTANCE CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION (CUTIL::X CUTIL::X) (CUTIL::Y CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION (EQUAL (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :CASES ((CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :DO-NOT-INDUCT T)))) (ENCAPSULATE NIL (LOGIC) (SET-INHIBIT-WARNINGS "theory" "free" "non-rec" "double-rewrite") (LOCAL (DEFTHM CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM (OR (EQUAL (CUTIL::FOO-P CUTIL::X) T) (EQUAL (CUTIL::FOO-P CUTIL::X) NIL)) :RULE-CLASSES :TYPE-PRESCRIPTION)) (RECORD-EXPANSION (LOCAL (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::DEFLIST-LOCAL-ELEMENTP-OF-NIL-THM (EQUAL (CUTIL::FOO-P (QUOTE NIL)) (QUOTE NIL)))) (LOCAL (VALUE-TRIPLE :ELIDED))) (LOCAL (IN-THEORY (THEORY (QUOTE MINIMAL-THEORY)))) (LOCAL (IN-THEORY (ENABLE CUTIL::DEFLIST-SUPPORT-LEMMAS CUTIL::FOO-LIST-P (:TYPE-PRESCRIPTION CUTIL::FOO-LIST-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 CUTIL::FOO-LIST-P-WHEN-NOT-CONSP (IMPLIES (NOT (CONSP CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (NOT CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (DEFTHM CUTIL::FOO-LIST-P-OF-CONS (EQUAL (CUTIL::FOO-LIST-P (CONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::FOO-LIST-P)))) (LOCAL (IN-THEORY (ENABLE CUTIL::FOO-LIST-P-WHEN-NOT-CONSP CUTIL::FOO-LIST-P-OF-CONS))) (LOCAL (IN-THEORY (DISABLE CUTIL::FOO-LIST-P))) (DEFTHM CUTIL::TRUE-LISTP-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :INDUCT (LEN CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-LIST-FIX (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) (DEFTHM CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::X) (MEMBER-EQUAL CUTIL::A CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (MEMBER-EQUAL CUTIL::A CUTIL::X) (CUTIL::FOO-LIST-P CUTIL::X)) (EQUAL (CUTIL::FOO-P CUTIL::A) T)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE MEMBER-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (IMPLIES (AND (CUTIL::FOO-LIST-P CUTIL::Y) (SUBSETP-EQUAL CUTIL::X CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))) :RULE-CLASSES ((:REWRITE) (:REWRITE :COROLLARY (IMPLIES (AND (SUBSETP-EQUAL CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P CUTIL::X) (TRUE-LISTP CUTIL::X))))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE SUBSETP-EQUAL CUTIL::FOO-LIST-P) :EXPAND (TRUE-LISTP CUTIL::X) :DO-NOT (QUOTE (ELIMINATE-DESTRUCTORS))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:USE ((:INSTANCE CUTIL::FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P (CUTIL::A (CAR CUTIL::X)) (CUTIL::X CUTIL::Y)))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-APPEND (EQUAL (CUTIL::FOO-LIST-P (APPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE APPEND)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REV (EQUAL (CUTIL::FOO-LIST-P (REV CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :EXPAND (LIST-FIX CUTIL::X) :IN-THEORY (ENABLE REV)))) (DEFTHM CUTIL::FOO-LIST-P-OF-REVAPPEND (EQUAL (CUTIL::FOO-LIST-P (REVAPPEND CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P CUTIL::Y))) :HINTS (("Goal" :INDUCT (REVAPPEND CUTIL::X CUTIL::Y) :IN-THEORY (ENABLE REVAPPEND)))) (DEFTHM CUTIL::FOO-P-OF-CAR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (CAR CUTIL::X)) (CONSP CUTIL::X))) :HINTS (("Goal" :IN-THEORY (ENABLE DEFAULT-CAR) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-CDR-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (CDR CUTIL::X)) T))) (DEFTHM CUTIL::FOO-P-OF-NTH-WHEN-FOO-LIST-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-P (NTH CUTIL::N CUTIL::X)) (< (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :INDUCT (NTH CUTIL::N CUTIL::X)))) (DEFTHM CUTIL::FOO-LIST-P-OF-UPDATE-NTH-WHEN-FOO-P (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (UPDATE-NTH CUTIL::N CUTIL::Y CUTIL::X)) (AND (<= (NFIX CUTIL::N) (LEN CUTIL::X)) (CUTIL::FOO-P CUTIL::Y))))) (DEFTHM CUTIL::FOO-LIST-P-OF-NTHCDR (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (NTHCDR CUTIL::N CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-TAKE (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (TAKE CUTIL::N CUTIL::X)) (<= (NFIX CUTIL::N) (LEN CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE TAKE-REDEFINITION) :INDUCT (TAKE CUTIL::N CUTIL::X) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-REPEAT (EQUAL (CUTIL::FOO-LIST-P (REPEAT CUTIL::X CUTIL::N)) (OR (CUTIL::FOO-P CUTIL::X) (ZP CUTIL::N))) :HINTS (("Goal" :INDUCT (REPEAT CUTIL::X CUTIL::N) :IN-THEORY (ENABLE REPEAT CUTIL::DEFLIST-LOCAL-BOOLEANP-ELEMENT-THM) :EXPAND ((CUTIL::FOO-LIST-P CUTIL::X) (:FREE (CUTIL::X CUTIL::Y) (CUTIL::FOO-LIST-P (CONS CUTIL::X CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-LAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (LAST CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-BUTLAST (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (BUTLAST CUTIL::X CUTIL::N)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-RCONS (EQUAL (CUTIL::FOO-LIST-P (RCONS CUTIL::A CUTIL::X)) (AND (CUTIL::FOO-P CUTIL::A) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)))) :HINTS (("Goal" :IN-THEORY (ENABLE RCONS)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DUPLICATED-MEMBERS (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (DUPLICATED-MEMBERS CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SET-DIFFERENCE-EQUAL (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SET-DIFFERENCE-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-1 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECTION-EQUAL-2 (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)) (EQUAL (CUTIL::FOO-LIST-P (INTERSECTION-EQUAL CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-SFIX (IMPLIES (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::X)) (EQUAL (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T :CASES ((SETS::SETP CUTIL::X))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-EQUAL (EQUAL (CUTIL::FOO-LIST-P (UNION-EQUAL CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X)) (CUTIL::FOO-LIST-P (DOUBLE-REWRITE CUTIL::Y)))) :HINTS (("Goal" :INDUCT (LEN CUTIL::X) :IN-THEORY (ENABLE UNION-EQUAL)))) (DEFTHM CUTIL::FOO-LIST-P-OF-DIFFERENCE (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::DIFFERENCE CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-1 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::X) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-INTERSECT-2 (IMPLIES (CUTIL::FOO-LIST-P CUTIL::Y) (EQUAL (CUTIL::FOO-LIST-P (SETS::INTERSECT CUTIL::X CUTIL::Y)) T)) :HINTS (("Goal" :DO-NOT-INDUCT T))) (DEFTHM CUTIL::FOO-LIST-P-OF-MERGESORT (EQUAL (CUTIL::FOO-LIST-P (SETS::MERGESORT CUTIL::X)) (CUTIL::FOO-LIST-P (LIST-FIX CUTIL::X))) :HINTS (("Goal" :DO-NOT-INDUCT T :USE ((:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::X (SETS::MERGESORT CUTIL::X)) (CUTIL::Y (LIST-FIX CUTIL::X))) (:INSTANCE CUTIL::FOO-LIST-P-WHEN-SUBSETP-EQUAL (CUTIL::Y (SETS::MERGESORT CUTIL::X)) (CUTIL::X (LIST-FIX CUTIL::X))))))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-1 (IMPLIES (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :DO-NOT-INDUCT T)))) (LOCAL (DEFTHM CUTIL::FOO-LIST-P-OF-UNION-LEMMA-2 (IMPLIES (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y))) (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :HINTS (("Goal" :DO-NOT-INDUCT T :IN-THEORY (DISABLE SETS::UNION-UNDER-SET-EQUIV CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION) :USE ((:INSTANCE CUTIL::DEFLIST-LEMMA-SUBSETP-OF-UNION (CUTIL::X CUTIL::X) (CUTIL::Y CUTIL::Y))))))) (DEFTHM CUTIL::FOO-LIST-P-OF-UNION (EQUAL (CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y)) (AND (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::X)) (CUTIL::FOO-LIST-P (SETS::SFIX CUTIL::Y)))) :HINTS (("Goal" :CASES ((CUTIL::FOO-LIST-P (SETS::UNION CUTIL::X CUTIL::Y))) :DO-NOT-INDUCT T)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::FOO-LIST-P)) (XDOC::PARENTS (QUOTE (UNDOCUMENTED))) (XDOC::SHORT (QUOTE "@(call FOO-LIST-P) recognizes lists where every element satisfies @(see FOO-P).")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::FOO-LIST-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
\"strict\" in that it requires @('x') to be a \"properly\" nil-terminated
list.</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 . CUTIL::FOO-LIST-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT . "@(call FOO-LIST-P) recognizes lists where every element satisfies @(see FOO-P).") (:LONG . "<p>This is an ordinary @(see cutil::deflist).  It is
\"strict\" in that it requires @('x') to be a \"properly\" nil-terminated
list.</p>

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|FOO-LIST-P-WHEN-NOT-CONSP|)
@(def |CUTIL|::|FOO-LIST-P-OF-CONS|)
@(def |CUTIL|::|TRUE-LISTP-WHEN-FOO-LIST-P|)
@(def |CUTIL|::|FOO-LIST-P-OF-LIST-FIX|)
@(def |CUTIL|::|FOO-P-WHEN-MEMBER-EQUAL-OF-FOO-LIST-P|)
@(def |CUTIL|::|FOO-LIST-P-WHEN-SUBSETP-EQUAL|)
@(def |CUTIL|::|FOO-LIST-P-OF-APPEND|)
@(def |CUTIL|::|FOO-LIST-P-OF-REV|)
@(def |CUTIL|::|FOO-LIST-P-OF-REVAPPEND|)
@(def |CUTIL|::|FOO-P-OF-CAR-WHEN-FOO-LIST-P|)
@(def |CUTIL|::|FOO-LIST-P-OF-CDR-WHEN-FOO-LIST-P|)
@(def |CUTIL|::|FOO-P-OF-NTH-WHEN-FOO-LIST-P|)
@(def |CUTIL|::|FOO-LIST-P-OF-UPDATE-NTH-WHEN-FOO-P|)
@(def |CUTIL|::|FOO-LIST-P-OF-NTHCDR|)
@(def |CUTIL|::|FOO-LIST-P-OF-TAKE|)
@(def |CUTIL|::|FOO-LIST-P-OF-REPEAT|)
@(def |CUTIL|::|FOO-LIST-P-OF-LAST|)
@(def |CUTIL|::|FOO-LIST-P-OF-BUTLAST|)
@(def |CUTIL|::|FOO-LIST-P-OF-RCONS|)
@(def |CUTIL|::|FOO-LIST-P-OF-DUPLICATED-MEMBERS|)
@(def |CUTIL|::|FOO-LIST-P-OF-SET-DIFFERENCE-EQUAL|)
@(def |CUTIL|::|FOO-LIST-P-OF-INTERSECTION-EQUAL-1|)
@(def |CUTIL|::|FOO-LIST-P-OF-INTERSECTION-EQUAL-2|)
@(def |CUTIL|::|FOO-LIST-P-OF-SFIX|)
@(def |CUTIL|::|FOO-LIST-P-OF-UNION-EQUAL|)
@(def |CUTIL|::|FOO-LIST-P-OF-DIFFERENCE|)
@(def |CUTIL|::|FOO-LIST-P-OF-INTERSECT-1|)
@(def |CUTIL|::|FOO-LIST-P-OF-INTERSECT-2|)
@(def |CUTIL|::|FOO-LIST-P-OF-MERGESORT|)
@(def |CUTIL|::|FOO-LIST-P-OF-UNION|)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::FOO-LIST-P)))))) (VALUE-TRIPLE (QUOTE CUTIL::FOO-LIST-P))))) (7 RECORD-EXPANSION (CUTIL::DEFAGGREGATE CUTIL::PAIR-O-INTS ((CUTIL::LEFT INTEGERP "Left part of pair") (CUTIL::RIGHT INTEGERP "Right part of pair")) :TAG :PAIR-O-INTS) (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 . :PAIR-O-INTS) (CUTIL::NAME . CUTIL::PAIR-O-INTS) (CUTIL::FIELDS CUTIL::LEFT CUTIL::RIGHT) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . CUTIL::LEFT) (GUARD INTEGERP CUTIL::LEFT) (DOC . "Left part of pair") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::RIGHT) (GUARD INTEGERP CUTIL::RIGHT) (DOC . "Right part of pair") (CUTIL::OPTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::PAIR-O-INTS-P :PARENTS (UNDOCUMENTED) :SHORT NIL :LONG "<p>@(call CUTIL::PAIR-O-INTS-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>left</tt> &mdash; Left part of pair.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(integerp left)').</color></li>
<li><tt>right</tt> &mdash; Right part of pair.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(integerp right)').</color></li>
</ul><p>Source link: @(srclink pair-o-ints)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::PAIR-O-INTS-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT) (:LONG . "<p>@(call CUTIL::PAIR-O-INTS-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>left</tt> &mdash; Left part of pair.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(integerp left)').</color></li>
<li><tt>right</tt> &mdash; Right part of pair.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(integerp right)').</color></li>
</ul><p>Source link: @(srclink pair-o-ints)</p>") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::PAIR-O-INTS-P)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::PAIR-O-INTS :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Raw constructor for <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures." :LONG "<p>Syntax:</p>@(ccall CUTIL::PAIR-O-INTS)<p>This is the lowest-level constructor for <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-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=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</see> or <see topic=\"CUTIL____CHANGE-PAIR-O-INTS\">change-pair-o-ints</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>pair-o-ints-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=\"CUTIL____HONSED-PAIR-O-INTS\">honsed-pair-o-ints</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::PAIR-O-INTS)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::PAIR-O-INTS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "Raw constructor for <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall CUTIL::PAIR-O-INTS)<p>This is the lowest-level constructor for <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-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=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</see> or <see topic=\"CUTIL____CHANGE-PAIR-O-INTS\">change-pair-o-ints</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>pair-o-ints-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=\"CUTIL____HONSED-PAIR-O-INTS\">honsed-pair-o-ints</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::PAIR-O-INTS)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::PAIR-O-INTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::HONSED-PAIR-O-INTS :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures." :LONG "<p>Syntax:</p> @(ccall CUTIL::HONSED-PAIR-O-INTS)<p>This is identical to <see topic=\"CUTIL____PAIR-O-INTS\">pair-o-ints</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 CUTIL::HONSED-PAIR-O-INTS)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::HONSED-PAIR-O-INTS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall CUTIL::HONSED-PAIR-O-INTS)<p>This is identical to <see topic=\"CUTIL____PAIR-O-INTS\">pair-o-ints</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 CUTIL::HONSED-PAIR-O-INTS)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::HONSED-PAIR-O-INTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-PAIR-O-INTS :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Constructor macro for <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-pair-o-ints [:left &lt;left&gt;]
                  [:right &lt;right&gt;])
</code><p>This is our preferred way to construct <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>pair-o-ints-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-PAIR-O-INTS\">change-pair-o-ints</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>pair-o-ints-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=\"CUTIL____MAKE-HONSED-PAIR-O-INTS\">make-honsed-pair-o-ints</see> instead.</p><h3>Definition</h3>

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

                <p>This macro generates a new <tt>pair-o-ints-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-PAIR-O-INTS\">change-pair-o-ints</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>pair-o-ints-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=\"CUTIL____MAKE-HONSED-PAIR-O-INTS\">make-honsed-pair-o-ints</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::MAKE-PAIR-O-INTS)@(def CUTIL::MAKE-PAIR-O-INTS-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-PAIR-O-INTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-HONSED-PAIR-O-INTS :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-pair-o-ints [:left &lt;left&gt;]
                         [:right &lt;right&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</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 CUTIL::MAKE-HONSED-PAIR-O-INTS)@(def CUTIL::MAKE-HONSED-PAIR-O-INTS-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::MAKE-HONSED-PAIR-O-INTS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-pair-o-ints [:left &lt;left&gt;]
                         [:right &lt;right&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</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 CUTIL::MAKE-HONSED-PAIR-O-INTS)@(def CUTIL::MAKE-HONSED-PAIR-O-INTS-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-HONSED-PAIR-O-INTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CHANGE-PAIR-O-INTS :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "A copying macro that lets you create new <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-pair-o-ints x
                    [:left &lt;left&gt;]
                    [:right &lt;right&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</see>.
                It constructs a new <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-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 CUTIL::CHANGE-PAIR-O-INTS)@(def CUTIL::CHANGE-PAIR-O-INTS-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CHANGE-PAIR-O-INTS) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "A copying macro that lets you create new <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-pair-o-ints x
                    [:left &lt;left&gt;]
                    [:right &lt;right&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-PAIR-O-INTS\">make-pair-o-ints</see>.
                It constructs a new <see topic=\"CUTIL____PAIR-O-INTS-P\">pair-o-ints-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 CUTIL::CHANGE-PAIR-O-INTS)@(def CUTIL::CHANGE-PAIR-O-INTS-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CHANGE-PAIR-O-INTS)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::PAIR-O-INTS->LEFT :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Access the <tt>left</tt> field of a @(see CUTIL::PAIR-O-INTS-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::PAIR-O-INTS->LEFT) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "Access the <tt>left</tt> field of a @(see CUTIL::PAIR-O-INTS-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::PAIR-O-INTS->LEFT)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::PAIR-O-INTS->RIGHT :PARENTS (CUTIL::PAIR-O-INTS-P) :SHORT "Access the <tt>right</tt> field of a @(see CUTIL::PAIR-O-INTS-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::PAIR-O-INTS->RIGHT) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::PAIR-O-INTS-P) (:SHORT . "Access the <tt>right</tt> field of a @(see CUTIL::PAIR-O-INTS-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::PAIR-O-INTS->RIGHT)))))) (LOGIC) (DEFUND CUTIL::PAIR-O-INTS-P (CUTIL::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 CUTIL::X) (EQ (CAR CUTIL::X) :PAIR-O-INTS) (ALISTP (CDR CUTIL::X)) (CONSP (CDR CUTIL::X)) (LET ((CUTIL::LEFT (CDR (ASSOC (QUOTE CUTIL::LEFT) (CDR CUTIL::X)))) (CUTIL::RIGHT (CDR (ASSOC (QUOTE CUTIL::RIGHT) (CDR CUTIL::X))))) (DECLARE (IGNORABLE CUTIL::LEFT CUTIL::RIGHT)) (AND (INTEGERP CUTIL::LEFT) (INTEGERP CUTIL::RIGHT))))) (DEFUND CUTIL::PAIR-O-INTS (CUTIL::LEFT CUTIL::RIGHT) (DECLARE (XARGS :GUARD (AND (INTEGERP CUTIL::LEFT) (INTEGERP CUTIL::RIGHT)) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :PAIR-O-INTS (CONS (CONS (QUOTE CUTIL::LEFT) CUTIL::LEFT) (CONS (CONS (QUOTE CUTIL::RIGHT) CUTIL::RIGHT) NIL)))) (DEFUN CUTIL::HONSED-PAIR-O-INTS (CUTIL::LEFT CUTIL::RIGHT) (DECLARE (XARGS :GUARD (AND (INTEGERP CUTIL::LEFT) (INTEGERP CUTIL::RIGHT)) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT) :EXEC (HONS :PAIR-O-INTS (HONS (HONS (QUOTE CUTIL::LEFT) CUTIL::LEFT) (HONS (HONS (QUOTE CUTIL::RIGHT) CUTIL::RIGHT) NIL))))) (DEFUND-INLINE CUTIL::PAIR-O-INTS->LEFT (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::PAIR-O-INTS-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::PAIR-O-INTS-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE CUTIL::LEFT) (CDR CUTIL::X)))) (DEFUND-INLINE CUTIL::PAIR-O-INTS->RIGHT (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::PAIR-O-INTS-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::PAIR-O-INTS-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (ASSOC (QUOTE CUTIL::RIGHT) (CDR CUTIL::X)))) (DEFTHM CUTIL::CONSP-OF-PAIR-O-INTS (CONSP (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::PAIR-O-INTS)))) (DEFTHM CUTIL::BOOLEANP-OF-PAIR-O-INTS-P (BOOLEANP (CUTIL::PAIR-O-INTS-P CUTIL::X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::PAIR-O-INTS-P)))) (DEFTHM CUTIL::PAIR-O-INTS-P-OF-PAIR-O-INTS (IMPLIES (FORCE (AND (INTEGERP CUTIL::LEFT) (INTEGERP CUTIL::RIGHT))) (EQUAL (CUTIL::PAIR-O-INTS-P (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT)) T)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P CUTIL::PAIR-O-INTS)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE CUTIL::BOOLEANP-OF-PAIR-O-INTS-P (CUTIL::X (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT))))))) (DEFTHM CUTIL::TAG-OF-PAIR-O-INTS (EQUAL (TAG (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT)) :PAIR-O-INTS) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::TAG-WHEN-PAIR-O-INTS-P (IMPLIES (CUTIL::PAIR-O-INTS-P CUTIL::X) (EQUAL (TAG CUTIL::X) :PAIR-O-INTS)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::PAIR-O-INTS-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG CUTIL::X) :PAIR-O-INTS)) (EQUAL (CUTIL::PAIR-O-INTS-P CUTIL::X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (CUTIL::TAG-WHEN-PAIR-O-INTS-P CUTIL::PAIR-O-INTS-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (CUTIL::TAG-WHEN-PAIR-O-INTS-P CUTIL::PAIR-O-INTS-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CUTIL::CONSP-WHEN-PAIR-O-INTS-P (IMPLIES (CUTIL::PAIR-O-INTS-P CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::PAIR-O-INTS->LEFT-OF-PAIR-O-INTS (EQUAL (CUTIL::PAIR-O-INTS->LEFT (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT)) CUTIL::LEFT) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS->LEFT CUTIL::PAIR-O-INTS)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::PAIR-O-INTS->RIGHT-OF-PAIR-O-INTS (EQUAL (CUTIL::PAIR-O-INTS->RIGHT (CUTIL::PAIR-O-INTS CUTIL::LEFT CUTIL::RIGHT)) CUTIL::RIGHT) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS->RIGHT CUTIL::PAIR-O-INTS)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::RETURN-TYPE-OF-PAIR-O-INTS->LEFT (IMPLIES (FORCE (CUTIL::PAIR-O-INTS-P CUTIL::X)) (INTEGERP (CUTIL::PAIR-O-INTS->LEFT CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P CUTIL::PAIR-O-INTS->LEFT CUTIL::PAIR-O-INTS->RIGHT)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::RETURN-TYPE-OF-PAIR-O-INTS->RIGHT (IMPLIES (FORCE (CUTIL::PAIR-O-INTS-P CUTIL::X)) (INTEGERP (CUTIL::PAIR-O-INTS->RIGHT CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::PAIR-O-INTS-P CUTIL::PAIR-O-INTS->LEFT CUTIL::PAIR-O-INTS->RIGHT)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO CUTIL::PATBIND-PAIR-O-INTS (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE CUTIL::PAIR-O-INTS) (QUOTE (CUTIL::LEFT CUTIL::RIGHT)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CUTIL::CHANGE-PAIR-O-INTS-FN (CUTIL::X CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::PAIR-O-INTS) (LIST (IF (ASSOC :LEFT CUTIL::ALIST) (CDR (ASSOC :LEFT CUTIL::ALIST)) (LIST (QUOTE CUTIL::PAIR-O-INTS->LEFT) CUTIL::X)) (IF (ASSOC :RIGHT CUTIL::ALIST) (CDR (ASSOC :RIGHT CUTIL::ALIST)) (LIST (QUOTE CUTIL::PAIR-O-INTS->RIGHT) CUTIL::X))))) (DEFMACRO CUTIL::CHANGE-PAIR-O-INTS (CUTIL::X &REST ARGS) (CUTIL::CHANGE-PAIR-O-INTS-FN CUTIL::X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:LEFT :RIGHT))))) (DEFUN CUTIL::MAKE-PAIR-O-INTS-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::PAIR-O-INTS) (LIST (IF (ASSOC :LEFT CUTIL::ALIST) (CDR (ASSOC :LEFT CUTIL::ALIST)) (QUOTE NIL)) (IF (ASSOC :RIGHT CUTIL::ALIST) (CDR (ASSOC :RIGHT CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-PAIR-O-INTS (&REST ARGS) (CUTIL::MAKE-PAIR-O-INTS-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:LEFT :RIGHT))))) (DEFUN CUTIL::MAKE-HONSED-PAIR-O-INTS-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::HONSED-PAIR-O-INTS) (LIST (IF (ASSOC :LEFT CUTIL::ALIST) (CDR (ASSOC :LEFT CUTIL::ALIST)) (QUOTE NIL)) (IF (ASSOC :RIGHT CUTIL::ALIST) (CDR (ASSOC :RIGHT CUTIL::ALIST)) (QUOTE NIL))))) (DEFMACRO CUTIL::MAKE-HONSED-PAIR-O-INTS (&REST ARGS) (CUTIL::MAKE-HONSED-PAIR-O-INTS-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:LEFT :RIGHT))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE CUTIL::PAIR-O-INTS)))))) (9 RECORD-EXPANSION (ASSERT! (EQUAL (CUTIL::SUM-A-PAIR (CUTIL::MAKE-PAIR-O-INTS :LEFT 4 :RIGHT 5)) 9)) (VALUE-TRIPLE :SUCCESS)) (10 RECORD-EXPANSION (CUTIL::DEFAGGREGATE CUTIL::EMPLOYEE :TAG :EMPLOYEE ((CUTIL::NAME STRINGP "some documentation") (CUTIL::SALARY NATP :RULE-CLASSES :TYPE-PRESCRIPTION :DEFAULT 25)) :LEGIBLEP NIL :SHORT "Hello!") (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 . :EMPLOYEE) (CUTIL::NAME . CUTIL::EMPLOYEE) (CUTIL::FIELDS CUTIL::NAME CUTIL::SALARY) (CUTIL::EFIELDS (:FORMAL (CUTIL::NAME . CUTIL::NAME) (GUARD STRINGP CUTIL::NAME) (DOC . "some documentation") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::SALARY) (GUARD NATP CUTIL::SALARY) (DOC . "") (CUTIL::OPTS (:DEFAULT . 25) (:RULE-CLASSES . :TYPE-PRESCRIPTION))))))) (RECORD-EXPANSION (DEFXDOC CUTIL::EMPLOYEE-P :PARENTS (UNDOCUMENTED) :SHORT "Hello!" :LONG "<p>@(call CUTIL::EMPLOYEE-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>name</tt> &mdash; some documentation.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(stringp name)').</color></li>
<li><tt>salary</tt> &mdash; <color rgb='#606060'>Invariant @('(natp salary)').</color></li>
</ul><p>Source link: @(srclink employee)</p>") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::EMPLOYEE-P) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS UNDOCUMENTED) (:SHORT . "Hello!") (:LONG . "<p>@(call CUTIL::EMPLOYEE-P) is a @(see cutil::defaggregate) of the following fields.</p><ul><li><tt>name</tt> &mdash; some documentation.<br/>&nbsp;&nbsp;&nbsp;&nbsp;<color rgb='#606060'>Invariant @('(stringp name)').</color></li>
<li><tt>salary</tt> &mdash; <color rgb='#606060'>Invariant @('(natp salary)').</color></li>
</ul><p>Source link: @(srclink employee)</p>") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::EMPLOYEE-P)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::EMPLOYEE :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Raw constructor for <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures." :LONG "<p>Syntax:</p>@(ccall CUTIL::EMPLOYEE)<p>This is the lowest-level constructor for <see topic=\"CUTIL____EMPLOYEE-P\">employee-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=\"CUTIL____MAKE-EMPLOYEE\">make-employee</see> or <see topic=\"CUTIL____CHANGE-EMPLOYEE\">change-employee</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>employee-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=\"CUTIL____HONSED-EMPLOYEE\">honsed-employee</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::EMPLOYEE)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::EMPLOYEE) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "Raw constructor for <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures.") (:LONG . "<p>Syntax:</p>@(ccall CUTIL::EMPLOYEE)<p>This is the lowest-level constructor for <see topic=\"CUTIL____EMPLOYEE-P\">employee-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=\"CUTIL____MAKE-EMPLOYEE\">make-employee</see> or <see topic=\"CUTIL____CHANGE-EMPLOYEE\">change-employee</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>employee-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=\"CUTIL____HONSED-EMPLOYEE\">honsed-employee</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary constructor function introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::EMPLOYEE)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::EMPLOYEE)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::HONSED-EMPLOYEE :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures." :LONG "<p>Syntax:</p> @(ccall CUTIL::HONSED-EMPLOYEE)<p>This is identical to <see topic=\"CUTIL____EMPLOYEE\">employee</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 CUTIL::HONSED-EMPLOYEE)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::HONSED-EMPLOYEE) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "Raw constructor for @(see acl2::hons)ed <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures.") (:LONG . "<p>Syntax:</p> @(ccall CUTIL::HONSED-EMPLOYEE)<p>This is identical to <see topic=\"CUTIL____EMPLOYEE\">employee</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 CUTIL::HONSED-EMPLOYEE)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::HONSED-EMPLOYEE)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-EMPLOYEE :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Constructor macro for <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-employee [:name &lt;name&gt;]
               [:salary &lt;salary&gt;])
</code><p>This is our preferred way to construct <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new <tt>employee-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-EMPLOYEE\">change-employee</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>employee-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=\"CUTIL____MAKE-HONSED-EMPLOYEE\">make-honsed-employee</see> instead.</p><h3>Definition</h3>

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

                <p>This macro generates a new <tt>employee-p</tt> structure from
                scratch.  See also <see topic=\"CUTIL____CHANGE-EMPLOYEE\">change-employee</see>, which can \"change\" an
                existing structure, instead.</p><p>The <tt>employee-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=\"CUTIL____MAKE-HONSED-EMPLOYEE\">make-honsed-employee</see> instead.</p><h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                cutil::defaggregate).</p>@(def CUTIL::MAKE-EMPLOYEE)@(def CUTIL::MAKE-EMPLOYEE-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-EMPLOYEE)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::MAKE-HONSED-EMPLOYEE :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures." :LONG "<p>Syntax:</p><code>
(make-honsed-employee [:name &lt;name&gt;]
                      [:salary &lt;salary&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-EMPLOYEE\">make-employee</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 CUTIL::MAKE-HONSED-EMPLOYEE)@(def CUTIL::MAKE-HONSED-EMPLOYEE-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::MAKE-HONSED-EMPLOYEE) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "Constructor macro for @(see acl2::hons)ed <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures.") (:LONG . "<p>Syntax:</p><code>
(make-honsed-employee [:name &lt;name&gt;]
                      [:salary &lt;salary&gt;])
</code><p>This is identical to <see topic=\"CUTIL____MAKE-EMPLOYEE\">make-employee</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 CUTIL::MAKE-HONSED-EMPLOYEE)@(def CUTIL::MAKE-HONSED-EMPLOYEE-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::MAKE-HONSED-EMPLOYEE)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::CHANGE-EMPLOYEE :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "A copying macro that lets you create new <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures, based on existing structures." :LONG "<p>Syntax:</p><code>
(change-employee x
                 [:name &lt;name&gt;]
                 [:salary &lt;salary&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-EMPLOYEE\">make-employee</see>.
                It constructs a new <see topic=\"CUTIL____EMPLOYEE-P\">employee-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 CUTIL::CHANGE-EMPLOYEE)@(def CUTIL::CHANGE-EMPLOYEE-FN)") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::CHANGE-EMPLOYEE) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "A copying macro that lets you create new <see topic=\"CUTIL____EMPLOYEE-P\">employee-p</see> structures, based on existing structures.") (:LONG . "<p>Syntax:</p><code>
(change-employee x
                 [:name &lt;name&gt;]
                 [:salary &lt;salary&gt;])
</code><p>This is a sometimes useful alternative to <see topic=\"CUTIL____MAKE-EMPLOYEE\">make-employee</see>.
                It constructs a new <see topic=\"CUTIL____EMPLOYEE-P\">employee-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 CUTIL::CHANGE-EMPLOYEE)@(def CUTIL::CHANGE-EMPLOYEE-FN)") (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::CHANGE-EMPLOYEE)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::EMPLOYEE->NAME :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Access the <tt>name</tt> field of a @(see CUTIL::EMPLOYEE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::EMPLOYEE->NAME) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "Access the <tt>name</tt> field of a @(see CUTIL::EMPLOYEE-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::EMPLOYEE->NAME)))))) (RECORD-EXPANSION (DEFXDOC CUTIL::EMPLOYEE->SALARY :PARENTS (CUTIL::EMPLOYEE-P) :SHORT "Access the <tt>salary</tt> field of a @(see CUTIL::EMPLOYEE-P) structure.") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . CUTIL::EMPLOYEE->SALARY) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::EMPLOYEE-P) (:SHORT . "Access the <tt>salary</tt> field of a @(see CUTIL::EMPLOYEE-P) structure.") (:LONG) (:FROM . "[books]/cutil/defaggregate-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::EMPLOYEE->SALARY)))))) (LOGIC) (DEFUND CUTIL::EMPLOYEE-P (CUTIL::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 CUTIL::X) (EQ (CAR CUTIL::X) :EMPLOYEE) (CONSP (CDR CUTIL::X)) (LET ((CUTIL::NAME (CAR (CDR CUTIL::X))) (CUTIL::SALARY (CDR (CDR CUTIL::X)))) (DECLARE (IGNORABLE CUTIL::NAME CUTIL::SALARY)) (AND (STRINGP CUTIL::NAME) (NATP CUTIL::SALARY))))) (DEFUND CUTIL::EMPLOYEE (CUTIL::NAME CUTIL::SALARY) (DECLARE (XARGS :GUARD (AND (STRINGP CUTIL::NAME) (NATP CUTIL::SALARY)) :GUARD-HINTS (("Goal" :IN-THEORY (THEORY (QUOTE MINIMAL-THEORY))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (CONS :EMPLOYEE (CONS CUTIL::NAME CUTIL::SALARY))) (DEFUN CUTIL::HONSED-EMPLOYEE (CUTIL::NAME CUTIL::SALARY) (DECLARE (XARGS :GUARD (AND (STRINGP CUTIL::NAME) (NATP CUTIL::SALARY)) :GUARD-HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE)) (THEORY (QUOTE MINIMAL-THEORY)))) (AND STABLE-UNDER-SIMPLIFICATIONP (QUOTE (:IN-THEORY (ENABLE))))))) (MBE :LOGIC (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY) :EXEC (HONS :EMPLOYEE (HONS CUTIL::NAME CUTIL::SALARY)))) (DEFUND-INLINE CUTIL::EMPLOYEE->NAME (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::EMPLOYEE-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::EMPLOYEE-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CAR (CDR CUTIL::X))) (DEFUND-INLINE CUTIL::EMPLOYEE->SALARY (CUTIL::X) (DECLARE (XARGS :GUARD (CUTIL::EMPLOYEE-P CUTIL::X) :GUARD-HINTS (("Goal" :EXPAND (CUTIL::EMPLOYEE-P CUTIL::X) :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P (:EXECUTABLE-COUNTERPART EQLABLEP) CONSP-ASSOC-EQUAL ASSOC-EQL-EXEC-IS-ASSOC-EQUAL)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))))))) (CDR (CDR CUTIL::X))) (DEFTHM CUTIL::CONSP-OF-EMPLOYEE (CONSP (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::EMPLOYEE)))) (DEFTHM CUTIL::BOOLEANP-OF-EMPLOYEE-P (BOOLEANP (CUTIL::EMPLOYEE-P CUTIL::X)) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (ENABLE CUTIL::EMPLOYEE-P)))) (DEFTHM CUTIL::EMPLOYEE-P-OF-EMPLOYEE (IMPLIES (FORCE (AND (STRINGP CUTIL::NAME) (NATP CUTIL::SALARY))) (EQUAL (CUTIL::EMPLOYEE-P (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY)) T)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P CUTIL::EMPLOYEE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY))) :USE ((:INSTANCE CUTIL::BOOLEANP-OF-EMPLOYEE-P (CUTIL::X (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY))))))) (DEFTHM CUTIL::TAG-OF-EMPLOYEE (EQUAL (TAG (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY)) :EMPLOYEE) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::TAG-WHEN-EMPLOYEE-P (IMPLIES (CUTIL::EMPLOYEE-P CUTIL::X) (EQUAL (TAG CUTIL::X) :EMPLOYEE)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 0) (:FORWARD-CHAINING)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::EMPLOYEE-P-WHEN-WRONG-TAG (IMPLIES (NOT (EQUAL (TAG CUTIL::X) :EMPLOYEE)) (EQUAL (CUTIL::EMPLOYEE-P CUTIL::X) NIL)) :RULE-CLASSES ((:REWRITE :BACKCHAIN-LIMIT-LST 1)) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (RECORD-EXPANSION (ADD-TO-RULESET TAG-REASONING (QUOTE (CUTIL::TAG-WHEN-EMPLOYEE-P CUTIL::EMPLOYEE-P-WHEN-WRONG-TAG))) (TABLE RULESET-TABLE (QUOTE TAG-REASONING) (UNION-EQUAL (QUOTE (CUTIL::TAG-WHEN-EMPLOYEE-P CUTIL::EMPLOYEE-P-WHEN-WRONG-TAG)) (RULESET (QUOTE TAG-REASONING))))) (DEFTHM CUTIL::CONSP-WHEN-EMPLOYEE-P (IMPLIES (CUTIL::EMPLOYEE-P CUTIL::X) (CONSP CUTIL::X)) :RULE-CLASSES :COMPOUND-RECOGNIZER :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::EMPLOYEE->NAME-OF-EMPLOYEE (EQUAL (CUTIL::EMPLOYEE->NAME (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY)) CUTIL::NAME) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE->NAME CUTIL::EMPLOYEE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::EMPLOYEE->SALARY-OF-EMPLOYEE (EQUAL (CUTIL::EMPLOYEE->SALARY (CUTIL::EMPLOYEE CUTIL::NAME CUTIL::SALARY)) CUTIL::SALARY) :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE->SALARY CUTIL::EMPLOYEE)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::RETURN-TYPE-OF-EMPLOYEE->NAME (IMPLIES (FORCE (CUTIL::EMPLOYEE-P CUTIL::X)) (STRINGP (CUTIL::EMPLOYEE->NAME CUTIL::X))) :RULE-CLASSES :REWRITE :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P CUTIL::EMPLOYEE->NAME CUTIL::EMPLOYEE->SALARY)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFTHM CUTIL::RETURN-TYPE-OF-EMPLOYEE->SALARY (IMPLIES (FORCE (CUTIL::EMPLOYEE-P CUTIL::X)) (NATP (CUTIL::EMPLOYEE->SALARY CUTIL::X))) :RULE-CLASSES :TYPE-PRESCRIPTION :HINTS (("Goal" :IN-THEORY (UNION-THEORIES (QUOTE (CUTIL::EMPLOYEE-P CUTIL::EMPLOYEE->NAME CUTIL::EMPLOYEE->SALARY)) (THEORY (QUOTE CUTIL::DEFAGGREGATE-BASIC-THEORY)))))) (DEFMACRO CUTIL::PATBIND-EMPLOYEE (ARGS CUTIL::FORMS CUTIL::REST-EXPR) (CUTIL::DA-PATBIND-FN (QUOTE CUTIL::EMPLOYEE) (QUOTE (CUTIL::NAME CUTIL::SALARY)) ARGS CUTIL::FORMS CUTIL::REST-EXPR)) (DEFUN CUTIL::CHANGE-EMPLOYEE-FN (CUTIL::X CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::EMPLOYEE) (LIST (IF (ASSOC :NAME CUTIL::ALIST) (CDR (ASSOC :NAME CUTIL::ALIST)) (LIST (QUOTE CUTIL::EMPLOYEE->NAME) CUTIL::X)) (IF (ASSOC :SALARY CUTIL::ALIST) (CDR (ASSOC :SALARY CUTIL::ALIST)) (LIST (QUOTE CUTIL::EMPLOYEE->SALARY) CUTIL::X))))) (DEFMACRO CUTIL::CHANGE-EMPLOYEE (CUTIL::X &REST ARGS) (CUTIL::CHANGE-EMPLOYEE-FN CUTIL::X (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:NAME :SALARY))))) (DEFUN CUTIL::MAKE-EMPLOYEE-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::EMPLOYEE) (LIST (IF (ASSOC :NAME CUTIL::ALIST) (CDR (ASSOC :NAME CUTIL::ALIST)) (QUOTE NIL)) (IF (ASSOC :SALARY CUTIL::ALIST) (CDR (ASSOC :SALARY CUTIL::ALIST)) (QUOTE 25))))) (DEFMACRO CUTIL::MAKE-EMPLOYEE (&REST ARGS) (CUTIL::MAKE-EMPLOYEE-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:NAME :SALARY))))) (DEFUN CUTIL::MAKE-HONSED-EMPLOYEE-FN (CUTIL::ALIST) (DECLARE (XARGS :MODE :PROGRAM)) (CONS (QUOTE CUTIL::HONSED-EMPLOYEE) (LIST (IF (ASSOC :NAME CUTIL::ALIST) (CDR (ASSOC :NAME CUTIL::ALIST)) (QUOTE NIL)) (IF (ASSOC :SALARY CUTIL::ALIST) (CDR (ASSOC :SALARY CUTIL::ALIST)) (QUOTE 25))))) (DEFMACRO CUTIL::MAKE-HONSED-EMPLOYEE (&REST ARGS) (CUTIL::MAKE-HONSED-EMPLOYEE-FN (CUTIL::DA-CHANGER-ARGS-TO-ALIST ARGS (QUOTE (:NAME :SALARY))))) (WITH-OUTPUT :STACK :POP (PROGN)) (VALUE-TRIPLE (QUOTE (CUTIL::DEFAGGREGATE CUTIL::EMPLOYEE)))))) (11 RECORD-EXPANSION (ASSERT! (B* ((CUTIL::EMP (CUTIL::MAKE-EMPLOYEE :NAME "foo"))) (AND (EQUAL (CUTIL::EMPLOYEE->NAME CUTIL::EMP) "foo") (EQUAL (CUTIL::EMPLOYEE->SALARY CUTIL::EMP) 25)))) (VALUE-TRIPLE :SUCCESS)) (12 RECORD-EXPANSION (ASSERT! (B* ((CUTIL::EMP (CUTIL::MAKE-EMPLOYEE :NAME "foo")) ((CUTIL::EMPLOYEE CUTIL::EMP) CUTIL::EMP)) (AND (EQUAL CUTIL::EMP.NAME "foo") (EQUAL CUTIL::EMP.SALARY 25)))) (VALUE-TRIPLE :SUCCESS)))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/cutil/defaggregate-tests.lisp" "defaggregate-tests" "defaggregate-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1663166670) ("/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)) (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) (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))
276195646