(IN-PACKAGE "ACL2") "ACL2 Version 3.2" :BEGIN-PORTCULLIS-CMDS (DEFPKG "U" (UNION-EQ '(& &ALLOW-OTHER-KEYS &AUX &BODY &KEY &OPTIONAL &REST &WHOLE * *ACL2-EXPORTS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *MAIN-LISP-PACKAGE-NAME* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-OI* + - / /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP AND AND-MACRO APPEND AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP-GLOBAL BOUNDP-GLOBAL1 BRR BRR@ BUILD-STATE1 BUTLAST CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CBD CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CERTIFY-BOOK CERTIFY-BOOK! CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-UPCASE CHAR< CHAR<= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CLAUSE CLEAR-HASH-TABLES CLEAR-MEMOIZE-TABLES CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSURE CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 CONCATENATE COND COND-CLAUSESP COND-MACRO CONJUGATE CONS CONS-EQUAL CONSP CONSP-ASSOC CONSP-ASSOC-EQ CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DECLARE DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCONG DEFCONST DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFLABEL DEFMACRO DEFPKG DEFREFINEMENT DEFSTOBJ DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFUN DEFUN-SK DEFUND DEFUNS DELETE-PAIR DENOMINATOR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DISABLE DISABLE-FORCING DISABLEDP DISTRIBUTIVITY DOC DOC! DOCS DOUBLE-REWRITE DUPLICATES E/D E0-ORD-< E0-ORDINALP EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ENABLE ENABLE-FORCING ENCAPSULATE ENDP EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE ER ER-PROGN ER-PROGN-FN EVENP EVENS EVENT EXECUTABLE-COUNTERPART-THEORY EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD FERTILIZE FGETPROP FIFTH FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FIRST FIRST-N-AC FIX FIX-TRUE-LIST FLOOR FLUSH-HONS-GET-HASH-TABLE-LINK FMS FMT FMT-TO-COMMENT-WINDOW FMT1 FORCE FOURTH FUNCTION-SYMBOLP FUNCTION-THEORY GENERALIZE GET-GLOBAL GET-TIMER GETPROP-DEFAULT GETPROPS GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS GLOBAL-TABLE-CARS1 GLOBAL-VAL GOOD-BYE GOOD-DEFUN-MODE-P GROUND-ZERO HARD-ERROR HAS-PROPSP HAS-PROPSP1 HEADER HELP HIDE HONS HONS-ACONS HONS-ACONS! HONS-COPY HONS-EQUAL HONS-GET HONS-GET-FN-DO-HOPY HONS-GET-FN-DO-NOT-HOPY HONS-LET HONS-READ-OBJECT HONS-SHRINK-ALIST HONS-SHRINK-ALIST! I-AM-HERE ID IDATES IDENTITY IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1 IFF-IMPLIES-EQUAL-IMPLIES-2 IFF-IMPLIES-EQUAL-NOT IFF-IS-AN-EQUIVALENCE IFIX IGNORE ILLEGAL IMAGPART IMAGPART-COMPLEX IMMEDIATE-FORCE-MODEP IMPLIES IMPROPER-CONSP IN-ARITHMETIC-THEORY IN-PACKAGE IN-THEORY INCLUDE-BOOK INCOMPATIBLE INCREMENT-TIMER INDUCT INIT-HASH-TABLES INIT-HONS-ACONS-TABLE INT= INTEGER INTEGER-0 INTEGER-1 INTEGER-ABS INTEGER-IMPLIES-RATIONAL INTEGER-LENGTH INTEGER-LISTP INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP INTEGER-STEP INTEGERP INTERN INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME INTERSECTION-EQ INTERSECTION-THEORIES INTERSECTP-EQ INTERSECTP-EQUAL INVERSE-OF-* INVERSE-OF-+ INVISIBLE-FNS-TABLE KEYWORD-PACKAGE KEYWORD-VALUE-LISTP KEYWORD-VALUE-LISTP-ASSOC-KEYWORD KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP LAMBDA LAST LD LD-ERROR-ACTION LD-ERROR-TRIPLES LD-KEYWORD-ALIASES LD-POST-EVAL-PRINT LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT LD-PROMPT LD-QUERY-CONTROL-ALIST LD-REDEFINITION-ACTION LD-SKIP-PROOFSP LD-VERBOSE LEGAL-CASE-CLAUSESP LEN LEN-UPDATE-NTH LENGTH LET* LIST LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES LIST-ALL-PACKAGE-NAMES-LST LIST-MACRO LISTP LOCAL LOGAND LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT LOGEQV LOGIC LOGIOR LOGNAND LOGNOR LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P LOWEST-TERMS LP MACRO-ALIASES MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION MAKE-CHARACTER-LIST MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST MAKE-EVENT MAKE-FMT-BINDINGS MAKE-INPUT-CHANNEL MAKE-LIST MAKE-LIST-AC MAKE-MV-NTHS MAKE-ORD MAKE-OUTPUT-CHANNEL MAKE-VAR-LST MAKE-VAR-LST1 MAKUNBOUND-GLOBAL MAX MAXIMUM-LENGTH MAY-NEED-SLASHES MBE MBT MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-SYMBOL-NAME MEMOIZE-LET MEMOIZE-OFF MEMOIZE-ON MFC MIN MINIMAL-THEORY MINUSP MOD MONITOR MONITORED-RUNES MORE MORE! MORE-DOC MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP MV MV-LET MV-NTH NATP NEWLINE NFIX NIL NIL-IS-NOT-CIRCULAR NINTH NO-DUPLICATESP NO-DUPLICATESP-EQUAL NONNEGATIVE-INTEGER-QUOTIENT NONNEGATIVE-PRODUCT NONZERO-IMAGPART NOT NQTHM-TO-ACL2 NTH NTH-0-CONS NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION NTH-ADD1 NTH-ALIASES NTH-UPDATE-NTH NTHCDR NULL NUMERATOR O-FINP O-FIRST-COEFF O-FIRST-EXPT O-INFP O-P O-RST O< O<= O> O>= OBSERVATION ODDP ODDS OK-IF OOPS OPEN-CHANNEL-LISTP OPEN-CHANNEL1 OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD OPEN-INPUT-CHANNEL OPEN-INPUT-CHANNEL-ANY-P OPEN-INPUT-CHANNEL-ANY-P1 OPEN-INPUT-CHANNEL-P OPEN-INPUT-CHANNEL-P1 OPEN-INPUT-CHANNELS OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL! OPEN-OUTPUT-CHANNEL-ANY-P OPEN-OUTPUT-CHANNEL-ANY-P1 OPEN-OUTPUT-CHANNEL-P OPEN-OUTPUT-CHANNEL-P1 OPEN-OUTPUT-CHANNELS OR OR-MACRO ORDERED-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-ADD-PAIR ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-GETPROPS ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR OTHERWISE OUR-DIGIT-CHAR-P PAIRLIS$ PAIRLIS2 PBT PC PCB PCB! PCS PE PEEK-CHAR$ PF PL PLEV0 PLUSP POP-TIMER POSITION POSITION-AC POSITION-EQ POSITION-EQ-AC POSITION-EQUAL POSITION-EQUAL-AC POSITIVE POSP POWER-EVAL PPROGN PR PR! PREPROCESS PRIN1$ PRIN1-WITH-SLASHES PRIN1-WITH-SLASHES1 PRINC$ PRINT-OBJECT$ PRINT-RATIONAL-AS-DECIMAL PRINT-TIMER PROG2$ PROGN PROGRAM PROOF-TREE PROOFS-CO PROPER-CONSP PROPS PROVE PSEUDO-TERM-LISTP PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP PSEUDO-TERMP PSTACK PUFF PUFF* PUSH-TIMER PUSH-UNTOUCHABLE PUT-ASSOC-EQ PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP QUOTE QUOTEP R-EQLABLE-ALISTP RASSOC RASSOC-EQ RASSOC-EQUAL RATIO RATIONAL RATIONAL-IMPLIES1 RATIONAL-IMPLIES2 RATIONAL-LISTP RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP RATIONALP RATIONALP-* RATIONALP-+ RATIONALP-EXPT-TYPE-PRESCRIPTION RATIONALP-IMPLIES-ACL2-NUMBERP RATIONALP-UNARY-- RATIONALP-UNARY-/ READ-ACL2-ORACLE READ-ACL2-ORACLE-PRESERVES-STATE-P1 READ-BYTE$ READ-CHAR$ READ-FILE-LISTP READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP READ-FILE-LISTP1 READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP READ-FILES READ-FILES-P READ-FILES-P-FORWARD-TO-READ-FILE-LISTP READ-IDATE READ-OBJECT READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1 READABLE-FILE READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP READABLE-FILES READABLE-FILES-LISTP READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP READABLE-FILES-P READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP REAL/RATIONALP REALFIX REALPART REALPART-COMPLEX REALPART-IMAGPART-ELIM REBUILD REDEF REDEF! REM REMOVE REMOVE-BINOP REMOVE-DEFAULT-HINTS REMOVE-DEFAULT-HINTS! REMOVE-DUPLICATES REMOVE-DUPLICATES-EQL REMOVE-DUPLICATES-EQUAL REMOVE-EQ REMOVE-EQUAL REMOVE-FIRST-PAIR REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-NTH-ALIAS REMOVE-UNTOUCHABLE REMOVE1 REMOVE1-EQ REMOVE1-EQUAL RESET-LD-SPECIALS RESET-PREHISTORY REST RETRACT-WORLD RETRIEVE REVAPPEND REVERSE RFIX ROUND SATISFIES SECOND SET-BACKCHAIN-LIMIT SET-BODY SET-BOGUS-MUTUAL-RECURSION-OK SET-CASE-SPLIT-LIMITATIONS SET-CBD SET-COMPILE-FNS SET-DEFAULT-HINTS SET-DEFAULT-HINTS! SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL SET-DIFFERENCE-THEORIES SET-ENFORCE-REDUNDANCY SET-EQUALP-EQUAL SET-GUARD-CHECKING SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST SET-INHIBIT-WARNINGS SET-INVISIBLE-FNS-TABLE SET-IRRELEVANT-FORMALS-OK SET-MEASURE-FUNCTION SET-NON-LINEARP SET-SAVED-OUTPUT SET-STATE-OK SET-TIMER SET-VERIFY-GUARDS-EAGERNESS SET-W SET-WELL-FOUNDED-RELATION SEVENTH SGETPROP SHOW-ACCUMULATED-PERSISTENCE SHOW-BDD SHOW-BODIES SHRINK-32-BIT-INTEGER-STACK SHRINK-T-STACK SIGNED-BYTE SIGNUM SIMPLIFY SIXTH SKIP-PROOFS SOME-SLASHABLE STABLE-UNDER-SIMPLIFICATIONP STANDARD-CHAR STANDARD-CHAR-LISTP STANDARD-CHAR-LISTP-APPEND STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP STANDARD-CHAR-P STANDARD-CHAR-P-NTH STANDARD-CO STANDARD-OI STANDARD-STRING-ALISTP STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP START-PROOF-TREE STATE STATE-GLOBAL-LET*-CLEANUP STATE-GLOBAL-LET*-GET-GLOBALS STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1 STATE-P1 STATE-P1-FORWARD STATE-P1-UPDATE-MAIN-TIMER STATE-P1-UPDATE-NTH-2-WORLD STOP-PROOF-TREE STRING STRING-APPEND STRING-APPEND-LST STRING-DOWNCASE STRING-DOWNCASE1 STRING-EQUAL STRING-EQUAL1 STRING-IS-NOT-CIRCULAR STRING-LISTP STRING-UPCASE STRING-UPCASE1 STRING< STRING<-IRREFLEXIVE STRING<-L STRING<-L-ASYMMETRIC STRING<-L-IRREFLEXIVE STRING<-L-TRANSITIVE STRING<-L-TRICHOTOMY STRING<= STRING> STRING>= STRINGP STRINGP-SYMBOL-PACKAGE-NAME STRIP-CARS STRIP-CDRS SUBLIS SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQUAL SUBST SUBSTITUTE SUBSTITUTE-AC SUMMARY SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP SYMBOL-DOUBLET-LISTP SYMBOL-EQUALITY SYMBOL-LISTP SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP SYMBOL-NAME SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL SYMBOL-PACKAGE-NAME SYMBOLP SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL SYNP SYNTAXP SYS-CALL SYS-CALL-STATUS T T-STACK T-STACK-LENGTH T-STACK-LENGTH1 TABLE TABLE-ALIST TAKE TENTH THE THE-ERROR THE-FIXNUM THE-FIXNUM! THEORY THEORY-INVARIANT THIRD THM TIME$ TIMER-ALISTP TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP TOGGLE-PC-MACRO TRACE$ TRANS TRANS1 TRICHOTOMY TRUE-LIST-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ TRUE-LISTP TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P TRUE-LISTP-UPDATE-NTH TRUNCATE TYPE TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP U UBT UBT! UNARY-- UNARY-/ UNARY-FUNCTION-SYMBOL-LISTP UNICITY-OF-0 UNICITY-OF-1 UNION-EQ UNION-EQUAL UNION-THEORIES UNIVERSAL-THEORY UNMONITOR UNSAVE UNSIGNED-BYTE UNTRACE$ UPDATE-32-BIT-INTEGER-STACK UPDATE-ACL2-ORACLE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1 UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK UPDATE-GLOBAL-TABLE UPDATE-IDATES UPDATE-LIST-ALL-PACKAGE-NAMES-LST UPDATE-NTH UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS UPDATE-READ-FILES UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST UPDATE-USER-STOBJ-ALIST1 UPDATE-WRITTEN-FILES UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P USER-STOBJ-ALIST USER-STOBJ-ALIST1 VALUE-TRIPLE VERBOSE-PSTACK VERIFY VERIFY-GUARDS VERIFY-TERMINATION W WARNING! WET WITH-OUTPUT WORLD WORLDP WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP WORMHOLE WORMHOLE1 WRITABLE-FILE-LISTP WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP WRITABLE-FILE-LISTP1 WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITE-BYTE$ WRITEABLE-FILES WRITEABLE-FILES-P WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP WRITTEN-FILE WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITTEN-FILE-LISTP WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP WRITTEN-FILES WRITTEN-FILES-P WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP XARGS XXXJOIN ZERO ZEROP ZIP ZP) '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH* &AUX *PRINT-PPRINT-DISPATCH* &BODY *PRINT-PRETTY* &ENVIRONMENT *PRINT-RADIX* &KEY *PRINT-READABLY* &OPTIONAL *PRINT-RIGHT-MARGIN* &REST *QUERY-IO* &WHOLE *RANDOM-STATE* * *READ-BASE* ** *READ-DEFAULT-FLOAT-FORMAT* *** *READ-EVAL* *BREAK-ON-SIGNALS* *READ-SUPPRESS* *COMPILE-FILE-PATHNAME* *READTABLE* *COMPILE-FILE-TRUENAME* *STANDARD-INPUT* *COMPILE-PRINT* *STANDARD-OUTPUT* *COMPILE-VERBOSE* *TERMINAL-IO* *DEBUG-IO* *TRACE-OUTPUT* *DEBUGGER-HOOK* + *DEFAULT-PATHNAME-DEFAULTS* ++ *ERROR-OUTPUT* +++ *FEATURES* - *GENSYM-COUNTER* / *LOAD-PATHNAME* // *LOAD-PRINT* /// *LOAD-TRUENAME* /= *LOAD-VERBOSE* 1+ *MACROEXPAND-HOOK* 1- *MODULES* < *PACKAGE* <= *PRINT-ARRAY* = *PRINT-BASE* > *PRINT-CASE* >= *PRINT-CIRCLE* ABORT *PRINT-ESCAPE* ABS *PRINT-GENSYM* ACONS *PRINT-LENGTH* ACOS *PRINT-LEVEL* ACOSH *PRINT-LINES* ADD-METHOD ADJOIN ATOM BOUNDP ADJUST-ARRAY BASE-CHAR BREAK ADJUSTABLE-ARRAY-P BASE-STRING BROADCAST-STREAM ALLOCATE-INSTANCE BIGNUM BROADCAST-STREAM-STREAMS ALPHA-CHAR-P BIT BUILT-IN-CLASS ALPHANUMERICP BIT-AND BUTLAST AND BIT-ANDC1 BYTE APPEND BIT-ANDC2 BYTE-POSITION APPLY BIT-EQV BYTE-SIZE APROPOS BIT-IOR CAAAAR APROPOS-LIST BIT-NAND CAAADR AREF BIT-NOR CAAAR ARITHMETIC-ERROR BIT-NOT CAADAR ARITHMETIC-ERROR-OPERANDS BIT-ORC1 CAADDR ARITHMETIC-ERROR-OPERATION BIT-ORC2 CAADR ARRAY BIT-VECTOR CAAR ARRAY-DIMENSION BIT-VECTOR-P CADAAR ARRAY-DIMENSION-LIMIT BIT-XOR CADADR ARRAY-DIMENSIONS BLOCK CADAR ARRAY-DISPLACEMENT BOOLE CADDAR ARRAY-ELEMENT-TYPE BOOLE-1 CADDDR ARRAY-HAS-FILL-POINTER-P BOOLE-2 CADDR ARRAY-IN-BOUNDS-P BOOLE-AND CADR ARRAY-RANK BOOLE-ANDC1 CALL-ARGUMENTS-LIMIT ARRAY-RANK-LIMIT BOOLE-ANDC2 CALL-METHOD ARRAY-ROW-MAJOR-INDEX BOOLE-C1 CALL-NEXT-METHOD ARRAY-TOTAL-SIZE BOOLE-C2 CAR ARRAY-TOTAL-SIZE-LIMIT BOOLE-CLR CASE ARRAYP BOOLE-EQV CATCH ASH BOOLE-IOR CCASE ASIN BOOLE-NAND CDAAAR ASINH BOOLE-NOR CDAADR ASSERT BOOLE-ORC1 CDAAR ASSOC BOOLE-ORC2 CDADAR ASSOC-IF BOOLE-SET CDADDR ASSOC-IF-NOT BOOLE-XOR CDADR ATAN BOOLEAN CDAR ATANH BOTH-CASE-P CDDAAR CDDADR CLEAR-INPUT COPY-TREE CDDAR CLEAR-OUTPUT COS CDDDAR CLOSE COSH CDDDDR CLRHASH COUNT CDDDR CODE-CHAR COUNT-IF CDDR COERCE COUNT-IF-NOT CDR COMPILATION-SPEED CTYPECASE CEILING COMPILE DEBUG CELL-ERROR COMPILE-FILE DECF CELL-ERROR-NAME COMPILE-FILE-PATHNAME DECLAIM CERROR COMPILED-FUNCTION DECLARATION CHANGE-CLASS COMPILED-FUNCTION-P DECLARE CHAR COMPILER-MACRO DECODE-FLOAT CHAR-CODE COMPILER-MACRO-FUNCTION DECODE-UNIVERSAL-TIME CHAR-CODE-LIMIT COMPLEMENT DEFCLASS CHAR-DOWNCASE COMPLEX DEFCONSTANT CHAR-EQUAL COMPLEXP DEFGENERIC CHAR-GREATERP COMPUTE-APPLICABLE-METHODS DEFINE-COMPILER-MACRO CHAR-INT COMPUTE-RESTARTS DEFINE-CONDITION CHAR-LESSP CONCATENATE DEFINE-METHOD-COMBINATION CHAR-NAME CONCATENATED-STREAM DEFINE-MODIFY-MACRO CHAR-NOT-EQUAL CONCATENATED-STREAM-STREAMS DEFINE-SETF-EXPANDER CHAR-NOT-GREATERP COND DEFINE-SYMBOL-MACRO CHAR-NOT-LESSP CONDITION DEFMACRO CHAR-UPCASE CONJUGATE DEFMETHOD CHAR/= CONS DEFPACKAGE CHAR< CONSP DEFPARAMETER CHAR<= CONSTANTLY DEFSETF CHAR= CONSTANTP DEFSTRUCT CHAR> CONTINUE DEFTYPE CHAR>= CONTROL-ERROR DEFUN CHARACTER COPY-ALIST DEFVAR CHARACTERP COPY-LIST DELETE CHECK-TYPE COPY-PPRINT-DISPATCH DELETE-DUPLICATES CIS COPY-READTABLE DELETE-FILE CLASS COPY-SEQ DELETE-IF CLASS-NAME COPY-STRUCTURE DELETE-IF-NOT CLASS-OF COPY-SYMBOL DELETE-PACKAGE DENOMINATOR EQ DEPOSIT-FIELD EQL DESCRIBE EQUAL DESCRIBE-OBJECT EQUALP DESTRUCTURING-BIND ERROR DIGIT-CHAR ETYPECASE DIGIT-CHAR-P EVAL DIRECTORY EVAL-WHEN DIRECTORY-NAMESTRING EVENP DISASSEMBLE EVERY DIVISION-BY-ZERO EXP DO EXPORT DO* EXPT DO-ALL-SYMBOLS EXTENDED-CHAR DO-EXTERNAL-SYMBOLS FBOUNDP DO-SYMBOLS FCEILING DOCUMENTATION FDEFINITION DOLIST FFLOOR DOTIMES FIFTH DOUBLE-FLOAT FILE-AUTHOR DOUBLE-FLOAT-EPSILON FILE-ERROR DOUBLE-FLOAT-NEGATIVE-EPSILON FILE-ERROR-PATHNAME DPB FILE-LENGTH DRIBBLE FILE-NAMESTRING DYNAMIC-EXTENT FILE-POSITION ECASE FILE-STREAM ECHO-STREAM FILE-STRING-LENGTH ECHO-STREAM-INPUT-STREAM FILE-WRITE-DATE ECHO-STREAM-OUTPUT-STREAM FILL ED FILL-POINTER EIGHTH FIND ELT FIND-ALL-SYMBOLS ENCODE-UNIVERSAL-TIME FIND-CLASS END-OF-FILE FIND-IF ENDP FIND-IF-NOT ENOUGH-NAMESTRING FIND-METHOD ENSURE-DIRECTORIES-EXIST FIND-PACKAGE ENSURE-GENERIC-FUNCTION FIND-RESTART FIND-SYMBOL GET-INTERNAL-RUN-TIME FINISH-OUTPUT GET-MACRO-CHARACTER FIRST GET-OUTPUT-STREAM-STRING FIXNUM GET-PROPERTIES FLET GET-SETF-EXPANSION FLOAT GET-UNIVERSAL-TIME FLOAT-DIGITS GETF FLOAT-PRECISION GETHASH FLOAT-RADIX GO FLOAT-SIGN GRAPHIC-CHAR-P FLOATING-POINT-INEXACT HANDLER-BIND FLOATING-POINT-INVALID-OPERATION HANDLER-CASE FLOATING-POINT-OVERFLOW HASH-TABLE FLOATING-POINT-UNDERFLOW HASH-TABLE-COUNT FLOATP HASH-TABLE-P FLOOR HASH-TABLE-REHASH-SIZE FMAKUNBOUND HASH-TABLE-REHASH-THRESHOLD FORCE-OUTPUT HASH-TABLE-SIZE FORMAT HASH-TABLE-TEST FORMATTER HOST-NAMESTRING FOURTH IDENTITY FRESH-LINE IF FROUND IGNORABLE FTRUNCATE IGNORE FTYPE IGNORE-ERRORS FUNCALL IMAGPART FUNCTION IMPORT FUNCTION-KEYWORDS IN-PACKAGE FUNCTION-LAMBDA-EXPRESSION INCF FUNCTIONP INITIALIZE-INSTANCE GCD INLINE GENERIC-FUNCTION INPUT-STREAM-P GENSYM INSPECT GENTEMP INTEGER GET INTEGER-DECODE-FLOAT GET-DECODED-TIME INTEGER-LENGTH GET-DISPATCH-MACRO-CHARACTER INTEGERP GET-INTERNAL-REAL-TIME INTERACTIVE-STREAM-P INTERN LISP-IMPLEMENTATION-TYPE INTERNAL-TIME-UNITS-PER-SECOND LISP-IMPLEMENTATION-VERSION INTERSECTION LIST INVALID-METHOD-ERROR LIST* INVOKE-DEBUGGER LIST-ALL-PACKAGES INVOKE-RESTART LIST-LENGTH INVOKE-RESTART-INTERACTIVELY LISTEN ISQRT LISTP KEYWORD LOAD KEYWORDP LOAD-LOGICAL-PATHNAME-TRANSLATIONS LABELS LOAD-TIME-VALUE LAMBDA LOCALLY LAMBDA-LIST-KEYWORDS LOG LAMBDA-PARAMETERS-LIMIT LOGAND LAST LOGANDC1 LCM LOGANDC2 LDB LOGBITP LDB-TEST LOGCOUNT LDIFF LOGEQV LEAST-NEGATIVE-DOUBLE-FLOAT LOGICAL-PATHNAME LEAST-NEGATIVE-LONG-FLOAT LOGICAL-PATHNAME-TRANSLATIONS LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT LOGIOR LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT LOGNAND LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT LOGNOR LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT LOGNOT LEAST-NEGATIVE-SHORT-FLOAT LOGORC1 LEAST-NEGATIVE-SINGLE-FLOAT LOGORC2 LEAST-POSITIVE-DOUBLE-FLOAT LOGTEST LEAST-POSITIVE-LONG-FLOAT LOGXOR LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT LONG-FLOAT LEAST-POSITIVE-NORMALIZED-LONG-FLOAT LONG-FLOAT-EPSILON LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT LONG-FLOAT-NEGATIVE-EPSILON LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT LONG-SITE-NAME LEAST-POSITIVE-SHORT-FLOAT LOOP LEAST-POSITIVE-SINGLE-FLOAT LOOP-FINISH LENGTH LOWER-CASE-P LET MACHINE-INSTANCE LET* MACHINE-TYPE MACHINE-VERSION MASK-FIELD MACRO-FUNCTION MAX MACROEXPAND MEMBER MACROEXPAND-1 MEMBER-IF MACROLET MEMBER-IF-NOT MAKE-ARRAY MERGE MAKE-BROADCAST-STREAM MERGE-PATHNAMES MAKE-CONCATENATED-STREAM METHOD MAKE-CONDITION METHOD-COMBINATION MAKE-DISPATCH-MACRO-CHARACTER METHOD-COMBINATION-ERROR MAKE-ECHO-STREAM METHOD-QUALIFIERS MAKE-HASH-TABLE MIN MAKE-INSTANCE MINUSP MAKE-INSTANCES-OBSOLETE MISMATCH MAKE-LIST MOD MAKE-LOAD-FORM MOST-NEGATIVE-DOUBLE-FLOAT MAKE-LOAD-FORM-SAVING-SLOTS MOST-NEGATIVE-FIXNUM MAKE-METHOD MOST-NEGATIVE-LONG-FLOAT MAKE-PACKAGE MOST-NEGATIVE-SHORT-FLOAT MAKE-PATHNAME MOST-NEGATIVE-SINGLE-FLOAT MAKE-RANDOM-STATE MOST-POSITIVE-DOUBLE-FLOAT MAKE-SEQUENCE MOST-POSITIVE-FIXNUM MAKE-STRING MOST-POSITIVE-LONG-FLOAT MAKE-STRING-INPUT-STREAM MOST-POSITIVE-SHORT-FLOAT MAKE-STRING-OUTPUT-STREAM MOST-POSITIVE-SINGLE-FLOAT MAKE-SYMBOL MUFFLE-WARNING MAKE-SYNONYM-STREAM MULTIPLE-VALUE-BIND MAKE-TWO-WAY-STREAM MULTIPLE-VALUE-CALL MAKUNBOUND MULTIPLE-VALUE-LIST MAP MULTIPLE-VALUE-PROG1 MAP-INTO MULTIPLE-VALUE-SETQ MAPC MULTIPLE-VALUES-LIMIT MAPCAN NAME-CHAR MAPCAR NAMESTRING MAPCON NBUTLAST MAPHASH NCONC MAPL NEXT-METHOD-P MAPLIST NIL NINTERSECTION PACKAGE-ERROR NINTH PACKAGE-ERROR-PACKAGE NO-APPLICABLE-METHOD PACKAGE-NAME NO-NEXT-METHOD PACKAGE-NICKNAMES NOT PACKAGE-SHADOWING-SYMBOLS NOTANY PACKAGE-USE-LIST NOTEVERY PACKAGE-USED-BY-LIST NOTINLINE PACKAGEP NRECONC PAIRLIS NREVERSE PARSE-ERROR NSET-DIFFERENCE PARSE-INTEGER NSET-EXCLUSIVE-OR PARSE-NAMESTRING NSTRING-CAPITALIZE PATHNAME NSTRING-DOWNCASE PATHNAME-DEVICE NSTRING-UPCASE PATHNAME-DIRECTORY NSUBLIS PATHNAME-HOST NSUBST PATHNAME-MATCH-P NSUBST-IF PATHNAME-NAME NSUBST-IF-NOT PATHNAME-TYPE NSUBSTITUTE PATHNAME-VERSION NSUBSTITUTE-IF PATHNAMEP NSUBSTITUTE-IF-NOT PEEK-CHAR NTH PHASE NTH-VALUE PI NTHCDR PLUSP NULL POP NUMBER POSITION NUMBERP POSITION-IF NUMERATOR POSITION-IF-NOT NUNION PPRINT ODDP PPRINT-DISPATCH OPEN PPRINT-EXIT-IF-LIST-EXHAUSTED OPEN-STREAM-P PPRINT-FILL OPTIMIZE PPRINT-INDENT OR PPRINT-LINEAR OTHERWISE PPRINT-LOGICAL-BLOCK OUTPUT-STREAM-P PPRINT-NEWLINE PACKAGE PPRINT-POP PPRINT-TAB READ-CHAR PPRINT-TABULAR READ-CHAR-NO-HANG PRIN1 READ-DELIMITED-LIST PRIN1-TO-STRING READ-FROM-STRING PRINC READ-LINE PRINC-TO-STRING READ-PRESERVING-WHITESPACE PRINT READ-SEQUENCE PRINT-NOT-READABLE READER-ERROR PRINT-NOT-READABLE-OBJECT READTABLE PRINT-OBJECT READTABLE-CASE PRINT-UNREADABLE-OBJECT READTABLEP PROBE-FILE REAL PROCLAIM REALP PROG REALPART PROG* REDUCE PROG1 REINITIALIZE-INSTANCE PROG2 REM PROGN REMF PROGRAM-ERROR REMHASH PROGV REMOVE PROVIDE REMOVE-DUPLICATES PSETF REMOVE-IF PSETQ REMOVE-IF-NOT PUSH REMOVE-METHOD PUSHNEW REMPROP QUOTE RENAME-FILE RANDOM RENAME-PACKAGE RANDOM-STATE REPLACE RANDOM-STATE-P REQUIRE RASSOC REST RASSOC-IF RESTART RASSOC-IF-NOT RESTART-BIND RATIO RESTART-CASE RATIONAL RESTART-NAME RATIONALIZE RETURN RATIONALP RETURN-FROM READ REVAPPEND READ-BYTE REVERSE ROOM SIMPLE-BIT-VECTOR ROTATEF SIMPLE-BIT-VECTOR-P ROUND SIMPLE-CONDITION ROW-MAJOR-AREF SIMPLE-CONDITION-FORMAT-ARGUMENTS RPLACA SIMPLE-CONDITION-FORMAT-CONTROL RPLACD SIMPLE-ERROR SAFETY SIMPLE-STRING SATISFIES SIMPLE-STRING-P SBIT SIMPLE-TYPE-ERROR SCALE-FLOAT SIMPLE-VECTOR SCHAR SIMPLE-VECTOR-P SEARCH SIMPLE-WARNING SECOND SIN SEQUENCE SINGLE-FLOAT SERIOUS-CONDITION SINGLE-FLOAT-EPSILON SET SINGLE-FLOAT-NEGATIVE-EPSILON SET-DIFFERENCE SINH SET-DISPATCH-MACRO-CHARACTER SIXTH SET-EXCLUSIVE-OR SLEEP SET-MACRO-CHARACTER SLOT-BOUNDP SET-PPRINT-DISPATCH SLOT-EXISTS-P SET-SYNTAX-FROM-CHAR SLOT-MAKUNBOUND SETF SLOT-MISSING SETQ SLOT-UNBOUND SEVENTH SLOT-VALUE SHADOW SOFTWARE-TYPE SHADOWING-IMPORT SOFTWARE-VERSION SHARED-INITIALIZE SOME SHIFTF SORT SHORT-FLOAT SPACE SHORT-FLOAT-EPSILON SPECIAL SHORT-FLOAT-NEGATIVE-EPSILON SPECIAL-OPERATOR-P SHORT-SITE-NAME SPEED SIGNAL SQRT SIGNED-BYTE STABLE-SORT SIGNUM STANDARD SIMPLE-ARRAY STANDARD-CHAR SIMPLE-BASE-STRING STANDARD-CHAR-P STANDARD-CLASS SUBLIS STANDARD-GENERIC-FUNCTION SUBSEQ STANDARD-METHOD SUBSETP STANDARD-OBJECT SUBST STEP SUBST-IF STORAGE-CONDITION SUBST-IF-NOT STORE-VALUE SUBSTITUTE STREAM SUBSTITUTE-IF STREAM-ELEMENT-TYPE SUBSTITUTE-IF-NOT STREAM-ERROR SUBTYPEP STREAM-ERROR-STREAM SVREF STREAM-EXTERNAL-FORMAT SXHASH STREAMP SYMBOL STRING SYMBOL-FUNCTION STRING-CAPITALIZE SYMBOL-MACROLET STRING-DOWNCASE SYMBOL-NAME STRING-EQUAL SYMBOL-PACKAGE STRING-GREATERP SYMBOL-PLIST STRING-LEFT-TRIM SYMBOL-VALUE STRING-LESSP SYMBOLP STRING-NOT-EQUAL SYNONYM-STREAM STRING-NOT-GREATERP SYNONYM-STREAM-SYMBOL STRING-NOT-LESSP T STRING-RIGHT-TRIM TAGBODY STRING-STREAM TAILP STRING-TRIM TAN STRING-UPCASE TANH STRING/= TENTH STRING< TERPRI STRING<= THE STRING= THIRD STRING> THROW STRING>= TIME STRINGP TRACE STRUCTURE TRANSLATE-LOGICAL-PATHNAME STRUCTURE-CLASS TRANSLATE-PATHNAME STRUCTURE-OBJECT TREE-EQUAL STYLE-WARNING TRUENAME TRUNCATE VALUES-LIST TWO-WAY-STREAM VARIABLE TWO-WAY-STREAM-INPUT-STREAM VECTOR TWO-WAY-STREAM-OUTPUT-STREAM VECTOR-POP TYPE VECTOR-PUSH TYPE-ERROR VECTOR-PUSH-EXTEND TYPE-ERROR-DATUM VECTORP TYPE-ERROR-EXPECTED-TYPE WARN TYPE-OF WARNING TYPECASE WHEN TYPEP WILD-PATHNAME-P UNBOUND-SLOT WITH-ACCESSORS UNBOUND-SLOT-INSTANCE WITH-COMPILATION-UNIT UNBOUND-VARIABLE WITH-CONDITION-RESTARTS UNDEFINED-FUNCTION WITH-HASH-TABLE-ITERATOR UNEXPORT WITH-INPUT-FROM-STRING UNINTERN WITH-OPEN-FILE UNION WITH-OPEN-STREAM UNLESS WITH-OUTPUT-TO-STRING UNREAD-CHAR WITH-PACKAGE-ITERATOR UNSIGNED-BYTE WITH-SIMPLE-RESTART UNTRACE WITH-SLOTS UNUSE-PACKAGE WITH-STANDARD-IO-SYNTAX UNWIND-PROTECT WRITE UPDATE-INSTANCE-FOR-DIFFERENT-CLASS WRITE-BYTE UPDATE-INSTANCE-FOR-REDEFINED-CLASS WRITE-CHAR UPGRADED-ARRAY-ELEMENT-TYPE WRITE-LINE UPGRADED-COMPLEX-PART-TYPE WRITE-SEQUENCE UPPER-CASE-P WRITE-STRING USE-PACKAGE WRITE-TO-STRING USE-VALUE Y-OR-N-P USER-HOMEDIR-PATHNAME YES-OR-NO-P VALUES ZEROP)) NIL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/ihs-init.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp")) (DEFPKG "ACL2-ASG" (SET-DIFFERENCE-EQUAL (UNION-EQ '(& &ALLOW-OTHER-KEYS &AUX &BODY &KEY &OPTIONAL &REST &WHOLE * *ACL2-EXPORTS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *MAIN-LISP-PACKAGE-NAME* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-OI* + - / /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP AND AND-MACRO APPEND AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP-GLOBAL BOUNDP-GLOBAL1 BRR BRR@ BUILD-STATE1 BUTLAST CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CBD CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CERTIFY-BOOK CERTIFY-BOOK! CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-UPCASE CHAR< CHAR<= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CLAUSE CLEAR-HASH-TABLES CLEAR-MEMOIZE-TABLES CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSURE CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 CONCATENATE COND COND-CLAUSESP COND-MACRO CONJUGATE CONS CONS-EQUAL CONSP CONSP-ASSOC CONSP-ASSOC-EQ CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DECLARE DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCONG DEFCONST DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFLABEL DEFMACRO DEFPKG DEFREFINEMENT DEFSTOBJ DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFUN DEFUN-SK DEFUND DEFUNS DELETE-PAIR DENOMINATOR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DISABLE DISABLE-FORCING DISABLEDP DISTRIBUTIVITY DOC DOC! DOCS DOUBLE-REWRITE DUPLICATES E/D E0-ORD-< E0-ORDINALP EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ENABLE ENABLE-FORCING ENCAPSULATE ENDP EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE ER ER-PROGN ER-PROGN-FN EVENP EVENS EVENT EXECUTABLE-COUNTERPART-THEORY EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD FERTILIZE FGETPROP FIFTH FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FIRST FIRST-N-AC FIX FIX-TRUE-LIST FLOOR FLUSH-HONS-GET-HASH-TABLE-LINK FMS FMT FMT-TO-COMMENT-WINDOW FMT1 FORCE FOURTH FUNCTION-SYMBOLP FUNCTION-THEORY GENERALIZE GET-GLOBAL GET-TIMER GETPROP-DEFAULT GETPROPS GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS GLOBAL-TABLE-CARS1 GLOBAL-VAL GOOD-BYE GOOD-DEFUN-MODE-P GROUND-ZERO HARD-ERROR HAS-PROPSP HAS-PROPSP1 HEADER HELP HIDE HONS HONS-ACONS HONS-ACONS! HONS-COPY HONS-EQUAL HONS-GET HONS-GET-FN-DO-HOPY HONS-GET-FN-DO-NOT-HOPY HONS-LET HONS-READ-OBJECT HONS-SHRINK-ALIST HONS-SHRINK-ALIST! I-AM-HERE ID IDATES IDENTITY IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1 IFF-IMPLIES-EQUAL-IMPLIES-2 IFF-IMPLIES-EQUAL-NOT IFF-IS-AN-EQUIVALENCE IFIX IGNORE ILLEGAL IMAGPART IMAGPART-COMPLEX IMMEDIATE-FORCE-MODEP IMPLIES IMPROPER-CONSP IN-ARITHMETIC-THEORY IN-PACKAGE IN-THEORY INCLUDE-BOOK INCOMPATIBLE INCREMENT-TIMER INDUCT INIT-HASH-TABLES INIT-HONS-ACONS-TABLE INT= INTEGER INTEGER-0 INTEGER-1 INTEGER-ABS INTEGER-IMPLIES-RATIONAL INTEGER-LENGTH INTEGER-LISTP INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP INTEGER-STEP INTEGERP INTERN INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME INTERSECTION-EQ INTERSECTION-THEORIES INTERSECTP-EQ INTERSECTP-EQUAL INVERSE-OF-* INVERSE-OF-+ INVISIBLE-FNS-TABLE KEYWORD-PACKAGE KEYWORD-VALUE-LISTP KEYWORD-VALUE-LISTP-ASSOC-KEYWORD KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP LAMBDA LAST LD LD-ERROR-ACTION LD-ERROR-TRIPLES LD-KEYWORD-ALIASES LD-POST-EVAL-PRINT LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT LD-PROMPT LD-QUERY-CONTROL-ALIST LD-REDEFINITION-ACTION LD-SKIP-PROOFSP LD-VERBOSE LEGAL-CASE-CLAUSESP LEN LEN-UPDATE-NTH LENGTH LET* LIST LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES LIST-ALL-PACKAGE-NAMES-LST LIST-MACRO LISTP LOCAL LOGAND LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT LOGEQV LOGIC LOGIOR LOGNAND LOGNOR LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P LOWEST-TERMS LP MACRO-ALIASES MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION MAKE-CHARACTER-LIST MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST MAKE-EVENT MAKE-FMT-BINDINGS MAKE-INPUT-CHANNEL MAKE-LIST MAKE-LIST-AC MAKE-MV-NTHS MAKE-ORD MAKE-OUTPUT-CHANNEL MAKE-VAR-LST MAKE-VAR-LST1 MAKUNBOUND-GLOBAL MAX MAXIMUM-LENGTH MAY-NEED-SLASHES MBE MBT MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-SYMBOL-NAME MEMOIZE-LET MEMOIZE-OFF MEMOIZE-ON MFC MIN MINIMAL-THEORY MINUSP MOD MONITOR MONITORED-RUNES MORE MORE! MORE-DOC MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP MV MV-LET MV-NTH NATP NEWLINE NFIX NIL NIL-IS-NOT-CIRCULAR NINTH NO-DUPLICATESP NO-DUPLICATESP-EQUAL NONNEGATIVE-INTEGER-QUOTIENT NONNEGATIVE-PRODUCT NONZERO-IMAGPART NOT NQTHM-TO-ACL2 NTH NTH-0-CONS NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION NTH-ADD1 NTH-ALIASES NTH-UPDATE-NTH NTHCDR NULL NUMERATOR O-FINP O-FIRST-COEFF O-FIRST-EXPT O-INFP O-P O-RST O< O<= O> O>= OBSERVATION ODDP ODDS OK-IF OOPS OPEN-CHANNEL-LISTP OPEN-CHANNEL1 OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD OPEN-INPUT-CHANNEL OPEN-INPUT-CHANNEL-ANY-P OPEN-INPUT-CHANNEL-ANY-P1 OPEN-INPUT-CHANNEL-P OPEN-INPUT-CHANNEL-P1 OPEN-INPUT-CHANNELS OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL! OPEN-OUTPUT-CHANNEL-ANY-P OPEN-OUTPUT-CHANNEL-ANY-P1 OPEN-OUTPUT-CHANNEL-P OPEN-OUTPUT-CHANNEL-P1 OPEN-OUTPUT-CHANNELS OR OR-MACRO ORDERED-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-ADD-PAIR ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-GETPROPS ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR OTHERWISE OUR-DIGIT-CHAR-P PAIRLIS$ PAIRLIS2 PBT PC PCB PCB! PCS PE PEEK-CHAR$ PF PL PLEV0 PLUSP POP-TIMER POSITION POSITION-AC POSITION-EQ POSITION-EQ-AC POSITION-EQUAL POSITION-EQUAL-AC POSITIVE POSP POWER-EVAL PPROGN PR PR! PREPROCESS PRIN1$ PRIN1-WITH-SLASHES PRIN1-WITH-SLASHES1 PRINC$ PRINT-OBJECT$ PRINT-RATIONAL-AS-DECIMAL PRINT-TIMER PROG2$ PROGN PROGRAM PROOF-TREE PROOFS-CO PROPER-CONSP PROPS PROVE PSEUDO-TERM-LISTP PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP PSEUDO-TERMP PSTACK PUFF PUFF* PUSH-TIMER PUSH-UNTOUCHABLE PUT-ASSOC-EQ PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP QUOTE QUOTEP R-EQLABLE-ALISTP RASSOC RASSOC-EQ RASSOC-EQUAL RATIO RATIONAL RATIONAL-IMPLIES1 RATIONAL-IMPLIES2 RATIONAL-LISTP RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP RATIONALP RATIONALP-* RATIONALP-+ RATIONALP-EXPT-TYPE-PRESCRIPTION RATIONALP-IMPLIES-ACL2-NUMBERP RATIONALP-UNARY-- RATIONALP-UNARY-/ READ-ACL2-ORACLE READ-ACL2-ORACLE-PRESERVES-STATE-P1 READ-BYTE$ READ-CHAR$ READ-FILE-LISTP READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP READ-FILE-LISTP1 READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP READ-FILES READ-FILES-P READ-FILES-P-FORWARD-TO-READ-FILE-LISTP READ-IDATE READ-OBJECT READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1 READABLE-FILE READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP READABLE-FILES READABLE-FILES-LISTP READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP READABLE-FILES-P READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP REAL/RATIONALP REALFIX REALPART REALPART-COMPLEX REALPART-IMAGPART-ELIM REBUILD REDEF REDEF! REM REMOVE REMOVE-BINOP REMOVE-DEFAULT-HINTS REMOVE-DEFAULT-HINTS! REMOVE-DUPLICATES REMOVE-DUPLICATES-EQL REMOVE-DUPLICATES-EQUAL REMOVE-EQ REMOVE-EQUAL REMOVE-FIRST-PAIR REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-NTH-ALIAS REMOVE-UNTOUCHABLE REMOVE1 REMOVE1-EQ REMOVE1-EQUAL RESET-LD-SPECIALS RESET-PREHISTORY REST RETRACT-WORLD RETRIEVE REVAPPEND REVERSE RFIX ROUND SATISFIES SECOND SET-BACKCHAIN-LIMIT SET-BODY SET-BOGUS-MUTUAL-RECURSION-OK SET-CASE-SPLIT-LIMITATIONS SET-CBD SET-COMPILE-FNS SET-DEFAULT-HINTS SET-DEFAULT-HINTS! SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL SET-DIFFERENCE-THEORIES SET-ENFORCE-REDUNDANCY SET-EQUALP-EQUAL SET-GUARD-CHECKING SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST SET-INHIBIT-WARNINGS SET-INVISIBLE-FNS-TABLE SET-IRRELEVANT-FORMALS-OK SET-MEASURE-FUNCTION SET-NON-LINEARP SET-SAVED-OUTPUT SET-STATE-OK SET-TIMER SET-VERIFY-GUARDS-EAGERNESS SET-W SET-WELL-FOUNDED-RELATION SEVENTH SGETPROP SHOW-ACCUMULATED-PERSISTENCE SHOW-BDD SHOW-BODIES SHRINK-32-BIT-INTEGER-STACK SHRINK-T-STACK SIGNED-BYTE SIGNUM SIMPLIFY SIXTH SKIP-PROOFS SOME-SLASHABLE STABLE-UNDER-SIMPLIFICATIONP STANDARD-CHAR STANDARD-CHAR-LISTP STANDARD-CHAR-LISTP-APPEND STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP STANDARD-CHAR-P STANDARD-CHAR-P-NTH STANDARD-CO STANDARD-OI STANDARD-STRING-ALISTP STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP START-PROOF-TREE STATE STATE-GLOBAL-LET*-CLEANUP STATE-GLOBAL-LET*-GET-GLOBALS STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1 STATE-P1 STATE-P1-FORWARD STATE-P1-UPDATE-MAIN-TIMER STATE-P1-UPDATE-NTH-2-WORLD STOP-PROOF-TREE STRING STRING-APPEND STRING-APPEND-LST STRING-DOWNCASE STRING-DOWNCASE1 STRING-EQUAL STRING-EQUAL1 STRING-IS-NOT-CIRCULAR STRING-LISTP STRING-UPCASE STRING-UPCASE1 STRING< STRING<-IRREFLEXIVE STRING<-L STRING<-L-ASYMMETRIC STRING<-L-IRREFLEXIVE STRING<-L-TRANSITIVE STRING<-L-TRICHOTOMY STRING<= STRING> STRING>= STRINGP STRINGP-SYMBOL-PACKAGE-NAME STRIP-CARS STRIP-CDRS SUBLIS SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQUAL SUBST SUBSTITUTE SUBSTITUTE-AC SUMMARY SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP SYMBOL-DOUBLET-LISTP SYMBOL-EQUALITY SYMBOL-LISTP SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP SYMBOL-NAME SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL SYMBOL-PACKAGE-NAME SYMBOLP SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL SYNP SYNTAXP SYS-CALL SYS-CALL-STATUS T T-STACK T-STACK-LENGTH T-STACK-LENGTH1 TABLE TABLE-ALIST TAKE TENTH THE THE-ERROR THE-FIXNUM THE-FIXNUM! THEORY THEORY-INVARIANT THIRD THM TIME$ TIMER-ALISTP TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP TOGGLE-PC-MACRO TRACE$ TRANS TRANS1 TRICHOTOMY TRUE-LIST-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ TRUE-LISTP TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P TRUE-LISTP-UPDATE-NTH TRUNCATE TYPE TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP U UBT UBT! UNARY-- UNARY-/ UNARY-FUNCTION-SYMBOL-LISTP UNICITY-OF-0 UNICITY-OF-1 UNION-EQ UNION-EQUAL UNION-THEORIES UNIVERSAL-THEORY UNMONITOR UNSAVE UNSIGNED-BYTE UNTRACE$ UPDATE-32-BIT-INTEGER-STACK UPDATE-ACL2-ORACLE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1 UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK UPDATE-GLOBAL-TABLE UPDATE-IDATES UPDATE-LIST-ALL-PACKAGE-NAMES-LST UPDATE-NTH UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS UPDATE-READ-FILES UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST UPDATE-USER-STOBJ-ALIST1 UPDATE-WRITTEN-FILES UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P USER-STOBJ-ALIST USER-STOBJ-ALIST1 VALUE-TRIPLE VERBOSE-PSTACK VERIFY VERIFY-GUARDS VERIFY-TERMINATION W WARNING! WET WITH-OUTPUT WORLD WORLDP WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP WORMHOLE WORMHOLE1 WRITABLE-FILE-LISTP WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP WRITABLE-FILE-LISTP1 WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITE-BYTE$ WRITEABLE-FILES WRITEABLE-FILES-P WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP WRITTEN-FILE WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITTEN-FILE-LISTP WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP WRITTEN-FILES WRITTEN-FILES-P WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP XARGS XXXJOIN ZERO ZEROP ZIP ZP) '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH* &AUX *PRINT-PPRINT-DISPATCH* &BODY *PRINT-PRETTY* &ENVIRONMENT *PRINT-RADIX* &KEY *PRINT-READABLY* &OPTIONAL *PRINT-RIGHT-MARGIN* &REST *QUERY-IO* &WHOLE *RANDOM-STATE* * *READ-BASE* ** *READ-DEFAULT-FLOAT-FORMAT* *** *READ-EVAL* *BREAK-ON-SIGNALS* *READ-SUPPRESS* *COMPILE-FILE-PATHNAME* *READTABLE* *COMPILE-FILE-TRUENAME* *STANDARD-INPUT* *COMPILE-PRINT* *STANDARD-OUTPUT* *COMPILE-VERBOSE* *TERMINAL-IO* *DEBUG-IO* *TRACE-OUTPUT* *DEBUGGER-HOOK* + *DEFAULT-PATHNAME-DEFAULTS* ++ *ERROR-OUTPUT* +++ *FEATURES* - *GENSYM-COUNTER* / *LOAD-PATHNAME* // *LOAD-PRINT* /// *LOAD-TRUENAME* /= *LOAD-VERBOSE* 1+ *MACROEXPAND-HOOK* 1- *MODULES* < *PACKAGE* <= *PRINT-ARRAY* = *PRINT-BASE* > *PRINT-CASE* >= *PRINT-CIRCLE* ABORT *PRINT-ESCAPE* ABS *PRINT-GENSYM* ACONS *PRINT-LENGTH* ACOS *PRINT-LEVEL* ACOSH *PRINT-LINES* ADD-METHOD ADJOIN ATOM BOUNDP ADJUST-ARRAY BASE-CHAR BREAK ADJUSTABLE-ARRAY-P BASE-STRING BROADCAST-STREAM ALLOCATE-INSTANCE BIGNUM BROADCAST-STREAM-STREAMS ALPHA-CHAR-P BIT BUILT-IN-CLASS ALPHANUMERICP BIT-AND BUTLAST AND BIT-ANDC1 BYTE APPEND BIT-ANDC2 BYTE-POSITION APPLY BIT-EQV BYTE-SIZE APROPOS BIT-IOR CAAAAR APROPOS-LIST BIT-NAND CAAADR AREF BIT-NOR CAAAR ARITHMETIC-ERROR BIT-NOT CAADAR ARITHMETIC-ERROR-OPERANDS BIT-ORC1 CAADDR ARITHMETIC-ERROR-OPERATION BIT-ORC2 CAADR ARRAY BIT-VECTOR CAAR ARRAY-DIMENSION BIT-VECTOR-P CADAAR ARRAY-DIMENSION-LIMIT BIT-XOR CADADR ARRAY-DIMENSIONS BLOCK CADAR ARRAY-DISPLACEMENT BOOLE CADDAR ARRAY-ELEMENT-TYPE BOOLE-1 CADDDR ARRAY-HAS-FILL-POINTER-P BOOLE-2 CADDR ARRAY-IN-BOUNDS-P BOOLE-AND CADR ARRAY-RANK BOOLE-ANDC1 CALL-ARGUMENTS-LIMIT ARRAY-RANK-LIMIT BOOLE-ANDC2 CALL-METHOD ARRAY-ROW-MAJOR-INDEX BOOLE-C1 CALL-NEXT-METHOD ARRAY-TOTAL-SIZE BOOLE-C2 CAR ARRAY-TOTAL-SIZE-LIMIT BOOLE-CLR CASE ARRAYP BOOLE-EQV CATCH ASH BOOLE-IOR CCASE ASIN BOOLE-NAND CDAAAR ASINH BOOLE-NOR CDAADR ASSERT BOOLE-ORC1 CDAAR ASSOC BOOLE-ORC2 CDADAR ASSOC-IF BOOLE-SET CDADDR ASSOC-IF-NOT BOOLE-XOR CDADR ATAN BOOLEAN CDAR ATANH BOTH-CASE-P CDDAAR CDDADR CLEAR-INPUT COPY-TREE CDDAR CLEAR-OUTPUT COS CDDDAR CLOSE COSH CDDDDR CLRHASH COUNT CDDDR CODE-CHAR COUNT-IF CDDR COERCE COUNT-IF-NOT CDR COMPILATION-SPEED CTYPECASE CEILING COMPILE DEBUG CELL-ERROR COMPILE-FILE DECF CELL-ERROR-NAME COMPILE-FILE-PATHNAME DECLAIM CERROR COMPILED-FUNCTION DECLARATION CHANGE-CLASS COMPILED-FUNCTION-P DECLARE CHAR COMPILER-MACRO DECODE-FLOAT CHAR-CODE COMPILER-MACRO-FUNCTION DECODE-UNIVERSAL-TIME CHAR-CODE-LIMIT COMPLEMENT DEFCLASS CHAR-DOWNCASE COMPLEX DEFCONSTANT CHAR-EQUAL COMPLEXP DEFGENERIC CHAR-GREATERP COMPUTE-APPLICABLE-METHODS DEFINE-COMPILER-MACRO CHAR-INT COMPUTE-RESTARTS DEFINE-CONDITION CHAR-LESSP CONCATENATE DEFINE-METHOD-COMBINATION CHAR-NAME CONCATENATED-STREAM DEFINE-MODIFY-MACRO CHAR-NOT-EQUAL CONCATENATED-STREAM-STREAMS DEFINE-SETF-EXPANDER CHAR-NOT-GREATERP COND DEFINE-SYMBOL-MACRO CHAR-NOT-LESSP CONDITION DEFMACRO CHAR-UPCASE CONJUGATE DEFMETHOD CHAR/= CONS DEFPACKAGE CHAR< CONSP DEFPARAMETER CHAR<= CONSTANTLY DEFSETF CHAR= CONSTANTP DEFSTRUCT CHAR> CONTINUE DEFTYPE CHAR>= CONTROL-ERROR DEFUN CHARACTER COPY-ALIST DEFVAR CHARACTERP COPY-LIST DELETE CHECK-TYPE COPY-PPRINT-DISPATCH DELETE-DUPLICATES CIS COPY-READTABLE DELETE-FILE CLASS COPY-SEQ DELETE-IF CLASS-NAME COPY-STRUCTURE DELETE-IF-NOT CLASS-OF COPY-SYMBOL DELETE-PACKAGE DENOMINATOR EQ DEPOSIT-FIELD EQL DESCRIBE EQUAL DESCRIBE-OBJECT EQUALP DESTRUCTURING-BIND ERROR DIGIT-CHAR ETYPECASE DIGIT-CHAR-P EVAL DIRECTORY EVAL-WHEN DIRECTORY-NAMESTRING EVENP DISASSEMBLE EVERY DIVISION-BY-ZERO EXP DO EXPORT DO* EXPT DO-ALL-SYMBOLS EXTENDED-CHAR DO-EXTERNAL-SYMBOLS FBOUNDP DO-SYMBOLS FCEILING DOCUMENTATION FDEFINITION DOLIST FFLOOR DOTIMES FIFTH DOUBLE-FLOAT FILE-AUTHOR DOUBLE-FLOAT-EPSILON FILE-ERROR DOUBLE-FLOAT-NEGATIVE-EPSILON FILE-ERROR-PATHNAME DPB FILE-LENGTH DRIBBLE FILE-NAMESTRING DYNAMIC-EXTENT FILE-POSITION ECASE FILE-STREAM ECHO-STREAM FILE-STRING-LENGTH ECHO-STREAM-INPUT-STREAM FILE-WRITE-DATE ECHO-STREAM-OUTPUT-STREAM FILL ED FILL-POINTER EIGHTH FIND ELT FIND-ALL-SYMBOLS ENCODE-UNIVERSAL-TIME FIND-CLASS END-OF-FILE FIND-IF ENDP FIND-IF-NOT ENOUGH-NAMESTRING FIND-METHOD ENSURE-DIRECTORIES-EXIST FIND-PACKAGE ENSURE-GENERIC-FUNCTION FIND-RESTART FIND-SYMBOL GET-INTERNAL-RUN-TIME FINISH-OUTPUT GET-MACRO-CHARACTER FIRST GET-OUTPUT-STREAM-STRING FIXNUM GET-PROPERTIES FLET GET-SETF-EXPANSION FLOAT GET-UNIVERSAL-TIME FLOAT-DIGITS GETF FLOAT-PRECISION GETHASH FLOAT-RADIX GO FLOAT-SIGN GRAPHIC-CHAR-P FLOATING-POINT-INEXACT HANDLER-BIND FLOATING-POINT-INVALID-OPERATION HANDLER-CASE FLOATING-POINT-OVERFLOW HASH-TABLE FLOATING-POINT-UNDERFLOW HASH-TABLE-COUNT FLOATP HASH-TABLE-P FLOOR HASH-TABLE-REHASH-SIZE FMAKUNBOUND HASH-TABLE-REHASH-THRESHOLD FORCE-OUTPUT HASH-TABLE-SIZE FORMAT HASH-TABLE-TEST FORMATTER HOST-NAMESTRING FOURTH IDENTITY FRESH-LINE IF FROUND IGNORABLE FTRUNCATE IGNORE FTYPE IGNORE-ERRORS FUNCALL IMAGPART FUNCTION IMPORT FUNCTION-KEYWORDS IN-PACKAGE FUNCTION-LAMBDA-EXPRESSION INCF FUNCTIONP INITIALIZE-INSTANCE GCD INLINE GENERIC-FUNCTION INPUT-STREAM-P GENSYM INSPECT GENTEMP INTEGER GET INTEGER-DECODE-FLOAT GET-DECODED-TIME INTEGER-LENGTH GET-DISPATCH-MACRO-CHARACTER INTEGERP GET-INTERNAL-REAL-TIME INTERACTIVE-STREAM-P INTERN LISP-IMPLEMENTATION-TYPE INTERNAL-TIME-UNITS-PER-SECOND LISP-IMPLEMENTATION-VERSION INTERSECTION LIST INVALID-METHOD-ERROR LIST* INVOKE-DEBUGGER LIST-ALL-PACKAGES INVOKE-RESTART LIST-LENGTH INVOKE-RESTART-INTERACTIVELY LISTEN ISQRT LISTP KEYWORD LOAD KEYWORDP LOAD-LOGICAL-PATHNAME-TRANSLATIONS LABELS LOAD-TIME-VALUE LAMBDA LOCALLY LAMBDA-LIST-KEYWORDS LOG LAMBDA-PARAMETERS-LIMIT LOGAND LAST LOGANDC1 LCM LOGANDC2 LDB LOGBITP LDB-TEST LOGCOUNT LDIFF LOGEQV LEAST-NEGATIVE-DOUBLE-FLOAT LOGICAL-PATHNAME LEAST-NEGATIVE-LONG-FLOAT LOGICAL-PATHNAME-TRANSLATIONS LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT LOGIOR LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT LOGNAND LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT LOGNOR LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT LOGNOT LEAST-NEGATIVE-SHORT-FLOAT LOGORC1 LEAST-NEGATIVE-SINGLE-FLOAT LOGORC2 LEAST-POSITIVE-DOUBLE-FLOAT LOGTEST LEAST-POSITIVE-LONG-FLOAT LOGXOR LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT LONG-FLOAT LEAST-POSITIVE-NORMALIZED-LONG-FLOAT LONG-FLOAT-EPSILON LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT LONG-FLOAT-NEGATIVE-EPSILON LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT LONG-SITE-NAME LEAST-POSITIVE-SHORT-FLOAT LOOP LEAST-POSITIVE-SINGLE-FLOAT LOOP-FINISH LENGTH LOWER-CASE-P LET MACHINE-INSTANCE LET* MACHINE-TYPE MACHINE-VERSION MASK-FIELD MACRO-FUNCTION MAX MACROEXPAND MEMBER MACROEXPAND-1 MEMBER-IF MACROLET MEMBER-IF-NOT MAKE-ARRAY MERGE MAKE-BROADCAST-STREAM MERGE-PATHNAMES MAKE-CONCATENATED-STREAM METHOD MAKE-CONDITION METHOD-COMBINATION MAKE-DISPATCH-MACRO-CHARACTER METHOD-COMBINATION-ERROR MAKE-ECHO-STREAM METHOD-QUALIFIERS MAKE-HASH-TABLE MIN MAKE-INSTANCE MINUSP MAKE-INSTANCES-OBSOLETE MISMATCH MAKE-LIST MOD MAKE-LOAD-FORM MOST-NEGATIVE-DOUBLE-FLOAT MAKE-LOAD-FORM-SAVING-SLOTS MOST-NEGATIVE-FIXNUM MAKE-METHOD MOST-NEGATIVE-LONG-FLOAT MAKE-PACKAGE MOST-NEGATIVE-SHORT-FLOAT MAKE-PATHNAME MOST-NEGATIVE-SINGLE-FLOAT MAKE-RANDOM-STATE MOST-POSITIVE-DOUBLE-FLOAT MAKE-SEQUENCE MOST-POSITIVE-FIXNUM MAKE-STRING MOST-POSITIVE-LONG-FLOAT MAKE-STRING-INPUT-STREAM MOST-POSITIVE-SHORT-FLOAT MAKE-STRING-OUTPUT-STREAM MOST-POSITIVE-SINGLE-FLOAT MAKE-SYMBOL MUFFLE-WARNING MAKE-SYNONYM-STREAM MULTIPLE-VALUE-BIND MAKE-TWO-WAY-STREAM MULTIPLE-VALUE-CALL MAKUNBOUND MULTIPLE-VALUE-LIST MAP MULTIPLE-VALUE-PROG1 MAP-INTO MULTIPLE-VALUE-SETQ MAPC MULTIPLE-VALUES-LIMIT MAPCAN NAME-CHAR MAPCAR NAMESTRING MAPCON NBUTLAST MAPHASH NCONC MAPL NEXT-METHOD-P MAPLIST NIL NINTERSECTION PACKAGE-ERROR NINTH PACKAGE-ERROR-PACKAGE NO-APPLICABLE-METHOD PACKAGE-NAME NO-NEXT-METHOD PACKAGE-NICKNAMES NOT PACKAGE-SHADOWING-SYMBOLS NOTANY PACKAGE-USE-LIST NOTEVERY PACKAGE-USED-BY-LIST NOTINLINE PACKAGEP NRECONC PAIRLIS NREVERSE PARSE-ERROR NSET-DIFFERENCE PARSE-INTEGER NSET-EXCLUSIVE-OR PARSE-NAMESTRING NSTRING-CAPITALIZE PATHNAME NSTRING-DOWNCASE PATHNAME-DEVICE NSTRING-UPCASE PATHNAME-DIRECTORY NSUBLIS PATHNAME-HOST NSUBST PATHNAME-MATCH-P NSUBST-IF PATHNAME-NAME NSUBST-IF-NOT PATHNAME-TYPE NSUBSTITUTE PATHNAME-VERSION NSUBSTITUTE-IF PATHNAMEP NSUBSTITUTE-IF-NOT PEEK-CHAR NTH PHASE NTH-VALUE PI NTHCDR PLUSP NULL POP NUMBER POSITION NUMBERP POSITION-IF NUMERATOR POSITION-IF-NOT NUNION PPRINT ODDP PPRINT-DISPATCH OPEN PPRINT-EXIT-IF-LIST-EXHAUSTED OPEN-STREAM-P PPRINT-FILL OPTIMIZE PPRINT-INDENT OR PPRINT-LINEAR OTHERWISE PPRINT-LOGICAL-BLOCK OUTPUT-STREAM-P PPRINT-NEWLINE PACKAGE PPRINT-POP PPRINT-TAB READ-CHAR PPRINT-TABULAR READ-CHAR-NO-HANG PRIN1 READ-DELIMITED-LIST PRIN1-TO-STRING READ-FROM-STRING PRINC READ-LINE PRINC-TO-STRING READ-PRESERVING-WHITESPACE PRINT READ-SEQUENCE PRINT-NOT-READABLE READER-ERROR PRINT-NOT-READABLE-OBJECT READTABLE PRINT-OBJECT READTABLE-CASE PRINT-UNREADABLE-OBJECT READTABLEP PROBE-FILE REAL PROCLAIM REALP PROG REALPART PROG* REDUCE PROG1 REINITIALIZE-INSTANCE PROG2 REM PROGN REMF PROGRAM-ERROR REMHASH PROGV REMOVE PROVIDE REMOVE-DUPLICATES PSETF REMOVE-IF PSETQ REMOVE-IF-NOT PUSH REMOVE-METHOD PUSHNEW REMPROP QUOTE RENAME-FILE RANDOM RENAME-PACKAGE RANDOM-STATE REPLACE RANDOM-STATE-P REQUIRE RASSOC REST RASSOC-IF RESTART RASSOC-IF-NOT RESTART-BIND RATIO RESTART-CASE RATIONAL RESTART-NAME RATIONALIZE RETURN RATIONALP RETURN-FROM READ REVAPPEND READ-BYTE REVERSE ROOM SIMPLE-BIT-VECTOR ROTATEF SIMPLE-BIT-VECTOR-P ROUND SIMPLE-CONDITION ROW-MAJOR-AREF SIMPLE-CONDITION-FORMAT-ARGUMENTS RPLACA SIMPLE-CONDITION-FORMAT-CONTROL RPLACD SIMPLE-ERROR SAFETY SIMPLE-STRING SATISFIES SIMPLE-STRING-P SBIT SIMPLE-TYPE-ERROR SCALE-FLOAT SIMPLE-VECTOR SCHAR SIMPLE-VECTOR-P SEARCH SIMPLE-WARNING SECOND SIN SEQUENCE SINGLE-FLOAT SERIOUS-CONDITION SINGLE-FLOAT-EPSILON SET SINGLE-FLOAT-NEGATIVE-EPSILON SET-DIFFERENCE SINH SET-DISPATCH-MACRO-CHARACTER SIXTH SET-EXCLUSIVE-OR SLEEP SET-MACRO-CHARACTER SLOT-BOUNDP SET-PPRINT-DISPATCH SLOT-EXISTS-P SET-SYNTAX-FROM-CHAR SLOT-MAKUNBOUND SETF SLOT-MISSING SETQ SLOT-UNBOUND SEVENTH SLOT-VALUE SHADOW SOFTWARE-TYPE SHADOWING-IMPORT SOFTWARE-VERSION SHARED-INITIALIZE SOME SHIFTF SORT SHORT-FLOAT SPACE SHORT-FLOAT-EPSILON SPECIAL SHORT-FLOAT-NEGATIVE-EPSILON SPECIAL-OPERATOR-P SHORT-SITE-NAME SPEED SIGNAL SQRT SIGNED-BYTE STABLE-SORT SIGNUM STANDARD SIMPLE-ARRAY STANDARD-CHAR SIMPLE-BASE-STRING STANDARD-CHAR-P STANDARD-CLASS SUBLIS STANDARD-GENERIC-FUNCTION SUBSEQ STANDARD-METHOD SUBSETP STANDARD-OBJECT SUBST STEP SUBST-IF STORAGE-CONDITION SUBST-IF-NOT STORE-VALUE SUBSTITUTE STREAM SUBSTITUTE-IF STREAM-ELEMENT-TYPE SUBSTITUTE-IF-NOT STREAM-ERROR SUBTYPEP STREAM-ERROR-STREAM SVREF STREAM-EXTERNAL-FORMAT SXHASH STREAMP SYMBOL STRING SYMBOL-FUNCTION STRING-CAPITALIZE SYMBOL-MACROLET STRING-DOWNCASE SYMBOL-NAME STRING-EQUAL SYMBOL-PACKAGE STRING-GREATERP SYMBOL-PLIST STRING-LEFT-TRIM SYMBOL-VALUE STRING-LESSP SYMBOLP STRING-NOT-EQUAL SYNONYM-STREAM STRING-NOT-GREATERP SYNONYM-STREAM-SYMBOL STRING-NOT-LESSP T STRING-RIGHT-TRIM TAGBODY STRING-STREAM TAILP STRING-TRIM TAN STRING-UPCASE TANH STRING/= TENTH STRING< TERPRI STRING<= THE STRING= THIRD STRING> THROW STRING>= TIME STRINGP TRACE STRUCTURE TRANSLATE-LOGICAL-PATHNAME STRUCTURE-CLASS TRANSLATE-PATHNAME STRUCTURE-OBJECT TREE-EQUAL STYLE-WARNING TRUENAME TRUNCATE VALUES-LIST TWO-WAY-STREAM VARIABLE TWO-WAY-STREAM-INPUT-STREAM VECTOR TWO-WAY-STREAM-OUTPUT-STREAM VECTOR-POP TYPE VECTOR-PUSH TYPE-ERROR VECTOR-PUSH-EXTEND TYPE-ERROR-DATUM VECTORP TYPE-ERROR-EXPECTED-TYPE WARN TYPE-OF WARNING TYPECASE WHEN TYPEP WILD-PATHNAME-P UNBOUND-SLOT WITH-ACCESSORS UNBOUND-SLOT-INSTANCE WITH-COMPILATION-UNIT UNBOUND-VARIABLE WITH-CONDITION-RESTARTS UNDEFINED-FUNCTION WITH-HASH-TABLE-ITERATOR UNEXPORT WITH-INPUT-FROM-STRING UNINTERN WITH-OPEN-FILE UNION WITH-OPEN-STREAM UNLESS WITH-OUTPUT-TO-STRING UNREAD-CHAR WITH-PACKAGE-ITERATOR UNSIGNED-BYTE WITH-SIMPLE-RESTART UNTRACE WITH-SLOTS UNUSE-PACKAGE WITH-STANDARD-IO-SYNTAX UNWIND-PROTECT WRITE UPDATE-INSTANCE-FOR-DIFFERENT-CLASS WRITE-BYTE UPDATE-INSTANCE-FOR-REDEFINED-CLASS WRITE-CHAR UPGRADED-ARRAY-ELEMENT-TYPE WRITE-LINE UPGRADED-COMPLEX-PART-TYPE WRITE-SEQUENCE UPPER-CASE-P WRITE-STRING USE-PACKAGE WRITE-TO-STRING USE-VALUE Y-OR-N-P USER-HOMEDIR-PATHNAME YES-OR-NO-P VALUES ZEROP)) '(ZERO)) NIL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/math-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp")) (DEFPKG "ACL2-AGP" (SET-DIFFERENCE-EQUAL (UNION-EQ '(& &ALLOW-OTHER-KEYS &AUX &BODY &KEY &OPTIONAL &REST &WHOLE * *ACL2-EXPORTS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *MAIN-LISP-PACKAGE-NAME* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-OI* + - / /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP AND AND-MACRO APPEND AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP-GLOBAL BOUNDP-GLOBAL1 BRR BRR@ BUILD-STATE1 BUTLAST CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CBD CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CERTIFY-BOOK CERTIFY-BOOK! CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-UPCASE CHAR< CHAR<= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CLAUSE CLEAR-HASH-TABLES CLEAR-MEMOIZE-TABLES CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSURE CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 CONCATENATE COND COND-CLAUSESP COND-MACRO CONJUGATE CONS CONS-EQUAL CONSP CONSP-ASSOC CONSP-ASSOC-EQ CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DECLARE DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCONG DEFCONST DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFLABEL DEFMACRO DEFPKG DEFREFINEMENT DEFSTOBJ DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFUN DEFUN-SK DEFUND DEFUNS DELETE-PAIR DENOMINATOR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DISABLE DISABLE-FORCING DISABLEDP DISTRIBUTIVITY DOC DOC! DOCS DOUBLE-REWRITE DUPLICATES E/D E0-ORD-< E0-ORDINALP EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ENABLE ENABLE-FORCING ENCAPSULATE ENDP EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE ER ER-PROGN ER-PROGN-FN EVENP EVENS EVENT EXECUTABLE-COUNTERPART-THEORY EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD FERTILIZE FGETPROP FIFTH FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FIRST FIRST-N-AC FIX FIX-TRUE-LIST FLOOR FLUSH-HONS-GET-HASH-TABLE-LINK FMS FMT FMT-TO-COMMENT-WINDOW FMT1 FORCE FOURTH FUNCTION-SYMBOLP FUNCTION-THEORY GENERALIZE GET-GLOBAL GET-TIMER GETPROP-DEFAULT GETPROPS GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS GLOBAL-TABLE-CARS1 GLOBAL-VAL GOOD-BYE GOOD-DEFUN-MODE-P GROUND-ZERO HARD-ERROR HAS-PROPSP HAS-PROPSP1 HEADER HELP HIDE HONS HONS-ACONS HONS-ACONS! HONS-COPY HONS-EQUAL HONS-GET HONS-GET-FN-DO-HOPY HONS-GET-FN-DO-NOT-HOPY HONS-LET HONS-READ-OBJECT HONS-SHRINK-ALIST HONS-SHRINK-ALIST! I-AM-HERE ID IDATES IDENTITY IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1 IFF-IMPLIES-EQUAL-IMPLIES-2 IFF-IMPLIES-EQUAL-NOT IFF-IS-AN-EQUIVALENCE IFIX IGNORE ILLEGAL IMAGPART IMAGPART-COMPLEX IMMEDIATE-FORCE-MODEP IMPLIES IMPROPER-CONSP IN-ARITHMETIC-THEORY IN-PACKAGE IN-THEORY INCLUDE-BOOK INCOMPATIBLE INCREMENT-TIMER INDUCT INIT-HASH-TABLES INIT-HONS-ACONS-TABLE INT= INTEGER INTEGER-0 INTEGER-1 INTEGER-ABS INTEGER-IMPLIES-RATIONAL INTEGER-LENGTH INTEGER-LISTP INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP INTEGER-STEP INTEGERP INTERN INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME INTERSECTION-EQ INTERSECTION-THEORIES INTERSECTP-EQ INTERSECTP-EQUAL INVERSE-OF-* INVERSE-OF-+ INVISIBLE-FNS-TABLE KEYWORD-PACKAGE KEYWORD-VALUE-LISTP KEYWORD-VALUE-LISTP-ASSOC-KEYWORD KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP LAMBDA LAST LD LD-ERROR-ACTION LD-ERROR-TRIPLES LD-KEYWORD-ALIASES LD-POST-EVAL-PRINT LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT LD-PROMPT LD-QUERY-CONTROL-ALIST LD-REDEFINITION-ACTION LD-SKIP-PROOFSP LD-VERBOSE LEGAL-CASE-CLAUSESP LEN LEN-UPDATE-NTH LENGTH LET* LIST LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES LIST-ALL-PACKAGE-NAMES-LST LIST-MACRO LISTP LOCAL LOGAND LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT LOGEQV LOGIC LOGIOR LOGNAND LOGNOR LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P LOWEST-TERMS LP MACRO-ALIASES MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION MAKE-CHARACTER-LIST MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST MAKE-EVENT MAKE-FMT-BINDINGS MAKE-INPUT-CHANNEL MAKE-LIST MAKE-LIST-AC MAKE-MV-NTHS MAKE-ORD MAKE-OUTPUT-CHANNEL MAKE-VAR-LST MAKE-VAR-LST1 MAKUNBOUND-GLOBAL MAX MAXIMUM-LENGTH MAY-NEED-SLASHES MBE MBT MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-SYMBOL-NAME MEMOIZE-LET MEMOIZE-OFF MEMOIZE-ON MFC MIN MINIMAL-THEORY MINUSP MOD MONITOR MONITORED-RUNES MORE MORE! MORE-DOC MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP MV MV-LET MV-NTH NATP NEWLINE NFIX NIL NIL-IS-NOT-CIRCULAR NINTH NO-DUPLICATESP NO-DUPLICATESP-EQUAL NONNEGATIVE-INTEGER-QUOTIENT NONNEGATIVE-PRODUCT NONZERO-IMAGPART NOT NQTHM-TO-ACL2 NTH NTH-0-CONS NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION NTH-ADD1 NTH-ALIASES NTH-UPDATE-NTH NTHCDR NULL NUMERATOR O-FINP O-FIRST-COEFF O-FIRST-EXPT O-INFP O-P O-RST O< O<= O> O>= OBSERVATION ODDP ODDS OK-IF OOPS OPEN-CHANNEL-LISTP OPEN-CHANNEL1 OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD OPEN-INPUT-CHANNEL OPEN-INPUT-CHANNEL-ANY-P OPEN-INPUT-CHANNEL-ANY-P1 OPEN-INPUT-CHANNEL-P OPEN-INPUT-CHANNEL-P1 OPEN-INPUT-CHANNELS OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL! OPEN-OUTPUT-CHANNEL-ANY-P OPEN-OUTPUT-CHANNEL-ANY-P1 OPEN-OUTPUT-CHANNEL-P OPEN-OUTPUT-CHANNEL-P1 OPEN-OUTPUT-CHANNELS OR OR-MACRO ORDERED-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-ADD-PAIR ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-GETPROPS ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR OTHERWISE OUR-DIGIT-CHAR-P PAIRLIS$ PAIRLIS2 PBT PC PCB PCB! PCS PE PEEK-CHAR$ PF PL PLEV0 PLUSP POP-TIMER POSITION POSITION-AC POSITION-EQ POSITION-EQ-AC POSITION-EQUAL POSITION-EQUAL-AC POSITIVE POSP POWER-EVAL PPROGN PR PR! PREPROCESS PRIN1$ PRIN1-WITH-SLASHES PRIN1-WITH-SLASHES1 PRINC$ PRINT-OBJECT$ PRINT-RATIONAL-AS-DECIMAL PRINT-TIMER PROG2$ PROGN PROGRAM PROOF-TREE PROOFS-CO PROPER-CONSP PROPS PROVE PSEUDO-TERM-LISTP PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP PSEUDO-TERMP PSTACK PUFF PUFF* PUSH-TIMER PUSH-UNTOUCHABLE PUT-ASSOC-EQ PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP QUOTE QUOTEP R-EQLABLE-ALISTP RASSOC RASSOC-EQ RASSOC-EQUAL RATIO RATIONAL RATIONAL-IMPLIES1 RATIONAL-IMPLIES2 RATIONAL-LISTP RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP RATIONALP RATIONALP-* RATIONALP-+ RATIONALP-EXPT-TYPE-PRESCRIPTION RATIONALP-IMPLIES-ACL2-NUMBERP RATIONALP-UNARY-- RATIONALP-UNARY-/ READ-ACL2-ORACLE READ-ACL2-ORACLE-PRESERVES-STATE-P1 READ-BYTE$ READ-CHAR$ READ-FILE-LISTP READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP READ-FILE-LISTP1 READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP READ-FILES READ-FILES-P READ-FILES-P-FORWARD-TO-READ-FILE-LISTP READ-IDATE READ-OBJECT READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1 READABLE-FILE READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP READABLE-FILES READABLE-FILES-LISTP READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP READABLE-FILES-P READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP REAL/RATIONALP REALFIX REALPART REALPART-COMPLEX REALPART-IMAGPART-ELIM REBUILD REDEF REDEF! REM REMOVE REMOVE-BINOP REMOVE-DEFAULT-HINTS REMOVE-DEFAULT-HINTS! REMOVE-DUPLICATES REMOVE-DUPLICATES-EQL REMOVE-DUPLICATES-EQUAL REMOVE-EQ REMOVE-EQUAL REMOVE-FIRST-PAIR REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-NTH-ALIAS REMOVE-UNTOUCHABLE REMOVE1 REMOVE1-EQ REMOVE1-EQUAL RESET-LD-SPECIALS RESET-PREHISTORY REST RETRACT-WORLD RETRIEVE REVAPPEND REVERSE RFIX ROUND SATISFIES SECOND SET-BACKCHAIN-LIMIT SET-BODY SET-BOGUS-MUTUAL-RECURSION-OK SET-CASE-SPLIT-LIMITATIONS SET-CBD SET-COMPILE-FNS SET-DEFAULT-HINTS SET-DEFAULT-HINTS! SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL SET-DIFFERENCE-THEORIES SET-ENFORCE-REDUNDANCY SET-EQUALP-EQUAL SET-GUARD-CHECKING SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST SET-INHIBIT-WARNINGS SET-INVISIBLE-FNS-TABLE SET-IRRELEVANT-FORMALS-OK SET-MEASURE-FUNCTION SET-NON-LINEARP SET-SAVED-OUTPUT SET-STATE-OK SET-TIMER SET-VERIFY-GUARDS-EAGERNESS SET-W SET-WELL-FOUNDED-RELATION SEVENTH SGETPROP SHOW-ACCUMULATED-PERSISTENCE SHOW-BDD SHOW-BODIES SHRINK-32-BIT-INTEGER-STACK SHRINK-T-STACK SIGNED-BYTE SIGNUM SIMPLIFY SIXTH SKIP-PROOFS SOME-SLASHABLE STABLE-UNDER-SIMPLIFICATIONP STANDARD-CHAR STANDARD-CHAR-LISTP STANDARD-CHAR-LISTP-APPEND STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP STANDARD-CHAR-P STANDARD-CHAR-P-NTH STANDARD-CO STANDARD-OI STANDARD-STRING-ALISTP STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP START-PROOF-TREE STATE STATE-GLOBAL-LET*-CLEANUP STATE-GLOBAL-LET*-GET-GLOBALS STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1 STATE-P1 STATE-P1-FORWARD STATE-P1-UPDATE-MAIN-TIMER STATE-P1-UPDATE-NTH-2-WORLD STOP-PROOF-TREE STRING STRING-APPEND STRING-APPEND-LST STRING-DOWNCASE STRING-DOWNCASE1 STRING-EQUAL STRING-EQUAL1 STRING-IS-NOT-CIRCULAR STRING-LISTP STRING-UPCASE STRING-UPCASE1 STRING< STRING<-IRREFLEXIVE STRING<-L STRING<-L-ASYMMETRIC STRING<-L-IRREFLEXIVE STRING<-L-TRANSITIVE STRING<-L-TRICHOTOMY STRING<= STRING> STRING>= STRINGP STRINGP-SYMBOL-PACKAGE-NAME STRIP-CARS STRIP-CDRS SUBLIS SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQUAL SUBST SUBSTITUTE SUBSTITUTE-AC SUMMARY SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP SYMBOL-DOUBLET-LISTP SYMBOL-EQUALITY SYMBOL-LISTP SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP SYMBOL-NAME SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL SYMBOL-PACKAGE-NAME SYMBOLP SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL SYNP SYNTAXP SYS-CALL SYS-CALL-STATUS T T-STACK T-STACK-LENGTH T-STACK-LENGTH1 TABLE TABLE-ALIST TAKE TENTH THE THE-ERROR THE-FIXNUM THE-FIXNUM! THEORY THEORY-INVARIANT THIRD THM TIME$ TIMER-ALISTP TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP TOGGLE-PC-MACRO TRACE$ TRANS TRANS1 TRICHOTOMY TRUE-LIST-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ TRUE-LISTP TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P TRUE-LISTP-UPDATE-NTH TRUNCATE TYPE TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP U UBT UBT! UNARY-- UNARY-/ UNARY-FUNCTION-SYMBOL-LISTP UNICITY-OF-0 UNICITY-OF-1 UNION-EQ UNION-EQUAL UNION-THEORIES UNIVERSAL-THEORY UNMONITOR UNSAVE UNSIGNED-BYTE UNTRACE$ UPDATE-32-BIT-INTEGER-STACK UPDATE-ACL2-ORACLE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1 UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK UPDATE-GLOBAL-TABLE UPDATE-IDATES UPDATE-LIST-ALL-PACKAGE-NAMES-LST UPDATE-NTH UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS UPDATE-READ-FILES UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST UPDATE-USER-STOBJ-ALIST1 UPDATE-WRITTEN-FILES UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P USER-STOBJ-ALIST USER-STOBJ-ALIST1 VALUE-TRIPLE VERBOSE-PSTACK VERIFY VERIFY-GUARDS VERIFY-TERMINATION W WARNING! WET WITH-OUTPUT WORLD WORLDP WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP WORMHOLE WORMHOLE1 WRITABLE-FILE-LISTP WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP WRITABLE-FILE-LISTP1 WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITE-BYTE$ WRITEABLE-FILES WRITEABLE-FILES-P WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP WRITTEN-FILE WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITTEN-FILE-LISTP WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP WRITTEN-FILES WRITTEN-FILES-P WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP XARGS XXXJOIN ZERO ZEROP ZIP ZP) '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH* &AUX *PRINT-PPRINT-DISPATCH* &BODY *PRINT-PRETTY* &ENVIRONMENT *PRINT-RADIX* &KEY *PRINT-READABLY* &OPTIONAL *PRINT-RIGHT-MARGIN* &REST *QUERY-IO* &WHOLE *RANDOM-STATE* * *READ-BASE* ** *READ-DEFAULT-FLOAT-FORMAT* *** *READ-EVAL* *BREAK-ON-SIGNALS* *READ-SUPPRESS* *COMPILE-FILE-PATHNAME* *READTABLE* *COMPILE-FILE-TRUENAME* *STANDARD-INPUT* *COMPILE-PRINT* *STANDARD-OUTPUT* *COMPILE-VERBOSE* *TERMINAL-IO* *DEBUG-IO* *TRACE-OUTPUT* *DEBUGGER-HOOK* + *DEFAULT-PATHNAME-DEFAULTS* ++ *ERROR-OUTPUT* +++ *FEATURES* - *GENSYM-COUNTER* / *LOAD-PATHNAME* // *LOAD-PRINT* /// *LOAD-TRUENAME* /= *LOAD-VERBOSE* 1+ *MACROEXPAND-HOOK* 1- *MODULES* < *PACKAGE* <= *PRINT-ARRAY* = *PRINT-BASE* > *PRINT-CASE* >= *PRINT-CIRCLE* ABORT *PRINT-ESCAPE* ABS *PRINT-GENSYM* ACONS *PRINT-LENGTH* ACOS *PRINT-LEVEL* ACOSH *PRINT-LINES* ADD-METHOD ADJOIN ATOM BOUNDP ADJUST-ARRAY BASE-CHAR BREAK ADJUSTABLE-ARRAY-P BASE-STRING BROADCAST-STREAM ALLOCATE-INSTANCE BIGNUM BROADCAST-STREAM-STREAMS ALPHA-CHAR-P BIT BUILT-IN-CLASS ALPHANUMERICP BIT-AND BUTLAST AND BIT-ANDC1 BYTE APPEND BIT-ANDC2 BYTE-POSITION APPLY BIT-EQV BYTE-SIZE APROPOS BIT-IOR CAAAAR APROPOS-LIST BIT-NAND CAAADR AREF BIT-NOR CAAAR ARITHMETIC-ERROR BIT-NOT CAADAR ARITHMETIC-ERROR-OPERANDS BIT-ORC1 CAADDR ARITHMETIC-ERROR-OPERATION BIT-ORC2 CAADR ARRAY BIT-VECTOR CAAR ARRAY-DIMENSION BIT-VECTOR-P CADAAR ARRAY-DIMENSION-LIMIT BIT-XOR CADADR ARRAY-DIMENSIONS BLOCK CADAR ARRAY-DISPLACEMENT BOOLE CADDAR ARRAY-ELEMENT-TYPE BOOLE-1 CADDDR ARRAY-HAS-FILL-POINTER-P BOOLE-2 CADDR ARRAY-IN-BOUNDS-P BOOLE-AND CADR ARRAY-RANK BOOLE-ANDC1 CALL-ARGUMENTS-LIMIT ARRAY-RANK-LIMIT BOOLE-ANDC2 CALL-METHOD ARRAY-ROW-MAJOR-INDEX BOOLE-C1 CALL-NEXT-METHOD ARRAY-TOTAL-SIZE BOOLE-C2 CAR ARRAY-TOTAL-SIZE-LIMIT BOOLE-CLR CASE ARRAYP BOOLE-EQV CATCH ASH BOOLE-IOR CCASE ASIN BOOLE-NAND CDAAAR ASINH BOOLE-NOR CDAADR ASSERT BOOLE-ORC1 CDAAR ASSOC BOOLE-ORC2 CDADAR ASSOC-IF BOOLE-SET CDADDR ASSOC-IF-NOT BOOLE-XOR CDADR ATAN BOOLEAN CDAR ATANH BOTH-CASE-P CDDAAR CDDADR CLEAR-INPUT COPY-TREE CDDAR CLEAR-OUTPUT COS CDDDAR CLOSE COSH CDDDDR CLRHASH COUNT CDDDR CODE-CHAR COUNT-IF CDDR COERCE COUNT-IF-NOT CDR COMPILATION-SPEED CTYPECASE CEILING COMPILE DEBUG CELL-ERROR COMPILE-FILE DECF CELL-ERROR-NAME COMPILE-FILE-PATHNAME DECLAIM CERROR COMPILED-FUNCTION DECLARATION CHANGE-CLASS COMPILED-FUNCTION-P DECLARE CHAR COMPILER-MACRO DECODE-FLOAT CHAR-CODE COMPILER-MACRO-FUNCTION DECODE-UNIVERSAL-TIME CHAR-CODE-LIMIT COMPLEMENT DEFCLASS CHAR-DOWNCASE COMPLEX DEFCONSTANT CHAR-EQUAL COMPLEXP DEFGENERIC CHAR-GREATERP COMPUTE-APPLICABLE-METHODS DEFINE-COMPILER-MACRO CHAR-INT COMPUTE-RESTARTS DEFINE-CONDITION CHAR-LESSP CONCATENATE DEFINE-METHOD-COMBINATION CHAR-NAME CONCATENATED-STREAM DEFINE-MODIFY-MACRO CHAR-NOT-EQUAL CONCATENATED-STREAM-STREAMS DEFINE-SETF-EXPANDER CHAR-NOT-GREATERP COND DEFINE-SYMBOL-MACRO CHAR-NOT-LESSP CONDITION DEFMACRO CHAR-UPCASE CONJUGATE DEFMETHOD CHAR/= CONS DEFPACKAGE CHAR< CONSP DEFPARAMETER CHAR<= CONSTANTLY DEFSETF CHAR= CONSTANTP DEFSTRUCT CHAR> CONTINUE DEFTYPE CHAR>= CONTROL-ERROR DEFUN CHARACTER COPY-ALIST DEFVAR CHARACTERP COPY-LIST DELETE CHECK-TYPE COPY-PPRINT-DISPATCH DELETE-DUPLICATES CIS COPY-READTABLE DELETE-FILE CLASS COPY-SEQ DELETE-IF CLASS-NAME COPY-STRUCTURE DELETE-IF-NOT CLASS-OF COPY-SYMBOL DELETE-PACKAGE DENOMINATOR EQ DEPOSIT-FIELD EQL DESCRIBE EQUAL DESCRIBE-OBJECT EQUALP DESTRUCTURING-BIND ERROR DIGIT-CHAR ETYPECASE DIGIT-CHAR-P EVAL DIRECTORY EVAL-WHEN DIRECTORY-NAMESTRING EVENP DISASSEMBLE EVERY DIVISION-BY-ZERO EXP DO EXPORT DO* EXPT DO-ALL-SYMBOLS EXTENDED-CHAR DO-EXTERNAL-SYMBOLS FBOUNDP DO-SYMBOLS FCEILING DOCUMENTATION FDEFINITION DOLIST FFLOOR DOTIMES FIFTH DOUBLE-FLOAT FILE-AUTHOR DOUBLE-FLOAT-EPSILON FILE-ERROR DOUBLE-FLOAT-NEGATIVE-EPSILON FILE-ERROR-PATHNAME DPB FILE-LENGTH DRIBBLE FILE-NAMESTRING DYNAMIC-EXTENT FILE-POSITION ECASE FILE-STREAM ECHO-STREAM FILE-STRING-LENGTH ECHO-STREAM-INPUT-STREAM FILE-WRITE-DATE ECHO-STREAM-OUTPUT-STREAM FILL ED FILL-POINTER EIGHTH FIND ELT FIND-ALL-SYMBOLS ENCODE-UNIVERSAL-TIME FIND-CLASS END-OF-FILE FIND-IF ENDP FIND-IF-NOT ENOUGH-NAMESTRING FIND-METHOD ENSURE-DIRECTORIES-EXIST FIND-PACKAGE ENSURE-GENERIC-FUNCTION FIND-RESTART FIND-SYMBOL GET-INTERNAL-RUN-TIME FINISH-OUTPUT GET-MACRO-CHARACTER FIRST GET-OUTPUT-STREAM-STRING FIXNUM GET-PROPERTIES FLET GET-SETF-EXPANSION FLOAT GET-UNIVERSAL-TIME FLOAT-DIGITS GETF FLOAT-PRECISION GETHASH FLOAT-RADIX GO FLOAT-SIGN GRAPHIC-CHAR-P FLOATING-POINT-INEXACT HANDLER-BIND FLOATING-POINT-INVALID-OPERATION HANDLER-CASE FLOATING-POINT-OVERFLOW HASH-TABLE FLOATING-POINT-UNDERFLOW HASH-TABLE-COUNT FLOATP HASH-TABLE-P FLOOR HASH-TABLE-REHASH-SIZE FMAKUNBOUND HASH-TABLE-REHASH-THRESHOLD FORCE-OUTPUT HASH-TABLE-SIZE FORMAT HASH-TABLE-TEST FORMATTER HOST-NAMESTRING FOURTH IDENTITY FRESH-LINE IF FROUND IGNORABLE FTRUNCATE IGNORE FTYPE IGNORE-ERRORS FUNCALL IMAGPART FUNCTION IMPORT FUNCTION-KEYWORDS IN-PACKAGE FUNCTION-LAMBDA-EXPRESSION INCF FUNCTIONP INITIALIZE-INSTANCE GCD INLINE GENERIC-FUNCTION INPUT-STREAM-P GENSYM INSPECT GENTEMP INTEGER GET INTEGER-DECODE-FLOAT GET-DECODED-TIME INTEGER-LENGTH GET-DISPATCH-MACRO-CHARACTER INTEGERP GET-INTERNAL-REAL-TIME INTERACTIVE-STREAM-P INTERN LISP-IMPLEMENTATION-TYPE INTERNAL-TIME-UNITS-PER-SECOND LISP-IMPLEMENTATION-VERSION INTERSECTION LIST INVALID-METHOD-ERROR LIST* INVOKE-DEBUGGER LIST-ALL-PACKAGES INVOKE-RESTART LIST-LENGTH INVOKE-RESTART-INTERACTIVELY LISTEN ISQRT LISTP KEYWORD LOAD KEYWORDP LOAD-LOGICAL-PATHNAME-TRANSLATIONS LABELS LOAD-TIME-VALUE LAMBDA LOCALLY LAMBDA-LIST-KEYWORDS LOG LAMBDA-PARAMETERS-LIMIT LOGAND LAST LOGANDC1 LCM LOGANDC2 LDB LOGBITP LDB-TEST LOGCOUNT LDIFF LOGEQV LEAST-NEGATIVE-DOUBLE-FLOAT LOGICAL-PATHNAME LEAST-NEGATIVE-LONG-FLOAT LOGICAL-PATHNAME-TRANSLATIONS LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT LOGIOR LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT LOGNAND LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT LOGNOR LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT LOGNOT LEAST-NEGATIVE-SHORT-FLOAT LOGORC1 LEAST-NEGATIVE-SINGLE-FLOAT LOGORC2 LEAST-POSITIVE-DOUBLE-FLOAT LOGTEST LEAST-POSITIVE-LONG-FLOAT LOGXOR LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT LONG-FLOAT LEAST-POSITIVE-NORMALIZED-LONG-FLOAT LONG-FLOAT-EPSILON LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT LONG-FLOAT-NEGATIVE-EPSILON LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT LONG-SITE-NAME LEAST-POSITIVE-SHORT-FLOAT LOOP LEAST-POSITIVE-SINGLE-FLOAT LOOP-FINISH LENGTH LOWER-CASE-P LET MACHINE-INSTANCE LET* MACHINE-TYPE MACHINE-VERSION MASK-FIELD MACRO-FUNCTION MAX MACROEXPAND MEMBER MACROEXPAND-1 MEMBER-IF MACROLET MEMBER-IF-NOT MAKE-ARRAY MERGE MAKE-BROADCAST-STREAM MERGE-PATHNAMES MAKE-CONCATENATED-STREAM METHOD MAKE-CONDITION METHOD-COMBINATION MAKE-DISPATCH-MACRO-CHARACTER METHOD-COMBINATION-ERROR MAKE-ECHO-STREAM METHOD-QUALIFIERS MAKE-HASH-TABLE MIN MAKE-INSTANCE MINUSP MAKE-INSTANCES-OBSOLETE MISMATCH MAKE-LIST MOD MAKE-LOAD-FORM MOST-NEGATIVE-DOUBLE-FLOAT MAKE-LOAD-FORM-SAVING-SLOTS MOST-NEGATIVE-FIXNUM MAKE-METHOD MOST-NEGATIVE-LONG-FLOAT MAKE-PACKAGE MOST-NEGATIVE-SHORT-FLOAT MAKE-PATHNAME MOST-NEGATIVE-SINGLE-FLOAT MAKE-RANDOM-STATE MOST-POSITIVE-DOUBLE-FLOAT MAKE-SEQUENCE MOST-POSITIVE-FIXNUM MAKE-STRING MOST-POSITIVE-LONG-FLOAT MAKE-STRING-INPUT-STREAM MOST-POSITIVE-SHORT-FLOAT MAKE-STRING-OUTPUT-STREAM MOST-POSITIVE-SINGLE-FLOAT MAKE-SYMBOL MUFFLE-WARNING MAKE-SYNONYM-STREAM MULTIPLE-VALUE-BIND MAKE-TWO-WAY-STREAM MULTIPLE-VALUE-CALL MAKUNBOUND MULTIPLE-VALUE-LIST MAP MULTIPLE-VALUE-PROG1 MAP-INTO MULTIPLE-VALUE-SETQ MAPC MULTIPLE-VALUES-LIMIT MAPCAN NAME-CHAR MAPCAR NAMESTRING MAPCON NBUTLAST MAPHASH NCONC MAPL NEXT-METHOD-P MAPLIST NIL NINTERSECTION PACKAGE-ERROR NINTH PACKAGE-ERROR-PACKAGE NO-APPLICABLE-METHOD PACKAGE-NAME NO-NEXT-METHOD PACKAGE-NICKNAMES NOT PACKAGE-SHADOWING-SYMBOLS NOTANY PACKAGE-USE-LIST NOTEVERY PACKAGE-USED-BY-LIST NOTINLINE PACKAGEP NRECONC PAIRLIS NREVERSE PARSE-ERROR NSET-DIFFERENCE PARSE-INTEGER NSET-EXCLUSIVE-OR PARSE-NAMESTRING NSTRING-CAPITALIZE PATHNAME NSTRING-DOWNCASE PATHNAME-DEVICE NSTRING-UPCASE PATHNAME-DIRECTORY NSUBLIS PATHNAME-HOST NSUBST PATHNAME-MATCH-P NSUBST-IF PATHNAME-NAME NSUBST-IF-NOT PATHNAME-TYPE NSUBSTITUTE PATHNAME-VERSION NSUBSTITUTE-IF PATHNAMEP NSUBSTITUTE-IF-NOT PEEK-CHAR NTH PHASE NTH-VALUE PI NTHCDR PLUSP NULL POP NUMBER POSITION NUMBERP POSITION-IF NUMERATOR POSITION-IF-NOT NUNION PPRINT ODDP PPRINT-DISPATCH OPEN PPRINT-EXIT-IF-LIST-EXHAUSTED OPEN-STREAM-P PPRINT-FILL OPTIMIZE PPRINT-INDENT OR PPRINT-LINEAR OTHERWISE PPRINT-LOGICAL-BLOCK OUTPUT-STREAM-P PPRINT-NEWLINE PACKAGE PPRINT-POP PPRINT-TAB READ-CHAR PPRINT-TABULAR READ-CHAR-NO-HANG PRIN1 READ-DELIMITED-LIST PRIN1-TO-STRING READ-FROM-STRING PRINC READ-LINE PRINC-TO-STRING READ-PRESERVING-WHITESPACE PRINT READ-SEQUENCE PRINT-NOT-READABLE READER-ERROR PRINT-NOT-READABLE-OBJECT READTABLE PRINT-OBJECT READTABLE-CASE PRINT-UNREADABLE-OBJECT READTABLEP PROBE-FILE REAL PROCLAIM REALP PROG REALPART PROG* REDUCE PROG1 REINITIALIZE-INSTANCE PROG2 REM PROGN REMF PROGRAM-ERROR REMHASH PROGV REMOVE PROVIDE REMOVE-DUPLICATES PSETF REMOVE-IF PSETQ REMOVE-IF-NOT PUSH REMOVE-METHOD PUSHNEW REMPROP QUOTE RENAME-FILE RANDOM RENAME-PACKAGE RANDOM-STATE REPLACE RANDOM-STATE-P REQUIRE RASSOC REST RASSOC-IF RESTART RASSOC-IF-NOT RESTART-BIND RATIO RESTART-CASE RATIONAL RESTART-NAME RATIONALIZE RETURN RATIONALP RETURN-FROM READ REVAPPEND READ-BYTE REVERSE ROOM SIMPLE-BIT-VECTOR ROTATEF SIMPLE-BIT-VECTOR-P ROUND SIMPLE-CONDITION ROW-MAJOR-AREF SIMPLE-CONDITION-FORMAT-ARGUMENTS RPLACA SIMPLE-CONDITION-FORMAT-CONTROL RPLACD SIMPLE-ERROR SAFETY SIMPLE-STRING SATISFIES SIMPLE-STRING-P SBIT SIMPLE-TYPE-ERROR SCALE-FLOAT SIMPLE-VECTOR SCHAR SIMPLE-VECTOR-P SEARCH SIMPLE-WARNING SECOND SIN SEQUENCE SINGLE-FLOAT SERIOUS-CONDITION SINGLE-FLOAT-EPSILON SET SINGLE-FLOAT-NEGATIVE-EPSILON SET-DIFFERENCE SINH SET-DISPATCH-MACRO-CHARACTER SIXTH SET-EXCLUSIVE-OR SLEEP SET-MACRO-CHARACTER SLOT-BOUNDP SET-PPRINT-DISPATCH SLOT-EXISTS-P SET-SYNTAX-FROM-CHAR SLOT-MAKUNBOUND SETF SLOT-MISSING SETQ SLOT-UNBOUND SEVENTH SLOT-VALUE SHADOW SOFTWARE-TYPE SHADOWING-IMPORT SOFTWARE-VERSION SHARED-INITIALIZE SOME SHIFTF SORT SHORT-FLOAT SPACE SHORT-FLOAT-EPSILON SPECIAL SHORT-FLOAT-NEGATIVE-EPSILON SPECIAL-OPERATOR-P SHORT-SITE-NAME SPEED SIGNAL SQRT SIGNED-BYTE STABLE-SORT SIGNUM STANDARD SIMPLE-ARRAY STANDARD-CHAR SIMPLE-BASE-STRING STANDARD-CHAR-P STANDARD-CLASS SUBLIS STANDARD-GENERIC-FUNCTION SUBSEQ STANDARD-METHOD SUBSETP STANDARD-OBJECT SUBST STEP SUBST-IF STORAGE-CONDITION SUBST-IF-NOT STORE-VALUE SUBSTITUTE STREAM SUBSTITUTE-IF STREAM-ELEMENT-TYPE SUBSTITUTE-IF-NOT STREAM-ERROR SUBTYPEP STREAM-ERROR-STREAM SVREF STREAM-EXTERNAL-FORMAT SXHASH STREAMP SYMBOL STRING SYMBOL-FUNCTION STRING-CAPITALIZE SYMBOL-MACROLET STRING-DOWNCASE SYMBOL-NAME STRING-EQUAL SYMBOL-PACKAGE STRING-GREATERP SYMBOL-PLIST STRING-LEFT-TRIM SYMBOL-VALUE STRING-LESSP SYMBOLP STRING-NOT-EQUAL SYNONYM-STREAM STRING-NOT-GREATERP SYNONYM-STREAM-SYMBOL STRING-NOT-LESSP T STRING-RIGHT-TRIM TAGBODY STRING-STREAM TAILP STRING-TRIM TAN STRING-UPCASE TANH STRING/= TENTH STRING< TERPRI STRING<= THE STRING= THIRD STRING> THROW STRING>= TIME STRINGP TRACE STRUCTURE TRANSLATE-LOGICAL-PATHNAME STRUCTURE-CLASS TRANSLATE-PATHNAME STRUCTURE-OBJECT TREE-EQUAL STYLE-WARNING TRUENAME TRUNCATE VALUES-LIST TWO-WAY-STREAM VARIABLE TWO-WAY-STREAM-INPUT-STREAM VECTOR TWO-WAY-STREAM-OUTPUT-STREAM VECTOR-POP TYPE VECTOR-PUSH TYPE-ERROR VECTOR-PUSH-EXTEND TYPE-ERROR-DATUM VECTORP TYPE-ERROR-EXPECTED-TYPE WARN TYPE-OF WARNING TYPECASE WHEN TYPEP WILD-PATHNAME-P UNBOUND-SLOT WITH-ACCESSORS UNBOUND-SLOT-INSTANCE WITH-COMPILATION-UNIT UNBOUND-VARIABLE WITH-CONDITION-RESTARTS UNDEFINED-FUNCTION WITH-HASH-TABLE-ITERATOR UNEXPORT WITH-INPUT-FROM-STRING UNINTERN WITH-OPEN-FILE UNION WITH-OPEN-STREAM UNLESS WITH-OUTPUT-TO-STRING UNREAD-CHAR WITH-PACKAGE-ITERATOR UNSIGNED-BYTE WITH-SIMPLE-RESTART UNTRACE WITH-SLOTS UNUSE-PACKAGE WITH-STANDARD-IO-SYNTAX UNWIND-PROTECT WRITE UPDATE-INSTANCE-FOR-DIFFERENT-CLASS WRITE-BYTE UPDATE-INSTANCE-FOR-REDEFINED-CLASS WRITE-CHAR UPGRADED-ARRAY-ELEMENT-TYPE WRITE-LINE UPGRADED-COMPLEX-PART-TYPE WRITE-SEQUENCE UPPER-CASE-P WRITE-STRING USE-PACKAGE WRITE-TO-STRING USE-VALUE Y-OR-N-P USER-HOMEDIR-PATHNAME YES-OR-NO-P VALUES ZEROP)) '(ZERO)) NIL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/math-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp")) (DEFPKG "ACL2-CRG" (SET-DIFFERENCE-EQUAL (UNION-EQ '(& &ALLOW-OTHER-KEYS &AUX &BODY &KEY &OPTIONAL &REST &WHOLE * *ACL2-EXPORTS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *MAIN-LISP-PACKAGE-NAME* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-OI* + - / /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP AND AND-MACRO APPEND AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP-GLOBAL BOUNDP-GLOBAL1 BRR BRR@ BUILD-STATE1 BUTLAST CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CBD CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CERTIFY-BOOK CERTIFY-BOOK! CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-UPCASE CHAR< CHAR<= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CLAUSE CLEAR-HASH-TABLES CLEAR-MEMOIZE-TABLES CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSURE CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 CONCATENATE COND COND-CLAUSESP COND-MACRO CONJUGATE CONS CONS-EQUAL CONSP CONSP-ASSOC CONSP-ASSOC-EQ CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DECLARE DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCONG DEFCONST DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFLABEL DEFMACRO DEFPKG DEFREFINEMENT DEFSTOBJ DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFUN DEFUN-SK DEFUND DEFUNS DELETE-PAIR DENOMINATOR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DISABLE DISABLE-FORCING DISABLEDP DISTRIBUTIVITY DOC DOC! DOCS DOUBLE-REWRITE DUPLICATES E/D E0-ORD-< E0-ORDINALP EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ENABLE ENABLE-FORCING ENCAPSULATE ENDP EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE ER ER-PROGN ER-PROGN-FN EVENP EVENS EVENT EXECUTABLE-COUNTERPART-THEORY EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD FERTILIZE FGETPROP FIFTH FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FIRST FIRST-N-AC FIX FIX-TRUE-LIST FLOOR FLUSH-HONS-GET-HASH-TABLE-LINK FMS FMT FMT-TO-COMMENT-WINDOW FMT1 FORCE FOURTH FUNCTION-SYMBOLP FUNCTION-THEORY GENERALIZE GET-GLOBAL GET-TIMER GETPROP-DEFAULT GETPROPS GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS GLOBAL-TABLE-CARS1 GLOBAL-VAL GOOD-BYE GOOD-DEFUN-MODE-P GROUND-ZERO HARD-ERROR HAS-PROPSP HAS-PROPSP1 HEADER HELP HIDE HONS HONS-ACONS HONS-ACONS! HONS-COPY HONS-EQUAL HONS-GET HONS-GET-FN-DO-HOPY HONS-GET-FN-DO-NOT-HOPY HONS-LET HONS-READ-OBJECT HONS-SHRINK-ALIST HONS-SHRINK-ALIST! I-AM-HERE ID IDATES IDENTITY IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1 IFF-IMPLIES-EQUAL-IMPLIES-2 IFF-IMPLIES-EQUAL-NOT IFF-IS-AN-EQUIVALENCE IFIX IGNORE ILLEGAL IMAGPART IMAGPART-COMPLEX IMMEDIATE-FORCE-MODEP IMPLIES IMPROPER-CONSP IN-ARITHMETIC-THEORY IN-PACKAGE IN-THEORY INCLUDE-BOOK INCOMPATIBLE INCREMENT-TIMER INDUCT INIT-HASH-TABLES INIT-HONS-ACONS-TABLE INT= INTEGER INTEGER-0 INTEGER-1 INTEGER-ABS INTEGER-IMPLIES-RATIONAL INTEGER-LENGTH INTEGER-LISTP INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP INTEGER-STEP INTEGERP INTERN INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME INTERSECTION-EQ INTERSECTION-THEORIES INTERSECTP-EQ INTERSECTP-EQUAL INVERSE-OF-* INVERSE-OF-+ INVISIBLE-FNS-TABLE KEYWORD-PACKAGE KEYWORD-VALUE-LISTP KEYWORD-VALUE-LISTP-ASSOC-KEYWORD KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP LAMBDA LAST LD LD-ERROR-ACTION LD-ERROR-TRIPLES LD-KEYWORD-ALIASES LD-POST-EVAL-PRINT LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT LD-PROMPT LD-QUERY-CONTROL-ALIST LD-REDEFINITION-ACTION LD-SKIP-PROOFSP LD-VERBOSE LEGAL-CASE-CLAUSESP LEN LEN-UPDATE-NTH LENGTH LET* LIST LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES LIST-ALL-PACKAGE-NAMES-LST LIST-MACRO LISTP LOCAL LOGAND LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT LOGEQV LOGIC LOGIOR LOGNAND LOGNOR LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P LOWEST-TERMS LP MACRO-ALIASES MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION MAKE-CHARACTER-LIST MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST MAKE-EVENT MAKE-FMT-BINDINGS MAKE-INPUT-CHANNEL MAKE-LIST MAKE-LIST-AC MAKE-MV-NTHS MAKE-ORD MAKE-OUTPUT-CHANNEL MAKE-VAR-LST MAKE-VAR-LST1 MAKUNBOUND-GLOBAL MAX MAXIMUM-LENGTH MAY-NEED-SLASHES MBE MBT MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-SYMBOL-NAME MEMOIZE-LET MEMOIZE-OFF MEMOIZE-ON MFC MIN MINIMAL-THEORY MINUSP MOD MONITOR MONITORED-RUNES MORE MORE! MORE-DOC MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP MV MV-LET MV-NTH NATP NEWLINE NFIX NIL NIL-IS-NOT-CIRCULAR NINTH NO-DUPLICATESP NO-DUPLICATESP-EQUAL NONNEGATIVE-INTEGER-QUOTIENT NONNEGATIVE-PRODUCT NONZERO-IMAGPART NOT NQTHM-TO-ACL2 NTH NTH-0-CONS NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION NTH-ADD1 NTH-ALIASES NTH-UPDATE-NTH NTHCDR NULL NUMERATOR O-FINP O-FIRST-COEFF O-FIRST-EXPT O-INFP O-P O-RST O< O<= O> O>= OBSERVATION ODDP ODDS OK-IF OOPS OPEN-CHANNEL-LISTP OPEN-CHANNEL1 OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD OPEN-INPUT-CHANNEL OPEN-INPUT-CHANNEL-ANY-P OPEN-INPUT-CHANNEL-ANY-P1 OPEN-INPUT-CHANNEL-P OPEN-INPUT-CHANNEL-P1 OPEN-INPUT-CHANNELS OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL! OPEN-OUTPUT-CHANNEL-ANY-P OPEN-OUTPUT-CHANNEL-ANY-P1 OPEN-OUTPUT-CHANNEL-P OPEN-OUTPUT-CHANNEL-P1 OPEN-OUTPUT-CHANNELS OR OR-MACRO ORDERED-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-ADD-PAIR ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-GETPROPS ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR OTHERWISE OUR-DIGIT-CHAR-P PAIRLIS$ PAIRLIS2 PBT PC PCB PCB! PCS PE PEEK-CHAR$ PF PL PLEV0 PLUSP POP-TIMER POSITION POSITION-AC POSITION-EQ POSITION-EQ-AC POSITION-EQUAL POSITION-EQUAL-AC POSITIVE POSP POWER-EVAL PPROGN PR PR! PREPROCESS PRIN1$ PRIN1-WITH-SLASHES PRIN1-WITH-SLASHES1 PRINC$ PRINT-OBJECT$ PRINT-RATIONAL-AS-DECIMAL PRINT-TIMER PROG2$ PROGN PROGRAM PROOF-TREE PROOFS-CO PROPER-CONSP PROPS PROVE PSEUDO-TERM-LISTP PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP PSEUDO-TERMP PSTACK PUFF PUFF* PUSH-TIMER PUSH-UNTOUCHABLE PUT-ASSOC-EQ PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP QUOTE QUOTEP R-EQLABLE-ALISTP RASSOC RASSOC-EQ RASSOC-EQUAL RATIO RATIONAL RATIONAL-IMPLIES1 RATIONAL-IMPLIES2 RATIONAL-LISTP RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP RATIONALP RATIONALP-* RATIONALP-+ RATIONALP-EXPT-TYPE-PRESCRIPTION RATIONALP-IMPLIES-ACL2-NUMBERP RATIONALP-UNARY-- RATIONALP-UNARY-/ READ-ACL2-ORACLE READ-ACL2-ORACLE-PRESERVES-STATE-P1 READ-BYTE$ READ-CHAR$ READ-FILE-LISTP READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP READ-FILE-LISTP1 READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP READ-FILES READ-FILES-P READ-FILES-P-FORWARD-TO-READ-FILE-LISTP READ-IDATE READ-OBJECT READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1 READABLE-FILE READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP READABLE-FILES READABLE-FILES-LISTP READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP READABLE-FILES-P READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP REAL/RATIONALP REALFIX REALPART REALPART-COMPLEX REALPART-IMAGPART-ELIM REBUILD REDEF REDEF! REM REMOVE REMOVE-BINOP REMOVE-DEFAULT-HINTS REMOVE-DEFAULT-HINTS! REMOVE-DUPLICATES REMOVE-DUPLICATES-EQL REMOVE-DUPLICATES-EQUAL REMOVE-EQ REMOVE-EQUAL REMOVE-FIRST-PAIR REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-NTH-ALIAS REMOVE-UNTOUCHABLE REMOVE1 REMOVE1-EQ REMOVE1-EQUAL RESET-LD-SPECIALS RESET-PREHISTORY REST RETRACT-WORLD RETRIEVE REVAPPEND REVERSE RFIX ROUND SATISFIES SECOND SET-BACKCHAIN-LIMIT SET-BODY SET-BOGUS-MUTUAL-RECURSION-OK SET-CASE-SPLIT-LIMITATIONS SET-CBD SET-COMPILE-FNS SET-DEFAULT-HINTS SET-DEFAULT-HINTS! SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL SET-DIFFERENCE-THEORIES SET-ENFORCE-REDUNDANCY SET-EQUALP-EQUAL SET-GUARD-CHECKING SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST SET-INHIBIT-WARNINGS SET-INVISIBLE-FNS-TABLE SET-IRRELEVANT-FORMALS-OK SET-MEASURE-FUNCTION SET-NON-LINEARP SET-SAVED-OUTPUT SET-STATE-OK SET-TIMER SET-VERIFY-GUARDS-EAGERNESS SET-W SET-WELL-FOUNDED-RELATION SEVENTH SGETPROP SHOW-ACCUMULATED-PERSISTENCE SHOW-BDD SHOW-BODIES SHRINK-32-BIT-INTEGER-STACK SHRINK-T-STACK SIGNED-BYTE SIGNUM SIMPLIFY SIXTH SKIP-PROOFS SOME-SLASHABLE STABLE-UNDER-SIMPLIFICATIONP STANDARD-CHAR STANDARD-CHAR-LISTP STANDARD-CHAR-LISTP-APPEND STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP STANDARD-CHAR-P STANDARD-CHAR-P-NTH STANDARD-CO STANDARD-OI STANDARD-STRING-ALISTP STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP START-PROOF-TREE STATE STATE-GLOBAL-LET*-CLEANUP STATE-GLOBAL-LET*-GET-GLOBALS STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1 STATE-P1 STATE-P1-FORWARD STATE-P1-UPDATE-MAIN-TIMER STATE-P1-UPDATE-NTH-2-WORLD STOP-PROOF-TREE STRING STRING-APPEND STRING-APPEND-LST STRING-DOWNCASE STRING-DOWNCASE1 STRING-EQUAL STRING-EQUAL1 STRING-IS-NOT-CIRCULAR STRING-LISTP STRING-UPCASE STRING-UPCASE1 STRING< STRING<-IRREFLEXIVE STRING<-L STRING<-L-ASYMMETRIC STRING<-L-IRREFLEXIVE STRING<-L-TRANSITIVE STRING<-L-TRICHOTOMY STRING<= STRING> STRING>= STRINGP STRINGP-SYMBOL-PACKAGE-NAME STRIP-CARS STRIP-CDRS SUBLIS SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQUAL SUBST SUBSTITUTE SUBSTITUTE-AC SUMMARY SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP SYMBOL-DOUBLET-LISTP SYMBOL-EQUALITY SYMBOL-LISTP SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP SYMBOL-NAME SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL SYMBOL-PACKAGE-NAME SYMBOLP SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL SYNP SYNTAXP SYS-CALL SYS-CALL-STATUS T T-STACK T-STACK-LENGTH T-STACK-LENGTH1 TABLE TABLE-ALIST TAKE TENTH THE THE-ERROR THE-FIXNUM THE-FIXNUM! THEORY THEORY-INVARIANT THIRD THM TIME$ TIMER-ALISTP TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP TOGGLE-PC-MACRO TRACE$ TRANS TRANS1 TRICHOTOMY TRUE-LIST-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ TRUE-LISTP TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P TRUE-LISTP-UPDATE-NTH TRUNCATE TYPE TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP U UBT UBT! UNARY-- UNARY-/ UNARY-FUNCTION-SYMBOL-LISTP UNICITY-OF-0 UNICITY-OF-1 UNION-EQ UNION-EQUAL UNION-THEORIES UNIVERSAL-THEORY UNMONITOR UNSAVE UNSIGNED-BYTE UNTRACE$ UPDATE-32-BIT-INTEGER-STACK UPDATE-ACL2-ORACLE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1 UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK UPDATE-GLOBAL-TABLE UPDATE-IDATES UPDATE-LIST-ALL-PACKAGE-NAMES-LST UPDATE-NTH UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS UPDATE-READ-FILES UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST UPDATE-USER-STOBJ-ALIST1 UPDATE-WRITTEN-FILES UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P USER-STOBJ-ALIST USER-STOBJ-ALIST1 VALUE-TRIPLE VERBOSE-PSTACK VERIFY VERIFY-GUARDS VERIFY-TERMINATION W WARNING! WET WITH-OUTPUT WORLD WORLDP WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP WORMHOLE WORMHOLE1 WRITABLE-FILE-LISTP WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP WRITABLE-FILE-LISTP1 WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITE-BYTE$ WRITEABLE-FILES WRITEABLE-FILES-P WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP WRITTEN-FILE WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITTEN-FILE-LISTP WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP WRITTEN-FILES WRITTEN-FILES-P WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP XARGS XXXJOIN ZERO ZEROP ZIP ZP) '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH* &AUX *PRINT-PPRINT-DISPATCH* &BODY *PRINT-PRETTY* &ENVIRONMENT *PRINT-RADIX* &KEY *PRINT-READABLY* &OPTIONAL *PRINT-RIGHT-MARGIN* &REST *QUERY-IO* &WHOLE *RANDOM-STATE* * *READ-BASE* ** *READ-DEFAULT-FLOAT-FORMAT* *** *READ-EVAL* *BREAK-ON-SIGNALS* *READ-SUPPRESS* *COMPILE-FILE-PATHNAME* *READTABLE* *COMPILE-FILE-TRUENAME* *STANDARD-INPUT* *COMPILE-PRINT* *STANDARD-OUTPUT* *COMPILE-VERBOSE* *TERMINAL-IO* *DEBUG-IO* *TRACE-OUTPUT* *DEBUGGER-HOOK* + *DEFAULT-PATHNAME-DEFAULTS* ++ *ERROR-OUTPUT* +++ *FEATURES* - *GENSYM-COUNTER* / *LOAD-PATHNAME* // *LOAD-PRINT* /// *LOAD-TRUENAME* /= *LOAD-VERBOSE* 1+ *MACROEXPAND-HOOK* 1- *MODULES* < *PACKAGE* <= *PRINT-ARRAY* = *PRINT-BASE* > *PRINT-CASE* >= *PRINT-CIRCLE* ABORT *PRINT-ESCAPE* ABS *PRINT-GENSYM* ACONS *PRINT-LENGTH* ACOS *PRINT-LEVEL* ACOSH *PRINT-LINES* ADD-METHOD ADJOIN ATOM BOUNDP ADJUST-ARRAY BASE-CHAR BREAK ADJUSTABLE-ARRAY-P BASE-STRING BROADCAST-STREAM ALLOCATE-INSTANCE BIGNUM BROADCAST-STREAM-STREAMS ALPHA-CHAR-P BIT BUILT-IN-CLASS ALPHANUMERICP BIT-AND BUTLAST AND BIT-ANDC1 BYTE APPEND BIT-ANDC2 BYTE-POSITION APPLY BIT-EQV BYTE-SIZE APROPOS BIT-IOR CAAAAR APROPOS-LIST BIT-NAND CAAADR AREF BIT-NOR CAAAR ARITHMETIC-ERROR BIT-NOT CAADAR ARITHMETIC-ERROR-OPERANDS BIT-ORC1 CAADDR ARITHMETIC-ERROR-OPERATION BIT-ORC2 CAADR ARRAY BIT-VECTOR CAAR ARRAY-DIMENSION BIT-VECTOR-P CADAAR ARRAY-DIMENSION-LIMIT BIT-XOR CADADR ARRAY-DIMENSIONS BLOCK CADAR ARRAY-DISPLACEMENT BOOLE CADDAR ARRAY-ELEMENT-TYPE BOOLE-1 CADDDR ARRAY-HAS-FILL-POINTER-P BOOLE-2 CADDR ARRAY-IN-BOUNDS-P BOOLE-AND CADR ARRAY-RANK BOOLE-ANDC1 CALL-ARGUMENTS-LIMIT ARRAY-RANK-LIMIT BOOLE-ANDC2 CALL-METHOD ARRAY-ROW-MAJOR-INDEX BOOLE-C1 CALL-NEXT-METHOD ARRAY-TOTAL-SIZE BOOLE-C2 CAR ARRAY-TOTAL-SIZE-LIMIT BOOLE-CLR CASE ARRAYP BOOLE-EQV CATCH ASH BOOLE-IOR CCASE ASIN BOOLE-NAND CDAAAR ASINH BOOLE-NOR CDAADR ASSERT BOOLE-ORC1 CDAAR ASSOC BOOLE-ORC2 CDADAR ASSOC-IF BOOLE-SET CDADDR ASSOC-IF-NOT BOOLE-XOR CDADR ATAN BOOLEAN CDAR ATANH BOTH-CASE-P CDDAAR CDDADR CLEAR-INPUT COPY-TREE CDDAR CLEAR-OUTPUT COS CDDDAR CLOSE COSH CDDDDR CLRHASH COUNT CDDDR CODE-CHAR COUNT-IF CDDR COERCE COUNT-IF-NOT CDR COMPILATION-SPEED CTYPECASE CEILING COMPILE DEBUG CELL-ERROR COMPILE-FILE DECF CELL-ERROR-NAME COMPILE-FILE-PATHNAME DECLAIM CERROR COMPILED-FUNCTION DECLARATION CHANGE-CLASS COMPILED-FUNCTION-P DECLARE CHAR COMPILER-MACRO DECODE-FLOAT CHAR-CODE COMPILER-MACRO-FUNCTION DECODE-UNIVERSAL-TIME CHAR-CODE-LIMIT COMPLEMENT DEFCLASS CHAR-DOWNCASE COMPLEX DEFCONSTANT CHAR-EQUAL COMPLEXP DEFGENERIC CHAR-GREATERP COMPUTE-APPLICABLE-METHODS DEFINE-COMPILER-MACRO CHAR-INT COMPUTE-RESTARTS DEFINE-CONDITION CHAR-LESSP CONCATENATE DEFINE-METHOD-COMBINATION CHAR-NAME CONCATENATED-STREAM DEFINE-MODIFY-MACRO CHAR-NOT-EQUAL CONCATENATED-STREAM-STREAMS DEFINE-SETF-EXPANDER CHAR-NOT-GREATERP COND DEFINE-SYMBOL-MACRO CHAR-NOT-LESSP CONDITION DEFMACRO CHAR-UPCASE CONJUGATE DEFMETHOD CHAR/= CONS DEFPACKAGE CHAR< CONSP DEFPARAMETER CHAR<= CONSTANTLY DEFSETF CHAR= CONSTANTP DEFSTRUCT CHAR> CONTINUE DEFTYPE CHAR>= CONTROL-ERROR DEFUN CHARACTER COPY-ALIST DEFVAR CHARACTERP COPY-LIST DELETE CHECK-TYPE COPY-PPRINT-DISPATCH DELETE-DUPLICATES CIS COPY-READTABLE DELETE-FILE CLASS COPY-SEQ DELETE-IF CLASS-NAME COPY-STRUCTURE DELETE-IF-NOT CLASS-OF COPY-SYMBOL DELETE-PACKAGE DENOMINATOR EQ DEPOSIT-FIELD EQL DESCRIBE EQUAL DESCRIBE-OBJECT EQUALP DESTRUCTURING-BIND ERROR DIGIT-CHAR ETYPECASE DIGIT-CHAR-P EVAL DIRECTORY EVAL-WHEN DIRECTORY-NAMESTRING EVENP DISASSEMBLE EVERY DIVISION-BY-ZERO EXP DO EXPORT DO* EXPT DO-ALL-SYMBOLS EXTENDED-CHAR DO-EXTERNAL-SYMBOLS FBOUNDP DO-SYMBOLS FCEILING DOCUMENTATION FDEFINITION DOLIST FFLOOR DOTIMES FIFTH DOUBLE-FLOAT FILE-AUTHOR DOUBLE-FLOAT-EPSILON FILE-ERROR DOUBLE-FLOAT-NEGATIVE-EPSILON FILE-ERROR-PATHNAME DPB FILE-LENGTH DRIBBLE FILE-NAMESTRING DYNAMIC-EXTENT FILE-POSITION ECASE FILE-STREAM ECHO-STREAM FILE-STRING-LENGTH ECHO-STREAM-INPUT-STREAM FILE-WRITE-DATE ECHO-STREAM-OUTPUT-STREAM FILL ED FILL-POINTER EIGHTH FIND ELT FIND-ALL-SYMBOLS ENCODE-UNIVERSAL-TIME FIND-CLASS END-OF-FILE FIND-IF ENDP FIND-IF-NOT ENOUGH-NAMESTRING FIND-METHOD ENSURE-DIRECTORIES-EXIST FIND-PACKAGE ENSURE-GENERIC-FUNCTION FIND-RESTART FIND-SYMBOL GET-INTERNAL-RUN-TIME FINISH-OUTPUT GET-MACRO-CHARACTER FIRST GET-OUTPUT-STREAM-STRING FIXNUM GET-PROPERTIES FLET GET-SETF-EXPANSION FLOAT GET-UNIVERSAL-TIME FLOAT-DIGITS GETF FLOAT-PRECISION GETHASH FLOAT-RADIX GO FLOAT-SIGN GRAPHIC-CHAR-P FLOATING-POINT-INEXACT HANDLER-BIND FLOATING-POINT-INVALID-OPERATION HANDLER-CASE FLOATING-POINT-OVERFLOW HASH-TABLE FLOATING-POINT-UNDERFLOW HASH-TABLE-COUNT FLOATP HASH-TABLE-P FLOOR HASH-TABLE-REHASH-SIZE FMAKUNBOUND HASH-TABLE-REHASH-THRESHOLD FORCE-OUTPUT HASH-TABLE-SIZE FORMAT HASH-TABLE-TEST FORMATTER HOST-NAMESTRING FOURTH IDENTITY FRESH-LINE IF FROUND IGNORABLE FTRUNCATE IGNORE FTYPE IGNORE-ERRORS FUNCALL IMAGPART FUNCTION IMPORT FUNCTION-KEYWORDS IN-PACKAGE FUNCTION-LAMBDA-EXPRESSION INCF FUNCTIONP INITIALIZE-INSTANCE GCD INLINE GENERIC-FUNCTION INPUT-STREAM-P GENSYM INSPECT GENTEMP INTEGER GET INTEGER-DECODE-FLOAT GET-DECODED-TIME INTEGER-LENGTH GET-DISPATCH-MACRO-CHARACTER INTEGERP GET-INTERNAL-REAL-TIME INTERACTIVE-STREAM-P INTERN LISP-IMPLEMENTATION-TYPE INTERNAL-TIME-UNITS-PER-SECOND LISP-IMPLEMENTATION-VERSION INTERSECTION LIST INVALID-METHOD-ERROR LIST* INVOKE-DEBUGGER LIST-ALL-PACKAGES INVOKE-RESTART LIST-LENGTH INVOKE-RESTART-INTERACTIVELY LISTEN ISQRT LISTP KEYWORD LOAD KEYWORDP LOAD-LOGICAL-PATHNAME-TRANSLATIONS LABELS LOAD-TIME-VALUE LAMBDA LOCALLY LAMBDA-LIST-KEYWORDS LOG LAMBDA-PARAMETERS-LIMIT LOGAND LAST LOGANDC1 LCM LOGANDC2 LDB LOGBITP LDB-TEST LOGCOUNT LDIFF LOGEQV LEAST-NEGATIVE-DOUBLE-FLOAT LOGICAL-PATHNAME LEAST-NEGATIVE-LONG-FLOAT LOGICAL-PATHNAME-TRANSLATIONS LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT LOGIOR LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT LOGNAND LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT LOGNOR LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT LOGNOT LEAST-NEGATIVE-SHORT-FLOAT LOGORC1 LEAST-NEGATIVE-SINGLE-FLOAT LOGORC2 LEAST-POSITIVE-DOUBLE-FLOAT LOGTEST LEAST-POSITIVE-LONG-FLOAT LOGXOR LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT LONG-FLOAT LEAST-POSITIVE-NORMALIZED-LONG-FLOAT LONG-FLOAT-EPSILON LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT LONG-FLOAT-NEGATIVE-EPSILON LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT LONG-SITE-NAME LEAST-POSITIVE-SHORT-FLOAT LOOP LEAST-POSITIVE-SINGLE-FLOAT LOOP-FINISH LENGTH LOWER-CASE-P LET MACHINE-INSTANCE LET* MACHINE-TYPE MACHINE-VERSION MASK-FIELD MACRO-FUNCTION MAX MACROEXPAND MEMBER MACROEXPAND-1 MEMBER-IF MACROLET MEMBER-IF-NOT MAKE-ARRAY MERGE MAKE-BROADCAST-STREAM MERGE-PATHNAMES MAKE-CONCATENATED-STREAM METHOD MAKE-CONDITION METHOD-COMBINATION MAKE-DISPATCH-MACRO-CHARACTER METHOD-COMBINATION-ERROR MAKE-ECHO-STREAM METHOD-QUALIFIERS MAKE-HASH-TABLE MIN MAKE-INSTANCE MINUSP MAKE-INSTANCES-OBSOLETE MISMATCH MAKE-LIST MOD MAKE-LOAD-FORM MOST-NEGATIVE-DOUBLE-FLOAT MAKE-LOAD-FORM-SAVING-SLOTS MOST-NEGATIVE-FIXNUM MAKE-METHOD MOST-NEGATIVE-LONG-FLOAT MAKE-PACKAGE MOST-NEGATIVE-SHORT-FLOAT MAKE-PATHNAME MOST-NEGATIVE-SINGLE-FLOAT MAKE-RANDOM-STATE MOST-POSITIVE-DOUBLE-FLOAT MAKE-SEQUENCE MOST-POSITIVE-FIXNUM MAKE-STRING MOST-POSITIVE-LONG-FLOAT MAKE-STRING-INPUT-STREAM MOST-POSITIVE-SHORT-FLOAT MAKE-STRING-OUTPUT-STREAM MOST-POSITIVE-SINGLE-FLOAT MAKE-SYMBOL MUFFLE-WARNING MAKE-SYNONYM-STREAM MULTIPLE-VALUE-BIND MAKE-TWO-WAY-STREAM MULTIPLE-VALUE-CALL MAKUNBOUND MULTIPLE-VALUE-LIST MAP MULTIPLE-VALUE-PROG1 MAP-INTO MULTIPLE-VALUE-SETQ MAPC MULTIPLE-VALUES-LIMIT MAPCAN NAME-CHAR MAPCAR NAMESTRING MAPCON NBUTLAST MAPHASH NCONC MAPL NEXT-METHOD-P MAPLIST NIL NINTERSECTION PACKAGE-ERROR NINTH PACKAGE-ERROR-PACKAGE NO-APPLICABLE-METHOD PACKAGE-NAME NO-NEXT-METHOD PACKAGE-NICKNAMES NOT PACKAGE-SHADOWING-SYMBOLS NOTANY PACKAGE-USE-LIST NOTEVERY PACKAGE-USED-BY-LIST NOTINLINE PACKAGEP NRECONC PAIRLIS NREVERSE PARSE-ERROR NSET-DIFFERENCE PARSE-INTEGER NSET-EXCLUSIVE-OR PARSE-NAMESTRING NSTRING-CAPITALIZE PATHNAME NSTRING-DOWNCASE PATHNAME-DEVICE NSTRING-UPCASE PATHNAME-DIRECTORY NSUBLIS PATHNAME-HOST NSUBST PATHNAME-MATCH-P NSUBST-IF PATHNAME-NAME NSUBST-IF-NOT PATHNAME-TYPE NSUBSTITUTE PATHNAME-VERSION NSUBSTITUTE-IF PATHNAMEP NSUBSTITUTE-IF-NOT PEEK-CHAR NTH PHASE NTH-VALUE PI NTHCDR PLUSP NULL POP NUMBER POSITION NUMBERP POSITION-IF NUMERATOR POSITION-IF-NOT NUNION PPRINT ODDP PPRINT-DISPATCH OPEN PPRINT-EXIT-IF-LIST-EXHAUSTED OPEN-STREAM-P PPRINT-FILL OPTIMIZE PPRINT-INDENT OR PPRINT-LINEAR OTHERWISE PPRINT-LOGICAL-BLOCK OUTPUT-STREAM-P PPRINT-NEWLINE PACKAGE PPRINT-POP PPRINT-TAB READ-CHAR PPRINT-TABULAR READ-CHAR-NO-HANG PRIN1 READ-DELIMITED-LIST PRIN1-TO-STRING READ-FROM-STRING PRINC READ-LINE PRINC-TO-STRING READ-PRESERVING-WHITESPACE PRINT READ-SEQUENCE PRINT-NOT-READABLE READER-ERROR PRINT-NOT-READABLE-OBJECT READTABLE PRINT-OBJECT READTABLE-CASE PRINT-UNREADABLE-OBJECT READTABLEP PROBE-FILE REAL PROCLAIM REALP PROG REALPART PROG* REDUCE PROG1 REINITIALIZE-INSTANCE PROG2 REM PROGN REMF PROGRAM-ERROR REMHASH PROGV REMOVE PROVIDE REMOVE-DUPLICATES PSETF REMOVE-IF PSETQ REMOVE-IF-NOT PUSH REMOVE-METHOD PUSHNEW REMPROP QUOTE RENAME-FILE RANDOM RENAME-PACKAGE RANDOM-STATE REPLACE RANDOM-STATE-P REQUIRE RASSOC REST RASSOC-IF RESTART RASSOC-IF-NOT RESTART-BIND RATIO RESTART-CASE RATIONAL RESTART-NAME RATIONALIZE RETURN RATIONALP RETURN-FROM READ REVAPPEND READ-BYTE REVERSE ROOM SIMPLE-BIT-VECTOR ROTATEF SIMPLE-BIT-VECTOR-P ROUND SIMPLE-CONDITION ROW-MAJOR-AREF SIMPLE-CONDITION-FORMAT-ARGUMENTS RPLACA SIMPLE-CONDITION-FORMAT-CONTROL RPLACD SIMPLE-ERROR SAFETY SIMPLE-STRING SATISFIES SIMPLE-STRING-P SBIT SIMPLE-TYPE-ERROR SCALE-FLOAT SIMPLE-VECTOR SCHAR SIMPLE-VECTOR-P SEARCH SIMPLE-WARNING SECOND SIN SEQUENCE SINGLE-FLOAT SERIOUS-CONDITION SINGLE-FLOAT-EPSILON SET SINGLE-FLOAT-NEGATIVE-EPSILON SET-DIFFERENCE SINH SET-DISPATCH-MACRO-CHARACTER SIXTH SET-EXCLUSIVE-OR SLEEP SET-MACRO-CHARACTER SLOT-BOUNDP SET-PPRINT-DISPATCH SLOT-EXISTS-P SET-SYNTAX-FROM-CHAR SLOT-MAKUNBOUND SETF SLOT-MISSING SETQ SLOT-UNBOUND SEVENTH SLOT-VALUE SHADOW SOFTWARE-TYPE SHADOWING-IMPORT SOFTWARE-VERSION SHARED-INITIALIZE SOME SHIFTF SORT SHORT-FLOAT SPACE SHORT-FLOAT-EPSILON SPECIAL SHORT-FLOAT-NEGATIVE-EPSILON SPECIAL-OPERATOR-P SHORT-SITE-NAME SPEED SIGNAL SQRT SIGNED-BYTE STABLE-SORT SIGNUM STANDARD SIMPLE-ARRAY STANDARD-CHAR SIMPLE-BASE-STRING STANDARD-CHAR-P STANDARD-CLASS SUBLIS STANDARD-GENERIC-FUNCTION SUBSEQ STANDARD-METHOD SUBSETP STANDARD-OBJECT SUBST STEP SUBST-IF STORAGE-CONDITION SUBST-IF-NOT STORE-VALUE SUBSTITUTE STREAM SUBSTITUTE-IF STREAM-ELEMENT-TYPE SUBSTITUTE-IF-NOT STREAM-ERROR SUBTYPEP STREAM-ERROR-STREAM SVREF STREAM-EXTERNAL-FORMAT SXHASH STREAMP SYMBOL STRING SYMBOL-FUNCTION STRING-CAPITALIZE SYMBOL-MACROLET STRING-DOWNCASE SYMBOL-NAME STRING-EQUAL SYMBOL-PACKAGE STRING-GREATERP SYMBOL-PLIST STRING-LEFT-TRIM SYMBOL-VALUE STRING-LESSP SYMBOLP STRING-NOT-EQUAL SYNONYM-STREAM STRING-NOT-GREATERP SYNONYM-STREAM-SYMBOL STRING-NOT-LESSP T STRING-RIGHT-TRIM TAGBODY STRING-STREAM TAILP STRING-TRIM TAN STRING-UPCASE TANH STRING/= TENTH STRING< TERPRI STRING<= THE STRING= THIRD STRING> THROW STRING>= TIME STRINGP TRACE STRUCTURE TRANSLATE-LOGICAL-PATHNAME STRUCTURE-CLASS TRANSLATE-PATHNAME STRUCTURE-OBJECT TREE-EQUAL STYLE-WARNING TRUENAME TRUNCATE VALUES-LIST TWO-WAY-STREAM VARIABLE TWO-WAY-STREAM-INPUT-STREAM VECTOR TWO-WAY-STREAM-OUTPUT-STREAM VECTOR-POP TYPE VECTOR-PUSH TYPE-ERROR VECTOR-PUSH-EXTEND TYPE-ERROR-DATUM VECTORP TYPE-ERROR-EXPECTED-TYPE WARN TYPE-OF WARNING TYPECASE WHEN TYPEP WILD-PATHNAME-P UNBOUND-SLOT WITH-ACCESSORS UNBOUND-SLOT-INSTANCE WITH-COMPILATION-UNIT UNBOUND-VARIABLE WITH-CONDITION-RESTARTS UNDEFINED-FUNCTION WITH-HASH-TABLE-ITERATOR UNEXPORT WITH-INPUT-FROM-STRING UNINTERN WITH-OPEN-FILE UNION WITH-OPEN-STREAM UNLESS WITH-OUTPUT-TO-STRING UNREAD-CHAR WITH-PACKAGE-ITERATOR UNSIGNED-BYTE WITH-SIMPLE-RESTART UNTRACE WITH-SLOTS UNUSE-PACKAGE WITH-STANDARD-IO-SYNTAX UNWIND-PROTECT WRITE UPDATE-INSTANCE-FOR-DIFFERENT-CLASS WRITE-BYTE UPDATE-INSTANCE-FOR-REDEFINED-CLASS WRITE-CHAR UPGRADED-ARRAY-ELEMENT-TYPE WRITE-LINE UPGRADED-COMPLEX-PART-TYPE WRITE-SEQUENCE UPPER-CASE-P WRITE-STRING USE-PACKAGE WRITE-TO-STRING USE-VALUE Y-OR-N-P USER-HOMEDIR-PATHNAME YES-OR-NO-P VALUES ZEROP)) '(ZERO)) NIL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/math-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp")) :END-PORTCULLIS-CMDS NIL (("/Users/cce/plt/research/dracula/trunk/src/teachpacks/rand.lisp" "rand" "rand" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 60571017) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod.lisp" "arithmetic-2/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 230207184)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/floor-mod/floor-mod-helper.lisp" "floor-mod-helper" "floor-mod-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 250164037)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/quotient-remainder-lemmas.lisp" "../../ihs/quotient-remainder-lemmas" "quotient-remainder-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 75580058)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/math-lemmas.lisp" "math-lemmas" "math-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 41383250)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/top.lisp" "../arithmetic/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 51353441)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rationals.lisp" "rationals" "rationals" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 192778911)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/mod-gcd.lisp" "mod-gcd" "mod-gcd" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 49344105)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130234613)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 103475026)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260688904)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 106260818)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 44566077)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/natp-posp.lisp" "natp-posp" "natp-posp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 77763855)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130234613)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/rational-listp.lisp" "rational-listp" "rational-listp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 64148425)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic/equalities.lisp" "equalities" "equalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 103475026)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-crg.lisp" "../cowles/acl2-crg" "acl2-crg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 260688904)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-agp.lisp" "acl2-agp" "acl2-agp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 106260818)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/cowles/acl2-asg.lisp" "acl2-asg" "acl2-asg" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 44566077)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/ihs-theories.lisp" "ihs-theories" "ihs-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 88130948)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/ihs/ihs-init.lisp" "ihs-init" "ihs-init" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 115970970)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/data-structures/utilities.lisp" "../data-structures/utilities" "utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 58465099)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/top.lisp" "../meta/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 112844677)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/post.lisp" "post" "post" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 111875395)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 159968747)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 236109322)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 82194709)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 249242356)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 254673040)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/collect-terms-meta.lisp" "collect-terms-meta" "collect-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 86943081)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/cancel-terms-meta.lisp" "cancel-terms-meta" "cancel-terms-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 201143376)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/cancel-terms-helper.lisp" "cancel-terms-helper" "cancel-terms-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 59403007)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/common-meta.lisp" "common-meta" "common-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 18424879)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 23974661)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 27882705)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/meta/pre.lisp" "pre" "pre" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 217072582)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 228875392)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 130872758)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/numerator-and-denominator-helper.lisp" "numerator-and-denominator-helper" "numerator-and-denominator-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 41852482)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 208853457)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 244408932)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 244408932)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 136146365)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 245418597)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 218438736)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 239360158)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 239360158)) (LOCAL ("/Users/cce/Local/ACL2/3.2/openmcl-64/books/arithmetic-2/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 51473664))) 98531785