/usr/share/acl2-6.3/books/cutil/define-tests.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (DEFINE CUTIL::FOO NIL :RETURNS (CUTIL::ANS INTEGERP) 3) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO (DEFUND CUTIL::FOO NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO))) (DECLARE (IGNORABLE __FUNCTION__)) 3)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO :FN (QUOTE CUTIL::FOO) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO))) (DECLARE (IGNORABLE __FUNCTION__)) 3)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO :FN (QUOTE CUTIL::FOO) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO))) (DECLARE (IGNORABLE __FUNCTION__)) 3)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO :FN (QUOTE CUTIL::FOO) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM CUTIL::RETURN-TYPE-OF-FOO (LET ((CUTIL::ANS (CUTIL::FOO))) (INTEGERP CUTIL::ANS)) :HINTS NIL :RULE-CLASSES :REWRITE))))))))) (VALUE-TRIPLE :INVISIBLE))) (3 RECORD-EXPANSION (DEFINE CUTIL::FOO2 NIL (MV 3 "hi")) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO2 (DEFUND CUTIL::FOO2 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO2))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO2 :FN (QUOTE CUTIL::FOO2) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO2) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO2))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO2) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO2 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO2))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO2 :FN (QUOTE CUTIL::FOO2) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO2) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO2))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO2) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO2 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO2))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO2 :FN (QUOTE CUTIL::FOO2) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO2) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO2))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO2) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))) (4 RECORD-EXPANSION (DEFINE CUTIL::FOO3 NIL (MV 3 "hi")) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO3 (DEFUND CUTIL::FOO3 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO3))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO3 :FN (QUOTE CUTIL::FOO3) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO3) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO3))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO3) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO3 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO3))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO3 :FN (QUOTE CUTIL::FOO3) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO3) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO3))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO3) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO3 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO3))) (DECLARE (IGNORABLE __FUNCTION__)) (MV 3 "hi"))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO3 :FN (QUOTE CUTIL::FOO3) :RETURNS (QUOTE NIL) :FORMALS (QUOTE NIL)) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO3) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO3))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO3) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))) (5 RECORD-EXPANSION (DEFINE CUTIL::FOO4 NIL :RETURNS (CUTIL::ANS INTEGERP) 44) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO4 (DEFUND CUTIL::FOO4 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO4))) (DECLARE (IGNORABLE __FUNCTION__)) 44)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO4 :FN (QUOTE CUTIL::FOO4) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO4) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO4))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO4) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO4 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO4))) (DECLARE (IGNORABLE __FUNCTION__)) 44)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO4 :FN (QUOTE CUTIL::FOO4) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO4) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO4))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO4) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO4 NIL (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO4))) (DECLARE (IGNORABLE __FUNCTION__)) 44)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO4 :FN (QUOTE CUTIL::FOO4) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE NIL)) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO4) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO4))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO4) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . T) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM CUTIL::RETURN-TYPE-OF-FOO4 (LET ((CUTIL::ANS (CUTIL::FOO4))) (INTEGERP CUTIL::ANS)) :HINTS NIL :RULE-CLASSES :REWRITE))))))))) (VALUE-TRIPLE :INVISIBLE))) (6 RECORD-EXPANSION (DEFINE CUTIL::FOO5 ((CUTIL::X ODDP :TYPE INTEGER)) :RETURNS (CUTIL::ANS INTEGERP :HYP :GUARD) (- CUTIL::X 1)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO5 (DEFUND CUTIL::FOO5 (CUTIL::X) (DECLARE (TYPE INTEGER CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO5))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO5 :FN (QUOTE CUTIL::FOO5) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE . INTEGER)))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO5) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO5))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO5) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO5 (CUTIL::X) (DECLARE (TYPE INTEGER CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO5))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO5 :FN (QUOTE CUTIL::FOO5) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE . INTEGER)))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO5) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO5))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO5) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO5 (CUTIL::X) (DECLARE (TYPE INTEGER CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO5))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO5 :FN (QUOTE CUTIL::FOO5) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE . INTEGER)))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO5) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO5))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO5) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE INTEGERP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM CUTIL::RETURN-TYPE-OF-FOO5 (IMPLIES (AND (INTEGERP CUTIL::X) (ODDP CUTIL::X)) (LET ((CUTIL::ANS (CUTIL::FOO5 CUTIL::X))) (INTEGERP CUTIL::ANS))) :HINTS NIL :RULE-CLASSES :REWRITE))))))))) (VALUE-TRIPLE :INVISIBLE))) (7 RECORD-EXPANSION (DEFINE CUTIL::FOO6 ((CUTIL::X ODDP :TYPE (INTEGER 0 *))) :RETURNS (CUTIL::ANS NATP :HYP :GUARD) (- CUTIL::X 1)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO6 (DEFUND CUTIL::FOO6 (CUTIL::X) (DECLARE (TYPE (INTEGER 0 *) CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO6))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO6 :FN (QUOTE CUTIL::FOO6) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE INTEGER 0 *)))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO6) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO6))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO6) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO6 (CUTIL::X) (DECLARE (TYPE (INTEGER 0 *) CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO6))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO6 :FN (QUOTE CUTIL::FOO6) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE INTEGER 0 *)))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO6) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO6))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO6) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO6 (CUTIL::X) (DECLARE (TYPE (INTEGER 0 *) CUTIL::X)) (DECLARE (XARGS :GUARD (ODDP CUTIL::X))) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO6))) (DECLARE (IGNORABLE __FUNCTION__)) (- CUTIL::X 1))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO6 :FN (QUOTE CUTIL::FOO6) :RETURNS (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD ODDP CUTIL::X) (DOC . "") (CUTIL::OPTS (:TYPE INTEGER 0 *)))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO6) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO6))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO6) (QUOTE ((:RETURN-SPEC (CUTIL::NAME . CUTIL::ANS) (DOC . "") (CUTIL::RETURN-TYPE NATP CUTIL::ANS) (CUTIL::HYP . :GUARD) (CUTIL::HINTS) (CUTIL::RULE-CLASSES . :REWRITE)))) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN (DEFTHM CUTIL::RETURN-TYPE-OF-FOO6 (IMPLIES (AND (IF (INTEGERP CUTIL::X) (NOT (< CUTIL::X (QUOTE 0))) (QUOTE NIL)) (ODDP CUTIL::X)) (LET ((CUTIL::ANS (CUTIL::FOO6 CUTIL::X))) (NATP CUTIL::ANS))) :HINTS NIL :RULE-CLASSES :REWRITE))))))))) (VALUE-TRIPLE :INVISIBLE))) (8 RECORD-EXPANSION (DEFINE CUTIL::FOO7 :PARENTS (CUTIL::|look ma, parents before formals, even!|) (CUTIL::X) (CONSP CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO7 :PARENTS (CUTIL::|look ma, parents before formals, even!|) (DEFUND CUTIL::FOO7 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO7))) (DECLARE (IGNORABLE __FUNCTION__)) (CONSP CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO7 :FN (QUOTE CUTIL::FOO7) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO7) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO7))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO7) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::FOO7)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO7 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO7))) (DECLARE (IGNORABLE __FUNCTION__)) (CONSP CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO7 :FN (QUOTE CUTIL::FOO7) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO7) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO7))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO7) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO7 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO7))) (DECLARE (IGNORABLE __FUNCTION__)) (CONSP CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO7 :FN (QUOTE CUTIL::FOO7) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO7) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO7))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO7) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE CUTIL::FOO7)) (XDOC::PARENTS (QUOTE (CUTIL::|look ma, parents before formals, even!|))) (XDOC::SHORT (QUOTE NIL)) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE CUTIL::FOO7))) 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 "") (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::FOO7) (:BASE-PKG . CUTIL::ACL2-PKG-WITNESS) (:PARENTS CUTIL::|look ma, parents before formals, even!|) (:SHORT) (:LONG . "

<h3>Definitions and Theorems</h3>@(def |CUTIL|::|FOO7|)") (:FROM . "[books]/cutil/define-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC CUTIL::FOO7)))))) (VALUE-TRIPLE (QUOTE CUTIL::FOO7))))) (RECORD-EXPANSION (MAKE-EVENT (B* ((CUTIL::CURRENT-PKG (F-GET-GLOBAL (QUOTE CURRENT-PACKAGE) STATE)) (CUTIL::BASE-PKG (PKG-WITNESS CUTIL::CURRENT-PKG)) (CUTIL::FNNAME (QUOTE CUTIL::FOO7)) ((MV CUTIL::STR STATE) (CUTIL::MAKE-XDOC-TOP CUTIL::FNNAME (QUOTE CUTIL::FOO7) (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)))) (QUOTE NIL) CUTIL::BASE-PKG STATE)) (EVENT (LIST (QUOTE XDOC::XDOC-PREPEND) CUTIL::FNNAME CUTIL::STR))) (VALUE EVENT))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE CUTIL::FOO7) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING:  Ignoring attempt to prepend to topic ~x0, ~
                         because no such topic is currently defined.~%" (QUOTE CUTIL::FOO7)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) "<box><dl>
<dt>Signature</dt><dt><code>(foo7 x) &rarr; *</code></dt></dl></box>
" XDOC::OLD-LONG)) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))))) (9 RECORD-EXPANSION (ENCAPSULATE NIL (LOGIC) (DEFINE CUTIL::FOO8 (CUTIL::X) :MODE :PROGRAM (+ 1 CUTIL::X))) (ENCAPSULATE NIL (LOGIC) (RECORD-EXPANSION (DEFINE CUTIL::FOO8 (CUTIL::X) :MODE :PROGRAM (+ 1 CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO8 (DEFUND CUTIL::FOO8 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO8 :FN (QUOTE CUTIL::FOO8) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO8) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO8) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO8 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO8 :FN (QUOTE CUTIL::FOO8) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO8) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO8) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO8 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO8 :FN (QUOTE CUTIL::FOO8) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO8) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO8) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (10 RECORD-EXPANSION (ENCAPSULATE NIL (LOGIC) (DEFINE CUTIL::FOO9 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 2 CUTIL::X))) (ENCAPSULATE NIL (LOGIC) (RECORD-EXPANSION (DEFINE CUTIL::FOO9 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 2 CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO9 (DEFUND CUTIL::FOO9 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO9 :FN (QUOTE CUTIL::FOO9) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO9) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO9) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO9 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO9 :FN (QUOTE CUTIL::FOO9) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO9) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO9) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO9 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO9 :FN (QUOTE CUTIL::FOO9) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO9) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO9) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (11 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::FOO10 ((CUTIL::X NATP)) (DECLARE (XARGS :MODE :LOGIC)) (+ 2 CUTIL::X))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::FOO10 ((CUTIL::X NATP)) (DECLARE (XARGS :MODE :LOGIC)) (+ 2 CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO10 (DEFUND CUTIL::FOO10 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO10 :FN (QUOTE CUTIL::FOO10) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO10) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO10) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO10 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO10 :FN (QUOTE CUTIL::FOO10) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO10) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO10) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO10 (CUTIL::X) (DECLARE (XARGS :GUARD (NATP CUTIL::X))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO10 :FN (QUOTE CUTIL::FOO10) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO10) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO10) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (12 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::FOO11 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 3 CUTIL::X))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::FOO11 (CUTIL::X) (DECLARE (XARGS :MODE :PROGRAM)) (+ 3 CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO11 (DEFUND CUTIL::FOO11 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO11 :FN (QUOTE CUTIL::FOO11) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO11) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO11) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO11 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO11 :FN (QUOTE CUTIL::FOO11) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO11) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO11) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO11 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO11 :FN (QUOTE CUTIL::FOO11) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO11) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO11) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (13 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::FOO12 (CUTIL::X) :MODE :PROGRAM (+ 3 CUTIL::X))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::FOO12 (CUTIL::X) :MODE :PROGRAM (+ 3 CUTIL::X)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::FOO12 (DEFUND CUTIL::FOO12 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO12 :FN (QUOTE CUTIL::FOO12) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO12) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO12) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO12 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO12 :FN (QUOTE CUTIL::FOO12) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO12) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO12) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND CUTIL::FOO12 (CUTIL::X) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::FOO12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X))) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::FOO12 :FN (QUOTE CUTIL::FOO12) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::FOO12) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::FOO12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::FOO12) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (14 RECORD-EXPANSION (ENCAPSULATE NIL (LOGIC) (DEFINE CUTIL::BAR8 (CUTIL::X &OPTIONAL CUTIL::Y) :MODE :PROGRAM (+ 1 CUTIL::X CUTIL::Y))) (ENCAPSULATE NIL (LOGIC) (RECORD-EXPANSION (DEFINE CUTIL::BAR8 (CUTIL::X &OPTIONAL CUTIL::Y) :MODE :PROGRAM (+ 1 CUTIL::X CUTIL::Y)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::BAR8 (DEFMACRO CUTIL::BAR8 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR8-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR8-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR8 CUTIL::BAR8-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR8-FN) (QUOTE CUTIL::BAR8)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR8 :FN (QUOTE CUTIL::BAR8-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR8-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR8-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR8 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR8-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR8-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR8 CUTIL::BAR8-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR8-FN) (QUOTE CUTIL::BAR8)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR8 :FN (QUOTE CUTIL::BAR8-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR8-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR8-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR8 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR8-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR8-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR8))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 1 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR8 CUTIL::BAR8-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR8-FN) (QUOTE CUTIL::BAR8)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR8 :FN (QUOTE CUTIL::BAR8-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR8-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR8))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR8-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (15 RECORD-EXPANSION (ENCAPSULATE NIL (LOGIC) (DEFINE CUTIL::BAR9 (CUTIL::X &OPTIONAL CUTIL::Y) (DECLARE (XARGS :MODE :PROGRAM)) (+ 2 CUTIL::X CUTIL::Y))) (ENCAPSULATE NIL (LOGIC) (RECORD-EXPANSION (DEFINE CUTIL::BAR9 (CUTIL::X &OPTIONAL CUTIL::Y) (DECLARE (XARGS :MODE :PROGRAM)) (+ 2 CUTIL::X CUTIL::Y)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::BAR9 (DEFMACRO CUTIL::BAR9 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR9-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR9-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR9 CUTIL::BAR9-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR9-FN) (QUOTE CUTIL::BAR9)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR9 :FN (QUOTE CUTIL::BAR9-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR9-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR9-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR9 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR9-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR9-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR9 CUTIL::BAR9-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR9-FN) (QUOTE CUTIL::BAR9)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR9 :FN (QUOTE CUTIL::BAR9-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR9-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR9-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR9 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR9-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR9-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR9))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR9 CUTIL::BAR9-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR9-FN) (QUOTE CUTIL::BAR9)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR9 :FN (QUOTE CUTIL::BAR9-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (RECORD-EXPANSION (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR9-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR9))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (LOCAL (VALUE-TRIPLE :ELIDED))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR9-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (16 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::BAR10 ((CUTIL::X NATP) &OPTIONAL (CUTIL::Y NATP)) (DECLARE (XARGS :MODE :LOGIC)) (+ 2 CUTIL::X CUTIL::Y))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::BAR10 ((CUTIL::X NATP) &OPTIONAL (CUTIL::Y NATP)) (DECLARE (XARGS :MODE :LOGIC)) (+ 2 CUTIL::X CUTIL::Y)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::BAR10 (DEFMACRO CUTIL::BAR10 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR10-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR10-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD (AND (NATP CUTIL::X) (NATP CUTIL::Y)))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR10 CUTIL::BAR10-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR10-FN) (QUOTE CUTIL::BAR10)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR10 :FN (QUOTE CUTIL::BAR10-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD NATP CUTIL::Y) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR10-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR10-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR10 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR10-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR10-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD (AND (NATP CUTIL::X) (NATP CUTIL::Y)))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR10 CUTIL::BAR10-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR10-FN) (QUOTE CUTIL::BAR10)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR10 :FN (QUOTE CUTIL::BAR10-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD NATP CUTIL::Y) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR10-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR10-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR10 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR10-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR10-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD (AND (NATP CUTIL::X) (NATP CUTIL::Y)))) (DECLARE (XARGS :MODE :LOGIC)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR10))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 2 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR10 CUTIL::BAR10-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR10-FN) (QUOTE CUTIL::BAR10)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR10 :FN (QUOTE CUTIL::BAR10-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD NATP CUTIL::X) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD NATP CUTIL::Y) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR10-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR10))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR10-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (17 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::BAR11 (CUTIL::X &OPTIONAL CUTIL::Y) (DECLARE (XARGS :MODE :PROGRAM)) (+ 3 CUTIL::X CUTIL::Y))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::BAR11 (CUTIL::X &OPTIONAL CUTIL::Y) (DECLARE (XARGS :MODE :PROGRAM)) (+ 3 CUTIL::X CUTIL::Y)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::BAR11 (DEFMACRO CUTIL::BAR11 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR11-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR11-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR11 CUTIL::BAR11-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR11-FN) (QUOTE CUTIL::BAR11)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR11 :FN (QUOTE CUTIL::BAR11-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR11-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR11-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR11 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR11-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR11-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR11 CUTIL::BAR11-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR11-FN) (QUOTE CUTIL::BAR11)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR11 :FN (QUOTE CUTIL::BAR11-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR11-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR11-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR11 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR11-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR11-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR11))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR11 CUTIL::BAR11-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR11-FN) (QUOTE CUTIL::BAR11)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR11 :FN (QUOTE CUTIL::BAR11-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR11-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR11))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR11-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))) (18 RECORD-EXPANSION (ENCAPSULATE NIL (PROGRAM) (DEFINE CUTIL::BAR12 (CUTIL::X &OPTIONAL CUTIL::Y) :MODE :PROGRAM (+ 3 CUTIL::X CUTIL::Y))) (ENCAPSULATE NIL (PROGRAM) (RECORD-EXPANSION (DEFINE CUTIL::BAR12 (CUTIL::X &OPTIONAL CUTIL::Y) :MODE :PROGRAM (+ 3 CUTIL::X CUTIL::Y)) (PROGN (RECORD-EXPANSION (DEFSECTION CUTIL::BAR12 (DEFMACRO CUTIL::BAR12 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR12-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR12-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR12 CUTIL::BAR12-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR12-FN) (QUOTE CUTIL::BAR12)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR12 :FN (QUOTE CUTIL::BAR12-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR12-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR12-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR12 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR12-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR12-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR12 CUTIL::BAR12-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR12-FN) (QUOTE CUTIL::BAR12)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR12 :FN (QUOTE CUTIL::BAR12-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR12-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR12-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFMACRO CUTIL::BAR12 (CUTIL::X &OPTIONAL CUTIL::Y) (LIST (QUOTE CUTIL::BAR12-FN) CUTIL::X CUTIL::Y)) (DEFUND CUTIL::BAR12-FN (CUTIL::X CUTIL::Y) (DECLARE (XARGS :GUARD T)) (DECLARE (XARGS :MODE :PROGRAM)) (LET ((__FUNCTION__ (QUOTE CUTIL::BAR12))) (DECLARE (IGNORABLE __FUNCTION__)) (+ 3 CUTIL::X CUTIL::Y))) (ADD-MACRO-ALIAS CUTIL::BAR12 CUTIL::BAR12-FN) (TABLE CUTIL::DEFINE-MACRO-FNS (QUOTE CUTIL::BAR12-FN) (QUOTE CUTIL::BAR12)) (CUTIL::EXTEND-DEFINE-TABLE CUTIL::BAR12 :FN (QUOTE CUTIL::BAR12-FN) :RETURNS (QUOTE NIL) :FORMALS (QUOTE ((:FORMAL (CUTIL::NAME . CUTIL::X) (GUARD . T) (DOC . "") (CUTIL::OPTS)) (:FORMAL (CUTIL::NAME . CUTIL::Y) (GUARD . T) (DOC . "") (CUTIL::OPTS))))) (LOCAL (MAKE-EVENT (IF (CUTIL::LOGIC-MODE-P (QUOTE CUTIL::BAR12-FN) (W STATE)) (QUOTE (IN-THEORY (ENABLE CUTIL::BAR12))) (QUOTE (VALUE-TRIPLE :INVISIBLE))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((WORLD (W STATE)) (CUTIL::EVENTS (CUTIL::RETURNSPEC-THMS (QUOTE CUTIL::BAR12-FN) (QUOTE NIL) WORLD))) (VALUE (CONS (QUOTE PROGN) CUTIL::EVENTS)))) (PROGN)))))))) (VALUE-TRIPLE :INVISIBLE))))))
(("/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/define-tests.lisp" "define-tests" "define-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1809954125) ("/usr/share/acl2-6.3/books/cutil/define.lisp" "define" "define" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1768331178) ("/usr/share/acl2-6.3/books/str/cat.lisp" "str/cat" "cat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1576295912) ("/usr/share/acl2-6.3/books/str/ieqv.lisp" "ieqv" "ieqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 620245362) ("/usr/share/acl2-6.3/books/std/lists/list-defuns.lisp" "std/lists/list-defuns" "list-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 321177760) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sublistp.lisp" "sublistp" "sublistp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1635583873)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top-with-meta.lisp" "arithmetic/top-with-meta" "top-with-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 349005499)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta.lisp" "meta/meta" "meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1434715577)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-times-equal.lisp" "meta-times-equal" "meta-times-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2078846479)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/equalities.lisp" "arithmetic/equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 597034595)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-lessp.lisp" "meta-plus-lessp" "meta-plus-lessp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 932651372)) (LOCAL ("/usr/share/acl2-6.3/books/meta/meta-plus-equal.lisp" "meta-plus-equal" "meta-plus-equal" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948431900)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-lemmas.lisp" "term-lemmas" "term-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 304413851)) (LOCAL ("/usr/share/acl2-6.3/books/meta/term-defuns.lisp" "term-defuns" "term-defuns" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1038247295)) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/same-lengthp.lisp" "same-lengthp" "same-lengthp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2063823673)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/sets.lisp" "sets" "sets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 878261262)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/mfc-utils.lisp" "mfc-utils" "mfc-utils" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1043482843)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/rcons.lisp" "rcons" "rcons" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 105042482)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/prefixp.lisp" "prefixp" "prefixp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 689235789)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/final-cdr.lisp" "final-cdr" "final-cdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 96013958)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/duplicity.lisp" "duplicity" "duplicity" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 914433854)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/flatten.lisp" "flatten" "flatten" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1125138266)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) ("/usr/share/acl2-6.3/books/tools/rulesets.lisp" "tools/rulesets" "rulesets" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 639683473) ("/usr/share/acl2-6.3/books/str/char-case.lisp" "char-case" "char-case" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2059343298) ("/usr/share/acl2-6.3/books/str/eqv.lisp" "eqv" "eqv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1920438599) (LOCAL ("/usr/share/acl2-6.3/books/str/arithmetic.lisp" "arithmetic" "arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 216355320)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/repeat.lisp" "std/lists/repeat" "repeat" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293545519)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/nthcdr.lisp" "std/lists/nthcdr" "nthcdr" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1415704060)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/len.lisp" "std/lists/len" "len" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 963137114)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "std/lists/take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/std/lists/rev.lisp" "std/lists/rev" "rev" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 327117871) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/revappend.lisp" "revappend" "revappend" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1368863429)) ("/usr/share/acl2-6.3/books/std/lists/equiv.lisp" "std/lists/equiv" "equiv" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1948483556) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/take.lisp" "take" "take" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1496833916)) ("/usr/share/acl2-6.3/books/str/coerce.lisp" "coerce" "coerce" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1053051260) ("/usr/share/acl2-6.3/books/str/make-character-list.lisp" "make-character-list" "make-character-list" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1622566814) (LOCAL ("/usr/share/acl2-6.3/books/std/lists/append.lisp" "std/lists/append" "append" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 567759210)) ("/usr/share/acl2-6.3/books/std/lists/list-fix.lisp" "list-fix" "list-fix" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1844974260) (LOCAL ("/usr/share/acl2-6.3/books/arithmetic/top.lisp" "arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 956305966)) (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/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/tools/mv-nth.lisp" "tools/mv-nth" "mv-nth" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82993140) ("/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/returnspecs.lisp" "returnspecs" "returnspecs" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 722876511) ("/usr/share/acl2-6.3/books/cutil/formals.lisp" "formals" "formals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 606017704) ("/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/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/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))
764647143
acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / cutil / define-tests.cert
