mac:~$ cd talks/seminar-2009-10-28/ mac:~/talks/seminar-2009-10-28$ lt total 72 -rw-r--r-- 1 kaufmann staff 11400 Oct 27 20:47 enabledp-change.lisp -rw-r--r-- 1 kaufmann staff 1719 Oct 27 20:47 abstract.txt -rw-r--r-- 1 kaufmann staff 5749 Oct 27 20:47 talk.txt -rw-r--r-- 1 kaufmann staff 92 Oct 27 20:47 h.lisp -rw-r--r-- 1 kaufmann staff 257 Oct 27 20:48 enabledp-change.cert -rw-r--r-- 1 kaufmann staff 216 Oct 27 20:48 h.cert mac:~/talks/seminar-2009-10-28$ cd ~/acl2h-e4/e4/ mac:~/acl2h-e4/e4$ cd ~/acl2/v3-6-1/acl2-sources/ mac:~/acl2/v3-6-1/acl2-sources$ wc *.lisp 300 1810 13274 acl2-check.lisp 1186 5158 48101 acl2-fns.lisp 1359 5961 53828 acl2-init.lisp 3 12 75 acl2-proclaims.lisp 1840 9118 71409 acl2.lisp 1 0 1 acl2r.lisp 235 884 8799 akcl-acl2-trace.lisp 261 1252 10168 allegro-acl2-trace.lisp 37844 190343 1502366 axioms.lisp 13037 68666 539954 basis.lisp 4028 20120 168206 bdd.lisp 473 2360 26668 defpkgs.lisp 13808 74284 623494 defthm.lisp 9126 48328 403258 defuns.lisp 20072 106482 869042 history-management.lisp 8943 30107 314661 hons-raw.lisp 1209 6342 47268 hons.lisp 3145 17774 137905 induct.lisp 87 536 3602 init.lisp 5867 30159 256701 interface-raw.lisp 21658 126391 945049 ld.lisp 3649 21591 154334 linear-a.lisp 893 3848 38283 linear-b.lisp 119 781 5354 mcl-acl2-startup.lisp 981 3715 42323 non-linear.lisp 222 970 8880 openmcl-acl2-trace.lisp 24041 121045 1063341 other-events.lisp 2725 14606 122356 other-processes.lisp 2131 11587 89079 parallel-raw.lisp 1255 6553 50257 parallel.lisp 1633 6366 66731 proof-checker-a.lisp 7095 32669 293818 proof-checker-b.lisp 29 202 1230 proof-checker-pkg.lisp 7541 39454 335133 prove.lisp 16563 88147 727353 rewrite.lisp 7163 39375 316665 simplify.lisp 87 557 3302 sum-list-example.lisp 6453 32755 285914 translate.lisp 3535 19869 139822 tutorial.lisp 864 2878 38605 type-set-a.lisp 10837 58801 486050 type-set-b.lisp 242298 1251856 10312659 total mac:~/acl2/v3-6-1/acl2-sources$ acl2-3.6.1 Welcome to Clozure Common Lisp Version 1.3-r11936 (DarwinX8664)! ACL2 Version 3.6.1 built September 7, 2009 10:14:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/acl2/v3-6-1/acl2-sources/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>state ACL2 !>(assign foo (+ 3 4)) 7 ACL2 !>(@ foo) 7 ACL2 !>Bye. mac:~/acl2/v3-6-1/acl2-sources$ acl2-3.6.1 Welcome to Clozure Common Lisp Version 1.3-r11936 (DarwinX8664)! ACL2 Version 3.6.1 built September 7, 2009 10:14:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/acl2/v3-6-1/acl2-sources/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defun fact (n) (if (zp n) 1 (* n (fact (1- n))))) The admission of FACT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT N). We observe that the type of FACT is described by the theorem (AND (INTEGERP (FACT N)) (< 0 (FACT N))). We used the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Summary Form: ( DEFUN FACT ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.01, other: 0.03) FACT ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) (EVENT-LANDMARK GLOBAL-VALUE 6462 ...) (FACT ABSOLUTE-EVENT-NUMBER . 6462) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5936 (:LOGIC DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) :(= a) (walkabout= A) is (COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) :q ACL2 !>(walkabout= A) (COMMAND-LANDMARK GLOBAL-VALUE 5936 (:LOGIC DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) ACL2 !>(cddr (walkabout= A)) (5936 (:LOGIC DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) (EVENT-LANDMARK GLOBAL-VALUE 6462 ...) (FACT ABSOLUTE-EVENT-NUMBER . 6462) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6462 ...) :q ACL2 !>(set-iprint t) ACL2 Observation in SET-IPRINT: Iprinting has been enabled. ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5936 . #@1#) (EVENT-LANDMARK GLOBAL-VALUE 6462 . #@2#) (FACT ABSOLUTE-EVENT-NUMBER . 6462) . #@3#) :q ACL2 !>(without-evisc '((COMMAND-LANDMARK GLOBAL-VALUE 5936 . #@1#) (EVENT-LANDMARK GLOBAL-VALUE 6462 . #@2#) (FACT ABSOLUTE-EVENT-NUMBER . 6462) . nil)) ((COMMAND-LANDMARK GLOBAL-VALUE 5936 (:LOGIC DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) (EVENT-LANDMARK GLOBAL-VALUE 6462 (DEFUN FACT . :IDEAL) DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N))))) (FACT ABSOLUTE-EVENT-NUMBER . 6462)) ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5936 . #@4#) (EVENT-LANDMARK GLOBAL-VALUE 6462 . #@5#) (FACT ABSOLUTE-EVENT-NUMBER . 6462) . #@6#) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5936 . #@7#) :nx (EVENT-LANDMARK GLOBAL-VALUE 6462 . #@8#) :q ACL2 !>(defun k (x) x) Since K is non-recursive, its admission is trivial. We observe that the type of K is described by the theorem (EQUAL (K X) X). Summary Form: ( DEFUN K ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) K ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN FACT (N) ...) L 2:x(DEFUN K (X) ...) ACL2 !>(defmacro abc (&rest x) `(defun ,@x)) Summary Form: ( DEFMACRO ABC ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) ABC ACL2 !>(abc fn (a b) (list a b)) Since FN is non-recursive, its admission is trivial. We observe that the type of FN is described by the theorem (AND (CONSP (FN A B)) (TRUE-LISTP (FN A B))). We used primitive type reasoning. Summary Form: ( DEFUN FN ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FN ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN FACT (N) ...) L 2 (DEFUN K (X) ...) 3 (DEFMACRO ABC (&REST X) ...) L 4:x(ABC FN (A B) ...) ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5939 . #@9#) (EVENT-LANDMARK GLOBAL-VALUE 6465 . #@10#) (FN ABSOLUTE-EVENT-NUMBER . 6465) . #@11#) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5939 . #@12#) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5939 (:LOGIC ABC FN (A B) (LIST A B))) :nx (EVENT-LANDMARK GLOBAL-VALUE 6465 . #@13#) :pp (EVENT-LANDMARK GLOBAL-VALUE 6465 (DEFUN FN . :IDEAL) DEFUN FN (A B) (LIST A B)) :0 ((COMMAND-LANDMARK GLOBAL-VALUE 5939 . #@14#) (EVENT-LANDMARK GLOBAL-VALUE 6465 . #@15#) (FN ABSOLUTE-EVENT-NUMBER . 6465) . #@16#) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5939 . #@17#) :nx (EVENT-LANDMARK GLOBAL-VALUE 6465 . #@18#) :q ACL2 !>(set-iprint nil) ACL2 Observation in SET-IPRINT: Iprinting has been disabled. ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) (FN ABSOLUTE-EVENT-NUMBER . 6465) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) :nx (FN ABSOLUTE-EVENT-NUMBER . 6465) :nx (CLTL-COMMAND GLOBAL-VALUE DEFUNS ...) :nx (FN COARSENINGS . NIL) :nx (FN CONGRUENCES) :nx (FN PRIMITIVE-RECURSIVE-DEFUNP . T) :nx (FN LEVEL-NO . 0) :nx (FN TYPE-PRESCRIPTIONS (512 # NIL ...)) :pp (FN TYPE-PRESCRIPTIONS (512 (2105 FN A B) NIL (NIL :TYPE-PRESCRIPTION FN) IF (CONSP (FN A B)) (TRUE-LISTP (FN A B)) 'NIL)) :nx (FN TYPE-PRESCRIPTIONS (512 # NIL ...)) :nx (FN TYPE-PRESCRIPTIONS (0 # NIL ...)) :nx (FN DEF-BODIES (# NIL # ...)) :nx (FN LEMMAS (REWRITE-RULE # 2103 ...)) :nx (FN UNNORMALIZED-BODY CONS ...) :nx (FN RUNIC-MAPPING-PAIRS (2103 :DEFINITION FN) ...) :nx (FN STOBJS-OUT NIL) :nx (FN STOBJS-IN NIL ...) :nx (FN FORMALS A ...) :nx (FN SYMBOL-CLASS . :IDEAL) :nx (COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5938 (:LOGIC DEFMACRO ABC (&REST X) (CONS 'DEFUN (APPEND X 'NIL)))) :nx (EVENT-LANDMARK GLOBAL-VALUE 6464 ...) :pp (EVENT-LANDMARK GLOBAL-VALUE 6464 DEFMACRO ABC (&REST X) (CONS 'DEFUN (APPEND X 'NIL))) :nx (ABC ABSOLUTE-EVENT-NUMBER . 6464) :nx (CLTL-COMMAND GLOBAL-VALUE DEFMACRO ...) :nx (ABC MACRO-ARGS &REST ...) :nx (ABC MACRO-BODY CONS ...) :nx (COMMAND-LANDMARK GLOBAL-VALUE 5937 ...) :q ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN FACT (N) ...) L 2 (DEFUN K (X) ...) 3 (DEFMACRO ABC (&REST X) ...) L 4:x(ABC FN (A B) ...) ACL2 !>:ubu 1 ACL2 Query (:UBU): The command (DEFMACRO ABC (&REST X) (CONS 'DEFUN (APPEND X #))) introduced the :program name ABC. Do you wish to re-execute this command after the :UBU? (Y, N, Y!, N!, Q or ?): n! L 1:x(DEFUN FACT (N) ...) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1:x(DEFUN FACT (N) ...) ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) (EVENT-LANDMARK GLOBAL-VALUE 6462 ...) (FACT ABSOLUTE-EVENT-NUMBER . 6462) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6462 ...) :pp (EVENT-LANDMARK GLOBAL-VALUE 6462 (DEFUN FACT . :IDEAL) DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N))))) :nx (FACT ABSOLUTE-EVENT-NUMBER . 6462) :nx (CLTL-COMMAND GLOBAL-VALUE DEFUNS ...) :pp (CLTL-COMMAND GLOBAL-VALUE DEFUNS :LOGIC NIL (FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) :nx (FACT COARSENINGS) :nx (FACT CONGRUENCES) :nx (FACT PRIMITIVE-RECURSIVE-DEFUNP . T) :nx (FACT LEVEL-NO . 1) :nx (FACT TYPE-PRESCRIPTIONS (2 # NIL ...)) :nx (FACT TYPE-PRESCRIPTIONS (2 # NIL ...)) :nx (FACT TYPE-PRESCRIPTIONS (0 # NIL ...)) :nx (FACT DEF-BODIES (# # # ...)) :pp (FACT DEF-BODIES ((2096 NIL IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) (FACT) (N) (:DEFINITION FACT) (FACT T))) :nx (FACT LEMMAS (REWRITE-RULE # 2096 ...)) :pp (FACT LEMMAS (REWRITE-RULE (:DEFINITION FACT) 2096 NIL EQUAL (FACT N) (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) DEFINITION ((FACT) (FACT T)) NIL T)) :nx (FACT UNNORMALIZED-BODY IF ...) :nx (FACT RUNIC-MAPPING-PAIRS (2096 :DEFINITION FACT) ...) :nx (FACT QUICK-BLOCK-INFO SELF-REFLEXIVE) :nx (FACT JUSTIFICATION JUSTIFICATION ...) :nx (FACT INDUCTION-MACHINE (TESTS-AND-CALLS #) ...) :nx (FACT RECURSIVEP FACT) :bk (FACT INDUCTION-MACHINE (TESTS-AND-CALLS #) ...) :pp (FACT INDUCTION-MACHINE (TESTS-AND-CALLS ((ZP N))) (TESTS-AND-CALLS ((NOT (ZP N))) (FACT (BINARY-+ '-1 N)))) :nx (FACT RECURSIVEP FACT) :nx (FACT STOBJS-OUT NIL) :nx (FACT STOBJS-IN NIL) :nx (FACT FORMALS N) :nx (FACT SYMBOL-CLASS . :IDEAL) :nx (COMMAND-LANDMARK GLOBAL-VALUE 5935 ...) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5935 (:LOGIC EXIT-BOOT-STRAP-MODE)) :q ACL2 !>(reset-prehistory) Summary Form: ( RESET-PREHISTORY NIL) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :NEW-PREHISTORY-SET ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5937 ...) (EVENT-LANDMARK GLOBAL-VALUE 6463 ...) (COMMAND-NUMBER-BASELINE-INFO GLOBAL-VALUE COMMAND-NUMBER-BASELINE-INFO ...) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5937 ...) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5937 (:LOGIC RESET-PREHISTORY)) :nx (EVENT-LANDMARK GLOBAL-VALUE 6463 ...) :pp (EVENT-LANDMARK GLOBAL-VALUE 6463 (RESET-PREHISTORY 0) RESET-PREHISTORY) :nx (COMMAND-NUMBER-BASELINE-INFO GLOBAL-VALUE COMMAND-NUMBER-BASELINE-INFO ...) :pp (COMMAND-NUMBER-BASELINE-INFO GLOBAL-VALUE COMMAND-NUMBER-BASELINE-INFO 5937 NIL . 5935) :nx (COMMAND-LANDMARK GLOBAL-VALUE 5936 ...) :pp (COMMAND-LANDMARK GLOBAL-VALUE 5936 (:LOGIC DEFUN FACT (N) (IF (ZP N) 1 (* N (FACT (1- N)))))) :q ACL2 !>(getprop 'COMMAND-NUMBER-BASELINE-INFO 'GLOBAL-VALUE nil 'current-acl2-world (w state)) (COMMAND-NUMBER-BASELINE-INFO 5937 NIL . 5935) ACL2 !>:props fact ACL2 Properties of FACT: ABSOLUTE-EVENT-NUMBER 6462 COARSENINGS NIL CONGRUENCES NIL DEF-BODIES (((2096 NIL IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) (FACT) (N) (:DEFINITION FACT) (FACT T))) FORMALS (N) INDUCTION-MACHINE ((TESTS-AND-CALLS ((ZP N))) (TESTS-AND-CALLS ((NOT (ZP N))) (FACT (BINARY-+ '-1 N)))) JUSTIFICATION (JUSTIFICATION (N) (NIL O-P . O<) ((ACL2-COUNT N) EC-CALL PROG2$)) LEMMAS ((REWRITE-RULE (:DEFINITION FACT) 2096 NIL EQUAL (FACT N) (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) DEFINITION ((FACT) (FACT T)) NIL T)) LEVEL-NO 1 PRIMITIVE-RECURSIVE-DEFUNP T QUICK-BLOCK-INFO (SELF-REFLEXIVE) RECURSIVEP (FACT) RUNIC-MAPPING-PAIRS ((2096 :DEFINITION FACT) (2097 :EXECUTABLE-COUNTERPART FACT) (2098 :TYPE-PRESCRIPTION FACT) (2099 :INDUCTION FACT)) STOBJS-IN (NIL) STOBJS-OUT (NIL) SYMBOL-CLASS :IDEAL TYPE-PRESCRIPTIONS ((2 (2098 FACT N) NIL (NIL :TYPE-PRESCRIPTION FACT) IF (INTEGERP (FACT N)) (< '0 (FACT N)) 'NIL)) UNNORMALIZED-BODY (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) ACL2 !>(global-val 'command-number-baseline (w state)) HARD ACL2 ERROR in GETPROP: No property was found under symbol COMMAND-NUMBER-BASELINE for key GLOBAL-VALUE. GLOBAL-VAL didn't find a value. Initialize this symbol in PRIMORDIAL-WORLD-GLOBALS. ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print- gv, see :DOC trace, and see :DOC wet. ACL2 !>(global-val 'command-number-baseline-info (w state)) (COMMAND-NUMBER-BASELINE-INFO 5937 NIL . 5935) ACL2 !>(deflabel foo) Summary Form: ( DEFLABEL FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) (EVENT-LANDMARK GLOBAL-VALUE 6464 ...) (FOO ABSOLUTE-EVENT-NUMBER . 6464) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6464 ...) :nx (FOO ABSOLUTE-EVENT-NUMBER . 6464) :nx (FOO LABEL . T) :q ACL2 !>(getprop 'fact 'lemmas nil 'current-acl2-world (w state)) ((REWRITE-RULE (:DEFINITION FACT) 2096 NIL EQUAL (FACT N) (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) DEFINITION ((FACT) (FACT T)) NIL T)) ACL2 !>(defthm fact-lemma (equal (fact 0) 1)) Q.E.D. Summary Form: ( DEFTHM FACT-LEMMA ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT-LEMMA ACL2 !>(getprop 'fact 'lemmas nil 'current-acl2-world (w state)) ((REWRITE-RULE (:REWRITE FACT-LEMMA) 2100 NIL EQUAL (FACT '0) '1 ABBREVIATION NIL NIL NIL) (REWRITE-RULE (:DEFINITION FACT) 2096 NIL EQUAL (FACT N) (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) DEFINITION ((FACT) (FACT T)) NIL T)) ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) (FACT-LEMMA ABSOLUTE-EVENT-NUMBER . 6465) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) :nx (FACT-LEMMA ABSOLUTE-EVENT-NUMBER . 6465) :nx (FACT-LEMMA RUNIC-MAPPING-PAIRS (2100 :REWRITE FACT-LEMMA)) :nx (FACT-LEMMA THEOREM EQUAL ...) :nx (FACT-LEMMA UNTRANSLATED-THEOREM EQUAL ...) :nx (FACT-LEMMA CLASSES (:REWRITE)) :nx (FACT LEMMAS (REWRITE-RULE # 2100 ...) ...) :nx (COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) :bk (FACT LEMMAS (REWRITE-RULE # 2100 ...) ...) :q ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) (FACT-LEMMA ABSOLUTE-EVENT-NUMBER . 6465) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5939 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6465 ...) :nx (FACT-LEMMA ABSOLUTE-EVENT-NUMBER . 6465) :nx (FACT-LEMMA RUNIC-MAPPING-PAIRS (2100 :REWRITE FACT-LEMMA)) :nx (FACT-LEMMA THEOREM EQUAL ...) :nx (FACT-LEMMA UNTRANSLATED-THEOREM EQUAL ...) :nx (FACT-LEMMA CLASSES (:REWRITE)) :nx (FACT LEMMAS (REWRITE-RULE # 2100 ...) ...) :pp (FACT LEMMAS (REWRITE-RULE (:REWRITE FACT-LEMMA) 2100 NIL EQUAL (FACT '0) '1 ABBREVIATION NIL NIL NIL) (REWRITE-RULE (:DEFINITION FACT) 2096 NIL EQUAL (FACT N) (IF (ZP N) '1 (BINARY-* N (FACT (BINARY-+ '-1 N)))) DEFINITION ((FACT) (FACT T)) NIL T)) :q ACL2 !>state ACL2 !>(length (w state)) 72391 ACL2 !>(length (w state)) 72391 ACL2 !>state ACL2 !>(w state) ACL2 !>(trace$ w) Unhandled exception 10 at 0x19bda, context->regs at #xb029ae90 ? for help [272] Clozure CL kernel debugger: k mac:~/acl2/v3-6-1/acl2-sources$ acl2 Welcome to Clozure Common Lisp Version 1.4-dev-r12679M-trunk (DarwinX8664)! ACL2 Version 3.6.1 built October 15, 2009 06:54:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/devel/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/acl2/v3-6-1/acl2-sources/". Distributed books directory "/Users/kaufmann/acl2/devel/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(ens state) ((2101 (:HEADER :DIMENSIONS (2500) :MAXIMUM-LENGTH 2501 :DEFAULT NIL :NAME ENABLED-ARRAY-0 :ORDER NIL) (2101 :TYPE-PRESCRIPTION HONSP-CHECK) (2100 :EXECUTABLE-COUNTERPART HONSP-CHECK) (2099 :DEFINITION HONSP-CHECK) (2098 :TYPE-PRESCRIPTION NUMBER-SUBTREES) (2097 :EXECUTABLE-COUNTERPART NUMBER-SUBTREES) (2096 :DEFINITION NUMBER-SUBTREES) (2095 :INDUCTION FASTER-CONS-SUBTREES) (2094 :TYPE-PRESCRIPTION FASTER-CONS-SUBTREES) (2093 :EXECUTABLE-COUNTERPART FASTER-CONS-SUBTREES) (2092 :DEFINITION FASTER-CONS-SUBTREES) (2091 :INDUCTION CONS-SUBTREES) (2090 :TYPE-PRESCRIPTION CONS-SUBTREES) (2089 :EXECUTABLE-COUNTERPART CONS-SUBTREES) (2088 :DEFINITION CONS-SUBTREES) (2087 :INDUCTION HONS-SHRINK-ALIST) (2086 :TYPE-PRESCRIPTION HONS-SHRINK-ALIST) (2085 :EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST) (2084 :DEFINITION HONS-SHRINK-ALIST) (2083 :INDUCTION HONS-SHRINK-ALIST!) (2082 :TYPE-PRESCRIPTION HONS-SHRINK-ALIST!) (2081 :EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST!) (2080 :DEFINITION HONS-SHRINK-ALIST!) (2079 :TYPE-PRESCRIPTION MEMOIZE-OFF) (2078 :EXECUTABLE-COUNTERPART MEMOIZE-OFF) (2077 :DEFINITION MEMOIZE-OFF) (2076 :TYPE-PRESCRIPTION MEMOIZE-ON) (2075 :EXECUTABLE-COUNTERPART MEMOIZE-ON) (2074 :DEFINITION MEMOIZE-ON) (2073 :TYPE-PRESCRIPTION MEMOIZE-FORM) (2072 :EXECUTABLE-COUNTERPART MEMOIZE-FORM) (2071 :DEFINITION MEMOIZE-FORM) (2070 :TYPE-PRESCRIPTION HONS-ENABLEDP) (2069 :EXECUTABLE-COUNTERPART HONS-ENABLEDP) (2068 :DEFINITION HONS-ENABLEDP) (2067 :TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLES) (2066 :EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLES) (2065 :DEFINITION CLEAR-MEMOIZE-TABLES) (2064 :TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLE) (2063 :EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLE) (2062 :DEFINITION CLEAR-MEMOIZE-TABLE) (2061 :TYPE-PRESCRIPTION FLUSH-HONS-GET-HASH-TABLE-LINK) (2060 :EXECUTABLE-COUNTERPART FLUSH-HONS-GET-HASH-TABLE-LINK) (2059 :DEFINITION FLUSH-HONS-GET-HASH-TABLE-LINK) (2058 :TYPE-PRESCRIPTION FAST-ALIST-LEN) (2057 :EXECUTABLE-COUNTERPART FAST-ALIST-LEN) (2056 :DEFINITION FAST-ALIST-LEN) (2055 :INDUCTION FAST-ALIST-LEN-ACC) (2054 :TYPE-PRESCRIPTION FAST-ALIST-LEN-ACC) (2053 :EXECUTABLE-COUNTERPART FAST-ALIST-LEN-ACC) (2052 :DEFINITION FAST-ALIST-LEN-ACC) (2051 :TYPE-PRESCRIPTION HONS-ACONS!) (2050 :EXECUTABLE-COUNTERPART HONS-ACONS!) (2049 :DEFINITION HONS-ACONS!) (2048 :TYPE-PRESCRIPTION HONS-ACONS) (2047 :EXECUTABLE-COUNTERPART HONS-ACONS) (2046 :DEFINITION HONS-ACONS) (2045 :TYPE-PRESCRIPTION HONS-GET-FN-DO-NOT-HOPY) (2044 :EXECUTABLE-COUNTERPART HONS-GET-FN-DO-NOT-HOPY) (2043 :DEFINITION HONS-GET-FN-DO-NOT-HOPY) (2042 :TYPE-PRESCRIPTION HONS-GET-FN-DO-HOPY) (2041 :EXECUTABLE-COUNTERPART HONS-GET-FN-DO-HOPY) (2040 :DEFINITION HONS-GET-FN-DO-HOPY) (2039 :INDUCTION HONS-ASSOC-EQUAL) (2038 :TYPE-PRESCRIPTION HONS-ASSOC-EQUAL) (2037 :EXECUTABLE-COUNTERPART HONS-ASSOC-EQUAL) (2036 :DEFINITION HONS-ASSOC-EQUAL) (2035 :TYPE-PRESCRIPTION HONS-COPY) (2034 :EXECUTABLE-COUNTERPART HONS-COPY) (2033 :DEFINITION HONS-COPY) (2032 :TYPE-PRESCRIPTION HONS-EQUAL) (2031 :EXECUTABLE-COUNTERPART HONS-EQUAL) (2030 :DEFINITION HONS-EQUAL) (2029 :TYPE-PRESCRIPTION HONS) (2028 :EXECUTABLE-COUNTERPART HONS) (2027 :DEFINITION HONS) (2026 :TYPE-PRESCRIPTION CLEAR-HASH-TABLES) (2025 :EXECUTABLE-COUNTERPART CLEAR-HASH-TABLES) (2024 :DEFINITION CLEAR-HASH-TABLES) (2023 :TYPE-PRESCRIPTION TIME$-LOGIC) (2022 :EXECUTABLE-COUNTERPART TIME$-LOGIC) (2021 :DEFINITION TIME$-LOGIC) (2020 :TYPE-PRESCRIPTION CPU-CORE-COUNT) (2019 :EXECUTABLE-COUNTERPART CPU-CORE-COUNT) (2018 :DEFINITION CPU-CORE-COUNT) (2017 :TYPE-PRESCRIPTION SEARCH-FN) (2016 :EXECUTABLE-COUNTERPART SEARCH-FN) (2015 :DEFINITION SEARCH-FN) (2014 :INDUCTION SEARCH-FROM-END) (2013 :TYPE-PRESCRIPTION SEARCH-FROM-END) (2012 :EXECUTABLE-COUNTERPART SEARCH-FROM-END) (2011 :DEFINITION SEARCH-FROM-END) (2010 :INDUCTION SEARCH-FROM-START) (2009 :TYPE-PRESCRIPTION SEARCH-FROM-START) (2008 :EXECUTABLE-COUNTERPART SEARCH-FROM-START) (2007 :DEFINITION SEARCH-FROM-START) (2006 :TYPE-PRESCRIPTION SEARCH-FN-GUARD) (2005 :EXECUTABLE-COUNTERPART SEARCH-FN-GUARD) (2004 :DEFINITION SEARCH-FN-GUARD) (2003 :INDUCTION SPLICE-KEYWORD-ALIST) (2002 :TYPE-PRESCRIPTION SPLICE-KEYWORD-ALIST) (2001 :EXECUTABLE-COUNTERPART SPLICE-KEYWORD-ALIST) (2000 :DEFINITION SPLICE-KEYWORD-ALIST) (1999 :TYPE-PRESCRIPTION CLAUSES-RESULT) (1998 :EXECUTABLE-COUNTERPART CLAUSES-RESULT) (1997 :DEFINITION CLAUSES-RESULT) (1996 :TYPE-PRESCRIPTION CONJOIN-CLAUSES) (1995 :EXECUTABLE-COUNTERPART CONJOIN-CLAUSES) (1994 :DEFINITION CONJOIN-CLAUSES) (1993 :INDUCTION DISJOIN-LST) (1992 :TYPE-PRESCRIPTION DISJOIN-LST) (1991 :EXECUTABLE-COUNTERPART DISJOIN-LST) (1990 :DEFINITION DISJOIN-LST) (1989 :INDUCTION DISJOIN) (1988 :TYPE-PRESCRIPTION DISJOIN) (1987 :EXECUTABLE-COUNTERPART DISJOIN) (1986 :DEFINITION DISJOIN) (1985 :TYPE-PRESCRIPTION DISJOIN2) (1984 :EXECUTABLE-COUNTERPART DISJOIN2) (1983 :DEFINITION DISJOIN2) (1982 :INDUCTION CONJOIN) (1981 :TYPE-PRESCRIPTION CONJOIN) (1980 :EXECUTABLE-COUNTERPART CONJOIN) (1979 :DEFINITION CONJOIN) (1978 :TYPE-PRESCRIPTION CONJOIN2) (1977 :EXECUTABLE-COUNTERPART CONJOIN2) (1976 :DEFINITION CONJOIN2) (1975 :TYPE-PRESCRIPTION MOD-EXPT) (1974 :EXECUTABLE-COUNTERPART MOD-EXPT) (1973 :DEFINITION MOD-EXPT) (1972 :INDUCTION E/D-FN) (1971 :TYPE-PRESCRIPTION E/D-FN) (1970 :EXECUTABLE-COUNTERPART E/D-FN) (1969 :DEFINITION E/D-FN) (1968 :INDUCTION RESIZE-LIST) (1967 :TYPE-PRESCRIPTION RESIZE-LIST) (1966 :EXECUTABLE-COUNTERPART RESIZE-LIST) (1965 :DEFINITION RESIZE-LIST) (1964 :INDUCTION MERGE-SORT-LEXORDER) (1963 :TYPE-PRESCRIPTION MERGE-SORT-LEXORDER) (1962 :EXECUTABLE-COUNTERPART MERGE-SORT-LEXORDER) (1961 :DEFINITION MERGE-SORT-LEXORDER) (1960 :TYPE-PRESCRIPTION TRUE-LISTP-MERGE-SORT-LEXORDER) (1959 :INDUCTION MERGE-LEXORDER) (1958 :TYPE-PRESCRIPTION MERGE-LEXORDER) (1957 :EXECUTABLE-COUNTERPART MERGE-LEXORDER) (1956 :DEFINITION MERGE-LEXORDER) (1955 :FORWARD-CHAINING LEXORDER-TOTAL) (1954 :REWRITE LEXORDER-TRANSITIVE) (1953 :FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC) (1952 :REWRITE LEXORDER-REFLEXIVE) (1951 :FORWARD-CHAINING ALPHORDER-TOTAL) (1950 :FORWARD-CHAINING ALPHORDER-ANTI-SYMMETRIC) (1949 :REWRITE ALPHORDER-TRANSITIVE) (1948 :REWRITE ALPHORDER-REFLEXIVE) (1946 :TYPE-PRESCRIPTION LEXORDER) (1945 :EXECUTABLE-COUNTERPART LEXORDER) (1943 :TYPE-PRESCRIPTION ALPHORDER) (1942 :EXECUTABLE-COUNTERPART ALPHORDER) (1940 :REWRITE BAD-ATOM<=-TRANSITIVE) (1939 :TYPE-PRESCRIPTION BOOLEANP-BAD-ATOM<=) (1938 :COMPOUND-RECOGNIZER BAD-ATOM-COMPOUND-RECOGNIZER) (1937 :TYPE-PRESCRIPTION BAD-ATOM) (1936 :EXECUTABLE-COUNTERPART BAD-ATOM) (1934 :REWRITE TYPE-ALISTP-MFC-TYPE-ALIST) (1933 :REWRITE PSEUDO-TERM-LISTP-MFC-CLAUSE) (1932 :TYPE-PRESCRIPTION MFC-ANCESTORS) (1931 :EXECUTABLE-COUNTERPART MFC-ANCESTORS) (1930 :DEFINITION MFC-ANCESTORS) (1929 :TYPE-PRESCRIPTION MFC-TYPE-ALIST) (1928 :EXECUTABLE-COUNTERPART MFC-TYPE-ALIST) (1927 :DEFINITION MFC-TYPE-ALIST) (1926 :INDUCTION TYPE-ALISTP) (1925 :TYPE-PRESCRIPTION TYPE-ALISTP) (1924 :EXECUTABLE-COUNTERPART TYPE-ALISTP) (1923 :DEFINITION TYPE-ALISTP) (1922 :TYPE-PRESCRIPTION TYPE-ALIST-ENTRYP) (1921 :EXECUTABLE-COUNTERPART TYPE-ALIST-ENTRYP) (1920 :DEFINITION TYPE-ALIST-ENTRYP) (1919 :TYPE-PRESCRIPTION MFC-RDEPTH) (1918 :EXECUTABLE-COUNTERPART MFC-RDEPTH) (1917 :DEFINITION MFC-RDEPTH) (1916 :TYPE-PRESCRIPTION MFC-CLAUSE) (1915 :EXECUTABLE-COUNTERPART MFC-CLAUSE) (1914 :DEFINITION MFC-CLAUSE) (1913 :TYPE-PRESCRIPTION RECORD-ACCESSOR-FUNCTION-NAME) (1912 :EXECUTABLE-COUNTERPART RECORD-ACCESSOR-FUNCTION-NAME) (1911 :DEFINITION RECORD-ACCESSOR-FUNCTION-NAME) (1910 :TYPE-PRESCRIPTION RECORD-ERROR) (1909 :EXECUTABLE-COUNTERPART RECORD-ERROR) (1908 :DEFINITION RECORD-ERROR) (1907 :TYPE-PRESCRIPTION SET-EQUALP-EQUAL) (1906 :EXECUTABLE-COUNTERPART SET-EQUALP-EQUAL) (1905 :DEFINITION SET-EQUALP-EQUAL) (1904 :TYPE-PRESCRIPTION ODDS) (1903 :EXECUTABLE-COUNTERPART ODDS) (1902 :DEFINITION ODDS) (1901 :INDUCTION EVENS) (1900 :TYPE-PRESCRIPTION EVENS) (1899 :EXECUTABLE-COUNTERPART EVENS) (1898 :DEFINITION EVENS) (1897 :INDUCTION INTERSECTION-EQ) (1896 :TYPE-PRESCRIPTION INTERSECTION-EQ) (1895 :EXECUTABLE-COUNTERPART INTERSECTION-EQ) (1894 :DEFINITION INTERSECTION-EQ) (1893 :TYPE-PRESCRIPTION ADD-TO-SET-EQUAL) (1892 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQUAL) (1891 :DEFINITION ADD-TO-SET-EQUAL) (1890 :INDUCTION DUPLICATES) (1889 :TYPE-PRESCRIPTION DUPLICATES) (1888 :EXECUTABLE-COUNTERPART DUPLICATES) (1887 :DEFINITION DUPLICATES) (1886 :INDUCTION PAIRLIS2) (1885 :TYPE-PRESCRIPTION PAIRLIS2) (1884 :EXECUTABLE-COUNTERPART PAIRLIS2) (1883 :DEFINITION PAIRLIS2) (1882 :TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW!) (1881 :EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW!) (1880 :DEFINITION FMT-TO-COMMENT-WINDOW!) (1879 :TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW) (1878 :EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW) (1877 :DEFINITION FMT-TO-COMMENT-WINDOW) (1876 :TYPE-PRESCRIPTION ABORT!) (1873 :TYPE-PRESCRIPTION WORMHOLE-P) (1872 :EXECUTABLE-COUNTERPART WORMHOLE-P) (1871 :DEFINITION WORMHOLE-P) (1870 :TYPE-PRESCRIPTION WORMHOLE1) (1869 :EXECUTABLE-COUNTERPART WORMHOLE1) (1868 :DEFINITION WORMHOLE1) (1867 :TYPE-PRESCRIPTION TIME-LIMIT4-REACHED-P) (1866 :EXECUTABLE-COUNTERPART TIME-LIMIT4-REACHED-P) (1865 :DEFINITION TIME-LIMIT4-REACHED-P) (1864 :TYPE-PRESCRIPTION WITH-PROVER-TIME-LIMIT) (1863 :EXECUTABLE-COUNTERPART WITH-PROVER-TIME-LIMIT) (1862 :DEFINITION WITH-PROVER-TIME-LIMIT) (1861 :TYPE-PRESCRIPTION DOUBLE-REWRITE) (1860 :EXECUTABLE-COUNTERPART DOUBLE-REWRITE) (1859 :DEFINITION DOUBLE-REWRITE) (1858 :REWRITE DEFAULT-SYMBOL-PACKAGE-NAME) (1857 :REWRITE DEFAULT-SYMBOL-NAME) (1856 :REWRITE DEFAULT-REALPART) (1855 :REWRITE DEFAULT-NUMERATOR) (1854 :REWRITE DEFAULT-IMAGPART) (1853 :REWRITE DEFAULT-DENOMINATOR) (1852 :REWRITE DEFAULT-COERCE-3) (1851 :REWRITE DEFAULT-COERCE-2) (1850 :REWRITE MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST) (1849 :REWRITE DEFAULT-COERCE-1) (1848 :REWRITE IMAGPART-+) (1847 :REWRITE REALPART-+) (1846 :REWRITE COMPLEX-0) (1845 :REWRITE DEFAULT-COMPLEX-2) (1844 :REWRITE DEFAULT-COMPLEX-1) (1843 :REWRITE DEFAULT-CHAR-CODE) (1842 :REWRITE CONS-CAR-CDR) (1841 :REWRITE DEFAULT-CDR) (1840 :REWRITE DEFAULT-CAR) (1839 :REWRITE DEFAULT-<-2) (1838 :REWRITE DEFAULT-<-1) (1837 :REWRITE DEFAULT-UNARY-/) (1836 :REWRITE DEFAULT-UNARY-MINUS) (1835 :REWRITE DEFAULT-*-2) (1834 :REWRITE DEFAULT-*-1) (1833 :REWRITE DEFAULT-+-2) (1832 :REWRITE DEFAULT-+-1) (1831 :FORWARD-CHAINING BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP) (1830 :FORWARD-CHAINING BOOLEAN-LISTP-FORWARD) (1829 :REWRITE BOOLEAN-LISTP-CONS) (1828 :INDUCTION BOOLEAN-LISTP) (1827 :TYPE-PRESCRIPTION BOOLEAN-LISTP) (1826 :EXECUTABLE-COUNTERPART BOOLEAN-LISTP) (1825 :DEFINITION BOOLEAN-LISTP) (1824 :REWRITE PAIRLIS$-FIX-TRUE-LIST) (1823 :INDUCTION FIX-TRUE-LIST) (1822 :TYPE-PRESCRIPTION FIX-TRUE-LIST) (1821 :EXECUTABLE-COUNTERPART FIX-TRUE-LIST) (1820 :DEFINITION FIX-TRUE-LIST) (1819 :TYPE-PRESCRIPTION DEFAULT-HINTS) (1818 :EXECUTABLE-COUNTERPART DEFAULT-HINTS) (1817 :DEFINITION DEFAULT-HINTS) (1816 :TYPE-PRESCRIPTION NTH-ALIASES) (1815 :EXECUTABLE-COUNTERPART NTH-ALIASES) (1814 :DEFINITION NTH-ALIASES) (1813 :TYPE-PRESCRIPTION MACRO-ALIASES) (1812 :EXECUTABLE-COUNTERPART MACRO-ALIASES) (1811 :DEFINITION MACRO-ALIASES) (1810 :TYPE-PRESCRIPTION NON-LINEARP) (1809 :EXECUTABLE-COUNTERPART NON-LINEARP) (1808 :DEFINITION NON-LINEARP) (1807 :TYPE-PRESCRIPTION MATCH-FREE-OVERRIDE) (1806 :EXECUTABLE-COUNTERPART MATCH-FREE-OVERRIDE) (1805 :DEFINITION MATCH-FREE-OVERRIDE) (1804 :TYPE-PRESCRIPTION MATCH-FREE-DEFAULT) (1803 :EXECUTABLE-COUNTERPART MATCH-FREE-DEFAULT) (1802 :DEFINITION MATCH-FREE-DEFAULT) (1801 :TYPE-PRESCRIPTION BINOP-TABLE) (1800 :EXECUTABLE-COUNTERPART BINOP-TABLE) (1799 :DEFINITION BINOP-TABLE) (1798 :TYPE-PRESCRIPTION CASE-SPLIT-LIMITATIONS) (1797 :EXECUTABLE-COUNTERPART CASE-SPLIT-LIMITATIONS) (1796 :DEFINITION CASE-SPLIT-LIMITATIONS) (1795 :TYPE-PRESCRIPTION REWRITE-STACK-LIMIT) (1794 :EXECUTABLE-COUNTERPART REWRITE-STACK-LIMIT) (1793 :DEFINITION REWRITE-STACK-LIMIT) (1792 :TYPE-PRESCRIPTION DEFAULT-BACKCHAIN-LIMIT) (1791 :EXECUTABLE-COUNTERPART DEFAULT-BACKCHAIN-LIMIT) (1790 :DEFINITION DEFAULT-BACKCHAIN-LIMIT) (1789 :TYPE-PRESCRIPTION BACKCHAIN-LIMIT) (1788 :EXECUTABLE-COUNTERPART BACKCHAIN-LIMIT) (1787 :DEFINITION BACKCHAIN-LIMIT) (1786 :INDUCTION DELETE-ASSOC-EQUAL) (1785 :TYPE-PRESCRIPTION DELETE-ASSOC-EQUAL) (1784 :EXECUTABLE-COUNTERPART DELETE-ASSOC-EQUAL) (1783 :DEFINITION DELETE-ASSOC-EQUAL) (1782 :INDUCTION DELETE-ASSOC-EQ) (1781 :TYPE-PRESCRIPTION DELETE-ASSOC-EQ) (1780 :EXECUTABLE-COUNTERPART DELETE-ASSOC-EQ) (1779 :DEFINITION DELETE-ASSOC-EQ) (1778 :TYPE-PRESCRIPTION INVISIBLE-FNS-ENTRYP) (1777 :EXECUTABLE-COUNTERPART INVISIBLE-FNS-ENTRYP) (1776 :DEFINITION INVISIBLE-FNS-ENTRYP) (1775 :INDUCTION UNARY-FUNCTION-SYMBOL-LISTP) (1774 :TYPE-PRESCRIPTION UNARY-FUNCTION-SYMBOL-LISTP) (1773 :EXECUTABLE-COUNTERPART UNARY-FUNCTION-SYMBOL-LISTP) (1772 :DEFINITION UNARY-FUNCTION-SYMBOL-LISTP) (1771 :TYPE-PRESCRIPTION INVISIBLE-FNS-TABLE) (1770 :EXECUTABLE-COUNTERPART INVISIBLE-FNS-TABLE) (1769 :DEFINITION INVISIBLE-FNS-TABLE) (1768 :TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE-FROM-STATE) (1767 :EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE-FROM-STATE) (1766 :DEFINITION DEFAULT-DEFUN-MODE-FROM-STATE) (1765 :TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE) (1764 :EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE) (1763 :DEFINITION DEFAULT-DEFUN-MODE) (1762 :TYPE-PRESCRIPTION DEFAULT-WELL-FOUNDED-RELATION) (1761 :EXECUTABLE-COUNTERPART DEFAULT-WELL-FOUNDED-RELATION) (1760 :DEFINITION DEFAULT-WELL-FOUNDED-RELATION) (1759 :TYPE-PRESCRIPTION DEFAULT-MEASURE-FUNCTION) (1758 :EXECUTABLE-COUNTERPART DEFAULT-MEASURE-FUNCTION) (1757 :DEFINITION DEFAULT-MEASURE-FUNCTION) (1756 :TYPE-PRESCRIPTION DEFAULT-COMPILE-FNS) (1755 :EXECUTABLE-COUNTERPART DEFAULT-COMPILE-FNS) (1754 :DEFINITION DEFAULT-COMPILE-FNS) (1753 :TYPE-PRESCRIPTION DEFAULT-VERIFY-GUARDS-EAGERNESS) (1752 :EXECUTABLE-COUNTERPART DEFAULT-VERIFY-GUARDS-EAGERNESS) (1751 :DEFINITION DEFAULT-VERIFY-GUARDS-EAGERNESS) (1750 :TYPE-PRESCRIPTION TABLE-ALIST) (1749 :EXECUTABLE-COUNTERPART TABLE-ALIST) (1748 :DEFINITION TABLE-ALIST) (1747 :INDUCTION LEGAL-RULER-EXTENDERS-P) (1746 :TYPE-PRESCRIPTION LEGAL-RULER-EXTENDERS-P) (1745 :EXECUTABLE-COUNTERPART LEGAL-RULER-EXTENDERS-P) (1744 :DEFINITION LEGAL-RULER-EXTENDERS-P) (1743 :INDUCTION INCLUDE-BOOK-DIR-ALISTP) (1742 :TYPE-PRESCRIPTION INCLUDE-BOOK-DIR-ALISTP) (1741 :EXECUTABLE-COUNTERPART INCLUDE-BOOK-DIR-ALISTP) (1740 :DEFINITION INCLUDE-BOOK-DIR-ALISTP) (1739 :TYPE-PRESCRIPTION OS) (1738 :EXECUTABLE-COUNTERPART OS) (1737 :DEFINITION OS) (1736 :TYPE-PRESCRIPTION ABSOLUTE-PATHNAME-STRING-P) (1735 :EXECUTABLE-COUNTERPART ABSOLUTE-PATHNAME-STRING-P) (1734 :DEFINITION ABSOLUTE-PATHNAME-STRING-P) (1733 :TYPE-PRESCRIPTION NATP-POSITION-AC) (1732 :TYPE-PRESCRIPTION FREE-VAR-RUNES) (1731 :EXECUTABLE-COUNTERPART FREE-VAR-RUNES) (1730 :DEFINITION FREE-VAR-RUNES) (1729 :INDUCTION NON-FREE-VAR-RUNES) (1728 :TYPE-PRESCRIPTION NON-FREE-VAR-RUNES) (1727 :EXECUTABLE-COUNTERPART NON-FREE-VAR-RUNES) (1726 :DEFINITION NON-FREE-VAR-RUNES) (1725 :TYPE-PRESCRIPTION MAKE-VAR-LST) (1724 :EXECUTABLE-COUNTERPART MAKE-VAR-LST) (1723 :DEFINITION MAKE-VAR-LST) (1722 :INDUCTION MAKE-VAR-LST1) (1721 :TYPE-PRESCRIPTION MAKE-VAR-LST1) (1720 :EXECUTABLE-COUNTERPART MAKE-VAR-LST1) (1719 :DEFINITION MAKE-VAR-LST1) (1718 :TYPE-PRESCRIPTION LD-SKIP-PROOFSP) (1717 :EXECUTABLE-COUNTERPART LD-SKIP-PROOFSP) (1716 :DEFINITION LD-SKIP-PROOFSP) (1715 :INDUCTION UNION-EQ) (1714 :TYPE-PRESCRIPTION UNION-EQ) (1713 :EXECUTABLE-COUNTERPART UNION-EQ) (1712 :DEFINITION UNION-EQ) (1711 :TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL) (1710 :REWRITE STATE-P1-UPDATE-NTH-2-WORLD) (1709 :TYPE-PRESCRIPTION KNOWN-PACKAGE-ALIST) (1708 :EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALIST) (1707 :DEFINITION KNOWN-PACKAGE-ALIST) (1706 :TYPE-PRESCRIPTION CURRENT-PACKAGE) (1705 :EXECUTABLE-COUNTERPART CURRENT-PACKAGE) (1704 :DEFINITION CURRENT-PACKAGE) (1703 :TYPE-PRESCRIPTION W) (1702 :EXECUTABLE-COUNTERPART W) (1701 :DEFINITION W) (1700 :TYPE-PRESCRIPTION PRIN1$) (1699 :EXECUTABLE-COUNTERPART PRIN1$) (1698 :DEFINITION PRIN1$) (1697 :TYPE-PRESCRIPTION PRINT-TIMER) (1696 :EXECUTABLE-COUNTERPART PRINT-TIMER) (1695 :DEFINITION PRINT-TIMER) (1694 :TYPE-PRESCRIPTION PRINT-RATIONAL-AS-DECIMAL) (1693 :EXECUTABLE-COUNTERPART PRINT-RATIONAL-AS-DECIMAL) (1692 :DEFINITION PRINT-RATIONAL-AS-DECIMAL) (1691 :TYPE-PRESCRIPTION INCREMENT-TIMER) (1690 :EXECUTABLE-COUNTERPART INCREMENT-TIMER) (1689 :DEFINITION INCREMENT-TIMER) (1688 :FORWARD-CHAINING STATE-P1-UPDATE-MAIN-TIMER) (1687 :REWRITE ADD-PAIR-PRESERVES-ALL-BOUNDP) (1686 :REWRITE ASSOC-ADD-PAIR) (1685 :FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD) (1684 :TYPE-PRESCRIPTION MAIN-TIMER-TYPE-PRESCRIPTION) (1683 :REWRITE NTH-ADD1) (1682 :REWRITE NTH-0-CONS) (1681 :TYPE-PRESCRIPTION ADD-TIMERS) (1680 :EXECUTABLE-COUNTERPART ADD-TIMERS) (1679 :DEFINITION ADD-TIMERS) (1678 :TYPE-PRESCRIPTION POP-TIMER) (1677 :EXECUTABLE-COUNTERPART POP-TIMER) (1676 :DEFINITION POP-TIMER) (1675 :REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP) (1674 :REWRITE RATIONALP-UNARY-/) (1673 :REWRITE RATIONALP-UNARY--) (1672 :REWRITE RATIONALP-*) (1671 :REWRITE RATIONALP-+) (1670 :TYPE-PRESCRIPTION PUSH-TIMER) (1669 :EXECUTABLE-COUNTERPART PUSH-TIMER) (1668 :DEFINITION PUSH-TIMER) (1667 :TYPE-PRESCRIPTION GET-TIMER) (1666 :EXECUTABLE-COUNTERPART GET-TIMER) (1665 :DEFINITION GET-TIMER) (1664 :TYPE-PRESCRIPTION SET-TIMER) (1663 :EXECUTABLE-COUNTERPART SET-TIMER) (1662 :DEFINITION SET-TIMER) (1661 :INDUCTION PUT-ASSOC-EQUAL) (1660 :TYPE-PRESCRIPTION PUT-ASSOC-EQUAL) (1659 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQUAL) (1658 :DEFINITION PUT-ASSOC-EQUAL) (1657 :INDUCTION PUT-ASSOC-EQL) (1656 :TYPE-PRESCRIPTION PUT-ASSOC-EQL) (1655 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQL) (1654 :DEFINITION PUT-ASSOC-EQL) (1653 :INDUCTION PUT-ASSOC-EQ) (1652 :TYPE-PRESCRIPTION PUT-ASSOC-EQ) (1651 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQ) (1650 :DEFINITION PUT-ASSOC-EQ) (1649 :TYPE-PRESCRIPTION MAIN-TIMER) (1648 :EXECUTABLE-COUNTERPART MAIN-TIMER) (1647 :DEFINITION MAIN-TIMER) (1646 :TYPE-PRESCRIPTION NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION) (1645 :FORWARD-CHAINING READ-ACL2-ORACLE-PRESERVES-STATE-P1) (1644 :FORWARD-CHAINING READ-RUN-TIME-PRESERVES-STATE-P1) (1643 :REWRITE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1) (1642 :REWRITE LEN-UPDATE-NTH) (1639 :TYPE-PRESCRIPTION RANDOM$) (1638 :EXECUTABLE-COUNTERPART RANDOM$) (1636 :TYPE-PRESCRIPTION SETENV$) (1635 :EXECUTABLE-COUNTERPART SETENV$) (1634 :DEFINITION SETENV$) (1633 :TYPE-PRESCRIPTION GETENV$) (1632 :EXECUTABLE-COUNTERPART GETENV$) (1631 :DEFINITION GETENV$) (1630 :TYPE-PRESCRIPTION READ-ACL2-ORACLE) (1629 :EXECUTABLE-COUNTERPART READ-ACL2-ORACLE) (1627 :TYPE-PRESCRIPTION READ-RUN-TIME) (1626 :EXECUTABLE-COUNTERPART READ-RUN-TIME) (1624 :TYPE-PRESCRIPTION READ-IDATE) (1623 :EXECUTABLE-COUNTERPART READ-IDATE) (1622 :DEFINITION READ-IDATE) (1621 :INDUCTION POWER-EVAL) (1620 :TYPE-PRESCRIPTION POWER-EVAL) (1619 :EXECUTABLE-COUNTERPART POWER-EVAL) (1618 :DEFINITION POWER-EVAL) (1617 :TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST) (1616 :EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST) (1615 :DEFINITION UPDATE-USER-STOBJ-ALIST) (1614 :TYPE-PRESCRIPTION USER-STOBJ-ALIST) (1613 :EXECUTABLE-COUNTERPART USER-STOBJ-ALIST) (1612 :DEFINITION USER-STOBJ-ALIST) (1611 :TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES) (1610 :EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES) (1609 :DEFINITION LIST-ALL-PACKAGE-NAMES) (1608 :TYPE-PRESCRIPTION DECREMENT-BIG-CLOCK) (1607 :EXECUTABLE-COUNTERPART DECREMENT-BIG-CLOCK) (1606 :DEFINITION DECREMENT-BIG-CLOCK) (1605 :TYPE-PRESCRIPTION BIG-CLOCK-NEGATIVE-P) (1604 :EXECUTABLE-COUNTERPART BIG-CLOCK-NEGATIVE-P) (1603 :DEFINITION BIG-CLOCK-NEGATIVE-P) (1602 :TYPE-PRESCRIPTION ASET-32-BIT-INTEGER-STACK) (1601 :EXECUTABLE-COUNTERPART ASET-32-BIT-INTEGER-STACK) (1600 :DEFINITION ASET-32-BIT-INTEGER-STACK) (1599 :TYPE-PRESCRIPTION AREF-32-BIT-INTEGER-STACK) (1598 :EXECUTABLE-COUNTERPART AREF-32-BIT-INTEGER-STACK) (1597 :DEFINITION AREF-32-BIT-INTEGER-STACK) (1596 :TYPE-PRESCRIPTION SHRINK-32-BIT-INTEGER-STACK) (1595 :EXECUTABLE-COUNTERPART SHRINK-32-BIT-INTEGER-STACK) (1594 :DEFINITION SHRINK-32-BIT-INTEGER-STACK) (1593 :TYPE-PRESCRIPTION EXTEND-32-BIT-INTEGER-STACK) (1592 :EXECUTABLE-COUNTERPART EXTEND-32-BIT-INTEGER-STACK) (1591 :DEFINITION EXTEND-32-BIT-INTEGER-STACK) (1590 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH) (1589 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH) (1588 :DEFINITION 32-BIT-INTEGER-STACK-LENGTH) (1587 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH1) (1586 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH1) (1585 :DEFINITION 32-BIT-INTEGER-STACK-LENGTH1) (1584 :TYPE-PRESCRIPTION ASET-T-STACK) (1583 :EXECUTABLE-COUNTERPART ASET-T-STACK) (1582 :DEFINITION ASET-T-STACK) (1581 :TYPE-PRESCRIPTION AREF-T-STACK) (1580 :EXECUTABLE-COUNTERPART AREF-T-STACK) (1579 :DEFINITION AREF-T-STACK) (1578 :TYPE-PRESCRIPTION SHRINK-T-STACK) (1577 :EXECUTABLE-COUNTERPART SHRINK-T-STACK) (1576 :DEFINITION SHRINK-T-STACK) (1575 :TYPE-PRESCRIPTION SUBSEQ) (1574 :EXECUTABLE-COUNTERPART SUBSEQ) (1573 :DEFINITION SUBSEQ) (1572 :TYPE-PRESCRIPTION SUBSEQ-LIST) (1571 :EXECUTABLE-COUNTERPART SUBSEQ-LIST) (1570 :DEFINITION SUBSEQ-LIST) (1569 :TYPE-PRESCRIPTION EXTEND-T-STACK) (1568 :EXECUTABLE-COUNTERPART EXTEND-T-STACK) (1567 :DEFINITION EXTEND-T-STACK) (1566 :INDUCTION MAKE-LIST-AC) (1565 :TYPE-PRESCRIPTION MAKE-LIST-AC) (1564 :EXECUTABLE-COUNTERPART MAKE-LIST-AC) (1563 :DEFINITION MAKE-LIST-AC) (1562 :TYPE-PRESCRIPTION T-STACK-LENGTH) (1561 :EXECUTABLE-COUNTERPART T-STACK-LENGTH) (1560 :DEFINITION T-STACK-LENGTH) (1559 :TYPE-PRESCRIPTION T-STACK-LENGTH1) (1558 :EXECUTABLE-COUNTERPART T-STACK-LENGTH1) (1557 :DEFINITION T-STACK-LENGTH1) (1556 :TYPE-PRESCRIPTION NEEDS-SLASHES) (1555 :EXECUTABLE-COUNTERPART NEEDS-SLASHES) (1554 :DEFINITION NEEDS-SLASHES) (1553 :TYPE-PRESCRIPTION MAY-NEED-SLASHES-FN) (1552 :EXECUTABLE-COUNTERPART MAY-NEED-SLASHES-FN) (1551 :DEFINITION MAY-NEED-SLASHES-FN) (1550 :INDUCTION MAY-NEED-SLASHES1) (1549 :TYPE-PRESCRIPTION MAY-NEED-SLASHES1) (1548 :EXECUTABLE-COUNTERPART MAY-NEED-SLASHES1) (1547 :DEFINITION MAY-NEED-SLASHES1) (1546 :TYPE-PRESCRIPTION PRIN1-WITH-SLASHES) (1545 :EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES) (1544 :DEFINITION PRIN1-WITH-SLASHES) (1543 :INDUCTION PRIN1-WITH-SLASHES1) (1542 :TYPE-PRESCRIPTION PRIN1-WITH-SLASHES1) (1541 :EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES1) (1540 :DEFINITION PRIN1-WITH-SLASHES1) (1539 :INDUCTION SOME-SLASHABLE) (1538 :TYPE-PRESCRIPTION SOME-SLASHABLE) (1537 :EXECUTABLE-COUNTERPART SOME-SLASHABLE) (1536 :DEFINITION SOME-SLASHABLE) (1535 :TYPE-PRESCRIPTION READ-OBJECT) (1534 :EXECUTABLE-COUNTERPART READ-OBJECT) (1533 :DEFINITION READ-OBJECT) (1532 :TYPE-PRESCRIPTION READ-BYTE$) (1531 :EXECUTABLE-COUNTERPART READ-BYTE$) (1530 :DEFINITION READ-BYTE$) (1529 :TYPE-PRESCRIPTION PEEK-CHAR$) (1528 :EXECUTABLE-COUNTERPART PEEK-CHAR$) (1527 :DEFINITION PEEK-CHAR$) (1526 :TYPE-PRESCRIPTION READ-CHAR$) (1525 :EXECUTABLE-COUNTERPART READ-CHAR$) (1524 :DEFINITION READ-CHAR$) (1523 :TYPE-PRESCRIPTION CLOSE-OUTPUT-CHANNEL) (1522 :EXECUTABLE-COUNTERPART CLOSE-OUTPUT-CHANNEL) (1521 :DEFINITION CLOSE-OUTPUT-CHANNEL) (1520 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL!) (1519 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL!) (1518 :DEFINITION OPEN-OUTPUT-CHANNEL!) (1517 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL) (1516 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL) (1515 :DEFINITION OPEN-OUTPUT-CHANNEL) (1514 :TYPE-PRESCRIPTION CLOSE-INPUT-CHANNEL) (1513 :EXECUTABLE-COUNTERPART CLOSE-INPUT-CHANNEL) (1512 :DEFINITION CLOSE-INPUT-CHANNEL) (1511 :REWRITE NTH-UPDATE-NTH-ARRAY) (1510 :TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH) (1509 :REWRITE NTH-UPDATE-NTH) (1508 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL) (1507 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL) (1506 :DEFINITION OPEN-INPUT-CHANNEL) (1505 :TYPE-PRESCRIPTION MAKE-OUTPUT-CHANNEL) (1504 :EXECUTABLE-COUNTERPART MAKE-OUTPUT-CHANNEL) (1503 :DEFINITION MAKE-OUTPUT-CHANNEL) (1502 :TYPE-PRESCRIPTION MAKE-INPUT-CHANNEL) (1501 :EXECUTABLE-COUNTERPART MAKE-INPUT-CHANNEL) (1500 :DEFINITION MAKE-INPUT-CHANNEL) (1499 :TYPE-PRESCRIPTION PRINT-OBJECT$) (1498 :EXECUTABLE-COUNTERPART PRINT-OBJECT$) (1497 :DEFINITION PRINT-OBJECT$) (1496 :TYPE-PRESCRIPTION WRITE-BYTE$) (1495 :EXECUTABLE-COUNTERPART WRITE-BYTE$) (1494 :DEFINITION WRITE-BYTE$) (1493 :TYPE-PRESCRIPTION PRINC$) (1492 :EXECUTABLE-COUNTERPART PRINC$) (1491 :DEFINITION PRINC$) (1490 :TYPE-PRESCRIPTION SET-PRINT-RIGHT-MARGIN) (1489 :EXECUTABLE-COUNTERPART SET-PRINT-RIGHT-MARGIN) (1488 :DEFINITION SET-PRINT-RIGHT-MARGIN) (1487 :TYPE-PRESCRIPTION SET-PRINT-LINES) (1486 :EXECUTABLE-COUNTERPART SET-PRINT-LINES) (1485 :DEFINITION SET-PRINT-LINES) (1484 :TYPE-PRESCRIPTION SET-PRINT-LEVEL) (1483 :EXECUTABLE-COUNTERPART SET-PRINT-LEVEL) (1482 :DEFINITION SET-PRINT-LEVEL) (1481 :TYPE-PRESCRIPTION SET-PRINT-LENGTH) (1480 :EXECUTABLE-COUNTERPART SET-PRINT-LENGTH) (1479 :DEFINITION SET-PRINT-LENGTH) (1478 :TYPE-PRESCRIPTION CHECK-NULL-OR-NATP) (1477 :EXECUTABLE-COUNTERPART CHECK-NULL-OR-NATP) (1476 :DEFINITION CHECK-NULL-OR-NATP) (1475 :TYPE-PRESCRIPTION SET-PRINT-READABLY) (1474 :EXECUTABLE-COUNTERPART SET-PRINT-READABLY) (1473 :DEFINITION SET-PRINT-READABLY) (1472 :TYPE-PRESCRIPTION SET-PRINT-RADIX) (1471 :EXECUTABLE-COUNTERPART SET-PRINT-RADIX) (1470 :DEFINITION SET-PRINT-RADIX) (1469 :TYPE-PRESCRIPTION SET-PRINT-PRETTY) (1468 :EXECUTABLE-COUNTERPART SET-PRINT-PRETTY) (1467 :DEFINITION SET-PRINT-PRETTY) (1466 :TYPE-PRESCRIPTION SET-PRINT-ESCAPE) (1465 :EXECUTABLE-COUNTERPART SET-PRINT-ESCAPE) (1464 :DEFINITION SET-PRINT-ESCAPE) (1463 :TYPE-PRESCRIPTION SET-PRINT-CIRCLE) (1462 :EXECUTABLE-COUNTERPART SET-PRINT-CIRCLE) (1461 :DEFINITION SET-PRINT-CIRCLE) (1460 :TYPE-PRESCRIPTION SET-PRINT-BASE) (1459 :EXECUTABLE-COUNTERPART SET-PRINT-BASE) (1458 :DEFINITION SET-PRINT-BASE) (1457 :TYPE-PRESCRIPTION CHECK-PRINT-BASE) (1456 :EXECUTABLE-COUNTERPART CHECK-PRINT-BASE) (1455 :DEFINITION CHECK-PRINT-BASE) (1454 :TYPE-PRESCRIPTION SET-PRINT-CASE) (1453 :EXECUTABLE-COUNTERPART SET-PRINT-CASE) (1452 :DEFINITION SET-PRINT-CASE) (1451 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P) (1450 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P) (1449 :DEFINITION OPEN-INPUT-CHANNEL-ANY-P) (1448 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P1) (1447 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P1) (1446 :DEFINITION OPEN-INPUT-CHANNEL-ANY-P1) (1445 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P) (1444 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P) (1443 :DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P) (1442 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P1) (1441 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P1) (1440 :DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P1) (1439 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P) (1438 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P) (1437 :DEFINITION OPEN-OUTPUT-CHANNEL-P) (1436 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P) (1435 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P) (1434 :DEFINITION OPEN-INPUT-CHANNEL-P) (1433 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P1) (1432 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P1) (1431 :DEFINITION OPEN-OUTPUT-CHANNEL-P1) (1430 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P1) (1429 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P1) (1428 :DEFINITION OPEN-INPUT-CHANNEL-P1) (1427 :FORWARD-CHAINING TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P) (1426 :TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ) (1425 :INDUCTION EXPLODE-ATOM) (1424 :TYPE-PRESCRIPTION EXPLODE-ATOM) (1423 :EXECUTABLE-COUNTERPART EXPLODE-ATOM) (1422 :DEFINITION EXPLODE-ATOM) (1421 :INDUCTION EXPLODE-NONNEGATIVE-INTEGER) (1420 :TYPE-PRESCRIPTION EXPLODE-NONNEGATIVE-INTEGER) (1419 :EXECUTABLE-COUNTERPART EXPLODE-NONNEGATIVE-INTEGER) (1418 :DEFINITION EXPLODE-NONNEGATIVE-INTEGER) (1417 :TYPE-PRESCRIPTION PRINT-BASE-P) (1416 :EXECUTABLE-COUNTERPART PRINT-BASE-P) (1415 :DEFINITION PRINT-BASE-P) (1414 :TYPE-PRESCRIPTION DIGIT-TO-CHAR) (1413 :EXECUTABLE-COUNTERPART DIGIT-TO-CHAR) (1412 :DEFINITION DIGIT-TO-CHAR) (1411 :INDUCTION ALIST-DIFFERENCE-EQ) (1410 :TYPE-PRESCRIPTION ALIST-DIFFERENCE-EQ) (1409 :EXECUTABLE-COUNTERPART ALIST-DIFFERENCE-EQ) (1408 :DEFINITION ALIST-DIFFERENCE-EQ) (1407 :INDUCTION SET-FORMS-FROM-BINDINGS) (1406 :TYPE-PRESCRIPTION SET-FORMS-FROM-BINDINGS) (1405 :EXECUTABLE-COUNTERPART SET-FORMS-FROM-BINDINGS) (1404 :DEFINITION SET-FORMS-FROM-BINDINGS) (1403 :TYPE-PRESCRIPTION BOOLE$) (1402 :EXECUTABLE-COUNTERPART BOOLE$) (1401 :DEFINITION BOOLE$) (1400 :TYPE-PRESCRIPTION LOGTEST) (1399 :EXECUTABLE-COUNTERPART LOGTEST) (1398 :DEFINITION LOGTEST) (1397 :TYPE-PRESCRIPTION LOGNOR) (1396 :EXECUTABLE-COUNTERPART LOGNOR) (1395 :DEFINITION LOGNOR) (1394 :TYPE-PRESCRIPTION BINARY-LOGXOR) (1393 :EXECUTABLE-COUNTERPART BINARY-LOGXOR) (1392 :DEFINITION BINARY-LOGXOR) (1391 :TYPE-PRESCRIPTION BINARY-LOGEQV) (1390 :EXECUTABLE-COUNTERPART BINARY-LOGEQV) (1389 :DEFINITION BINARY-LOGEQV) (1388 :TYPE-PRESCRIPTION LOGANDC2) (1387 :EXECUTABLE-COUNTERPART LOGANDC2) (1386 :DEFINITION LOGANDC2) (1385 :TYPE-PRESCRIPTION LOGANDC1) (1384 :EXECUTABLE-COUNTERPART LOGANDC1) (1383 :DEFINITION LOGANDC1) (1382 :TYPE-PRESCRIPTION LOGORC2) (1381 :EXECUTABLE-COUNTERPART LOGORC2) (1380 :DEFINITION LOGORC2) (1379 :TYPE-PRESCRIPTION LOGORC1) (1378 :EXECUTABLE-COUNTERPART LOGORC1) (1377 :DEFINITION LOGORC1) (1376 :TYPE-PRESCRIPTION BINARY-LOGIOR) (1375 :EXECUTABLE-COUNTERPART BINARY-LOGIOR) (1374 :DEFINITION BINARY-LOGIOR) (1373 :TYPE-PRESCRIPTION LOGNAND) (1372 :EXECUTABLE-COUNTERPART LOGNAND) (1371 :DEFINITION LOGNAND) (1370 :INDUCTION BINARY-LOGAND) (1369 :TYPE-PRESCRIPTION BINARY-LOGAND) (1368 :EXECUTABLE-COUNTERPART BINARY-LOGAND) (1367 :DEFINITION BINARY-LOGAND) (1366 :INDUCTION INTEGER-LENGTH) (1365 :TYPE-PRESCRIPTION INTEGER-LENGTH) (1364 :EXECUTABLE-COUNTERPART INTEGER-LENGTH) (1363 :DEFINITION INTEGER-LENGTH) (1362 :REWRITE ORDERED-SYMBOL-ALISTP-GETPROPS) (1361 :REWRITE ORDERED-SYMBOL-ALISTP-ADD-PAIR) (1360 :REWRITE SYMBOL-<-IRREFLEXIVE) (1359 :REWRITE ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR) (1358 :REWRITE SYMBOL-<-TRICHOTOMY) (1357 :REWRITE STRING<-L-TRICHOTOMY) (1356 :REWRITE SYMBOL-<-TRANSITIVE) (1355 :REWRITE STRING<-L-TRANSITIVE) (1354 :REWRITE SYMBOL-<-ASYMMETRIC) (1353 :REWRITE STRING<-L-ASYMMETRIC) (1352 :TYPE-PRESCRIPTION ZPF) (1351 :EXECUTABLE-COUNTERPART ZPF) (1350 :DEFINITION ZPF) (1349 :FORWARD-CHAINING UNSIGNED-BYTE-P-FORWARD-TO-NONNEGATIVE-INTEGERP) (1348 :FORWARD-CHAINING SIGNED-BYTE-P-FORWARD-TO-INTEGERP) (1347 :FORWARD-CHAINING INTEGER-RANGE-P-FORWARD) (1346 :TYPE-PRESCRIPTION UNSIGNED-BYTE-P) (1345 :EXECUTABLE-COUNTERPART UNSIGNED-BYTE-P) (1344 :DEFINITION UNSIGNED-BYTE-P) (1343 :TYPE-PRESCRIPTION SIGNED-BYTE-P) (1342 :EXECUTABLE-COUNTERPART SIGNED-BYTE-P) (1341 :DEFINITION SIGNED-BYTE-P) (1340 :TYPE-PRESCRIPTION INTEGER-RANGE-P) (1339 :EXECUTABLE-COUNTERPART INTEGER-RANGE-P) (1338 :DEFINITION INTEGER-RANGE-P) (1337 :INDUCTION STATE-GLOBAL-LET*-CLEANUP) (1336 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-CLEANUP) (1335 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-CLEANUP) (1334 :DEFINITION STATE-GLOBAL-LET*-CLEANUP) (1333 :INDUCTION STATE-GLOBAL-LET*-PUT-GLOBALS) (1332 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-PUT-GLOBALS) (1331 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-PUT-GLOBALS) (1330 :DEFINITION STATE-GLOBAL-LET*-PUT-GLOBALS) (1329 :INDUCTION STATE-GLOBAL-LET*-GET-GLOBALS) (1328 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-GET-GLOBALS) (1327 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-GET-GLOBALS) (1326 :DEFINITION STATE-GLOBAL-LET*-GET-GLOBALS) (1325 :INDUCTION STATE-GLOBAL-LET*-BINDINGS-P) (1324 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-BINDINGS-P) (1323 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-BINDINGS-P) (1322 :DEFINITION STATE-GLOBAL-LET*-BINDINGS-P) (1321 :TYPE-PRESCRIPTION ALWAYS-BOUNDP-GLOBAL) (1320 :EXECUTABLE-COUNTERPART ALWAYS-BOUNDP-GLOBAL) (1319 :DEFINITION ALWAYS-BOUNDP-GLOBAL) (1318 :INDUCTION SYMBOL-DOUBLET-LISTP) (1317 :TYPE-PRESCRIPTION SYMBOL-DOUBLET-LISTP) (1316 :EXECUTABLE-COUNTERPART SYMBOL-DOUBLET-LISTP) (1315 :DEFINITION SYMBOL-DOUBLET-LISTP) (1314 :TYPE-PRESCRIPTION PUT-GLOBAL) (1313 :EXECUTABLE-COUNTERPART PUT-GLOBAL) (1312 :DEFINITION PUT-GLOBAL) (1311 :TYPE-PRESCRIPTION GET-GLOBAL) (1310 :EXECUTABLE-COUNTERPART GET-GLOBAL) (1309 :DEFINITION GET-GLOBAL) (1308 :TYPE-PRESCRIPTION MAKUNBOUND-GLOBAL) (1307 :EXECUTABLE-COUNTERPART MAKUNBOUND-GLOBAL) (1306 :DEFINITION MAKUNBOUND-GLOBAL) (1305 :INDUCTION DELETE-PAIR) (1304 :TYPE-PRESCRIPTION DELETE-PAIR) (1303 :EXECUTABLE-COUNTERPART DELETE-PAIR) (1302 :DEFINITION DELETE-PAIR) (1301 :TYPE-PRESCRIPTION BOUNDP-GLOBAL) (1300 :EXECUTABLE-COUNTERPART BOUNDP-GLOBAL) (1299 :DEFINITION BOUNDP-GLOBAL) (1298 :TYPE-PRESCRIPTION BOUNDP-GLOBAL1) (1297 :EXECUTABLE-COUNTERPART BOUNDP-GLOBAL1) (1296 :DEFINITION BOUNDP-GLOBAL1) (1295 :TYPE-PRESCRIPTION GLOBAL-TABLE-CARS) (1294 :EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS) (1293 :DEFINITION GLOBAL-TABLE-CARS) (1292 :TYPE-PRESCRIPTION GLOBAL-TABLE-CARS1) (1291 :EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS1) (1290 :DEFINITION GLOBAL-TABLE-CARS1) (1289 :TYPE-PRESCRIPTION COERCE-OBJECT-TO-STATE) (1288 :EXECUTABLE-COUNTERPART COERCE-OBJECT-TO-STATE) (1287 :DEFINITION COERCE-OBJECT-TO-STATE) (1286 :TYPE-PRESCRIPTION COERCE-STATE-TO-OBJECT) (1285 :EXECUTABLE-COUNTERPART COERCE-STATE-TO-OBJECT) (1284 :DEFINITION COERCE-STATE-TO-OBJECT) (1283 :TYPE-PRESCRIPTION BUILD-STATE1) (1282 :EXECUTABLE-COUNTERPART BUILD-STATE1) (1281 :DEFINITION BUILD-STATE1) (1280 :REWRITE STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (1279 :FORWARD-CHAINING STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (1278 :TYPE-PRESCRIPTION STATE-P) (1277 :EXECUTABLE-COUNTERPART STATE-P) (1276 :DEFINITION STATE-P) (1275 :FORWARD-CHAINING STATE-P1-FORWARD) (1274 :TYPE-PRESCRIPTION STATE-P1) (1273 :EXECUTABLE-COUNTERPART STATE-P1) (1271 :FORWARD-CHAINING WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP) (1270 :TYPE-PRESCRIPTION WRITEABLE-FILES-P) (1269 :EXECUTABLE-COUNTERPART WRITEABLE-FILES-P) (1268 :DEFINITION WRITEABLE-FILES-P) (1267 :FORWARD-CHAINING WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (1266 :INDUCTION WRITABLE-FILE-LISTP) (1265 :TYPE-PRESCRIPTION WRITABLE-FILE-LISTP) (1264 :EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP) (1263 :DEFINITION WRITABLE-FILE-LISTP) (1262 :FORWARD-CHAINING WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1261 :TYPE-PRESCRIPTION WRITABLE-FILE-LISTP1) (1260 :EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP1) (1259 :DEFINITION WRITABLE-FILE-LISTP1) (1258 :FORWARD-CHAINING READ-FILES-P-FORWARD-TO-READ-FILE-LISTP) (1257 :TYPE-PRESCRIPTION READ-FILES-P) (1256 :EXECUTABLE-COUNTERPART READ-FILES-P) (1255 :DEFINITION READ-FILES-P) (1254 :FORWARD-CHAINING READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (1253 :INDUCTION READ-FILE-LISTP) (1252 :TYPE-PRESCRIPTION READ-FILE-LISTP) (1251 :EXECUTABLE-COUNTERPART READ-FILE-LISTP) (1250 :DEFINITION READ-FILE-LISTP) (1249 :FORWARD-CHAINING READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1248 :TYPE-PRESCRIPTION READ-FILE-LISTP1) (1247 :EXECUTABLE-COUNTERPART READ-FILE-LISTP1) (1246 :DEFINITION READ-FILE-LISTP1) (1245 :FORWARD-CHAINING WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP) (1244 :TYPE-PRESCRIPTION WRITTEN-FILES-P) (1243 :EXECUTABLE-COUNTERPART WRITTEN-FILES-P) (1242 :DEFINITION WRITTEN-FILES-P) (1241 :FORWARD-CHAINING WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1240 :INDUCTION WRITTEN-FILE-LISTP) (1239 :TYPE-PRESCRIPTION WRITTEN-FILE-LISTP) (1238 :EXECUTABLE-COUNTERPART WRITTEN-FILE-LISTP) (1237 :DEFINITION WRITTEN-FILE-LISTP) (1236 :FORWARD-CHAINING WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1235 :TYPE-PRESCRIPTION WRITTEN-FILE) (1234 :EXECUTABLE-COUNTERPART WRITTEN-FILE) (1233 :DEFINITION WRITTEN-FILE) (1232 :FORWARD-CHAINING READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP) (1231 :TYPE-PRESCRIPTION READABLE-FILES-P) (1230 :EXECUTABLE-COUNTERPART READABLE-FILES-P) (1229 :DEFINITION READABLE-FILES-P) (1228 :FORWARD-CHAINING READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1227 :INDUCTION READABLE-FILES-LISTP) (1226 :TYPE-PRESCRIPTION READABLE-FILES-LISTP) (1225 :EXECUTABLE-COUNTERPART READABLE-FILES-LISTP) (1224 :DEFINITION READABLE-FILES-LISTP) (1223 :FORWARD-CHAINING READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1222 :TYPE-PRESCRIPTION READABLE-FILE) (1221 :EXECUTABLE-COUNTERPART READABLE-FILE) (1220 :DEFINITION READABLE-FILE) (1219 :FORWARD-CHAINING FILE-CLOCK-P-FORWARD-TO-INTEGERP) (1218 :TYPE-PRESCRIPTION FILE-CLOCK-P) (1217 :EXECUTABLE-COUNTERPART FILE-CLOCK-P) (1216 :DEFINITION FILE-CLOCK-P) (1215 :FORWARD-CHAINING OPEN-CHANNELS-P-FORWARD) (1214 :TYPE-PRESCRIPTION OPEN-CHANNELS-P) (1213 :EXECUTABLE-COUNTERPART OPEN-CHANNELS-P) (1212 :DEFINITION OPEN-CHANNELS-P) (1211 :INDUCTION OPEN-CHANNEL-LISTP) (1210 :TYPE-PRESCRIPTION OPEN-CHANNEL-LISTP) (1209 :EXECUTABLE-COUNTERPART OPEN-CHANNEL-LISTP) (1208 :DEFINITION OPEN-CHANNEL-LISTP) (1207 :FORWARD-CHAINING OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1206 :TYPE-PRESCRIPTION OPEN-CHANNEL1) (1205 :EXECUTABLE-COUNTERPART OPEN-CHANNEL1) (1204 :DEFINITION OPEN-CHANNEL1) (1203 :FORWARD-CHAINING TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP) (1202 :INDUCTION TYPED-IO-LISTP) (1201 :TYPE-PRESCRIPTION TYPED-IO-LISTP) (1200 :EXECUTABLE-COUNTERPART TYPED-IO-LISTP) (1199 :DEFINITION TYPED-IO-LISTP) (1198 :FORWARD-CHAINING TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP) (1197 :INDUCTION TIMER-ALISTP) (1196 :TYPE-PRESCRIPTION TIMER-ALISTP) (1195 :EXECUTABLE-COUNTERPART TIMER-ALISTP) (1194 :DEFINITION TIMER-ALISTP) (1193 :FORWARD-CHAINING KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1192 :INDUCTION KNOWN-PACKAGE-ALISTP) (1191 :TYPE-PRESCRIPTION KNOWN-PACKAGE-ALISTP) (1190 :EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALISTP) (1189 :DEFINITION KNOWN-PACKAGE-ALISTP) (1188 :INDUCTION ALL-BOUNDP) (1187 :TYPE-PRESCRIPTION ALL-BOUNDP) (1186 :EXECUTABLE-COUNTERPART ALL-BOUNDP) (1185 :DEFINITION ALL-BOUNDP) (1184 :TYPE-PRESCRIPTION INIT-IPRINT-AR) (1183 :EXECUTABLE-COUNTERPART INIT-IPRINT-AR) (1182 :DEFINITION INIT-IPRINT-AR) (1181 :TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST1) (1180 :EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST1) (1179 :DEFINITION UPDATE-USER-STOBJ-ALIST1) (1178 :TYPE-PRESCRIPTION USER-STOBJ-ALIST1) (1177 :EXECUTABLE-COUNTERPART USER-STOBJ-ALIST1) (1176 :DEFINITION USER-STOBJ-ALIST1) (1175 :TYPE-PRESCRIPTION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1174 :EXECUTABLE-COUNTERPART UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1173 :DEFINITION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1172 :TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES-LST) (1171 :EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES-LST) (1170 :DEFINITION LIST-ALL-PACKAGE-NAMES-LST) (1169 :TYPE-PRESCRIPTION WRITEABLE-FILES) (1168 :EXECUTABLE-COUNTERPART WRITEABLE-FILES) (1167 :DEFINITION WRITEABLE-FILES) (1166 :TYPE-PRESCRIPTION UPDATE-READ-FILES) (1165 :EXECUTABLE-COUNTERPART UPDATE-READ-FILES) (1164 :DEFINITION UPDATE-READ-FILES) (1163 :TYPE-PRESCRIPTION READ-FILES) (1162 :EXECUTABLE-COUNTERPART READ-FILES) (1161 :DEFINITION READ-FILES) (1160 :TYPE-PRESCRIPTION UPDATE-WRITTEN-FILES) (1159 :EXECUTABLE-COUNTERPART UPDATE-WRITTEN-FILES) (1158 :DEFINITION UPDATE-WRITTEN-FILES) (1157 :TYPE-PRESCRIPTION WRITTEN-FILES) (1156 :EXECUTABLE-COUNTERPART WRITTEN-FILES) (1155 :DEFINITION WRITTEN-FILES) (1154 :TYPE-PRESCRIPTION READABLE-FILES) (1153 :EXECUTABLE-COUNTERPART READABLE-FILES) (1152 :DEFINITION READABLE-FILES) (1151 :TYPE-PRESCRIPTION UPDATE-FILE-CLOCK) (1150 :EXECUTABLE-COUNTERPART UPDATE-FILE-CLOCK) (1149 :DEFINITION UPDATE-FILE-CLOCK) (1148 :TYPE-PRESCRIPTION FILE-CLOCK) (1147 :EXECUTABLE-COUNTERPART FILE-CLOCK) (1146 :DEFINITION FILE-CLOCK) (1145 :TYPE-PRESCRIPTION UPDATE-ACL2-ORACLE) (1144 :EXECUTABLE-COUNTERPART UPDATE-ACL2-ORACLE) (1142 :TYPE-PRESCRIPTION ACL2-ORACLE) (1141 :EXECUTABLE-COUNTERPART ACL2-ORACLE) (1140 :DEFINITION ACL2-ORACLE) (1139 :TYPE-PRESCRIPTION UPDATE-IDATES) (1138 :EXECUTABLE-COUNTERPART UPDATE-IDATES) (1137 :DEFINITION UPDATE-IDATES) (1136 :TYPE-PRESCRIPTION IDATES) (1135 :EXECUTABLE-COUNTERPART IDATES) (1134 :DEFINITION IDATES) (1133 :TYPE-PRESCRIPTION UPDATE-BIG-CLOCK-ENTRY) (1132 :EXECUTABLE-COUNTERPART UPDATE-BIG-CLOCK-ENTRY) (1131 :DEFINITION UPDATE-BIG-CLOCK-ENTRY) (1130 :TYPE-PRESCRIPTION BIG-CLOCK-ENTRY) (1129 :EXECUTABLE-COUNTERPART BIG-CLOCK-ENTRY) (1128 :DEFINITION BIG-CLOCK-ENTRY) (1127 :TYPE-PRESCRIPTION UPDATE-32-BIT-INTEGER-STACK) (1126 :EXECUTABLE-COUNTERPART UPDATE-32-BIT-INTEGER-STACK) (1125 :DEFINITION UPDATE-32-BIT-INTEGER-STACK) (1124 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK) (1123 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK) (1122 :DEFINITION 32-BIT-INTEGER-STACK) (1121 :TYPE-PRESCRIPTION UPDATE-T-STACK) (1120 :EXECUTABLE-COUNTERPART UPDATE-T-STACK) (1119 :DEFINITION UPDATE-T-STACK) (1118 :TYPE-PRESCRIPTION T-STACK) (1117 :EXECUTABLE-COUNTERPART T-STACK) (1116 :DEFINITION T-STACK) (1115 :TYPE-PRESCRIPTION UPDATE-GLOBAL-TABLE) (1114 :EXECUTABLE-COUNTERPART UPDATE-GLOBAL-TABLE) (1113 :DEFINITION UPDATE-GLOBAL-TABLE) (1112 :TYPE-PRESCRIPTION GLOBAL-TABLE) (1111 :EXECUTABLE-COUNTERPART GLOBAL-TABLE) (1110 :DEFINITION GLOBAL-TABLE) (1109 :TYPE-PRESCRIPTION UPDATE-OPEN-OUTPUT-CHANNELS) (1108 :EXECUTABLE-COUNTERPART UPDATE-OPEN-OUTPUT-CHANNELS) (1107 :DEFINITION UPDATE-OPEN-OUTPUT-CHANNELS) (1106 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNELS) (1105 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNELS) (1104 :DEFINITION OPEN-OUTPUT-CHANNELS) (1103 :TYPE-PRESCRIPTION UPDATE-OPEN-INPUT-CHANNELS) (1102 :EXECUTABLE-COUNTERPART UPDATE-OPEN-INPUT-CHANNELS) (1101 :DEFINITION UPDATE-OPEN-INPUT-CHANNELS) (1100 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNELS) (1099 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNELS) (1098 :DEFINITION OPEN-INPUT-CHANNELS) (1097 :FORWARD-CHAINING 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP) (1096 :INDUCTION 32-BIT-INTEGER-LISTP) (1095 :TYPE-PRESCRIPTION 32-BIT-INTEGER-LISTP) (1094 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-LISTP) (1093 :DEFINITION 32-BIT-INTEGER-LISTP) (1092 :FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP) (1091 :INDUCTION INTEGER-LISTP) (1090 :TYPE-PRESCRIPTION INTEGER-LISTP) (1089 :EXECUTABLE-COUNTERPART INTEGER-LISTP) (1088 :DEFINITION INTEGER-LISTP) (1087 :FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP) (1086 :INDUCTION RATIONAL-LISTP) (1085 :TYPE-PRESCRIPTION RATIONAL-LISTP) (1084 :EXECUTABLE-COUNTERPART RATIONAL-LISTP) (1083 :DEFINITION RATIONAL-LISTP) (1082 :FORWARD-CHAINING 32-BIT-INTEGERP-FORWARD-TO-INTEGERP) (1081 :TYPE-PRESCRIPTION 32-BIT-INTEGERP) (1080 :EXECUTABLE-COUNTERPART 32-BIT-INTEGERP) (1079 :DEFINITION 32-BIT-INTEGERP) (1078 :TYPE-PRESCRIPTION UPDATE-NTH-ARRAY) (1077 :EXECUTABLE-COUNTERPART UPDATE-NTH-ARRAY) (1076 :DEFINITION UPDATE-NTH-ARRAY) (1075 :INDUCTION UPDATE-NTH) (1074 :TYPE-PRESCRIPTION UPDATE-NTH) (1073 :EXECUTABLE-COUNTERPART UPDATE-NTH) (1072 :DEFINITION UPDATE-NTH) (1071 :INDUCTION MAKE-MV-NTHS) (1070 :TYPE-PRESCRIPTION MAKE-MV-NTHS) (1069 :EXECUTABLE-COUNTERPART MAKE-MV-NTHS) (1068 :DEFINITION MAKE-MV-NTHS) (1067 :INDUCTION MV-NTH) (1066 :TYPE-PRESCRIPTION MV-NTH) (1065 :EXECUTABLE-COUNTERPART MV-NTH) (1064 :DEFINITION MV-NTH) (1063 :INDUCTION CDRN) (1062 :TYPE-PRESCRIPTION CDRN) (1061 :EXECUTABLE-COUNTERPART CDRN) (1060 :DEFINITION CDRN) (1059 :TYPE-PRESCRIPTION FLUSH-COMPRESS) (1058 :EXECUTABLE-COUNTERPART FLUSH-COMPRESS) (1057 :DEFINITION FLUSH-COMPRESS) (1056 :TYPE-PRESCRIPTION ASET2) (1055 :EXECUTABLE-COUNTERPART ASET2) (1054 :DEFINITION ASET2) (1053 :REWRITE ARRAY2P-CONS) (1052 :TYPE-PRESCRIPTION COMPRESS2) (1051 :EXECUTABLE-COUNTERPART COMPRESS2) (1050 :DEFINITION COMPRESS2) (1049 :INDUCTION COMPRESS21) (1048 :TYPE-PRESCRIPTION COMPRESS21) (1047 :EXECUTABLE-COUNTERPART COMPRESS21) (1046 :DEFINITION COMPRESS21) (1045 :INDUCTION COMPRESS211) (1044 :TYPE-PRESCRIPTION COMPRESS211) (1043 :EXECUTABLE-COUNTERPART COMPRESS211) (1042 :DEFINITION COMPRESS211) (1041 :TYPE-PRESCRIPTION AREF2) (1040 :EXECUTABLE-COUNTERPART AREF2) (1039 :DEFINITION AREF2) (1038 :TYPE-PRESCRIPTION ASET1) (1037 :EXECUTABLE-COUNTERPART ASET1) (1036 :DEFINITION ASET1) (1035 :REWRITE ARRAY1P-CONS) (1034 :TYPE-PRESCRIPTION COMPRESS1) (1033 :EXECUTABLE-COUNTERPART COMPRESS1) (1032 :DEFINITION COMPRESS1) (1031 :TYPE-PRESCRIPTION ARRAY-ORDER) (1030 :EXECUTABLE-COUNTERPART ARRAY-ORDER) (1029 :DEFINITION ARRAY-ORDER) (1028 :INDUCTION COMPRESS11) (1027 :TYPE-PRESCRIPTION COMPRESS11) (1026 :EXECUTABLE-COUNTERPART COMPRESS11) (1025 :DEFINITION COMPRESS11) (1024 :TYPE-PRESCRIPTION AREF1) (1023 :EXECUTABLE-COUNTERPART AREF1) (1022 :DEFINITION AREF1) (1021 :TYPE-PRESCRIPTION CONSP-ASSOC) (1020 :TYPE-PRESCRIPTION DEFAULT) (1019 :EXECUTABLE-COUNTERPART DEFAULT) (1018 :DEFINITION DEFAULT) (1017 :TYPE-PRESCRIPTION MAXIMUM-LENGTH) (1016 :EXECUTABLE-COUNTERPART MAXIMUM-LENGTH) (1015 :DEFINITION MAXIMUM-LENGTH) (1014 :TYPE-PRESCRIPTION DIMENSIONS) (1013 :EXECUTABLE-COUNTERPART DIMENSIONS) (1012 :DEFINITION DIMENSIONS) (1011 :TYPE-PRESCRIPTION HEADER) (1010 :EXECUTABLE-COUNTERPART HEADER) (1009 :DEFINITION HEADER) (1008 :LINEAR ARRAY2P-LINEAR) (1007 :FORWARD-CHAINING ARRAY2P-FORWARD) (1006 :TYPE-PRESCRIPTION ARRAY2P) (1005 :EXECUTABLE-COUNTERPART ARRAY2P) (1004 :DEFINITION ARRAY2P) (1003 :INDUCTION ASSOC2) (1002 :TYPE-PRESCRIPTION ASSOC2) (1001 :EXECUTABLE-COUNTERPART ASSOC2) (1000 :DEFINITION ASSOC2) (999 :INDUCTION BOUNDED-INTEGER-ALISTP2) (998 :TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP2) (997 :EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP2) (996 :DEFINITION BOUNDED-INTEGER-ALISTP2) (995 :LINEAR ARRAY1P-LINEAR) (994 :FORWARD-CHAINING ARRAY1P-FORWARD) (993 :TYPE-PRESCRIPTION ARRAY1P) (992 :EXECUTABLE-COUNTERPART ARRAY1P) (991 :DEFINITION ARRAY1P) (990 :TYPE-PRESCRIPTION CONSP-ASSOC-EQ) (989 :FORWARD-CHAINING KEYWORD-VALUE-LISTP-ASSOC-KEYWORD) (988 :INDUCTION ASSOC-KEYWORD) (987 :TYPE-PRESCRIPTION ASSOC-KEYWORD) (986 :EXECUTABLE-COUNTERPART ASSOC-KEYWORD) (985 :DEFINITION ASSOC-KEYWORD) (984 :FORWARD-CHAINING KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP) (983 :INDUCTION KEYWORD-VALUE-LISTP) (982 :TYPE-PRESCRIPTION KEYWORD-VALUE-LISTP) (981 :EXECUTABLE-COUNTERPART KEYWORD-VALUE-LISTP) (980 :DEFINITION KEYWORD-VALUE-LISTP) (979 :FORWARD-CHAINING BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP) (978 :INDUCTION BOUNDED-INTEGER-ALISTP) (977 :TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP) (976 :EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP) (975 :DEFINITION BOUNDED-INTEGER-ALISTP) (974 :INDUCTION SET-DIFFERENCE-EQUAL) (973 :TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL) (972 :EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQUAL) (971 :DEFINITION SET-DIFFERENCE-EQUAL) (970 :TYPE-PRESCRIPTION THE-ERROR) (969 :EXECUTABLE-COUNTERPART THE-ERROR) (968 :DEFINITION THE-ERROR) (967 :TYPE-PRESCRIPTION WEAK-SATISFIES-TYPE-SPEC-P) (966 :EXECUTABLE-COUNTERPART WEAK-SATISFIES-TYPE-SPEC-P) (965 :DEFINITION WEAK-SATISFIES-TYPE-SPEC-P) (964 :TYPE-PRESCRIPTION FUNCTION-SYMBOLP) (963 :EXECUTABLE-COUNTERPART FUNCTION-SYMBOLP) (962 :DEFINITION FUNCTION-SYMBOLP) (961 :TYPE-PRESCRIPTION GLOBAL-VAL) (960 :EXECUTABLE-COUNTERPART GLOBAL-VAL) (959 :DEFINITION GLOBAL-VAL) (958 :TYPE-PRESCRIPTION RETRACT-WORLD) (957 :EXECUTABLE-COUNTERPART RETRACT-WORLD) (956 :DEFINITION RETRACT-WORLD) (955 :TYPE-PRESCRIPTION EXTEND-WORLD) (954 :EXECUTABLE-COUNTERPART EXTEND-WORLD) (953 :DEFINITION EXTEND-WORLD) (952 :INDUCTION HAS-PROPSP) (951 :TYPE-PRESCRIPTION HAS-PROPSP) (950 :EXECUTABLE-COUNTERPART HAS-PROPSP) (949 :DEFINITION HAS-PROPSP) (948 :INDUCTION HAS-PROPSP1) (947 :TYPE-PRESCRIPTION HAS-PROPSP1) (946 :EXECUTABLE-COUNTERPART HAS-PROPSP1) (945 :DEFINITION HAS-PROPSP1) (944 :INDUCTION GETPROPS) (943 :TYPE-PRESCRIPTION GETPROPS) (942 :EXECUTABLE-COUNTERPART GETPROPS) (941 :DEFINITION GETPROPS) (940 :INDUCTION GETPROPS1) (939 :TYPE-PRESCRIPTION GETPROPS1) (938 :EXECUTABLE-COUNTERPART GETPROPS1) (937 :DEFINITION GETPROPS1) (936 :INDUCTION REMOVE-FIRST-PAIR) (935 :TYPE-PRESCRIPTION REMOVE-FIRST-PAIR) (934 :EXECUTABLE-COUNTERPART REMOVE-FIRST-PAIR) (933 :DEFINITION REMOVE-FIRST-PAIR) (932 :INDUCTION ADD-PAIR) (931 :TYPE-PRESCRIPTION ADD-PAIR) (930 :EXECUTABLE-COUNTERPART ADD-PAIR) (929 :DEFINITION ADD-PAIR) (928 :FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP) (927 :INDUCTION ORDERED-SYMBOL-ALISTP) (926 :TYPE-PRESCRIPTION ORDERED-SYMBOL-ALISTP) (925 :EXECUTABLE-COUNTERPART ORDERED-SYMBOL-ALISTP) (924 :DEFINITION ORDERED-SYMBOL-ALISTP) (923 :INDUCTION SGETPROP) (922 :TYPE-PRESCRIPTION SGETPROP) (921 :EXECUTABLE-COUNTERPART SGETPROP) (920 :DEFINITION SGETPROP) (919 :INDUCTION FGETPROP) (918 :TYPE-PRESCRIPTION FGETPROP) (917 :EXECUTABLE-COUNTERPART FGETPROP) (916 :DEFINITION FGETPROP) (915 :TYPE-PRESCRIPTION GETPROP-DEFAULT) (914 :EXECUTABLE-COUNTERPART GETPROP-DEFAULT) (913 :DEFINITION GETPROP-DEFAULT) (912 :TYPE-PRESCRIPTION PUTPROP) (911 :EXECUTABLE-COUNTERPART PUTPROP) (910 :DEFINITION PUTPROP) (909 :FORWARD-CHAINING WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP) (908 :INDUCTION WORLDP) (907 :TYPE-PRESCRIPTION WORLDP) (906 :EXECUTABLE-COUNTERPART WORLDP) (905 :DEFINITION WORLDP) (904 :INDUCTION SUBST) (903 :TYPE-PRESCRIPTION SUBST) (902 :EXECUTABLE-COUNTERPART SUBST) (901 :DEFINITION SUBST) (900 :INDUCTION SUBSETP) (899 :TYPE-PRESCRIPTION SUBSETP) (898 :EXECUTABLE-COUNTERPART SUBSETP) (897 :DEFINITION SUBSETP) (896 :TYPE-PRESCRIPTION SUBSTITUTE) (895 :EXECUTABLE-COUNTERPART SUBSTITUTE) (894 :DEFINITION SUBSTITUTE) (893 :INDUCTION SUBSTITUTE-AC) (892 :TYPE-PRESCRIPTION SUBSTITUTE-AC) (891 :EXECUTABLE-COUNTERPART SUBSTITUTE-AC) (890 :DEFINITION SUBSTITUTE-AC) (889 :REWRITE STRING<-IRREFLEXIVE) (888 :REWRITE STRING<-L-IRREFLEXIVE) (887 :TYPE-PRESCRIPTION SYMBOL-<) (886 :EXECUTABLE-COUNTERPART SYMBOL-<) (884 :TYPE-PRESCRIPTION STRING>=) (883 :EXECUTABLE-COUNTERPART STRING>=) (882 :DEFINITION STRING>=) (881 :TYPE-PRESCRIPTION STRING<=) (880 :EXECUTABLE-COUNTERPART STRING<=) (879 :DEFINITION STRING<=) (878 :TYPE-PRESCRIPTION STRING>) (877 :EXECUTABLE-COUNTERPART STRING>) (876 :DEFINITION STRING>) (875 :TYPE-PRESCRIPTION STRING<) (874 :EXECUTABLE-COUNTERPART STRING<) (871 :TYPE-PRESCRIPTION STRING<-L) (870 :EXECUTABLE-COUNTERPART STRING<-L) (868 :TYPE-PRESCRIPTION CHAR>=) (867 :EXECUTABLE-COUNTERPART CHAR>=) (866 :DEFINITION CHAR>=) (865 :TYPE-PRESCRIPTION CHAR<=) (864 :EXECUTABLE-COUNTERPART CHAR<=) (863 :DEFINITION CHAR<=) (862 :TYPE-PRESCRIPTION CHAR>) (861 :EXECUTABLE-COUNTERPART CHAR>) (860 :DEFINITION CHAR>) (859 :TYPE-PRESCRIPTION CHAR<) (858 :EXECUTABLE-COUNTERPART CHAR<) (857 :DEFINITION CHAR<) (856 :REWRITE CHAR-CODE-CODE-CHAR-IS-IDENTITY) (855 :REWRITE CODE-CHAR-CHAR-CODE-IS-IDENTITY) (854 :TYPE-PRESCRIPTION CODE-CHAR-TYPE) (853 :LINEAR CHAR-CODE-LINEAR) (852 :TYPE-PRESCRIPTION ASH) (851 :EXECUTABLE-COUNTERPART ASH) (850 :DEFINITION ASH) (849 :TYPE-PRESCRIPTION LOGBITP) (848 :EXECUTABLE-COUNTERPART LOGBITP) (847 :DEFINITION LOGBITP) (846 :TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION) (845 :TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE) (844 :INDUCTION NTHCDR) (843 :TYPE-PRESCRIPTION NTHCDR) (842 :EXECUTABLE-COUNTERPART NTHCDR) (841 :DEFINITION NTHCDR) (840 :INDUCTION LOGCOUNT) (839 :TYPE-PRESCRIPTION LOGCOUNT) (838 :EXECUTABLE-COUNTERPART LOGCOUNT) (837 :DEFINITION LOGCOUNT) (836 :INDUCTION EXPT) (835 :TYPE-PRESCRIPTION EXPT) (834 :EXECUTABLE-COUNTERPART EXPT) (833 :DEFINITION EXPT) (832 :INDUCTION XXXJOIN) (831 :TYPE-PRESCRIPTION XXXJOIN) (830 :EXECUTABLE-COUNTERPART XXXJOIN) (829 :DEFINITION XXXJOIN) (828 :INDUCTION ASSOC-STRING-EQUAL) (827 :TYPE-PRESCRIPTION ASSOC-STRING-EQUAL) (826 :EXECUTABLE-COUNTERPART ASSOC-STRING-EQUAL) (825 :DEFINITION ASSOC-STRING-EQUAL) (824 :TYPE-PRESCRIPTION STRING-EQUAL) (823 :EXECUTABLE-COUNTERPART STRING-EQUAL) (822 :DEFINITION STRING-EQUAL) (821 :INDUCTION STRING-EQUAL1) (820 :TYPE-PRESCRIPTION STRING-EQUAL1) (819 :EXECUTABLE-COUNTERPART STRING-EQUAL1) (818 :DEFINITION STRING-EQUAL1) (817 :REWRITE STANDARD-CHAR-P-NTH) (816 :TYPE-PRESCRIPTION LOGNOT) (815 :EXECUTABLE-COUNTERPART LOGNOT) (814 :DEFINITION LOGNOT) (813 :TYPE-PRESCRIPTION SIGNUM) (812 :EXECUTABLE-COUNTERPART SIGNUM) (811 :DEFINITION SIGNUM) (810 :TYPE-PRESCRIPTION ABS) (809 :EXECUTABLE-COUNTERPART ABS) (808 :DEFINITION ABS) (807 :TYPE-PRESCRIPTION MAX) (806 :EXECUTABLE-COUNTERPART MAX) (805 :DEFINITION MAX) (804 :TYPE-PRESCRIPTION MIN) (803 :EXECUTABLE-COUNTERPART MIN) (802 :DEFINITION MIN) (801 :TYPE-PRESCRIPTION ODDP) (800 :EXECUTABLE-COUNTERPART ODDP) (799 :DEFINITION ODDP) (798 :TYPE-PRESCRIPTION EVENP) (797 :EXECUTABLE-COUNTERPART EVENP) (796 :DEFINITION EVENP) (795 :TYPE-PRESCRIPTION REM) (794 :EXECUTABLE-COUNTERPART REM) (793 :DEFINITION REM) (792 :TYPE-PRESCRIPTION MOD) (791 :EXECUTABLE-COUNTERPART MOD) (790 :DEFINITION MOD) (789 :TYPE-PRESCRIPTION ROUND) (788 :EXECUTABLE-COUNTERPART ROUND) (787 :DEFINITION ROUND) (786 :TYPE-PRESCRIPTION TRUNCATE) (785 :EXECUTABLE-COUNTERPART TRUNCATE) (784 :DEFINITION TRUNCATE) (783 :TYPE-PRESCRIPTION CEILING) (782 :EXECUTABLE-COUNTERPART CEILING) (781 :DEFINITION CEILING) (780 :INDUCTION RESTRICT-ALIST) (779 :TYPE-PRESCRIPTION RESTRICT-ALIST) (778 :EXECUTABLE-COUNTERPART RESTRICT-ALIST) (777 :DEFINITION RESTRICT-ALIST) (776 :INDUCTION APPEND-LST) (775 :TYPE-PRESCRIPTION APPEND-LST) (774 :EXECUTABLE-COUNTERPART APPEND-LST) (773 :DEFINITION APPEND-LST) (772 :INDUCTION COLLECT-CDRS-WHEN-CAR-EQ) (771 :TYPE-PRESCRIPTION COLLECT-CDRS-WHEN-CAR-EQ) (770 :EXECUTABLE-COUNTERPART COLLECT-CDRS-WHEN-CAR-EQ) (769 :DEFINITION COLLECT-CDRS-WHEN-CAR-EQ) (768 :INDUCTION LET*-MACRO) (767 :TYPE-PRESCRIPTION LET*-MACRO) (766 :EXECUTABLE-COUNTERPART LET*-MACRO) (765 :DEFINITION LET*-MACRO) (764 :INDUCTION GET-TYPE-DECLS) (763 :TYPE-PRESCRIPTION GET-TYPE-DECLS) (762 :EXECUTABLE-COUNTERPART GET-TYPE-DECLS) (761 :DEFINITION GET-TYPE-DECLS) (760 :INDUCTION SYMBOL-LIST-LISTP) (759 :TYPE-PRESCRIPTION SYMBOL-LIST-LISTP) (758 :EXECUTABLE-COUNTERPART SYMBOL-LIST-LISTP) (757 :DEFINITION SYMBOL-LIST-LISTP) (756 :INDUCTION WELL-FORMED-TYPE-DECLS-P) (755 :TYPE-PRESCRIPTION WELL-FORMED-TYPE-DECLS-P) (754 :EXECUTABLE-COUNTERPART WELL-FORMED-TYPE-DECLS-P) (753 :DEFINITION WELL-FORMED-TYPE-DECLS-P) (752 :INDUCTION LEGAL-LET*-P) (751 :TYPE-PRESCRIPTION LEGAL-LET*-P) (750 :EXECUTABLE-COUNTERPART LEGAL-LET*-P) (749 :DEFINITION LEGAL-LET*-P) (748 :FORWARD-CHAINING TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP) (747 :INDUCTION TRUE-LIST-LISTP) (746 :TYPE-PRESCRIPTION TRUE-LIST-LISTP) (745 :EXECUTABLE-COUNTERPART TRUE-LIST-LISTP) (744 :DEFINITION TRUE-LIST-LISTP) (743 :TYPE-PRESCRIPTION POSITION) (742 :EXECUTABLE-COUNTERPART POSITION) (741 :DEFINITION POSITION) (740 :TYPE-PRESCRIPTION POSITION-EQ) (739 :EXECUTABLE-COUNTERPART POSITION-EQ) (738 :DEFINITION POSITION-EQ) (737 :INDUCTION POSITION-EQ-AC) (736 :TYPE-PRESCRIPTION POSITION-EQ-AC) (735 :EXECUTABLE-COUNTERPART POSITION-EQ-AC) (734 :DEFINITION POSITION-EQ-AC) (733 :TYPE-PRESCRIPTION POSITION-EQUAL) (732 :EXECUTABLE-COUNTERPART POSITION-EQUAL) (731 :DEFINITION POSITION-EQUAL) (730 :INDUCTION POSITION-AC) (729 :TYPE-PRESCRIPTION POSITION-AC) (728 :EXECUTABLE-COUNTERPART POSITION-AC) (727 :DEFINITION POSITION-AC) (726 :INDUCTION POSITION-EQUAL-AC) (725 :TYPE-PRESCRIPTION POSITION-EQUAL-AC) (724 :EXECUTABLE-COUNTERPART POSITION-EQUAL-AC) (723 :DEFINITION POSITION-EQUAL-AC) (722 :INDUCTION CASE-LIST-CHECK) (721 :TYPE-PRESCRIPTION CASE-LIST-CHECK) (720 :EXECUTABLE-COUNTERPART CASE-LIST-CHECK) (719 :DEFINITION CASE-LIST-CHECK) (718 :INDUCTION CASE-LIST) (717 :TYPE-PRESCRIPTION CASE-LIST) (716 :EXECUTABLE-COUNTERPART CASE-LIST) (715 :DEFINITION CASE-LIST) (714 :TYPE-PRESCRIPTION CASE-TEST) (713 :EXECUTABLE-COUNTERPART CASE-TEST) (712 :DEFINITION CASE-TEST) (711 :INDUCTION LEGAL-CASE-CLAUSESP) (710 :TYPE-PRESCRIPTION LEGAL-CASE-CLAUSESP) (709 :EXECUTABLE-COUNTERPART LEGAL-CASE-CLAUSESP) (708 :DEFINITION LEGAL-CASE-CLAUSESP) (707 :INDUCTION ER-PROGN-FN) (706 :TYPE-PRESCRIPTION ER-PROGN-FN) (705 :EXECUTABLE-COUNTERPART ER-PROGN-FN) (704 :DEFINITION ER-PROGN-FN) (703 :INDUCTION MAKE-FMT-BINDINGS) (702 :TYPE-PRESCRIPTION MAKE-FMT-BINDINGS) (701 :EXECUTABLE-COUNTERPART MAKE-FMT-BINDINGS) (700 :DEFINITION MAKE-FMT-BINDINGS) (699 :INDUCTION INTERSECTP-EQUAL) (698 :TYPE-PRESCRIPTION INTERSECTP-EQUAL) (697 :EXECUTABLE-COUNTERPART INTERSECTP-EQUAL) (696 :DEFINITION INTERSECTP-EQUAL) (695 :INDUCTION INTERSECTP) (694 :TYPE-PRESCRIPTION INTERSECTP) (693 :EXECUTABLE-COUNTERPART INTERSECTP) (692 :DEFINITION INTERSECTP) (691 :INDUCTION INTERSECTP-EQ) (690 :TYPE-PRESCRIPTION INTERSECTP-EQ) (689 :EXECUTABLE-COUNTERPART INTERSECTP-EQ) (688 :DEFINITION INTERSECTP-EQ) (687 :TYPE-PRESCRIPTION ALL-VARS) (686 :EXECUTABLE-COUNTERPART ALL-VARS) (685 :DEFINITION ALL-VARS) (684 :INDUCTION ALL-VARS1-LST) (683 :TYPE-PRESCRIPTION ALL-VARS1-LST) (682 :EXECUTABLE-COUNTERPART ALL-VARS1-LST) (681 :DEFINITION ALL-VARS1-LST) (680 :INDUCTION ALL-VARS1) (679 :TYPE-PRESCRIPTION ALL-VARS1) (678 :EXECUTABLE-COUNTERPART ALL-VARS1) (677 :DEFINITION ALL-VARS1) (676 :TYPE-PRESCRIPTION FN-SYMB) (675 :EXECUTABLE-COUNTERPART FN-SYMB) (674 :DEFINITION FN-SYMB) (673 :INDUCTION KWOTE-LST) (672 :TYPE-PRESCRIPTION KWOTE-LST) (671 :EXECUTABLE-COUNTERPART KWOTE-LST) (670 :DEFINITION KWOTE-LST) (669 :TYPE-PRESCRIPTION KWOTE) (668 :EXECUTABLE-COUNTERPART KWOTE) (667 :DEFINITION KWOTE) (666 :TYPE-PRESCRIPTION QUOTEP) (665 :EXECUTABLE-COUNTERPART QUOTEP) (664 :DEFINITION QUOTEP) (663 :TYPE-PRESCRIPTION ADD-TO-SET-EQL) (662 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQL) (661 :DEFINITION ADD-TO-SET-EQL) (660 :TYPE-PRESCRIPTION ADD-TO-SET-EQ) (659 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQ) (658 :DEFINITION ADD-TO-SET-EQ) (657 :INDUCTION PSEUDO-TERM-LIST-LISTP) (656 :TYPE-PRESCRIPTION PSEUDO-TERM-LIST-LISTP) (655 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LIST-LISTP) (654 :DEFINITION PSEUDO-TERM-LIST-LISTP) (653 :FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) (652 :INDUCTION PSEUDO-TERM-LISTP) (651 :TYPE-PRESCRIPTION PSEUDO-TERM-LISTP) (650 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP) (649 :DEFINITION PSEUDO-TERM-LISTP) (648 :INDUCTION PSEUDO-TERMP) (647 :TYPE-PRESCRIPTION PSEUDO-TERMP) (646 :EXECUTABLE-COUNTERPART PSEUDO-TERMP) (645 :DEFINITION PSEUDO-TERMP) (644 :INDUCTION DEFUND-NAME-LIST) (643 :TYPE-PRESCRIPTION DEFUND-NAME-LIST) (642 :EXECUTABLE-COUNTERPART DEFUND-NAME-LIST) (641 :DEFINITION DEFUND-NAME-LIST) (640 :TYPE-PRESCRIPTION XD-NAME) (639 :EXECUTABLE-COUNTERPART XD-NAME) (638 :DEFINITION XD-NAME) (637 :TYPE-PRESCRIPTION VALUE-TRIPLE-FN) (636 :EXECUTABLE-COUNTERPART VALUE-TRIPLE-FN) (635 :DEFINITION VALUE-TRIPLE-FN) (634 :INDUCTION COLLECT-CADRS-WHEN-CAR-EQ) (633 :TYPE-PRESCRIPTION COLLECT-CADRS-WHEN-CAR-EQ) (632 :EXECUTABLE-COUNTERPART COLLECT-CADRS-WHEN-CAR-EQ) (631 :DEFINITION COLLECT-CADRS-WHEN-CAR-EQ) (630 :INDUCTION MUTUAL-RECURSION-GUARDP) (629 :TYPE-PRESCRIPTION MUTUAL-RECURSION-GUARDP) (628 :EXECUTABLE-COUNTERPART MUTUAL-RECURSION-GUARDP) (627 :DEFINITION MUTUAL-RECURSION-GUARDP) (626 :INDUCTION STRIP-CDRS) (625 :TYPE-PRESCRIPTION STRIP-CDRS) (624 :EXECUTABLE-COUNTERPART STRIP-CDRS) (623 :DEFINITION STRIP-CDRS) (622 :TYPE-PRESCRIPTION BUTLAST) (621 :EXECUTABLE-COUNTERPART BUTLAST) (620 :DEFINITION BUTLAST) (619 :TYPE-PRESCRIPTION TAKE) (618 :EXECUTABLE-COUNTERPART TAKE) (617 :DEFINITION TAKE) (616 :INDUCTION FIRST-N-AC) (615 :TYPE-PRESCRIPTION FIRST-N-AC) (614 :EXECUTABLE-COUNTERPART FIRST-N-AC) (613 :DEFINITION FIRST-N-AC) (612 :INDUCTION LAST) (611 :TYPE-PRESCRIPTION LAST) (610 :EXECUTABLE-COUNTERPART LAST) (609 :DEFINITION LAST) (608 :INDUCTION SET-DIFFERENCE-EQ) (607 :TYPE-PRESCRIPTION SET-DIFFERENCE-EQ) (606 :EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQ) (605 :DEFINITION SET-DIFFERENCE-EQ) (604 :TYPE-PRESCRIPTION REVERSE) (603 :EXECUTABLE-COUNTERPART REVERSE) (602 :DEFINITION REVERSE) (601 :REWRITE CHARACTER-LISTP-REVAPPEND) (600 :INDUCTION REVAPPEND) (599 :TYPE-PRESCRIPTION REVAPPEND) (598 :EXECUTABLE-COUNTERPART REVAPPEND) (597 :DEFINITION REVAPPEND) (596 :TYPE-PRESCRIPTION IDENTITY) (595 :EXECUTABLE-COUNTERPART IDENTITY) (594 :DEFINITION IDENTITY) (593 :INDUCTION REMOVE-DUPLICATES-EQUAL) (592 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL) (591 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQUAL) (590 :DEFINITION REMOVE-DUPLICATES-EQUAL) (589 :TYPE-PRESCRIPTION REMOVE-DUPLICATES) (588 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES) (587 :DEFINITION REMOVE-DUPLICATES) (586 :REWRITE CHARACTER-LISTP-REMOVE-DUPLICATES-EQL) (585 :INDUCTION REMOVE-DUPLICATES-EQL) (584 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQL) (583 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQL) (582 :DEFINITION REMOVE-DUPLICATES-EQL) (581 :INDUCTION PAIRLIS$) (580 :TYPE-PRESCRIPTION PAIRLIS$) (579 :EXECUTABLE-COUNTERPART PAIRLIS$) (578 :DEFINITION PAIRLIS$) (577 :INDUCTION REMOVE1-EQUAL) (576 :TYPE-PRESCRIPTION REMOVE1-EQUAL) (575 :EXECUTABLE-COUNTERPART REMOVE1-EQUAL) (574 :DEFINITION REMOVE1-EQUAL) (573 :INDUCTION REMOVE1-EQ) (572 :TYPE-PRESCRIPTION REMOVE1-EQ) (571 :EXECUTABLE-COUNTERPART REMOVE1-EQ) (570 :DEFINITION REMOVE1-EQ) (569 :INDUCTION REMOVE1) (568 :TYPE-PRESCRIPTION REMOVE1) (567 :EXECUTABLE-COUNTERPART REMOVE1) (566 :DEFINITION REMOVE1) (565 :INDUCTION REMOVE-EQUAL) (564 :TYPE-PRESCRIPTION REMOVE-EQUAL) (563 :EXECUTABLE-COUNTERPART REMOVE-EQUAL) (562 :DEFINITION REMOVE-EQUAL) (561 :INDUCTION REMOVE-EQ) (560 :TYPE-PRESCRIPTION REMOVE-EQ) (559 :EXECUTABLE-COUNTERPART REMOVE-EQ) (558 :DEFINITION REMOVE-EQ) (557 :INDUCTION REMOVE) (556 :TYPE-PRESCRIPTION REMOVE) (555 :EXECUTABLE-COUNTERPART REMOVE) (554 :DEFINITION REMOVE) (553 :INDUCTION STRING-APPEND-LST) (552 :TYPE-PRESCRIPTION STRING-APPEND-LST) (551 :EXECUTABLE-COUNTERPART STRING-APPEND-LST) (550 :DEFINITION STRING-APPEND-LST) (549 :INDUCTION STRING-LISTP) (548 :TYPE-PRESCRIPTION STRING-LISTP) (547 :EXECUTABLE-COUNTERPART STRING-LISTP) (546 :DEFINITION STRING-LISTP) (545 :TYPE-PRESCRIPTION STRING-APPEND) (544 :EXECUTABLE-COUNTERPART STRING-APPEND) (543 :DEFINITION STRING-APPEND) (542 :REWRITE APPEND-TO-NIL) (541 :REWRITE CHARACTER-LISTP-APPEND) (540 :REWRITE STANDARD-CHAR-LISTP-APPEND) (539 :INDUCTION BINARY-APPEND) (538 :TYPE-PRESCRIPTION BINARY-APPEND) (537 :EXECUTABLE-COUNTERPART BINARY-APPEND) (536 :DEFINITION BINARY-APPEND) (535 :REWRITE KEYWORD-PACKAGE) (534 :REWRITE ACL2-PACKAGE) (533 :REWRITE ACL2-OUTPUT-CHANNEL-PACKAGE) (532 :REWRITE ACL2-INPUT-CHANNEL-PACKAGE) (531 :REWRITE SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL) (530 :INDUCTION MEMBER-SYMBOL-NAME) (529 :TYPE-PRESCRIPTION MEMBER-SYMBOL-NAME) (528 :EXECUTABLE-COUNTERPART MEMBER-SYMBOL-NAME) (527 :DEFINITION MEMBER-SYMBOL-NAME) (526 :REWRITE SYMBOL-PACKAGE-NAME-PKG-WITNESS-NAME) (525 :REWRITE SYMBOL-NAME-PKG-WITNESS) (524 :FORWARD-CHAINING SYMBOL-PACKAGE-NAME-OF-SYMBOL-IS-NOT-EMPTY-STRING) (523 :REWRITE INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME) (522 :FORWARD-CHAINING KEYWORDP-FORWARD-TO-SYMBOLP) (521 :TYPE-PRESCRIPTION KEYWORDP) (520 :EXECUTABLE-COUNTERPART KEYWORDP) (519 :DEFINITION KEYWORDP) (518 :TYPE-PRESCRIPTION ILLEGAL) (517 :EXECUTABLE-COUNTERPART ILLEGAL) (516 :DEFINITION ILLEGAL) (515 :TYPE-PRESCRIPTION HARD-ERROR) (514 :EXECUTABLE-COUNTERPART HARD-ERROR) (513 :DEFINITION HARD-ERROR) (512 :TYPE-PRESCRIPTION SYMBOLP-PKG-WITNESS) (511 :TYPE-PRESCRIPTION SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL) (510 :TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME) (509 :TYPE-PRESCRIPTION NULL-BODY-ER) (508 :EXECUTABLE-COUNTERPART NULL-BODY-ER) (507 :DEFINITION NULL-BODY-ER) (506 :INDUCTION LIST*-MACRO) (505 :TYPE-PRESCRIPTION LIST*-MACRO) (504 :EXECUTABLE-COUNTERPART LIST*-MACRO) (503 :DEFINITION LIST*-MACRO) (502 :TYPE-PRESCRIPTION MAKE-ORD) (501 :EXECUTABLE-COUNTERPART MAKE-ORD) (500 :DEFINITION MAKE-ORD) (499 :REWRITE O-P-IMPLIES-O(global-table state) ACL2 Error in TOP-LEVEL: A single-threaded object, namely STATE, is being used where an ordinary object is expected. ACL2 !>(trace$ ens) ((ENS)) ACL2 !>(ens state) 1> (ACL2_*1*_ACL2::ENS |*the-live-state*|) 2> (ENS |*the-live-state*|) <2 (ENS |some-enabled-structure|) <1 (ACL2_*1*_ACL2::ENS |some-enabled-structure|) ((2101 (:HEADER :DIMENSIONS (2500) :MAXIMUM-LENGTH 2501 :DEFAULT NIL :NAME ENABLED-ARRAY-0 :ORDER NIL) (2101 :TYPE-PRESCRIPTION HONSP-CHECK) (2100 :EXECUTABLE-COUNTERPART HONSP-CHECK) (2099 :DEFINITION HONSP-CHECK) (2098 :TYPE-PRESCRIPTION NUMBER-SUBTREES) (2097 :EXECUTABLE-COUNTERPART NUMBER-SUBTREES) (2096 :DEFINITION NUMBER-SUBTREES) (2095 :INDUCTION FASTER-CONS-SUBTREES) (2094 :TYPE-PRESCRIPTION FASTER-CONS-SUBTREES) (2093 :EXECUTABLE-COUNTERPART FASTER-CONS-SUBTREES) (2092 :DEFINITION FASTER-CONS-SUBTREES) (2091 :INDUCTION CONS-SUBTREES) (2090 :TYPE-PRESCRIPTION CONS-SUBTREES) (2089 :EXECUTABLE-COUNTERPART CONS-SUBTREES) (2088 :DEFINITION CONS-SUBTREES) (2087 :INDUCTION HONS-SHRINK-ALIST) (2086 :TYPE-PRESCRIPTION HONS-SHRINK-ALIST) (2085 :EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST) (2084 :DEFINITION HONS-SHRINK-ALIST) (2083 :INDUCTION HONS-SHRINK-ALIST!) (2082 :TYPE-PRESCRIPTION HONS-SHRINK-ALIST!) (2081 :EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST!) (2080 :DEFINITION HONS-SHRINK-ALIST!) (2079 :TYPE-PRESCRIPTION MEMOIZE-OFF) (2078 :EXECUTABLE-COUNTERPART MEMOIZE-OFF) (2077 :DEFINITION MEMOIZE-OFF) (2076 :TYPE-PRESCRIPTION MEMOIZE-ON) (2075 :EXECUTABLE-COUNTERPART MEMOIZE-ON) (2074 :DEFINITION MEMOIZE-ON) (2073 :TYPE-PRESCRIPTION MEMOIZE-FORM) (2072 :EXECUTABLE-COUNTERPART MEMOIZE-FORM) (2071 :DEFINITION MEMOIZE-FORM) (2070 :TYPE-PRESCRIPTION HONS-ENABLEDP) (2069 :EXECUTABLE-COUNTERPART HONS-ENABLEDP) (2068 :DEFINITION HONS-ENABLEDP) (2067 :TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLES) (2066 :EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLES) (2065 :DEFINITION CLEAR-MEMOIZE-TABLES) (2064 :TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLE) (2063 :EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLE) (2062 :DEFINITION CLEAR-MEMOIZE-TABLE) (2061 :TYPE-PRESCRIPTION FLUSH-HONS-GET-HASH-TABLE-LINK) (2060 :EXECUTABLE-COUNTERPART FLUSH-HONS-GET-HASH-TABLE-LINK) (2059 :DEFINITION FLUSH-HONS-GET-HASH-TABLE-LINK) (2058 :TYPE-PRESCRIPTION FAST-ALIST-LEN) (2057 :EXECUTABLE-COUNTERPART FAST-ALIST-LEN) (2056 :DEFINITION FAST-ALIST-LEN) (2055 :INDUCTION FAST-ALIST-LEN-ACC) (2054 :TYPE-PRESCRIPTION FAST-ALIST-LEN-ACC) (2053 :EXECUTABLE-COUNTERPART FAST-ALIST-LEN-ACC) (2052 :DEFINITION FAST-ALIST-LEN-ACC) (2051 :TYPE-PRESCRIPTION HONS-ACONS!) (2050 :EXECUTABLE-COUNTERPART HONS-ACONS!) (2049 :DEFINITION HONS-ACONS!) (2048 :TYPE-PRESCRIPTION HONS-ACONS) (2047 :EXECUTABLE-COUNTERPART HONS-ACONS) (2046 :DEFINITION HONS-ACONS) (2045 :TYPE-PRESCRIPTION HONS-GET-FN-DO-NOT-HOPY) (2044 :EXECUTABLE-COUNTERPART HONS-GET-FN-DO-NOT-HOPY) (2043 :DEFINITION HONS-GET-FN-DO-NOT-HOPY) (2042 :TYPE-PRESCRIPTION HONS-GET-FN-DO-HOPY) (2041 :EXECUTABLE-COUNTERPART HONS-GET-FN-DO-HOPY) (2040 :DEFINITION HONS-GET-FN-DO-HOPY) (2039 :INDUCTION HONS-ASSOC-EQUAL) (2038 :TYPE-PRESCRIPTION HONS-ASSOC-EQUAL) (2037 :EXECUTABLE-COUNTERPART HONS-ASSOC-EQUAL) (2036 :DEFINITION HONS-ASSOC-EQUAL) (2035 :TYPE-PRESCRIPTION HONS-COPY) (2034 :EXECUTABLE-COUNTERPART HONS-COPY) (2033 :DEFINITION HONS-COPY) (2032 :TYPE-PRESCRIPTION HONS-EQUAL) (2031 :EXECUTABLE-COUNTERPART HONS-EQUAL) (2030 :DEFINITION HONS-EQUAL) (2029 :TYPE-PRESCRIPTION HONS) (2028 :EXECUTABLE-COUNTERPART HONS) (2027 :DEFINITION HONS) (2026 :TYPE-PRESCRIPTION CLEAR-HASH-TABLES) (2025 :EXECUTABLE-COUNTERPART CLEAR-HASH-TABLES) (2024 :DEFINITION CLEAR-HASH-TABLES) (2023 :TYPE-PRESCRIPTION TIME$-LOGIC) (2022 :EXECUTABLE-COUNTERPART TIME$-LOGIC) (2021 :DEFINITION TIME$-LOGIC) (2020 :TYPE-PRESCRIPTION CPU-CORE-COUNT) (2019 :EXECUTABLE-COUNTERPART CPU-CORE-COUNT) (2018 :DEFINITION CPU-CORE-COUNT) (2017 :TYPE-PRESCRIPTION SEARCH-FN) (2016 :EXECUTABLE-COUNTERPART SEARCH-FN) (2015 :DEFINITION SEARCH-FN) (2014 :INDUCTION SEARCH-FROM-END) (2013 :TYPE-PRESCRIPTION SEARCH-FROM-END) (2012 :EXECUTABLE-COUNTERPART SEARCH-FROM-END) (2011 :DEFINITION SEARCH-FROM-END) (2010 :INDUCTION SEARCH-FROM-START) (2009 :TYPE-PRESCRIPTION SEARCH-FROM-START) (2008 :EXECUTABLE-COUNTERPART SEARCH-FROM-START) (2007 :DEFINITION SEARCH-FROM-START) (2006 :TYPE-PRESCRIPTION SEARCH-FN-GUARD) (2005 :EXECUTABLE-COUNTERPART SEARCH-FN-GUARD) (2004 :DEFINITION SEARCH-FN-GUARD) (2003 :INDUCTION SPLICE-KEYWORD-ALIST) (2002 :TYPE-PRESCRIPTION SPLICE-KEYWORD-ALIST) (2001 :EXECUTABLE-COUNTERPART SPLICE-KEYWORD-ALIST) (2000 :DEFINITION SPLICE-KEYWORD-ALIST) (1999 :TYPE-PRESCRIPTION CLAUSES-RESULT) (1998 :EXECUTABLE-COUNTERPART CLAUSES-RESULT) (1997 :DEFINITION CLAUSES-RESULT) (1996 :TYPE-PRESCRIPTION CONJOIN-CLAUSES) (1995 :EXECUTABLE-COUNTERPART CONJOIN-CLAUSES) (1994 :DEFINITION CONJOIN-CLAUSES) (1993 :INDUCTION DISJOIN-LST) (1992 :TYPE-PRESCRIPTION DISJOIN-LST) (1991 :EXECUTABLE-COUNTERPART DISJOIN-LST) (1990 :DEFINITION DISJOIN-LST) (1989 :INDUCTION DISJOIN) (1988 :TYPE-PRESCRIPTION DISJOIN) (1987 :EXECUTABLE-COUNTERPART DISJOIN) (1986 :DEFINITION DISJOIN) (1985 :TYPE-PRESCRIPTION DISJOIN2) (1984 :EXECUTABLE-COUNTERPART DISJOIN2) (1983 :DEFINITION DISJOIN2) (1982 :INDUCTION CONJOIN) (1981 :TYPE-PRESCRIPTION CONJOIN) (1980 :EXECUTABLE-COUNTERPART CONJOIN) (1979 :DEFINITION CONJOIN) (1978 :TYPE-PRESCRIPTION CONJOIN2) (1977 :EXECUTABLE-COUNTERPART CONJOIN2) (1976 :DEFINITION CONJOIN2) (1975 :TYPE-PRESCRIPTION MOD-EXPT) (1974 :EXECUTABLE-COUNTERPART MOD-EXPT) (1973 :DEFINITION MOD-EXPT) (1972 :INDUCTION E/D-FN) (1971 :TYPE-PRESCRIPTION E/D-FN) (1970 :EXECUTABLE-COUNTERPART E/D-FN) (1969 :DEFINITION E/D-FN) (1968 :INDUCTION RESIZE-LIST) (1967 :TYPE-PRESCRIPTION RESIZE-LIST) (1966 :EXECUTABLE-COUNTERPART RESIZE-LIST) (1965 :DEFINITION RESIZE-LIST) (1964 :INDUCTION MERGE-SORT-LEXORDER) (1963 :TYPE-PRESCRIPTION MERGE-SORT-LEXORDER) (1962 :EXECUTABLE-COUNTERPART MERGE-SORT-LEXORDER) (1961 :DEFINITION MERGE-SORT-LEXORDER) (1960 :TYPE-PRESCRIPTION TRUE-LISTP-MERGE-SORT-LEXORDER) (1959 :INDUCTION MERGE-LEXORDER) (1958 :TYPE-PRESCRIPTION MERGE-LEXORDER) (1957 :EXECUTABLE-COUNTERPART MERGE-LEXORDER) (1956 :DEFINITION MERGE-LEXORDER) (1955 :FORWARD-CHAINING LEXORDER-TOTAL) (1954 :REWRITE LEXORDER-TRANSITIVE) (1953 :FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC) (1952 :REWRITE LEXORDER-REFLEXIVE) (1951 :FORWARD-CHAINING ALPHORDER-TOTAL) (1950 :FORWARD-CHAINING ALPHORDER-ANTI-SYMMETRIC) (1949 :REWRITE ALPHORDER-TRANSITIVE) (1948 :REWRITE ALPHORDER-REFLEXIVE) (1946 :TYPE-PRESCRIPTION LEXORDER) (1945 :EXECUTABLE-COUNTERPART LEXORDER) (1943 :TYPE-PRESCRIPTION ALPHORDER) (1942 :EXECUTABLE-COUNTERPART ALPHORDER) (1940 :REWRITE BAD-ATOM<=-TRANSITIVE) (1939 :TYPE-PRESCRIPTION BOOLEANP-BAD-ATOM<=) (1938 :COMPOUND-RECOGNIZER BAD-ATOM-COMPOUND-RECOGNIZER) (1937 :TYPE-PRESCRIPTION BAD-ATOM) (1936 :EXECUTABLE-COUNTERPART BAD-ATOM) (1934 :REWRITE TYPE-ALISTP-MFC-TYPE-ALIST) (1933 :REWRITE PSEUDO-TERM-LISTP-MFC-CLAUSE) (1932 :TYPE-PRESCRIPTION MFC-ANCESTORS) (1931 :EXECUTABLE-COUNTERPART MFC-ANCESTORS) (1930 :DEFINITION MFC-ANCESTORS) (1929 :TYPE-PRESCRIPTION MFC-TYPE-ALIST) (1928 :EXECUTABLE-COUNTERPART MFC-TYPE-ALIST) (1927 :DEFINITION MFC-TYPE-ALIST) (1926 :INDUCTION TYPE-ALISTP) (1925 :TYPE-PRESCRIPTION TYPE-ALISTP) (1924 :EXECUTABLE-COUNTERPART TYPE-ALISTP) (1923 :DEFINITION TYPE-ALISTP) (1922 :TYPE-PRESCRIPTION TYPE-ALIST-ENTRYP) (1921 :EXECUTABLE-COUNTERPART TYPE-ALIST-ENTRYP) (1920 :DEFINITION TYPE-ALIST-ENTRYP) (1919 :TYPE-PRESCRIPTION MFC-RDEPTH) (1918 :EXECUTABLE-COUNTERPART MFC-RDEPTH) (1917 :DEFINITION MFC-RDEPTH) (1916 :TYPE-PRESCRIPTION MFC-CLAUSE) (1915 :EXECUTABLE-COUNTERPART MFC-CLAUSE) (1914 :DEFINITION MFC-CLAUSE) (1913 :TYPE-PRESCRIPTION RECORD-ACCESSOR-FUNCTION-NAME) (1912 :EXECUTABLE-COUNTERPART RECORD-ACCESSOR-FUNCTION-NAME) (1911 :DEFINITION RECORD-ACCESSOR-FUNCTION-NAME) (1910 :TYPE-PRESCRIPTION RECORD-ERROR) (1909 :EXECUTABLE-COUNTERPART RECORD-ERROR) (1908 :DEFINITION RECORD-ERROR) (1907 :TYPE-PRESCRIPTION SET-EQUALP-EQUAL) (1906 :EXECUTABLE-COUNTERPART SET-EQUALP-EQUAL) (1905 :DEFINITION SET-EQUALP-EQUAL) (1904 :TYPE-PRESCRIPTION ODDS) (1903 :EXECUTABLE-COUNTERPART ODDS) (1902 :DEFINITION ODDS) (1901 :INDUCTION EVENS) (1900 :TYPE-PRESCRIPTION EVENS) (1899 :EXECUTABLE-COUNTERPART EVENS) (1898 :DEFINITION EVENS) (1897 :INDUCTION INTERSECTION-EQ) (1896 :TYPE-PRESCRIPTION INTERSECTION-EQ) (1895 :EXECUTABLE-COUNTERPART INTERSECTION-EQ) (1894 :DEFINITION INTERSECTION-EQ) (1893 :TYPE-PRESCRIPTION ADD-TO-SET-EQUAL) (1892 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQUAL) (1891 :DEFINITION ADD-TO-SET-EQUAL) (1890 :INDUCTION DUPLICATES) (1889 :TYPE-PRESCRIPTION DUPLICATES) (1888 :EXECUTABLE-COUNTERPART DUPLICATES) (1887 :DEFINITION DUPLICATES) (1886 :INDUCTION PAIRLIS2) (1885 :TYPE-PRESCRIPTION PAIRLIS2) (1884 :EXECUTABLE-COUNTERPART PAIRLIS2) (1883 :DEFINITION PAIRLIS2) (1882 :TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW!) (1881 :EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW!) (1880 :DEFINITION FMT-TO-COMMENT-WINDOW!) (1879 :TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW) (1878 :EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW) (1877 :DEFINITION FMT-TO-COMMENT-WINDOW) (1876 :TYPE-PRESCRIPTION ABORT!) (1873 :TYPE-PRESCRIPTION WORMHOLE-P) (1872 :EXECUTABLE-COUNTERPART WORMHOLE-P) (1871 :DEFINITION WORMHOLE-P) (1870 :TYPE-PRESCRIPTION WORMHOLE1) (1869 :EXECUTABLE-COUNTERPART WORMHOLE1) (1868 :DEFINITION WORMHOLE1) (1867 :TYPE-PRESCRIPTION TIME-LIMIT4-REACHED-P) (1866 :EXECUTABLE-COUNTERPART TIME-LIMIT4-REACHED-P) (1865 :DEFINITION TIME-LIMIT4-REACHED-P) (1864 :TYPE-PRESCRIPTION WITH-PROVER-TIME-LIMIT) (1863 :EXECUTABLE-COUNTERPART WITH-PROVER-TIME-LIMIT) (1862 :DEFINITION WITH-PROVER-TIME-LIMIT) (1861 :TYPE-PRESCRIPTION DOUBLE-REWRITE) (1860 :EXECUTABLE-COUNTERPART DOUBLE-REWRITE) (1859 :DEFINITION DOUBLE-REWRITE) (1858 :REWRITE DEFAULT-SYMBOL-PACKAGE-NAME) (1857 :REWRITE DEFAULT-SYMBOL-NAME) (1856 :REWRITE DEFAULT-REALPART) (1855 :REWRITE DEFAULT-NUMERATOR) (1854 :REWRITE DEFAULT-IMAGPART) (1853 :REWRITE DEFAULT-DENOMINATOR) (1852 :REWRITE DEFAULT-COERCE-3) (1851 :REWRITE DEFAULT-COERCE-2) (1850 :REWRITE MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST) (1849 :REWRITE DEFAULT-COERCE-1) (1848 :REWRITE IMAGPART-+) (1847 :REWRITE REALPART-+) (1846 :REWRITE COMPLEX-0) (1845 :REWRITE DEFAULT-COMPLEX-2) (1844 :REWRITE DEFAULT-COMPLEX-1) (1843 :REWRITE DEFAULT-CHAR-CODE) (1842 :REWRITE CONS-CAR-CDR) (1841 :REWRITE DEFAULT-CDR) (1840 :REWRITE DEFAULT-CAR) (1839 :REWRITE DEFAULT-<-2) (1838 :REWRITE DEFAULT-<-1) (1837 :REWRITE DEFAULT-UNARY-/) (1836 :REWRITE DEFAULT-UNARY-MINUS) (1835 :REWRITE DEFAULT-*-2) (1834 :REWRITE DEFAULT-*-1) (1833 :REWRITE DEFAULT-+-2) (1832 :REWRITE DEFAULT-+-1) (1831 :FORWARD-CHAINING BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP) (1830 :FORWARD-CHAINING BOOLEAN-LISTP-FORWARD) (1829 :REWRITE BOOLEAN-LISTP-CONS) (1828 :INDUCTION BOOLEAN-LISTP) (1827 :TYPE-PRESCRIPTION BOOLEAN-LISTP) (1826 :EXECUTABLE-COUNTERPART BOOLEAN-LISTP) (1825 :DEFINITION BOOLEAN-LISTP) (1824 :REWRITE PAIRLIS$-FIX-TRUE-LIST) (1823 :INDUCTION FIX-TRUE-LIST) (1822 :TYPE-PRESCRIPTION FIX-TRUE-LIST) (1821 :EXECUTABLE-COUNTERPART FIX-TRUE-LIST) (1820 :DEFINITION FIX-TRUE-LIST) (1819 :TYPE-PRESCRIPTION DEFAULT-HINTS) (1818 :EXECUTABLE-COUNTERPART DEFAULT-HINTS) (1817 :DEFINITION DEFAULT-HINTS) (1816 :TYPE-PRESCRIPTION NTH-ALIASES) (1815 :EXECUTABLE-COUNTERPART NTH-ALIASES) (1814 :DEFINITION NTH-ALIASES) (1813 :TYPE-PRESCRIPTION MACRO-ALIASES) (1812 :EXECUTABLE-COUNTERPART MACRO-ALIASES) (1811 :DEFINITION MACRO-ALIASES) (1810 :TYPE-PRESCRIPTION NON-LINEARP) (1809 :EXECUTABLE-COUNTERPART NON-LINEARP) (1808 :DEFINITION NON-LINEARP) (1807 :TYPE-PRESCRIPTION MATCH-FREE-OVERRIDE) (1806 :EXECUTABLE-COUNTERPART MATCH-FREE-OVERRIDE) (1805 :DEFINITION MATCH-FREE-OVERRIDE) (1804 :TYPE-PRESCRIPTION MATCH-FREE-DEFAULT) (1803 :EXECUTABLE-COUNTERPART MATCH-FREE-DEFAULT) (1802 :DEFINITION MATCH-FREE-DEFAULT) (1801 :TYPE-PRESCRIPTION BINOP-TABLE) (1800 :EXECUTABLE-COUNTERPART BINOP-TABLE) (1799 :DEFINITION BINOP-TABLE) (1798 :TYPE-PRESCRIPTION CASE-SPLIT-LIMITATIONS) (1797 :EXECUTABLE-COUNTERPART CASE-SPLIT-LIMITATIONS) (1796 :DEFINITION CASE-SPLIT-LIMITATIONS) (1795 :TYPE-PRESCRIPTION REWRITE-STACK-LIMIT) (1794 :EXECUTABLE-COUNTERPART REWRITE-STACK-LIMIT) (1793 :DEFINITION REWRITE-STACK-LIMIT) (1792 :TYPE-PRESCRIPTION DEFAULT-BACKCHAIN-LIMIT) (1791 :EXECUTABLE-COUNTERPART DEFAULT-BACKCHAIN-LIMIT) (1790 :DEFINITION DEFAULT-BACKCHAIN-LIMIT) (1789 :TYPE-PRESCRIPTION BACKCHAIN-LIMIT) (1788 :EXECUTABLE-COUNTERPART BACKCHAIN-LIMIT) (1787 :DEFINITION BACKCHAIN-LIMIT) (1786 :INDUCTION DELETE-ASSOC-EQUAL) (1785 :TYPE-PRESCRIPTION DELETE-ASSOC-EQUAL) (1784 :EXECUTABLE-COUNTERPART DELETE-ASSOC-EQUAL) (1783 :DEFINITION DELETE-ASSOC-EQUAL) (1782 :INDUCTION DELETE-ASSOC-EQ) (1781 :TYPE-PRESCRIPTION DELETE-ASSOC-EQ) (1780 :EXECUTABLE-COUNTERPART DELETE-ASSOC-EQ) (1779 :DEFINITION DELETE-ASSOC-EQ) (1778 :TYPE-PRESCRIPTION INVISIBLE-FNS-ENTRYP) (1777 :EXECUTABLE-COUNTERPART INVISIBLE-FNS-ENTRYP) (1776 :DEFINITION INVISIBLE-FNS-ENTRYP) (1775 :INDUCTION UNARY-FUNCTION-SYMBOL-LISTP) (1774 :TYPE-PRESCRIPTION UNARY-FUNCTION-SYMBOL-LISTP) (1773 :EXECUTABLE-COUNTERPART UNARY-FUNCTION-SYMBOL-LISTP) (1772 :DEFINITION UNARY-FUNCTION-SYMBOL-LISTP) (1771 :TYPE-PRESCRIPTION INVISIBLE-FNS-TABLE) (1770 :EXECUTABLE-COUNTERPART INVISIBLE-FNS-TABLE) (1769 :DEFINITION INVISIBLE-FNS-TABLE) (1768 :TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE-FROM-STATE) (1767 :EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE-FROM-STATE) (1766 :DEFINITION DEFAULT-DEFUN-MODE-FROM-STATE) (1765 :TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE) (1764 :EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE) (1763 :DEFINITION DEFAULT-DEFUN-MODE) (1762 :TYPE-PRESCRIPTION DEFAULT-WELL-FOUNDED-RELATION) (1761 :EXECUTABLE-COUNTERPART DEFAULT-WELL-FOUNDED-RELATION) (1760 :DEFINITION DEFAULT-WELL-FOUNDED-RELATION) (1759 :TYPE-PRESCRIPTION DEFAULT-MEASURE-FUNCTION) (1758 :EXECUTABLE-COUNTERPART DEFAULT-MEASURE-FUNCTION) (1757 :DEFINITION DEFAULT-MEASURE-FUNCTION) (1756 :TYPE-PRESCRIPTION DEFAULT-COMPILE-FNS) (1755 :EXECUTABLE-COUNTERPART DEFAULT-COMPILE-FNS) (1754 :DEFINITION DEFAULT-COMPILE-FNS) (1753 :TYPE-PRESCRIPTION DEFAULT-VERIFY-GUARDS-EAGERNESS) (1752 :EXECUTABLE-COUNTERPART DEFAULT-VERIFY-GUARDS-EAGERNESS) (1751 :DEFINITION DEFAULT-VERIFY-GUARDS-EAGERNESS) (1750 :TYPE-PRESCRIPTION TABLE-ALIST) (1749 :EXECUTABLE-COUNTERPART TABLE-ALIST) (1748 :DEFINITION TABLE-ALIST) (1747 :INDUCTION LEGAL-RULER-EXTENDERS-P) (1746 :TYPE-PRESCRIPTION LEGAL-RULER-EXTENDERS-P) (1745 :EXECUTABLE-COUNTERPART LEGAL-RULER-EXTENDERS-P) (1744 :DEFINITION LEGAL-RULER-EXTENDERS-P) (1743 :INDUCTION INCLUDE-BOOK-DIR-ALISTP) (1742 :TYPE-PRESCRIPTION INCLUDE-BOOK-DIR-ALISTP) (1741 :EXECUTABLE-COUNTERPART INCLUDE-BOOK-DIR-ALISTP) (1740 :DEFINITION INCLUDE-BOOK-DIR-ALISTP) (1739 :TYPE-PRESCRIPTION OS) (1738 :EXECUTABLE-COUNTERPART OS) (1737 :DEFINITION OS) (1736 :TYPE-PRESCRIPTION ABSOLUTE-PATHNAME-STRING-P) (1735 :EXECUTABLE-COUNTERPART ABSOLUTE-PATHNAME-STRING-P) (1734 :DEFINITION ABSOLUTE-PATHNAME-STRING-P) (1733 :TYPE-PRESCRIPTION NATP-POSITION-AC) (1732 :TYPE-PRESCRIPTION FREE-VAR-RUNES) (1731 :EXECUTABLE-COUNTERPART FREE-VAR-RUNES) (1730 :DEFINITION FREE-VAR-RUNES) (1729 :INDUCTION NON-FREE-VAR-RUNES) (1728 :TYPE-PRESCRIPTION NON-FREE-VAR-RUNES) (1727 :EXECUTABLE-COUNTERPART NON-FREE-VAR-RUNES) (1726 :DEFINITION NON-FREE-VAR-RUNES) (1725 :TYPE-PRESCRIPTION MAKE-VAR-LST) (1724 :EXECUTABLE-COUNTERPART MAKE-VAR-LST) (1723 :DEFINITION MAKE-VAR-LST) (1722 :INDUCTION MAKE-VAR-LST1) (1721 :TYPE-PRESCRIPTION MAKE-VAR-LST1) (1720 :EXECUTABLE-COUNTERPART MAKE-VAR-LST1) (1719 :DEFINITION MAKE-VAR-LST1) (1718 :TYPE-PRESCRIPTION LD-SKIP-PROOFSP) (1717 :EXECUTABLE-COUNTERPART LD-SKIP-PROOFSP) (1716 :DEFINITION LD-SKIP-PROOFSP) (1715 :INDUCTION UNION-EQ) (1714 :TYPE-PRESCRIPTION UNION-EQ) (1713 :EXECUTABLE-COUNTERPART UNION-EQ) (1712 :DEFINITION UNION-EQ) (1711 :TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL) (1710 :REWRITE STATE-P1-UPDATE-NTH-2-WORLD) (1709 :TYPE-PRESCRIPTION KNOWN-PACKAGE-ALIST) (1708 :EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALIST) (1707 :DEFINITION KNOWN-PACKAGE-ALIST) (1706 :TYPE-PRESCRIPTION CURRENT-PACKAGE) (1705 :EXECUTABLE-COUNTERPART CURRENT-PACKAGE) (1704 :DEFINITION CURRENT-PACKAGE) (1703 :TYPE-PRESCRIPTION W) (1702 :EXECUTABLE-COUNTERPART W) (1701 :DEFINITION W) (1700 :TYPE-PRESCRIPTION PRIN1$) (1699 :EXECUTABLE-COUNTERPART PRIN1$) (1698 :DEFINITION PRIN1$) (1697 :TYPE-PRESCRIPTION PRINT-TIMER) (1696 :EXECUTABLE-COUNTERPART PRINT-TIMER) (1695 :DEFINITION PRINT-TIMER) (1694 :TYPE-PRESCRIPTION PRINT-RATIONAL-AS-DECIMAL) (1693 :EXECUTABLE-COUNTERPART PRINT-RATIONAL-AS-DECIMAL) (1692 :DEFINITION PRINT-RATIONAL-AS-DECIMAL) (1691 :TYPE-PRESCRIPTION INCREMENT-TIMER) (1690 :EXECUTABLE-COUNTERPART INCREMENT-TIMER) (1689 :DEFINITION INCREMENT-TIMER) (1688 :FORWARD-CHAINING STATE-P1-UPDATE-MAIN-TIMER) (1687 :REWRITE ADD-PAIR-PRESERVES-ALL-BOUNDP) (1686 :REWRITE ASSOC-ADD-PAIR) (1685 :FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD) (1684 :TYPE-PRESCRIPTION MAIN-TIMER-TYPE-PRESCRIPTION) (1683 :REWRITE NTH-ADD1) (1682 :REWRITE NTH-0-CONS) (1681 :TYPE-PRESCRIPTION ADD-TIMERS) (1680 :EXECUTABLE-COUNTERPART ADD-TIMERS) (1679 :DEFINITION ADD-TIMERS) (1678 :TYPE-PRESCRIPTION POP-TIMER) (1677 :EXECUTABLE-COUNTERPART POP-TIMER) (1676 :DEFINITION POP-TIMER) (1675 :REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP) (1674 :REWRITE RATIONALP-UNARY-/) (1673 :REWRITE RATIONALP-UNARY--) (1672 :REWRITE RATIONALP-*) (1671 :REWRITE RATIONALP-+) (1670 :TYPE-PRESCRIPTION PUSH-TIMER) (1669 :EXECUTABLE-COUNTERPART PUSH-TIMER) (1668 :DEFINITION PUSH-TIMER) (1667 :TYPE-PRESCRIPTION GET-TIMER) (1666 :EXECUTABLE-COUNTERPART GET-TIMER) (1665 :DEFINITION GET-TIMER) (1664 :TYPE-PRESCRIPTION SET-TIMER) (1663 :EXECUTABLE-COUNTERPART SET-TIMER) (1662 :DEFINITION SET-TIMER) (1661 :INDUCTION PUT-ASSOC-EQUAL) (1660 :TYPE-PRESCRIPTION PUT-ASSOC-EQUAL) (1659 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQUAL) (1658 :DEFINITION PUT-ASSOC-EQUAL) (1657 :INDUCTION PUT-ASSOC-EQL) (1656 :TYPE-PRESCRIPTION PUT-ASSOC-EQL) (1655 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQL) (1654 :DEFINITION PUT-ASSOC-EQL) (1653 :INDUCTION PUT-ASSOC-EQ) (1652 :TYPE-PRESCRIPTION PUT-ASSOC-EQ) (1651 :EXECUTABLE-COUNTERPART PUT-ASSOC-EQ) (1650 :DEFINITION PUT-ASSOC-EQ) (1649 :TYPE-PRESCRIPTION MAIN-TIMER) (1648 :EXECUTABLE-COUNTERPART MAIN-TIMER) (1647 :DEFINITION MAIN-TIMER) (1646 :TYPE-PRESCRIPTION NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION) (1645 :FORWARD-CHAINING READ-ACL2-ORACLE-PRESERVES-STATE-P1) (1644 :FORWARD-CHAINING READ-RUN-TIME-PRESERVES-STATE-P1) (1643 :REWRITE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1) (1642 :REWRITE LEN-UPDATE-NTH) (1639 :TYPE-PRESCRIPTION RANDOM$) (1638 :EXECUTABLE-COUNTERPART RANDOM$) (1636 :TYPE-PRESCRIPTION SETENV$) (1635 :EXECUTABLE-COUNTERPART SETENV$) (1634 :DEFINITION SETENV$) (1633 :TYPE-PRESCRIPTION GETENV$) (1632 :EXECUTABLE-COUNTERPART GETENV$) (1631 :DEFINITION GETENV$) (1630 :TYPE-PRESCRIPTION READ-ACL2-ORACLE) (1629 :EXECUTABLE-COUNTERPART READ-ACL2-ORACLE) (1627 :TYPE-PRESCRIPTION READ-RUN-TIME) (1626 :EXECUTABLE-COUNTERPART READ-RUN-TIME) (1624 :TYPE-PRESCRIPTION READ-IDATE) (1623 :EXECUTABLE-COUNTERPART READ-IDATE) (1622 :DEFINITION READ-IDATE) (1621 :INDUCTION POWER-EVAL) (1620 :TYPE-PRESCRIPTION POWER-EVAL) (1619 :EXECUTABLE-COUNTERPART POWER-EVAL) (1618 :DEFINITION POWER-EVAL) (1617 :TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST) (1616 :EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST) (1615 :DEFINITION UPDATE-USER-STOBJ-ALIST) (1614 :TYPE-PRESCRIPTION USER-STOBJ-ALIST) (1613 :EXECUTABLE-COUNTERPART USER-STOBJ-ALIST) (1612 :DEFINITION USER-STOBJ-ALIST) (1611 :TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES) (1610 :EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES) (1609 :DEFINITION LIST-ALL-PACKAGE-NAMES) (1608 :TYPE-PRESCRIPTION DECREMENT-BIG-CLOCK) (1607 :EXECUTABLE-COUNTERPART DECREMENT-BIG-CLOCK) (1606 :DEFINITION DECREMENT-BIG-CLOCK) (1605 :TYPE-PRESCRIPTION BIG-CLOCK-NEGATIVE-P) (1604 :EXECUTABLE-COUNTERPART BIG-CLOCK-NEGATIVE-P) (1603 :DEFINITION BIG-CLOCK-NEGATIVE-P) (1602 :TYPE-PRESCRIPTION ASET-32-BIT-INTEGER-STACK) (1601 :EXECUTABLE-COUNTERPART ASET-32-BIT-INTEGER-STACK) (1600 :DEFINITION ASET-32-BIT-INTEGER-STACK) (1599 :TYPE-PRESCRIPTION AREF-32-BIT-INTEGER-STACK) (1598 :EXECUTABLE-COUNTERPART AREF-32-BIT-INTEGER-STACK) (1597 :DEFINITION AREF-32-BIT-INTEGER-STACK) (1596 :TYPE-PRESCRIPTION SHRINK-32-BIT-INTEGER-STACK) (1595 :EXECUTABLE-COUNTERPART SHRINK-32-BIT-INTEGER-STACK) (1594 :DEFINITION SHRINK-32-BIT-INTEGER-STACK) (1593 :TYPE-PRESCRIPTION EXTEND-32-BIT-INTEGER-STACK) (1592 :EXECUTABLE-COUNTERPART EXTEND-32-BIT-INTEGER-STACK) (1591 :DEFINITION EXTEND-32-BIT-INTEGER-STACK) (1590 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH) (1589 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH) (1588 :DEFINITION 32-BIT-INTEGER-STACK-LENGTH) (1587 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH1) (1586 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH1) (1585 :DEFINITION 32-BIT-INTEGER-STACK-LENGTH1) (1584 :TYPE-PRESCRIPTION ASET-T-STACK) (1583 :EXECUTABLE-COUNTERPART ASET-T-STACK) (1582 :DEFINITION ASET-T-STACK) (1581 :TYPE-PRESCRIPTION AREF-T-STACK) (1580 :EXECUTABLE-COUNTERPART AREF-T-STACK) (1579 :DEFINITION AREF-T-STACK) (1578 :TYPE-PRESCRIPTION SHRINK-T-STACK) (1577 :EXECUTABLE-COUNTERPART SHRINK-T-STACK) (1576 :DEFINITION SHRINK-T-STACK) (1575 :TYPE-PRESCRIPTION SUBSEQ) (1574 :EXECUTABLE-COUNTERPART SUBSEQ) (1573 :DEFINITION SUBSEQ) (1572 :TYPE-PRESCRIPTION SUBSEQ-LIST) (1571 :EXECUTABLE-COUNTERPART SUBSEQ-LIST) (1570 :DEFINITION SUBSEQ-LIST) (1569 :TYPE-PRESCRIPTION EXTEND-T-STACK) (1568 :EXECUTABLE-COUNTERPART EXTEND-T-STACK) (1567 :DEFINITION EXTEND-T-STACK) (1566 :INDUCTION MAKE-LIST-AC) (1565 :TYPE-PRESCRIPTION MAKE-LIST-AC) (1564 :EXECUTABLE-COUNTERPART MAKE-LIST-AC) (1563 :DEFINITION MAKE-LIST-AC) (1562 :TYPE-PRESCRIPTION T-STACK-LENGTH) (1561 :EXECUTABLE-COUNTERPART T-STACK-LENGTH) (1560 :DEFINITION T-STACK-LENGTH) (1559 :TYPE-PRESCRIPTION T-STACK-LENGTH1) (1558 :EXECUTABLE-COUNTERPART T-STACK-LENGTH1) (1557 :DEFINITION T-STACK-LENGTH1) (1556 :TYPE-PRESCRIPTION NEEDS-SLASHES) (1555 :EXECUTABLE-COUNTERPART NEEDS-SLASHES) (1554 :DEFINITION NEEDS-SLASHES) (1553 :TYPE-PRESCRIPTION MAY-NEED-SLASHES-FN) (1552 :EXECUTABLE-COUNTERPART MAY-NEED-SLASHES-FN) (1551 :DEFINITION MAY-NEED-SLASHES-FN) (1550 :INDUCTION MAY-NEED-SLASHES1) (1549 :TYPE-PRESCRIPTION MAY-NEED-SLASHES1) (1548 :EXECUTABLE-COUNTERPART MAY-NEED-SLASHES1) (1547 :DEFINITION MAY-NEED-SLASHES1) (1546 :TYPE-PRESCRIPTION PRIN1-WITH-SLASHES) (1545 :EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES) (1544 :DEFINITION PRIN1-WITH-SLASHES) (1543 :INDUCTION PRIN1-WITH-SLASHES1) (1542 :TYPE-PRESCRIPTION PRIN1-WITH-SLASHES1) (1541 :EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES1) (1540 :DEFINITION PRIN1-WITH-SLASHES1) (1539 :INDUCTION SOME-SLASHABLE) (1538 :TYPE-PRESCRIPTION SOME-SLASHABLE) (1537 :EXECUTABLE-COUNTERPART SOME-SLASHABLE) (1536 :DEFINITION SOME-SLASHABLE) (1535 :TYPE-PRESCRIPTION READ-OBJECT) (1534 :EXECUTABLE-COUNTERPART READ-OBJECT) (1533 :DEFINITION READ-OBJECT) (1532 :TYPE-PRESCRIPTION READ-BYTE$) (1531 :EXECUTABLE-COUNTERPART READ-BYTE$) (1530 :DEFINITION READ-BYTE$) (1529 :TYPE-PRESCRIPTION PEEK-CHAR$) (1528 :EXECUTABLE-COUNTERPART PEEK-CHAR$) (1527 :DEFINITION PEEK-CHAR$) (1526 :TYPE-PRESCRIPTION READ-CHAR$) (1525 :EXECUTABLE-COUNTERPART READ-CHAR$) (1524 :DEFINITION READ-CHAR$) (1523 :TYPE-PRESCRIPTION CLOSE-OUTPUT-CHANNEL) (1522 :EXECUTABLE-COUNTERPART CLOSE-OUTPUT-CHANNEL) (1521 :DEFINITION CLOSE-OUTPUT-CHANNEL) (1520 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL!) (1519 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL!) (1518 :DEFINITION OPEN-OUTPUT-CHANNEL!) (1517 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL) (1516 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL) (1515 :DEFINITION OPEN-OUTPUT-CHANNEL) (1514 :TYPE-PRESCRIPTION CLOSE-INPUT-CHANNEL) (1513 :EXECUTABLE-COUNTERPART CLOSE-INPUT-CHANNEL) (1512 :DEFINITION CLOSE-INPUT-CHANNEL) (1511 :REWRITE NTH-UPDATE-NTH-ARRAY) (1510 :TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH) (1509 :REWRITE NTH-UPDATE-NTH) (1508 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL) (1507 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL) (1506 :DEFINITION OPEN-INPUT-CHANNEL) (1505 :TYPE-PRESCRIPTION MAKE-OUTPUT-CHANNEL) (1504 :EXECUTABLE-COUNTERPART MAKE-OUTPUT-CHANNEL) (1503 :DEFINITION MAKE-OUTPUT-CHANNEL) (1502 :TYPE-PRESCRIPTION MAKE-INPUT-CHANNEL) (1501 :EXECUTABLE-COUNTERPART MAKE-INPUT-CHANNEL) (1500 :DEFINITION MAKE-INPUT-CHANNEL) (1499 :TYPE-PRESCRIPTION PRINT-OBJECT$) (1498 :EXECUTABLE-COUNTERPART PRINT-OBJECT$) (1497 :DEFINITION PRINT-OBJECT$) (1496 :TYPE-PRESCRIPTION WRITE-BYTE$) (1495 :EXECUTABLE-COUNTERPART WRITE-BYTE$) (1494 :DEFINITION WRITE-BYTE$) (1493 :TYPE-PRESCRIPTION PRINC$) (1492 :EXECUTABLE-COUNTERPART PRINC$) (1491 :DEFINITION PRINC$) (1490 :TYPE-PRESCRIPTION SET-PRINT-RIGHT-MARGIN) (1489 :EXECUTABLE-COUNTERPART SET-PRINT-RIGHT-MARGIN) (1488 :DEFINITION SET-PRINT-RIGHT-MARGIN) (1487 :TYPE-PRESCRIPTION SET-PRINT-LINES) (1486 :EXECUTABLE-COUNTERPART SET-PRINT-LINES) (1485 :DEFINITION SET-PRINT-LINES) (1484 :TYPE-PRESCRIPTION SET-PRINT-LEVEL) (1483 :EXECUTABLE-COUNTERPART SET-PRINT-LEVEL) (1482 :DEFINITION SET-PRINT-LEVEL) (1481 :TYPE-PRESCRIPTION SET-PRINT-LENGTH) (1480 :EXECUTABLE-COUNTERPART SET-PRINT-LENGTH) (1479 :DEFINITION SET-PRINT-LENGTH) (1478 :TYPE-PRESCRIPTION CHECK-NULL-OR-NATP) (1477 :EXECUTABLE-COUNTERPART CHECK-NULL-OR-NATP) (1476 :DEFINITION CHECK-NULL-OR-NATP) (1475 :TYPE-PRESCRIPTION SET-PRINT-READABLY) (1474 :EXECUTABLE-COUNTERPART SET-PRINT-READABLY) (1473 :DEFINITION SET-PRINT-READABLY) (1472 :TYPE-PRESCRIPTION SET-PRINT-RADIX) (1471 :EXECUTABLE-COUNTERPART SET-PRINT-RADIX) (1470 :DEFINITION SET-PRINT-RADIX) (1469 :TYPE-PRESCRIPTION SET-PRINT-PRETTY) (1468 :EXECUTABLE-COUNTERPART SET-PRINT-PRETTY) (1467 :DEFINITION SET-PRINT-PRETTY) (1466 :TYPE-PRESCRIPTION SET-PRINT-ESCAPE) (1465 :EXECUTABLE-COUNTERPART SET-PRINT-ESCAPE) (1464 :DEFINITION SET-PRINT-ESCAPE) (1463 :TYPE-PRESCRIPTION SET-PRINT-CIRCLE) (1462 :EXECUTABLE-COUNTERPART SET-PRINT-CIRCLE) (1461 :DEFINITION SET-PRINT-CIRCLE) (1460 :TYPE-PRESCRIPTION SET-PRINT-BASE) (1459 :EXECUTABLE-COUNTERPART SET-PRINT-BASE) (1458 :DEFINITION SET-PRINT-BASE) (1457 :TYPE-PRESCRIPTION CHECK-PRINT-BASE) (1456 :EXECUTABLE-COUNTERPART CHECK-PRINT-BASE) (1455 :DEFINITION CHECK-PRINT-BASE) (1454 :TYPE-PRESCRIPTION SET-PRINT-CASE) (1453 :EXECUTABLE-COUNTERPART SET-PRINT-CASE) (1452 :DEFINITION SET-PRINT-CASE) (1451 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P) (1450 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P) (1449 :DEFINITION OPEN-INPUT-CHANNEL-ANY-P) (1448 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P1) (1447 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P1) (1446 :DEFINITION OPEN-INPUT-CHANNEL-ANY-P1) (1445 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P) (1444 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P) (1443 :DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P) (1442 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P1) (1441 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P1) (1440 :DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P1) (1439 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P) (1438 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P) (1437 :DEFINITION OPEN-OUTPUT-CHANNEL-P) (1436 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P) (1435 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P) (1434 :DEFINITION OPEN-INPUT-CHANNEL-P) (1433 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P1) (1432 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P1) (1431 :DEFINITION OPEN-OUTPUT-CHANNEL-P1) (1430 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P1) (1429 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P1) (1428 :DEFINITION OPEN-INPUT-CHANNEL-P1) (1427 :FORWARD-CHAINING TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P) (1426 :TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ) (1425 :INDUCTION EXPLODE-ATOM) (1424 :TYPE-PRESCRIPTION EXPLODE-ATOM) (1423 :EXECUTABLE-COUNTERPART EXPLODE-ATOM) (1422 :DEFINITION EXPLODE-ATOM) (1421 :INDUCTION EXPLODE-NONNEGATIVE-INTEGER) (1420 :TYPE-PRESCRIPTION EXPLODE-NONNEGATIVE-INTEGER) (1419 :EXECUTABLE-COUNTERPART EXPLODE-NONNEGATIVE-INTEGER) (1418 :DEFINITION EXPLODE-NONNEGATIVE-INTEGER) (1417 :TYPE-PRESCRIPTION PRINT-BASE-P) (1416 :EXECUTABLE-COUNTERPART PRINT-BASE-P) (1415 :DEFINITION PRINT-BASE-P) (1414 :TYPE-PRESCRIPTION DIGIT-TO-CHAR) (1413 :EXECUTABLE-COUNTERPART DIGIT-TO-CHAR) (1412 :DEFINITION DIGIT-TO-CHAR) (1411 :INDUCTION ALIST-DIFFERENCE-EQ) (1410 :TYPE-PRESCRIPTION ALIST-DIFFERENCE-EQ) (1409 :EXECUTABLE-COUNTERPART ALIST-DIFFERENCE-EQ) (1408 :DEFINITION ALIST-DIFFERENCE-EQ) (1407 :INDUCTION SET-FORMS-FROM-BINDINGS) (1406 :TYPE-PRESCRIPTION SET-FORMS-FROM-BINDINGS) (1405 :EXECUTABLE-COUNTERPART SET-FORMS-FROM-BINDINGS) (1404 :DEFINITION SET-FORMS-FROM-BINDINGS) (1403 :TYPE-PRESCRIPTION BOOLE$) (1402 :EXECUTABLE-COUNTERPART BOOLE$) (1401 :DEFINITION BOOLE$) (1400 :TYPE-PRESCRIPTION LOGTEST) (1399 :EXECUTABLE-COUNTERPART LOGTEST) (1398 :DEFINITION LOGTEST) (1397 :TYPE-PRESCRIPTION LOGNOR) (1396 :EXECUTABLE-COUNTERPART LOGNOR) (1395 :DEFINITION LOGNOR) (1394 :TYPE-PRESCRIPTION BINARY-LOGXOR) (1393 :EXECUTABLE-COUNTERPART BINARY-LOGXOR) (1392 :DEFINITION BINARY-LOGXOR) (1391 :TYPE-PRESCRIPTION BINARY-LOGEQV) (1390 :EXECUTABLE-COUNTERPART BINARY-LOGEQV) (1389 :DEFINITION BINARY-LOGEQV) (1388 :TYPE-PRESCRIPTION LOGANDC2) (1387 :EXECUTABLE-COUNTERPART LOGANDC2) (1386 :DEFINITION LOGANDC2) (1385 :TYPE-PRESCRIPTION LOGANDC1) (1384 :EXECUTABLE-COUNTERPART LOGANDC1) (1383 :DEFINITION LOGANDC1) (1382 :TYPE-PRESCRIPTION LOGORC2) (1381 :EXECUTABLE-COUNTERPART LOGORC2) (1380 :DEFINITION LOGORC2) (1379 :TYPE-PRESCRIPTION LOGORC1) (1378 :EXECUTABLE-COUNTERPART LOGORC1) (1377 :DEFINITION LOGORC1) (1376 :TYPE-PRESCRIPTION BINARY-LOGIOR) (1375 :EXECUTABLE-COUNTERPART BINARY-LOGIOR) (1374 :DEFINITION BINARY-LOGIOR) (1373 :TYPE-PRESCRIPTION LOGNAND) (1372 :EXECUTABLE-COUNTERPART LOGNAND) (1371 :DEFINITION LOGNAND) (1370 :INDUCTION BINARY-LOGAND) (1369 :TYPE-PRESCRIPTION BINARY-LOGAND) (1368 :EXECUTABLE-COUNTERPART BINARY-LOGAND) (1367 :DEFINITION BINARY-LOGAND) (1366 :INDUCTION INTEGER-LENGTH) (1365 :TYPE-PRESCRIPTION INTEGER-LENGTH) (1364 :EXECUTABLE-COUNTERPART INTEGER-LENGTH) (1363 :DEFINITION INTEGER-LENGTH) (1362 :REWRITE ORDERED-SYMBOL-ALISTP-GETPROPS) (1361 :REWRITE ORDERED-SYMBOL-ALISTP-ADD-PAIR) (1360 :REWRITE SYMBOL-<-IRREFLEXIVE) (1359 :REWRITE ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR) (1358 :REWRITE SYMBOL-<-TRICHOTOMY) (1357 :REWRITE STRING<-L-TRICHOTOMY) (1356 :REWRITE SYMBOL-<-TRANSITIVE) (1355 :REWRITE STRING<-L-TRANSITIVE) (1354 :REWRITE SYMBOL-<-ASYMMETRIC) (1353 :REWRITE STRING<-L-ASYMMETRIC) (1352 :TYPE-PRESCRIPTION ZPF) (1351 :EXECUTABLE-COUNTERPART ZPF) (1350 :DEFINITION ZPF) (1349 :FORWARD-CHAINING UNSIGNED-BYTE-P-FORWARD-TO-NONNEGATIVE-INTEGERP) (1348 :FORWARD-CHAINING SIGNED-BYTE-P-FORWARD-TO-INTEGERP) (1347 :FORWARD-CHAINING INTEGER-RANGE-P-FORWARD) (1346 :TYPE-PRESCRIPTION UNSIGNED-BYTE-P) (1345 :EXECUTABLE-COUNTERPART UNSIGNED-BYTE-P) (1344 :DEFINITION UNSIGNED-BYTE-P) (1343 :TYPE-PRESCRIPTION SIGNED-BYTE-P) (1342 :EXECUTABLE-COUNTERPART SIGNED-BYTE-P) (1341 :DEFINITION SIGNED-BYTE-P) (1340 :TYPE-PRESCRIPTION INTEGER-RANGE-P) (1339 :EXECUTABLE-COUNTERPART INTEGER-RANGE-P) (1338 :DEFINITION INTEGER-RANGE-P) (1337 :INDUCTION STATE-GLOBAL-LET*-CLEANUP) (1336 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-CLEANUP) (1335 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-CLEANUP) (1334 :DEFINITION STATE-GLOBAL-LET*-CLEANUP) (1333 :INDUCTION STATE-GLOBAL-LET*-PUT-GLOBALS) (1332 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-PUT-GLOBALS) (1331 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-PUT-GLOBALS) (1330 :DEFINITION STATE-GLOBAL-LET*-PUT-GLOBALS) (1329 :INDUCTION STATE-GLOBAL-LET*-GET-GLOBALS) (1328 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-GET-GLOBALS) (1327 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-GET-GLOBALS) (1326 :DEFINITION STATE-GLOBAL-LET*-GET-GLOBALS) (1325 :INDUCTION STATE-GLOBAL-LET*-BINDINGS-P) (1324 :TYPE-PRESCRIPTION STATE-GLOBAL-LET*-BINDINGS-P) (1323 :EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-BINDINGS-P) (1322 :DEFINITION STATE-GLOBAL-LET*-BINDINGS-P) (1321 :TYPE-PRESCRIPTION ALWAYS-BOUNDP-GLOBAL) (1320 :EXECUTABLE-COUNTERPART ALWAYS-BOUNDP-GLOBAL) (1319 :DEFINITION ALWAYS-BOUNDP-GLOBAL) (1318 :INDUCTION SYMBOL-DOUBLET-LISTP) (1317 :TYPE-PRESCRIPTION SYMBOL-DOUBLET-LISTP) (1316 :EXECUTABLE-COUNTERPART SYMBOL-DOUBLET-LISTP) (1315 :DEFINITION SYMBOL-DOUBLET-LISTP) (1314 :TYPE-PRESCRIPTION PUT-GLOBAL) (1313 :EXECUTABLE-COUNTERPART PUT-GLOBAL) (1312 :DEFINITION PUT-GLOBAL) (1311 :TYPE-PRESCRIPTION GET-GLOBAL) (1310 :EXECUTABLE-COUNTERPART GET-GLOBAL) (1309 :DEFINITION GET-GLOBAL) (1308 :TYPE-PRESCRIPTION MAKUNBOUND-GLOBAL) (1307 :EXECUTABLE-COUNTERPART MAKUNBOUND-GLOBAL) (1306 :DEFINITION MAKUNBOUND-GLOBAL) (1305 :INDUCTION DELETE-PAIR) (1304 :TYPE-PRESCRIPTION DELETE-PAIR) (1303 :EXECUTABLE-COUNTERPART DELETE-PAIR) (1302 :DEFINITION DELETE-PAIR) (1301 :TYPE-PRESCRIPTION BOUNDP-GLOBAL) (1300 :EXECUTABLE-COUNTERPART BOUNDP-GLOBAL) (1299 :DEFINITION BOUNDP-GLOBAL) (1298 :TYPE-PRESCRIPTION BOUNDP-GLOBAL1) (1297 :EXECUTABLE-COUNTERPART BOUNDP-GLOBAL1) (1296 :DEFINITION BOUNDP-GLOBAL1) (1295 :TYPE-PRESCRIPTION GLOBAL-TABLE-CARS) (1294 :EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS) (1293 :DEFINITION GLOBAL-TABLE-CARS) (1292 :TYPE-PRESCRIPTION GLOBAL-TABLE-CARS1) (1291 :EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS1) (1290 :DEFINITION GLOBAL-TABLE-CARS1) (1289 :TYPE-PRESCRIPTION COERCE-OBJECT-TO-STATE) (1288 :EXECUTABLE-COUNTERPART COERCE-OBJECT-TO-STATE) (1287 :DEFINITION COERCE-OBJECT-TO-STATE) (1286 :TYPE-PRESCRIPTION COERCE-STATE-TO-OBJECT) (1285 :EXECUTABLE-COUNTERPART COERCE-STATE-TO-OBJECT) (1284 :DEFINITION COERCE-STATE-TO-OBJECT) (1283 :TYPE-PRESCRIPTION BUILD-STATE1) (1282 :EXECUTABLE-COUNTERPART BUILD-STATE1) (1281 :DEFINITION BUILD-STATE1) (1280 :REWRITE STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (1279 :FORWARD-CHAINING STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (1278 :TYPE-PRESCRIPTION STATE-P) (1277 :EXECUTABLE-COUNTERPART STATE-P) (1276 :DEFINITION STATE-P) (1275 :FORWARD-CHAINING STATE-P1-FORWARD) (1274 :TYPE-PRESCRIPTION STATE-P1) (1273 :EXECUTABLE-COUNTERPART STATE-P1) (1271 :FORWARD-CHAINING WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP) (1270 :TYPE-PRESCRIPTION WRITEABLE-FILES-P) (1269 :EXECUTABLE-COUNTERPART WRITEABLE-FILES-P) (1268 :DEFINITION WRITEABLE-FILES-P) (1267 :FORWARD-CHAINING WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (1266 :INDUCTION WRITABLE-FILE-LISTP) (1265 :TYPE-PRESCRIPTION WRITABLE-FILE-LISTP) (1264 :EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP) (1263 :DEFINITION WRITABLE-FILE-LISTP) (1262 :FORWARD-CHAINING WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1261 :TYPE-PRESCRIPTION WRITABLE-FILE-LISTP1) (1260 :EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP1) (1259 :DEFINITION WRITABLE-FILE-LISTP1) (1258 :FORWARD-CHAINING READ-FILES-P-FORWARD-TO-READ-FILE-LISTP) (1257 :TYPE-PRESCRIPTION READ-FILES-P) (1256 :EXECUTABLE-COUNTERPART READ-FILES-P) (1255 :DEFINITION READ-FILES-P) (1254 :FORWARD-CHAINING READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (1253 :INDUCTION READ-FILE-LISTP) (1252 :TYPE-PRESCRIPTION READ-FILE-LISTP) (1251 :EXECUTABLE-COUNTERPART READ-FILE-LISTP) (1250 :DEFINITION READ-FILE-LISTP) (1249 :FORWARD-CHAINING READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1248 :TYPE-PRESCRIPTION READ-FILE-LISTP1) (1247 :EXECUTABLE-COUNTERPART READ-FILE-LISTP1) (1246 :DEFINITION READ-FILE-LISTP1) (1245 :FORWARD-CHAINING WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP) (1244 :TYPE-PRESCRIPTION WRITTEN-FILES-P) (1243 :EXECUTABLE-COUNTERPART WRITTEN-FILES-P) (1242 :DEFINITION WRITTEN-FILES-P) (1241 :FORWARD-CHAINING WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1240 :INDUCTION WRITTEN-FILE-LISTP) (1239 :TYPE-PRESCRIPTION WRITTEN-FILE-LISTP) (1238 :EXECUTABLE-COUNTERPART WRITTEN-FILE-LISTP) (1237 :DEFINITION WRITTEN-FILE-LISTP) (1236 :FORWARD-CHAINING WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1235 :TYPE-PRESCRIPTION WRITTEN-FILE) (1234 :EXECUTABLE-COUNTERPART WRITTEN-FILE) (1233 :DEFINITION WRITTEN-FILE) (1232 :FORWARD-CHAINING READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP) (1231 :TYPE-PRESCRIPTION READABLE-FILES-P) (1230 :EXECUTABLE-COUNTERPART READABLE-FILES-P) (1229 :DEFINITION READABLE-FILES-P) (1228 :FORWARD-CHAINING READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1227 :INDUCTION READABLE-FILES-LISTP) (1226 :TYPE-PRESCRIPTION READABLE-FILES-LISTP) (1225 :EXECUTABLE-COUNTERPART READABLE-FILES-LISTP) (1224 :DEFINITION READABLE-FILES-LISTP) (1223 :FORWARD-CHAINING READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1222 :TYPE-PRESCRIPTION READABLE-FILE) (1221 :EXECUTABLE-COUNTERPART READABLE-FILE) (1220 :DEFINITION READABLE-FILE) (1219 :FORWARD-CHAINING FILE-CLOCK-P-FORWARD-TO-INTEGERP) (1218 :TYPE-PRESCRIPTION FILE-CLOCK-P) (1217 :EXECUTABLE-COUNTERPART FILE-CLOCK-P) (1216 :DEFINITION FILE-CLOCK-P) (1215 :FORWARD-CHAINING OPEN-CHANNELS-P-FORWARD) (1214 :TYPE-PRESCRIPTION OPEN-CHANNELS-P) (1213 :EXECUTABLE-COUNTERPART OPEN-CHANNELS-P) (1212 :DEFINITION OPEN-CHANNELS-P) (1211 :INDUCTION OPEN-CHANNEL-LISTP) (1210 :TYPE-PRESCRIPTION OPEN-CHANNEL-LISTP) (1209 :EXECUTABLE-COUNTERPART OPEN-CHANNEL-LISTP) (1208 :DEFINITION OPEN-CHANNEL-LISTP) (1207 :FORWARD-CHAINING OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (1206 :TYPE-PRESCRIPTION OPEN-CHANNEL1) (1205 :EXECUTABLE-COUNTERPART OPEN-CHANNEL1) (1204 :DEFINITION OPEN-CHANNEL1) (1203 :FORWARD-CHAINING TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP) (1202 :INDUCTION TYPED-IO-LISTP) (1201 :TYPE-PRESCRIPTION TYPED-IO-LISTP) (1200 :EXECUTABLE-COUNTERPART TYPED-IO-LISTP) (1199 :DEFINITION TYPED-IO-LISTP) (1198 :FORWARD-CHAINING TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP) (1197 :INDUCTION TIMER-ALISTP) (1196 :TYPE-PRESCRIPTION TIMER-ALISTP) (1195 :EXECUTABLE-COUNTERPART TIMER-ALISTP) (1194 :DEFINITION TIMER-ALISTP) (1193 :FORWARD-CHAINING KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (1192 :INDUCTION KNOWN-PACKAGE-ALISTP) (1191 :TYPE-PRESCRIPTION KNOWN-PACKAGE-ALISTP) (1190 :EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALISTP) (1189 :DEFINITION KNOWN-PACKAGE-ALISTP) (1188 :INDUCTION ALL-BOUNDP) (1187 :TYPE-PRESCRIPTION ALL-BOUNDP) (1186 :EXECUTABLE-COUNTERPART ALL-BOUNDP) (1185 :DEFINITION ALL-BOUNDP) (1184 :TYPE-PRESCRIPTION INIT-IPRINT-AR) (1183 :EXECUTABLE-COUNTERPART INIT-IPRINT-AR) (1182 :DEFINITION INIT-IPRINT-AR) (1181 :TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST1) (1180 :EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST1) (1179 :DEFINITION UPDATE-USER-STOBJ-ALIST1) (1178 :TYPE-PRESCRIPTION USER-STOBJ-ALIST1) (1177 :EXECUTABLE-COUNTERPART USER-STOBJ-ALIST1) (1176 :DEFINITION USER-STOBJ-ALIST1) (1175 :TYPE-PRESCRIPTION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1174 :EXECUTABLE-COUNTERPART UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1173 :DEFINITION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (1172 :TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES-LST) (1171 :EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES-LST) (1170 :DEFINITION LIST-ALL-PACKAGE-NAMES-LST) (1169 :TYPE-PRESCRIPTION WRITEABLE-FILES) (1168 :EXECUTABLE-COUNTERPART WRITEABLE-FILES) (1167 :DEFINITION WRITEABLE-FILES) (1166 :TYPE-PRESCRIPTION UPDATE-READ-FILES) (1165 :EXECUTABLE-COUNTERPART UPDATE-READ-FILES) (1164 :DEFINITION UPDATE-READ-FILES) (1163 :TYPE-PRESCRIPTION READ-FILES) (1162 :EXECUTABLE-COUNTERPART READ-FILES) (1161 :DEFINITION READ-FILES) (1160 :TYPE-PRESCRIPTION UPDATE-WRITTEN-FILES) (1159 :EXECUTABLE-COUNTERPART UPDATE-WRITTEN-FILES) (1158 :DEFINITION UPDATE-WRITTEN-FILES) (1157 :TYPE-PRESCRIPTION WRITTEN-FILES) (1156 :EXECUTABLE-COUNTERPART WRITTEN-FILES) (1155 :DEFINITION WRITTEN-FILES) (1154 :TYPE-PRESCRIPTION READABLE-FILES) (1153 :EXECUTABLE-COUNTERPART READABLE-FILES) (1152 :DEFINITION READABLE-FILES) (1151 :TYPE-PRESCRIPTION UPDATE-FILE-CLOCK) (1150 :EXECUTABLE-COUNTERPART UPDATE-FILE-CLOCK) (1149 :DEFINITION UPDATE-FILE-CLOCK) (1148 :TYPE-PRESCRIPTION FILE-CLOCK) (1147 :EXECUTABLE-COUNTERPART FILE-CLOCK) (1146 :DEFINITION FILE-CLOCK) (1145 :TYPE-PRESCRIPTION UPDATE-ACL2-ORACLE) (1144 :EXECUTABLE-COUNTERPART UPDATE-ACL2-ORACLE) (1142 :TYPE-PRESCRIPTION ACL2-ORACLE) (1141 :EXECUTABLE-COUNTERPART ACL2-ORACLE) (1140 :DEFINITION ACL2-ORACLE) (1139 :TYPE-PRESCRIPTION UPDATE-IDATES) (1138 :EXECUTABLE-COUNTERPART UPDATE-IDATES) (1137 :DEFINITION UPDATE-IDATES) (1136 :TYPE-PRESCRIPTION IDATES) (1135 :EXECUTABLE-COUNTERPART IDATES) (1134 :DEFINITION IDATES) (1133 :TYPE-PRESCRIPTION UPDATE-BIG-CLOCK-ENTRY) (1132 :EXECUTABLE-COUNTERPART UPDATE-BIG-CLOCK-ENTRY) (1131 :DEFINITION UPDATE-BIG-CLOCK-ENTRY) (1130 :TYPE-PRESCRIPTION BIG-CLOCK-ENTRY) (1129 :EXECUTABLE-COUNTERPART BIG-CLOCK-ENTRY) (1128 :DEFINITION BIG-CLOCK-ENTRY) (1127 :TYPE-PRESCRIPTION UPDATE-32-BIT-INTEGER-STACK) (1126 :EXECUTABLE-COUNTERPART UPDATE-32-BIT-INTEGER-STACK) (1125 :DEFINITION UPDATE-32-BIT-INTEGER-STACK) (1124 :TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK) (1123 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK) (1122 :DEFINITION 32-BIT-INTEGER-STACK) (1121 :TYPE-PRESCRIPTION UPDATE-T-STACK) (1120 :EXECUTABLE-COUNTERPART UPDATE-T-STACK) (1119 :DEFINITION UPDATE-T-STACK) (1118 :TYPE-PRESCRIPTION T-STACK) (1117 :EXECUTABLE-COUNTERPART T-STACK) (1116 :DEFINITION T-STACK) (1115 :TYPE-PRESCRIPTION UPDATE-GLOBAL-TABLE) (1114 :EXECUTABLE-COUNTERPART UPDATE-GLOBAL-TABLE) (1113 :DEFINITION UPDATE-GLOBAL-TABLE) (1112 :TYPE-PRESCRIPTION GLOBAL-TABLE) (1111 :EXECUTABLE-COUNTERPART GLOBAL-TABLE) (1110 :DEFINITION GLOBAL-TABLE) (1109 :TYPE-PRESCRIPTION UPDATE-OPEN-OUTPUT-CHANNELS) (1108 :EXECUTABLE-COUNTERPART UPDATE-OPEN-OUTPUT-CHANNELS) (1107 :DEFINITION UPDATE-OPEN-OUTPUT-CHANNELS) (1106 :TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNELS) (1105 :EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNELS) (1104 :DEFINITION OPEN-OUTPUT-CHANNELS) (1103 :TYPE-PRESCRIPTION UPDATE-OPEN-INPUT-CHANNELS) (1102 :EXECUTABLE-COUNTERPART UPDATE-OPEN-INPUT-CHANNELS) (1101 :DEFINITION UPDATE-OPEN-INPUT-CHANNELS) (1100 :TYPE-PRESCRIPTION OPEN-INPUT-CHANNELS) (1099 :EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNELS) (1098 :DEFINITION OPEN-INPUT-CHANNELS) (1097 :FORWARD-CHAINING 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP) (1096 :INDUCTION 32-BIT-INTEGER-LISTP) (1095 :TYPE-PRESCRIPTION 32-BIT-INTEGER-LISTP) (1094 :EXECUTABLE-COUNTERPART 32-BIT-INTEGER-LISTP) (1093 :DEFINITION 32-BIT-INTEGER-LISTP) (1092 :FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP) (1091 :INDUCTION INTEGER-LISTP) (1090 :TYPE-PRESCRIPTION INTEGER-LISTP) (1089 :EXECUTABLE-COUNTERPART INTEGER-LISTP) (1088 :DEFINITION INTEGER-LISTP) (1087 :FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP) (1086 :INDUCTION RATIONAL-LISTP) (1085 :TYPE-PRESCRIPTION RATIONAL-LISTP) (1084 :EXECUTABLE-COUNTERPART RATIONAL-LISTP) (1083 :DEFINITION RATIONAL-LISTP) (1082 :FORWARD-CHAINING 32-BIT-INTEGERP-FORWARD-TO-INTEGERP) (1081 :TYPE-PRESCRIPTION 32-BIT-INTEGERP) (1080 :EXECUTABLE-COUNTERPART 32-BIT-INTEGERP) (1079 :DEFINITION 32-BIT-INTEGERP) (1078 :TYPE-PRESCRIPTION UPDATE-NTH-ARRAY) (1077 :EXECUTABLE-COUNTERPART UPDATE-NTH-ARRAY) (1076 :DEFINITION UPDATE-NTH-ARRAY) (1075 :INDUCTION UPDATE-NTH) (1074 :TYPE-PRESCRIPTION UPDATE-NTH) (1073 :EXECUTABLE-COUNTERPART UPDATE-NTH) (1072 :DEFINITION UPDATE-NTH) (1071 :INDUCTION MAKE-MV-NTHS) (1070 :TYPE-PRESCRIPTION MAKE-MV-NTHS) (1069 :EXECUTABLE-COUNTERPART MAKE-MV-NTHS) (1068 :DEFINITION MAKE-MV-NTHS) (1067 :INDUCTION MV-NTH) (1066 :TYPE-PRESCRIPTION MV-NTH) (1065 :EXECUTABLE-COUNTERPART MV-NTH) (1064 :DEFINITION MV-NTH) (1063 :INDUCTION CDRN) (1062 :TYPE-PRESCRIPTION CDRN) (1061 :EXECUTABLE-COUNTERPART CDRN) (1060 :DEFINITION CDRN) (1059 :TYPE-PRESCRIPTION FLUSH-COMPRESS) (1058 :EXECUTABLE-COUNTERPART FLUSH-COMPRESS) (1057 :DEFINITION FLUSH-COMPRESS) (1056 :TYPE-PRESCRIPTION ASET2) (1055 :EXECUTABLE-COUNTERPART ASET2) (1054 :DEFINITION ASET2) (1053 :REWRITE ARRAY2P-CONS) (1052 :TYPE-PRESCRIPTION COMPRESS2) (1051 :EXECUTABLE-COUNTERPART COMPRESS2) (1050 :DEFINITION COMPRESS2) (1049 :INDUCTION COMPRESS21) (1048 :TYPE-PRESCRIPTION COMPRESS21) (1047 :EXECUTABLE-COUNTERPART COMPRESS21) (1046 :DEFINITION COMPRESS21) (1045 :INDUCTION COMPRESS211) (1044 :TYPE-PRESCRIPTION COMPRESS211) (1043 :EXECUTABLE-COUNTERPART COMPRESS211) (1042 :DEFINITION COMPRESS211) (1041 :TYPE-PRESCRIPTION AREF2) (1040 :EXECUTABLE-COUNTERPART AREF2) (1039 :DEFINITION AREF2) (1038 :TYPE-PRESCRIPTION ASET1) (1037 :EXECUTABLE-COUNTERPART ASET1) (1036 :DEFINITION ASET1) (1035 :REWRITE ARRAY1P-CONS) (1034 :TYPE-PRESCRIPTION COMPRESS1) (1033 :EXECUTABLE-COUNTERPART COMPRESS1) (1032 :DEFINITION COMPRESS1) (1031 :TYPE-PRESCRIPTION ARRAY-ORDER) (1030 :EXECUTABLE-COUNTERPART ARRAY-ORDER) (1029 :DEFINITION ARRAY-ORDER) (1028 :INDUCTION COMPRESS11) (1027 :TYPE-PRESCRIPTION COMPRESS11) (1026 :EXECUTABLE-COUNTERPART COMPRESS11) (1025 :DEFINITION COMPRESS11) (1024 :TYPE-PRESCRIPTION AREF1) (1023 :EXECUTABLE-COUNTERPART AREF1) (1022 :DEFINITION AREF1) (1021 :TYPE-PRESCRIPTION CONSP-ASSOC) (1020 :TYPE-PRESCRIPTION DEFAULT) (1019 :EXECUTABLE-COUNTERPART DEFAULT) (1018 :DEFINITION DEFAULT) (1017 :TYPE-PRESCRIPTION MAXIMUM-LENGTH) (1016 :EXECUTABLE-COUNTERPART MAXIMUM-LENGTH) (1015 :DEFINITION MAXIMUM-LENGTH) (1014 :TYPE-PRESCRIPTION DIMENSIONS) (1013 :EXECUTABLE-COUNTERPART DIMENSIONS) (1012 :DEFINITION DIMENSIONS) (1011 :TYPE-PRESCRIPTION HEADER) (1010 :EXECUTABLE-COUNTERPART HEADER) (1009 :DEFINITION HEADER) (1008 :LINEAR ARRAY2P-LINEAR) (1007 :FORWARD-CHAINING ARRAY2P-FORWARD) (1006 :TYPE-PRESCRIPTION ARRAY2P) (1005 :EXECUTABLE-COUNTERPART ARRAY2P) (1004 :DEFINITION ARRAY2P) (1003 :INDUCTION ASSOC2) (1002 :TYPE-PRESCRIPTION ASSOC2) (1001 :EXECUTABLE-COUNTERPART ASSOC2) (1000 :DEFINITION ASSOC2) (999 :INDUCTION BOUNDED-INTEGER-ALISTP2) (998 :TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP2) (997 :EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP2) (996 :DEFINITION BOUNDED-INTEGER-ALISTP2) (995 :LINEAR ARRAY1P-LINEAR) (994 :FORWARD-CHAINING ARRAY1P-FORWARD) (993 :TYPE-PRESCRIPTION ARRAY1P) (992 :EXECUTABLE-COUNTERPART ARRAY1P) (991 :DEFINITION ARRAY1P) (990 :TYPE-PRESCRIPTION CONSP-ASSOC-EQ) (989 :FORWARD-CHAINING KEYWORD-VALUE-LISTP-ASSOC-KEYWORD) (988 :INDUCTION ASSOC-KEYWORD) (987 :TYPE-PRESCRIPTION ASSOC-KEYWORD) (986 :EXECUTABLE-COUNTERPART ASSOC-KEYWORD) (985 :DEFINITION ASSOC-KEYWORD) (984 :FORWARD-CHAINING KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP) (983 :INDUCTION KEYWORD-VALUE-LISTP) (982 :TYPE-PRESCRIPTION KEYWORD-VALUE-LISTP) (981 :EXECUTABLE-COUNTERPART KEYWORD-VALUE-LISTP) (980 :DEFINITION KEYWORD-VALUE-LISTP) (979 :FORWARD-CHAINING BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP) (978 :INDUCTION BOUNDED-INTEGER-ALISTP) (977 :TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP) (976 :EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP) (975 :DEFINITION BOUNDED-INTEGER-ALISTP) (974 :INDUCTION SET-DIFFERENCE-EQUAL) (973 :TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL) (972 :EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQUAL) (971 :DEFINITION SET-DIFFERENCE-EQUAL) (970 :TYPE-PRESCRIPTION THE-ERROR) (969 :EXECUTABLE-COUNTERPART THE-ERROR) (968 :DEFINITION THE-ERROR) (967 :TYPE-PRESCRIPTION WEAK-SATISFIES-TYPE-SPEC-P) (966 :EXECUTABLE-COUNTERPART WEAK-SATISFIES-TYPE-SPEC-P) (965 :DEFINITION WEAK-SATISFIES-TYPE-SPEC-P) (964 :TYPE-PRESCRIPTION FUNCTION-SYMBOLP) (963 :EXECUTABLE-COUNTERPART FUNCTION-SYMBOLP) (962 :DEFINITION FUNCTION-SYMBOLP) (961 :TYPE-PRESCRIPTION GLOBAL-VAL) (960 :EXECUTABLE-COUNTERPART GLOBAL-VAL) (959 :DEFINITION GLOBAL-VAL) (958 :TYPE-PRESCRIPTION RETRACT-WORLD) (957 :EXECUTABLE-COUNTERPART RETRACT-WORLD) (956 :DEFINITION RETRACT-WORLD) (955 :TYPE-PRESCRIPTION EXTEND-WORLD) (954 :EXECUTABLE-COUNTERPART EXTEND-WORLD) (953 :DEFINITION EXTEND-WORLD) (952 :INDUCTION HAS-PROPSP) (951 :TYPE-PRESCRIPTION HAS-PROPSP) (950 :EXECUTABLE-COUNTERPART HAS-PROPSP) (949 :DEFINITION HAS-PROPSP) (948 :INDUCTION HAS-PROPSP1) (947 :TYPE-PRESCRIPTION HAS-PROPSP1) (946 :EXECUTABLE-COUNTERPART HAS-PROPSP1) (945 :DEFINITION HAS-PROPSP1) (944 :INDUCTION GETPROPS) (943 :TYPE-PRESCRIPTION GETPROPS) (942 :EXECUTABLE-COUNTERPART GETPROPS) (941 :DEFINITION GETPROPS) (940 :INDUCTION GETPROPS1) (939 :TYPE-PRESCRIPTION GETPROPS1) (938 :EXECUTABLE-COUNTERPART GETPROPS1) (937 :DEFINITION GETPROPS1) (936 :INDUCTION REMOVE-FIRST-PAIR) (935 :TYPE-PRESCRIPTION REMOVE-FIRST-PAIR) (934 :EXECUTABLE-COUNTERPART REMOVE-FIRST-PAIR) (933 :DEFINITION REMOVE-FIRST-PAIR) (932 :INDUCTION ADD-PAIR) (931 :TYPE-PRESCRIPTION ADD-PAIR) (930 :EXECUTABLE-COUNTERPART ADD-PAIR) (929 :DEFINITION ADD-PAIR) (928 :FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP) (927 :INDUCTION ORDERED-SYMBOL-ALISTP) (926 :TYPE-PRESCRIPTION ORDERED-SYMBOL-ALISTP) (925 :EXECUTABLE-COUNTERPART ORDERED-SYMBOL-ALISTP) (924 :DEFINITION ORDERED-SYMBOL-ALISTP) (923 :INDUCTION SGETPROP) (922 :TYPE-PRESCRIPTION SGETPROP) (921 :EXECUTABLE-COUNTERPART SGETPROP) (920 :DEFINITION SGETPROP) (919 :INDUCTION FGETPROP) (918 :TYPE-PRESCRIPTION FGETPROP) (917 :EXECUTABLE-COUNTERPART FGETPROP) (916 :DEFINITION FGETPROP) (915 :TYPE-PRESCRIPTION GETPROP-DEFAULT) (914 :EXECUTABLE-COUNTERPART GETPROP-DEFAULT) (913 :DEFINITION GETPROP-DEFAULT) (912 :TYPE-PRESCRIPTION PUTPROP) (911 :EXECUTABLE-COUNTERPART PUTPROP) (910 :DEFINITION PUTPROP) (909 :FORWARD-CHAINING WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP) (908 :INDUCTION WORLDP) (907 :TYPE-PRESCRIPTION WORLDP) (906 :EXECUTABLE-COUNTERPART WORLDP) (905 :DEFINITION WORLDP) (904 :INDUCTION SUBST) (903 :TYPE-PRESCRIPTION SUBST) (902 :EXECUTABLE-COUNTERPART SUBST) (901 :DEFINITION SUBST) (900 :INDUCTION SUBSETP) (899 :TYPE-PRESCRIPTION SUBSETP) (898 :EXECUTABLE-COUNTERPART SUBSETP) (897 :DEFINITION SUBSETP) (896 :TYPE-PRESCRIPTION SUBSTITUTE) (895 :EXECUTABLE-COUNTERPART SUBSTITUTE) (894 :DEFINITION SUBSTITUTE) (893 :INDUCTION SUBSTITUTE-AC) (892 :TYPE-PRESCRIPTION SUBSTITUTE-AC) (891 :EXECUTABLE-COUNTERPART SUBSTITUTE-AC) (890 :DEFINITION SUBSTITUTE-AC) (889 :REWRITE STRING<-IRREFLEXIVE) (888 :REWRITE STRING<-L-IRREFLEXIVE) (887 :TYPE-PRESCRIPTION SYMBOL-<) (886 :EXECUTABLE-COUNTERPART SYMBOL-<) (884 :TYPE-PRESCRIPTION STRING>=) (883 :EXECUTABLE-COUNTERPART STRING>=) (882 :DEFINITION STRING>=) (881 :TYPE-PRESCRIPTION STRING<=) (880 :EXECUTABLE-COUNTERPART STRING<=) (879 :DEFINITION STRING<=) (878 :TYPE-PRESCRIPTION STRING>) (877 :EXECUTABLE-COUNTERPART STRING>) (876 :DEFINITION STRING>) (875 :TYPE-PRESCRIPTION STRING<) (874 :EXECUTABLE-COUNTERPART STRING<) (871 :TYPE-PRESCRIPTION STRING<-L) (870 :EXECUTABLE-COUNTERPART STRING<-L) (868 :TYPE-PRESCRIPTION CHAR>=) (867 :EXECUTABLE-COUNTERPART CHAR>=) (866 :DEFINITION CHAR>=) (865 :TYPE-PRESCRIPTION CHAR<=) (864 :EXECUTABLE-COUNTERPART CHAR<=) (863 :DEFINITION CHAR<=) (862 :TYPE-PRESCRIPTION CHAR>) (861 :EXECUTABLE-COUNTERPART CHAR>) (860 :DEFINITION CHAR>) (859 :TYPE-PRESCRIPTION CHAR<) (858 :EXECUTABLE-COUNTERPART CHAR<) (857 :DEFINITION CHAR<) (856 :REWRITE CHAR-CODE-CODE-CHAR-IS-IDENTITY) (855 :REWRITE CODE-CHAR-CHAR-CODE-IS-IDENTITY) (854 :TYPE-PRESCRIPTION CODE-CHAR-TYPE) (853 :LINEAR CHAR-CODE-LINEAR) (852 :TYPE-PRESCRIPTION ASH) (851 :EXECUTABLE-COUNTERPART ASH) (850 :DEFINITION ASH) (849 :TYPE-PRESCRIPTION LOGBITP) (848 :EXECUTABLE-COUNTERPART LOGBITP) (847 :DEFINITION LOGBITP) (846 :TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION) (845 :TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE) (844 :INDUCTION NTHCDR) (843 :TYPE-PRESCRIPTION NTHCDR) (842 :EXECUTABLE-COUNTERPART NTHCDR) (841 :DEFINITION NTHCDR) (840 :INDUCTION LOGCOUNT) (839 :TYPE-PRESCRIPTION LOGCOUNT) (838 :EXECUTABLE-COUNTERPART LOGCOUNT) (837 :DEFINITION LOGCOUNT) (836 :INDUCTION EXPT) (835 :TYPE-PRESCRIPTION EXPT) (834 :EXECUTABLE-COUNTERPART EXPT) (833 :DEFINITION EXPT) (832 :INDUCTION XXXJOIN) (831 :TYPE-PRESCRIPTION XXXJOIN) (830 :EXECUTABLE-COUNTERPART XXXJOIN) (829 :DEFINITION XXXJOIN) (828 :INDUCTION ASSOC-STRING-EQUAL) (827 :TYPE-PRESCRIPTION ASSOC-STRING-EQUAL) (826 :EXECUTABLE-COUNTERPART ASSOC-STRING-EQUAL) (825 :DEFINITION ASSOC-STRING-EQUAL) (824 :TYPE-PRESCRIPTION STRING-EQUAL) (823 :EXECUTABLE-COUNTERPART STRING-EQUAL) (822 :DEFINITION STRING-EQUAL) (821 :INDUCTION STRING-EQUAL1) (820 :TYPE-PRESCRIPTION STRING-EQUAL1) (819 :EXECUTABLE-COUNTERPART STRING-EQUAL1) (818 :DEFINITION STRING-EQUAL1) (817 :REWRITE STANDARD-CHAR-P-NTH) (816 :TYPE-PRESCRIPTION LOGNOT) (815 :EXECUTABLE-COUNTERPART LOGNOT) (814 :DEFINITION LOGNOT) (813 :TYPE-PRESCRIPTION SIGNUM) (812 :EXECUTABLE-COUNTERPART SIGNUM) (811 :DEFINITION SIGNUM) (810 :TYPE-PRESCRIPTION ABS) (809 :EXECUTABLE-COUNTERPART ABS) (808 :DEFINITION ABS) (807 :TYPE-PRESCRIPTION MAX) (806 :EXECUTABLE-COUNTERPART MAX) (805 :DEFINITION MAX) (804 :TYPE-PRESCRIPTION MIN) (803 :EXECUTABLE-COUNTERPART MIN) (802 :DEFINITION MIN) (801 :TYPE-PRESCRIPTION ODDP) (800 :EXECUTABLE-COUNTERPART ODDP) (799 :DEFINITION ODDP) (798 :TYPE-PRESCRIPTION EVENP) (797 :EXECUTABLE-COUNTERPART EVENP) (796 :DEFINITION EVENP) (795 :TYPE-PRESCRIPTION REM) (794 :EXECUTABLE-COUNTERPART REM) (793 :DEFINITION REM) (792 :TYPE-PRESCRIPTION MOD) (791 :EXECUTABLE-COUNTERPART MOD) (790 :DEFINITION MOD) (789 :TYPE-PRESCRIPTION ROUND) (788 :EXECUTABLE-COUNTERPART ROUND) (787 :DEFINITION ROUND) (786 :TYPE-PRESCRIPTION TRUNCATE) (785 :EXECUTABLE-COUNTERPART TRUNCATE) (784 :DEFINITION TRUNCATE) (783 :TYPE-PRESCRIPTION CEILING) (782 :EXECUTABLE-COUNTERPART CEILING) (781 :DEFINITION CEILING) (780 :INDUCTION RESTRICT-ALIST) (779 :TYPE-PRESCRIPTION RESTRICT-ALIST) (778 :EXECUTABLE-COUNTERPART RESTRICT-ALIST) (777 :DEFINITION RESTRICT-ALIST) (776 :INDUCTION APPEND-LST) (775 :TYPE-PRESCRIPTION APPEND-LST) (774 :EXECUTABLE-COUNTERPART APPEND-LST) (773 :DEFINITION APPEND-LST) (772 :INDUCTION COLLECT-CDRS-WHEN-CAR-EQ) (771 :TYPE-PRESCRIPTION COLLECT-CDRS-WHEN-CAR-EQ) (770 :EXECUTABLE-COUNTERPART COLLECT-CDRS-WHEN-CAR-EQ) (769 :DEFINITION COLLECT-CDRS-WHEN-CAR-EQ) (768 :INDUCTION LET*-MACRO) (767 :TYPE-PRESCRIPTION LET*-MACRO) (766 :EXECUTABLE-COUNTERPART LET*-MACRO) (765 :DEFINITION LET*-MACRO) (764 :INDUCTION GET-TYPE-DECLS) (763 :TYPE-PRESCRIPTION GET-TYPE-DECLS) (762 :EXECUTABLE-COUNTERPART GET-TYPE-DECLS) (761 :DEFINITION GET-TYPE-DECLS) (760 :INDUCTION SYMBOL-LIST-LISTP) (759 :TYPE-PRESCRIPTION SYMBOL-LIST-LISTP) (758 :EXECUTABLE-COUNTERPART SYMBOL-LIST-LISTP) (757 :DEFINITION SYMBOL-LIST-LISTP) (756 :INDUCTION WELL-FORMED-TYPE-DECLS-P) (755 :TYPE-PRESCRIPTION WELL-FORMED-TYPE-DECLS-P) (754 :EXECUTABLE-COUNTERPART WELL-FORMED-TYPE-DECLS-P) (753 :DEFINITION WELL-FORMED-TYPE-DECLS-P) (752 :INDUCTION LEGAL-LET*-P) (751 :TYPE-PRESCRIPTION LEGAL-LET*-P) (750 :EXECUTABLE-COUNTERPART LEGAL-LET*-P) (749 :DEFINITION LEGAL-LET*-P) (748 :FORWARD-CHAINING TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP) (747 :INDUCTION TRUE-LIST-LISTP) (746 :TYPE-PRESCRIPTION TRUE-LIST-LISTP) (745 :EXECUTABLE-COUNTERPART TRUE-LIST-LISTP) (744 :DEFINITION TRUE-LIST-LISTP) (743 :TYPE-PRESCRIPTION POSITION) (742 :EXECUTABLE-COUNTERPART POSITION) (741 :DEFINITION POSITION) (740 :TYPE-PRESCRIPTION POSITION-EQ) (739 :EXECUTABLE-COUNTERPART POSITION-EQ) (738 :DEFINITION POSITION-EQ) (737 :INDUCTION POSITION-EQ-AC) (736 :TYPE-PRESCRIPTION POSITION-EQ-AC) (735 :EXECUTABLE-COUNTERPART POSITION-EQ-AC) (734 :DEFINITION POSITION-EQ-AC) (733 :TYPE-PRESCRIPTION POSITION-EQUAL) (732 :EXECUTABLE-COUNTERPART POSITION-EQUAL) (731 :DEFINITION POSITION-EQUAL) (730 :INDUCTION POSITION-AC) (729 :TYPE-PRESCRIPTION POSITION-AC) (728 :EXECUTABLE-COUNTERPART POSITION-AC) (727 :DEFINITION POSITION-AC) (726 :INDUCTION POSITION-EQUAL-AC) (725 :TYPE-PRESCRIPTION POSITION-EQUAL-AC) (724 :EXECUTABLE-COUNTERPART POSITION-EQUAL-AC) (723 :DEFINITION POSITION-EQUAL-AC) (722 :INDUCTION CASE-LIST-CHECK) (721 :TYPE-PRESCRIPTION CASE-LIST-CHECK) (720 :EXECUTABLE-COUNTERPART CASE-LIST-CHECK) (719 :DEFINITION CASE-LIST-CHECK) (718 :INDUCTION CASE-LIST) (717 :TYPE-PRESCRIPTION CASE-LIST) (716 :EXECUTABLE-COUNTERPART CASE-LIST) (715 :DEFINITION CASE-LIST) (714 :TYPE-PRESCRIPTION CASE-TEST) (713 :EXECUTABLE-COUNTERPART CASE-TEST) (712 :DEFINITION CASE-TEST) (711 :INDUCTION LEGAL-CASE-CLAUSESP) (710 :TYPE-PRESCRIPTION LEGAL-CASE-CLAUSESP) (709 :EXECUTABLE-COUNTERPART LEGAL-CASE-CLAUSESP) (708 :DEFINITION LEGAL-CASE-CLAUSESP) (707 :INDUCTION ER-PROGN-FN) (706 :TYPE-PRESCRIPTION ER-PROGN-FN) (705 :EXECUTABLE-COUNTERPART ER-PROGN-FN) (704 :DEFINITION ER-PROGN-FN) (703 :INDUCTION MAKE-FMT-BINDINGS) (702 :TYPE-PRESCRIPTION MAKE-FMT-BINDINGS) (701 :EXECUTABLE-COUNTERPART MAKE-FMT-BINDINGS) (700 :DEFINITION MAKE-FMT-BINDINGS) (699 :INDUCTION INTERSECTP-EQUAL) (698 :TYPE-PRESCRIPTION INTERSECTP-EQUAL) (697 :EXECUTABLE-COUNTERPART INTERSECTP-EQUAL) (696 :DEFINITION INTERSECTP-EQUAL) (695 :INDUCTION INTERSECTP) (694 :TYPE-PRESCRIPTION INTERSECTP) (693 :EXECUTABLE-COUNTERPART INTERSECTP) (692 :DEFINITION INTERSECTP) (691 :INDUCTION INTERSECTP-EQ) (690 :TYPE-PRESCRIPTION INTERSECTP-EQ) (689 :EXECUTABLE-COUNTERPART INTERSECTP-EQ) (688 :DEFINITION INTERSECTP-EQ) (687 :TYPE-PRESCRIPTION ALL-VARS) (686 :EXECUTABLE-COUNTERPART ALL-VARS) (685 :DEFINITION ALL-VARS) (684 :INDUCTION ALL-VARS1-LST) (683 :TYPE-PRESCRIPTION ALL-VARS1-LST) (682 :EXECUTABLE-COUNTERPART ALL-VARS1-LST) (681 :DEFINITION ALL-VARS1-LST) (680 :INDUCTION ALL-VARS1) (679 :TYPE-PRESCRIPTION ALL-VARS1) (678 :EXECUTABLE-COUNTERPART ALL-VARS1) (677 :DEFINITION ALL-VARS1) (676 :TYPE-PRESCRIPTION FN-SYMB) (675 :EXECUTABLE-COUNTERPART FN-SYMB) (674 :DEFINITION FN-SYMB) (673 :INDUCTION KWOTE-LST) (672 :TYPE-PRESCRIPTION KWOTE-LST) (671 :EXECUTABLE-COUNTERPART KWOTE-LST) (670 :DEFINITION KWOTE-LST) (669 :TYPE-PRESCRIPTION KWOTE) (668 :EXECUTABLE-COUNTERPART KWOTE) (667 :DEFINITION KWOTE) (666 :TYPE-PRESCRIPTION QUOTEP) (665 :EXECUTABLE-COUNTERPART QUOTEP) (664 :DEFINITION QUOTEP) (663 :TYPE-PRESCRIPTION ADD-TO-SET-EQL) (662 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQL) (661 :DEFINITION ADD-TO-SET-EQL) (660 :TYPE-PRESCRIPTION ADD-TO-SET-EQ) (659 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQ) (658 :DEFINITION ADD-TO-SET-EQ) (657 :INDUCTION PSEUDO-TERM-LIST-LISTP) (656 :TYPE-PRESCRIPTION PSEUDO-TERM-LIST-LISTP) (655 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LIST-LISTP) (654 :DEFINITION PSEUDO-TERM-LIST-LISTP) (653 :FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) (652 :INDUCTION PSEUDO-TERM-LISTP) (651 :TYPE-PRESCRIPTION PSEUDO-TERM-LISTP) (650 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP) (649 :DEFINITION PSEUDO-TERM-LISTP) (648 :INDUCTION PSEUDO-TERMP) (647 :TYPE-PRESCRIPTION PSEUDO-TERMP) (646 :EXECUTABLE-COUNTERPART PSEUDO-TERMP) (645 :DEFINITION PSEUDO-TERMP) (644 :INDUCTION DEFUND-NAME-LIST) (643 :TYPE-PRESCRIPTION DEFUND-NAME-LIST) (642 :EXECUTABLE-COUNTERPART DEFUND-NAME-LIST) (641 :DEFINITION DEFUND-NAME-LIST) (640 :TYPE-PRESCRIPTION XD-NAME) (639 :EXECUTABLE-COUNTERPART XD-NAME) (638 :DEFINITION XD-NAME) (637 :TYPE-PRESCRIPTION VALUE-TRIPLE-FN) (636 :EXECUTABLE-COUNTERPART VALUE-TRIPLE-FN) (635 :DEFINITION VALUE-TRIPLE-FN) (634 :INDUCTION COLLECT-CADRS-WHEN-CAR-EQ) (633 :TYPE-PRESCRIPTION COLLECT-CADRS-WHEN-CAR-EQ) (632 :EXECUTABLE-COUNTERPART COLLECT-CADRS-WHEN-CAR-EQ) (631 :DEFINITION COLLECT-CADRS-WHEN-CAR-EQ) (630 :INDUCTION MUTUAL-RECURSION-GUARDP) (629 :TYPE-PRESCRIPTION MUTUAL-RECURSION-GUARDP) (628 :EXECUTABLE-COUNTERPART MUTUAL-RECURSION-GUARDP) (627 :DEFINITION MUTUAL-RECURSION-GUARDP) (626 :INDUCTION STRIP-CDRS) (625 :TYPE-PRESCRIPTION STRIP-CDRS) (624 :EXECUTABLE-COUNTERPART STRIP-CDRS) (623 :DEFINITION STRIP-CDRS) (622 :TYPE-PRESCRIPTION BUTLAST) (621 :EXECUTABLE-COUNTERPART BUTLAST) (620 :DEFINITION BUTLAST) (619 :TYPE-PRESCRIPTION TAKE) (618 :EXECUTABLE-COUNTERPART TAKE) (617 :DEFINITION TAKE) (616 :INDUCTION FIRST-N-AC) (615 :TYPE-PRESCRIPTION FIRST-N-AC) (614 :EXECUTABLE-COUNTERPART FIRST-N-AC) (613 :DEFINITION FIRST-N-AC) (612 :INDUCTION LAST) (611 :TYPE-PRESCRIPTION LAST) (610 :EXECUTABLE-COUNTERPART LAST) (609 :DEFINITION LAST) (608 :INDUCTION SET-DIFFERENCE-EQ) (607 :TYPE-PRESCRIPTION SET-DIFFERENCE-EQ) (606 :EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQ) (605 :DEFINITION SET-DIFFERENCE-EQ) (604 :TYPE-PRESCRIPTION REVERSE) (603 :EXECUTABLE-COUNTERPART REVERSE) (602 :DEFINITION REVERSE) (601 :REWRITE CHARACTER-LISTP-REVAPPEND) (600 :INDUCTION REVAPPEND) (599 :TYPE-PRESCRIPTION REVAPPEND) (598 :EXECUTABLE-COUNTERPART REVAPPEND) (597 :DEFINITION REVAPPEND) (596 :TYPE-PRESCRIPTION IDENTITY) (595 :EXECUTABLE-COUNTERPART IDENTITY) (594 :DEFINITION IDENTITY) (593 :INDUCTION REMOVE-DUPLICATES-EQUAL) (592 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL) (591 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQUAL) (590 :DEFINITION REMOVE-DUPLICATES-EQUAL) (589 :TYPE-PRESCRIPTION REMOVE-DUPLICATES) (588 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES) (587 :DEFINITION REMOVE-DUPLICATES) (586 :REWRITE CHARACTER-LISTP-REMOVE-DUPLICATES-EQL) (585 :INDUCTION REMOVE-DUPLICATES-EQL) (584 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQL) (583 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQL) (582 :DEFINITION REMOVE-DUPLICATES-EQL) (581 :INDUCTION PAIRLIS$) (580 :TYPE-PRESCRIPTION PAIRLIS$) (579 :EXECUTABLE-COUNTERPART PAIRLIS$) (578 :DEFINITION PAIRLIS$) (577 :INDUCTION REMOVE1-EQUAL) (576 :TYPE-PRESCRIPTION REMOVE1-EQUAL) (575 :EXECUTABLE-COUNTERPART REMOVE1-EQUAL) (574 :DEFINITION REMOVE1-EQUAL) (573 :INDUCTION REMOVE1-EQ) (572 :TYPE-PRESCRIPTION REMOVE1-EQ) (571 :EXECUTABLE-COUNTERPART REMOVE1-EQ) (570 :DEFINITION REMOVE1-EQ) (569 :INDUCTION REMOVE1) (568 :TYPE-PRESCRIPTION REMOVE1) (567 :EXECUTABLE-COUNTERPART REMOVE1) (566 :DEFINITION REMOVE1) (565 :INDUCTION REMOVE-EQUAL) (564 :TYPE-PRESCRIPTION REMOVE-EQUAL) (563 :EXECUTABLE-COUNTERPART REMOVE-EQUAL) (562 :DEFINITION REMOVE-EQUAL) (561 :INDUCTION REMOVE-EQ) (560 :TYPE-PRESCRIPTION REMOVE-EQ) (559 :EXECUTABLE-COUNTERPART REMOVE-EQ) (558 :DEFINITION REMOVE-EQ) (557 :INDUCTION REMOVE) (556 :TYPE-PRESCRIPTION REMOVE) (555 :EXECUTABLE-COUNTERPART REMOVE) (554 :DEFINITION REMOVE) (553 :INDUCTION STRING-APPEND-LST) (552 :TYPE-PRESCRIPTION STRING-APPEND-LST) (551 :EXECUTABLE-COUNTERPART STRING-APPEND-LST) (550 :DEFINITION STRING-APPEND-LST) (549 :INDUCTION STRING-LISTP) (548 :TYPE-PRESCRIPTION STRING-LISTP) (547 :EXECUTABLE-COUNTERPART STRING-LISTP) (546 :DEFINITION STRING-LISTP) (545 :TYPE-PRESCRIPTION STRING-APPEND) (544 :EXECUTABLE-COUNTERPART STRING-APPEND) (543 :DEFINITION STRING-APPEND) (542 :REWRITE APPEND-TO-NIL) (541 :REWRITE CHARACTER-LISTP-APPEND) (540 :REWRITE STANDARD-CHAR-LISTP-APPEND) (539 :INDUCTION BINARY-APPEND) (538 :TYPE-PRESCRIPTION BINARY-APPEND) (537 :EXECUTABLE-COUNTERPART BINARY-APPEND) (536 :DEFINITION BINARY-APPEND) (535 :REWRITE KEYWORD-PACKAGE) (534 :REWRITE ACL2-PACKAGE) (533 :REWRITE ACL2-OUTPUT-CHANNEL-PACKAGE) (532 :REWRITE ACL2-INPUT-CHANNEL-PACKAGE) (531 :REWRITE SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL) (530 :INDUCTION MEMBER-SYMBOL-NAME) (529 :TYPE-PRESCRIPTION MEMBER-SYMBOL-NAME) (528 :EXECUTABLE-COUNTERPART MEMBER-SYMBOL-NAME) (527 :DEFINITION MEMBER-SYMBOL-NAME) (526 :REWRITE SYMBOL-PACKAGE-NAME-PKG-WITNESS-NAME) (525 :REWRITE SYMBOL-NAME-PKG-WITNESS) (524 :FORWARD-CHAINING SYMBOL-PACKAGE-NAME-OF-SYMBOL-IS-NOT-EMPTY-STRING) (523 :REWRITE INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME) (522 :FORWARD-CHAINING KEYWORDP-FORWARD-TO-SYMBOLP) (521 :TYPE-PRESCRIPTION KEYWORDP) (520 :EXECUTABLE-COUNTERPART KEYWORDP) (519 :DEFINITION KEYWORDP) (518 :TYPE-PRESCRIPTION ILLEGAL) (517 :EXECUTABLE-COUNTERPART ILLEGAL) (516 :DEFINITION ILLEGAL) (515 :TYPE-PRESCRIPTION HARD-ERROR) (514 :EXECUTABLE-COUNTERPART HARD-ERROR) (513 :DEFINITION HARD-ERROR) (512 :TYPE-PRESCRIPTION SYMBOLP-PKG-WITNESS) (511 :TYPE-PRESCRIPTION SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL) (510 :TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME) (509 :TYPE-PRESCRIPTION NULL-BODY-ER) (508 :EXECUTABLE-COUNTERPART NULL-BODY-ER) (507 :DEFINITION NULL-BODY-ER) (506 :INDUCTION LIST*-MACRO) (505 :TYPE-PRESCRIPTION LIST*-MACRO) (504 :EXECUTABLE-COUNTERPART LIST*-MACRO) (503 :DEFINITION LIST*-MACRO) (502 :TYPE-PRESCRIPTION MAKE-ORD) (501 :EXECUTABLE-COUNTERPART MAKE-ORD) (500 :DEFINITION MAKE-ORD) (499 :REWRITE O-P-IMPLIES-O:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? [RAW LISP] state ACL2_INVISIBLE::|The Live State Itself| ? [RAW LISP] *the-live-state* ACL2_INVISIBLE::|The Live State Itself| ? [RAW LISP] (with-live-state state) ACL2_INVISIBLE::|The Live State Itself| ? [RAW LISP] state ACL2_INVISIBLE::|The Live State Itself| ? [RAW LISP] (quit) mac:~/acl2/v3-6-1/acl2-sources$ popd bash: popd: directory stack empty mac:~/acl2/v3-6-1/acl2-sources$ cd mac:~$ cd talks/seminar-2009-10-28/ mac:~/talks/seminar-2009-10-28$ acl2-3.6.1 Welcome to Clozure Common Lisp Version 1.3-r11936 (DarwinX8664)! ACL2 Version 3.6.1 built September 7, 2009 10:14:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/talks/seminar-2009-10-28/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>Bye. mac:~/talks/seminar-2009-10-28$ acl2-3.6.1 Welcome to Clozure Common Lisp Version 1.3-r11936 (DarwinX8664)! ACL2 Version 3.6.1 built September 7, 2009 10:14:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/talks/seminar-2009-10-28/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(certify-book "enabledp-change") CERTIFICATION ATTEMPT FOR "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" ACL2 Version 3.6.1 * Step 1: Read "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" and compute its check sum. * Step 2: There were ten forms in the file. We now attempt to establish that each form, whether local or non-local, is indeed an admissible embedded event form in the context of the previously admitted ones. ACL2 >>(PROGRAM) :INVISIBLE ACL2 p>>(SET-STATE-OK T) T ACL2 p>>(DEFUN WRLD-TAIL-MAKING-DISABLED (NUME WRLD OLDEST-DISABLED-WRLD MIN-EVENT-NUMBER) (COND ((NULL WRLD) NIL) ((AND (EQ (CAAR WRLD) 'COMMAND-LANDMARK) (EQ (CADAR WRLD) 'GLOBAL-VALUE) (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDAR WRLD)) '(EXIT-BOOT-STRAP-MODE))) (IF (ASSOC NUME (GLOBAL-VAL 'CURRENT-THEORY-AUGMENTED WRLD)) OLDEST-DISABLED-WRLD NIL)) ((AND (EQ (CAAR WRLD) 'EVENT-LANDMARK) (EQ (CADAR WRLD) 'GLOBAL-VALUE) (< (ACCESS-EVENT-TUPLE-NUMBER (CDDR (CAR WRLD))) MIN-EVENT-NUMBER)) OLDEST-DISABLED-WRLD) ((AND (EQ (CAAR WRLD) 'CURRENT-THEORY-AUGMENTED) (EQ (CADAR WRLD) 'GLOBAL-VALUE)) (IF (ASSOC NUME (CDDR (CAR WRLD))) (ASSERT$ OLDEST-DISABLED-WRLD OLDEST-DISABLED-WRLD) (WRLD-TAIL-MAKING-DISABLED NUME (CDR WRLD) WRLD MIN-EVENT-NUMBER))) (T (WRLD-TAIL-MAKING-DISABLED NUME (CDR WRLD) OLDEST-DISABLED-WRLD MIN-EVENT-NUMBER)))) Summary Form: ( DEFUN WRLD-TAIL-MAKING-DISABLED ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) WRLD-TAIL-MAKING-DISABLED ACL2 p>>(DEFUN WRLD-TAIL-MAKING-ENABLED (NUME WRLD OLDEST-ENABLED-WRLD MIN-EVENT-NUMBER) (COND ((NULL WRLD) NIL) ((AND (EQ (CAAR WRLD) 'COMMAND-LANDMARK) (EQ (CADAR WRLD) 'GLOBAL-VALUE) (EQUAL (ACCESS-COMMAND-TUPLE-FORM (CDDAR WRLD)) '(EXIT-BOOT-STRAP-MODE))) (IF (ASSOC NUME (GLOBAL-VAL 'CURRENT-THEORY-AUGMENTED WRLD)) NIL OLDEST-ENABLED-WRLD)) ((AND (EQ (CAAR WRLD) 'EVENT-LANDMARK) (EQ (CADAR WRLD) 'GLOBAL-VALUE) (< (ACCESS-EVENT-TUPLE-NUMBER (CDDR (CAR WRLD))) MIN-EVENT-NUMBER)) NIL) ((AND (EQ (CAAR WRLD) 'CURRENT-THEORY-AUGMENTED) (EQ (CADAR WRLD) 'GLOBAL-VALUE)) (IF (NOT (ASSOC NUME (CDDR (CAR WRLD)))) (ASSERT$ OLDEST-ENABLED-WRLD OLDEST-ENABLED-WRLD) (WRLD-TAIL-MAKING-ENABLED NUME (CDR WRLD) WRLD MIN-EVENT-NUMBER))) (T (WRLD-TAIL-MAKING-ENABLED NUME (CDR WRLD) OLDEST-ENABLED-WRLD MIN-EVENT-NUMBER)))) Summary Form: ( DEFUN WRLD-TAIL-MAKING-ENABLED ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) WRLD-TAIL-MAKING-ENABLED ACL2 p>>(DEFUN NAME-OF-PRECEDING-EVENT (WRLD) (COND ((NULL WRLD) NIL) ((AND (EQ (CAAR WRLD) 'EVENT-LANDMARK) (EQ (CADAR WRLD) 'GLOBAL-VALUE)) (LET ((NAMEX (ACCESS-EVENT-TUPLE-NAMEX (CDDR (CAR WRLD))))) (COND ((OR (AND NAMEX (SYMBOLP NAMEX)) (STRINGP NAMEX)) NAMEX) ((AND NAMEX (SYMBOL-LISTP NAMEX)) (CAR NAMEX)) (T (NAME-OF-PRECEDING-EVENT (CDR WRLD)))))) (T (NAME-OF-PRECEDING-EVENT (CDR WRLD))))) Summary Form: ( DEFUN NAME-OF-PRECEDING-EVENT ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) NAME-OF-PRECEDING-EVENT ACL2 p>>(DEFUN EVENT-NUMBER-OF-RUNE (RUNE WRLD) (GETPROP (BASE-SYMBOL RUNE) 'ABSOLUTE-EVENT-NUMBER 0 'CURRENT-ACL2-WORLD WRLD)) Summary Form: ( DEFUN EVENT-NUMBER-OF-RUNE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) EVENT-NUMBER-OF-RUNE ACL2 p>>(DEFUN EVENT-PRECEDING-ENABLEDP-CHANGE (RUNE CTX STATE) (LET* ((WRLD (W STATE)) (NUME (FNUME RUNE WRLD))) (COND ((NULL NUME) (ER SOFT CTX "The rune ~x0 does not exist!" RUNE)) (T (LET* ((ENS (ENS STATE)) (ENABLEDP (ENABLED-NUMEP NUME ENS)) (MIN-EVENT-NUMBER (EVENT-NUMBER-OF-RUNE RUNE WRLD)) (TAIL (COND ((ENABLED-NUMEP NUME ENS) (WRLD-TAIL-MAKING-ENABLED NUME WRLD NIL MIN-EVENT-NUMBER)) (T (WRLD-TAIL-MAKING-DISABLED NUME WRLD NIL MIN-EVENT-NUMBER))))) (COND ((NULL TAIL) (PPROGN (FMS "The rune ~x0 is ~s1, and always has been since the ~ boot-strap world.~%" (LIST (CONS #\0 RUNE) (CONS #\1 (IF ENABLEDP "enabled" "disabled"))) (STANDARD-CO STATE) STATE NIL) (VALUE :INVISIBLE))) (T (LET ((NAME (NAME-OF-PRECEDING-EVENT TAIL))) (COND (NAME (PE-FN NAME STATE)) (T (ER SOFT CTX "Implementation error in finding preceding name ~ for enabled status change in rune ~x0!" RUNE))))))))))) Summary Form: ( DEFUN EVENT-PRECEDING-ENABLEDP-CHANGE ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) EVENT-PRECEDING-ENABLEDP-CHANGE ACL2 p>>(DEFUN NAME-TO-RUNE (NAME WRLD) (COND ((RULE-NAME-DESIGNATORP NAME (MACRO-ALIASES WRLD) WRLD) (LET ((THY (RUNIC-THEORY (LIST NAME) WRLD))) (COND ((NULL THY) NIL) ((NULL (CDR THY)) (CAR THY)) (T (OR (ASSOC-EQ :DEFINITION THY) (CAR THY)))))) (T NIL))) Summary Form: ( DEFUN NAME-TO-RUNE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) NAME-TO-RUNE ACL2 p>>(DEFMACRO PE-PED (NAME) ":Doc-Section History print the event just before changing of enabled status of a logical name~/ Note that ``~c[pe-ped]'' stands for ``Print the Event Preceding Enable/Disable status change''. The following example should illustrate how ~c[:pe-ped] works. If ~c[append] (actually its corresponding function, ~c[binary-append]) is disabled, then the following command uses ~c[:]~ilc[pe] to print the event immediately preceding the most recent ~c[in-theory] event that disabled ~ilc[append]. ~bv[] Example: :pe-ped append ~ev[]~/ If the name is not the ~il[logical-name] of any ~il[events], an error will occur. Note that the search for an enabled/disabled status change goes back to the initial (boot-strap, ground-zero) ACL2 logical ~il[world]. If no status change is found, a message will be printed to that effect.~/" (CONS 'LET* (CONS (CONS (CONS 'NAME (CONS NAME 'NIL)) (CONS (CONS 'RUNE (CONS (CONS 'NAME-TO-RUNE (CONS 'NAME (CONS (CONS 'W (CONS 'STATE 'NIL)) 'NIL))) 'NIL)) (CONS (CONS 'CTX (CONS (CONS 'QUOTE (CONS 'PE-PED 'NIL)) 'NIL)) 'NIL))) (CONS (CONS 'COND (CONS (CONS 'RUNE (CONS (CONS 'EVENT-PRECEDING-ENABLEDP-CHANGE (CONS 'RUNE (CONS 'CTX (CONS 'STATE 'NIL)))) 'NIL)) (CONS (CONS 'T (CONS (CONS 'ER (CONS 'SOFT (CONS 'CTX (CONS '"No rune was found named ~x0." (CONS 'NAME 'NIL))))) 'NIL)) 'NIL))) 'NIL)))) Summary Form: ( DEFMACRO PE-PED ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) PE-PED * Step 3: That completes the admissibility check. Each form read was an embedded event form and was admissible. We now retract back to the initial world and try to include the book. This may expose local incompatibilities. Summary Form: ( INCLUDE-BOOK "enabledp-change" ...) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) * Step 4: Write the certificate for "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" in "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.cert". The final check sum alist is (("/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" "enabledp-change" "enabledp-change" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 883237531)). Summary Form: (CERTIFY-BOOK "enabledp-change" ...) Rules: NIL Warnings: None Time: 0.07 seconds (prove: 0.00, print: 0.00, other: 0.07) "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" ACL2 !>:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(include-book "enabledp-change") Summary Form: ( INCLUDE-BOOK "enabledp-change" ...) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" ACL2 !>(include-book "arithmetic-3/extra/top-ext" :dir :system) ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "arithmetic-3/extra/top-ext" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "arithmetic-3/bind-free/top" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/top.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "default-hint" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/default-hint.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "building-blocks" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/building-blocks.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "mini-theories" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/mini-theories.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "common" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/common.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "normalize" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/normalize.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "simplify" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/simplify.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "numerator-and-denominator" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/numerator-and-denominator.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "integerp" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/integerp.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "integerp-meta" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/integerp-meta.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "basic" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/basic.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "collect" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/collect.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "remove-weak-inequalities" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "arithmetic-theory" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/arithmetic-theory.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "banner" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/banner.lisp". To turn on non-linear arithmetic: (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))) ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "arithmetic-3/floor-mod/floor-mod" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/floor-mod/floor-mod.lisp". ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "ext" ...): There is no certificate on file for "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/ext.lisp". Summary Form: ( INCLUDE-BOOK "arithmetic-3/extra/top-ext" ...) Rules: NIL Warnings: Uncertified Time: 0.68 seconds (prove: 0.00, print: 0.00, other: 0.68) "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" ACL2 !>:pe EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT d 2:x(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/top.lisp" "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/mini-theories.lisp" ] \ > (DEFTHM EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT (IMPLIES (AND (< R 0) (RATIONALP R) (INTEGERP I) (INTEGERP (* 1/2 I))) (< 0 (EXPT R I))) :RULE-CLASSES (:TYPE-PRESCRIPTION :GENERALIZE)) ACL2 !>:pe-ped EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT d 2:x(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" ] \ > (INCLUDE-BOOK "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/ext.lisp") ACL2 !>:pe strong-expt-type-prescription-rules d 2:x(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/top.lisp" ] \ > (DEFTHEORY STRONG-EXPT-TYPE-PRESCRIPTION-RULES '(EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-ODD-EXPONENT EXPT-NEGATIVE-BASE-EVEN-EXPONENT EXPT-NEGATIVE-BASE-ODD-EXPONENT)) ACL2 !>:pe EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT d 2:x(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/top.lisp" "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/bind-free/mini-theories.lisp" ] \ > (DEFTHM EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT (IMPLIES (AND (< R 0) (RATIONALP R) (INTEGERP I) (INTEGERP (* 1/2 I))) (< 0 (EXPT R I))) :RULE-CLASSES (:TYPE-PRESCRIPTION :GENERALIZE)) ACL2 !>:pe-ped EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT d 2:x(INCLUDE-BOOK "arithmetic-3/extra/top-ext" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/top-ext.lisp" ] \ > (INCLUDE-BOOK "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/arithmetic-3/extra/ext.lisp") ACL2 !>:doc pe-ped | PE-PED print the event just before changing of enabled status of a logical name | | Note that ``pe-ped'' stands for ``Print the Event Preceding | Enable/Disable status change''. The following example should illustrate how | :pe-ped works. If append (actually its corresponding function, | binary-append) is disabled, then the following command uses :pe | to print the event immediately preceding the most recent in-theory event | that disabled append. | | Example: | :pe-ped append | (type :more for more, :more! for the rest) ACL2 !>:more | If the name is not the logical-name of any events, an error will | occur. Note that the search for an enabled/disabled status change goes back | to the initial (boot-strap, ground-zero) ACL2 logical world. If no | status change is found, a message will be printed to that effect. *- ACL2 !>Bye. mac:~/talks/seminar-2009-10-28$ acl2-3.6.1 Welcome to Clozure Common Lisp Version 1.3-r11936 (DarwinX8664)! ACL2 Version 3.6.1 built September 7, 2009 10:14:24. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !>Bye. ACL2 Version 3.6.1. Level 1. Cbd "/Users/kaufmann/talks/seminar-2009-10-28/". Distributed books directory "/Users/kaufmann/acl2/v3-6-1/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "h") Summary Form: ( INCLUDE-BOOK "h" ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) "/Users/kaufmann/talks/seminar-2009-10-28/h.lisp" ACL2 !>:pe-ped append ACL2 Error in LD: Unrecognized keyword command :PE-PED. ACL2 !> ACL2 Error in TOP-LEVEL: Global variables, such as APPEND, are not allowed. See :DOC ASSIGN and :DOC @. ACL2 !>(include-book "enabledp-change") Summary Form: ( INCLUDE-BOOK "enabledp-change" ...) Rules: NIL Warnings: None Time: 0.05 seconds (prove: 0.00, print: 0.00, other: 0.05) "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" ACL2 !>:pe-ped append 1 (INCLUDE-BOOK "h") \ [Included books, outermost to innermost: "/Users/kaufmann/talks/seminar-2009-10-28/h.lisp" ] \ >L (DEFUN FOO (X) X) ACL2 !>(in-theory (enable append)) Summary Form: ( IN-THEORY (ENABLE ...)) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 2068 ACL2 !>(walkabout (w state) state) Commands: 0, 1, 2, ..., nx, bk, pp, =, (= symb), and q. ((COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) (EVENT-LANDMARK GLOBAL-VALUE 6476 ...) (CURRENT-THEORY GLOBAL-VALUE # ...) ...) :1 (COMMAND-LANDMARK GLOBAL-VALUE 5938 ...) :nx (EVENT-LANDMARK GLOBAL-VALUE 6476 ...) :nx (CURRENT-THEORY GLOBAL-VALUE (:TYPE-PRESCRIPTION BAR) ...) :pp (CURRENT-THEORY GLOBAL-VALUE (:TYPE-PRESCRIPTION BAR) (:EXECUTABLE-COUNTERPART BAR) (:DEFINITION BAR) (:TYPE-PRESCRIPTION FOO) (:EXECUTABLE-COUNTERPART FOO) (:DEFINITION FOO) (:TYPE-PRESCRIPTION HONSP-CHECK) (:EXECUTABLE-COUNTERPART HONSP-CHECK) (:DEFINITION HONSP-CHECK) (:TYPE-PRESCRIPTION NUMBER-SUBTREES) (:EXECUTABLE-COUNTERPART NUMBER-SUBTREES) (:DEFINITION NUMBER-SUBTREES) (:INDUCTION FASTER-CONS-SUBTREES) (:TYPE-PRESCRIPTION FASTER-CONS-SUBTREES) (:EXECUTABLE-COUNTERPART FASTER-CONS-SUBTREES) (:DEFINITION FASTER-CONS-SUBTREES) (:INDUCTION CONS-SUBTREES) (:TYPE-PRESCRIPTION CONS-SUBTREES) (:EXECUTABLE-COUNTERPART CONS-SUBTREES) (:DEFINITION CONS-SUBTREES) (:INDUCTION HONS-SHRINK-ALIST) (:TYPE-PRESCRIPTION HONS-SHRINK-ALIST) (:EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST) (:DEFINITION HONS-SHRINK-ALIST) (:INDUCTION HONS-SHRINK-ALIST!) (:TYPE-PRESCRIPTION HONS-SHRINK-ALIST!) (:EXECUTABLE-COUNTERPART HONS-SHRINK-ALIST!) (:DEFINITION HONS-SHRINK-ALIST!) (:TYPE-PRESCRIPTION MEMOIZE-OFF) (:EXECUTABLE-COUNTERPART MEMOIZE-OFF) (:DEFINITION MEMOIZE-OFF) (:TYPE-PRESCRIPTION MEMOIZE-ON) (:EXECUTABLE-COUNTERPART MEMOIZE-ON) (:DEFINITION MEMOIZE-ON) (:TYPE-PRESCRIPTION HONS-ENABLEDP) (:EXECUTABLE-COUNTERPART HONS-ENABLEDP) (:DEFINITION HONS-ENABLEDP) (:TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLES) (:EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLES) (:DEFINITION CLEAR-MEMOIZE-TABLES) (:TYPE-PRESCRIPTION CLEAR-MEMOIZE-TABLE) (:EXECUTABLE-COUNTERPART CLEAR-MEMOIZE-TABLE) (:DEFINITION CLEAR-MEMOIZE-TABLE) (:TYPE-PRESCRIPTION FLUSH-HONS-GET-HASH-TABLE-LINK) (:EXECUTABLE-COUNTERPART FLUSH-HONS-GET-HASH-TABLE-LINK) (:DEFINITION FLUSH-HONS-GET-HASH-TABLE-LINK) (:TYPE-PRESCRIPTION FAST-ALIST-LEN) (:EXECUTABLE-COUNTERPART FAST-ALIST-LEN) (:DEFINITION FAST-ALIST-LEN) (:INDUCTION FAST-ALIST-LEN-ACC) (:TYPE-PRESCRIPTION FAST-ALIST-LEN-ACC) (:EXECUTABLE-COUNTERPART FAST-ALIST-LEN-ACC) (:DEFINITION FAST-ALIST-LEN-ACC) (:TYPE-PRESCRIPTION HONS-ACONS!) (:EXECUTABLE-COUNTERPART HONS-ACONS!) (:DEFINITION HONS-ACONS!) (:TYPE-PRESCRIPTION HONS-ACONS) (:EXECUTABLE-COUNTERPART HONS-ACONS) (:DEFINITION HONS-ACONS) (:TYPE-PRESCRIPTION HONS-GET-FN-DO-NOT-HOPY) (:EXECUTABLE-COUNTERPART HONS-GET-FN-DO-NOT-HOPY) (:DEFINITION HONS-GET-FN-DO-NOT-HOPY) (:TYPE-PRESCRIPTION HONS-GET-FN-DO-HOPY) (:EXECUTABLE-COUNTERPART HONS-GET-FN-DO-HOPY) (:DEFINITION HONS-GET-FN-DO-HOPY) (:INDUCTION HONS-ASSOC-EQUAL) (:TYPE-PRESCRIPTION HONS-ASSOC-EQUAL) (:EXECUTABLE-COUNTERPART HONS-ASSOC-EQUAL) (:DEFINITION HONS-ASSOC-EQUAL) (:TYPE-PRESCRIPTION HONS-COPY) (:EXECUTABLE-COUNTERPART HONS-COPY) (:DEFINITION HONS-COPY) (:TYPE-PRESCRIPTION HONS-EQUAL) (:EXECUTABLE-COUNTERPART HONS-EQUAL) (:DEFINITION HONS-EQUAL) (:TYPE-PRESCRIPTION HONS) (:EXECUTABLE-COUNTERPART HONS) (:DEFINITION HONS) (:TYPE-PRESCRIPTION CLEAR-HASH-TABLES) (:EXECUTABLE-COUNTERPART CLEAR-HASH-TABLES) (:DEFINITION CLEAR-HASH-TABLES) (:TYPE-PRESCRIPTION CPU-CORE-COUNT) (:EXECUTABLE-COUNTERPART CPU-CORE-COUNT) (:DEFINITION CPU-CORE-COUNT) (:TYPE-PRESCRIPTION SEARCH-FN) (:EXECUTABLE-COUNTERPART SEARCH-FN) (:DEFINITION SEARCH-FN) (:INDUCTION SEARCH-FROM-END) (:TYPE-PRESCRIPTION SEARCH-FROM-END) (:EXECUTABLE-COUNTERPART SEARCH-FROM-END) (:DEFINITION SEARCH-FROM-END) (:INDUCTION SEARCH-FROM-START) (:TYPE-PRESCRIPTION SEARCH-FROM-START) (:EXECUTABLE-COUNTERPART SEARCH-FROM-START) (:DEFINITION SEARCH-FROM-START) (:TYPE-PRESCRIPTION SEARCH-FN-GUARD) (:EXECUTABLE-COUNTERPART SEARCH-FN-GUARD) (:DEFINITION SEARCH-FN-GUARD) (:INDUCTION SPLICE-KEYWORD-ALIST) (:TYPE-PRESCRIPTION SPLICE-KEYWORD-ALIST) (:EXECUTABLE-COUNTERPART SPLICE-KEYWORD-ALIST) (:DEFINITION SPLICE-KEYWORD-ALIST) (:TYPE-PRESCRIPTION CLAUSES-RESULT) (:EXECUTABLE-COUNTERPART CLAUSES-RESULT) (:DEFINITION CLAUSES-RESULT) (:TYPE-PRESCRIPTION CONJOIN-CLAUSES) (:EXECUTABLE-COUNTERPART CONJOIN-CLAUSES) (:DEFINITION CONJOIN-CLAUSES) (:INDUCTION DISJOIN-LST) (:TYPE-PRESCRIPTION DISJOIN-LST) (:EXECUTABLE-COUNTERPART DISJOIN-LST) (:DEFINITION DISJOIN-LST) (:INDUCTION DISJOIN) (:TYPE-PRESCRIPTION DISJOIN) (:EXECUTABLE-COUNTERPART DISJOIN) (:DEFINITION DISJOIN) (:TYPE-PRESCRIPTION DISJOIN2) (:EXECUTABLE-COUNTERPART DISJOIN2) (:DEFINITION DISJOIN2) (:INDUCTION CONJOIN) (:TYPE-PRESCRIPTION CONJOIN) (:EXECUTABLE-COUNTERPART CONJOIN) (:DEFINITION CONJOIN) (:TYPE-PRESCRIPTION CONJOIN2) (:EXECUTABLE-COUNTERPART CONJOIN2) (:DEFINITION CONJOIN2) (:TYPE-PRESCRIPTION MOD-EXPT) (:EXECUTABLE-COUNTERPART MOD-EXPT) (:DEFINITION MOD-EXPT) (:INDUCTION E/D-FN) (:TYPE-PRESCRIPTION E/D-FN) (:EXECUTABLE-COUNTERPART E/D-FN) (:DEFINITION E/D-FN) (:INDUCTION RESIZE-LIST) (:TYPE-PRESCRIPTION RESIZE-LIST) (:EXECUTABLE-COUNTERPART RESIZE-LIST) (:DEFINITION RESIZE-LIST) (:INDUCTION MERGE-SORT-LEXORDER) (:TYPE-PRESCRIPTION MERGE-SORT-LEXORDER) (:EXECUTABLE-COUNTERPART MERGE-SORT-LEXORDER) (:DEFINITION MERGE-SORT-LEXORDER) (:TYPE-PRESCRIPTION TRUE-LISTP-MERGE-SORT-LEXORDER) (:INDUCTION MERGE-LEXORDER) (:TYPE-PRESCRIPTION MERGE-LEXORDER) (:EXECUTABLE-COUNTERPART MERGE-LEXORDER) (:DEFINITION MERGE-LEXORDER) (:FORWARD-CHAINING LEXORDER-TOTAL) (:REWRITE LEXORDER-TRANSITIVE) (:FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC) (:REWRITE LEXORDER-REFLEXIVE) (:FORWARD-CHAINING ALPHORDER-TOTAL) (:FORWARD-CHAINING ALPHORDER-ANTI-SYMMETRIC) (:REWRITE ALPHORDER-TRANSITIVE) (:REWRITE ALPHORDER-REFLEXIVE) (:TYPE-PRESCRIPTION LEXORDER) (:EXECUTABLE-COUNTERPART LEXORDER) (:TYPE-PRESCRIPTION ALPHORDER) (:EXECUTABLE-COUNTERPART ALPHORDER) (:REWRITE BAD-ATOM<=-TRANSITIVE) (:TYPE-PRESCRIPTION BOOLEANP-BAD-ATOM<=) (:COMPOUND-RECOGNIZER BAD-ATOM-COMPOUND-RECOGNIZER) (:TYPE-PRESCRIPTION BAD-ATOM) (:EXECUTABLE-COUNTERPART BAD-ATOM) (:REWRITE TYPE-ALISTP-MFC-TYPE-ALIST) (:REWRITE PSEUDO-TERM-LISTP-MFC-CLAUSE) (:TYPE-PRESCRIPTION MFC-ANCESTORS) (:EXECUTABLE-COUNTERPART MFC-ANCESTORS) (:DEFINITION MFC-ANCESTORS) (:TYPE-PRESCRIPTION MFC-TYPE-ALIST) (:EXECUTABLE-COUNTERPART MFC-TYPE-ALIST) (:DEFINITION MFC-TYPE-ALIST) (:INDUCTION TYPE-ALISTP) (:TYPE-PRESCRIPTION TYPE-ALISTP) (:EXECUTABLE-COUNTERPART TYPE-ALISTP) (:DEFINITION TYPE-ALISTP) (:TYPE-PRESCRIPTION TYPE-ALIST-ENTRYP) (:EXECUTABLE-COUNTERPART TYPE-ALIST-ENTRYP) (:DEFINITION TYPE-ALIST-ENTRYP) (:TYPE-PRESCRIPTION MFC-RDEPTH) (:EXECUTABLE-COUNTERPART MFC-RDEPTH) (:DEFINITION MFC-RDEPTH) (:TYPE-PRESCRIPTION MFC-CLAUSE) (:EXECUTABLE-COUNTERPART MFC-CLAUSE) (:DEFINITION MFC-CLAUSE) (:TYPE-PRESCRIPTION RECORD-ACCESSOR-FUNCTION-NAME) (:EXECUTABLE-COUNTERPART RECORD-ACCESSOR-FUNCTION-NAME) (:DEFINITION RECORD-ACCESSOR-FUNCTION-NAME) (:TYPE-PRESCRIPTION RECORD-ERROR) (:EXECUTABLE-COUNTERPART RECORD-ERROR) (:DEFINITION RECORD-ERROR) (:TYPE-PRESCRIPTION SET-EQUALP-EQUAL) (:EXECUTABLE-COUNTERPART SET-EQUALP-EQUAL) (:DEFINITION SET-EQUALP-EQUAL) (:TYPE-PRESCRIPTION ODDS) (:EXECUTABLE-COUNTERPART ODDS) (:DEFINITION ODDS) (:INDUCTION EVENS) (:TYPE-PRESCRIPTION EVENS) (:EXECUTABLE-COUNTERPART EVENS) (:DEFINITION EVENS) (:INDUCTION INTERSECTION-EQ) (:TYPE-PRESCRIPTION INTERSECTION-EQ) (:EXECUTABLE-COUNTERPART INTERSECTION-EQ) (:DEFINITION INTERSECTION-EQ) (:TYPE-PRESCRIPTION ADD-TO-SET-EQUAL) (:EXECUTABLE-COUNTERPART ADD-TO-SET-EQUAL) (:DEFINITION ADD-TO-SET-EQUAL) (:INDUCTION DUPLICATES) (:TYPE-PRESCRIPTION DUPLICATES) (:EXECUTABLE-COUNTERPART DUPLICATES) (:DEFINITION DUPLICATES) (:INDUCTION PAIRLIS2) (:TYPE-PRESCRIPTION PAIRLIS2) (:EXECUTABLE-COUNTERPART PAIRLIS2) (:DEFINITION PAIRLIS2) (:TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW!) (:EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW!) (:DEFINITION FMT-TO-COMMENT-WINDOW!) (:TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW) (:EXECUTABLE-COUNTERPART FMT-TO-COMMENT-WINDOW) (:DEFINITION FMT-TO-COMMENT-WINDOW) (:TYPE-PRESCRIPTION ABORT!) (:TYPE-PRESCRIPTION WORMHOLE-P) (:EXECUTABLE-COUNTERPART WORMHOLE-P) (:DEFINITION WORMHOLE-P) (:TYPE-PRESCRIPTION WORMHOLE1) (:EXECUTABLE-COUNTERPART WORMHOLE1) (:DEFINITION WORMHOLE1) (:TYPE-PRESCRIPTION TIME-LIMIT4-REACHED-P) (:EXECUTABLE-COUNTERPART TIME-LIMIT4-REACHED-P) (:DEFINITION TIME-LIMIT4-REACHED-P) (:TYPE-PRESCRIPTION WITH-PROVER-TIME-LIMIT) (:EXECUTABLE-COUNTERPART WITH-PROVER-TIME-LIMIT) (:DEFINITION WITH-PROVER-TIME-LIMIT) (:TYPE-PRESCRIPTION DOUBLE-REWRITE) (:EXECUTABLE-COUNTERPART DOUBLE-REWRITE) (:DEFINITION DOUBLE-REWRITE) (:REWRITE DEFAULT-SYMBOL-PACKAGE-NAME) (:REWRITE DEFAULT-SYMBOL-NAME) (:REWRITE DEFAULT-REALPART) (:REWRITE DEFAULT-NUMERATOR) (:REWRITE DEFAULT-IMAGPART) (:REWRITE DEFAULT-DENOMINATOR) (:REWRITE DEFAULT-COERCE-3) (:REWRITE DEFAULT-COERCE-2) (:REWRITE MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST) (:REWRITE DEFAULT-COERCE-1) (:REWRITE IMAGPART-+) (:REWRITE REALPART-+) (:REWRITE COMPLEX-0) (:REWRITE DEFAULT-COMPLEX-2) (:REWRITE DEFAULT-COMPLEX-1) (:REWRITE DEFAULT-CHAR-CODE) (:REWRITE CONS-CAR-CDR) (:REWRITE DEFAULT-CDR) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-<-2) (:REWRITE DEFAULT-<-1) (:REWRITE DEFAULT-UNARY-/) (:REWRITE DEFAULT-UNARY-MINUS) (:REWRITE DEFAULT-*-2) (:REWRITE DEFAULT-*-1) (:REWRITE DEFAULT-+-2) (:REWRITE DEFAULT-+-1) (:FORWARD-CHAINING BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP) (:FORWARD-CHAINING BOOLEAN-LISTP-FORWARD) (:REWRITE BOOLEAN-LISTP-CONS) (:INDUCTION BOOLEAN-LISTP) (:TYPE-PRESCRIPTION BOOLEAN-LISTP) (:EXECUTABLE-COUNTERPART BOOLEAN-LISTP) (:DEFINITION BOOLEAN-LISTP) (:REWRITE PAIRLIS$-FIX-TRUE-LIST) (:INDUCTION FIX-TRUE-LIST) (:TYPE-PRESCRIPTION FIX-TRUE-LIST) (:EXECUTABLE-COUNTERPART FIX-TRUE-LIST) (:DEFINITION FIX-TRUE-LIST) (:TYPE-PRESCRIPTION DEFAULT-HINTS) (:EXECUTABLE-COUNTERPART DEFAULT-HINTS) (:DEFINITION DEFAULT-HINTS) (:TYPE-PRESCRIPTION NTH-ALIASES) (:EXECUTABLE-COUNTERPART NTH-ALIASES) (:DEFINITION NTH-ALIASES) (:TYPE-PRESCRIPTION MACRO-ALIASES) (:EXECUTABLE-COUNTERPART MACRO-ALIASES) (:DEFINITION MACRO-ALIASES) (:TYPE-PRESCRIPTION NON-LINEARP) (:EXECUTABLE-COUNTERPART NON-LINEARP) (:DEFINITION NON-LINEARP) (:TYPE-PRESCRIPTION MATCH-FREE-OVERRIDE) (:EXECUTABLE-COUNTERPART MATCH-FREE-OVERRIDE) (:DEFINITION MATCH-FREE-OVERRIDE) (:TYPE-PRESCRIPTION MATCH-FREE-DEFAULT) (:EXECUTABLE-COUNTERPART MATCH-FREE-DEFAULT) (:DEFINITION MATCH-FREE-DEFAULT) (:TYPE-PRESCRIPTION BINOP-TABLE) (:EXECUTABLE-COUNTERPART BINOP-TABLE) (:DEFINITION BINOP-TABLE) (:TYPE-PRESCRIPTION CASE-SPLIT-LIMITATIONS) (:EXECUTABLE-COUNTERPART CASE-SPLIT-LIMITATIONS) (:DEFINITION CASE-SPLIT-LIMITATIONS) (:TYPE-PRESCRIPTION REWRITE-STACK-LIMIT) (:EXECUTABLE-COUNTERPART REWRITE-STACK-LIMIT) (:DEFINITION REWRITE-STACK-LIMIT) (:TYPE-PRESCRIPTION DEFAULT-BACKCHAIN-LIMIT) (:EXECUTABLE-COUNTERPART DEFAULT-BACKCHAIN-LIMIT) (:DEFINITION DEFAULT-BACKCHAIN-LIMIT) (:TYPE-PRESCRIPTION BACKCHAIN-LIMIT) (:EXECUTABLE-COUNTERPART BACKCHAIN-LIMIT) (:DEFINITION BACKCHAIN-LIMIT) (:INDUCTION DELETE-ASSOC-EQUAL) (:TYPE-PRESCRIPTION DELETE-ASSOC-EQUAL) (:EXECUTABLE-COUNTERPART DELETE-ASSOC-EQUAL) (:DEFINITION DELETE-ASSOC-EQUAL) (:INDUCTION DELETE-ASSOC-EQ) (:TYPE-PRESCRIPTION DELETE-ASSOC-EQ) (:EXECUTABLE-COUNTERPART DELETE-ASSOC-EQ) (:DEFINITION DELETE-ASSOC-EQ) (:TYPE-PRESCRIPTION INVISIBLE-FNS-ENTRYP) (:EXECUTABLE-COUNTERPART INVISIBLE-FNS-ENTRYP) (:DEFINITION INVISIBLE-FNS-ENTRYP) (:INDUCTION UNARY-FUNCTION-SYMBOL-LISTP) (:TYPE-PRESCRIPTION UNARY-FUNCTION-SYMBOL-LISTP) (:EXECUTABLE-COUNTERPART UNARY-FUNCTION-SYMBOL-LISTP) (:DEFINITION UNARY-FUNCTION-SYMBOL-LISTP) (:TYPE-PRESCRIPTION INVISIBLE-FNS-TABLE) (:EXECUTABLE-COUNTERPART INVISIBLE-FNS-TABLE) (:DEFINITION INVISIBLE-FNS-TABLE) (:TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE-FROM-STATE) (:EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE-FROM-STATE) (:DEFINITION DEFAULT-DEFUN-MODE-FROM-STATE) (:TYPE-PRESCRIPTION DEFAULT-DEFUN-MODE) (:EXECUTABLE-COUNTERPART DEFAULT-DEFUN-MODE) (:DEFINITION DEFAULT-DEFUN-MODE) (:TYPE-PRESCRIPTION DEFAULT-WELL-FOUNDED-RELATION) (:EXECUTABLE-COUNTERPART DEFAULT-WELL-FOUNDED-RELATION) (:DEFINITION DEFAULT-WELL-FOUNDED-RELATION) (:TYPE-PRESCRIPTION DEFAULT-MEASURE-FUNCTION) (:EXECUTABLE-COUNTERPART DEFAULT-MEASURE-FUNCTION) (:DEFINITION DEFAULT-MEASURE-FUNCTION) (:TYPE-PRESCRIPTION DEFAULT-COMPILE-FNS) (:EXECUTABLE-COUNTERPART DEFAULT-COMPILE-FNS) (:DEFINITION DEFAULT-COMPILE-FNS) (:TYPE-PRESCRIPTION DEFAULT-VERIFY-GUARDS-EAGERNESS) (:EXECUTABLE-COUNTERPART DEFAULT-VERIFY-GUARDS-EAGERNESS) (:DEFINITION DEFAULT-VERIFY-GUARDS-EAGERNESS) (:TYPE-PRESCRIPTION TABLE-ALIST) (:EXECUTABLE-COUNTERPART TABLE-ALIST) (:DEFINITION TABLE-ALIST) (:INDUCTION LEGAL-RULER-EXTENDERS-P) (:TYPE-PRESCRIPTION LEGAL-RULER-EXTENDERS-P) (:EXECUTABLE-COUNTERPART LEGAL-RULER-EXTENDERS-P) (:DEFINITION LEGAL-RULER-EXTENDERS-P) (:INDUCTION INCLUDE-BOOK-DIR-ALISTP) (:TYPE-PRESCRIPTION INCLUDE-BOOK-DIR-ALISTP) (:EXECUTABLE-COUNTERPART INCLUDE-BOOK-DIR-ALISTP) (:DEFINITION INCLUDE-BOOK-DIR-ALISTP) (:TYPE-PRESCRIPTION OS) (:EXECUTABLE-COUNTERPART OS) (:DEFINITION OS) (:TYPE-PRESCRIPTION ABSOLUTE-PATHNAME-STRING-P) (:EXECUTABLE-COUNTERPART ABSOLUTE-PATHNAME-STRING-P) (:DEFINITION ABSOLUTE-PATHNAME-STRING-P) (:TYPE-PRESCRIPTION NATP-POSITION-AC) (:TYPE-PRESCRIPTION FREE-VAR-RUNES) (:EXECUTABLE-COUNTERPART FREE-VAR-RUNES) (:DEFINITION FREE-VAR-RUNES) (:INDUCTION NON-FREE-VAR-RUNES) (:TYPE-PRESCRIPTION NON-FREE-VAR-RUNES) (:EXECUTABLE-COUNTERPART NON-FREE-VAR-RUNES) (:DEFINITION NON-FREE-VAR-RUNES) (:TYPE-PRESCRIPTION MAKE-VAR-LST) (:EXECUTABLE-COUNTERPART MAKE-VAR-LST) (:DEFINITION MAKE-VAR-LST) (:INDUCTION MAKE-VAR-LST1) (:TYPE-PRESCRIPTION MAKE-VAR-LST1) (:EXECUTABLE-COUNTERPART MAKE-VAR-LST1) (:DEFINITION MAKE-VAR-LST1) (:TYPE-PRESCRIPTION LD-SKIP-PROOFSP) (:EXECUTABLE-COUNTERPART LD-SKIP-PROOFSP) (:DEFINITION LD-SKIP-PROOFSP) (:INDUCTION UNION-EQ) (:TYPE-PRESCRIPTION UNION-EQ) (:EXECUTABLE-COUNTERPART UNION-EQ) (:DEFINITION UNION-EQ) (:TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL) (:REWRITE STATE-P1-UPDATE-NTH-2-WORLD) (:TYPE-PRESCRIPTION KNOWN-PACKAGE-ALIST) (:EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALIST) (:DEFINITION KNOWN-PACKAGE-ALIST) (:TYPE-PRESCRIPTION CURRENT-PACKAGE) (:EXECUTABLE-COUNTERPART CURRENT-PACKAGE) (:DEFINITION CURRENT-PACKAGE) (:TYPE-PRESCRIPTION W) (:EXECUTABLE-COUNTERPART W) (:DEFINITION W) (:TYPE-PRESCRIPTION PRIN1$) (:EXECUTABLE-COUNTERPART PRIN1$) (:DEFINITION PRIN1$) (:TYPE-PRESCRIPTION PRINT-TIMER) (:EXECUTABLE-COUNTERPART PRINT-TIMER) (:DEFINITION PRINT-TIMER) (:TYPE-PRESCRIPTION PRINT-RATIONAL-AS-DECIMAL) (:EXECUTABLE-COUNTERPART PRINT-RATIONAL-AS-DECIMAL) (:DEFINITION PRINT-RATIONAL-AS-DECIMAL) (:TYPE-PRESCRIPTION INCREMENT-TIMER) (:EXECUTABLE-COUNTERPART INCREMENT-TIMER) (:DEFINITION INCREMENT-TIMER) (:FORWARD-CHAINING STATE-P1-UPDATE-MAIN-TIMER) (:REWRITE ADD-PAIR-PRESERVES-ALL-BOUNDP) (:REWRITE ASSOC-ADD-PAIR) (:FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD) (:TYPE-PRESCRIPTION MAIN-TIMER-TYPE-PRESCRIPTION) (:REWRITE NTH-ADD1) (:REWRITE NTH-0-CONS) (:TYPE-PRESCRIPTION ADD-TIMERS) (:EXECUTABLE-COUNTERPART ADD-TIMERS) (:DEFINITION ADD-TIMERS) (:TYPE-PRESCRIPTION POP-TIMER) (:EXECUTABLE-COUNTERPART POP-TIMER) (:DEFINITION POP-TIMER) (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP) (:REWRITE RATIONALP-UNARY-/) (:REWRITE RATIONALP-UNARY--) (:REWRITE RATIONALP-*) (:REWRITE RATIONALP-+) (:TYPE-PRESCRIPTION PUSH-TIMER) (:EXECUTABLE-COUNTERPART PUSH-TIMER) (:DEFINITION PUSH-TIMER) (:TYPE-PRESCRIPTION GET-TIMER) (:EXECUTABLE-COUNTERPART GET-TIMER) (:DEFINITION GET-TIMER) (:TYPE-PRESCRIPTION SET-TIMER) (:EXECUTABLE-COUNTERPART SET-TIMER) (:DEFINITION SET-TIMER) (:INDUCTION PUT-ASSOC-EQUAL) (:TYPE-PRESCRIPTION PUT-ASSOC-EQUAL) (:EXECUTABLE-COUNTERPART PUT-ASSOC-EQUAL) (:DEFINITION PUT-ASSOC-EQUAL) (:INDUCTION PUT-ASSOC-EQL) (:TYPE-PRESCRIPTION PUT-ASSOC-EQL) (:EXECUTABLE-COUNTERPART PUT-ASSOC-EQL) (:DEFINITION PUT-ASSOC-EQL) (:INDUCTION PUT-ASSOC-EQ) (:TYPE-PRESCRIPTION PUT-ASSOC-EQ) (:EXECUTABLE-COUNTERPART PUT-ASSOC-EQ) (:DEFINITION PUT-ASSOC-EQ) (:TYPE-PRESCRIPTION MAIN-TIMER) (:EXECUTABLE-COUNTERPART MAIN-TIMER) (:DEFINITION MAIN-TIMER) (:TYPE-PRESCRIPTION NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION) (:FORWARD-CHAINING READ-ACL2-ORACLE-PRESERVES-STATE-P1) (:FORWARD-CHAINING READ-RUN-TIME-PRESERVES-STATE-P1) (:REWRITE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1) (:REWRITE LEN-UPDATE-NTH) (:TYPE-PRESCRIPTION RANDOM$) (:EXECUTABLE-COUNTERPART RANDOM$) (:TYPE-PRESCRIPTION SETENV$) (:EXECUTABLE-COUNTERPART SETENV$) (:DEFINITION SETENV$) (:TYPE-PRESCRIPTION GETENV$) (:EXECUTABLE-COUNTERPART GETENV$) (:DEFINITION GETENV$) (:TYPE-PRESCRIPTION READ-ACL2-ORACLE) (:EXECUTABLE-COUNTERPART READ-ACL2-ORACLE) (:TYPE-PRESCRIPTION READ-RUN-TIME) (:EXECUTABLE-COUNTERPART READ-RUN-TIME) (:TYPE-PRESCRIPTION READ-IDATE) (:EXECUTABLE-COUNTERPART READ-IDATE) (:DEFINITION READ-IDATE) (:INDUCTION POWER-EVAL) (:TYPE-PRESCRIPTION POWER-EVAL) (:EXECUTABLE-COUNTERPART POWER-EVAL) (:DEFINITION POWER-EVAL) (:TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST) (:EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST) (:DEFINITION UPDATE-USER-STOBJ-ALIST) (:TYPE-PRESCRIPTION USER-STOBJ-ALIST) (:EXECUTABLE-COUNTERPART USER-STOBJ-ALIST) (:DEFINITION USER-STOBJ-ALIST) (:TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES) (:EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES) (:DEFINITION LIST-ALL-PACKAGE-NAMES) (:TYPE-PRESCRIPTION DECREMENT-BIG-CLOCK) (:EXECUTABLE-COUNTERPART DECREMENT-BIG-CLOCK) (:DEFINITION DECREMENT-BIG-CLOCK) (:TYPE-PRESCRIPTION BIG-CLOCK-NEGATIVE-P) (:EXECUTABLE-COUNTERPART BIG-CLOCK-NEGATIVE-P) (:DEFINITION BIG-CLOCK-NEGATIVE-P) (:TYPE-PRESCRIPTION ASET-32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART ASET-32-BIT-INTEGER-STACK) (:DEFINITION ASET-32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION AREF-32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART AREF-32-BIT-INTEGER-STACK) (:DEFINITION AREF-32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION SHRINK-32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART SHRINK-32-BIT-INTEGER-STACK) (:DEFINITION SHRINK-32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION EXTEND-32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART EXTEND-32-BIT-INTEGER-STACK) (:DEFINITION EXTEND-32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH) (:EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH) (:DEFINITION 32-BIT-INTEGER-STACK-LENGTH) (:TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK-LENGTH1) (:EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK-LENGTH1) (:DEFINITION 32-BIT-INTEGER-STACK-LENGTH1) (:TYPE-PRESCRIPTION ASET-T-STACK) (:EXECUTABLE-COUNTERPART ASET-T-STACK) (:DEFINITION ASET-T-STACK) (:TYPE-PRESCRIPTION AREF-T-STACK) (:EXECUTABLE-COUNTERPART AREF-T-STACK) (:DEFINITION AREF-T-STACK) (:TYPE-PRESCRIPTION SHRINK-T-STACK) (:EXECUTABLE-COUNTERPART SHRINK-T-STACK) (:DEFINITION SHRINK-T-STACK) (:TYPE-PRESCRIPTION SUBSEQ) (:EXECUTABLE-COUNTERPART SUBSEQ) (:DEFINITION SUBSEQ) (:TYPE-PRESCRIPTION SUBSEQ-LIST) (:EXECUTABLE-COUNTERPART SUBSEQ-LIST) (:DEFINITION SUBSEQ-LIST) (:TYPE-PRESCRIPTION EXTEND-T-STACK) (:EXECUTABLE-COUNTERPART EXTEND-T-STACK) (:DEFINITION EXTEND-T-STACK) (:INDUCTION MAKE-LIST-AC) (:TYPE-PRESCRIPTION MAKE-LIST-AC) (:EXECUTABLE-COUNTERPART MAKE-LIST-AC) (:DEFINITION MAKE-LIST-AC) (:TYPE-PRESCRIPTION T-STACK-LENGTH) (:EXECUTABLE-COUNTERPART T-STACK-LENGTH) (:DEFINITION T-STACK-LENGTH) (:TYPE-PRESCRIPTION T-STACK-LENGTH1) (:EXECUTABLE-COUNTERPART T-STACK-LENGTH1) (:DEFINITION T-STACK-LENGTH1) (:TYPE-PRESCRIPTION NEEDS-SLASHES) (:EXECUTABLE-COUNTERPART NEEDS-SLASHES) (:DEFINITION NEEDS-SLASHES) (:TYPE-PRESCRIPTION MAY-NEED-SLASHES-FN) (:EXECUTABLE-COUNTERPART MAY-NEED-SLASHES-FN) (:DEFINITION MAY-NEED-SLASHES-FN) (:INDUCTION MAY-NEED-SLASHES1) (:TYPE-PRESCRIPTION MAY-NEED-SLASHES1) (:EXECUTABLE-COUNTERPART MAY-NEED-SLASHES1) (:DEFINITION MAY-NEED-SLASHES1) (:TYPE-PRESCRIPTION PRIN1-WITH-SLASHES) (:EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES) (:DEFINITION PRIN1-WITH-SLASHES) (:INDUCTION PRIN1-WITH-SLASHES1) (:TYPE-PRESCRIPTION PRIN1-WITH-SLASHES1) (:EXECUTABLE-COUNTERPART PRIN1-WITH-SLASHES1) (:DEFINITION PRIN1-WITH-SLASHES1) (:INDUCTION SOME-SLASHABLE) (:TYPE-PRESCRIPTION SOME-SLASHABLE) (:EXECUTABLE-COUNTERPART SOME-SLASHABLE) (:DEFINITION SOME-SLASHABLE) (:TYPE-PRESCRIPTION READ-OBJECT) (:EXECUTABLE-COUNTERPART READ-OBJECT) (:DEFINITION READ-OBJECT) (:TYPE-PRESCRIPTION READ-BYTE$) (:EXECUTABLE-COUNTERPART READ-BYTE$) (:DEFINITION READ-BYTE$) (:TYPE-PRESCRIPTION PEEK-CHAR$) (:EXECUTABLE-COUNTERPART PEEK-CHAR$) (:DEFINITION PEEK-CHAR$) (:TYPE-PRESCRIPTION READ-CHAR$) (:EXECUTABLE-COUNTERPART READ-CHAR$) (:DEFINITION READ-CHAR$) (:TYPE-PRESCRIPTION CLOSE-OUTPUT-CHANNEL) (:EXECUTABLE-COUNTERPART CLOSE-OUTPUT-CHANNEL) (:DEFINITION CLOSE-OUTPUT-CHANNEL) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL!) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL!) (:DEFINITION OPEN-OUTPUT-CHANNEL!) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL) (:DEFINITION OPEN-OUTPUT-CHANNEL) (:TYPE-PRESCRIPTION CLOSE-INPUT-CHANNEL) (:EXECUTABLE-COUNTERPART CLOSE-INPUT-CHANNEL) (:DEFINITION CLOSE-INPUT-CHANNEL) (:REWRITE NTH-UPDATE-NTH-ARRAY) (:TYPE-PRESCRIPTION TRUE-LISTP-UPDATE-NTH) (:REWRITE NTH-UPDATE-NTH) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL) (:DEFINITION OPEN-INPUT-CHANNEL) (:TYPE-PRESCRIPTION MAKE-OUTPUT-CHANNEL) (:EXECUTABLE-COUNTERPART MAKE-OUTPUT-CHANNEL) (:DEFINITION MAKE-OUTPUT-CHANNEL) (:TYPE-PRESCRIPTION MAKE-INPUT-CHANNEL) (:EXECUTABLE-COUNTERPART MAKE-INPUT-CHANNEL) (:DEFINITION MAKE-INPUT-CHANNEL) (:TYPE-PRESCRIPTION PRINT-OBJECT$) (:EXECUTABLE-COUNTERPART PRINT-OBJECT$) (:DEFINITION PRINT-OBJECT$) (:TYPE-PRESCRIPTION WRITE-BYTE$) (:EXECUTABLE-COUNTERPART WRITE-BYTE$) (:DEFINITION WRITE-BYTE$) (:TYPE-PRESCRIPTION PRINC$) (:EXECUTABLE-COUNTERPART PRINC$) (:DEFINITION PRINC$) (:TYPE-PRESCRIPTION SET-PRINT-RIGHT-MARGIN) (:EXECUTABLE-COUNTERPART SET-PRINT-RIGHT-MARGIN) (:DEFINITION SET-PRINT-RIGHT-MARGIN) (:TYPE-PRESCRIPTION SET-PRINT-LINES) (:EXECUTABLE-COUNTERPART SET-PRINT-LINES) (:DEFINITION SET-PRINT-LINES) (:TYPE-PRESCRIPTION SET-PRINT-LEVEL) (:EXECUTABLE-COUNTERPART SET-PRINT-LEVEL) (:DEFINITION SET-PRINT-LEVEL) (:TYPE-PRESCRIPTION SET-PRINT-LENGTH) (:EXECUTABLE-COUNTERPART SET-PRINT-LENGTH) (:DEFINITION SET-PRINT-LENGTH) (:TYPE-PRESCRIPTION CHECK-NULL-OR-NATP) (:EXECUTABLE-COUNTERPART CHECK-NULL-OR-NATP) (:DEFINITION CHECK-NULL-OR-NATP) (:TYPE-PRESCRIPTION SET-PRINT-READABLY) (:EXECUTABLE-COUNTERPART SET-PRINT-READABLY) (:DEFINITION SET-PRINT-READABLY) (:TYPE-PRESCRIPTION SET-PRINT-RADIX) (:EXECUTABLE-COUNTERPART SET-PRINT-RADIX) (:DEFINITION SET-PRINT-RADIX) (:TYPE-PRESCRIPTION SET-PRINT-PRETTY) (:EXECUTABLE-COUNTERPART SET-PRINT-PRETTY) (:DEFINITION SET-PRINT-PRETTY) (:TYPE-PRESCRIPTION SET-PRINT-ESCAPE) (:EXECUTABLE-COUNTERPART SET-PRINT-ESCAPE) (:DEFINITION SET-PRINT-ESCAPE) (:TYPE-PRESCRIPTION SET-PRINT-CIRCLE) (:EXECUTABLE-COUNTERPART SET-PRINT-CIRCLE) (:DEFINITION SET-PRINT-CIRCLE) (:TYPE-PRESCRIPTION SET-PRINT-BASE) (:EXECUTABLE-COUNTERPART SET-PRINT-BASE) (:DEFINITION SET-PRINT-BASE) (:TYPE-PRESCRIPTION CHECK-PRINT-BASE) (:EXECUTABLE-COUNTERPART CHECK-PRINT-BASE) (:DEFINITION CHECK-PRINT-BASE) (:TYPE-PRESCRIPTION SET-PRINT-CASE) (:EXECUTABLE-COUNTERPART SET-PRINT-CASE) (:DEFINITION SET-PRINT-CASE) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P) (:DEFINITION OPEN-INPUT-CHANNEL-ANY-P) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-ANY-P1) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-ANY-P1) (:DEFINITION OPEN-INPUT-CHANNEL-ANY-P1) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P) (:DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-ANY-P1) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-ANY-P1) (:DEFINITION OPEN-OUTPUT-CHANNEL-ANY-P1) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P) (:DEFINITION OPEN-OUTPUT-CHANNEL-P) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P) (:DEFINITION OPEN-INPUT-CHANNEL-P) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNEL-P1) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNEL-P1) (:DEFINITION OPEN-OUTPUT-CHANNEL-P1) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNEL-P1) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNEL-P1) (:DEFINITION OPEN-INPUT-CHANNEL-P1) (:FORWARD-CHAINING TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P) (:TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ) (:INDUCTION EXPLODE-ATOM) (:TYPE-PRESCRIPTION EXPLODE-ATOM) (:EXECUTABLE-COUNTERPART EXPLODE-ATOM) (:DEFINITION EXPLODE-ATOM) (:INDUCTION EXPLODE-NONNEGATIVE-INTEGER) (:TYPE-PRESCRIPTION EXPLODE-NONNEGATIVE-INTEGER) (:EXECUTABLE-COUNTERPART EXPLODE-NONNEGATIVE-INTEGER) (:DEFINITION EXPLODE-NONNEGATIVE-INTEGER) (:TYPE-PRESCRIPTION PRINT-BASE-P) (:EXECUTABLE-COUNTERPART PRINT-BASE-P) (:DEFINITION PRINT-BASE-P) (:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (:EXECUTABLE-COUNTERPART DIGIT-TO-CHAR) (:DEFINITION DIGIT-TO-CHAR) (:INDUCTION ALIST-DIFFERENCE-EQ) (:TYPE-PRESCRIPTION ALIST-DIFFERENCE-EQ) (:EXECUTABLE-COUNTERPART ALIST-DIFFERENCE-EQ) (:DEFINITION ALIST-DIFFERENCE-EQ) (:INDUCTION SET-FORMS-FROM-BINDINGS) (:TYPE-PRESCRIPTION SET-FORMS-FROM-BINDINGS) (:EXECUTABLE-COUNTERPART SET-FORMS-FROM-BINDINGS) (:DEFINITION SET-FORMS-FROM-BINDINGS) (:TYPE-PRESCRIPTION BOOLE$) (:EXECUTABLE-COUNTERPART BOOLE$) (:DEFINITION BOOLE$) (:TYPE-PRESCRIPTION LOGTEST) (:EXECUTABLE-COUNTERPART LOGTEST) (:DEFINITION LOGTEST) (:TYPE-PRESCRIPTION LOGNOR) (:EXECUTABLE-COUNTERPART LOGNOR) (:DEFINITION LOGNOR) (:TYPE-PRESCRIPTION BINARY-LOGXOR) (:EXECUTABLE-COUNTERPART BINARY-LOGXOR) (:DEFINITION BINARY-LOGXOR) (:TYPE-PRESCRIPTION BINARY-LOGEQV) (:EXECUTABLE-COUNTERPART BINARY-LOGEQV) (:DEFINITION BINARY-LOGEQV) (:TYPE-PRESCRIPTION LOGANDC2) (:EXECUTABLE-COUNTERPART LOGANDC2) (:DEFINITION LOGANDC2) (:TYPE-PRESCRIPTION LOGANDC1) (:EXECUTABLE-COUNTERPART LOGANDC1) (:DEFINITION LOGANDC1) (:TYPE-PRESCRIPTION LOGORC2) (:EXECUTABLE-COUNTERPART LOGORC2) (:DEFINITION LOGORC2) (:TYPE-PRESCRIPTION LOGORC1) (:EXECUTABLE-COUNTERPART LOGORC1) (:DEFINITION LOGORC1) (:TYPE-PRESCRIPTION BINARY-LOGIOR) (:EXECUTABLE-COUNTERPART BINARY-LOGIOR) (:DEFINITION BINARY-LOGIOR) (:TYPE-PRESCRIPTION LOGNAND) (:EXECUTABLE-COUNTERPART LOGNAND) (:DEFINITION LOGNAND) (:INDUCTION BINARY-LOGAND) (:TYPE-PRESCRIPTION BINARY-LOGAND) (:EXECUTABLE-COUNTERPART BINARY-LOGAND) (:DEFINITION BINARY-LOGAND) (:INDUCTION INTEGER-LENGTH) (:TYPE-PRESCRIPTION INTEGER-LENGTH) (:EXECUTABLE-COUNTERPART INTEGER-LENGTH) (:DEFINITION INTEGER-LENGTH) (:REWRITE ORDERED-SYMBOL-ALISTP-GETPROPS) (:REWRITE ORDERED-SYMBOL-ALISTP-ADD-PAIR) (:REWRITE SYMBOL-<-IRREFLEXIVE) (:REWRITE ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR) (:REWRITE SYMBOL-<-TRICHOTOMY) (:REWRITE STRING<-L-TRICHOTOMY) (:REWRITE SYMBOL-<-TRANSITIVE) (:REWRITE STRING<-L-TRANSITIVE) (:REWRITE SYMBOL-<-ASYMMETRIC) (:REWRITE STRING<-L-ASYMMETRIC) (:TYPE-PRESCRIPTION ZPF) (:EXECUTABLE-COUNTERPART ZPF) (:DEFINITION ZPF) (:FORWARD-CHAINING UNSIGNED-BYTE-P-FORWARD-TO-NONNEGATIVE-INTEGERP) (:FORWARD-CHAINING SIGNED-BYTE-P-FORWARD-TO-INTEGERP) (:FORWARD-CHAINING INTEGER-RANGE-P-FORWARD) (:TYPE-PRESCRIPTION UNSIGNED-BYTE-P) (:EXECUTABLE-COUNTERPART UNSIGNED-BYTE-P) (:DEFINITION UNSIGNED-BYTE-P) (:TYPE-PRESCRIPTION SIGNED-BYTE-P) (:EXECUTABLE-COUNTERPART SIGNED-BYTE-P) (:DEFINITION SIGNED-BYTE-P) (:TYPE-PRESCRIPTION INTEGER-RANGE-P) (:EXECUTABLE-COUNTERPART INTEGER-RANGE-P) (:DEFINITION INTEGER-RANGE-P) (:INDUCTION STATE-GLOBAL-LET*-CLEANUP) (:TYPE-PRESCRIPTION STATE-GLOBAL-LET*-CLEANUP) (:EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-CLEANUP) (:DEFINITION STATE-GLOBAL-LET*-CLEANUP) (:INDUCTION STATE-GLOBAL-LET*-PUT-GLOBALS) (:TYPE-PRESCRIPTION STATE-GLOBAL-LET*-PUT-GLOBALS) (:EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-PUT-GLOBALS) (:DEFINITION STATE-GLOBAL-LET*-PUT-GLOBALS) (:INDUCTION STATE-GLOBAL-LET*-GET-GLOBALS) (:TYPE-PRESCRIPTION STATE-GLOBAL-LET*-GET-GLOBALS) (:EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-GET-GLOBALS) (:DEFINITION STATE-GLOBAL-LET*-GET-GLOBALS) (:INDUCTION STATE-GLOBAL-LET*-BINDINGS-P) (:TYPE-PRESCRIPTION STATE-GLOBAL-LET*-BINDINGS-P) (:EXECUTABLE-COUNTERPART STATE-GLOBAL-LET*-BINDINGS-P) (:DEFINITION STATE-GLOBAL-LET*-BINDINGS-P) (:TYPE-PRESCRIPTION ALWAYS-BOUNDP-GLOBAL) (:EXECUTABLE-COUNTERPART ALWAYS-BOUNDP-GLOBAL) (:DEFINITION ALWAYS-BOUNDP-GLOBAL) (:INDUCTION SYMBOL-DOUBLET-LISTP) (:TYPE-PRESCRIPTION SYMBOL-DOUBLET-LISTP) (:EXECUTABLE-COUNTERPART SYMBOL-DOUBLET-LISTP) (:DEFINITION SYMBOL-DOUBLET-LISTP) (:TYPE-PRESCRIPTION PUT-GLOBAL) (:EXECUTABLE-COUNTERPART PUT-GLOBAL) (:DEFINITION PUT-GLOBAL) (:TYPE-PRESCRIPTION GET-GLOBAL) (:EXECUTABLE-COUNTERPART GET-GLOBAL) (:DEFINITION GET-GLOBAL) (:TYPE-PRESCRIPTION MAKUNBOUND-GLOBAL) (:EXECUTABLE-COUNTERPART MAKUNBOUND-GLOBAL) (:DEFINITION MAKUNBOUND-GLOBAL) (:INDUCTION DELETE-PAIR) (:TYPE-PRESCRIPTION DELETE-PAIR) (:EXECUTABLE-COUNTERPART DELETE-PAIR) (:DEFINITION DELETE-PAIR) (:TYPE-PRESCRIPTION BOUNDP-GLOBAL) (:EXECUTABLE-COUNTERPART BOUNDP-GLOBAL) (:DEFINITION BOUNDP-GLOBAL) (:TYPE-PRESCRIPTION BOUNDP-GLOBAL1) (:EXECUTABLE-COUNTERPART BOUNDP-GLOBAL1) (:DEFINITION BOUNDP-GLOBAL1) (:TYPE-PRESCRIPTION GLOBAL-TABLE-CARS) (:EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS) (:DEFINITION GLOBAL-TABLE-CARS) (:TYPE-PRESCRIPTION GLOBAL-TABLE-CARS1) (:EXECUTABLE-COUNTERPART GLOBAL-TABLE-CARS1) (:DEFINITION GLOBAL-TABLE-CARS1) (:TYPE-PRESCRIPTION COERCE-OBJECT-TO-STATE) (:EXECUTABLE-COUNTERPART COERCE-OBJECT-TO-STATE) (:DEFINITION COERCE-OBJECT-TO-STATE) (:TYPE-PRESCRIPTION COERCE-STATE-TO-OBJECT) (:EXECUTABLE-COUNTERPART COERCE-STATE-TO-OBJECT) (:DEFINITION COERCE-STATE-TO-OBJECT) (:TYPE-PRESCRIPTION BUILD-STATE1) (:EXECUTABLE-COUNTERPART BUILD-STATE1) (:DEFINITION BUILD-STATE1) (:REWRITE STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (:FORWARD-CHAINING STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1) (:TYPE-PRESCRIPTION STATE-P) (:EXECUTABLE-COUNTERPART STATE-P) (:DEFINITION STATE-P) (:FORWARD-CHAINING STATE-P1-FORWARD) (:TYPE-PRESCRIPTION STATE-P1) (:EXECUTABLE-COUNTERPART STATE-P1) (:FORWARD-CHAINING WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP) (:TYPE-PRESCRIPTION WRITEABLE-FILES-P) (:EXECUTABLE-COUNTERPART WRITEABLE-FILES-P) (:DEFINITION WRITEABLE-FILES-P) (:FORWARD-CHAINING WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (:INDUCTION WRITABLE-FILE-LISTP) (:TYPE-PRESCRIPTION WRITABLE-FILE-LISTP) (:EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP) (:DEFINITION WRITABLE-FILE-LISTP) (:FORWARD-CHAINING WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (:TYPE-PRESCRIPTION WRITABLE-FILE-LISTP1) (:EXECUTABLE-COUNTERPART WRITABLE-FILE-LISTP1) (:DEFINITION WRITABLE-FILE-LISTP1) (:FORWARD-CHAINING READ-FILES-P-FORWARD-TO-READ-FILE-LISTP) (:TYPE-PRESCRIPTION READ-FILES-P) (:EXECUTABLE-COUNTERPART READ-FILES-P) (:DEFINITION READ-FILES-P) (:FORWARD-CHAINING READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP) (:INDUCTION READ-FILE-LISTP) (:TYPE-PRESCRIPTION READ-FILE-LISTP) (:EXECUTABLE-COUNTERPART READ-FILE-LISTP) (:DEFINITION READ-FILE-LISTP) (:FORWARD-CHAINING READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (:TYPE-PRESCRIPTION READ-FILE-LISTP1) (:EXECUTABLE-COUNTERPART READ-FILE-LISTP1) (:DEFINITION READ-FILE-LISTP1) (:FORWARD-CHAINING WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP) (:TYPE-PRESCRIPTION WRITTEN-FILES-P) (:EXECUTABLE-COUNTERPART WRITTEN-FILES-P) (:DEFINITION WRITTEN-FILES-P) (:FORWARD-CHAINING WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (:INDUCTION WRITTEN-FILE-LISTP) (:TYPE-PRESCRIPTION WRITTEN-FILE-LISTP) (:EXECUTABLE-COUNTERPART WRITTEN-FILE-LISTP) (:DEFINITION WRITTEN-FILE-LISTP) (:FORWARD-CHAINING WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (:TYPE-PRESCRIPTION WRITTEN-FILE) (:EXECUTABLE-COUNTERPART WRITTEN-FILE) (:DEFINITION WRITTEN-FILE) (:FORWARD-CHAINING READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP) (:TYPE-PRESCRIPTION READABLE-FILES-P) (:EXECUTABLE-COUNTERPART READABLE-FILES-P) (:DEFINITION READABLE-FILES-P) (:FORWARD-CHAINING READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (:INDUCTION READABLE-FILES-LISTP) (:TYPE-PRESCRIPTION READABLE-FILES-LISTP) (:EXECUTABLE-COUNTERPART READABLE-FILES-LISTP) (:DEFINITION READABLE-FILES-LISTP) (:FORWARD-CHAINING READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP) (:TYPE-PRESCRIPTION READABLE-FILE) (:EXECUTABLE-COUNTERPART READABLE-FILE) (:DEFINITION READABLE-FILE) (:FORWARD-CHAINING FILE-CLOCK-P-FORWARD-TO-INTEGERP) (:TYPE-PRESCRIPTION FILE-CLOCK-P) (:EXECUTABLE-COUNTERPART FILE-CLOCK-P) (:DEFINITION FILE-CLOCK-P) (:FORWARD-CHAINING OPEN-CHANNELS-P-FORWARD) (:TYPE-PRESCRIPTION OPEN-CHANNELS-P) (:EXECUTABLE-COUNTERPART OPEN-CHANNELS-P) (:DEFINITION OPEN-CHANNELS-P) (:INDUCTION OPEN-CHANNEL-LISTP) (:TYPE-PRESCRIPTION OPEN-CHANNEL-LISTP) (:EXECUTABLE-COUNTERPART OPEN-CHANNEL-LISTP) (:DEFINITION OPEN-CHANNEL-LISTP) (:FORWARD-CHAINING OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP) (:TYPE-PRESCRIPTION OPEN-CHANNEL1) (:EXECUTABLE-COUNTERPART OPEN-CHANNEL1) (:DEFINITION OPEN-CHANNEL1) (:FORWARD-CHAINING TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP) (:INDUCTION TYPED-IO-LISTP) (:TYPE-PRESCRIPTION TYPED-IO-LISTP) (:EXECUTABLE-COUNTERPART TYPED-IO-LISTP) (:DEFINITION TYPED-IO-LISTP) (:FORWARD-CHAINING TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP) (:INDUCTION TIMER-ALISTP) (:TYPE-PRESCRIPTION TIMER-ALISTP) (:EXECUTABLE-COUNTERPART TIMER-ALISTP) (:DEFINITION TIMER-ALISTP) (:FORWARD-CHAINING KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP) (:INDUCTION KNOWN-PACKAGE-ALISTP) (:TYPE-PRESCRIPTION KNOWN-PACKAGE-ALISTP) (:EXECUTABLE-COUNTERPART KNOWN-PACKAGE-ALISTP) (:DEFINITION KNOWN-PACKAGE-ALISTP) (:INDUCTION ALL-BOUNDP) (:TYPE-PRESCRIPTION ALL-BOUNDP) (:EXECUTABLE-COUNTERPART ALL-BOUNDP) (:DEFINITION ALL-BOUNDP) (:TYPE-PRESCRIPTION INIT-IPRINT-AR) (:EXECUTABLE-COUNTERPART INIT-IPRINT-AR) (:DEFINITION INIT-IPRINT-AR) (:TYPE-PRESCRIPTION UPDATE-USER-STOBJ-ALIST1) (:EXECUTABLE-COUNTERPART UPDATE-USER-STOBJ-ALIST1) (:DEFINITION UPDATE-USER-STOBJ-ALIST1) (:TYPE-PRESCRIPTION USER-STOBJ-ALIST1) (:EXECUTABLE-COUNTERPART USER-STOBJ-ALIST1) (:DEFINITION USER-STOBJ-ALIST1) (:TYPE-PRESCRIPTION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (:EXECUTABLE-COUNTERPART UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (:DEFINITION UPDATE-LIST-ALL-PACKAGE-NAMES-LST) (:TYPE-PRESCRIPTION LIST-ALL-PACKAGE-NAMES-LST) (:EXECUTABLE-COUNTERPART LIST-ALL-PACKAGE-NAMES-LST) (:DEFINITION LIST-ALL-PACKAGE-NAMES-LST) (:TYPE-PRESCRIPTION WRITEABLE-FILES) (:EXECUTABLE-COUNTERPART WRITEABLE-FILES) (:DEFINITION WRITEABLE-FILES) (:TYPE-PRESCRIPTION UPDATE-READ-FILES) (:EXECUTABLE-COUNTERPART UPDATE-READ-FILES) (:DEFINITION UPDATE-READ-FILES) (:TYPE-PRESCRIPTION READ-FILES) (:EXECUTABLE-COUNTERPART READ-FILES) (:DEFINITION READ-FILES) (:TYPE-PRESCRIPTION UPDATE-WRITTEN-FILES) (:EXECUTABLE-COUNTERPART UPDATE-WRITTEN-FILES) (:DEFINITION UPDATE-WRITTEN-FILES) (:TYPE-PRESCRIPTION WRITTEN-FILES) (:EXECUTABLE-COUNTERPART WRITTEN-FILES) (:DEFINITION WRITTEN-FILES) (:TYPE-PRESCRIPTION READABLE-FILES) (:EXECUTABLE-COUNTERPART READABLE-FILES) (:DEFINITION READABLE-FILES) (:TYPE-PRESCRIPTION UPDATE-FILE-CLOCK) (:EXECUTABLE-COUNTERPART UPDATE-FILE-CLOCK) (:DEFINITION UPDATE-FILE-CLOCK) (:TYPE-PRESCRIPTION FILE-CLOCK) (:EXECUTABLE-COUNTERPART FILE-CLOCK) (:DEFINITION FILE-CLOCK) (:TYPE-PRESCRIPTION UPDATE-ACL2-ORACLE) (:EXECUTABLE-COUNTERPART UPDATE-ACL2-ORACLE) (:TYPE-PRESCRIPTION ACL2-ORACLE) (:EXECUTABLE-COUNTERPART ACL2-ORACLE) (:DEFINITION ACL2-ORACLE) (:TYPE-PRESCRIPTION UPDATE-IDATES) (:EXECUTABLE-COUNTERPART UPDATE-IDATES) (:DEFINITION UPDATE-IDATES) (:TYPE-PRESCRIPTION IDATES) (:EXECUTABLE-COUNTERPART IDATES) (:DEFINITION IDATES) (:TYPE-PRESCRIPTION UPDATE-BIG-CLOCK-ENTRY) (:EXECUTABLE-COUNTERPART UPDATE-BIG-CLOCK-ENTRY) (:DEFINITION UPDATE-BIG-CLOCK-ENTRY) (:TYPE-PRESCRIPTION BIG-CLOCK-ENTRY) (:EXECUTABLE-COUNTERPART BIG-CLOCK-ENTRY) (:DEFINITION BIG-CLOCK-ENTRY) (:TYPE-PRESCRIPTION UPDATE-32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART UPDATE-32-BIT-INTEGER-STACK) (:DEFINITION UPDATE-32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION 32-BIT-INTEGER-STACK) (:EXECUTABLE-COUNTERPART 32-BIT-INTEGER-STACK) (:DEFINITION 32-BIT-INTEGER-STACK) (:TYPE-PRESCRIPTION UPDATE-T-STACK) (:EXECUTABLE-COUNTERPART UPDATE-T-STACK) (:DEFINITION UPDATE-T-STACK) (:TYPE-PRESCRIPTION T-STACK) (:EXECUTABLE-COUNTERPART T-STACK) (:DEFINITION T-STACK) (:TYPE-PRESCRIPTION UPDATE-GLOBAL-TABLE) (:EXECUTABLE-COUNTERPART UPDATE-GLOBAL-TABLE) (:DEFINITION UPDATE-GLOBAL-TABLE) (:TYPE-PRESCRIPTION GLOBAL-TABLE) (:EXECUTABLE-COUNTERPART GLOBAL-TABLE) (:DEFINITION GLOBAL-TABLE) (:TYPE-PRESCRIPTION UPDATE-OPEN-OUTPUT-CHANNELS) (:EXECUTABLE-COUNTERPART UPDATE-OPEN-OUTPUT-CHANNELS) (:DEFINITION UPDATE-OPEN-OUTPUT-CHANNELS) (:TYPE-PRESCRIPTION OPEN-OUTPUT-CHANNELS) (:EXECUTABLE-COUNTERPART OPEN-OUTPUT-CHANNELS) (:DEFINITION OPEN-OUTPUT-CHANNELS) (:TYPE-PRESCRIPTION UPDATE-OPEN-INPUT-CHANNELS) (:EXECUTABLE-COUNTERPART UPDATE-OPEN-INPUT-CHANNELS) (:DEFINITION UPDATE-OPEN-INPUT-CHANNELS) (:TYPE-PRESCRIPTION OPEN-INPUT-CHANNELS) (:EXECUTABLE-COUNTERPART OPEN-INPUT-CHANNELS) (:DEFINITION OPEN-INPUT-CHANNELS) (:FORWARD-CHAINING 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP) (:INDUCTION 32-BIT-INTEGER-LISTP) (:TYPE-PRESCRIPTION 32-BIT-INTEGER-LISTP) (:EXECUTABLE-COUNTERPART 32-BIT-INTEGER-LISTP) (:DEFINITION 32-BIT-INTEGER-LISTP) (:FORWARD-CHAINING INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP) (:INDUCTION INTEGER-LISTP) (:TYPE-PRESCRIPTION INTEGER-LISTP) (:EXECUTABLE-COUNTERPART INTEGER-LISTP) (:DEFINITION INTEGER-LISTP) (:FORWARD-CHAINING RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP) (:INDUCTION RATIONAL-LISTP) (:TYPE-PRESCRIPTION RATIONAL-LISTP) (:EXECUTABLE-COUNTERPART RATIONAL-LISTP) (:DEFINITION RATIONAL-LISTP) (:FORWARD-CHAINING 32-BIT-INTEGERP-FORWARD-TO-INTEGERP) (:TYPE-PRESCRIPTION 32-BIT-INTEGERP) (:EXECUTABLE-COUNTERPART 32-BIT-INTEGERP) (:DEFINITION 32-BIT-INTEGERP) (:TYPE-PRESCRIPTION UPDATE-NTH-ARRAY) (:EXECUTABLE-COUNTERPART UPDATE-NTH-ARRAY) (:DEFINITION UPDATE-NTH-ARRAY) (:INDUCTION UPDATE-NTH) (:TYPE-PRESCRIPTION UPDATE-NTH) (:EXECUTABLE-COUNTERPART UPDATE-NTH) (:DEFINITION UPDATE-NTH) (:INDUCTION MAKE-MV-NTHS) (:TYPE-PRESCRIPTION MAKE-MV-NTHS) (:EXECUTABLE-COUNTERPART MAKE-MV-NTHS) (:DEFINITION MAKE-MV-NTHS) (:INDUCTION MV-NTH) (:TYPE-PRESCRIPTION MV-NTH) (:EXECUTABLE-COUNTERPART MV-NTH) (:DEFINITION MV-NTH) (:INDUCTION CDRN) (:TYPE-PRESCRIPTION CDRN) (:EXECUTABLE-COUNTERPART CDRN) (:DEFINITION CDRN) (:TYPE-PRESCRIPTION FLUSH-COMPRESS) (:EXECUTABLE-COUNTERPART FLUSH-COMPRESS) (:DEFINITION FLUSH-COMPRESS) (:TYPE-PRESCRIPTION ASET2) (:EXECUTABLE-COUNTERPART ASET2) (:DEFINITION ASET2) (:REWRITE ARRAY2P-CONS) (:TYPE-PRESCRIPTION COMPRESS2) (:EXECUTABLE-COUNTERPART COMPRESS2) (:DEFINITION COMPRESS2) (:INDUCTION COMPRESS21) (:TYPE-PRESCRIPTION COMPRESS21) (:EXECUTABLE-COUNTERPART COMPRESS21) (:DEFINITION COMPRESS21) (:INDUCTION COMPRESS211) (:TYPE-PRESCRIPTION COMPRESS211) (:EXECUTABLE-COUNTERPART COMPRESS211) (:DEFINITION COMPRESS211) (:TYPE-PRESCRIPTION AREF2) (:EXECUTABLE-COUNTERPART AREF2) (:DEFINITION AREF2) (:TYPE-PRESCRIPTION ASET1) (:EXECUTABLE-COUNTERPART ASET1) (:DEFINITION ASET1) (:REWRITE ARRAY1P-CONS) (:TYPE-PRESCRIPTION COMPRESS1) (:EXECUTABLE-COUNTERPART COMPRESS1) (:DEFINITION COMPRESS1) (:TYPE-PRESCRIPTION ARRAY-ORDER) (:EXECUTABLE-COUNTERPART ARRAY-ORDER) (:DEFINITION ARRAY-ORDER) (:INDUCTION COMPRESS11) (:TYPE-PRESCRIPTION COMPRESS11) (:EXECUTABLE-COUNTERPART COMPRESS11) (:DEFINITION COMPRESS11) (:TYPE-PRESCRIPTION AREF1) (:EXECUTABLE-COUNTERPART AREF1) (:DEFINITION AREF1) (:TYPE-PRESCRIPTION CONSP-ASSOC) (:TYPE-PRESCRIPTION DEFAULT) (:EXECUTABLE-COUNTERPART DEFAULT) (:DEFINITION DEFAULT) (:TYPE-PRESCRIPTION MAXIMUM-LENGTH) (:EXECUTABLE-COUNTERPART MAXIMUM-LENGTH) (:DEFINITION MAXIMUM-LENGTH) (:TYPE-PRESCRIPTION DIMENSIONS) (:EXECUTABLE-COUNTERPART DIMENSIONS) (:DEFINITION DIMENSIONS) (:TYPE-PRESCRIPTION HEADER) (:EXECUTABLE-COUNTERPART HEADER) (:DEFINITION HEADER) (:LINEAR ARRAY2P-LINEAR) (:FORWARD-CHAINING ARRAY2P-FORWARD) (:TYPE-PRESCRIPTION ARRAY2P) (:EXECUTABLE-COUNTERPART ARRAY2P) (:DEFINITION ARRAY2P) (:INDUCTION ASSOC2) (:TYPE-PRESCRIPTION ASSOC2) (:EXECUTABLE-COUNTERPART ASSOC2) (:DEFINITION ASSOC2) (:INDUCTION BOUNDED-INTEGER-ALISTP2) (:TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP2) (:EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP2) (:DEFINITION BOUNDED-INTEGER-ALISTP2) (:LINEAR ARRAY1P-LINEAR) (:FORWARD-CHAINING ARRAY1P-FORWARD) (:TYPE-PRESCRIPTION ARRAY1P) (:EXECUTABLE-COUNTERPART ARRAY1P) (:DEFINITION ARRAY1P) (:TYPE-PRESCRIPTION CONSP-ASSOC-EQ) (:FORWARD-CHAINING KEYWORD-VALUE-LISTP-ASSOC-KEYWORD) (:INDUCTION ASSOC-KEYWORD) (:TYPE-PRESCRIPTION ASSOC-KEYWORD) (:EXECUTABLE-COUNTERPART ASSOC-KEYWORD) (:DEFINITION ASSOC-KEYWORD) (:FORWARD-CHAINING KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP) (:INDUCTION KEYWORD-VALUE-LISTP) (:TYPE-PRESCRIPTION KEYWORD-VALUE-LISTP) (:EXECUTABLE-COUNTERPART KEYWORD-VALUE-LISTP) (:DEFINITION KEYWORD-VALUE-LISTP) (:FORWARD-CHAINING BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP) (:INDUCTION BOUNDED-INTEGER-ALISTP) (:TYPE-PRESCRIPTION BOUNDED-INTEGER-ALISTP) (:EXECUTABLE-COUNTERPART BOUNDED-INTEGER-ALISTP) (:DEFINITION BOUNDED-INTEGER-ALISTP) (:INDUCTION SET-DIFFERENCE-EQUAL) (:TYPE-PRESCRIPTION SET-DIFFERENCE-EQUAL) (:EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQUAL) (:DEFINITION SET-DIFFERENCE-EQUAL) (:TYPE-PRESCRIPTION THE-ERROR) (:EXECUTABLE-COUNTERPART THE-ERROR) (:DEFINITION THE-ERROR) (:TYPE-PRESCRIPTION WEAK-SATISFIES-TYPE-SPEC-P) (:EXECUTABLE-COUNTERPART WEAK-SATISFIES-TYPE-SPEC-P) (:DEFINITION WEAK-SATISFIES-TYPE-SPEC-P) (:TYPE-PRESCRIPTION FUNCTION-SYMBOLP) (:EXECUTABLE-COUNTERPART FUNCTION-SYMBOLP) (:DEFINITION FUNCTION-SYMBOLP) (:TYPE-PRESCRIPTION GLOBAL-VAL) (:EXECUTABLE-COUNTERPART GLOBAL-VAL) (:DEFINITION GLOBAL-VAL) (:TYPE-PRESCRIPTION RETRACT-WORLD) (:EXECUTABLE-COUNTERPART RETRACT-WORLD) (:DEFINITION RETRACT-WORLD) (:TYPE-PRESCRIPTION EXTEND-WORLD) (:EXECUTABLE-COUNTERPART EXTEND-WORLD) (:DEFINITION EXTEND-WORLD) (:INDUCTION HAS-PROPSP) (:TYPE-PRESCRIPTION HAS-PROPSP) (:EXECUTABLE-COUNTERPART HAS-PROPSP) (:DEFINITION HAS-PROPSP) (:INDUCTION HAS-PROPSP1) (:TYPE-PRESCRIPTION HAS-PROPSP1) (:EXECUTABLE-COUNTERPART HAS-PROPSP1) (:DEFINITION HAS-PROPSP1) (:INDUCTION GETPROPS) (:TYPE-PRESCRIPTION GETPROPS) (:EXECUTABLE-COUNTERPART GETPROPS) (:DEFINITION GETPROPS) (:INDUCTION GETPROPS1) (:TYPE-PRESCRIPTION GETPROPS1) (:EXECUTABLE-COUNTERPART GETPROPS1) (:DEFINITION GETPROPS1) (:INDUCTION REMOVE-FIRST-PAIR) (:TYPE-PRESCRIPTION REMOVE-FIRST-PAIR) (:EXECUTABLE-COUNTERPART REMOVE-FIRST-PAIR) (:DEFINITION REMOVE-FIRST-PAIR) (:INDUCTION ADD-PAIR) (:TYPE-PRESCRIPTION ADD-PAIR) (:EXECUTABLE-COUNTERPART ADD-PAIR) (:DEFINITION ADD-PAIR) (:FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP) (:INDUCTION ORDERED-SYMBOL-ALISTP) (:TYPE-PRESCRIPTION ORDERED-SYMBOL-ALISTP) (:EXECUTABLE-COUNTERPART ORDERED-SYMBOL-ALISTP) (:DEFINITION ORDERED-SYMBOL-ALISTP) (:INDUCTION SGETPROP) (:TYPE-PRESCRIPTION SGETPROP) (:EXECUTABLE-COUNTERPART SGETPROP) (:DEFINITION SGETPROP) (:INDUCTION FGETPROP) (:TYPE-PRESCRIPTION FGETPROP) (:EXECUTABLE-COUNTERPART FGETPROP) (:DEFINITION FGETPROP) (:TYPE-PRESCRIPTION GETPROP-DEFAULT) (:EXECUTABLE-COUNTERPART GETPROP-DEFAULT) (:DEFINITION GETPROP-DEFAULT) (:TYPE-PRESCRIPTION PUTPROP) (:EXECUTABLE-COUNTERPART PUTPROP) (:DEFINITION PUTPROP) (:FORWARD-CHAINING WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP) (:INDUCTION WORLDP) (:TYPE-PRESCRIPTION WORLDP) (:EXECUTABLE-COUNTERPART WORLDP) (:DEFINITION WORLDP) (:INDUCTION SUBST) (:TYPE-PRESCRIPTION SUBST) (:EXECUTABLE-COUNTERPART SUBST) (:DEFINITION SUBST) (:INDUCTION SUBSETP) (:TYPE-PRESCRIPTION SUBSETP) (:EXECUTABLE-COUNTERPART SUBSETP) (:DEFINITION SUBSETP) (:TYPE-PRESCRIPTION SUBSTITUTE) (:EXECUTABLE-COUNTERPART SUBSTITUTE) (:DEFINITION SUBSTITUTE) (:INDUCTION SUBSTITUTE-AC) (:TYPE-PRESCRIPTION SUBSTITUTE-AC) (:EXECUTABLE-COUNTERPART SUBSTITUTE-AC) (:DEFINITION SUBSTITUTE-AC) (:REWRITE STRING<-IRREFLEXIVE) (:REWRITE STRING<-L-IRREFLEXIVE) (:TYPE-PRESCRIPTION SYMBOL-<) (:EXECUTABLE-COUNTERPART SYMBOL-<) (:TYPE-PRESCRIPTION STRING>=) (:EXECUTABLE-COUNTERPART STRING>=) (:DEFINITION STRING>=) (:TYPE-PRESCRIPTION STRING<=) (:EXECUTABLE-COUNTERPART STRING<=) (:DEFINITION STRING<=) (:TYPE-PRESCRIPTION STRING>) (:EXECUTABLE-COUNTERPART STRING>) (:DEFINITION STRING>) (:TYPE-PRESCRIPTION STRING<) (:EXECUTABLE-COUNTERPART STRING<) (:TYPE-PRESCRIPTION STRING<-L) (:EXECUTABLE-COUNTERPART STRING<-L) (:TYPE-PRESCRIPTION CHAR>=) (:EXECUTABLE-COUNTERPART CHAR>=) (:DEFINITION CHAR>=) (:TYPE-PRESCRIPTION CHAR<=) (:EXECUTABLE-COUNTERPART CHAR<=) (:DEFINITION CHAR<=) (:TYPE-PRESCRIPTION CHAR>) (:EXECUTABLE-COUNTERPART CHAR>) (:DEFINITION CHAR>) (:TYPE-PRESCRIPTION CHAR<) (:EXECUTABLE-COUNTERPART CHAR<) (:DEFINITION CHAR<) (:REWRITE CHAR-CODE-CODE-CHAR-IS-IDENTITY) (:REWRITE CODE-CHAR-CHAR-CODE-IS-IDENTITY) (:TYPE-PRESCRIPTION CODE-CHAR-TYPE) (:LINEAR CHAR-CODE-LINEAR) (:TYPE-PRESCRIPTION ASH) (:EXECUTABLE-COUNTERPART ASH) (:DEFINITION ASH) (:TYPE-PRESCRIPTION LOGBITP) (:EXECUTABLE-COUNTERPART LOGBITP) (:DEFINITION LOGBITP) (:TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION) (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE) (:INDUCTION NTHCDR) (:TYPE-PRESCRIPTION NTHCDR) (:EXECUTABLE-COUNTERPART NTHCDR) (:DEFINITION NTHCDR) (:INDUCTION LOGCOUNT) (:TYPE-PRESCRIPTION LOGCOUNT) (:EXECUTABLE-COUNTERPART LOGCOUNT) (:DEFINITION LOGCOUNT) (:INDUCTION EXPT) (:TYPE-PRESCRIPTION EXPT) (:EXECUTABLE-COUNTERPART EXPT) (:DEFINITION EXPT) (:INDUCTION XXXJOIN) (:TYPE-PRESCRIPTION XXXJOIN) (:EXECUTABLE-COUNTERPART XXXJOIN) (:DEFINITION XXXJOIN) (:INDUCTION ASSOC-STRING-EQUAL) (:TYPE-PRESCRIPTION ASSOC-STRING-EQUAL) (:EXECUTABLE-COUNTERPART ASSOC-STRING-EQUAL) (:DEFINITION ASSOC-STRING-EQUAL) (:TYPE-PRESCRIPTION STRING-EQUAL) (:EXECUTABLE-COUNTERPART STRING-EQUAL) (:DEFINITION STRING-EQUAL) (:INDUCTION STRING-EQUAL1) (:TYPE-PRESCRIPTION STRING-EQUAL1) (:EXECUTABLE-COUNTERPART STRING-EQUAL1) (:DEFINITION STRING-EQUAL1) (:REWRITE STANDARD-CHAR-P-NTH) (:TYPE-PRESCRIPTION LOGNOT) (:EXECUTABLE-COUNTERPART LOGNOT) (:DEFINITION LOGNOT) (:TYPE-PRESCRIPTION SIGNUM) (:EXECUTABLE-COUNTERPART SIGNUM) (:DEFINITION SIGNUM) (:TYPE-PRESCRIPTION ABS) (:EXECUTABLE-COUNTERPART ABS) (:DEFINITION ABS) (:TYPE-PRESCRIPTION MAX) (:EXECUTABLE-COUNTERPART MAX) (:DEFINITION MAX) (:TYPE-PRESCRIPTION MIN) (:EXECUTABLE-COUNTERPART MIN) (:DEFINITION MIN) (:TYPE-PRESCRIPTION ODDP) (:EXECUTABLE-COUNTERPART ODDP) (:DEFINITION ODDP) (:TYPE-PRESCRIPTION EVENP) (:EXECUTABLE-COUNTERPART EVENP) (:DEFINITION EVENP) (:TYPE-PRESCRIPTION REM) (:EXECUTABLE-COUNTERPART REM) (:DEFINITION REM) (:TYPE-PRESCRIPTION MOD) (:EXECUTABLE-COUNTERPART MOD) (:DEFINITION MOD) (:TYPE-PRESCRIPTION ROUND) (:EXECUTABLE-COUNTERPART ROUND) (:DEFINITION ROUND) (:TYPE-PRESCRIPTION TRUNCATE) (:EXECUTABLE-COUNTERPART TRUNCATE) (:DEFINITION TRUNCATE) (:TYPE-PRESCRIPTION CEILING) (:EXECUTABLE-COUNTERPART CEILING) (:DEFINITION CEILING) (:INDUCTION RESTRICT-ALIST) (:TYPE-PRESCRIPTION RESTRICT-ALIST) (:EXECUTABLE-COUNTERPART RESTRICT-ALIST) (:DEFINITION RESTRICT-ALIST) (:INDUCTION APPEND-LST) (:TYPE-PRESCRIPTION APPEND-LST) (:EXECUTABLE-COUNTERPART APPEND-LST) (:DEFINITION APPEND-LST) (:INDUCTION COLLECT-CDRS-WHEN-CAR-EQ) (:TYPE-PRESCRIPTION COLLECT-CDRS-WHEN-CAR-EQ) (:EXECUTABLE-COUNTERPART COLLECT-CDRS-WHEN-CAR-EQ) (:DEFINITION COLLECT-CDRS-WHEN-CAR-EQ) (:INDUCTION LET*-MACRO) (:TYPE-PRESCRIPTION LET*-MACRO) (:EXECUTABLE-COUNTERPART LET*-MACRO) (:DEFINITION LET*-MACRO) (:INDUCTION GET-TYPE-DECLS) (:TYPE-PRESCRIPTION GET-TYPE-DECLS) (:EXECUTABLE-COUNTERPART GET-TYPE-DECLS) (:DEFINITION GET-TYPE-DECLS) (:INDUCTION SYMBOL-LIST-LISTP) (:TYPE-PRESCRIPTION SYMBOL-LIST-LISTP) (:EXECUTABLE-COUNTERPART SYMBOL-LIST-LISTP) (:DEFINITION SYMBOL-LIST-LISTP) (:INDUCTION WELL-FORMED-TYPE-DECLS-P) (:TYPE-PRESCRIPTION WELL-FORMED-TYPE-DECLS-P) (:EXECUTABLE-COUNTERPART WELL-FORMED-TYPE-DECLS-P) (:DEFINITION WELL-FORMED-TYPE-DECLS-P) (:INDUCTION LEGAL-LET*-P) (:TYPE-PRESCRIPTION LEGAL-LET*-P) (:EXECUTABLE-COUNTERPART LEGAL-LET*-P) (:DEFINITION LEGAL-LET*-P) (:FORWARD-CHAINING TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP) (:INDUCTION TRUE-LIST-LISTP) (:TYPE-PRESCRIPTION TRUE-LIST-LISTP) (:EXECUTABLE-COUNTERPART TRUE-LIST-LISTP) (:DEFINITION TRUE-LIST-LISTP) (:TYPE-PRESCRIPTION POSITION) (:EXECUTABLE-COUNTERPART POSITION) (:DEFINITION POSITION) (:TYPE-PRESCRIPTION POSITION-EQ) (:EXECUTABLE-COUNTERPART POSITION-EQ) (:DEFINITION POSITION-EQ) (:INDUCTION POSITION-EQ-AC) (:TYPE-PRESCRIPTION POSITION-EQ-AC) (:EXECUTABLE-COUNTERPART POSITION-EQ-AC) (:DEFINITION POSITION-EQ-AC) (:TYPE-PRESCRIPTION POSITION-EQUAL) (:EXECUTABLE-COUNTERPART POSITION-EQUAL) (:DEFINITION POSITION-EQUAL) (:INDUCTION POSITION-AC) (:TYPE-PRESCRIPTION POSITION-AC) (:EXECUTABLE-COUNTERPART POSITION-AC) (:DEFINITION POSITION-AC) (:INDUCTION POSITION-EQUAL-AC) (:TYPE-PRESCRIPTION POSITION-EQUAL-AC) (:EXECUTABLE-COUNTERPART POSITION-EQUAL-AC) (:DEFINITION POSITION-EQUAL-AC) (:INDUCTION CASE-LIST-CHECK) (:TYPE-PRESCRIPTION CASE-LIST-CHECK) (:EXECUTABLE-COUNTERPART CASE-LIST-CHECK) (:DEFINITION CASE-LIST-CHECK) (:INDUCTION CASE-LIST) (:TYPE-PRESCRIPTION CASE-LIST) (:EXECUTABLE-COUNTERPART CASE-LIST) (:DEFINITION CASE-LIST) (:TYPE-PRESCRIPTION CASE-TEST) (:EXECUTABLE-COUNTERPART CASE-TEST) (:DEFINITION CASE-TEST) (:INDUCTION LEGAL-CASE-CLAUSESP) (:TYPE-PRESCRIPTION LEGAL-CASE-CLAUSESP) (:EXECUTABLE-COUNTERPART LEGAL-CASE-CLAUSESP) (:DEFINITION LEGAL-CASE-CLAUSESP) (:INDUCTION ER-PROGN-FN) (:TYPE-PRESCRIPTION ER-PROGN-FN) (:EXECUTABLE-COUNTERPART ER-PROGN-FN) (:DEFINITION ER-PROGN-FN) (:INDUCTION MAKE-FMT-BINDINGS) (:TYPE-PRESCRIPTION MAKE-FMT-BINDINGS) (:EXECUTABLE-COUNTERPART MAKE-FMT-BINDINGS) (:DEFINITION MAKE-FMT-BINDINGS) (:INDUCTION INTERSECTP-EQUAL) (:TYPE-PRESCRIPTION INTERSECTP-EQUAL) (:EXECUTABLE-COUNTERPART INTERSECTP-EQUAL) (:DEFINITION INTERSECTP-EQUAL) (:INDUCTION INTERSECTP) (:TYPE-PRESCRIPTION INTERSECTP) (:EXECUTABLE-COUNTERPART INTERSECTP) (:DEFINITION INTERSECTP) (:INDUCTION INTERSECTP-EQ) (:TYPE-PRESCRIPTION INTERSECTP-EQ) (:EXECUTABLE-COUNTERPART INTERSECTP-EQ) (:DEFINITION INTERSECTP-EQ) (:TYPE-PRESCRIPTION ALL-VARS) (:EXECUTABLE-COUNTERPART ALL-VARS) (:DEFINITION ALL-VARS) (:INDUCTION ALL-VARS1-LST) (:TYPE-PRESCRIPTION ALL-VARS1-LST) (:EXECUTABLE-COUNTERPART ALL-VARS1-LST) (:DEFINITION ALL-VARS1-LST) (:INDUCTION ALL-VARS1) (:TYPE-PRESCRIPTION ALL-VARS1) (:EXECUTABLE-COUNTERPART ALL-VARS1) (:DEFINITION ALL-VARS1) (:TYPE-PRESCRIPTION FN-SYMB) (:EXECUTABLE-COUNTERPART FN-SYMB) (:DEFINITION FN-SYMB) (:INDUCTION KWOTE-LST) (:TYPE-PRESCRIPTION KWOTE-LST) (:EXECUTABLE-COUNTERPART KWOTE-LST) (:DEFINITION KWOTE-LST) (:TYPE-PRESCRIPTION KWOTE) (:EXECUTABLE-COUNTERPART KWOTE) (:DEFINITION KWOTE) (:TYPE-PRESCRIPTION QUOTEP) (:EXECUTABLE-COUNTERPART QUOTEP) (:DEFINITION QUOTEP) (:TYPE-PRESCRIPTION ADD-TO-SET-EQL) (:EXECUTABLE-COUNTERPART ADD-TO-SET-EQL) (:DEFINITION ADD-TO-SET-EQL) (:TYPE-PRESCRIPTION ADD-TO-SET-EQ) (:EXECUTABLE-COUNTERPART ADD-TO-SET-EQ) (:DEFINITION ADD-TO-SET-EQ) (:INDUCTION PSEUDO-TERM-LIST-LISTP) (:TYPE-PRESCRIPTION PSEUDO-TERM-LIST-LISTP) (:EXECUTABLE-COUNTERPART PSEUDO-TERM-LIST-LISTP) (:DEFINITION PSEUDO-TERM-LIST-LISTP) (:FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) (:INDUCTION PSEUDO-TERM-LISTP) (:TYPE-PRESCRIPTION PSEUDO-TERM-LISTP) (:EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP) (:DEFINITION PSEUDO-TERM-LISTP) (:INDUCTION PSEUDO-TERMP) (:TYPE-PRESCRIPTION PSEUDO-TERMP) (:EXECUTABLE-COUNTERPART PSEUDO-TERMP) (:DEFINITION PSEUDO-TERMP) (:INDUCTION DEFUND-NAME-LIST) (:TYPE-PRESCRIPTION DEFUND-NAME-LIST) (:EXECUTABLE-COUNTERPART DEFUND-NAME-LIST) (:DEFINITION DEFUND-NAME-LIST) (:TYPE-PRESCRIPTION XD-NAME) (:EXECUTABLE-COUNTERPART XD-NAME) (:DEFINITION XD-NAME) (:TYPE-PRESCRIPTION VALUE-TRIPLE-FN) (:EXECUTABLE-COUNTERPART VALUE-TRIPLE-FN) (:DEFINITION VALUE-TRIPLE-FN) (:INDUCTION COLLECT-CADRS-WHEN-CAR-EQ) (:TYPE-PRESCRIPTION COLLECT-CADRS-WHEN-CAR-EQ) (:EXECUTABLE-COUNTERPART COLLECT-CADRS-WHEN-CAR-EQ) (:DEFINITION COLLECT-CADRS-WHEN-CAR-EQ) (:INDUCTION MUTUAL-RECURSION-GUARDP) (:TYPE-PRESCRIPTION MUTUAL-RECURSION-GUARDP) (:EXECUTABLE-COUNTERPART MUTUAL-RECURSION-GUARDP) (:DEFINITION MUTUAL-RECURSION-GUARDP) (:INDUCTION STRIP-CDRS) (:TYPE-PRESCRIPTION STRIP-CDRS) (:EXECUTABLE-COUNTERPART STRIP-CDRS) (:DEFINITION STRIP-CDRS) (:TYPE-PRESCRIPTION BUTLAST) (:EXECUTABLE-COUNTERPART BUTLAST) (:DEFINITION BUTLAST) (:TYPE-PRESCRIPTION TAKE) (:EXECUTABLE-COUNTERPART TAKE) (:DEFINITION TAKE) (:INDUCTION FIRST-N-AC) (:TYPE-PRESCRIPTION FIRST-N-AC) (:EXECUTABLE-COUNTERPART FIRST-N-AC) (:DEFINITION FIRST-N-AC) (:INDUCTION LAST) (:TYPE-PRESCRIPTION LAST) (:EXECUTABLE-COUNTERPART LAST) (:DEFINITION LAST) (:INDUCTION SET-DIFFERENCE-EQ) (:TYPE-PRESCRIPTION SET-DIFFERENCE-EQ) (:EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQ) (:DEFINITION SET-DIFFERENCE-EQ) (:TYPE-PRESCRIPTION REVERSE) (:EXECUTABLE-COUNTERPART REVERSE) (:DEFINITION REVERSE) (:REWRITE CHARACTER-LISTP-REVAPPEND) (:INDUCTION REVAPPEND) (:TYPE-PRESCRIPTION REVAPPEND) (:EXECUTABLE-COUNTERPART REVAPPEND) (:DEFINITION REVAPPEND) (:TYPE-PRESCRIPTION IDENTITY) (:EXECUTABLE-COUNTERPART IDENTITY) (:DEFINITION IDENTITY) (:INDUCTION REMOVE-DUPLICATES-EQUAL) (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL) (:EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQUAL) (:DEFINITION REMOVE-DUPLICATES-EQUAL) (:TYPE-PRESCRIPTION REMOVE-DUPLICATES) (:EXECUTABLE-COUNTERPART REMOVE-DUPLICATES) (:DEFINITION REMOVE-DUPLICATES) (:REWRITE CHARACTER-LISTP-REMOVE-DUPLICATES-EQL) (:INDUCTION REMOVE-DUPLICATES-EQL) (:TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQL) (:EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQL) (:DEFINITION REMOVE-DUPLICATES-EQL) (:INDUCTION PAIRLIS$) (:TYPE-PRESCRIPTION PAIRLIS$) (:EXECUTABLE-COUNTERPART PAIRLIS$) (:DEFINITION PAIRLIS$) (:INDUCTION REMOVE1-EQUAL) (:TYPE-PRESCRIPTION REMOVE1-EQUAL) (:EXECUTABLE-COUNTERPART REMOVE1-EQUAL) (:DEFINITION REMOVE1-EQUAL) (:INDUCTION REMOVE1-EQ) (:TYPE-PRESCRIPTION REMOVE1-EQ) (:EXECUTABLE-COUNTERPART REMOVE1-EQ) (:DEFINITION REMOVE1-EQ) (:INDUCTION REMOVE1) (:TYPE-PRESCRIPTION REMOVE1) (:EXECUTABLE-COUNTERPART REMOVE1) (:DEFINITION REMOVE1) (:INDUCTION REMOVE-EQUAL) (:TYPE-PRESCRIPTION REMOVE-EQUAL) (:EXECUTABLE-COUNTERPART REMOVE-EQUAL) (:DEFINITION REMOVE-EQUAL) (:INDUCTION REMOVE-EQ) (:TYPE-PRESCRIPTION REMOVE-EQ) (:EXECUTABLE-COUNTERPART REMOVE-EQ) (:DEFINITION REMOVE-EQ) (:INDUCTION REMOVE) (:TYPE-PRESCRIPTION REMOVE) (:EXECUTABLE-COUNTERPART REMOVE) (:DEFINITION REMOVE) (:INDUCTION STRING-APPEND-LST) (:TYPE-PRESCRIPTION STRING-APPEND-LST) (:EXECUTABLE-COUNTERPART STRING-APPEND-LST) (:DEFINITION STRING-APPEND-LST) (:INDUCTION STRING-LISTP) (:TYPE-PRESCRIPTION STRING-LISTP) (:EXECUTABLE-COUNTERPART STRING-LISTP) (:DEFINITION STRING-LISTP) (:TYPE-PRESCRIPTION STRING-APPEND) (:EXECUTABLE-COUNTERPART STRING-APPEND) (:DEFINITION STRING-APPEND) (:REWRITE APPEND-TO-NIL) (:REWRITE CHARACTER-LISTP-APPEND) (:REWRITE STANDARD-CHAR-LISTP-APPEND) (:INDUCTION BINARY-APPEND) (:TYPE-PRESCRIPTION BINARY-APPEND) (:EXECUTABLE-COUNTERPART BINARY-APPEND) (:DEFINITION BINARY-APPEND) (:REWRITE KEYWORD-PACKAGE) (:REWRITE ACL2-PACKAGE) (:REWRITE ACL2-OUTPUT-CHANNEL-PACKAGE) (:REWRITE ACL2-INPUT-CHANNEL-PACKAGE) (:REWRITE SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL) (:INDUCTION MEMBER-SYMBOL-NAME) (:TYPE-PRESCRIPTION MEMBER-SYMBOL-NAME) (:EXECUTABLE-COUNTERPART MEMBER-SYMBOL-NAME) (:DEFINITION MEMBER-SYMBOL-NAME) (:REWRITE SYMBOL-PACKAGE-NAME-PKG-WITNESS-NAME) (:REWRITE SYMBOL-NAME-PKG-WITNESS) (:FORWARD-CHAINING SYMBOL-PACKAGE-NAME-OF-SYMBOL-IS-NOT-EMPTY-STRING) (:REWRITE INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME) (:FORWARD-CHAINING KEYWORDP-FORWARD-TO-SYMBOLP) (:TYPE-PRESCRIPTION KEYWORDP) (:EXECUTABLE-COUNTERPART KEYWORDP) (:DEFINITION KEYWORDP) (:TYPE-PRESCRIPTION ILLEGAL) (:EXECUTABLE-COUNTERPART ILLEGAL) (:DEFINITION ILLEGAL) (:TYPE-PRESCRIPTION HARD-ERROR) (:EXECUTABLE-COUNTERPART HARD-ERROR) (:DEFINITION HARD-ERROR) (:TYPE-PRESCRIPTION SYMBOLP-PKG-WITNESS) (:TYPE-PRESCRIPTION SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL) (:TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME) (:TYPE-PRESCRIPTION NULL-BODY-ER) (:EXECUTABLE-COUNTERPART NULL-BODY-ER) (:DEFINITION NULL-BODY-ER) (:INDUCTION LIST*-MACRO) (:TYPE-PRESCRIPTION LIST*-MACRO) (:EXECUTABLE-COUNTERPART LIST*-MACRO) (:DEFINITION LIST*-MACRO) (:TYPE-PRESCRIPTION MAKE-ORD) (:EXECUTABLE-COUNTERPART MAKE-ORD) (:DEFINITION MAKE-ORD) (:REWRITE O-P-IMPLIES-O=) (883 :EXECUTABLE-COUNTERPART STRING>=) (882 :DEFINITION STRING>=) (881 :TYPE-PRESCRIPTION STRING<=) (880 :EXECUTABLE-COUNTERPART STRING<=) (879 :DEFINITION STRING<=) (878 :TYPE-PRESCRIPTION STRING>) (877 :EXECUTABLE-COUNTERPART STRING>) (876 :DEFINITION STRING>) (875 :TYPE-PRESCRIPTION STRING<) (874 :EXECUTABLE-COUNTERPART STRING<) (871 :TYPE-PRESCRIPTION STRING<-L) (870 :EXECUTABLE-COUNTERPART STRING<-L) (868 :TYPE-PRESCRIPTION CHAR>=) (867 :EXECUTABLE-COUNTERPART CHAR>=) (866 :DEFINITION CHAR>=) (865 :TYPE-PRESCRIPTION CHAR<=) (864 :EXECUTABLE-COUNTERPART CHAR<=) (863 :DEFINITION CHAR<=) (862 :TYPE-PRESCRIPTION CHAR>) (861 :EXECUTABLE-COUNTERPART CHAR>) (860 :DEFINITION CHAR>) (859 :TYPE-PRESCRIPTION CHAR<) (858 :EXECUTABLE-COUNTERPART CHAR<) (857 :DEFINITION CHAR<) (856 :REWRITE CHAR-CODE-CODE-CHAR-IS-IDENTITY) (855 :REWRITE CODE-CHAR-CHAR-CODE-IS-IDENTITY) (854 :TYPE-PRESCRIPTION CODE-CHAR-TYPE) (853 :LINEAR CHAR-CODE-LINEAR) (852 :TYPE-PRESCRIPTION ASH) (851 :EXECUTABLE-COUNTERPART ASH) (850 :DEFINITION ASH) (849 :TYPE-PRESCRIPTION LOGBITP) (848 :EXECUTABLE-COUNTERPART LOGBITP) (847 :DEFINITION LOGBITP) (846 :TYPE-PRESCRIPTION RATIONALP-EXPT-TYPE-PRESCRIPTION) (845 :TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE) (844 :INDUCTION NTHCDR) (843 :TYPE-PRESCRIPTION NTHCDR) (842 :EXECUTABLE-COUNTERPART NTHCDR) (841 :DEFINITION NTHCDR) (840 :INDUCTION LOGCOUNT) (839 :TYPE-PRESCRIPTION LOGCOUNT) (838 :EXECUTABLE-COUNTERPART LOGCOUNT) (837 :DEFINITION LOGCOUNT) (836 :INDUCTION EXPT) (835 :TYPE-PRESCRIPTION EXPT) (834 :EXECUTABLE-COUNTERPART EXPT) (833 :DEFINITION EXPT) (832 :INDUCTION XXXJOIN) (831 :TYPE-PRESCRIPTION XXXJOIN) (830 :EXECUTABLE-COUNTERPART XXXJOIN) (829 :DEFINITION XXXJOIN) (828 :INDUCTION ASSOC-STRING-EQUAL) (827 :TYPE-PRESCRIPTION ASSOC-STRING-EQUAL) (826 :EXECUTABLE-COUNTERPART ASSOC-STRING-EQUAL) (825 :DEFINITION ASSOC-STRING-EQUAL) (824 :TYPE-PRESCRIPTION STRING-EQUAL) (823 :EXECUTABLE-COUNTERPART STRING-EQUAL) (822 :DEFINITION STRING-EQUAL) (821 :INDUCTION STRING-EQUAL1) (820 :TYPE-PRESCRIPTION STRING-EQUAL1) (819 :EXECUTABLE-COUNTERPART STRING-EQUAL1) (818 :DEFINITION STRING-EQUAL1) (817 :REWRITE STANDARD-CHAR-P-NTH) (816 :TYPE-PRESCRIPTION LOGNOT) (815 :EXECUTABLE-COUNTERPART LOGNOT) (814 :DEFINITION LOGNOT) (813 :TYPE-PRESCRIPTION SIGNUM) (812 :EXECUTABLE-COUNTERPART SIGNUM) (811 :DEFINITION SIGNUM) (810 :TYPE-PRESCRIPTION ABS) (809 :EXECUTABLE-COUNTERPART ABS) (808 :DEFINITION ABS) (807 :TYPE-PRESCRIPTION MAX) (806 :EXECUTABLE-COUNTERPART MAX) (805 :DEFINITION MAX) (804 :TYPE-PRESCRIPTION MIN) (803 :EXECUTABLE-COUNTERPART MIN) (802 :DEFINITION MIN) (801 :TYPE-PRESCRIPTION ODDP) (800 :EXECUTABLE-COUNTERPART ODDP) (799 :DEFINITION ODDP) (798 :TYPE-PRESCRIPTION EVENP) (797 :EXECUTABLE-COUNTERPART EVENP) (796 :DEFINITION EVENP) (795 :TYPE-PRESCRIPTION REM) (794 :EXECUTABLE-COUNTERPART REM) (793 :DEFINITION REM) (792 :TYPE-PRESCRIPTION MOD) (791 :EXECUTABLE-COUNTERPART MOD) (790 :DEFINITION MOD) (789 :TYPE-PRESCRIPTION ROUND) (788 :EXECUTABLE-COUNTERPART ROUND) (787 :DEFINITION ROUND) (786 :TYPE-PRESCRIPTION TRUNCATE) (785 :EXECUTABLE-COUNTERPART TRUNCATE) (784 :DEFINITION TRUNCATE) (783 :TYPE-PRESCRIPTION CEILING) (782 :EXECUTABLE-COUNTERPART CEILING) (781 :DEFINITION CEILING) (780 :INDUCTION RESTRICT-ALIST) (779 :TYPE-PRESCRIPTION RESTRICT-ALIST) (778 :EXECUTABLE-COUNTERPART RESTRICT-ALIST) (777 :DEFINITION RESTRICT-ALIST) (776 :INDUCTION APPEND-LST) (775 :TYPE-PRESCRIPTION APPEND-LST) (774 :EXECUTABLE-COUNTERPART APPEND-LST) (773 :DEFINITION APPEND-LST) (772 :INDUCTION COLLECT-CDRS-WHEN-CAR-EQ) (771 :TYPE-PRESCRIPTION COLLECT-CDRS-WHEN-CAR-EQ) (770 :EXECUTABLE-COUNTERPART COLLECT-CDRS-WHEN-CAR-EQ) (769 :DEFINITION COLLECT-CDRS-WHEN-CAR-EQ) (768 :INDUCTION LET*-MACRO) (767 :TYPE-PRESCRIPTION LET*-MACRO) (766 :EXECUTABLE-COUNTERPART LET*-MACRO) (765 :DEFINITION LET*-MACRO) (764 :INDUCTION GET-TYPE-DECLS) (763 :TYPE-PRESCRIPTION GET-TYPE-DECLS) (762 :EXECUTABLE-COUNTERPART GET-TYPE-DECLS) (761 :DEFINITION GET-TYPE-DECLS) (760 :INDUCTION SYMBOL-LIST-LISTP) (759 :TYPE-PRESCRIPTION SYMBOL-LIST-LISTP) (758 :EXECUTABLE-COUNTERPART SYMBOL-LIST-LISTP) (757 :DEFINITION SYMBOL-LIST-LISTP) (756 :INDUCTION WELL-FORMED-TYPE-DECLS-P) (755 :TYPE-PRESCRIPTION WELL-FORMED-TYPE-DECLS-P) (754 :EXECUTABLE-COUNTERPART WELL-FORMED-TYPE-DECLS-P) (753 :DEFINITION WELL-FORMED-TYPE-DECLS-P) (752 :INDUCTION LEGAL-LET*-P) (751 :TYPE-PRESCRIPTION LEGAL-LET*-P) (750 :EXECUTABLE-COUNTERPART LEGAL-LET*-P) (749 :DEFINITION LEGAL-LET*-P) (748 :FORWARD-CHAINING TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP) (747 :INDUCTION TRUE-LIST-LISTP) (746 :TYPE-PRESCRIPTION TRUE-LIST-LISTP) (745 :EXECUTABLE-COUNTERPART TRUE-LIST-LISTP) (744 :DEFINITION TRUE-LIST-LISTP) (743 :TYPE-PRESCRIPTION POSITION) (742 :EXECUTABLE-COUNTERPART POSITION) (741 :DEFINITION POSITION) (740 :TYPE-PRESCRIPTION POSITION-EQ) (739 :EXECUTABLE-COUNTERPART POSITION-EQ) (738 :DEFINITION POSITION-EQ) (737 :INDUCTION POSITION-EQ-AC) (736 :TYPE-PRESCRIPTION POSITION-EQ-AC) (735 :EXECUTABLE-COUNTERPART POSITION-EQ-AC) (734 :DEFINITION POSITION-EQ-AC) (733 :TYPE-PRESCRIPTION POSITION-EQUAL) (732 :EXECUTABLE-COUNTERPART POSITION-EQUAL) (731 :DEFINITION POSITION-EQUAL) (730 :INDUCTION POSITION-AC) (729 :TYPE-PRESCRIPTION POSITION-AC) (728 :EXECUTABLE-COUNTERPART POSITION-AC) (727 :DEFINITION POSITION-AC) (726 :INDUCTION POSITION-EQUAL-AC) (725 :TYPE-PRESCRIPTION POSITION-EQUAL-AC) (724 :EXECUTABLE-COUNTERPART POSITION-EQUAL-AC) (723 :DEFINITION POSITION-EQUAL-AC) (722 :INDUCTION CASE-LIST-CHECK) (721 :TYPE-PRESCRIPTION CASE-LIST-CHECK) (720 :EXECUTABLE-COUNTERPART CASE-LIST-CHECK) (719 :DEFINITION CASE-LIST-CHECK) (718 :INDUCTION CASE-LIST) (717 :TYPE-PRESCRIPTION CASE-LIST) (716 :EXECUTABLE-COUNTERPART CASE-LIST) (715 :DEFINITION CASE-LIST) (714 :TYPE-PRESCRIPTION CASE-TEST) (713 :EXECUTABLE-COUNTERPART CASE-TEST) (712 :DEFINITION CASE-TEST) (711 :INDUCTION LEGAL-CASE-CLAUSESP) (710 :TYPE-PRESCRIPTION LEGAL-CASE-CLAUSESP) (709 :EXECUTABLE-COUNTERPART LEGAL-CASE-CLAUSESP) (708 :DEFINITION LEGAL-CASE-CLAUSESP) (707 :INDUCTION ER-PROGN-FN) (706 :TYPE-PRESCRIPTION ER-PROGN-FN) (705 :EXECUTABLE-COUNTERPART ER-PROGN-FN) (704 :DEFINITION ER-PROGN-FN) (703 :INDUCTION MAKE-FMT-BINDINGS) (702 :TYPE-PRESCRIPTION MAKE-FMT-BINDINGS) (701 :EXECUTABLE-COUNTERPART MAKE-FMT-BINDINGS) (700 :DEFINITION MAKE-FMT-BINDINGS) (699 :INDUCTION INTERSECTP-EQUAL) (698 :TYPE-PRESCRIPTION INTERSECTP-EQUAL) (697 :EXECUTABLE-COUNTERPART INTERSECTP-EQUAL) (696 :DEFINITION INTERSECTP-EQUAL) (695 :INDUCTION INTERSECTP) (694 :TYPE-PRESCRIPTION INTERSECTP) (693 :EXECUTABLE-COUNTERPART INTERSECTP) (692 :DEFINITION INTERSECTP) (691 :INDUCTION INTERSECTP-EQ) (690 :TYPE-PRESCRIPTION INTERSECTP-EQ) (689 :EXECUTABLE-COUNTERPART INTERSECTP-EQ) (688 :DEFINITION INTERSECTP-EQ) (687 :TYPE-PRESCRIPTION ALL-VARS) (686 :EXECUTABLE-COUNTERPART ALL-VARS) (685 :DEFINITION ALL-VARS) (684 :INDUCTION ALL-VARS1-LST) (683 :TYPE-PRESCRIPTION ALL-VARS1-LST) (682 :EXECUTABLE-COUNTERPART ALL-VARS1-LST) (681 :DEFINITION ALL-VARS1-LST) (680 :INDUCTION ALL-VARS1) (679 :TYPE-PRESCRIPTION ALL-VARS1) (678 :EXECUTABLE-COUNTERPART ALL-VARS1) (677 :DEFINITION ALL-VARS1) (676 :TYPE-PRESCRIPTION FN-SYMB) (675 :EXECUTABLE-COUNTERPART FN-SYMB) (674 :DEFINITION FN-SYMB) (673 :INDUCTION KWOTE-LST) (672 :TYPE-PRESCRIPTION KWOTE-LST) (671 :EXECUTABLE-COUNTERPART KWOTE-LST) (670 :DEFINITION KWOTE-LST) (669 :TYPE-PRESCRIPTION KWOTE) (668 :EXECUTABLE-COUNTERPART KWOTE) (667 :DEFINITION KWOTE) (666 :TYPE-PRESCRIPTION QUOTEP) (665 :EXECUTABLE-COUNTERPART QUOTEP) (664 :DEFINITION QUOTEP) (663 :TYPE-PRESCRIPTION ADD-TO-SET-EQL) (662 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQL) (661 :DEFINITION ADD-TO-SET-EQL) (660 :TYPE-PRESCRIPTION ADD-TO-SET-EQ) (659 :EXECUTABLE-COUNTERPART ADD-TO-SET-EQ) (658 :DEFINITION ADD-TO-SET-EQ) (657 :INDUCTION PSEUDO-TERM-LIST-LISTP) (656 :TYPE-PRESCRIPTION PSEUDO-TERM-LIST-LISTP) (655 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LIST-LISTP) (654 :DEFINITION PSEUDO-TERM-LIST-LISTP) (653 :FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) (652 :INDUCTION PSEUDO-TERM-LISTP) (651 :TYPE-PRESCRIPTION PSEUDO-TERM-LISTP) (650 :EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP) (649 :DEFINITION PSEUDO-TERM-LISTP) (648 :INDUCTION PSEUDO-TERMP) (647 :TYPE-PRESCRIPTION PSEUDO-TERMP) (646 :EXECUTABLE-COUNTERPART PSEUDO-TERMP) (645 :DEFINITION PSEUDO-TERMP) (644 :INDUCTION DEFUND-NAME-LIST) (643 :TYPE-PRESCRIPTION DEFUND-NAME-LIST) (642 :EXECUTABLE-COUNTERPART DEFUND-NAME-LIST) (641 :DEFINITION DEFUND-NAME-LIST) (640 :TYPE-PRESCRIPTION XD-NAME) (639 :EXECUTABLE-COUNTERPART XD-NAME) (638 :DEFINITION XD-NAME) (637 :TYPE-PRESCRIPTION VALUE-TRIPLE-FN) (636 :EXECUTABLE-COUNTERPART VALUE-TRIPLE-FN) (635 :DEFINITION VALUE-TRIPLE-FN) (634 :INDUCTION COLLECT-CADRS-WHEN-CAR-EQ) (633 :TYPE-PRESCRIPTION COLLECT-CADRS-WHEN-CAR-EQ) (632 :EXECUTABLE-COUNTERPART COLLECT-CADRS-WHEN-CAR-EQ) (631 :DEFINITION COLLECT-CADRS-WHEN-CAR-EQ) (630 :INDUCTION MUTUAL-RECURSION-GUARDP) (629 :TYPE-PRESCRIPTION MUTUAL-RECURSION-GUARDP) (628 :EXECUTABLE-COUNTERPART MUTUAL-RECURSION-GUARDP) (627 :DEFINITION MUTUAL-RECURSION-GUARDP) (626 :INDUCTION STRIP-CDRS) (625 :TYPE-PRESCRIPTION STRIP-CDRS) (624 :EXECUTABLE-COUNTERPART STRIP-CDRS) (623 :DEFINITION STRIP-CDRS) (622 :TYPE-PRESCRIPTION BUTLAST) (621 :EXECUTABLE-COUNTERPART BUTLAST) (620 :DEFINITION BUTLAST) (619 :TYPE-PRESCRIPTION TAKE) (618 :EXECUTABLE-COUNTERPART TAKE) (617 :DEFINITION TAKE) (616 :INDUCTION FIRST-N-AC) (615 :TYPE-PRESCRIPTION FIRST-N-AC) (614 :EXECUTABLE-COUNTERPART FIRST-N-AC) (613 :DEFINITION FIRST-N-AC) (612 :INDUCTION LAST) (611 :TYPE-PRESCRIPTION LAST) (610 :EXECUTABLE-COUNTERPART LAST) (609 :DEFINITION LAST) (608 :INDUCTION SET-DIFFERENCE-EQ) (607 :TYPE-PRESCRIPTION SET-DIFFERENCE-EQ) (606 :EXECUTABLE-COUNTERPART SET-DIFFERENCE-EQ) (605 :DEFINITION SET-DIFFERENCE-EQ) (604 :TYPE-PRESCRIPTION REVERSE) (603 :EXECUTABLE-COUNTERPART REVERSE) (602 :DEFINITION REVERSE) (601 :REWRITE CHARACTER-LISTP-REVAPPEND) (600 :INDUCTION REVAPPEND) (599 :TYPE-PRESCRIPTION REVAPPEND) (598 :EXECUTABLE-COUNTERPART REVAPPEND) (597 :DEFINITION REVAPPEND) (596 :TYPE-PRESCRIPTION IDENTITY) (595 :EXECUTABLE-COUNTERPART IDENTITY) (594 :DEFINITION IDENTITY) (593 :INDUCTION REMOVE-DUPLICATES-EQUAL) (592 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQUAL) (591 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQUAL) (590 :DEFINITION REMOVE-DUPLICATES-EQUAL) (589 :TYPE-PRESCRIPTION REMOVE-DUPLICATES) (588 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES) (587 :DEFINITION REMOVE-DUPLICATES) (586 :REWRITE CHARACTER-LISTP-REMOVE-DUPLICATES-EQL) (585 :INDUCTION REMOVE-DUPLICATES-EQL) (584 :TYPE-PRESCRIPTION REMOVE-DUPLICATES-EQL) (583 :EXECUTABLE-COUNTERPART REMOVE-DUPLICATES-EQL) (582 :DEFINITION REMOVE-DUPLICATES-EQL) (581 :INDUCTION PAIRLIS$) (580 :TYPE-PRESCRIPTION PAIRLIS$) (579 :EXECUTABLE-COUNTERPART PAIRLIS$) (578 :DEFINITION PAIRLIS$) (577 :INDUCTION REMOVE1-EQUAL) (576 :TYPE-PRESCRIPTION REMOVE1-EQUAL) (575 :EXECUTABLE-COUNTERPART REMOVE1-EQUAL) (574 :DEFINITION REMOVE1-EQUAL) (573 :INDUCTION REMOVE1-EQ) (572 :TYPE-PRESCRIPTION REMOVE1-EQ) (571 :EXECUTABLE-COUNTERPART REMOVE1-EQ) (570 :DEFINITION REMOVE1-EQ) (569 :INDUCTION REMOVE1) (568 :TYPE-PRESCRIPTION REMOVE1) (567 :EXECUTABLE-COUNTERPART REMOVE1) (566 :DEFINITION REMOVE1) (565 :INDUCTION REMOVE-EQUAL) (564 :TYPE-PRESCRIPTION REMOVE-EQUAL) (563 :EXECUTABLE-COUNTERPART REMOVE-EQUAL) (562 :DEFINITION REMOVE-EQUAL) (561 :INDUCTION REMOVE-EQ) (560 :TYPE-PRESCRIPTION REMOVE-EQ) (559 :EXECUTABLE-COUNTERPART REMOVE-EQ) (558 :DEFINITION REMOVE-EQ) (557 :INDUCTION REMOVE) (556 :TYPE-PRESCRIPTION REMOVE) (555 :EXECUTABLE-COUNTERPART REMOVE) (554 :DEFINITION REMOVE) (553 :INDUCTION STRING-APPEND-LST) (552 :TYPE-PRESCRIPTION STRING-APPEND-LST) (551 :EXECUTABLE-COUNTERPART STRING-APPEND-LST) (550 :DEFINITION STRING-APPEND-LST) (549 :INDUCTION STRING-LISTP) (548 :TYPE-PRESCRIPTION STRING-LISTP) (547 :EXECUTABLE-COUNTERPART STRING-LISTP) (546 :DEFINITION STRING-LISTP) (545 :TYPE-PRESCRIPTION STRING-APPEND) (544 :EXECUTABLE-COUNTERPART STRING-APPEND) (543 :DEFINITION STRING-APPEND) (542 :REWRITE APPEND-TO-NIL) (541 :REWRITE CHARACTER-LISTP-APPEND) (540 :REWRITE STANDARD-CHAR-LISTP-APPEND) (539 :INDUCTION BINARY-APPEND) (538 :TYPE-PRESCRIPTION BINARY-APPEND) (537 :EXECUTABLE-COUNTERPART BINARY-APPEND) (536 :DEFINITION BINARY-APPEND) (535 :REWRITE KEYWORD-PACKAGE) (534 :REWRITE ACL2-PACKAGE) (533 :REWRITE ACL2-OUTPUT-CHANNEL-PACKAGE) (532 :REWRITE ACL2-INPUT-CHANNEL-PACKAGE) (531 :REWRITE SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL) (530 :INDUCTION MEMBER-SYMBOL-NAME) (529 :TYPE-PRESCRIPTION MEMBER-SYMBOL-NAME) (528 :EXECUTABLE-COUNTERPART MEMBER-SYMBOL-NAME) (527 :DEFINITION MEMBER-SYMBOL-NAME) (526 :REWRITE SYMBOL-PACKAGE-NAME-PKG-WITNESS-NAME) (525 :REWRITE SYMBOL-NAME-PKG-WITNESS) (524 :FORWARD-CHAINING SYMBOL-PACKAGE-NAME-OF-SYMBOL-IS-NOT-EMPTY-STRING) (523 :REWRITE INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME) (522 :FORWARD-CHAINING KEYWORDP-FORWARD-TO-SYMBOLP) (521 :TYPE-PRESCRIPTION KEYWORDP) (520 :EXECUTABLE-COUNTERPART KEYWORDP) (519 :DEFINITION KEYWORDP) (518 :TYPE-PRESCRIPTION ILLEGAL) (517 :EXECUTABLE-COUNTERPART ILLEGAL) (516 :DEFINITION ILLEGAL) (515 :TYPE-PRESCRIPTION HARD-ERROR) (514 :EXECUTABLE-COUNTERPART HARD-ERROR) (513 :DEFINITION HARD-ERROR) (512 :TYPE-PRESCRIPTION SYMBOLP-PKG-WITNESS) (511 :TYPE-PRESCRIPTION SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL) (510 :TYPE-PRESCRIPTION STRINGP-SYMBOL-PACKAGE-NAME) (509 :TYPE-PRESCRIPTION NULL-BODY-ER) (508 :EXECUTABLE-COUNTERPART NULL-BODY-ER) (507 :DEFINITION NULL-BODY-ER) (506 :INDUCTION LIST*-MACRO) (505 :TYPE-PRESCRIPTION LIST*-MACRO) (504 :EXECUTABLE-COUNTERPART LIST*-MACRO) (503 :DEFINITION LIST*-MACRO) (502 :TYPE-PRESCRIPTION MAKE-ORD) (501 :EXECUTABLE-COUNTERPART MAKE-ORD) (500 :DEFINITION MAKE-ORD) (499 :REWRITE O-P-IMPLIES-O:u 2:x(INCLUDE-BOOK "enabledp-change") ACL2 !>:u 1:x(INCLUDE-BOOK "h") ACL2 !>:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(include-book "enabledp-change") Summary Form: ( INCLUDE-BOOK "enabledp-change" ...) Rules: NIL Warnings: None Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04) "/Users/kaufmann/talks/seminar-2009-10-28/enabledp-change.lisp" ACL2 !>(encapsulate () (defun f (x) x) (in-theory (disable f))) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(DEFUN F (X) X) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) X). Summary Form: ( DEFUN F ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>>(IN-THEORY (DISABLE F)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 2064 End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. We export F. Summary Form: ( ENCAPSULATE NIL (DEFUN F ...) ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 !>:pe-ped f d 2:x(ENCAPSULATE NIL ...) \ >L d (DEFUN F (X) X) ACL2 !>(defun k (x) x) Since K is non-recursive, its admission is trivial. We observe that the type of K is described by the theorem (EQUAL (K X) X). Summary Form: ( DEFUN K ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) K ACL2 !>(in-theory (disable f)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 2067 ACL2 !>:pe-ped f d 2 (ENCAPSULATE NIL ...) \ >L d (DEFUN F (X) X) ACL2 !>:redef (:QUERY . :OVERWRITE) ACL2 !>(defun f (x) x) The event ( DEFUN F ...) is redundant. See :DOC redundant-events. Summary Form: ( DEFUN F ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT ACL2 !>(defun f (x) (cons x x)) ACL2 Query (:REDEF): The name F is in use as a function. Its current defun-mode is :logic. Do you want to redefine it? (N, Y, E, O or ?): y Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (CONSP (F X)). We used primitive type reasoning. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>:pe f L 5:x(DEFUN F (X) (CONS X X)) Additional events for the logical name F: 2 (ENCAPSULATE NIL ...) \ >L (DEFUN F (X) X) ACL2 !>:pe-ped f The rune (:DEFINITION F) is enabled, and always has been since the boot-strap world. ACL2 !>:pe-ped (:definition f) The rune (:DEFINITION F) is enabled, and always has been since the boot-strap world. ACL2 !>:u 4:x(IN-THEORY (DISABLE F)) ACL2 !>:pe-ped (:definition f) d 2 (ENCAPSULATE NIL ...) \ >L d (DEFUN F (X) X) ACL2 !>state ACL2 !>