(FILECREATED "27-Nov-85 12:02:38" ("compiled on " {ERIS}BOYERMOORE.;3) "12-Nov-85 14:59:23" recompiled explicitly: PPR2 PPR22 in "INTERLISP-D 22-Nov-85 ..." dated "22-Nov-85 11:32:58") (FILECREATED "27-Nov-85 11:28:23" {ERIS}BOYERMOORE.;3 659489 changes to: (FNS AN-ERROR CHAR-EQUAL CHAR-IN-STRING CHAR-UPCASE COMPILE-IF-APPROPRIATE-AND-POSSIBLE COPYLIST COPYTREE EXTEND-FILE-NAME FIND-CHAR-IN-FILE FIND-STRING-IN-FILE FIND-STRING-IN-STRING FTELL GET-TOTAL-STATS GET-FROM-FILE GET-PLIST-FROM-FILE GET-STATS-FILE BM:PRIN1 PRINT-SYSTEM PRINT-DATE-LINE RANDOM-INITIALIZATION RANDOM-NUMBER READ-FILE REMQ RUNTIME STORE-DEFINITION STRING-DOWNCASE STRING-LENGTH SWAP-OUT R-LOOP TIME-IT TIME-DIFFERENCE TIME-IN-60THS XSEARCH *1*CAR *1*CDR ACCESS-MACRO ADD-TO-SET ARGN-MACRO BINDINGS-MACRO CELL CREATE-LEMMA-STACK CREATE-LINEARIZE-ASSUMPTIONS-STACK CREATE-STACK1 FARGN-MACRO FN-SYMB-MACRO GET-FIELD-NUMBER HLOAD IPOSITION ITERPRI ITERPRIN ITERPRISPACES IPRIN1 IPRINC IPRINT ISPACES KILL-DEFINITION LINEL MAKE-LIB MAKE-MACRO MAKUNBOUND MATCH-MACRO MATCH!-MACRO MATCH1-MACRO MATCH2-MACRO NOTE-LIB BM:NTH PREPARE-FOR-THE-NIGHT RECORD-DECLARATION RECORD-DECLARATION-LST SPELL-NUMBER CHANGE-MACRO SUB-PAIR UNIONQ *1*ADD1 *1*AND *1*CONS *1*COUNT *1*DIFFERENCE *1*EQUAL *1*FALSE *1*FALSEP *1*FIX *1*IMPLIES *1*LESSP *1*LISTP *1*LITATOM *1*MINUS *1*NEGATIVE-GUTS *1*NEGATIVEP *1*NLISTP *1*NOT *1*NUMBERP *1*OR *1*PACK *1*PLUS *1*QUOTIENT *1*REMAINDER *1*SUB1 *1*TIMES *1*TRUE *1*TRUEP *1*UNPACK *1*ZERO *1*ZEROP ABBREVIATIONP ABBREVIATIONP1 ACCEPTABLE-TYPE-PRESCRIPTION-LEMMAP ACCESS-ERROR ADD-AXIOM1 ADD-DCELL ADD-ELIM-LEMMA ADD-EQUATION ADD-EQUATIONS ADD-EQUATIONS-TO-POT-LST ADD-FACT ADD-GENERALIZE-LEMMA ADD-LEMMA ADD-LEMMA0 ADD-LESSP-ASSUMPTION-TO-POLY ADD-LINEAR-TERM ADD-LINEAR-VARIABLE ADD-LINEAR-VARIABLE1 ADD-LITERAL ADD-META-LEMMA ADD-NOT-EQUAL-0-ASSUMPTION-TO-POLY ADD-NOT-LESSP-ASSUMPTION-TO-POLY ADD-NUMBERP-ASSUMPTION-TO-POLY ADD-PROCESS-HIST ADD-REWRITE-LEMMA ADD-SHELL-ROUTINES ADD-SHELL0 ADD-SUB-FACT ADD-TERM-TO-POT-LST ADD-TERMS-TO-POT-LST ADD-TO-SET-EQ ADD-TYPE-SET-LEMMAS ALL-ARGLISTS ALL-FNNAMES ALL-FNNAMES-LST ALL-FNNAMES1 ALL-FNNAMES1-EVG ALL-INSERTIONS ALL-PATHS ALL-PERMUTATIONS ALL-PICKS ALL-SUBSEQUENCES ALL-VARS ALL-VARS-BAG ALL-VARS-BAG1 ALL-VARS-LST ALL-VARS1 ALMOST-SUBSUMES ALMOST-SUBSUMES-LOOP ALMOST-VALUEP ALMOST-VALUEP1 APPLY-HINTS APPLY-INDUCT-HINT APPLY-USE-HINT ARG1-IN-ARG2-UNIFY-SUBST ARGN0 ARITY ASSOC-OF-APPEND ASSUME-TRUE-FALSE ATTEMPT-TO-REWRITE-RECOGNIZER BATCH-PROVEALL BOOLEAN BOOT-STRAP0 BREAK-LEMMA BTM-OBJECT BTM-OBJECT-OF-TYPE-SET BTM-OBJECTP BUILD-SUM CANCEL CANCEL-POSITIVE CANCEL1 CAR-CDRP CDR-ALL CHK-ACCEPTABLE-DEFN CHK-ACCEPTABLE-DCL CHK-ACCEPTABLE-ELIM-LEMMA CHK-ACCEPTABLE-GENERALIZE-LEMMA CHK-ACCEPTABLE-HINTS CHK-ACCEPTABLE-LEMMA CHK-ACCEPTABLE-META-LEMMA CHK-ACCEPTABLE-REFLECT CHK-ACCEPTABLE-REWRITE-LEMMA CHK-ACCEPTABLE-SHELL CHK-ACCEPTABLE-TOGGLE CHK-ARGLIST CHK-MEANING CHK-NEW-*1*NAME CHK-NEW-NAME CLAUSIFY CLAUSIFY-INPUT CLAUSIFY-INPUT1 CLEAN-UP-BRANCHES CNF-DNF COMMON-SWEEP COMMUTE-EQUALITIES COMPARE-STATS COMPLEMENTARY-MULTIPLEP COMPLEMENTARYP COMPLEXITY COMPRESS-POLY COMPRESS-POLY1 COMPUTE-VETOES COMSUBT1 COMSUBTERMS CONJOIN CONJOIN-CLAUSE-SETS CONJOIN2 CONS-PLUS CONS-TERM CONSJOIN CONTAINS-REWRITEABLE-CALLP CONVERT-CAR-CDR CONVERT-CONS CONVERT-NOT CONVERT-QUOTE CONVERT-TYPE-NO-TO-RECOGNIZER-TERM BM:COUNT COUNT-IFS CREATE-REWRITE-RULE DCL0 DECODE-IDATE DEFN-ASSUME-TRUE-FALSE DEFN-LOGIOR DEFN-SETUP DEFN-TYPE-SET DEFN-TYPE-SET2 DEFN-WRAPUP DEFN0 DELETE1 DELETE-TAUTOLOGIES DELETE-TOGGLES DEPEND DEPENDENT-EVENTS DEPENDENTS-OF DEPENDENTS-OF1 DESTRUCTORS DESTRUCTORS1 DETACH DETACHED-ERROR DETACHEDP DISJOIN DISJOIN-CLAUSES DISJOIN2 DTACK-0-ON-END DUMB-CONVERT-TYPE-SET-TO-TYPE-RESTRICTION-TERM DUMB-IMPLICATE-LITS DUMB-NEGATE-LIT DUMB-OCCUR DUMB-OCCUR-LST DUMP DUMP-ADD-AXIOM DUMP-ADD-SHELL DUMP-BEGIN-GROUP DUMP-DCL DUMP-DEFN DUMP-END-GROUP DUMP-HINTS DUMP-LEMMA-TYPES DUMP-OTHER DUMP-PROVE-LEMMA DUMP-TOGGLE ELIMINABLE-VAR-CANDS ELIMINABLEP ELIMINATE-DESTRUCTORS-CANDIDATEP ELIMINATE-DESTRUCTORS-CANDIDATES ELIMINATE-DESTRUCTORS-CANDIDATES1 ELIMINATE-DESTRUCTORS-CLAUSE ELIMINATE-DESTRUCTORS-CLAUSE1 ELIMINATE-DESTRUCTORS-SENT ELIMINATE-IRRELEVANCE-CLAUSE ELIMINATE-IRRELEVANCE-SENT EQUATIONAL-PAIR-FOR ERASE-EOL ERASE-EOP ERROR1 EVENT-FORM EVENT1-OCCURRED-BEFORE-EVENT2 EVENTS-SINCE EVG EVG-OCCUR-LEGAL-CHAR-CODE-SEQ EVG-OCCUR-NUMBER EVG-OCCUR-OTHER EXECUTE EXPAND-ABBREVIATIONS EXPAND-AND-ORS EXPAND-BOOT-STRAP-NON-REC-FNS EXPAND-NON-REC-FNS EXPAND-PPR-MACROS EXTEND-ALIST EXTERNAL-LINEARIZE EXTRACT-DEPENDENCIES-FROM-HINTS FALSE-NONFALSEP FAVOR-COMPLICATED-CANDIDATES FERTILIZE-CLAUSE FERTILIZE-FEASIBLE FERTILIZE-SENT FERTILIZE1 FILTER-ARGS FIND-EQUATIONAL-POLY FIRST-COEFFICIENT FIRST-VAR FITS FIXCAR-CDR FLATTEN-ANDS-IN-LIT FLESH-OUT-IND-PRIN FLUSH-CAND1-DOWN-CAND2 FN-SYMB0 FNNAMEP FNNAMEP-IF FORM-COUNT FORM-COUNT-EVG FORM-COUNT1 FORM-INDUCTION-CLAUSE FORMP-SIMPLIFIER FORMULA-OF FREE-VAR-CHK FREE-VARSP GEN-VARS GENERALIZE-CLAUSE GENERALIZE-SENT GENERALIZE1 GENERALIZE2 GENRLT1 GENRLTERMS GET-CANDS GET-LISP-SEXPR GET-LEVEL-NO GET-STACK-NAME GET-STACK-NAME1 GET-TYPES GREATEREQP GUARANTEE-CITIZENSHIP GUESS-RELATION-MEASURE-LST HAS-LIB-PROPS ILLEGAL-CALL ILLEGAL-NAME IMMEDIATE-DEPENDENTS-OF IMPLIES? IMPOSSIBLE-POLYP IND-FORMULA INDUCT INDUCT-VARS INDUCTION-MACHINE INFORM-SIMPLIFY INIT-LEMMA-STACK INIT-LIB INIT-LINEARIZE-ASSUMPTIONS-STACK INTERESTING-SUBTERMS INTERSECTP INTRODUCE-ANDS INTRODUCE-LISTS JUMPOUTP KILL-EVENT KILL-LIB KILLPROPLIST1 LEGAL-CHAR-CODE-SEQ LENGTH-TO-ATOM LESSEQP LEXORDER LINEARIZE LISTABLE LOGSUBSETP LOOKUP-HYP LOOP-STOPPER MAIN-EVENT-OF MAKE-EVENT MAKE-FLATTENED-MACHINE MAKE-NEW-NAME MAKE-REWRITE-RULES MAKE-TYPE-RESTRICTION MAX-FORM-COUNT MAXIMAL-ELEMENTS MEANING-SIMPLIFIER MEMB-NEGATIVE MENTIONSQ MENTIONSQ-LST MERGE-CAND1-INTO-CAND2 MERGE-CANDS MERGE-DESTRUCTOR-CANDIDATES MERGE-TESTS-AND-ALISTS MERGE-TESTS-AND-ALISTS-LSTS META-LEMMAP MULTIPLE-PIGEON-HOLE CL:NEGATE NEGATE-LIT NEXT-AVAILABLE-TYPE-NO NO-CROWDINGP NO-DUPLICATESP NO-OP NON-RECURSIVE-DEFNP NORMALIZE-IFS NOT-EQUAL-0? NOT-IDENT NOT-LESSP? NOT-TO-BE-REWRITTENP NUMBERP? OBJ-TABLE OCCUR OCCUR-CNT OCCUR-LST ONE-WAY-UNIFY ONE-WAY-UNIFY-LIST ONE-WAY-UNIFY1 ONE-WAY-UNIFY11 ONEIFY ONEIFY-ASSUME-FALSE ONEIFY-ASSUME-TRUE ONEIFY-TEST OPTIMIZE-COMMON-SUBTERMS PARTITION PARTITION-CLAUSES PATH-ADD-TO-SET PATH-EQ PATH-POT-SUBSUMES PATH-UNION PEGATE-LIT PETITIO-PRINCIPII PICK-HIGH-SCORES PIGEON-HOLE PIGEON-HOLE-IN-ALL-POSSIBLE-WAYS PIGEON-HOLE1 PLUSJOIN POLY-MEMBER POP-CLAUSE-SET POP-LEMMA-FRAME POP-LINEARIZE-ASSUMPTIONS-FRAME POPU POSSIBLE-IND-PRINCIPLES POSSIBLY-NUMERIC POWER-EVAL POWER-REP PPC PPE PPE-LST PPR PPRINDENT PPSD PPSD-LST PREPROCESS PREPROCESS-HYPS PRETTYIFY-CLAUSE PRETTYIFY-LISP PRIMITIVE-RECURSIVEP PRIMITIVEP PRINT-STACK PRINT-STATS PRINT-TO-DISPLAY PROCESS-EQUATIONAL-POLYS PROPERTYLESS-SYMBOLP PROVE PROVE-TERMINATION PROVEALL PUSH-CLAUSE-SET PUSH-LEMMA PUSH-LEMMA-FRAME PUSH-LINEARIZE-ASSUMPTION PUSH-LINEARIZE-ASSUMPTIONS-FRAME PUSHU PUT-CURSOR PUT-INDUCTION-INFO PUT-LEVEL-NO PUT-TYPE-PRESCRIPTION PUT0 PUT00 PUT1 PUT1-LST PUTD1 QUICK-BLOCK-INFO QUICK-BLOCK-INFO1 QUICK-WORSE-THAN R REDO! REDO-UNDONE-EVENTS REDUCE REDUCE1 REFLECT0 RELIEVE-HYPS RELIEVE-HYPS-NOT-OK RELIEVE-HYPS1 REMOVE-*2*IFS REMOVE-NEGATIVE REMOVE-REDUNDANT-TESTS REMOVE1 REMOVE-TRIVIAL-EQUATIONS REMOVE-UNCHANGING-VARS REMPROP1 RESTART RESTART-BATCH REWRITE REWRITE-FNCALL REWRITE-FNCALLP REWRITE-IF REWRITE-IF1 REWRITE-LINEAR-CONCL REWRITE-SOLIDIFY REWRITE-TYPE-PRED REWRITE-WITH-LEMMAS REWRITE-WITH-LINEAR RPLACAI S SARGS SCONS-TERM SCRUNCH SCRUNCH-CLAUSE SCRUNCH-CLAUSE-SET SEARCH-GROUND-UNITS SEQUENTIAL-DIFFERENCE SET-DIFF SET-DIFF-N SET-EQUAL SET-SIMPLIFY-CLAUSE-POT-LST SETTLED-DOWN-CLAUSE SETTLED-DOWN-SENT SETUP SETUP-META-NAMES SHELL-CONSTRUCTORP SHELL-DESTRUCTOR-NESTP SHELL-OCCUR SHELL-OCCUR1 SHELLP SIMPLIFY-CLAUSE SIMPLIFY-CLAUSE-MAXIMALLY SIMPLIFY-CLAUSE-MAXIMALLY1 SIMPLIFY-CLAUSE0 SIMPLIFY-CLAUSE1 SIMPLIFY-LOOP SIMPLIFY-SENT SINGLETON-CONSTRUCTOR-TO-RECOGNIZER SKO-DEST-NESTP SOME-SUBTERM-WORSE-THAN-OR-EQUAL SORT-DESTRUCTOR-CANDIDATES SOUND-IND-PRIN-MASK STACK-DEPTH START-STATS STOP-STATS STORE-SENT STRIP-BRANCHES STRIP-BRANCHES1 SUB-SEQUENCEP SUBBAGP SUBLIS-EXPR SUBLIS-EXPR1 SUBLIS-VAR SUBLIS-VAR-LST SUB-PAIR-EXPR SUB-PAIR-EXPR-LST SUB-PAIR-EXPR1 SUB-PAIR-VAR SUB-PAIR-VAR-LST SUBSETP SUBST-EXPR SUBST-EXPR-ERROR1 SUBST-EXPR-LST SUBST-EXPR1 SUBST-FN SUBST-VAR SUBST-VAR-LST SUBSTITUTE SUBSUMES SUBSUMES-REWRITE-RULE SUBSUMES1 SUBSUMES11 SUM-STATS-ALIST TABULATE TERM-ORDER TERMINATION-MACHINE TP-EXPLODEN1 TP-GETCHARN1 TP-IMPLODE1 TO-BE-IGNOREDP TOO-MANY-IFS TOP-FNNAME TOTAL-FUNCTIONP TRANSITIVE-CLOSURE TRANSLATE TRANSLATE-TO-LISP TREE-DEPENDENTS TRIVIAL-POLYP TRIVIAL-POLYP1 TRUE-POLYP TYPE-ALIST-CLAUSE TYPE-PRESCRIPTION-LEMMAP TYPE-SET TYPE-SET2 UBT UNBREAK-LEMMA UNCHANGING-VARS UNCHANGING-VARS1 UNDO-BACK-THROUGH UNDO-NAME UNION-EQUAL UNPRETTYIFY VARIANTP WORSE-THAN WORSE-THAN-OR-EQUAL WRAPUP XXXJOIN ZERO-POLY BOOT-STRAP ADD-AXIOM ADD-SHELL DCL DEFN DEFN& DISABLE ENABLE PROVE-LEMMA PROVE-LEMMA& REFLECT TOGGLE GENERATE-ADD-FACT-PART GENERATE-ADD-SUB-FACT1 GENERATE-SUB-FACT-PART GENERATE-UNDO-TUPLE-PART !CLAUSE-SET !CLAUSE EQUALITY-HYP-NO GET-SCHEMA-MEASURE-RELATION IO IO1 JUSTIFICATION-SENTENCE !LIST MAPRINEVAL NOTICE-CLAUSE PEVAL PEVAL-APPLY PEVALV PLURALP !PPR-LIST !PPR PRIN5* PRINEVAL PRINEVAL1 PRINT-DEFN-MSG TH-IFY UN-NOTICE-CLAUSE PPRIND PPRPACK PPR1 PPR2 PPR22 TERPRISPACES) (MACROS PRIND TYO1 ) previous date: "26-Nov-85 16:14:09" {ERIS}BOYERMOORE.;2) AN-ERROR D1 (I 0 MESSAGE) @ (3 ERROR) NIL () CHAR-EQUAL D1 (L (1 C2 0 C1)) @AjNIL NIL () CHAR-IN-STRING D1 (I 1 STRING I 0 CHAR) @ A hh(7 STRPOS 3 CHARACTER) NIL () CHAR-UPCASE D1 (L (0 N)) la@@dlzl @NIL NIL () COMPILE-IF-APPROPRIATE-AND-POSSIBLE D1 (P 0 FN I 0 FNS) @dH H h(23Q COMPILE! 16Q CCODEP 13Q GETD) NIL () COPYLIST D1 (L (0 L)) 0@dIHhZH&JNIL NIL () COPYTREE D1 (I 0 X) @ (3 COPY) NIL () EXTEND-FILE-NAME D1 (I 1 EXTENSION I 0 FILE) gAh@ (20Q PACKFILENAME 15Q \APPEND2 12Q UNPACKFILENAME) (2 EXTENSION) () FIND-CHAR-IN-FILE D1 (P 0 CH I 1 FILE I 0 CHAR) Am Xdmjh@jA (34Q FILEPOS 10Q TYI) NIL () FIND-STRING-IN-FILE D1 (P 7 CHAR P 5 *1*+FILE-LEN-STR-LEN P 4 OTHER-CHARS P 3 FIRST-CHAR P 2 CHARS P 1 POS P 0 STRING-LEN-1 I 1 FILE I 0 STRING F 10Q CHARS) f@ kHmA @ @ WWA H KA YdM%LN iIk_A jhN^AI (141Q SETFILEPTR 120Q TYI 61Q FIND-CHAR-IN-FILE 50Q MINUS 44Q GETEOFPTR 32Q CHCON 26Q CHCON 21Q GETFILEPTR 3 NCHARS) NIL () FIND-STRING-IN-STRING D1 (P 4 TAIL P 3 PAT-LEN P 2 PAT-CHARS P 1 I I 1 STR I 0 PAT) ^ A A @ @ HL$KIhJL"N_M i A I_OOjhNMLImԹ(70Q NCHARS 17Q NCHARS 13Q UNPACK 7 NCHARS 3 UNPACK) NIL () FTELL D1 (I 0 PORT) @jk (5 FSEEK) NIL () GET-TOTAL-STATS D1 (P 3 ROOT P 2 STATS P 1 IO-TIME P 0 TP-TIME I 0 DIR) @@o/dg@gKggh ZHظJIعHIh(51Q SUM-STATS-ALIST 46Q GET-STATS-FILE 43Q PACKFILENAME) (31Q PROOFS 26Q EXTENSION 22Q NAME 16Q DIRECTORY) ( 6 (PROVEALL RSA WILSON GAUSS FORTRAN CONTROLLER PR TMI UNSOLV ZTAK)) GET-FROM-FILE D1 (I 1 PROP I 0 ATM) @ HY AIIg(3 GET-PLIST-FROM-FILE) (27Q CDDR) () GET-PLIST-FROM-FILE D1 (P 2 ECHOFILES P 1 #+PDP10 P 0 LOC I 0 ATM F 3 LIB-FILE) $@g!Hhg SH S (34Q READ 30Q SETFILEPTR 21Q BOUNDP) (16Q LIB-FILE 3 LIB-LOC) () GET-STATS-FILE D1 (P 4 IO-TIME P 3 TP-TIME P 2 TEMP P 1 EOF-CONS P 0 EVENT-CHAR I 0 FILE F 10Q #/) ggk)hh2@g bdj 0H@ CI@I Z9W@ 1@I [3'@I \3JKLh_N Oh^O&M(103Q READ 71Q READ 62Q FIND-CHAR-IN-FILE 50Q READ 40Q FIND-CHAR-IN-FILE 30Q SETFILEPTR 21Q OPENSTREAM) (16Q INPUT 2 % ) () BM:PRIN1 D1 (I 1 FILE I 0 DATA) @A (4 PATOM) NIL () PRINT-SYSTEM D1 (P 0 FL I 0 FILE F 1 THEOREM-PROVER-FILES F 2 MAKESYSNAME F 3 MAKESYSDATE) Bg@ @ o@ QdHg R@ o@ S@ @ (77Q TERPRI 73Q PRIN1 66Q PRIN1 56Q PRIN1 44Q PRINT 22Q PRIN1 12Q TERPRI 6 PRIN1) (36Q FILEDATES 2 SYSTEM) ( 62Q " " 16Q "0.0 0.0") PRINT-DATE-LINE D1 (F 0 PROVE-FILE) P (6 PRIN1 2 GDATE) NIL () RANDOM-INITIALIZATION D1 (I 0 EVENT) o (6 RANDSET) NIL ( 3 (33432Q 114776Q 176503Q 160605Q 104147Q 12303Q 27516Q 35414Q 23625Q 25100Q 165301Q 55060Q 12770Q 51534Q 151241Q 35402Q 11114Q 121413Q 175052Q 56312Q 37620Q 5644Q 131124Q 146171Q 4472Q 107462Q 177406Q 124466Q 134362Q 114755Q 111443Q 127047Q 105060Q 56143Q 17344Q 102125Q 77056Q 53202Q 174307Q 130576Q 144271Q 26564Q 125273Q 165074Q 127765Q 136401Q 175404Q 110611Q 10573Q 35055Q 35203Q 136124Q 136552Q 54176Q 70527Q)) RANDOM-NUMBER D1 (I 0 N) j@k (6 RAND) NIL () READ-FILE D1 (P 5 TEMP P 1 MY-CONS P 0 FILE I 0 FILE-NAME) .@g hh@IHI ]MK Lh[L&J(25Q READ 6 OPENSTREAM) (3 INPUT) () REMQ D1 (L (1 L 0 I)) $A1HId@J KhZYHXK&ZNIL NIL () RUNTIME D1 NIL ol<(2 PTIME) NIL ( 7 3641100Q) STORE-DEFINITION D1 (I 1 EXPR I 0 ATM) @Ag @ (13Q COMPILE! 7 PUTD) (4 EXPR) () STRING-DOWNCASE D1 (I 0 STR) @ (3 L-CASE) NIL () STRING-LENGTH D1 (I 0 X) @ (3 NCHARS) NIL () SWAP-OUT D1 (I 0 NAME) g@ (11Q APPLY 6 MAKE-LIB) (2 NOTE-LIB) () R-LOOP D1 NIL h g h h (32Q PPR 27Q R 23Q TERPRI 17Q READ 12Q PRIN2 3 TERPRI) (7 *) () TIME-IT D1 (P 0 START-TIME I 0 FORM) @ H oh(20Q TIME-DIFFERENCE 14Q TIME-IN-60THS 11Q EVAL 2 TIME-IN-60THS) NIL ( 24Q 60.0) TIME-DIFFERENCE D1 (L (1 Y 0 X)) @ANIL NIL () TIME-IN-60THS D1 NIL (2 IDATE) NIL () XSEARCH D1 (P 10Q STRING P 6 FILE P 5 NAME P 4 L I 1 FILE-SPECS I 0 STRINGS) @@hbAAhb0AdhhXIHZYJaH I YH\>i L]i Mg @O%hhN oi MJ+KhZHX_Nj ON OiO_K&(224Q FIND-STRING-IN-FILE 215Q SETFILEPTR 164Q PRIN1 151Q CLOSE? 127Q OPENSTREAM 117Q PRIN1 107Q TERPRI 71Q LAST) (124Q INPUT) ( 160Q "Yes.") *1*CAR D1 (L (0 X1)) @jg@NIL (11Q *1*QUOTE) () *1*CDR D1 (L (0 X1)) @jg@NIL (11Q *1*QUOTE) () ACCESS-MACRO D1 (L (2 RECORD 1 FIELD 0 RECORD-NAME)) g@AhgBhNIL (12Q of 2 fetch) () ADD-TO-SET D1 (I 1 Y I 0 X) @A A@A(4 MEMBER) NIL () ARGN-MACRO D1 (I 0 TAIL) ,@3 o@@g @ho g@(43Q SUB-PAIR 25Q CELL) (47Q ARGN0 22Q TEMP-TEMP) ( 40Q (COND ((NEQ (CAR (SETQ TEMP-TEMP TERM)) (QUOTE QUOTE)) (CAR CELL)) (T (ARGN0 TEMP-TEMP N))) 12Q (TERM CELL N)) BINDINGS-MACRO D1 (I 0 TAIL) @hgd@@h@ h(27Q BINDINGS-MACRO) (7 CONS) () CELL D1 (I 1 FIELD I 0 N) @jjAg@kA h(21Q CELL) (12Q CDR) () CREATE-LEMMA-STACK D1 (L (0 N) F 0 LEMMA-STACK F 1 ORIG-LEMMA-STACK) hccNIL NIL () CREATE-LINEARIZE-ASSUMPTIONS-STACK D1 (L (0 N) F 0 LINEARIZE-ASSUMPTIONS-STACK F 1 ORIG-LINEARIZE-ASSUMPTIONS-STACK) hccNIL NIL () CREATE-STACK1 D1 (L (0 N)) ? @lk2KJLXdYIdHM Nh]Kk[N&IgNIL (73Q CDDR) () FARGN-MACRO D1 (I 0 TAIL) #@3 g@@ hg@@h(20Q CELL) (27Q BM:NTH 10Q CAR) () FN-SYMB-MACRO D1 (I 0 TAIL) @go (13Q SUBST) (4 TERM) ( 10Q (COND ((NEQ (QUOTE QUOTE) (CAR (SETQ TEMP-TEMP TERM))) (CAR TEMP-TEMP)) (T (FN-SYMB0 (CADR TEMP-TEMP))))) GET-FIELD-NUMBER D1 (I 1 LITATOM I 0 RECORD-NAME F 2 TEMP-TEMP F 3 RECORD-DECLARATIONS) Q@ScdRjkH+h&i oi i li @Ahi i kAIIkԹHX(75Q ITERPRI 71Q PRIN2 60Q SPACES 52Q TERPRI 46Q PRIN1 36Q TERPRI) NIL ( 42Q "***** Undeclared record name or illegal field name *****") HLOAD D1 (P 1 EXPR P 0 STREAM I 0 FILE) # @g XH YdgH  (36Q EVAL 32Q CLOSEF 16Q HREAD 11Q OPENSTREAM) (23Q STOP 6 INPUT) () IPOSITION D1 (P 0 PAIR I 2 FLG I 1 N I 0 FILE F 1 IPOSITION-ALIST) *@QX@jXQcAHBHHAHHHANIL NIL () ITERPRI D1 (I 0 FILE) @j @ (10Q TERPRI 4 IPOSITION) NIL () ITERPRIN D1 (P 1 I I 1 FILE I 0 N) @kIHhA IkY(16Q ITERPRI) NIL () ITERPRISPACES D1 (I 1 FILE I 0 N) A @A (10Q TABULATE 3 ITERPRI) NIL () IPRIN1 D1 (I 1 FILE I 0 X) A@ i @A (15Q PRIN2 10Q IPOSITION 4 NCHARS) NIL () IPRINC D1 (I 1 FILE I 0 X) A@ i @A (15Q PRIN1 10Q IPOSITION 4 NCHARS) NIL () IPRINT D1 (I 1 FILE I 0 X) A@ @A (14Q PRINT 7 IPOSITION 4 NCHARS) NIL () ISPACES D1 (P 1 I I 1 FILE I 0 N) &@jhA@i @kIHoA IkY(35Q PRIN1 13Q IPOSITION) NIL ( 31Q " ") KILL-DEFINITION D1 (I 0 FN) @ (3 PUTD) NIL () LINEL D1 (I 1 N I 0 FILE) A@ (4 LINELENGTH) NIL () MAKE-LIB D1 (P 15Q PROP P 11Q ATM P 10Q VAR P 4 REVERSED-LIB-PROPS P 3 FILE-PLIST P 2 FN-FILE P 1 PROP-FILE P 0 TEMP I 0 FILE F 16Q LIB-ATOMS-WITH-DEFS F 17Q LIB-PROPS F 20Q LIB-VARS F 21Q LIB-ATOMS-WITH-PROPS F 22Q FILECOMS) W \@g g YgWddi3 gWhW ddi3 gW hhI W ,dgOd ]ddi3 gMhhI ggW"ddi3 gW"hhI ggWddi3 gWhhI W"qd gOddi3 gOh0 L-d OO X OHh_O6O__O^ddi3 gNhhI W ` _Od gOddi3 gOhggOgXHhh_ddi3 gOhhI gI I Y@ c$dgW h @g ZIJh(707Q BCOMPL 704Q MAKEFILE 675Q SET 667Q REVERSE 654Q FILECOMS 647Q CLOSEF 643Q PRINT 627Q HPRINT 476Q LAST 471Q REVERSE 457Q HPRINT 363Q MEMB 360Q GETPROPLIST 276Q PRINT 234Q PRINT 165Q PRINT 133Q GETTOPVAL 111Q PRINT 25Q OPENSTREAM 17Q EXTEND-FILE-NAME 7 REVERSE) (701Q NEW 662Q FNS 637Q STOP 612Q QUOTE 554Q SEXPR 547Q LAMBDA 544Q SEXPR 534Q QUOTE 515Q PUT1-LST 443Q QUOTE 331Q QUOTE 312Q PUT1-LST 261Q QUOTE 242Q LIB-ATOMS-WITH-DEFS 237Q SETQ 217Q QUOTE 200Q LIB-ATOMS-WITH-PROPS 175Q SETQ 151Q QUOTE 125Q SETQ 74Q QUOTE 50Q QUOTE 31Q INIT-LIB 22Q OUTPUT 14Q LIB) () MAKE-MACRO D1 (P 4 ARG P 3 FIELD I 1 ARGLIST I 0 RECORD F 5 TEMP-TEMP) @ c #i oi i li @i i hA U j9g@AU2IH J JKgLh IHoi i li g@Ai i h(220Q ITERPRI 214Q PRIN2 201Q SPACES 173Q TERPRI 167Q IPRINC 146Q \NCONC2 124Q \APPEND2 63Q LENGTH 54Q LENGTH 46Q TERPRI 42Q PRIN2 35Q SPACES 27Q ITERPRI 23Q IPRINC 13Q ITERPRI 3 RECLOOK) (204Q MAKE 136Q _ 73Q create) ( 163Q "***** Wrong number of args *****" 17Q "***** Undeclared record name in MAKE expression *****") MAKUNBOUND D1 (I 0 NLISTP) @g (6 SET) (3 NOBIND) () MATCH-MACRO D1 (I 1 PAT I 0 TERM) &@dggg@hgA hA (43Q MATCH1-MACRO 32Q MATCH1-MACRO) (26Q MATCH-TEMP 16Q MATCH-TEMP 13Q SETQ 10Q PROGN) () MATCH!-MACRO D1 (I 1 PAT I 0 TERM) g@A oh(7 MATCH-MACRO) (2 OR) ( 13Q (ERROR "MATCH! failed!")) MATCH1-MACRO D1 (P 1 SETQ-LST P 0 TEST-LST I 1 PAT I 0 TERM) ' @A gHiHgHIih h(40Q \NCONC2 7 MATCH2-MACRO) (27Q AND 12Q COND) () MATCH2-MACRO D1 (P 0 SUBPAT I 1 PAT I 0 TERM F 1 TEST-LST F 2 SETQ-LST F 3 MATCH-X) :AdZdghiA"oi i li gSi i lRgA@hh cQgA@hh cg4Qg@hh cg@hA g@hAbbmAdg>lQggAh@hh cQggAh@hh cgggAhAb0A-dQg@hh cg@hH g@hbQg@hhh c(465Q \NCONC2 427Q MATCH2-MACRO 411Q \NCONC2 327Q \NCONC2 275Q \NCONC2 177Q MATCH2-MACRO 160Q \NCONC2 131Q \NCONC2 107Q \NCONC2 61Q ITERPRI 55Q PRIN2 44Q SPACES 36Q TERPRI 32Q PRIN1) (452Q EQ 433Q CDR 417Q CAR 400Q LISTP 347Q QUOTE 344Q LIST 336Q LIST 307Q QUOTE 304Q EQUAL 255Q QUOTE 252Q EQ 233Q QUOTE 202Q CDR 165Q CAR 147Q LISTP 140Q CONS 116Q EQUAL 74Q SETQ 47Q BM:MATCH 10Q &) ( 26Q "***** Attempt to smash T or NIL ignored *****") NOTE-LIB D1 (P 1 FILE2 P 0 FILE1 I 0 FILE F 2 LIB-FILE) - @g X@g Yg H cI h(47Q LOAD 41Q HLOAD 34Q KILL-LIB 30Q BOUNDP 21Q EXTEND-FILE-NAME 11Q EXTEND-FILE-NAME) (25Q LIB-FILE 16Q DCOM 6 LIB) () BM:NTH D1 (I 1 LIST I 0 N) A@ (4 NTH) NIL () PREPARE-FOR-THE-NIGHT D1 NIL hNIL NIL () RECORD-DECLARATION D1 (P 0 LST I 2 CHEAP I 1 FIELD-LST I 0 RECORD-NAME F 1 RECORD-DECLARATIONS) mg hcAAoABiBoBh @A BhXdQ /dQ$ddQQ cHi oi i HQc@(143Q ITERPRI 136Q IPRINC 125Q IPRINC 113Q REMOVE 72Q MEMBER 57Q COPY 51Q ERROR 10Q BOUNDP) (5 RECORD-DECLARATIONS) ( 132Q " redefined." 42Q "Illegal cheap flag: " 26Q "Illegal field list: ") RECORD-DECLARATION-LST D1 (P 0 TUPLE I 0 X) @dgH h(15Q APPLY) (11Q RECORD-DECLARATION) () SPELL-NUMBER D1 (L (0 N)) c@djgkg@dlglg@dlglg@dlglg@dlgl g@dl gNIL (140Q TEN 126Q NINE 116Q EIGHT 104Q SEVEN 74Q SIX 62Q FIVE 52Q FOUR 40Q THREE 30Q TWO 16Q ONE 7 ZERO) () CHANGE-MACRO D1 (I 3 VALUE I 2 RECORD I 1 FIELD I 0 RECORD-NAME F 0 RECORD-DECLARATIONS) @Pg@A B ChgggBdggBhhggBdgh@ddi3 g@hhhg@A Bdg Chhig@ddi3 g@hhhh(163Q CELL 150Q GET-FIELD-NUMBER 23Q CELL 17Q GET-FIELD-NUMBER) (215Q QUOTE 177Q ACCESS-ERROR 160Q RECORD-TEMP 143Q RPLACA 124Q QUOTE 103Q RECORD-TEMP 73Q CAR 70Q EQ 55Q RECORD-TEMP 52Q SETQ 42Q LISTP 37Q AND 34Q COND 12Q RPLACA) () SUB-PAIR D1 (I 2 X I 1 L2 I 0 L1 F 3 TEMP-TEMP) @@AIHhSBJciIHBB@AB @AB (74Q SUB-PAIR 65Q SUB-PAIR) NIL () UNIONQ D1 (L (1 LIST2 0 LIST1))  AX@YHdH HXI(21Q MEMB) NIL () *1*ADD1 D1 (I 0 X) @3 j@ @kk(10Q LESSEQP) NIL () *1*AND D1 (L (1 Y 0 X)) @ggAggNIL (23Q *1*TRUE 15Q *1*FALSE 10Q *1*FALSE 3 *1*FALSE) () *1*CONS D1 (L (1 Y 0 X)) @ANIL NIL () *1*COUNT D1 (P 2 ARG I 0 X F 3 *1*BTM-OBJECTS) p@d0dgjg@l@ kj@@ k@g)@dS jHIkIJ ԹHX@ @ k(152Q *1*COUNT 145Q *1*COUNT 131Q *1*COUNT 101Q MEMB 55Q MINUS 42Q *1*COUNT 37Q DTACK-0-ON-END 34Q CHCON) (66Q *1*QUOTE 17Q *1*FALSE 10Q *1*TRUE) () *1*DIFFERENCE D1 (I 1 J I 0 I) @ bA b@Aj(11Q *1*FIX 3 *1*FIX) NIL () *1*EQUAL D1 (L (1 Y 0 X)) @AggNIL (12Q *1*FALSE 6 *1*TRUE) () *1*FALSE D1 NIL gNIL (2 *1*FALSE) () *1*FALSEP D1 (L (0 X)) @gggNIL (14Q *1*FALSE 10Q *1*TRUE 3 *1*FALSE) () *1*FIX D1 (I 0 X) @3 j@ @j(10Q LESSEQP) NIL () *1*IMPLIES D1 (L (1 Y 0 X)) @ggAggNIL (23Q *1*FALSE 15Q *1*FALSE 10Q *1*TRUE 3 *1*FALSE) () *1*LESSP D1 (I 1 Y I 0 X) @ A gg(7 *1*FIX 3 *1*FIX) (21Q *1*FALSE 15Q *1*TRUE) () *1*LISTP D1 (L (0 X)) @gggNIL (21Q *1*TRUE 13Q *1*QUOTE 6 *1*FALSE) () *1*LITATOM D1 (L (0 X)) /@dldgg@@g@gggNIL (54Q *1*FALSE 50Q *1*TRUE 43Q PACK 33Q *1*QUOTE 17Q *1*FALSE 12Q *1*TRUE) () *1*MINUS D1 (I 0 X) @3 ggjhj@ (30Q MINUS) (12Q MINUS 7 *1*QUOTE) () *1*NEGATIVE-GUTS D1 (I 0 X) @3 j@@ j(13Q MINUS) NIL () *1*NEGATIVEP D1 (L (0 X)) '@d3 j@@@g@gggNIL (44Q *1*FALSE 40Q *1*TRUE 33Q MINUS 23Q *1*QUOTE) () *1*NLISTP D1 (L (0 X)) @gggNIL (21Q *1*FALSE 13Q *1*QUOTE 6 *1*TRUE) () *1*NOT D1 (L (0 X)) @gggNIL (14Q *1*FALSE 10Q *1*TRUE 3 *1*FALSE) () *1*NUMBERP D1 (I 0 X) @3 j@ gg(10Q LESSEQP) (20Q *1*FALSE 14Q *1*TRUE) () *1*OR D1 (L (1 Y 0 X)) @gAgggNIL (22Q *1*TRUE 16Q *1*FALSE 11Q *1*FALSE 3 *1*FALSE) () *1*PACK D1 (P 4 TAIL I 0 X) D@ 3@ j*@AH\LI  J KhZLK&gg@h(44Q CHARACTER 37Q TP-IMPLODE 11Q LAST 3 LEGAL-CHAR-CODE-SEQ) (74Q PACK 71Q *1*QUOTE) () *1*PLUS D1 (I 1 Y I 0 X) @ A (7 *1*FIX 3 *1*FIX) NIL () *1*QUOTIENT D1 (I 1 J I 0 I) A bjj@ A(16Q *1*FIX 3 *1*FIX) NIL () *1*REMAINDER D1 (I 1 J I 0 I) A bj@ @ A (25Q REMAINDER 21Q *1*FIX 14Q *1*FIX 3 *1*FIX) NIL () *1*SUB1 D1 (L (0 X)) @3 jj@kNIL NIL () *1*TIMES D1 (I 1 J I 0 I) @ A (7 *1*FIX 3 *1*FIX) NIL () *1*TRUE D1 NIL gNIL (2 *1*TRUE) () *1*TRUEP D1 (L (0 X)) @gggNIL (14Q *1*FALSE 10Q *1*TRUE 3 *1*TRUE) () *1*UNPACK D1 (P 0 TEMP I 0 X) =@dldgdg H jH@g@g@j(36Q LAST 27Q CHCON) (62Q PACK 52Q *1*QUOTE 22Q *1*FALSE 13Q *1*TRUE) () *1*ZERO D1 NIL jNIL NIL () *1*ZEROP D1 (L (0 X)) @3 k@ggNIL (16Q *1*FALSE 12Q *1*TRUE) () ABBREVIATIONP D1 (P 0 ANS I 1 TERM I 0 VARS) @A (7 ABBREVIATIONP1) NIL () ABBREVIATIONP1 D1 (P 1 X I 0 TERM F 2 ANS) 9@ Rhcig@do HiY HX(60Q ABBREVIATIONP1 37Q MEMB) (22Q QUOTE) ( 34Q (IF AND OR NOT IMPLIES)) ACCEPTABLE-TYPE-PRESCRIPTION-LEMMAP D1 (P 33Q LIT P 32Q LOOP-ANS P 30Q CL P 27Q LOOP-ANS P 25Q VAR P 23Q LIT P 17Q CL P 13Q FN P 7 VAR P 6 ARG P 5 CONST P 4 NEGFLG P 3 VARS P 2 CLAUSES P 1 RECOG P 0 TERM I 1 CONCL I 0 HYPS F 34Q MATCH-TEMP F 35Q TEMP-TEMP F 36Q RECOGNIZER-ALIST F 37Q TRUE F 40Q FALSE) g@i gAW>W@hW>h XkH j O Ojh_W<O Ok_O_H Z0Jd0OdO&!O&gO&O&h O&_&iO&dAdg9d4d.d(O&]Mc:dg c:WO&BO&dg:d5d/d)O&MMc:dg c:O&_&LgO&hHhO&_ O" O h_$O &_"O$_O Oh_O&_OZdddc8CW8g:W84W8-W8%W8W8W8W8IW<Jc8W8W8W8W8IW<_Jc8%W8gW8W8W8W8X5Jc8+W8g"W8W8W8h W8XhHH _=iH JO3iKO(ZiHc:dghO_O$ i!h_&d!ddO&IW<NHO&AO&dg9d4d.d'd dO&IW<NHO&@O&dg8d3d-d'O&_NHOH OK [jO&GO&g:O&0O&%O&hO&_O&^HOH OK [hO$_$O__*JO i5h_gHO*hO gO*HhO hO_O(_(Y JmO,O.0H _0O.O0jO2O4_.O,_,_6c:dg gUO4O6d3dg+d&d!_6c:dg W< mc:dg W< _4O2_2~dK i_O Oh_O&_O(2336Q MEMB 2313Q SASSOC 2306Q FN-SYMB0 2260Q SASSOC 2253Q FN-SYMB0 2167Q FN-SYMB0 2102Q SARGS 2055Q FN-SYMB0 2025Q MEMBER 2004Q MEMBER 1706Q ADD-TO-SET 1672Q MEMB 1667Q SARGS 1541Q ADD-TO-SET 1532Q MEMB 1527Q SARGS 1151Q NO-DUPLICATESP 1146Q SARGS 1132Q SARGS 434Q SINGLETON-CONSTRUCTOR-TO-RECOGNIZER 431Q FN-SYMB0 327Q SINGLETON-CONSTRUCTOR-TO-RECOGNIZER 324Q FN-SYMB0 131Q CLAUSIFY 106Q SINGLETON-CONSTRUCTOR-TO-RECOGNIZER 47Q ALL-FNNAMES 41Q EXPAND-NON-REC-FNS 12Q CONJOIN) (2275Q QUOTE 2242Q QUOTE 2212Q NOT 2172Q EQUAL 2156Q QUOTE 2011Q EQUAL 1770Q EQUAL 1563Q EQUAL 1455Q EQUAL 1351Q NOT 1221Q QUOTE 1056Q EQUAL 1003Q EQUAL 630Q NOT 452Q NOT 420Q QUOTE 347Q EQUAL 313Q QUOTE 243Q EQUAL 176Q NOT 15Q IF 5 IF) () ACCESS-ERROR D1 (I 0 REC) og@hg (20Q ERROR1) (15Q HARD 6 REC) ( 3 (PROGN ATTEMPT TO USE A RECORD OF THE WRONG TYPE (!PPR REC NIL))) ADD-AXIOM1 D1 (I 2 TERM I 1 TYPES I 0 NAME) @AB @AB (13Q ADD-LEMMA0 5 CHK-ACCEPTABLE-LEMMA) NIL () ADD-DCELL D1 (I 2 EXPR I 1 *1*NAME I 0 NAME) @gA AgB (17Q ADD-FACT 7 ADD-FACT) (13Q DCELL 3 LISP-CODE) () ADD-ELIM-LEMMA D1 (P 4 X P 3 DESTS P 2 REWRITE-RULE P 1 CONCL P 0 HYPS I 2 TERM I 1 TYPE I 0 NAME F 5 TEMP-TEMP) v@B c dXUYdc dgk h [@HI ZK@dLc dg gJ Lc dg gLdK  h(155Q ADD-FACT 151Q REMOVE 140Q FN-SYMB0 116Q ADD-FACT 107Q FN-SYMB0 55Q CREATE-REWRITE-RULE 46Q DESTRUCTORS 41Q ARGN0 6 UNPRETTYIFY) (143Q ELIMINATE-DESTRUCTORS-DESTS 127Q QUOTE 112Q ELIMINATE-DESTRUCTORS-SEQ 76Q QUOTE 30Q QUOTE) () ADD-EQUATION D1 (P 25Q EQUATION P 24Q TEMP P 23Q EQUATION1 P 3 NEW-POT-+ P 2 NEW-POT-- P 1 TO-DO-NEXT P 0 ADD-EQUATION-ANS I 1 POT-LST I 0 EQUATION F 26Q ADD-EQUATIONS-TO-DO F 27Q TEMP-TEMP) GAA@ K@ c.dhc,@ j`@ dL@hdM`@ dN@h_dOAA@ @d jAA hc,A@ jAAQOTO c,@ c.?@ jq`A_dO@A_dOA_dOoW,c,_& @O& _(_$O"O$h_"_ O_O$&_"`A_dOA_dO@A_dOA@A XhYA[AZW,}dAO* bO* j"O*K h'O* c. O*KJIO*J hO*JK!O$$_& O*O& _(IO$_$O*IIc,HAAKAJj`A_dOdKdJH(753Q CANCEL 743Q TO-BE-IGNOREDP 711Q POLY-MEMBER 662Q CANCEL-POSITIVE 651Q POLY-MEMBER 637Q FIRST-COEFFICIENT 627Q FIRST-VAR 557Q ADD-EQUATION 413Q CANCEL 403Q TO-BE-IGNOREDP 274Q FIRST-COEFFICIENT 264Q CANCEL-POSITIVE 221Q FIRST-COEFFICIENT 207Q POLY-MEMBER 162Q FIRST-COEFFICIENT 150Q FIRST-VAR 110Q FIRST-VAR 60Q FIRST-VAR 44Q FIRST-COEFFICIENT 30Q CANCEL-POSITIVE 22Q TERM-ORDER 17Q FIRST-VAR) (1055Q LINEAR-POT 1047Q LINEAR-POTTYPE# 1034Q LINEAR-POT 1022Q LINEAR-POT 620Q LINEAR-POT 577Q LINEAR-POT 567Q LINEAR-POT 531Q LINEAR-POT 510Q LINEAR-POT 470Q LINEAR-POT 462Q LINEAR-POTTYPE# 353Q LINEAR-POT 332Q LINEAR-POT 311Q LINEAR-POT 303Q LINEAR-POTTYPE# 241Q LINEAR-POT 231Q LINEAR-POT 202Q LINEAR-POT 172Q LINEAR-POT 142Q LINEAR-POT 103Q LINEAR-POTTYPE# 53Q LINEAR-POTTYPE# 11Q LINEAR-POT) () ADD-EQUATIONS D1 (P 6 EQUATION P 1 ADD-EQUATIONS-TO-DO P 0 NEW-EQUATIONS I 1 POT-LST I 0 EQUATIONS F 7 LINEAR-ASSUMPTIONS F 10Q LEMMAS-USED-BY-LINEAR) | @AJ Kb@`A^ 'NcNN cgg N iNL Mh\JZM&dNA bIH XHbh(154Q \NCONC2 144Q ADD-EQUATION 103Q TRUE-POLYP 76Q RETFROM 62Q UNIONQ 30Q IMPOSSIBLE-POLYP) (73Q CONTRADICTION 70Q ADD-EQUATIONS 55Q POLY 47Q POLY 36Q POLY) () ADD-EQUATIONS-TO-POT-LST D1 (P 32Q POT P 30Q PAIR1 P 26Q AND P 25Q POLY P 24Q HYPS P 23Q LEMMAS P 21Q POLY P 17Q SIMPLIFY-CLAUSE-POT-LST P 16Q SIMPLIFY-CLAUSE-POT-LST P 15Q LEMMA P 6 VAR P 2 LST P 1 NEW-VARS P 0 NEW-POT-LST I 2 ALL-NEW-FLG I 1 POT-LST I 0 POLY-LST F 33Q TEMP-TEMP F 34Q TEMPORARILY-DISABLED-LEMMAS F 35Q DISABLED-LEMMAS) P@A Xdgkg_%BAh[#hO_O,Oh__O_7\OLiKO&_HbIMHA OOhbIH^c6dg g OM]_c6W8 ]W6W:Tg ON 0HOO HO i ZO_JO =iJO #O$JH Xggg _"O. hbh_0AO2 iGO0i_4O0O4%O0 O4 O0O4 hO2_2O._.O _ I_*O&O*O(O* O$_$@(1004Q UNION-EQUAL 716Q WORSE-THAN-OR-EQUAL 677Q GREATEREQP 674Q FORM-COUNT 662Q FORM-COUNT 552Q RETFROM 532Q ADD-EQUATIONS 507Q POP-LINEARIZE-ASSUMPTIONS-FRAME 504Q ADD-TO-SET 501Q POP-LEMMA-FRAME 434Q POP-LINEARIZE-ASSUMPTIONS-FRAME 430Q POP-LEMMA-FRAME 421Q LINEARIZE 415Q REWRITE-LINEAR-CONCL 374Q RELIEVE-HYPS 345Q ONE-WAY-UNIFY 331Q PUSH-LINEARIZE-ASSUMPTIONS-FRAME 325Q PRINT-TO-DISPLAY 316Q PUSH-LEMMA-FRAME 300Q MEMB 237Q FN-SYMB0 7 ADD-EQUATIONS) (777Q POLY 770Q POLY 756Q POLY 711Q LINEAR-POT 667Q LINEAR-POT 647Q LINEAR-POT 562Q POLY 547Q CONTRADICTION 544Q ADD-EQUATIONS-TO-POT-LST 536Q CONTRADICTION 474Q LINEAR-LEMMA 410Q LINEAR-LEMMA 367Q LINEAR-LEMMA 360Q LINEAR-LEMMA 337Q LINEAR-LEMMA 322Q LINEAR 267Q LINEAR-LEMMA 242Q LINEAR-LEMMAS 226Q QUOTE 124Q LINEAR-POT 115Q LINEAR-POT 57Q LINEAR-POT 31Q LINEAR-POT 22Q CONTRADICTION 14Q CONTRADICTION) () ADD-FACT D1 (I 2 VAL I 1 PROP I 0 ATM) @d @AB (14Q ADD-SUB-FACT 5 GUARANTEE-CITIZENSHIP) NIL () ADD-GENERALIZE-LEMMA D1 (I 2 TERM I 1 TYPE I 0 NAME) hg`d@dB (24Q ADD-FACT) (6 GENERALIZE-LEMMATYPE# 3 GENERALIZE-LEMMAS) () ADD-LEMMA D1 NIL oi (7 IPRINT) NIL ( 3 (ADD-LEMMA IS UNDEFINED. USE EITHER ADD-AXIOM OR PROVE-LEMMA.)) ADD-LEMMA0 D1 (P 0 TYPE I 2 TERM I 1 TYPES I 0 NAME) ;@ A bB bA$dgHdgh @HBlIh(51Q PACK 15Q TRANSLATE 7 SCRUNCH 3 GUARANTEE-CITIZENSHIP) (42Q -LEMMA 32Q ADD-) () ADD-LESSP-ASSUMPTION-TO-POLY D1 (P 4 TYPE-ALIST P 3 LIT P 1 TERM P 0 TEMP I 2 POLY I 1 Y I 0 X F 5 FALSE F 6 TEMP-TEMP F 7 HEURISTIC-TYPE-ALIST F 10Q LITS-THAT-MAY-BE-ASSUMED-FALSE)  g@AhY XddljlkjBUh\W#WJ1hc ;BVB 9I kjBUh IK KJZBIB B(201Q ADD-TO-SET 152Q COMPLEMENTARYP 123Q TYPE-SET 110Q ADD-TO-SET-EQ 17Q TYPE-SET) (174Q POLY 167Q POLY 136Q POLY 103Q POLY 76Q POLY 42Q POLY 5 LESSP) () ADD-LINEAR-TERM D1 (I 2 POLY I 1 PARITY I 0 TERM) <@ @AB Bg<@3 @mAgBB@BB@@dg+BAgBk؇Bk@AB dgdgJAgBBk@AB ^@oB BBk@AB 8dg@AB @AB g Ag@gB @AB @@B @gB @AB (467Q ADD-LINEAR-TERM 456Q ADD-LINEAR-TERM 442Q ADD-NOT-LESSP-ASSUMPTION-TO-POLY 424Q ADD-LINEAR-TERM 413Q ADD-LINEAR-TERM 356Q ADD-LINEAR-TERM 345Q ADD-LINEAR-TERM 321Q ADD-LINEAR-TERM 271Q ADD-NOT-LESSP-ASSUMPTION-TO-POLY 253Q ADD-LINEAR-TERM 174Q ADD-LINEAR-TERM 11Q ADD-LINEAR-VARIABLE) (452Q POSITIVE 407Q NEGATIVE 375Q POSITIVE 364Q DIFFERENCE 330Q PLUS 302Q POLY 276Q POLY 234Q POLY 230Q POLY 221Q POSITIVE 211Q SUB1 202Q ZERO 155Q POLY 144Q POLY 136Q POSITIVE 132Q POLY 122Q ADD1 102Q POLY 76Q POLY 60Q POLY 54Q POLY 45Q POSITIVE 17Q QUOTE) ( 265Q (QUOTE 1)) ADD-LINEAR-VARIABLE D1 (P 1 TERM P 0 N I 2 POLY I 1 PARITY I 0 VAR F 2 TEMP-TEMP)  @)@g!@@@@@Hc"l@ LBk@AB 7gH3 HmlI BHIAB B(200Q ADD-LINEAR-VARIABLE1 154Q LOGSUBSETP 151Q TYPE-SET 110Q ADD-LINEAR-VARIABLE1 66Q LOGSUBSETP 63Q TYPE-SET) (173Q POLY 162Q POLY 121Q QUOTE 103Q POLY 74Q POLY 13Q TIMES) () ADD-LINEAR-VARIABLE1 D1 (I 3 ALIST I 2 PARITY I 1 VAR I 0 N) \CABg@@ hAC .ACBgC@CԆCC@CCd@ABC ABg@@ C(126Q MINUS 106Q ADD-LINEAR-VARIABLE1 33Q TERM-ORDER 20Q MINUS) (116Q POSITIVE 50Q POSITIVE 10Q POSITIVE) () ADD-LITERAL D1 (P 1 LIT2 I 2 AT-END-FLG I 1 CL I 0 LIT F 2 TRUE-CLAUSE F 3 FALSE F 4 TRUE) G@SA@TRARAHh@A BA@h @I IiHX@A(65Q COMPLEMENTARYP 55Q \APPEND2 41Q MEMBER) NIL () ADD-META-LEMMA D1 (P 2 X P 0 FN I 2 TERM I 1 TYPE I 0 NAME) ?0BA0gBBBBgBBBgBBBBgB}BmB\BKB;B+BBBBBdZg`d@HgdI h(466Q ADD-FACT) (454Q LISP-CODE 442Q REWRITE-RULETYPE# 437Q LEMMAS 172Q MEANING 111Q EQUAL 53Q AND 16Q IMPLIES) () ADD-NOT-EQUAL-0-ASSUMPTION-TO-POLY D1 (P 4 TYPE-ALIST P 3 EQUALITY P 2 TEMP P 1 Y P 0 X I 1 POLY I 0 TERM F 5 FALSE F 6 TEMP-TEMP F 7 ZERO F 10Q LITS-THAT-MAY-BE-ASSUMED-FALSE F 11Q HEURISTIC-TYPE-ALIST) @@d(dg ddd@YHA WAUhA@ddgdd8c %g@Wh[d ZddljAUheg@jAkjQWKW c -AVA 0K ljAUhAgKhA A(336Q ADD-TO-SET 271Q TYPE-SET 256Q ADD-TO-SET-EQ 233Q MEMBER 147Q TYPE-SET 54Q ADD-LESSP-ASSUMPTION-TO-POLY) (331Q POLY 321Q NOT 316Q POLY 305Q POLY 251Q POLY 243Q POLY 177Q QUOTE 166Q POLY 133Q EQUAL 106Q ADD1 65Q POLY 14Q DIFFERENCE) () ADD-NOT-LESSP-ASSUMPTION-TO-POLY D1 (P 5 TYPE-ALIST P 4 LIT P 3 TERM P 1 TERM P 0 TEMP I 2 POLY I 1 Y I 0 X F 6 TEMP-TEMP F 7 LITS-THAT-MAY-BE-ASSUMED-FALSE F 10Q FALSE F 11Q HEURISTIC-TYPE-ALIST)  AoJ@ lj)Wg@hJhc )BVB @B KL LJZg@AhY XddkjbljBWhPWIW c .BVB 1I ljBWhBgIhB B(306Q ADD-TO-SET 240Q TYPE-SET 225Q ADD-TO-SET-EQ 202Q MEMBER 137Q TYPE-SET 111Q COMPLEMENTARYP 101Q ADD-NOT-EQUAL-0-ASSUMPTION-TO-POLY 71Q ADD-TO-SET-EQ 16Q TYPE-SET) (301Q POLY 271Q NOT 266Q POLY 254Q POLY 220Q POLY 212Q POLY 162Q POLY 125Q LESSP 64Q POLY 57Q POLY 32Q NUMBERP) ( 7 (QUOTE 1)) ADD-NUMBERP-ASSUMPTION-TO-POLY D1 (P 3 LIT P 1 TYPE-ALIST P 0 TEMP I 1 POLY I 0 TERM F 4 FALSE F 5 HEURISTIC-TYPE-ALIST F 6 TEMP-TEMP F 7 LITS-THAT-MAY-BE-ASSUMED-FALSE) @ XdljulH AThcUlU@  AThHg@hWJhc #AVA ![H KJZAHA A(200Q ADD-TO-SET 151Q COMPLEMENTARYP 137Q ADD-TO-SET-EQ 60Q LOGSUBSETP 54Q TYPE-SET 25Q LOGSUBSETP 6 TYPE-SET) (173Q POLY 166Q POLY 132Q POLY 125Q POLY 75Q NUMBERP 65Q POLY 32Q POLY) () ADD-PROCESS-HIST D1 (I 4 HIST-ENTRY I 3 DESCENDANTS I 2 PARENT-HIST I 1 PARENT I 0 PROCESS) @ABCD @ADB(10Q IO) NIL () ADD-REWRITE-LEMMA D1 (P 23Q REWRITE-RULE P 22Q TERM P 21Q PAIR2 P 17Q PAIR P 11Q CONCL P 10Q HYPS P 7 TEMP P 6 LST P 5 MAX-TERMS P 4 ALL-VARS-CONCL P 3 ALL-VARS-HYPS P 2 LEMMA P 1 X I 2 TERM I 1 TYPE I 0 NAME F 24Q NO-BUILT-IN-ARITH-FLG F 25Q TEMP-TEMP) B  HhY_I_OO _QW(BOd9dg1d,d&dgdddd=@OO 4g@O 'gOOOOi O O NAO O]_9LO K )NO  iO_ODOh__O__"O%O O" O O" hO _ O&_d`d@O _dOdOdO$O$c*dg gJ dO gO& HX_(640Q ADD-FACT 630Q TOP-FNNAME 607Q ADD-FACT 600Q FN-SYMB0 530Q PREPROCESS-HYPS 462Q SUBBAGP 457Q ALL-VARS-BAG 451Q ALL-VARS-BAG 437Q FORM-COUNT 431Q FORM-COUNT 333Q SUBSETP 330Q UNIONQ 324Q ALL-VARS 256Q ALL-VARS 250Q ALL-VARS-LST 242Q EXTERNAL-LINEARIZE 175Q ADD-FACT 156Q MAKE-REWRITE-RULES 36Q ACCEPTABLE-TYPE-PRESCRIPTION-LEMMAP 3 UNPRETTYIFY) (633Q LEMMAS 603Q LINEAR-LEMMAS 567Q QUOTE 515Q LINEAR-LEMMATYPE# 343Q POLY 265Q POLY 205Q LESSP 165Q TYPE-PRESCRIPTION-LST 106Q LESSP 61Q NOT) () ADD-SHELL-ROUTINES D1 (P 20Q TUPLE P 17Q I P 15Q R P 11Q TEMP P 10Q TUPLE P 3 NAME I 3 DESTRUCTOR-TUPLES I 2 RECOGNIZER I 1 BTM-FN-SYMB I 0 SHELL-NAME F 21Q IN-BOOT-STRAP-FLG) W"G@B0CdIHhZH&JAdh dKggKh h@g@h g0CdIHhZH&Jggg@hCQ LRMh A#AgAh ogAho BgBh Ao@Aho_g@ O6d_gggOh Ohh_O Oh_O&_O_gOgOgOhOhigOh hhh_NOh^L\O&o@ho ClOh_ gO h ogBh Og gO h AhAoo O_Ok_(733Q ADD-DCELL 730Q SUB-PAIR 704Q PACK 666Q CELL 656Q PACK 640Q PACK 603Q ADD-DCELL 600Q SUB-PAIR 521Q PACK 373Q PACK 300Q PACK 264Q ADD-DCELL 261Q SUB-PAIR 237Q PACK 221Q ADD-DCELL 123Q PACK 101Q ADD-FACT 76Q PACK 47Q \APPEND2) (671Q *1* 663Q X 647Q *1* 627Q *1* 506Q *1* 467Q NOT 457Q ONE-OF 447Q COND 363Q *1* 360Q *1*T 355Q EQ 334Q OR 271Q *1* 246Q *1*QUOTE 230Q *1* 171Q QUOTE 166Q *1*SHELL-QUOTE-MARK 163Q LIST 126Q LAMBDA 114Q *1* 67Q *1* 64Q LISP-CODE) ( 725Q (LAMBDA (X) (COND ((EQ (R X) *1*T) (CAR CELL)) (T (DV)))) 720Q (LAMBDA (X) (COND ((AND (EQ (R X) *1*T) (NEQ (CADR X) (QUOTE BTM))) (CAR CELL)) (T (DV)))) 644Q (R CELL DV BTM) 575Q (LAMBDA (X) (COND ((AND (LISTP X) (EQ (CAR X) *1*SHELL-QUOTE-MARK) (EQ (CADR X) (QUOTE SHELL-NAME))) *1*T) (T *1*F))) 566Q (SHELL-NAME) 322Q (LAMBDA (X) (COND ((AND (LISTP X) (EQ (CAR X) *1*SHELL-QUOTE-MARK) (OR (EQ (CADR X) (QUOTE SHELL-NAME)) (EQ (CADR X) (QUOTE BTM)))) *1*T) (T *1*F))) 311Q (SHELL-NAME BTM) 256Q (LAMBDA NIL (QUOTE (*1*SHELL-QUOTE-MARK BTM))) 243Q (*1*SHELL-QUOTE-MARK BTM)) ADD-SHELL0 D1 (P 46Q PAIR P 45Q X P 37Q PAIR P 36Q ARG2 P 35Q ARG1 P 26Q DEST P 22Q PAIR P 21Q X P 13Q ARG-NAME P 12Q DEST-NAME P 11Q NAMES P 10Q NEW-TYPE-NO P 7 TERM P 6 DV P 5 DESTRUCTOR-NAMES P 4 RENAMED-SHELL-EXPR P 3 DESTRUCTOR-ALIST P 2 CURRENT-TYPE-NO P 1 SHELL-EXPR P 0 DEST-EXPRS-X I 3 DESTRUCTOR-TUPLES I 2 RECOGNIZER I 1 BTM-FN-SYMB I 0 SHELL-NAME F 47Q TRUE F 50Q ZERO) 8' _0Cd_O Oh_ O&_O ]@ABC 0C0dO"O"O"BO _O Oh_ O&_O [@ABK MW@M KxdO$__O$_O$Oo@h ogOIhOWNOgOgO ONhh OgBh oggBghhgOghNhh OWN8Ogh ogOgO gINOI hh Ogh ogA$gBghgggA hhhBghggOghhgghhh Ogh ogggghgOghhhh @@M%d_,oh _&O( O&h_*O&&_(O* @oh ogdILhKLIcO2_:O0__O>OWNgO:OgfO^OUOLOi _OOOohg O O OAO";O6 4O6K oKO6 og@gO6hg O4_4(1755Q ERROR1 1716Q SUBSUMES-REWRITE-RULE 1702Q SUBSUMES-REWRITE-RULE 1672Q META-LEMMAP 1652Q MEMB 1610Q TOP-FNNAME 1602Q ERROR1 1553Q ATTEMPT-TO-REWRITE-RECOGNIZER 1501Q SET-DIFF 1476Q ALL-VARS 1465Q INTERSECTP 1462Q ALL-VARS 1403Q SET-DIFF 1400Q ALL-VARS 1367Q INTERSECTP 1364Q ALL-VARS 1340Q ERROR1 1311Q SET-DIFF 1306Q ALL-VARS 1272Q SET-DIFF 1267Q ALL-VARS 1235Q SUBSETP 1232Q ALL-VARS 1207Q ERROR1 1145Q NON-RECURSIVE-DEFNP 1113Q SUBBAGP 1110Q ALL-VARS-BAG 1102Q ALL-VARS-BAG 1070Q FORM-COUNT 1062Q FORM-COUNT 762Q SUBSETP 757Q UNIONQ 753Q ALL-VARS 673Q ERROR1 621Q ALL-VARS 613Q ALL-VARS-LST 605Q ERROR1 552Q EXTERNAL-LINEARIZE 452Q SET-DIFF 437Q SET-DIFF 412Q SUBSETP 404Q ERROR1 372Q TOP-FNNAME 347Q NON-RECURSIVE-DEFNP 344Q TOP-FNNAME 336Q ALL-VARS 273Q ALL-VARS-LST 265Q CREATE-REWRITE-RULE 124Q ERROR1 71Q ERROR1 41Q ACCEPTABLE-TYPE-PRESCRIPTION-LEMMAP 31Q TOP-FNNAME 3 UNPRETTYIFY) (1752Q WARNING 1741Q REWRITE-RULE 1734Q OLDNAME 1727Q NAME 1641Q REWRITE-RULE 1613Q LEMMAS 1577Q WARNING 1570Q NAME 1335Q WARNING 1276Q LST 1261Q VARS 1253Q X 1246Q NAME 1204Q WARNING 1171Q FN 1163Q X 1156Q NAME 773Q POLY 670Q SOFT 661Q NAME 631Q POLY 602Q HARD 505Q LESSP 443Q LST 432Q VARS 425Q NAME 401Q WARNING 365Q FN 360Q NAME 307Q EQUAL 207Q LESSP 162Q NOT 136Q QUOTE 121Q SOFT 112Q NAME 100Q IF 66Q SOFT 57Q NAME) ( 1724Q (PROGN THE NEWLY PROPOSED LEMMA , (!PPR NAME NIL) , COULD BE APPLIED WHENEVER THE PREVIOUSLY ADDED LEMMA (!PPR OLDNAME NIL) COULD %. // //) 1707Q (PROGN THE PREVIOUSLY ADDED LEMMA , (!PPR OLDNAME NIL) , COULD BE APPLIED WHENEVER THE NEWLY PROPOSED (!PPR NAME NIL) COULD !) 1565Q (PROGN (!PPR NAME NIL) WILL SLOW DOWN THE THEOREM-PROVER BECAUSE IT WILL CAUSE BACKWARD CHAINING ON EVERY INSTANCE OF A PRIMITIVE TYPE EXPRESSION %.) 1243Q (PROGN WHEN THE LINEAR LEMMA (!PPR NAME NIL) IS STORED UNDER (!PPR X NIL) IT CONTAINS THE FREE (PLURAL? VARS VARIABLES VARIABLE) (!LIST VARS) WHICH WILL BE CHOSEN BY INSTANTIATING THE (PLURAL? LST HYPOTHESES HYPOTHESIS) (!PPR-LIST LST) %.) 1153Q (PROGN NOTE THAT THE LINEAR LEMMA (!PPR NAME NIL) IS BEING STORED UNDER THE TERM (!PPR X NIL) , WHICH IS UNUSUAL BECAUSE (!PPR FN NIL) IS A NONRECURSIVE FUNCTION SYMBOL %.) 656Q (PROGN (!PPR NAME NIL) IS AN UNACCEPTABLE REWRITE LEMMA BECAUSE THE NLISTP OF ITS CONCLUSION IS A LESSP AND IT CANNOT BE HANDLED BY OUR LINEAR ARITHMETIC PACKAGE. TO BE ACCEPTABLE, AT LEAST ONE NONVARIABLE ADDEND OF THE CONCLUSION MUST SATISFY TWO PROPERTIES. FIRST, IT MUST CONTAIN ALL THE VARIABLES OF THE LEMMA THAT ARE NOT IN THE HYPOTHESES. SECOND, IT MUST NOT BE THE CASE THAT UNDER EVERY SUBSTITUTION, THE TERM IS SMALLER THAN ANOTHER ADDEND OF THE CONCLUSION. %.) 576Q (PROGN LINEARIZE RETURNED A LIST OF MORE THAN ONE THING , EVEN THOUGH CALLED ON A LESSP NLISTP !) 422Q (PROGN NOTE THAT (!PPR NAME NIL) CONTAINS THE FREE (PLURAL? VARS VARIABLES VARIABLE) (!LIST VARS) WHICH WILL BE CHOSEN BY INSTANTIATING THE (PLURAL? LST HYPOTHESES HYPOTHESIS) (!PPR-LIST LST) %.) 355Q (PROGN NOTE THAT THE REWRITE RULE (!PPR NAME NIL) WILL BE STORED SO AS TO APPLY ONLY TO TERMS WITH THE NONRECURSIVE FUNCTION SYMBOL (!PPR FN NIL) %.) 107Q (PROGN (!PPR NAME NIL) IS AN UNACCEPTABLE REWRITE LEMMA BECAUSE IT REWRITES AN IF-EXPRESSION %.) 54Q (PROGN (!PPR NAME NIL) IS AN UNACCEPTABLE REWRITE LEMMA BECAUSE IT REWRITES A VARIABLE %.)) CHK-ACCEPTABLE-SHELL D1 (P 24Q X P 23Q LOOP-ANS P 21Q X P 17Q NAME P 13Q TUPLE P 7 FLG P 6 L P 5 TR P 4 DV P 3 AC P 2 AXIOM-NAMES P 1 NAMES P 0 DESTRUCTOR-NAMES I 3 DESTRUCTOR-TUPLES I 2 RECOGNIZER I 1 BTM-FN-SYMB I 0 SHELL-NAME F 25Q RECOGNIZER-ALIST F 26Q *1*BTM-OBJECTS) X C O 0CD_OOOohg O_d_O Oh_O&_OX@BHYAdj@mjAlj2JI#@kJjJA L Mh\JkZM&KXdVHgHlj2JI)j@kJjJA L Mh\JkZM&KXdWgH(172Q DUMB-NEGATE-LIT 167Q CONVERT-TYPE-NO-TO-RECOGNIZER-TERM 65Q CONVERT-TYPE-NO-TO-RECOGNIZER-TERM) (235Q AND 131Q OR) () DUMB-IMPLICATE-LITS D1 (L (1 L2 0 L1) F 0 TRUE F 1 TEMP-TEMP F 2 FALSE) "@cg@APhg@RPANIL (25Q QUOTE 10Q IF) () DUMB-NEGATE-LIT D1 (I 0 TERM F 0 FALSE F 1 TRUE F 2 TEMP-TEMP) 6@ g@hg@PQP@cdg g@(52Q FN-SYMB0) (55Q NOT 41Q QUOTE 17Q QUOTE 6 NOT) () DUMB-OCCUR D1 (P 1 ARG I 1 Y I 0 X) 0@A%AhgAHh@I IiHX(43Q DUMB-OCCUR) (16Q QUOTE) () DUMB-OCCUR-LST D1 (P 1 TERM I 1 LST I 0 X) AHh@I IiHX(20Q DUMB-OCCUR) NIL () DUMP D1 (P 5 L P 2 I P 0 PAIRS I 5 SCRIBE-FLG I 4 INDEX-FLG I 3 WIDTH I 2 INDENT I 1 FILE I 0 LST) iBlbClDbAg bdC @k2Ih]dlg]dg%kM lM lM lM DJ dg%kM lM lM lM DJ dgkM lM lM DJ dg$kM lM lM lM DJ tdgkM lM DJ XdgkM lM lM DJ 6dghkM hDJ ghkM iDJ MDJ kM JKLhIJkԺL&(517Q BM:NTH 511Q DUMP-OTHER 500Q DUMP-TOGGLE 470Q BM:NTH 453Q DUMP-TOGGLE 443Q BM:NTH 423Q DUMP-TOGGLE 414Q BM:NTH 406Q BM:NTH 400Q BM:NTH 361Q DUMP-DCL 352Q BM:NTH 344Q BM:NTH 325Q DUMP-ADD-SHELL 315Q BM:NTH 307Q BM:NTH 301Q BM:NTH 273Q BM:NTH 253Q DUMP-ADD-AXIOM 244Q BM:NTH 236Q BM:NTH 230Q BM:NTH 210Q DUMP-PROVE-LEMMA 200Q BM:NTH 172Q BM:NTH 164Q BM:NTH 156Q BM:NTH 136Q DUMP-DEFN 126Q BM:NTH 120Q BM:NTH 112Q BM:NTH 104Q BM:NTH 36Q LINEL 27Q OPENSTREAM) (460Q ENABLE 431Q DISABLE 367Q TOGGLE 333Q DCL 262Q ADD-SHELL 217Q ADD-AXIOM 145Q PROVE-LEMMA 73Q DEFN 64Q EVENT 24Q OUTPUT) () DUMP-ADD-AXIOM D1 (I 3 INDEX I 2 THM I 1 TYPES I 0 NAME F 0 FILE F 1 INDENT) ZP C>QP oP @P AkP A gP QP BQjP P P P oP QP ٰ(125Q IPOSITION 117Q IPRINC 106Q IPRINC 101Q DUMP-END-GROUP 75Q ITERPRI 71Q PPRINDENT 62Q SPACES 55Q IPRINT 45Q DUMP-LEMMA-TYPES 40Q SPACES 31Q IPRINC 24Q IPRINC 13Q ISPACES 3 DUMP-BEGIN-GROUP) (51Q :) ( 113Q "." 20Q "AXIOM.") DUMP-ADD-SHELL D1 (I 4 INDEX I 3 ACCESSORS I 2 RECOG I 1 BTM I 0 CONSTRUCTOR F 3 FILE F 4 INDENT F 5 TRUE) S D1TS ogBgAgCg@gC g0C(S oS TS ٰdIHhZH&JgCHhg0C+YiIUIiHXdIHhZH&Jg0CdIHhZH&JhTS S S (337Q DUMP-END-GROUP 333Q ITERPRI 327Q PRINEVAL 110Q IPOSITION 102Q IPRINC 71Q IPRINC 53Q LENGTH 13Q ISPACES 3 DUMP-BEGIN-GROUP) (252Q DEFAULTS 162Q RESTRICTIONS 144Q FLG 57Q NAMES 47Q N 42Q CONSTRUCTOR 35Q ACCESSORS 30Q BTM 23Q RECOG) ( 76Q "." 20Q (PROGN SHELL DEFINITION %. // ADD THE SHELL (!PPR CONSTRUCTOR NIL) OF (@ N) (PLURAL? ACCESSORS ARGUMENTS ARGUMENT) WITH // (COND (BTM BOTTOM OBJECT (!PPR BTM (PQUOTE ,) NIL) //)) RECOGNIZER (!PPR RECOG NIL) , // (PLURAL? ACCESSORS ACCESSORS ACCESSOR) (!PPR-LIST NAMES) , // (COND (FLG TYPE (PLURAL? ACCESSORS RESTRICTIONS RESTRICTION) (!PPR-LIST RESTRICTIONS) , //)) AND DEFAULT (PLURAL? ACCESSORS VALUES VALUE) (!PPR-LIST DEFAULTS NIL) %.)) DUMP-BEGIN-GROUP D1 (I 0 FILE F 0 SCRIBE-FLG) Pg@ @ g@ @ (30Q ITERPRI 24Q PRIN1 15Q ITERPRI 11Q PRIN1) (20Q @BEGIN 5 @BEGIN) () DUMP-DCL D1 (I 2 INDEX I 1 ARGS I 0 FN F 0 FILE F 1 INDENT) AP B%QP oP P QP @AP P P oP QP ٰ(74Q IPOSITION 66Q IPRINC 55Q IPRINC 50Q DUMP-END-GROUP 44Q IPRINT 35Q ISPACES 30Q ITERPRI 24Q IPRINC 13Q ISPACES 3 DUMP-BEGIN-GROUP) NIL ( 62Q "." 20Q "UNDEFINED FUNCTION.") DUMP-DEFN D1 (I 4 INDEX I 3 HINT I 2 BODY I 1 ARGS I 0 FN F 0 FILE F 1 INDENT) P DQP oP P QP @AP QlP gP QP BQjP P CjQP oP CdGoP CP QlP oP CP 'P oP QP ٱkQljP P P (266Q DUMP-END-GROUP 261Q ITERPRI 254Q PPRINDENT 237Q IPOSITION 231Q IPRINC 220Q IPRINC 212Q IPRINT 201Q IPRINC 170Q ISPACES 157Q IPRINT 147Q IPRINC 130Q IPRINC 117Q ISPACES 107Q ITERPRI 103Q PPRINDENT 74Q ISPACES 67Q IPRINT 60Q ISPACES 50Q IPRINT 41Q ISPACES 34Q ITERPRI 30Q IPRINC 17Q ISPACES 3 DUMP-BEGIN-GROUP) (63Q IEQP) ( 225Q "." 175Q "AND THE MEASURE" 143Q "CONSIDER THE WELL-FOUNDED RELATION" 124Q "HINT:" 24Q "DEFINITION.") DUMP-END-GROUP D1 (I 0 FILE F 0 SCRIBE-FLG) Pg@ @ g@ @ @ (34Q ITERPRI 30Q ITERPRI 24Q PRIN1 15Q ITERPRI 11Q PRIN1) (20Q @END 5 @END) () DUMP-HINTS D1 (P 13Q TL P 12Q PAIR P 11Q X P 3 ENABLED P 2 DISABLED P 1 USED P 0 INDENT I 0 HINT F 14Q FILE F 15Q INDENT F 16Q PPR-MACRO-LST) D WAg@Yg@ZI1MN[JA M0NZ0@dJ _OOh_^M]O&__IO_OOh_M]O&_d\dgKgI!gIgKhgJhgJLh]NDM_^ObHW @IoW Hlظ@[oW Hl ^Md HW W Odg#oW OW oW dgoW W Ord HkW OW OPoW O4d OW oW OW OoW oW W ldg&oW ogOhW W :g$oW ogOhW W OW jWW W h(1066Q ITERPRI 1060Q PPRIND 1047Q IPOSITION 1037Q PRINEVAL 1032Q IPOSITION 1007Q IPRINC 766Q PRINEVAL 761Q IPOSITION 736Q IPRINC 706Q ITERPRI 700Q IPRINC 661Q IPRINC 643Q IPRINC 630Q IPRINC 616Q IPRINC 574Q IPRINC 555Q IPRINC 544Q ISPACES 522Q ITERPRI 514Q IPRINC 466Q IPRINC 454Q IPRINC 442Q IPRINC 415Q ISPACES 407Q IPOSITION 367Q LAST 356Q IPRINC 327Q IPRINC 306Q ISPACES 66Q MEMB) (1017Q X 773Q DISABLE 746Q X 721Q ENABLE 475Q USE 425Q INDUCT 246Q DISABLE 235Q DISABLE 223Q ENABLE 216Q USE 207Q USE 176Q USE 16Q DISABLE 7 USE) ( 1014Q (!LIST X) 1002Q "DISABLE" 743Q (!LIST X) 731Q "ENABLE" 673Q "}" 654Q "," 623Q "/" 567Q "WITH {" 507Q "CONSIDER:" 461Q "." 435Q "INDUCT AS FOR" 351Q "HINTS:" 322Q "HINT:") DUMP-LEMMA-TYPES D1 (P 0 TAIL I 0 TYPES F 1 FILE) SoQ @=dHdgg Q HdoQ oQ kQ oQ (120Q IPRINC 103Q ISPACES 75Q IPRINC 64Q IPRINC 43Q IPRINC 37Q L-CASE 7 IPRINC) (32Q ELIMINATION 24Q ELIM) ( 114Q ")" 71Q "," 60Q "AND" 3 "(") DUMP-OTHER D1 (I 1 INDEX I 0 X F 0 FILE F 1 INDENT) 9P AQP @P jhP P P P oP QP ٰ(64Q IPOSITION 56Q IPRINC 45Q IPRINC 40Q DUMP-END-GROUP 34Q ITERPRI 30Q PPRIND 21Q IPOSITION 13Q ISPACES 3 DUMP-BEGIN-GROUP) NIL ( 52Q ".") DUMP-PROVE-LEMMA D1 (I 4 INDEX I 3 HINT I 2 THM I 1 TYPES I 0 NAME F 0 FILE F 1 INDENT) cP DGQP oP @P AkP A gP QP BQjP P CP  P oP QP ٰ(136Q IPOSITION 130Q IPRINC 117Q IPRINC 110Q DUMP-HINTS 104Q DUMP-END-GROUP 75Q ITERPRI 71Q PPRINDENT 62Q ISPACES 55Q IPRINT 45Q DUMP-LEMMA-TYPES 40Q ISPACES 31Q IPRINC 24Q IPRINC 13Q ISPACES 3 DUMP-BEGIN-GROUP) (51Q :) ( 124Q "." 20Q "THEOREM.") DUMP-TOGGLE D1 (I 3 INDEX I 2 FLG I 1 OLDNAME I 0 NAME F 0 FILE F 1 INDENT) LP CQP BoP oP QP ٰoP AP oP P P (111Q DUMP-END-GROUP 105Q ITERPRI 101Q IPRINC 71Q IPRINC 63Q IPRINC 50Q IPOSITION 42Q IPRINC 31Q IPRINC 13Q ISPACES 3 DUMP-BEGIN-GROUP) NIL ( 75Q "." 57Q "ENABLE" 36Q "." 23Q "DISABLE") ELIMINABLE-VAR-CANDS D1 (I 1 HIST I 0 CL F 0 ELIM-VARIABLE-NAMES1) @ P (7 SET-DIFF 3 ALL-VARS-LST) NIL () ELIMINABLEP D1 (P 1 LIT I 0 SET F 2 TEMP-TEMP) @H@i@ kj@ H,i@ x@cdg Y hHXhHX gE@cdgk Hi%@cdghHXk (254Q NO-DUPLICATESP 251Q SARGS 246Q ARGN0 176Q SARGS 173Q ARGN0 143Q FN-SYMB0 112Q PRIMITIVEP 64Q NO-DUPLICATESP 61Q SARGS 42Q SARGS 23Q LENGTH) (222Q QUOTE 162Q QUOTE 146Q NOT 77Q QUOTE) () ELIMINATE-DESTRUCTORS-CANDIDATEP D1 (P 6 V P 5 ARG P 1 VAR P 0 LEMMA I 0 TERM F 7 TEMP-TEMP F 10Q TEMPORARILY-DISABLED-LEMMAS F 11Q DISABLED-LEMMAS)  @gXddcW WWh@g@KJhYdV@g@"LHLKJKi@^HIM hLKbe(213Q OCCUR 31Q MEMB) (177Q REWRITE-RULE 133Q REWRITE-RULE 110Q ELIMINATE-DESTRUCTORS-DESTS 51Q ELIMINATE-DESTRUCTORS-DESTS 20Q REWRITE-RULE 7 ELIMINATE-DESTRUCTORS-SEQ) () ELIMINATE-DESTRUCTORS-CANDIDATES D1 (P 0 ANS I 0 CL) @d H (22Q MERGE-DESTRUCTOR-CANDIDATES 11Q ELIMINATE-DESTRUCTORS-CANDIDATES1) NIL () ELIMINATE-DESTRUCTORS-CANDIDATES1 D1 (I 0 TERM F 0 ANS F 1 TEMP-TEMP) ,@ @dghd @ cd@hP c(47Q ADD-TO-SET 33Q ELIMINATE-DESTRUCTORS-CANDIDATEP 22Q ELIMINATE-DESTRUCTORS-CANDIDATES1) (11Q QUOTE) () ELIMINATE-DESTRUCTORS-CLAUSE D1 (P 60Q PAIR P 57Q POCKET P 45Q POCKET P 40Q HYP P 33Q HYP P 22Q CAND P 21Q CAND-TAIL P 15Q INST-HYPS P 14Q INST-LHS P 13Q INST-RHS P 12Q INST-DESTS P 11Q ALIST P 10Q DESTS P 7 RHS P 6 LHS P 5 HYPS P 4 REWRITE-RULE P 3 CANDS P 2 TO-DO P 1 NEW-CL P 0 ELIMINABLES I 1 HIST I 0 CL F 61Q PROCESS-CLAUSES F 62Q PROCESS-HIST F 63Q GENERALIZING-SKOS F 64Q TRUE-CLAUSE F 65Q ALL-LEMMAS-USED F 66Q OBVIOUS-RESTRICTIONS F 67Q GENERALIZE-LEMMA-NAMES) 1@dA @ hhZhcbdcdJWdbJJJHK @Wbcb!O _"h@Wbcb_$g\LL_O$g_O$ORO(_0O&O*_O _H MO4iOO _OM _ON _OA O8O:J @OOOO WhIGIWfOH WdO"A%OBODI A*OL2ON hJLOWlWnOOWfO hWdcdO"i_2O0O2_.O,O.h_,_*O(_(O&_&O.&_,_6OO6 @ hO4_4_@WhO@@ Y*IHWdO"A/OV)OXh_>O<O>h_<_:O8_8O>&_<_^O O^_\OZO\h_Z_XOV_VO\&_Z_JI OJ_HOFOHh_F_DOB_BOH&_F_Th__hOT_ROP(ORh_P_NOL_L_Wf OiOOR&_PO"d0O`O`Wj cjWb cbWdhh(1351Q SCRUNCH-CLAUSE-SET 1335Q UNION-EQUAL 1332Q ADD-TO-SET 1254Q MEMB 1125Q OCCUR-LST 1052Q MEMBER 745Q ADD-LITERAL 714Q MEMBER 710Q SUBLIS-VAR 564Q SUB-PAIR-EXPR 526Q SORT-DESTRUCTOR-CANDIDATES 523Q MERGE-DESTRUCTOR-CANDIDATES 520Q UNION-EQUAL 476Q ELIMINATE-DESTRUCTORS-CANDIDATES 444Q UNIONQ 441Q REMOVE 421Q ELIMINATE-DESTRUCTORS-CLAUSE1 403Q \APPEND2 353Q SUBLIS-VAR 342Q SUBLIS-VAR-LST 331Q SUBLIS-VAR-LST 273Q MEMB 265Q SUBLIS-VAR 22Q SORT-DESTRUCTOR-CANDIDATES 17Q ELIMINATE-DESTRUCTORS-CANDIDATES 13Q ELIMINABLE-VAR-CANDS) (541Q REWRITE-RULE 212Q ELIMINATE-DESTRUCTORS-DESTS 174Q REWRITE-RULE 163Q REWRITE-RULE 154Q REWRITE-RULE 147Q ELIMINATE-DESTRUCTORS-SEQ) () ELIMINATE-DESTRUCTORS-CLAUSE1 D1 (P 3 HYP P 2 CL1 P 1 GEN-LHS P 0 GEN-CL I 4 DESTS I 3 RHS I 2 LHS I 1 HYPS I 0 CL F 4 ELIM-VARIABLE-NAMES1 F 5 GENERALIZING-SKOS) 30@ZA dK J ZJDT XDUB YdCH (60Q SUBST-VAR-LST 51Q SUB-PAIR-EXPR 42Q GENERALIZE1 26Q ADD-LITERAL 22Q NEGATE-LIT 10Q REVERSE) NIL () ELIMINATE-DESTRUCTORS-SENT D1 (I 1 HIST I 0 CL) g@Agg (16Q EXECUTE) (12Q FERTILIZE-SENT 7 SIMPLIFY-SENT 2 ELIMINATE-DESTRUCTORS-CLAUSE) () ELIMINATE-IRRELEVANCE-CLAUSEA0001 D1 (I 1 Y I 0 X) @A @A @A (26Q UNION-EQUAL 17Q UNION-EQUAL 6 INTERSECTP) NIL () ELIMINATE-IRRELEVANCE-CLAUSE D1 (P 10Q PAIR P 5 LIT P 1 ELIMINABLES P 0 PARTITION I 1 HIST I 0 CL F 15Q STACK F 16Q PROCESS-CLAUSES F 17Q PROCESS-HIST)  gW;@@d] MhKJh\J&Lg Xd!N OYdh_ OO _N^@1 OOhchcidI _OOh__O_O&_(170Q MEMB 124Q \NCONC2 113Q ELIMINABLEP 62Q TRANSITIVE-CLOSURE 26Q ALL-VARS) (57Q ELIMINATE-IRRELEVANCE-CLAUSEA0001 5 BEING-PROVED) () ELIMINATE-IRRELEVANCE-SENT D1 (I 1 HIST I 0 CL) g@Agd (14Q EXECUTE) (7 STORE-SENT 2 ELIMINATE-IRRELEVANCE-CLAUSE) () EQUATIONAL-PAIR-FOR D1 (I 1 POLY I 0 WINNING-PAIR) !@gA h@A (35Q CONS-PLUS 32Q BUILD-SUM 15Q ABS) (25Q POLY 10Q POLY 4 QUOTE) () ERASE-EOL D1 NIL g (5 CURSORPOS) (2 L) () ERASE-EOP D1 NIL g (5 CURSORPOS) (2 E) () ERROR1 D1 (I 2 HARDNESS I 1 ALIST I 0 SENTENCE F 0 PROVE-FILE F 1 TTY-FILE F 2 IN-REDO-UNDONE-EVENTS-FLG) pg@gBAbBgboAjP QPoAjQ BghAbBgRhi gg g@Ah (155Q ERROR 140Q RETFROM 127Q BREAK1 76Q DETACHED-ERROR 72Q DETACHEDP 56Q PRINEVAL 40Q PRINEVAL) (144Q ERROR1 135Q *****ERROR***** 132Q APPLY 115Q SOFT 63Q WARNING 23Q HARD 7 HARDNESS 2 SENTENCE) ( 50Q (PROGN // (COND ((EQ HARDNESS (QUOTE WARNING)) WARNING) ((EQ HARDNESS (QUOTE HARD)) FATAL ERROR) (T ERROR)) : (@ SENTENCE) // //) 32Q (PROGN // (COND ((EQ HARDNESS (QUOTE WARNING)) WARNING) ((EQ HARDNESS (QUOTE HARD)) FATAL ERROR) (T ERROR)) : (@ SENTENCE) // //)) EVENT-FORM D1 (L (0 X)) @l@g@g @ggNIL (34Q EVENT 30Q MAIN-EVENT 21Q MAIN-EVENT 12Q EVENT) () EVENT1-OCCURRED-BEFORE-EVENT2 D1 (L (2 EVENT-LST 1 EVENT2 0 EVENT1)) @AB  i(11Q MEMB 5 MEMB) NIL () EVENTS-SINCE D1 (I 0 EVENT F 4 CHRONOLOGY) :@T @gT1Hd@I gJ KhZHXK&(37Q DREVERSE 4 MEMB) (44Q EVENT 12Q EVENT) () EVG D1 (P 3 ARG P 2 RESTRICTION I 0 Y F 4 *1*BTM-OBJECTS F 5 SHELL-ALIST F 6 TEMP-TEMP) @d+d3 j ll gl@dgk hlg@@ h@ @ j@dT )U@@g"IHij@g*@ 9[ c dJ hIH@dgjo h@g@ @ l(365Q EVG 356Q EVG 332Q MEMB 266Q LOGSUBSETP 250Q EVG 241Q LEGAL-CHAR-CODE-SEQ 151Q MEMB 130Q ARITY 122Q LENGTH 103Q LAST 47Q ILLEGAL-NAME 14Q GREATEREQP) (344Q TYPE-PRESCRIPTION-LST 311Q MINUS 261Q TYPE-RESTRICTION 227Q PACK 176Q TYPE-RESTRICTIONS 61Q *1*QUOTE 40Q *1*FALSE 26Q *1*TRUE) ( 327Q (ADD1 ZERO CONS)) EVG-OCCUR-LEGAL-CHAR-CODE-SEQ D1 (P 4 ARG P 2 TAIL P 1 J I 1 EVG I 0 L) AMAdgVgPAd3 J @ ?@A @ kHJJiAI)jJIkԹg AKh@L LiK[@A@A Ab|(176Q EVG-OCCUR-LEGAL-CHAR-CODE-SEQ 150Q EVG-OCCUR-LEGAL-CHAR-CODE-SEQ 53Q LENGTH-TO-ATOM 47Q NCHARS 36Q LENGTH-TO-ATOM 32Q NCHARS) (122Q *1*QUOTE 16Q *1*FALSE 10Q *1*TRUE) () EVG-OCCUR-NUMBER D1 (P 3 ARG P 1 I I 1 EVG I 0 N) AYAdgbg\A3 j@@A@A j@A@dlZ:l- @A kIH&@AI) IiIkYg AJh@K KiJZ@A Abu(205Q EVG-OCCUR-NUMBER 164Q EVG-OCCUR-NUMBER 116Q LESSEQP 76Q NCHARS 70Q LESSEQP 46Q LESSEQP 43Q ABS) (136Q *1*QUOTE 16Q *1*FALSE 10Q *1*TRUE) () EVG-OCCUR-OTHER D1 (P 1 ARG I 1 EVG I 0 X) @@A&Ahg AHh@I IiHX@A Ab(65Q EVG-OCCUR-OTHER 44Q EVG-OCCUR-OTHER) (16Q *1*QUOTE) () EXECUTE D1 (P 1 CL1 P 0 NEW-HIST I 4 NO-CHANGE-EXIT I 3 NORMAL-EXIT I 2 HIST I 1 CL I 0 PROCESS F 2 PROCESS-CLAUSES F 3 PROCESS-HIST) 4ABl@!@ABRS XRdIHlChABlD(24Q ADD-PROCESS-HIST) NIL () EXPAND-ABBREVIATIONS D1 (P 20Q LEMMA P 16Q ARG P 15Q V P 7 ARG P 3 LHS P 2 RHS P 1 LEMMA P 0 TEMP I 1 ALIST I 0 TERM F 21Q MATCH-TEMP F 22Q ABBREVIATIONS-USED F 23Q TEMP-TEMP F 24Q FNS-TO-BE-IGNORED-BY-REWRITE F 25Q UNIFY-SUBST F 26Q TEMPORARILY-DISABLED-LEMMAS F 27Q DISABLED-LEMMAS) @@dA@g@dW( +0@dOA MLh^L&N  X @0@H @W$ c$H@HRO_OObbm_OOA _OOh__O_O_O&_dOA MLh^L&N bddggO!hY@W$ c$JW*bb_ c&W, /W&W.&O O O O c" O_gW"W"W"W"W"K J K@ O d(633Q ONE-WAY-UNIFY 624Q ABBREVIATIONP 620Q ALL-VARS-BAG 500Q META-LEMMAP 460Q MEMB 423Q ADD-TO-SET 351Q CONS-TERM 323Q EXPAND-ABBREVIATIONS 241Q EXPAND-ABBREVIATIONS 154Q ADD-TO-SET 143Q ABBREVIATIONP 116Q NON-RECURSIVE-DEFNP 111Q CONS-TERM 63Q EXPAND-ABBREVIATIONS 37Q MEMB) (552Q EQUAL 530Q REWRITE-RULE 520Q REWRITE-RULE 507Q REWRITE-RULE 447Q REWRITE-RULE 414Q REWRITE-RULE 371Q LEMMAS 361Q QUOTE 22Q QUOTE) () EXPAND-AND-ORS D1 (P 7 LEMMA P 5 C3 P 4 C2 P 3 LHS P 2 RHS P 1 LEMMA P 0 TEMP I 1 BOOL I 0 TERM F 10Q MATCH-TEMP F 11Q ABBREVIATIONS-USED F 12Q TEMP-TEMP F 13Q UNIFY-SUBST F 14Q DISABLED-LEMMAS F 15Q FALSE F 16Q TEMPORARILY-DISABLED-LEMMAS) `@hg@ X1@gNhYdW cWJ c?Wg6W0W)W!WWWLAPMAKAWHc~WgHckWg`WXWOWF@W cH@H _cW /WW&O OOOcN^gWWWWWZJgJJJoJJLAMAK@ O(621Q ONE-WAY-UNIFY 414Q META-LEMMAP 374Q MEMB 354Q EXPAND-ABBREVIATIONS 351Q SUB-PAIR-VAR 333Q ADD-TO-SET 105Q EXPAND-ABBREVIATIONS 102Q SUBLIS-VAR 72Q ADD-TO-SET 24Q NON-RECURSIVE-DEFNP) (537Q COND 465Q EQUAL 444Q REWRITE-RULE 434Q REWRITE-RULE 423Q REWRITE-RULE 363Q REWRITE-RULE 265Q OR 242Q AND 124Q IF 63Q REWRITE-RULE 34Q LEMMAS 14Q QUOTE) ( 565Q (& C2 C3)) EXPAND-BOOT-STRAP-NON-REC-FNS D1 (I 0 TERM) U@@g@do g@@g b0@d IHhZH&J (122Q CONS-TERM 75Q EXPAND-BOOT-STRAP-NON-REC-FNS 55Q SUB-PAIR-VAR 26Q MEMB) (46Q SDEFN 34Q SDEFN 11Q QUOTE) ( 23Q (AND OR NOT IMPLIES FIX ZEROP NLISTP)) EXPAND-NON-REC-FNS D1 (I 0 TERM) R@@g@ @g@@g b@0@d IHhZH&J (117Q CONS-TERM 72Q EXPAND-NON-REC-FNS 51Q SUB-PAIR-VAR 21Q NON-RECURSIVE-DEFNP) (42Q SDEFN 30Q SDEFN 11Q QUOTE) () EXPAND-PPR-MACROS D1 (P 0 PPR-MACRO-LST I 0 TERM F 5 TEMP-TEMP F 6 PPR-MACRO-LST) iV@d`Hc @0@J@kIc dgUU0Ud KJh\J&Ld KJh\J&L(123Q EXPAND-PPR-MACROS 72Q EXPAND-PPR-MACROS) (51Q QUOTE) () EXTEND-ALIST D1 (P 4 X I 1 ALIST2 I 0 ALIST1) *A@AHI \ALJ KhZHXK&(15Q \APPEND2) NIL () EXTERNAL-LINEARIZE D1 (P 1 LITS-THAT-MAY-BE-ASSUMED-FALSE P 0 HEURISTIC-TYPE-ALIST I 1 FLG I 0 TERM)  @A (7 LINEARIZE) NIL () EXTRACT-DEPENDENCIES-FROM-HINTS D1 (P 2 LOOP-ANS P 1 HINT I 0 HINTS) N@!HJYdg0IdLKh]K&MgI hJ HX(106Q UNIONQ 102Q NIL 73Q TRANSLATE) (63Q INDUCT 20Q USE) () FALSE-NONFALSEP D1 (P 0 TEMP I 0 TERM F 1 DEFINITELY-FALSE F 2 TEMP-TEMP F 3 FALSE) 3@cddgSci XdkjicjHkjhci(30Q TYPE-SET) (15Q QUOTE) () FAVOR-COMPLICATED-CANDIDATESA0001 D1 (P 2 TERM I 0 CAND F 3 TEMP-TEMP) 7@ @jHIZcdg IkعHX(53Q PRIMITIVE-RECURSIVEP 50Q FN-SYMB0) (37Q QUOTE 11Q CANDIDATE 3 CANDIDATE) () FAVOR-COMPLICATED-CANDIDATES D1 (I 0 CANDLST) @g (6 MAXIMAL-ELEMENTS) (3 FAVOR-COMPLICATED-CANDIDATESA0001) () FERTILIZE-CLAUSE D1 (P 21Q LIT2 P 14Q LIT2 P 12Q LIT P 10Q DIRECTION P 7 CROSS-FERT-FLG P 6 MASS-SUBST-FLG P 5 DONT-DELETE-LIT-FLG P 4 RHS2 P 3 LHS2 P 2 RHS1 P 1 LHS1 P 0 LIT I 1 HIST I 0 CL F 22Q TEMP-TEMP F 23Q STACK F 24Q IN-PROVE-LEMMA-FLG F 25Q HINTS F 26Q PROCESS-HIST F 27Q PROCESS-CLAUSES) @ O hXdqh_ O_gOOOgOOOOOOO@IJA _OIc$W$gJc$ W$g^Ic$W$g&Jc$W$gW(gW*h gW&h]gW&@ O:h @ Oyh_@AOOhc.NOOIJMhc,i_ O_gOOOOOOgJLIK Oi_ O_{gOOOOOOgJKIL O@i<_"MHdO"HO"HNFOBO"dUdgMdHdBdg8d1d)d!dOgIJO" ZJIO" QLO"dgDd?d9d3O"OggKIJL hgJIK LhO"_ OO h__O_fO &_(1164Q SUBSTITUTE 1145Q SUBSTITUTE 1053Q SUBSTITUTE 1042Q SUBSTITUTE 647Q OCCUR 532Q OCCUR 170Q FERTILIZE1) (1156Q EQUAL 1136Q EQUAL 1131Q LEFT-FOR-RIGHT 1067Q EQUAL 1031Q LEFT-FOR-RIGHT 764Q EQUAL 737Q NOT 635Q LEFT-FOR-RIGHT 566Q EQUAL 520Q LEFT-FOR-RIGHT 451Q EQUAL 322Q BEING-PROVED 311Q BEING-PROVED 277Q INDUCT 265Q QUOTE 247Q QUOTE 232Q QUOTE 213Q QUOTE 74Q EQUAL 44Q NOT) () FERTILIZE-FEASIBLE D1 (P 1 LIT2 I 3 HIST I 2 TERM I 1 CL I 0 LIT) B h%BB hAHhC1JhhY@BI IiHX[JZgKKKKKKKKKK@L@MKjif(65Q OCCUR 16Q SKO-DEST-NESTP 3 ALMOST-VALUEP) (117Q FERTILIZE-CLAUSE) () FERTILIZE-SENT D1 (I 1 HIST I 0 CL) g@Agg (16Q EXECUTE) (12Q GENERALIZE-SENT 7 SIMPLIFY-SENT 2 FERTILIZE-CLAUSE) () FERTILIZE1 D1 (I 4 HIST I 3 RHS I 2 LHS I 1 CL I 0 LIT) .@ABD @ACD B C g@ACD g(46Q FERTILIZE-FEASIBLE 30Q COMPLEXITY 24Q COMPLEXITY 17Q FERTILIZE-FEASIBLE 6 FERTILIZE-FEASIBLE) (53Q LEFT-FOR-RIGHT 36Q RIGHT-FOR-LEFT) () FILTER-ARGS D1 (L (2 ARGS 1 FORMALS 0 SUBSET)) D@AHIABN_MhJ KhZHXK&LONMNIL NIL () FIND-EQUATIONAL-POLY D1 (P 14Q POLY2 P 6 HYP2 P 5 HYP1 P 4 PAIR P 3 POLY2 P 2 WINNING-PAIR P 1 POLY1 I 1 POT I 0 HIST F 15Q LINEAR-ASSUMPTIONS F 16Q TEMP-TEMP F 17Q FALSE F 20Q LEMMAS-USED-BY-LINEAR F 21Q TRUE) 1 A HhY cHXWA Oh[JI \ L MWNW@h__qiIK W cW"MMW cW"NNW cgLhIK W c L_JIO OqO_a_gROh__ hBhw_OOgLOLOLOOiO/(301Q COMPLEMENTARY-MULTIPLEP 261Q UNIONQ 254Q UNIONQ 223Q ADD-TO-SET 205Q ADD-TO-SET 167Q UNION-EQUAL 162Q UNION-EQUAL 111Q NUMBERP? 103Q NUMBERP? 76Q EQUATIONAL-PAIR-FOR 23Q TRIVIAL-POLYP) (403Q FIND-EQUATIONAL-POLY 326Q SIMPLIFY-CLAUSE 247Q POLY 241Q POLY 231Q FIND-EQUATIONAL-POLY 155Q POLY 147Q POLY 46Q LINEAR-POT 3 LINEAR-POT) () FIRST-COEFFICIENT D1 (L (0 EQUATION)) @NIL (3 POLY) () FIRST-VAR D1 (L (0 EQUATION)) @NIL (3 POLY) () FITS D1 (P 1 VAR I 2 VARS I 1 ALIST2 I 0 ALIST1 F 2 TEMP-TEMP) +BHiY@cIIAcIhHXNIL NIL () FIXCAR-CDR D1 (P 0 TEMP I 0 TERM) 0@ X$@bHdggg@hb@(7 CAR-CDRP) (41Q CDR 35Q CAR 30Q A) () FLATTEN-ANDS-IN-LIT D1 (P 2 C3 P 1 C2 P 0 C1 I 0 TERM F 3 FALSE F 4 TRUE) 0@Th@dMdgEd@d:d3d,@@ISH J JS+@h@dgddd@H I (210Q \APPEND2 205Q FLATTEN-ANDS-IN-LIT 201Q FLATTEN-ANDS-IN-LIT 116Q \APPEND2 113Q FLATTEN-ANDS-IN-LIT 107Q FLATTEN-ANDS-IN-LIT 104Q DUMB-NEGATE-LIT) (141Q AND 22Q IF) () FLESH-OUT-IND-PRIN D1 (P 40Q LOOP-ANS P 37Q ARG P 36Q FLG P 35Q ACTUAL P 31Q ARGLIST P 22Q X P 15Q LOOP-ANS P 14Q FLG P 13Q ACTUAL P 4 LOOP-ANS P 3 V P 2 A I 5 QUICK-BLOCK-INFO I 4 MASK I 3 JUSTIFICATION I 2 MACHINE I 1 FORMALS I 0 TERM) !`DjH"IA HdIA@2IIkعHXHLHdID@ B N!'[C J L IH_MOHdID@ 2 O-4gO_OOh__NMO&__O0OHdIBaO>OHdIdC d@ _gO O _O_O_x_$`A@ O$ _&dO&O$AO*.O,_(dO(_"O O"h_ _O_qO"&_ _2D@ C O8_:O6_O h$0O: ddNMh_M&OO@ _@O8_8O6_6O4_4h(1005Q UNION-EQUAL 746Q ALL-VARS 731Q SUB-PAIR-VAR 724Q SARGS 577Q SARGS 463Q SUB-PAIR-VAR-LST 451Q SARGS 412Q UNIONQ 405Q ALL-VARS 216Q SARGS 153Q UNIONQ 147Q ALL-VARS 142Q MEMB 116Q SARGS 25Q LENGTH) (712Q CHANGEABLE 501Q TESTS-AND-CASES 456Q TESTS-AND-CASES 443Q TESTS-AND-ALISTSTYPE# 376Q UNCHANGEABLE 234Q CHANGEABLE 135Q JUSTIFICATION 21Q FLOATP 2 CANDIDATETYPE#) () FLUSH-CAND1-DOWN-CAND2A0001A0002A0003 D1 (I 1 PAIR2 I 0 PAIR1) @A @A (15Q OCCUR) NIL () FLUSH-CAND1-DOWN-CAND2A0001A0002 D1 (I 1 ALIST2 I 0 ALIST1) @Agid (12Q PIGEON-HOLE) (4 FLUSH-CAND1-DOWN-CAND2A0001A0002A0003) () FLUSH-CAND1-DOWN-CAND2A0001 D1 (I 1 TA2 I 0 TA1) 9@A (@Ah@Agid (66Q PIGEON-HOLE 16Q SUBSETP) (60Q FLUSH-CAND1-DOWN-CAND2A0001A0002 53Q TESTS-AND-ALISTS 45Q TESTS-AND-ALISTS 33Q TESTS-AND-ALISTS 24Q TESTS-AND-ALISTS 11Q TESTS-AND-ALISTS 3 TESTS-AND-ALISTS) () FLUSH-CAND1-DOWN-CAND2 D1 (P 17Q OTHER-TERMS2 P 16Q TERM2 P 15Q JUSTIFICATION2 P 14Q TESTS-AND-ALISTS-LST2 P 13Q UNCHANGEABLES2 P 12Q CHANGED-VARS2 P 11Q CONTROLLERS2 P 10Q SCORE2 P 7 OTHER-TERMS1 P 6 TERM1 P 5 JUSTIFICATION1 P 4 TESTS-AND-ALISTS-LST1 P 3 UNCHANGEABLES1 P 2 CHANGED-VARS1 P 1 CONTROLLERS1 P 0 SCORE1 I 1 CAND2 I 0 CAND1) @@X@Y@Z@[@\@ ]@ ^@_A_A_A_A_A_A _A _A_JO jKO bLOgid T`HO_ dO IO _"dO"dOdOdOdO dO NOO _$dO$(345Q ADD-TO-SET 342Q UNION-EQUAL 263Q UNIONQ 232Q PIGEON-HOLE 214Q SUBSETP 204Q SUBSETP) (237Q CANDIDATETYPE# 224Q FLUSH-CAND1-DOWN-CAND2A0001 172Q CANDIDATE 162Q CANDIDATE 152Q CANDIDATE 142Q CANDIDATE 132Q CANDIDATE 122Q CANDIDATE 112Q CANDIDATE 102Q CANDIDATE 72Q CANDIDATE 63Q CANDIDATE 54Q CANDIDATE 45Q CANDIDATE 36Q CANDIDATE 27Q CANDIDATE 20Q CANDIDATE 11Q CANDIDATE) () FN-SYMB0 D1 (L (0 X)) G@dldggggg3 j@g@jgg@g@gNIL (104Q CONS 73Q *1*QUOTE 65Q ADD1 61Q ZERO 51Q MINUS 35Q PACK 31Q FALSE 24Q *1*FALSE 20Q TRUE 13Q *1*TRUE) () FNNAMEP D1 (P 1 X I 1 TERM I 0 FN F 2 *1*BTM-OBJECTS F 3 SHELL-ALIST) EAhg@dR S @A @AAHh@I IiHX(70Q FNNAMEP 37Q MEMB 34Q ALL-FNNAMES 22Q MEMB) (11Q QUOTE) () FNNAMEP-IF D1 (P 1 X I 0 TERM) 1@hg@dgHhY IiHX(44Q FNNAMEP-IF) (22Q IF 11Q QUOTE) () FORM-COUNT D1 (I 0 TERM F 0 NUMBER-OF-VARIABLES) jc@ (6 FORM-COUNT1) NIL () FORM-COUNT-EVG D1 (P 6 X P 3 NUMBER P 1 I I 0 EVG F 7 LITATOM-FORM-COUNT-ALIST F 10Q TEMP-TEMP) @dbdgkg@d3 j@@ l@kWcdd@d l@ kjIHJ@I)ԺIkYJlWcdg @jLMkMN ԽL\@ @ k(223Q FORM-COUNT-EVG 216Q FORM-COUNT-EVG 202Q FORM-COUNT-EVG 77Q NCHARS 70Q NCHARS 41Q MINUS) (150Q *1*QUOTE 17Q *1*FALSE 10Q *1*TRUE) () FORM-COUNT1 D1 (P 2 T1 I 0 TERM F 3 NUMBER-OF-VARIABLES) 6@ Skcjg@ @jHIkIJ ԹHX(55Q FORM-COUNT1 26Q FORM-COUNT-EVG) (16Q QUOTE) () FORM-INDUCTION-CLAUSE D1 (I 3 TERMS I 2 CONCL I 1 HYPS I 0 TESTS) @AB (10Q \APPEND2 5 \APPEND2) NIL () FORMP-SIMPLIFIER D1 (P 2 TL P 1 FN P 0 X I 0 TERM F 3 TEMP-TEMP F 4 META-NAMES) 0@o H@g@@@X MHcdg gg@ Hcdgk YHcdgl ZIc@gIlIdgJgo gIT gJggI hho (323Q SUBLIS-VAR 305Q ARITY 262Q MEMB 242Q SUBSTITUTE 164Q ARGN0 140Q ARGN0 116Q CONS-TERM 101Q FN-SYMB0 56Q SHELLP 15Q ERROR) (277Q QUOTE 274Q A 267Q TL 250Q TYPE-PRESCRIPTION-LST 233Q TL 224Q QUOTE 201Q QUOTE 151Q QUOTE 127Q QUOTE 111Q LITATOM 104Q CONS 70Q QUOTE 30Q FORMP) ( 320Q (IF (EQUAL A (LENGTH TL)) (FORM-LSTP TL) (QUOTE *1*FALSE)) 237Q (IF (LISTP TL) (EQUAL (CDR TL) (QUOTE NIL)) (QUOTE *1*FALSE)) 12Q "MATCH! failed!") FORMULA-OF D1 (L (0 NAME)) $@gXddgdgH(41Q NIL) (24Q PROVE-LEMMA 16Q ADD-AXIOM 6 EVENT) () FREE-VAR-CHK D1 (P 0 TEMP I 2 FORM I 1 ARGS I 0 NAME) MB bdA Xdog@gHhg AB Xdog@gHhg h(111Q ERROR1 56Q SET-DIFF 50Q ERROR1 15Q SET-DIFF 6 ALL-VARS) (106Q WARNING 76Q TEMP 71Q NAME 45Q SOFT 35Q TEMP 30Q NAME) ( 66Q (PROGN (!LIST TEMP) (PLURAL? TEMP ARE IS) IN THE ARGLIST BUT NOT IN THE BODY OF THE DEFINITION OF (!PPR NAME NIL) !) 25Q (PROGN ILLEGAL FREE (PLURAL? TEMP VARIABLES VARIABLE) , (!PPR-LIST TEMP) , IN THE DEFINITION OF (!PPR NAME NIL) !)) FREE-VARSP D1 (P 1 ARG I 1 ALIST I 0 TERM) ,@dAhg@HhYA IiHX(37Q FREE-VARSP) (14Q QUOTE) () GEN-VARS D1 (P 2 LOOP-ANS P 1 LIT I 2 VARIABLE-NAMES I 1 N I 0 CL) B@!H JA Y J HX(30Q UNIONQ 24Q ALL-VARS 16Q SET-DIFF-N) NIL () GENERALIZE-CLAUSE D1 (P 0 COMMONSUBTERMS I 1 HIST I 0 CL F 1 GENERALIZE-LEMMA-NAMES F 2 ALL-LEMMAS-USED F 3 STACK F 4 GEN-VARIABLE-NAMES1 F 5 PROCESS-CLAUSES F 6 GENERALIZING-SKOS F 7 OBVIOUS-RESTRICTIONS F 10Q PROCESS-HIST) 5gSh@ Xd@HT hc VHWQhcQR ci(57Q UNIONQ 30Q GENERALIZE1 16Q GENRLTERMS) (5 BEING-PROVED) () GENERALIZE-SENT D1 (I 1 HIST I 0 CL) g@Agg (16Q EXECUTE) (12Q ELIMINATE-IRRELEVANCE-SENT 7 SIMPLIFY-SENT 2 GENERALIZE-CLAUSE) () GENERALIZE1 D1 (I 2 VARIABLE-NAMES I 1 SUBTERMLST I 0 CL F 0 GENERALIZING-SKOS F 1 OBVIOUS-RESTRICTIONS F 2 GENERALIZE-LEMMA-NAMES) @A B chcdcAP@ (26Q GENERALIZE2 10Q GEN-VARS 4 LENGTH) NIL () GENERALIZE2 D1 (P 12Q LIT P 6 SUBTERM I 2 CL I 1 VARLST I 0 TERMLST) z 00@=d0 NB d _O Oh_O&_O[LK]\MB $ \Kd @AO IHhZH&J(145Q SUB-PAIR-EXPR 124Q LAST 117Q SCRUNCH 114Q \NCONC2 34Q DUMB-NEGATE-LIT 25Q GET-TYPES) NIL () GENRLT1 D1 (P 5 LIT2 P 4 TAIL P 3 LIT P 1 RHS P 0 LHS I 0 CL)  @J@[ddgdddKGNKgFKAK;Kg1K*K"KKKKHI JZdLdLM hh(224Q COMSUBTERMS 177Q COMSUBTERMS) (116Q EQUAL 71Q NOT 32Q EQUAL) () GENRLTERMS D1 (P 0 GENRLTLIST I 0 CL) @ H(6 GENRLT1) NIL () GET-CANDS D1 (I 0 TERM F 3 TEMP-TEMP) @@hc @ 0@ghd XIHZYJ  YH(71Q LAST 65Q \NCONC2 42Q GET-CANDS 16Q POSSIBLE-IND-PRINCIPLES) (30Q QUOTE) () GET-LISP-SEXPR D1 (P 0 SEXPR I 0 FN) >@dgog@hg @ggXdog@hg (73Q ERROR1 34Q ERROR1) (70Q SOFT 61Q FN 45Q SEXPR 41Q LISP-CODE 31Q SOFT 22Q FN 7 LISP-CODE) ( 56Q (PROGN (!PPR FN NIL) IS PART OF THE BASIC SYSTEM AND HAS A HAND-CODED LISP DEFINITION %.) 17Q (PROGN (!PPR FN NIL) DOES NOT HAVE A RUNNABLE LISP DEFINITION %.)) GET-LEVEL-NO D1 (L (0 FNNAME)) @gjNIL (3 LEVEL-NO) () GET-STACK-NAME D1 (P 3 I I 0 STACKV) <g0@ dgK XIHZYJ  YH(65Q LAST 61Q PACK 32Q UNPACK 14Q DREVERSE 11Q GET-STACK-NAME1) (26Q %. 2 *) () GET-STACK-NAME1 D1 (P 0 ANS I 0 STACKV) &@khg@ ddkk@ (42Q GET-STACK-NAME1 25Q GET-STACK-NAME1) (16Q TO-BE-PROVED) () GET-TYPES D1 (P 13Q LEMMA P 4 INST-LEMMA P 3 PAIR P 2 TYPE P 1 LEMMA-RESTRICTIONS P 0 TYPE-RESTRICTION I 1 CL I 0 TERM F 14Q TEMP-TEMP F 15Q OBVIOUS-RESTRICTIONS F 16Q UNIFY-SUBST F 17Q GENERALIZE-LEMMA-NAMES F 20Q RECOGNIZER-ALIST F 21Q GENERALIZE-LEMMAS F 22Q TEMPORARILY-DISABLED-LEMMAS F 23Q DISABLED-LEMMAS) p@ ZW h],h[d@hXddW cW"A OOYHIJNjNM_cW$ nWW&e@O XOW J@cdg g@WO \ OWcL_OOh__O_`O&_(246Q FNNAMEP 243Q SUBST-EXPR 237Q SUBLIS-VAR 217Q FN-SYMB0 174Q FREE-VARSP 156Q ARG1-IN-ARG2-UNIFY-SUBST 130Q MEMB 41Q ADD-TO-SET 6 TYPE-SET) (255Q GENERALIZE-LEMMA 232Q GENERALIZE-LEMMA 222Q X 206Q QUOTE 165Q GENERALIZE-LEMMA 151Q GENERALIZE-LEMMA 117Q GENERALIZE-LEMMA) () GREATEREQP D1 (L (1 J 0 I)) A@hNIL NIL () GUARANTEE-CITIZENSHIP D1 (I 0 NAME F 0 MAIN-EVENT-NAME) (@g @gP@Pgg @Pg h(43Q PUT1 33Q PUT1) (40Q MAIN-EVENT 30Q SATELLITES 23Q SATELLITES 12Q MAIN-EVENT 3 EVENT) () GUESS-RELATION-MEASURE-LST D1 (P 7 X P 5 VAR P 1 I I 1 MACHINE I 0 FORMALS) e@jBHJAN%iggMhhK7Lh[HIkԹ_MO MIO hN^L&(124Q BM:NTH 106Q OCCUR-LST) (117Q TESTS-AND-CASE 101Q TESTS-AND-CASE 36Q COUNT 33Q LESSP) () HAS-LIB-PROPS D1 (I 0 ATM F 2 LIB-PROPS) #@ HYhR IIig(22Q MEMB 3 GETPROPLIST) (37Q CDDR) () ILLEGAL-CALL D1 NIL ohg (12Q ERROR1) (7 HARD) ( 3 (PROGN SOME FUNCTION WAS CALLED WITH INAPPROPRIATE ARGUMENTS %.)) ILLEGAL-NAME D1 (I 0 NAME) @l@l @ h(24Q LEGAL-CHAR-CODE-SEQ 21Q CHCON) NIL () IMMEDIATE-DEPENDENTS-OF D1 (P 5 X P 0 ATM I 0 NAME F 6 CHRONOLOGY) @dggV gog@hg @ X 0@g_ AIJ0@g.@MV MK Lh[IYL&dJIh[I&K dJIh[I&K(210Q UNION-EQUAL 134Q EVENT1-OCCURRED-BEFORE-EVENT2 101Q TREE-DEPENDENTS 76Q MAIN-EVENT-OF 56Q TYPE-PRESCRIPTION-LEMMAP 51Q ERROR1 21Q REMOVE1) (121Q IMMEDIATE-DEPENDENTS0 70Q IMMEDIATE-DEPENDENTS0 46Q HARD 37Q NAME 25Q EVENT 15Q GROUND-ZERO 7 GROUND-ZERO) ( 34Q (PROGN IMMEDIATE-DEPENDENTS-OF WAS CALLED ON A NONEVENT , (!PPR NAME NIL) %.)) IMPLIES? D1 (I 1 TERM I 0 TESTS) A@ (4 MEMBER) NIL () IMPOSSIBLE-POLYP D1 (P 1 PAIR I 0 POLY) )@j@HiYj hHX(37Q GREATEREQP) (15Q POLY 3 POLY) () IND-FORMULA D1 (P 27Q PICK P 20Q ALIST P 17Q LIT P 16Q CL1 P 7 TA P 3 CL I 2 CL-SET I 1 TERMS I 0 TESTS-AND-ALISTS-LST) ?0Bd0@d0 0 Bud!0OMd_ 0O&d_O O _(O* O(h_,O(&_*O,_"O$ O"h_&O"&_$O&_OO__O Z _Od0Od _0O2 O0h_4O0&_2O4O.KA _O Oh_O&_O\M4L^]NXIHZYJ  YH ]L(470Q LAST 460Q LAST 454Q DELETE-TAUTOLOGIES 451Q SCRUNCH-CLAUSE-SET 340Q FORM-INDUCTION-CLAUSE 276Q NEGATE-LIT 241Q LAST 234Q ALL-PICKS 114Q NEGATE-LIT 111Q SUBLIS-VAR) (265Q TESTS-AND-ALISTS 55Q TESTS-AND-ALISTS) () INDUCT D1 (P 12Q CL P 6 FAVOR-COMPLICATED-CANDIDATES-ANS P 5 COMPUTE-VETOES-ANS P 4 INDUCT-ANS P 3 WINNING-CAND P 2 PICK-HIGH-SCORES-ANS P 1 MERGED-CANDS-ANS P 0 GET-CANDS-ANS I 0 CL-SET F 16Q STACK F 17Q ALL-LEMMAS-USED) p0 @:d 0 Od _O~O__O_O]O__O@ Xg Y ] ^ Z[dFdK K@ KK K ; _O _Og@hdhW hjddddh h K W cg@hLW KH I MdIj J N h L(423Q IO 407Q LENGTH 403Q LENGTH 377Q LENGTH 364Q LENGTH 360Q LENGTH 353Q GET-STACK-NAME 335Q UNIONQ 314Q WRAPUP 307Q IO 265Q GET-STACK-NAME 240Q LAST 226Q LAST 221Q INFORM-SIMPLIFY 172Q IND-FORMULA 135Q PICK-HIGH-SCORES 131Q FAVOR-COMPLICATED-CANDIDATES 125Q COMPUTE-VETOES 121Q TRANSITIVE-CLOSURE 112Q REMOVE-UNCHANGING-VARS 31Q GET-CANDS) (342Q INDUCT 326Q JUSTIFICATION 321Q CANDIDATE 252Q INDUCT 213Q CANDIDATE 205Q CANDIDATE 177Q CANDIDATE 163Q CANDIDATE 155Q CANDIDATE 147Q CANDIDATE 116Q MERGE-CANDS) () INDUCT-VARS D1 (P 12Q MASK P 10Q ARG P 4 I P 2 LOOP-ANS P 1 TERM I 0 CAND) @ @!HJYjBKMJ HX_!Ig OhO_N1Oh^KLkԼ_jOL kjOiO_O&(145Q MINUS 46Q UNIONQ) (67Q CONTROLLER-POCKETS 11Q CANDIDATE 3 CANDIDATE) () INDUCTION-MACHINE D1 (P 3 TEST P 2 LOOP-ANS I 2 TESTS I 1 TERM I 0 FNNAME) |AAgAgA`B HdI Bd@K J J@A HdIh@ABAh @ABA h (171Q \NCONC2 166Q INDUCTION-MACHINE 163Q \APPEND2 156Q NEGATE-LIT 141Q INDUCTION-MACHINE 136Q \APPEND2 103Q UNION-EQUAL 100Q ALL-ARGLISTS 64Q UNION-EQUAL 60Q ALL-ARGLISTS 31Q REMOVE-REDUNDANT-TESTS) (24Q TESTS-AND-CASESTYPE# 16Q IF 7 QUOTE) () INFORM-SIMPLIFY D1 (P 7 ALIST P 3 TA I 1 TERMS I 0 TESTS-AND-ALISTS-LST F 10Q INDUCTION-CONCL-TERMS F 11Q INDUCTION-HYP-TERMS) ZAc0@:d0KdOA \M(L^]NXIHZYJc YH ]L(123Q LAST 113Q LAST 43Q SUBLIS-VAR-LST) (24Q TESTS-AND-ALISTS) () INIT-LEMMA-STACK D1 (F 0 ORIG-LEMMA-STACK F 1 LEMMA-STACK) PchNIL NIL () INIT-LIB D1 (P 0 VAR I 1 VARS I 0 PROPS F 1 LIB-PROPS F 2 LIB-VARS F 3 LIB-FILE F 4 LIB-ATOMS-WITH-PROPS F 5 LIB-ATOMS-WITH-DEFS) $@cAcddH hcdc dc(23Q SET 2 KILL-LIB) NIL () INIT-LINEARIZE-ASSUMPTIONS-STACK D1 (F 0 ORIG-LINEARIZE-ASSUMPTIONS-STACK F 1 LINEARIZE-ASSUMPTIONS-STACK) PchNIL NIL () INTERESTING-SUBTERMS D1 (P 0 ARG I 0 FORM) D@hg @do dH hddH h(72Q \APPEND2 67Q INTERESTING-SUBTERMS 45Q \APPEND2 42Q INTERESTING-SUBTERMS 26Q MEMB) (11Q QUOTE) ( 23Q (CAR CDR LISTP EQ NEQ NOT)) INTERSECTP D1 (P 1 E I 1 Y I 0 X) @HhYA IiHX(17Q MEMBER) NIL () INTRODUCE-ANDS D1 (P 1 REST2 P 0 REST1 I 0 X)  @@g@ddgzdudodh@d[ihT@ X@ YH I gHIhggHIgI HIh gHI @0@d KJh\J&L(242Q INTRODUCE-ANDS 224Q \APPEND2 206Q \APPEND2 121Q INTRODUCE-ANDS 111Q INTRODUCE-ANDS) (213Q AND 170Q AND 156Q AND 150Q AND 135Q AND 33Q *2*IF 14Q QUOTE) () INTRODUCE-LISTS D1 (P 0 REST I 0 X)  @ddgYdxdis3ogIhdg@ Xdg@ hHgg@ Hg@ Hh0@d KJh\J&L(172Q INTRODUCE-LISTS 150Q INTRODUCE-LISTS 132Q INTRODUCE-LISTS 103Q INTRODUCE-LISTS 66Q INTRODUCE-LISTS) (142Q CONS 124Q LIST 117Q LIST 75Q LIST 55Q CONS 43Q QUOTE 16Q QUOTE) () JUMPOUTP D1 (P 0 TYPE-ALIST I 1 NEW I 0 OLD F 1 DEFN-FLG F 2 TEMP-TEMP F 3 FNSTACK F 4 *ARGLIST* F 5 *TYPE-ALIST* F 6 *FNNAME*) >Q@Acdg gSA gUVT  (73Q RETFROM 67Q REWRITE-SOLIDIFY 64Q CONS-TERM 50Q POP-LEMMA-FRAME 43Q REWRITE-FNCALLP 27Q FN-SYMB0) (53Q REWRITE-FNCALL 32Q IF 16Q QUOTE) () KILL-EVENT D1 (P 0 TUPLE I 0 NAME F 1 CHRONOLOGY) @@dggdhddH @gd @ @Q c@(72Q REMOVE1 65Q KILLPROPLIST1 54Q KILLPROPLIST1 34Q ADD-SUB-FACT 12Q KILL-LIB) (45Q SATELLITES 16Q LOCAL-UNDO-TUPLES 4 GROUND-ZERO) () KILL-LIB D1 (F 0 LIB-ATOMS-WITH-PROPS F 1 LIB-ATOMS-WITH-DEFS F 2 LIB-VARS) Lg DPd Qd Rd g g g g g (111Q MAKUNBOUND 103Q MAKUNBOUND 75Q MAKUNBOUND 67Q MAKUNBOUND 61Q MAKUNBOUND 46Q MAKUNBOUND 32Q KILL-DEFINITION 16Q KILLPROPLIST1 5 BOUNDP) (106Q LIB-FILE 100Q LIB-PROPS 72Q LIB-ATOMS-WITH-DEFS 64Q LIB-ATOMS-WITH-PROPS 56Q LIB-VARS 2 LIB-PROPS) () KILLPROPLIST1 D1 (P 0 PROP I 0 ATM F 1 LIB-PROPS) Qd@H @g (27Q REMPROP 13Q REMPROP) (24Q LIB-LOC) () LEGAL-CHAR-CODE-SEQ D1 (P 2 C P 1 TAIL I 0 LST) `@-@!HYI"i@l-hl0@ @l9 hZ3 lAJ JlZ l0J Jl9 Jl-hI(121Q LESSEQP 112Q LESSEQP 102Q LESSEQP 73Q LESSEQP 54Q LESSEQP 43Q LESSEQP) NIL () LENGTH-TO-ATOM D1 (L (0 L)) @jHZIIkعJNIL NIL () LESSEQP D1 (L (1 J 0 I)) @AhNIL NIL () LEXORDER D1 (I 1 Y I 0 X) 0@A@A iAh@A@Abb@Abb(12Q ALPHORDER) NIL () LINEARIZE D1 (P 14Q POLY P 7 L P 3 CONTRA P 2 LST P 1 RHS P 0 LHS I 1 FLG I 0 TERM F 15Q FALSE) . @A$@$@g@@@@@w@2A@@g@@}@w@@g@@@g@@@@@@gHh gIg@ hh6@bA@@g@@@g@@@@@@+g@@@g@~@t@j@c@@H I vHgIg@ IgHg@ hhD@wA@3@g'@@@g@@@h@h@@jg@@z@r@@YgHg@ hh@@gz@u@o@hg@@H I SHIgHh gIg@ hHIgIh gHg@ hhZ@JRd_A OOM;Lh^7_WO O_OOh__O_O&_L&NZd ljJ O h[XJJ_ OO_d OKO OKO JhJ O h[VJJ_ OO_d OKO OKO JhJ(2036Q UNIONQ 2006Q UNION-EQUAL 1740Q IMPOSSIBLE-POLYP 1671Q UNIONQ 1641Q UNION-EQUAL 1573Q IMPOSSIBLE-POLYP 1530Q LENGTH 1447Q MEMBER 1362Q ADD-NUMBERP-ASSUMPTION-TO-POLY 1357Q ADD-NUMBERP-ASSUMPTION-TO-POLY 1354Q COMPRESS-POLY 1351Q ADD-LINEAR-TERM 1346Q ADD-LINEAR-TERM 1343Q ZERO-POLY 1330Q CONS-TERM 1313Q ADD-NUMBERP-ASSUMPTION-TO-POLY 1310Q ADD-NUMBERP-ASSUMPTION-TO-POLY 1305Q COMPRESS-POLY 1302Q ADD-LINEAR-TERM 1277Q ADD-LINEAR-TERM 1274Q ZERO-POLY 1261Q CONS-TERM 1244Q POSSIBLY-NUMERIC 1237Q POSSIBLY-NUMERIC 1150Q COMPRESS-POLY 1145Q ADD-LINEAR-TERM 1142Q ADD-LINEAR-TERM 1137Q ZERO-POLY 656Q COMPRESS-POLY 653Q ADD-LINEAR-TERM 650Q ADD-LINEAR-TERM 645Q ZERO-POLY 631Q COMPRESS-POLY 626Q ADD-LINEAR-TERM 623Q ADD-LINEAR-TERM 620Q ZERO-POLY 576Q POSSIBLY-NUMERIC 571Q POSSIBLY-NUMERIC 275Q COMPRESS-POLY 272Q ADD-LINEAR-TERM 267Q ADD-LINEAR-TERM 264Q ZERO-POLY 251Q CONS-TERM) (2031Q POLY 2022Q POLY 2016Q POLY 2001Q POLY 1772Q POLY 1766Q POLY 1664Q POLY 1655Q POLY 1651Q POLY 1634Q POLY 1625Q POLY 1621Q POLY 1442Q POLY 1337Q NEGATIVE 1333Q POSITIVE 1322Q ADD1 1270Q NEGATIVE 1264Q POSITIVE 1253Q ADD1 1174Q EQUAL 1133Q NEGATIVE 1127Q POSITIVE 1063Q LESSP 755Q EQUAL 714Q NOT 641Q NEGATIVE 635Q POSITIVE 614Q NEGATIVE 610Q POSITIVE 501Q EQUAL 454Q NOT 363Q LESSP 330Q NOT 260Q NEGATIVE 254Q POSITIVE 243Q ADD1 164Q LESSP 137Q NOT 73Q EQUAL 16Q LESSP) () LISTABLE D1 (P 1 RHS P 0 LHS I 0 X F 2 TEMP-TEMP) O @hg@;@g3@.@(@h @@YoHhI cHR(105Q LISTABLE) (30Q CONS 14Q QUOTE) ( 73Q (QUOTE NIL)) LOGSUBSETP D1 (L (1 Y 0 X)) @A@jNIL NIL () LOOKUP-HYP D1 (P 10Q LIT P 6 PAIR P 4 LIT P 3 NEG-HYP P 2 TYPE P 1 NOT-FLG P 0 TERM I 0 HYP F 11Q TYPE-ALIST F 12Q LITS-THAT-MAY-BE-ASSUMED-FALSE F 13Q RECOGNIZER-ALIST F 14Q TEMP-TEMP) P@@g@@h @i@HHgHWcmI6WMh6iHjJNjHN NiM]WM#hW@ WO&h\d i^J HN NiM]_KO OO_(277Q ONE-WAY-UNIFY1 251Q ONE-WAY-UNIFY1 242Q LOGSUBSETP 231Q PUSH-LEMMA 206Q DUMB-NEGATE-LIT 145Q ONE-WAY-UNIFY1) (54Q QUOTE 13Q NOT) () LOOP-STOPPER D1 (P 2 ALL-VARS P 1 RHS P 0 LHS I 0 TERM F 10Q UNIFY-SUBST) h0@<@g4@/@)@h!@@HI H ZWAKL_dOJ  M Nh]\K[N&](121Q MEMB 115Q MEMB 65Q ALL-VARS 57Q VARIANTP) (13Q EQUAL) () MAIN-EVENT-OF D1 (I 0 NAME) !@dggog@hg (36Q ERROR1) (33Q HARD 24Q NAME 12Q MAIN-EVENT 4 EVENT) ( 21Q (PROGN MAIN-EVENT-OF HAS BEEN CALLED ON AN OBJECT , NAMELY (!PPR NAME NIL) , THAT IS NEITHER AN EVENT NOR A SATELLITE OF ANOTHER EVENT !)) MAKE-EVENT D1 (I 1 EVENT I 0 NAME F 0 CHRONOLOGY F 1 MAIN-EVENT-NAME) @Ag @g @Pc@c(21Q PUT1 13Q IDATE 7 PUT1) (16Q IDATE 4 EVENT) () MAKE-FLATTENED-MACHINE D1 (P 3 ARG I 2 TESTS I 1 TERM I 0 FNNAME) A Adghg7@AB @ABAh @ABA h @AC`dBAHdI0Ad@KB XIHZYJ YH0Ad@KB XI HZYJ YH(265Q LAST 241Q MAKE-FLATTENED-MACHINE 213Q LAST 165Q MAKE-FLATTENED-MACHINE 110Q \NCONC2 105Q \NCONC2 102Q MAKE-FLATTENED-MACHINE 77Q \APPEND2 72Q NEGATE-LIT 55Q MAKE-FLATTENED-MACHINE 52Q \APPEND2 34Q MAKE-FLATTENED-MACHINE) (122Q TESTS-AND-CASETYPE# 21Q IF 11Q QUOTE) () MAKE-NEW-NAME D1 (P 0 TEMP) g Xi H(15Q CHK-NEW-NAME 10Q GENSYM) (5 G) () MAKE-REWRITE-RULES D1 (P 1 RHS P 0 LHS I 2 CONCL I 1 HYPS I 0 NAME F 2 TEMP-TEMP) S Bcddgh6Bg.B)B#BBBgHI hb@AB h(116Q CREATE-REWRITE-RULE 101Q NORMALIZE-IFS 76Q EXPAND-BOOT-STRAP-NON-REC-FNS) (71Q EQUAL 31Q EQUAL 15Q QUOTE) () MAKE-TYPE-RESTRICTION D1 (P 5 R P 4 LOOP-ANS P 0 TYPE-SET I 3 TYPE-NO I 2 RECOGNIZER I 1 DV I 0 TR F 11Q RECOGNIZER-ALIST) 0@jK#LX@gdm`@gA0@/LMBkCWK[dghONh_N&_O 20@"dMgh ONh_N&_O dIdHA dJ(245Q CONS-TERM 226Q CONJOIN 173Q DUMB-NEGATE-LIT 144Q DISJOIN) (165Q X 107Q X 44Q ONE-OF 36Q TYPE-RESTRICTIONTYPE# 24Q NONE-OF) () MAX-FORM-COUNT D1 (P 2 ARG I 0 X) K@jg@ @dg @ jHIkIJ ԹHX(102Q MAX-FORM-COUNT 54Q MAX 51Q MAX-FORM-COUNT 41Q MAX-FORM-COUNT 21Q COUNT) (30Q IF 11Q QUOTE) () MAXIMAL-ELEMENTS D1 (P 3 X P 2 TEMP P 1 MAX P 0 ANS I 1 MEASURE I 0 LST) .@@$d[kAIJdIJKhIHKh H(45Q \NCONC2) NIL () MEANING-SIMPLIFIER D1 (P 5 I P 3 TL P 2 FN P 1 ALIST P 0 X I 0 TERM F 11Q TEMP-TEMP F 12Q META-NAMES)  @@o H'@g@@@@@Y MHcdg gg@ Hcdgk ZHcdgl [Jc@gJlJdggKhgJW JJ k2ML3ggMkK hIh_OOh_Mk]O&_N (405Q CONS-TERM 334Q CELL 306Q ARITY 273Q MEMB 200Q ARGN0 154Q ARGN0 132Q CONS-TERM 115Q FN-SYMB0 72Q SHELLP 15Q ERROR) (325Q CAR 322Q MEANING 260Q TYPE-PRESCRIPTION-LST 246Q CAR 240Q QUOTE 215Q QUOTE 165Q QUOTE 143Q QUOTE 125Q LOOKUP 120Q CONS 104Q QUOTE 30Q MEANING) ( 12Q "MATCH! failed!") MEMB-NEGATIVE D1 (I 1 CL I 0 LIT) Ah@A iAb(12Q COMPLEMENTARYP) NIL () MENTIONSQ D1 (I 1 TREE I 0 AT) A@A@A Ab(14Q MENTIONSQ) NIL () MENTIONSQ-LST D1 (I 1 TREE I 0 LST) AA@ @A Ab(16Q MENTIONSQ-LST 7 MEMB) NIL () MERGE-CAND1-INTO-CAND2 D1 (P 22Q VARS P 21Q TESTS-AND-ALISTS-LST P 20Q ALISTS P 17Q OTHER-TERMS2 P 16Q TERM2 P 15Q JUSTIFICATION2 P 14Q TESTS-AND-ALISTS-LST2 P 13Q UNCHANGEABLES2 P 12Q CHANGED-VARS2 P 11Q CONTROLLERS2 P 10Q SCORE2 P 7 OTHER-TERMS1 P 6 TERM1 P 5 JUSTIFICATION1 P 4 TESTS-AND-ALISTS-LST1 P 3 UNCHANGEABLES1 P 2 CHANGED-VARS1 P 1 CONTROLLERS1 P 0 SCORE1 I 1 CAND2 I 0 CAND1) $@X@Y@Z@[@\@ ]@ ^@_A_A_A_A_A_A _A _A_IOJO JO _$KO h|OJ hrLOO$ _"f`HO_&dO&IO _(dO(JO _*dO*KO _,dO,dO"dO dO NOO _.dO.(430Q ADD-TO-SET 425Q UNION-EQUAL 362Q UNIONQ 343Q UNIONQ 324Q UNIONQ 271Q MERGE-TESTS-AND-ALISTS-LSTS 255Q INTERSECTP 243Q INTERSECTP 225Q INTERSECTION 215Q INTERSECTION 212Q INTERSECTION 207Q INTERSECTION) (300Q CANDIDATETYPE# 172Q CANDIDATE 162Q CANDIDATE 152Q CANDIDATE 142Q CANDIDATE 132Q CANDIDATE 122Q CANDIDATE 112Q CANDIDATE 102Q CANDIDATE 72Q CANDIDATE 63Q CANDIDATE 54Q CANDIDATE 45Q CANDIDATE 36Q CANDIDATE 27Q CANDIDATE 20Q CANDIDATE 11Q CANDIDATE) () MERGE-CANDS D1 (I 1 CAND2 I 0 CAND1) @A A@ @A A@ (31Q MERGE-CAND1-INTO-CAND2 22Q MERGE-CAND1-INTO-CAND2 13Q FLUSH-CAND1-DOWN-CAND2 4 FLUSH-CAND1-DOWN-CAND2) NIL () MERGE-DESTRUCTOR-CANDIDATESA0001 D1 (I 1 Y I 0 X) @A @@A (17Q UNION-EQUAL) NIL () MERGE-DESTRUCTOR-CANDIDATES D1 (I 0 LST) @g (6 TRANSITIVE-CLOSURE) (3 MERGE-DESTRUCTOR-CANDIDATESA0001) () MERGE-TESTS-AND-ALISTSA0001 D1 (P 2 PAIR2 P 1 PAIR1 I 1 ALIST2 I 0 ALIST1) K@Hh@!H$i@A YIIA IiHXYAZHXIh(51Q MEMBER 34Q UNION-EQUAL) NIL () MERGE-TESTS-AND-ALISTS D1 (I 1 TA2 I 0 TA1 F 2 ALISTS) 2@Agi c`AHdIdR(22Q PIGEON-HOLE) (36Q TESTS-AND-ALISTS 31Q TESTS-AND-ALISTSTYPE# 16Q MERGE-TESTS-AND-ALISTSA0001 11Q TESTS-AND-ALISTS 3 TESTS-AND-ALISTS) () MERGE-TESTS-AND-ALISTS-LSTS D1 (P 32Q LOOP-ANS P 31Q X P 27Q BUCKET P 26Q ALIST1 P 24Q BUCKET P 23Q TA P 15Q PAIR P 14Q TA1 P 2 FLG P 1 ALIST P 0 BUCKETS I 2 VARS I 1 TESTS-AND-ALISTS-LST2 I 0 TESTS-AND-ALISTS-LST1) H`0A@d0 Kdh_O Oh_O&_OONh_N&_OX@! OiHAROnu_O* iQh_,hH6dO.'d_O,OB OO,O O ihJhO*_*O__&OO _(`O&dLO(!O02O4dM_$O"O$h_"_ O_O_?O$&_"_2O2O4 _4O0_0(474Q UNION-EQUAL 263Q ADD-TO-SET 255Q EXTEND-ALIST 241Q FITS) (355Q TESTS-AND-ALISTS 347Q TESTS-AND-ALISTSTYPE# 160Q TESTS-AND-ALISTS 22Q TESTS-AND-ALISTS) () META-LEMMAP D1 (L (0 X)) @hNIL (3 REWRITE-RULE) () MULTIPLE-PIGEON-HOLE D1 (P 11Q FLG P 10Q PAIR P 6 PIGEON P 1 PAIRLST P 0 TEMP I 2 FN I 1 HOLES I 0 PIGEONS) 00AdhJLKh]K&MY@M iT0III! O O$h_NOlBXOHi_O_M]dLKh]K&Mohg (212Q ERROR1) (207Q HARD) ( 203Q (PROGN MULTIPLE-PIGEON-HOLE FAILED TO GETPROP EVERYTHING IN A POT.)) CL:NEGATE D1 (I 0 TERM F 0 TRUE F 1 FALSE F 2 DEFINITELY-FALSE) j@ RPQ@ g@hdg@ @g@PQhdg@ @ g@ @ (147Q CONJOIN2 144Q CL:NEGATE 135Q CL:NEGATE 120Q DISJOIN2 115Q CL:NEGATE 106Q CL:NEGATE 45Q BOOLEAN 3 FALSE-NONFALSEP) (124Q OR 74Q AND 55Q IF 33Q NOT 21Q NOT) () NEGATE-LIT D1 (I 0 TERM F 0 DEFINITELY-FALSE F 1 TRUE F 2 FALSE) #@ PQR@ g@hg@(3 FALSE-NONFALSEP) (32Q NOT 21Q NOT) () NEXT-AVAILABLE-TYPE-NO D1 (P 0 TYPE-NO F 4 SHELL-ALIST) 8@jTYh'KXddlohg HZKJiIKk԰(40Q ERROR1) (35Q HARD) ( 31Q (PROGN TOO MANY SHELLS ! BECAUSE OF OUR USE OF 32-BIT WORDS TO REPRESENT SETS OF SHELL TYPES , THE NEED TO RESERVE ONE BIT FOR INTERNAL USE , AND THE EXISTENCE OF 37Q PREVIOUSLY DEFINED SHELLS , WE CANNOT ACCEPT FURTHER ADD-SHELL COMMANDS %.)) NO-CROWDINGP D1 (P 3 Y P 1 X I 2 PICKS I 1 PRED I 0 HOLES) J@iHhiBJi%@AIB IiIKlAhJZHX(51Q NO-CROWDINGP) NIL () NO-DUPLICATESP D1 (L (0 L)) @HYiI hI(20Q MEMB) NIL () NO-OP D1 NIL hNIL NIL () NON-RECURSIVE-DEFNP D1 (I 0 FNNAME F 0 TEMP-TEMP F 1 TEMPORARILY-DISABLED-LEMMAS F 2 DISABLED-LEMMAS) "@cQ PRh@gh@g(6 MEMB) (36Q SDEFN 25Q INDUCTION-MACHINE) () NORMALIZE-IFS D1 (P 14Q ARG P 6 BAD-ARG P 5 T13 P 4 T12 P 3 T11 P 2 T3 P 1 T2 P 0 T1 I 2 FALSE-TERMS I 1 TRUE-TERMS I 0 TERM F 15Q TRUE F 16Q FALSE F 17Q DEFINITELY-FALSE) % @ddB Wg@@ddgdddd@@HAB XdWdA IbHWHB Jb~HIHAB YJAHB ZIJXIgHHHHHHHgKgLIJhgMIJhhb H IWJ WHgHIJh0 @#d OAB _O Oh_O&_O bddBddg8dd1dd)dd!@@HIWbHI Wb@g@h__*h^bgHIN@ HAB JN@ AHB h_OgOOOoOOO@B @A @ W(1034Q BOOLEAN 1024Q MEMBER 1013Q MEMBER 704Q NORMALIZE-IFS 675Q SUBST-EXPR 667Q NORMALIZE-IFS 660Q SUBST-EXPR 607Q NOT-IDENT 507Q CONS-TERM 450Q NORMALIZE-IFS 403Q FALSE-NONFALSEP 371Q BOOLEAN 231Q NORMALIZE-IFS 220Q NORMALIZE-IFS 174Q MEMBER 153Q MEMBER 140Q NORMALIZE-IFS 13Q MEMB) (731Q COND 651Q IF 622Q QUOTE 525Q EQUAL 414Q IF 342Q IF 327Q IF 323Q IF 245Q IF 46Q IF 26Q QUOTE) ( 762Q (T1 T2 T3)) NOT-EQUAL-0? D1 (P 3 EQUALITY P 2 TEMP P 1 Y P 0 X I 0 TERM F 4 TEMP-TEMP F 5 ZERO F 6 FALSE F 7 TRUE) @@d*dg"ddd@YH @dgdd/@cg@Uh[d ddljVg@jWkjgKh(131Q TYPE-SET 56Q CL:NEGATE 53Q NOT-LESSP?) (176Q NOT 150Q QUOTE 116Q EQUAL 70Q ADD1 14Q DIFFERENCE) () NOT-IDENT D1 (I 1 TERM2 I 0 TERM1 F 0 TEMP-TEMP) U@cddgAcPg@A3@ A (A @ j@ A j@A A@ i(117Q SHELL-OCCUR 111Q SHELL-OCCUR 77Q TYPE-SET 73Q TYPE-SET 64Q SHELL-CONSTRUCTORP 57Q BTM-OBJECTP 51Q SHELL-CONSTRUCTORP 44Q BTM-OBJECTP) (31Q QUOTE 13Q QUOTE) () NOT-LESSP? D1 (P 1 TERM P 0 TEMP I 1 Y I 0 X F 2 TRUE F 3 FALSE) > Ao@ lj@ g@AhY XddkjRljSI (73Q CL:NEGATE 45Q TYPE-SET 27Q NOT-EQUAL-0? 15Q TYPE-SET) (33Q LESSP) ( 7 (QUOTE 1)) NOT-TO-BE-REWRITTENP D1 (I 1 ALIST I 0 TERM F 2 TERMS-TO-BE-IGNORED-BY-REWRITE F 3 TEMP-TEMP) /RHhA@ cR S@IIiHX(26Q MEMBER 20Q SUBLIS-VAR) NIL () NUMBERP? D1 (P 0 TEMP I 0 TERM F 1 TRUE F 2 FALSE) #@ XdljQlH Rg@h(26Q LOGSUBSETP 6 TYPE-SET) (34Q NUMBERP) () OBJ-TABLE D1 (I 2 ID-IFF I 1 OBJECTIVE I 0 TYPE-SET F 0 TRUE F 1 FALSE) iAdg@ljPBg=k@ hg@kjQAg!@dkjljBgk@ hogAhg (146Q ERROR1 121Q LOGSUBSETP 35Q LOGSUBSETP) (143Q HARD 134Q OBJECTIVE 111Q ID 63Q ? 44Q FALSE 25Q ID 4 TRUE) ( 131Q (PROGN UNRECOGNIZED REWRITE OBJECTIVE , (!PPR OBJECTIVE NIL) %.)) OCCUR D1 (P 1 ARG I 1 TERM2 I 0 TERM1 F 2 TEMP-TEMP) uA@AgE@cRg@d3 A  @ j@A @A @AAHh@I IiHX(150Q OCCUR 120Q EVG-OCCUR-OTHER 106Q EVG-OCCUR-LEGAL-CHAR-CODE-SEQ 71Q LAST 61Q LEGAL-CHAR-CODE-SEQ 53Q EVG-OCCUR-NUMBER) (31Q QUOTE 13Q QUOTE) () OCCUR-CNT D1 (P 2 ARG I 1 TERM2 I 0 TERM1) /@AkAjgAjHII@J ԹHX(46Q OCCUR-CNT) (17Q QUOTE) () OCCUR-LST D1 (P 1 Y I 1 LST I 0 X) AHh@I IiHX(20Q OCCUR) NIL () ONE-WAY-UNIFY D1 (I 1 TERM2 I 0 TERM1 F 0 UNIFY-SUBST) hc@A (7 ONE-WAY-UNIFY1) NIL () ONE-WAY-UNIFY-LIST D1 (P 3 TERM2 P 2 TERM1 I 1 TERM2-LIST I 0 TERM1-LIST F 4 UNIFY-SUBST) (hcA@"IHiJK hIH(33Q ONE-WAY-UNIFY1) NIL () ONE-WAY-UNIFY1 D1 (P 0 OLD-ALIST I 1 TERM2 I 0 TERM1 F 1 UNIFY-SUBST F 2 COMMUTED-EQUALITY-FLG) hcQX@A iHch(14Q ONE-WAY-UNIFY11) NIL () ONE-WAY-UNIFY11 D1 (P 4 ARG2 P 3 ARG1 P 0 SAVED-UNIFY-SUBST I 1 TERM2 I 0 TERM1 F 5 UNIFY-SUBST F 6 TEMP-TEMP F 7 COMMUTED-EQUALITY-FLG) @dUc @AUc Ag@AAh@Ac dg C@g*OB_@ _g0Oo_:O< __>O@k_@OF&_Ddoh_ O" O h_$O &_"O$Oh(732Q PACK 725Q UNPACK 675Q ADD-TO-SET 650Q COMMON-SWEEP 461Q MEMBER 451Q MEMBER 437Q MEMB 311Q REVERSE 257Q PATH-POT-SUBSUMES 235Q \NCONC2 232Q \APPEND2 200Q ALL-PATHS 152Q PARTITION 11Q INTERESTING-SUBTERMS) (720Q TEMP 715Q *2* 655Q LET 572Q VAR 564Q TEST 542Q SET 422Q TEST-AND-SET) ( 1011Q (QUOTE *1*X)) PARTITION D1 (P 2 L1 P 1 TEMP P 0 POT I 0 L) %0@dZH Y JhHXJh H(34Q \NCONC2 14Q SASSOC) NIL () PARTITION-CLAUSES D1 (P 11Q LIT P 10Q PAIR P 3 N P 2 POCKETS P 1 FLG P 0 ALIST I 0 LST F 17Q TEMP-TEMP) >P0@dhLNMh_M&Obdrd Obd_!OgOOh O_iOH cOIOhcHX jIWWjWOWh@ [HO@1 OhOcJJ_j!O KjOAOOJO__diO_OOh__O_O&_d_OOh__O_}O&_(316Q LENGTH 236Q LENGTH 135Q SASSOC) (75Q NOT) () PATH-ADD-TO-SET D1 (P 1 Y1 I 1 Y I 0 X) &AHhA@I IiHX@A(24Q PATH-EQ) NIL () PATH-EQ D1 (I 1 Y I 0 X) 0@ A jA@"IHiJKhIH(7 LENGTH 3 LENGTH) NIL () PATH-POT-SUBSUMES D1 (P 5 L P 3 S P 1 I I 1 SMALLER I 0 LARGER) U@ kkIHDAJ i2Ii@L hhKIM MiL\JZIkYh(71Q BM:NTH 4 LENGTH) NIL () PATH-UNION D1 (P 6 Y1 P 4 X1 I 1 Y I 0 X) D@AH IA AMhLJKhZHXLN NiM]K&(61Q PATH-EQ 15Q \NCONC2) NIL () PEGATE-LIT D1 (I 0 TERM F 0 DEFINITELY-FALSE F 1 FALSE F 2 TRUE) @ PQR@(3 FALSE-NONFALSEP) NIL () PETITIO-PRINCIPII D1 (I 5 DO-NOT-PRINT-DATE-LINE-FLG I 4 DO-NOT-PRINT-FIRST-EVENT-FLG I 3 DETACH-FLG I 2 FAILURE-ACTION I 1 ALL-FLG I 0 EVENTS) C@@/d[dggKKKhIHhZH&JABCDE (100Q REDO-UNDONE-EVENTS) (24Q ADD-AXIOM 15Q PROVE-LEMMA) () PICK-HIGH-SCORESA0001 D1 (L (0 CAND)) @NIL (3 CANDIDATE) () PICK-HIGH-SCORES D1 (I 0 CANDLST) @g (6 MAXIMAL-ELEMENTS) (3 PICK-HIGH-SCORESA0001) () PIGEON-HOLE D1 (P 0 PAIRLST I 4 DO-NOT-SMASH-FLG I 3 DO-NOT-CROWD-FLG I 2 FN I 1 HOLES I 0 PIGEONS) L 0AdhIKJh\J&LX@HBCD DA0HdKJh\J&L(52Q PIGEON-HOLE1) NIL () PIGEON-HOLE-IN-ALL-POSSIBLE-WAYSA0001 D1 (L (1 Y 0 X)) @ANIL NIL () PIGEON-HOLE-IN-ALL-POSSIBLE-WAYS D1 (P 16Q X P 12Q HOLE P 5 PIGEON P 2 X P 1 POT P 0 ANS I 3 DO-NOT-CROWD-FLG I 2 FN I 1 HOLES I 0 PIGEONS) @@LiC_Hg VhAA NOYHIh X5h_MOlBZOJ_OOh__N^O&_L\0H7d0 Kd_O Oh_O&_O^ON__OAA NO  _N_HOhO_O(Oh__N^_OOOiO_O&_(305Q LAST 301Q UNION-EQUAL 67Q \NCONC2 34Q NO-CROWDINGP) (31Q PIGEON-HOLE-IN-ALL-POSSIBLE-WAYSA0001) () PIGEON-HOLE1 D1 (P 4 PAIR P 2 OLD-HOLE P 1 OLD-FLG P 0 TEMP I 4 DO-NOT-SMASH-FLG I 3 DO-NOT-CROWD-FLG I 2 FN I 1 PAIRLST I 0 PIGEONS) UP@A[hiCL;@LlBX/LLDLHLi@ABCD iLJLIhLiK(74Q PIGEON-HOLE1) NIL () PLUSJOIN D1 (I 0 LST) @o@g@@ h(26Q PLUSJOIN) (17Q PLUS) ( 6 (ZERO)) POLY-MEMBER D1 (L (1 LST 0 POLY)) 4AHh@I@IIiHXNIL (44Q POLY 36Q POLY 25Q POLY 17Q POLY) () POP-CLAUSE-SET D1 (P 7 CL1 P 5 CL2 P 3 STACK-TAIL P 1 TEMP P 0 CL-SET F 10Q STACK)  Wi 5g"WWcgIhdW h WWcWJ[HL5i-KgUgHhdW K Kh h KKN hh_M OiN^L\gHhdW K Kh /*gHhWcH(322Q IO 306Q GET-STACK-NAME 301Q GET-STACK-NAME 244Q SUBSUMES 204Q WRAPUP 177Q IO 163Q GET-STACK-NAME 156Q GET-STACK-NAME 61Q IO 53Q GET-STACK-NAME 12Q WRAPUP) (336Q BEING-PROVED 271Q SUBSUMED-BELOW 146Q SUBSUMED-BY-PARENT 140Q BEING-PROVED 43Q POP 21Q BEING-PROVED) () POP-LEMMA-FRAME D1 (F 0 LEMMA-STACK) PPohg c(17Q ERROR1) (14Q HARD) ( 10Q (PROGN LEMMA-STACK IS TOO POOPED TO POP !)) POP-LINEARIZE-ASSUMPTIONS-FRAME D1 (F 0 LINEARIZE-ASSUMPTIONS-STACK) PPohg c(17Q ERROR1) (14Q HARD) ( 10Q (PROGN LINEARIZE-ASSUMPTIONS-STACK IS TOO POOPED TO POP !)) POPU D1 (F 0 UNDONE-EVENTS-STACK F 1 UNDONE-EVENTS) PcPcQNIL NIL () POSSIBLE-IND-PRINCIPLES D1 (P 10Q J P 3 MASK P 2 QUICK-BLOCK-INFO P 1 FORMALS P 0 MACHINE I 0 TERM F 11Q TEMP-TEMP F 12Q TEMPORARILY-DISABLED-LEMMAS F 13Q DISABLED-LEMMAS) o @@gY@gZ@gX@cW WWh@gALM_@OIJ [@IHOKJ _N Oh^L\O&(126Q FLESH-OUT-IND-PRIN 110Q SOUND-IND-PRIN-MASK 42Q MEMB) (62Q JUSTIFICATIONS 27Q INDUCTION-MACHINE 20Q QUICK-BLOCK-INFO 7 SDEFN) () POSSIBLY-NUMERIC D1 (P 0 TYPE-ALIST I 0 TERM F 1 HEURISTIC-TYPE-ALIST F 2 TYPE-ALIST) QR@ lj(12Q TYPE-SET) NIL () POWER-EVAL D1 (I 1 B I 0 L) @jA@A (15Q POWER-EVAL) NIL () POWER-REP D1 (I 1 B I 0 N) A@@h@A @AA (23Q POWER-REP 14Q REMAINDER) NIL () PPC D1 (I 0 CL) @ h(6 PPR 3 PRETTYIFY-CLAUSE) NIL () PPE D1 (I 0 X) @h (5 PPE-LST) NIL () PPE-LST D1 (P 0 NAME I 0 X) X@Qdh Hg6Hg%gHggggHggh gHo h h(117Q ITERPRI 112Q PPR 13Q ITERPRI) (100Q ***** 62Q EVENT 56Q MAIN-EVENT 52Q OF 47Q SATELLITE 44Q A 41Q IS 35Q ***** 27Q MAIN-EVENT 20Q EVENT) ( 105Q (IS NEITHER AN EVENT NOR SATELLITE)) PPR D1 (P 0 LEFTMARGINCHAR I 1 PPRFILE I 0 FMLA F 1 PPR-MACRO-LST) @jdQA h(13Q PPRIND) NIL () PPRINDENT D1 (I 3 FILE I 2 RPARCNT I 1 LEFTMARGIN I 0 TERM F 0 PPR-MACRO-LST) !C AAC AC @ABjPC (36Q PPRIND 21Q TABULATE 13Q ITERPRISPACES 3 IPOSITION) NIL () PPSD D1 (I 0 X) @h (5 PPSD-LST) NIL () PPSD-LST D1 (P 0 FNNAME I 0 X) +@$dHdggh h h h(42Q ITERPRI 35Q ITERPRI 30Q PPR) (22Q UNDEFINED 14Q SDEFN) () PREPROCESS D1 (P 0 TYPE-ALIST I 0 TERM F 1 ABBREVIATIONS-USED) hc@ (14Q CLAUSIFY-INPUT 11Q EXPAND-ABBREVIATIONS) NIL () PREPROCESS-HYPS D1 (P 3 X P 2 HYP I 0 HYPS F 4 ZERO) @1HIIJdRdgJdEd?dg5d.d'd"gKhggKThhh,&JdgddggKhhJh HXr(216Q \NCONC2) (200Q LISTP 175Q NOT 152Q NLISTP 123Q EQUAL 120Q NOT 111Q NUMBERP 53Q ZEROP 26Q NOT) () PRETTYIFY-CLAUSE D1 (P 4 TAIL I 0 CL F 5 FALSE) T@U@@g@ @hgg@AH\I@ hL J KhZLK&(100Q DUMB-NEGATE-LIT 63Q LAST 25Q DUMB-NEGATE-LIT) (43Q AND 40Q IMPLIES 20Q IMPLIES) () PRETTYIFY-LISP D1 (I 0 X) @ (11Q REMOVE-*2*IFS 6 INTRODUCE-ANDS 3 INTRODUCE-LISTS) NIL () PRIMITIVE-RECURSIVEP D1 (P 10Q TERM P 7 VAR P 4 CASE P 2 X P 0 FORMALS I 0 FNNAME F 11Q TEMP-TEMP F 12Q TEMPORARILY-DISABLED-LEMMAS F 13Q DISABLED-LEMMAS) { @gX@cW WW@gIiZKi:h\H"N_M ih_OO hNMK[IY(143Q SHELL-DESTRUCTOR-NESTP 22Q MEMB) (57Q TESTS-AND-CASES 40Q INDUCTION-MACHINE 6 SDEFN) () PRIMITIVEP D1 (P 1 ARG I 0 TERM F 2 TEMP-TEMP F 3 TEMPORARILY-DISABLED-LEMMAS F 4 DISABLED-LEMMAS) F@h3@g+@dgcS RT@g @HiY hHX(74Q PRIMITIVEP 35Q MEMB) (51Q NOT 23Q SDEFN 12Q QUOTE) () PRINT-STACK D1 (P 0 X I 0 Y) @dHi gh(13Q IPRINT) (20Q CADR) () PRINT-STATS D1 (I 2 FILE I 1 IO I 0 ELAPSED) /B oB kB @B kB AB kB oB (54Q IPRINC 44Q ISPACES 37Q IPRINC 32Q ISPACES 25Q IPRINC 20Q ISPACES 13Q IPRINC 3 ITERPRI) NIL ( 50Q ")" 7 "(") PRINT-TO-DISPLAY D1 (P 1 I I 2 MSG3 I 1 MSG2 I 0 MSG1 F 2 LEMMA-DISPLAY-FLG F 3 LEMMA-STACK) {RhvRgJS kkIHoi IkYoi @i Aki Ai Bi i kS @i Aki Ai Bdi (170Q IPRINC 160Q IPRINC 152Q ISPACES 143Q IPRINC 136Q ERASE-EOP 133Q PUT-CURSOR 130Q STACK-DEPTH 120Q IPRINC 113Q ITERPRI 103Q IPRINC 75Q ISPACES 66Q IPRINC 61Q IPRINC 41Q IPRINC 17Q STACK-DEPTH) (10Q MODEL33) ( 55Q "*" 35Q "/") PROCESS-EQUATIONAL-POLYS D1 (P 2 PAIR P 1 POT I 2 POT-LST I 1 HIST I 0 CL F 3 LEMMAS-USED-BY-LINEAR F 4 LINEAR-ASSUMPTIONS) lhcdcB!H@AI ZLJJ JJ@ 3JJJ JJ@ ggJJhhJJ@ bHX(141Q SUBST-EXPR-LST 106Q SUBST-VAR-LST 75Q OCCUR 57Q SUBST-VAR-LST 46Q OCCUR 26Q FIND-EQUATIONAL-POLY) (116Q EQUAL 113Q NOT) () PROPERTYLESS-SYMBOLP D1 (I 0 X) @ @o (15Q MEMB 3 CAR-CDRP) NIL ( 12Q (NIL QUOTE LIST T F)) PROVE D1 (P 5 LOOP-ANS P 4 CL P 2 VARS P 1 CLAUSES P 0 THM I 0 FORM F 6 ABBREVIATIONS-USED F 7 ELIM-VARIABLE-NAMES F 10Q GEN-VARIABLE-NAMES1 F 11Q ELIM-VARIABLE-NAMES1 F 12Q GEN-VARIABLE-NAMES) N0@ X @IV I!K%MWJ cWJ cI  Y\ M K[(106Q UNIONQ 102Q ALL-VARS-LST 72Q INDUCT 67Q POP-CLAUSE-SET 63Q SIMPLIFY-LOOP 54Q SET-DIFF 43Q SET-DIFF 21Q SETUP 12Q PREPROCESS 6 TRANSLATE) NIL () PROVE-TERMINATION D1 (P 1 X I 2 MACHINE I 1 RM I 0 FORMALS F 5 PROVE-TERMINATION-LEMMAS-USED F 6 PROCESS-CLAUSES F 7 PROCESS-HIST) jhc BHi0Id KJh\J&LA@IA Ah h VWU c ihhHX(132Q UNION-EQUAL 120Q SIMPLIFY-CLAUSE-MAXIMALLY 115Q \NCONC2 110Q CONS-TERM 77Q SUB-PAIR-VAR 36Q NEGATE-LIT) (67Q TESTS-AND-CASE 25Q TESTS-AND-CASE) () PROVEALL D1 (I 2 FILENAME I 1 DETACH-FLG I 0 EVENT-LST F 0 MASTER-ROOT-NAME F 1 FAILED-THMS F 2 PROVE-FILE F 3 TTY-FILE) hcBgchcdc@igA P (35Q MAKE-LIB 31Q REDO-UNDONE-EVENTS) (25Q A 10Q PROVEALL) () PUSH-CLAUSE-SET D1 (L (0 CL-SET) F 0 STACK) g@hPcNIL (2 TO-BE-PROVED) () PUSH-LEMMA D1 (L (0 ELE) F 0 LEMMA-STACK) @P hP@Ph(5 MEMB) NIL () PUSH-LEMMA-FRAME D1 (F 0 LEMMA-STACK) hPchNIL NIL () PUSH-LINEARIZE-ASSUMPTION D1 (I 0 ELE F 0 LINEARIZE-ASSUMPTIONS-STACK) P@P h(6 ADD-TO-SET) NIL () PUSH-LINEARIZE-ASSUMPTIONS-FRAME D1 (F 0 LINEARIZE-ASSUMPTIONS-STACK) hPchNIL NIL () PUSHU D1 (F 0 UNDONE-EVENTS F 1 UNDONE-EVENTS-STACK) PQchcNIL NIL () PUT-CURSOR D1 (I 1 Y I 0 X) A@ (4 CURSORPOS) NIL () PUT-INDUCTION-INFO D1 (P 11Q RM P 1 I-MACHINE P 0 T-MACHINE I 4 TAK0 I 3 RELATION-MEASURE-LST I 2 BODY I 1 FORMALS I 0 FNNAME F 12Q ALL-LEMMAS-USED F 13Q PROVE-TERMINATION-LEMMAS-USED) PD@B XdhcCAH b@gCA M#N `dAh hc@D\dDB U_AOH :`O dJOdKOdLdW_OOh_M]O&_B Y@gI @gAI h(263Q ADD-FACT 260Q QUICK-BLOCK-INFO 247Q ADD-FACT 236Q INDUCTION-MACHINE 140Q ALL-VARS 123Q PROVE-TERMINATION 106Q SUBST-FN 71Q ADD-FACT 30Q GUESS-RELATION-MEASURE-LST 12Q TERMINATION-MACHINE) (253Q QUICK-BLOCK-INFO 243Q INDUCTION-MACHINE 130Q JUSTIFICATIONTYPE# 56Q JUSTIFICATIONTYPE# 37Q JUSTIFICATIONS) () PUT-LEVEL-NO D1 (P 3 FN P 1 MAX P 0 BODY I 0 FNNAME) F @gXjYH J@g@H Ikذ[d@ dIIYJZI (103Q ADD-FACT 62Q GET-LEVEL-NO 42Q FNNAMEP 21Q ALL-FNNAMES) (35Q LEVEL-NO 6 SDEFN) () PUT-TYPE-PRESCRIPTION D1 (P 6 TEMP P 5 ANS P 4 TYPE-ALIST P 3 FORMALS P 2 BODY P 1 NEW-TYPE-PRESCRIPTION P 0 OLD-TYPE-PRESCRIPTION I 0 NAME) X@gZJ0 K"d_jOh_O Oh_O&_Oj0 Kh_O Oh_O&_O@g@H @g^H@Ng J ]0 K!dM i_O Oh_O&_OHI0IH DHI" O_Oi*ohg h_OOhO_O_HIIHRO_O OXI_OO_OOh__O_O_O&_(346Q ERROR1 277Q LOGSUBSETP 223Q MEMB 204Q DEFN-TYPE-SET 177Q PUTPROP 154Q ADD-FACT) (343Q WARNING 174Q TYPE-PRESCRIPTION-LST 161Q TYPE-PRESCRIPTION-LST 146Q TYPE-PRESCRIPTION-LST 6 SDEFN) ( 337Q (PROGN AN UNEXPECTED SITUATION HAS ARISEN ! THE DEFN-TYPE-SET ITERATION STOPPED BECAUSE OF A PROPER SUBSET CHECK RATHER THAN THE EQUALITY OF THE OLD AND NEW TYPE SETS %.)) PUT0 D1 (I 3 HIGHER-PROPS I 2 VAL I 1 PROP I 0 ATM F 0 LIB-PROPS) .CAP bogAhg @d AB B(52Q SETPROPLIST 47Q PUT00 42Q GETPROPLIST 34Q ERROR1 7 MEMB) (31Q HARD 22Q PROP) ( 17Q (PROGN ATTEMPT TO PUT1 THE NON-LIB-PROPS PROPERTY (!PPR PROP NIL) %.)) PUT00 D1 (I 2 VAL I 1 PROP I 0 TAIL F 0 HIGHER-PROPS) <@ABhA@@B@@P @d@AB @ABh AB@(63Q \NCONC2 50Q PUT00 30Q MEMB) NIL () PUT1 D1 (P 0 HIGHER-PROPS I 2 PROP I 1 VAL I 0 ATM F 1 LIB-ATOMS-WITH-PROPS F 2 LIB-PROPS) Fg ohg 'BR XogBhg @dQ Qc@BAH (103Q PUT0 66Q MEMB 57Q ERROR1 33Q MEMB 24Q ERROR1 10Q BOUNDP) (54Q HARD 45Q PROP 21Q HARD 5 LIB-PROPS) ( 42Q (PROGN ATTEMPT TO USE PUT1 TO STORE THE NON-LIB-PROPS PROPERTY (!PPR PROP NIL) %.) 15Q (PROGN THEOREM PROVER NOT INITIALIZED %.)) PUT1-LST D1 (I 1 PROPS I 0 ATM) @A@ (13Q SETPROPLIST 10Q \APPEND2 5 GETPROPLIST) NIL () PUTD1 D1 (I 1 EXPR I 0 ATM F 0 LIB-ATOMS-WITH-DEFS) A@P c@ @Pc@A (27Q STORE-DEFINITION 14Q KILL-DEFINITION 6 DREMOVE) NIL () QUICK-BLOCK-INFO D1 (P 10Q TAIL P 7 ARG P 6 VAR P 2 TESTS-AND-CASES P 1 CASE P 0 BLOCK-TYPES I 1 TESTS-AND-CASES-LST I 0 FORMALS) 00@gLKh]K&MXA4dZ&dHI@3K_ML_O Hdg!gONO ONO OgMLO(166Q QUICK-BLOCK-INFO1 154Q QUICK-BLOCK-INFO1) (175Q QUESTIONABLE 142Q UN-INITIALIZED 134Q QUESTIONABLE 46Q TESTS-AND-CASES 12Q UN-INITIALIZED) () QUICK-BLOCK-INFO1 D1 (I 1 TERM I 0 VAR) @dAgA gg(14Q OCCUR) (24Q QUESTIONABLE 20Q SELF-REFLEXIVE 7 UNCHANGING) () QUICK-WORSE-THAN D1 (P 3 ARG2 P 2 ARG1 I 1 TERM2 I 0 TERM1 F 4 TEMP-TEMP) A @A.A@ g@ig@ A @hg@A@AA@"IHhA@"I9=JJcTgKdcTgKJ JiIHHhJK JiIH(260Q WORSE-THAN 222Q WORSE-THAN 56Q FORM-COUNT-EVG 50Q FORM-COUNT-EVG 15Q OCCUR) (213Q QUOTE 174Q QUOTE 72Q QUOTE 37Q QUOTE 22Q QUOTE) () R D1 (I 0 FORM F 0 R-ALIST F 1 TEMP-TEMP) #@ b h@P cdgo (40Q EXPAND-PPR-MACROS 20Q REDUCE 10Q ERRSET 3 TRANSLATE) (26Q *1*FAILED) ( 34Q (NOT REDUCIBLE)) REDO! D1 (I 0 NAME) @ ighid (16Q REDO-UNDONE-EVENTS 3 UNDO-NAME) (7 C) () REDO-UNDONE-EVENTS D1 (P 4 UNDONE-EVENTS P 3 FORM P 2 ANSLST P 1 ANS P 0 IN-REDO-UNDONE-EVENTS-FLG I 5 DO-NOT-PRINT-DATE-LINE-FLG I 4 DO-NOT-PRINT-FIRST-EVENT-FLG I 3 DETACH-FLG I 2 FAILURE-ACTION I 1 ALL-FLG I 0 EVENTS F 5 PROVE-FILE F 6 TTY-FILE F 7 UNDONE-EVENTS F 10Q IN-REDO-UNDONE-EVENTS-FLG F 11Q FAILURE-MSG F 12Q FAILED-THMS F 13Q BOOK-SYNTAX-FLG F 14Q PPR-MACRO-LST) Wohg i1BgbV hc U hc Cib@cEWJU8kU gU U oU U WU U U hc VJ hc DK@UJkU gU lU WKhUlU hi KjdWU U UKi Ko AK@o KK Igg "DK@U-IU "UIi Wi i oi JIh I{Bdg^KgTlU ggkK lK lK hhU U gkK lK lK h U Bg{Ko nWchb](731Q MEMB 704Q IPRINT 700Q APPLY 671Q BM:NTH 663Q BM:NTH 655Q BM:NTH 644Q ITERPRI 637Q PPR 623Q BM:NTH 615Q BM:NTH 607Q BM:NTH 573Q ITERPRIN 540Q \NCONC2 530Q IPRINC 517Q ITERPRI 512Q IPRINC 503Q ITERPRI 467Q DETACHEDP 463Q IPRINT 441Q AN-ERROR 424Q STOP-STATS 417Q APPLY 404Q START-STATS 375Q IPRINC 355Q MEMB 343Q IPRINC 333Q DETACHEDP 325Q ITERPRI 320Q PPRIND 305Q DUMP 277Q LINEL 260Q ITERPRIN 251Q IPRINC 241Q ITERPRIN 211Q CLOSEF 174Q CLOSEF 167Q ITERPRI 162Q PPR 153Q ITERPRI 146Q IPRINC 135Q PRINT-SYSTEM 130Q IPRINC 120Q ITERPRIN 103Q PRINT-DATE-LINE 71Q DETACH 57Q PREPARE-FOR-THE-NIGHT 47Q OPENP 36Q OPENP 15Q ERROR1) (713Q Q 650Q ADD-AXIOM 602Q ADD-AXIOM 577Q COMMENT 562Q PROVE-LEMMA 551Q A 436Q REDO-UNDONE-EVENTS 431Q *****ERROR***** 245Q % 124Q % 27Q Q 12Q HARD) ( 726Q (ADD-AXIOM ADD-SHELL DCL) 524Q "," 372Q "DO YOU WANT TO REDO THIS EVENT?" 352Q (DEFN REFLECT) 142Q "REDO-UNDONE-EVENTS COMPLETED. HERE IS FAILED-THMS:" 6 (PROGN IT IS ILLEGAL TO ENTER A THEOREM PROVER FUNCTION WHILE YOU ARE RECURSIVELY UNDER ANOTHER THEOREM PROVER FUNCTION %.)) REDUCE D1 (I 1 ALIST I 0 TERM) g@A h(7 REDUCE1) (2 QUOTE) () REDUCE1 D1 (P 3 ARG I 1 ALIST I 0 TERM F 4 TEMP-TEMP) @@Ac gg g@@dgA g@b@bgc@ dkjTdl@A kTdl@A @A lTl @A @A @A lTT@@d[A IHhZH&J (320Q APPLY 273Q REDUCE1 247Q REDUCE1 236Q REDUCE1 226Q REDUCE1 204Q REDUCE1 174Q REDUCE1 151Q REDUCE1 122Q LENGTH 57Q REDUCE1 23Q RETFROM) (111Q LISP-CODE 62Q *1*FALSE 46Q IF 32Q QUOTE 20Q *1*FAILED 15Q REDUCE) () REFLECT0 D1 (P 20Q ARG P 13Q TEMP P 5 BODY P 4 ARGS P 3 FN P 2 CONTROL-VARS P 1 TRANSLATED-BODY P 0 META-NAMES I 3 FLG I 2 RELATION-MEASURE-LST I 1 SATISFACTION-LEMMA-NAME I 0 NAME F 21Q MATCH-TEMP F 22Q TEMP-TEMP F 23Q META-NAMES) @W&qA c" M Y@ B\gW"W"W"W"W"W"W"]d_O h_O Oh_O&_Ob@LIBK @ggL@KI h @gKg @ @g@g@g1O#O Ci@gg@h Ljd O$O_OOh__O_O&_J OkO_O_Ok_I h_^in@g@h g@L;_@OghNd_ gO h _O Oh_O&_Oc$LW$@KI h @ og@hg h(711Q ERROR1 666Q TOTAL-FUNCTIONP 661Q ADD-DCELL 652Q TRANSLATE-TO-LISP 647Q SUB-PAIR-VAR 644Q SUBST-FN 576Q PACK 521Q PACK 473Q ALL-FNNAMES 435Q MEMB 341Q ADD-FACT 336Q PACK 314Q ADD-FACT 311Q SCRUNCH 253Q PUT-LEVEL-NO 247Q ADD-FACT 232Q ADD-FACT 223Q SUBST-FN 205Q PUT-INDUCTION-INFO 134Q TRANSLATE 23Q TRANSLATE 12Q FORMULA-OF) (706Q WARNING 677Q NAME 566Q *3* 545Q LISP-CODE 524Q LAMBDA 512Q *1* 350Q JUSTIFICATION 327Q *1* 324Q LISP-CODE 272Q JUSTIFICATIONS 266Q CONTROLLER-POCKETS 257Q JUSTIFICATIONS 242Q TYPE-PRESCRIPTION-LST 236Q TYPE-PRESCRIPTION-LST 214Q LAMBDA 211Q SDEFN 36Q EQUAL) ( 674Q (PROGN THE RECURSION IN (!PPR NAME NIL) IS UNJUSTIFIED %.)) RELIEVE-HYPS D1 (I 1 LEMMA-NAME I 0 HYPS) 4@A d d ih(60Q POP-LINEARIZE-ASSUMPTIONS-FRAME 55Q POP-LEMMA-FRAME 43Q PUSH-LINEARIZE-ASSUMPTION 35Q POP-LINEARIZE-ASSUMPTIONS-FRAME 25Q PUSH-LEMMA 17Q POP-LEMMA-FRAME 12Q RELIEVE-HYPS1 5 PUSH-LINEARIZE-ASSUMPTIONS-FRAME 2 PUSH-LEMMA-FRAME) NIL () RELIEVE-HYPS-NOT-OK D1 (P 3 ANS P 1 ANS-ATOM P 0 LIT-ATOM I 0 LIT F 4 RELIEVE-HYPS-NOT-OK-ANS F 5 ANCESTORS) m@@XddgdddUZh[Y @Kic1gKKKH I HI hciKiJ(133Q WORSE-THAN-OR-EQUAL 124Q GREATEREQP 121Q FORM-COUNT 115Q FORM-COUNT) (66Q NOT 15Q NOT) () RELIEVE-HYPS1 D1 (P 10Q ANCESTORS P 7 RHS P 6 LHS P 5 CHECK-FLG P 4 SPLIT-FLG P 3 HYP P 1 I I 1 LEMMA-NAME I 0 HYPS F 11Q UNIFY-SUBST F 12Q LAST-EXIT F 13Q INST-HYP F 14Q TYPE-ALIST F 15Q ANCESTORS F 16Q LAST-HYP F 17Q RELIEVE-HYPS-NOT-OK-ANS F 20Q DEFINITELY-FALSE F 21Q LITS-THAT-MAY-BE-ASSUMED-FALSE F 22Q FALSE F 23Q TRUE)  @kiSH:AIg KKgKKhKi\ KKgKKhKiK iKW hKdSdgKdFd@d:K_N+NW%OW NOWWgg WcK i~gchuWK c gcW_W gcW hMWW" gchA@AghRHh@AbbAI IiHX(60Q MEMB) (13Q QUOTE) () SHELL-OCCUR D1 (P 4 TR P 3 ARG P 0 TYPE-SET-TERM1 I 1 TERM2 I 0 TERM1 F 5 SHELL-ALIST F 6 TEMP-TEMP) \@ AhgAU@ XAgA"JIh@K c JIL Ki(123Q LOGSUBSETP 76Q SHELL-OCCUR1 36Q TYPE-SET 6 SHELLP) (116Q TYPE-RESTRICTION 44Q TYPE-RESTRICTIONS 21Q QUOTE) () SHELL-OCCUR1 D1 (P 3 TR P 2 ARG I 1 TERM2 I 0 TERM1 F 4 TYPE-SET-TERM1 F 5 SHELL-ALIST F 6 TEMP-TEMP) b@ATAhgAU%AgA"IHh Ag@J c IHK Ji(130Q LOGSUBSETP 103Q SHELL-OCCUR1) (123Q TYPE-RESTRICTION 67Q TYPE-PRESCRIPTION-LST 35Q TYPE-RESTRICTIONS 17Q QUOTE) () SHELLP D1 (I 0 TERM F 0 *1*BTM-OBJECTS F 1 SHELL-ALIST) @hgi@P @Q(23Q MEMB) (11Q QUOTE) () SIMPLIFY-CLAUSE D1 (P 11Q TERM P 2 ANS P 1 EXPAND-LST P 0 TERMS-TO-BE-IGNORED-BY-REWRITE I 1 HIST I 0 CURRENT-SIMPLIFY-CL F 12Q PROCESS-CLAUSES F 13Q ALL-LEMMAS-USED F 14Q INDUCTION-HYP-TERMS F 15Q TERMS-TO-BE-IGNORED-BY-REWRITE F 16Q EXPAND-LST F 17Q TEMP-TEMP F 20Q INDUCTION-CONCL-TERMS F 21Q PROCESS-HIST) WW2gAcCWH W I @A c1MENc"d[_W kjW@hAW Oih_@ hO_dd_OOh_^M]O&_\LdW WcK(245Q MEMB 154Q DUMB-OCCUR-LST 102Q LENGTH 55Q POP-LEMMA-FRAME 50Q SIMPLIFY-CLAUSE0 43Q PUSH-LEMMA-FRAME 40Q INIT-LEMMA-STACK 34Q \APPEND2 25Q \APPEND2) (11Q SETTLED-DOWN-CLAUSE) () SIMPLIFY-CLAUSE-MAXIMALLY D1 (P 1 SIMPLIFY-CLAUSE-MAXIMALLY-HIST P 0 SIMPLIFY-CLAUSE-MAXIMALLY-CLAUSES I 0 CURRENT-CL F 2 PROCESS-HIST F 3 PROCESS-CLAUSES)  @ IcHcd@hh(6 SIMPLIFY-CLAUSE-MAXIMALLY1) NIL () SIMPLIFY-CLAUSE-MAXIMALLY1 D1 (I 0 CL F 2 SIMPLIFY-CLAUSE-MAXIMALLY-HIST F 3 SIMPLIFY-CLAUSE-MAXIMALLY-CLAUSES F 4 PROCESS-HIST F 5 PROCESS-CLAUSES) :@ /THUYIdR RcHXd h@Sc(53Q SIMPLIFY-CLAUSE-MAXIMALLY1 33Q MEMB 3 SIMPLIFY-CLAUSE) NIL () SIMPLIFY-CLAUSE0 D1 (P 13Q CL P 12Q LIT P 10Q HYP P 3 NEG-HYPS P 2 CLS P 1 SIMPLIFY-CLAUSE-POT-LST P 0 TYPE-ALIST I 1 HIST I 0 CL F 14Q LINEAR-ASSUMPTIONS F 15Q LEMMAS-USED-BY-LINEAR) @@ bd Xdgh@H Igh@AI hZ kjJ@g Wd WALMc0WW_@ OhO_N'Oh^L\_OO OiO_O&d MLh^L&N0Jd KO MLh^L&NWd@JJ@hdk (373Q SIMPLIFY-CLAUSE1 320Q DISJOIN-CLAUSES 254Q DUMB-NEGATE-LIT 222Q COMPLEMENTARYP 112Q PUSH-LEMMA 101Q PUSH-LEMMA 56Q LENGTH 50Q PROCESS-EQUATIONAL-POLYS 32Q SET-SIMPLIFY-CLAUSE-POT-LST 14Q TYPE-ALIST-CLAUSE 6 REMOVE-TRIVIAL-EQUATIONS) (76Q ZERO 36Q CONTRADICTION 21Q CONTRADICTION) () SIMPLIFY-CLAUSE1 D1 (P 20Q HYP P 14Q CL P 12Q SEG P 6 BRANCHES P 5 CURRENT-ATM P 4 CURRENT-LIT P 3 NEG-HYPS P 2 TYPE-ALIST P 1 SEGS P 0 VAL I 3 I I 2 LITS-TO-BE-IGNORED-BY-LINEAR I 1 NEW-CLAUSE I 0 TAIL F 21Q LINEAR-ASSUMPTIONS F 22Q FNSTACK) Qp@AhgC @]\ddgddLBbhc$A Zgh@ ZgMhJgg LMH c"0 W"d _O Oh_O&_OH 0 N#d KO _O Oh_O&_OW"L BOO 0 IX_ O _OOh__O_O&_d @AO NoBBCk _OO__O _O(510Q LAST 456Q SIMPLIFY-CLAUSE1 435Q \APPEND2 361Q ADD-LITERAL 342Q CONJOIN-CLAUSE-SETS 324Q ADD-LITERAL 321Q PEGATE-LIT 257Q DISJOIN-CLAUSES 235Q CLAUSIFY 175Q NEGATE-LIT 156Q POP-LINEARIZE-ASSUMPTIONS-FRAME 152Q NEGATE-LIT 141Q REWRITE 123Q PUSH-LINEARIZE-ASSUMPTIONS-FRAME 117Q INIT-LINEARIZE-ASSUMPTIONS-STACK 105Q TYPE-ALIST-CLAUSE 70Q TYPE-ALIST-CLAUSE 17Q PRINT-TO-DISPLAY) (135Q IFF 132Q ? 111Q CONTRADICTION 74Q CONTRADICTION 35Q NOT 13Q SIMPLIFY-CLAUSE) ( 442Q (NIL)) SIMPLIFY-LOOP D1 (P 0 CURRENT-CL I 0 CLAUSES) @dH h(12Q SIMPLIFY-SENT) NIL () SIMPLIFY-SENT D1 (I 1 HIST I 0 CL) g@Agg (16Q EXECUTE) (12Q SETTLED-DOWN-SENT 7 SIMPLIFY-SENT 2 SIMPLIFY-CLAUSE) () SINGLETON-CONSTRUCTOR-TO-RECOGNIZER D1 (I 0 FNNAME F 2 TEMP-TEMP F 3 SHELL-ALIST F 4 SINGLETON-TYPE-SETS F 5 RECOGNIZER-ALIST) 0@SckRcdT UHhRIIHX(21Q MEMBER) NIL () SKO-DEST-NESTP D1 (P 1 X I 1 DEEPFLG I 0 TERM F 2 TEMP-TEMP F 3 TEMPORARILY-DISABLED-LEMMAS F 4 DISABLED-LEMMAS) ]@igh@gcdcS RTA@HiYA HX@HiHX(100Q SKO-DEST-NESTP 43Q MEMB) (33Q REWRITE-RULE 22Q ELIMINATE-DESTRUCTORS-SEQ 11Q QUOTE) () SOME-SUBTERM-WORSE-THAN-OR-EQUAL D1 (P 1 ARG I 1 TERM2 I 0 TERM1) 6@dAA%@A @dgHhYA IiHX(51Q SOME-SUBTERM-WORSE-THAN-OR-EQUAL 17Q QUICK-WORSE-THAN) (27Q QUOTE) () SORT-DESTRUCTOR-CANDIDATESA0001 D1 (P 2 TERM I 1 Y I 0 X) 9@jHIAjHIIJ ԹHXIJ ԹHX(60Q GET-LEVEL-NO 41Q GET-LEVEL-NO) NIL () SORT-DESTRUCTOR-CANDIDATES D1 (I 0 LST) @ g (11Q SORT 3 REVERSE) (6 SORT-DESTRUCTOR-CANDIDATESA0001) () SOUND-IND-PRIN-MASK D1 (P 26Q VAR P 25Q Q P 24Q ACTUAL P 12Q LOOP-ANS P 11Q Q P 10Q VAR P 7 ACTUAL P 2 CHANGEABLES P 1 SUBSET P 0 UNCHANGEABLES I 3 QUICK-BLOCK-INFO I 2 FORMALS I 1 JUSTIFICATION I 0 TERM) @AYCB@C N_M_LOXCB@cO/@_OI OgO O _NML_"O_$OOZd J[NJH Oh_&O$I O&gO"_ O O h__O_O_O_kO &_KBC@cO _(O_*OO"_,I O*gggO(EO*g;O(dJ (h_&O$HO&h_$_"O _ O_O_H gO(O(J O(H O(JgO&&_$(561Q MEMB 551Q MEMB 530Q ADD-TO-SET 454Q MEMB 405Q MEMB 231Q MEMB 213Q INTERSECTP 177Q NO-DUPLICATESP 126Q UNIONQ 121Q ALL-VARS 103Q MEMB) (573Q CHANGEABLE 534Q UNCHANGEABLE 442Q UNCHANGING 426Q CHANGEABLE 421Q UNCHANGEABLE 414Q UNCHANGING 240Q UNCHANGING 112Q UNCHANGING 6 JUSTIFICATION) () STACK-DEPTH D1 (I 0 STK) @ k(3 LENGTH) NIL () START-STATS D1 (F 0 ELAPSEDTHMTIME F 1 IOTHMTIME) cjc(2 TIME-IN-60THS) NIL () STOP-STATS D1 (F 0 IOTHMTIME F 1 ELAPSEDTHMTIME F 2 PROVE-FILE) Q PoPoR (35Q PRINT-STATS 6 TIME-DIFFERENCE 2 TIME-IN-60THS) (24Q FLOATP 13Q FLOATP) ( 30Q 60.0 17Q 60.0) STORE-SENT D1 (P 0 CL-SET I 1 HIST I 0 CL F 3 STACK F 4 DO-NOT-USE-INDUCTION-FLG F 5 THM F 6 IN-PROVE-LEMMA-FLG F 7 HINTS) 0@g@AhS h h Tg@AhS gh h VgWTSAhY6hSFgS?hcUg Xg@hdS Hh H g Zo JiI@hXg@AhS h H (252Q PUSH-CLAUSE-SET 246Q IO 240Q GET-STACK-NAME 207Q MEMB 174Q RETFROM 166Q PUSH-CLAUSE-SET 162Q IO 152Q GET-STACK-NAME 137Q CNF-DNF 65Q WRAPUP 61Q IO 47Q GET-STACK-NAME 31Q WRAPUP 25Q IO 17Q GET-STACK-NAME) (231Q STORE-SENT 171Q SIMPLIFY-LOOP 143Q STORE-SENT 134Q C 121Q BEING-PROVED 73Q INDUCT 52Q QUIT 40Q STORE-SENT 10Q STORE-SENT) ( 204Q (SETTLED-DOWN-CLAUSE SIMPLIFY-CLAUSE SETUP)) STRIP-BRANCHES D1 (P 5 PAIR P 0 CL I 0 TERM F 6 TRUE-CLAUSE) T@ddgddbid i AIJ] Mi XVHK Lh[IYL&(72Q ADD-LITERAL 64Q PEGATE-LIT 45Q STRIP-BRANCHES1 40Q STRIP-BRANCHES1) (14Q NOT) () STRIP-BRANCHES1 D1 (P 32Q ANS P 31Q PAIR P 27Q PICK P 22Q ARG P 16Q PAIR3 P 14Q PAIR2 P 12Q PAIR P 5 NEW-CL P 4 LST P 3 ANS P 2 ANS3 P 1 ANS2 P 0 ANS1 I 2 NEGATE-FLG I 1 TOPFLG I 0 TERM F 33Q FALSE F 34Q TRUE-CLAUSE F 35Q TRUE) `@B@ @hhg)A@W6BhBW6hhB@W6W:@gpAB@W6B_@W:U@A A NO@AB _ Oi ]W8W6M_OOh__N^O&_AmB@W6B`@W:W@Ai A NO@AB _ Oi ]W8W6M_OOh__N^O&_@ X@AB Y@AB ZHd I OJO2L_OO O [W8KLO__OO O [W8KLO_@@d_$ _O Oh_"O&_ O" AO&O(_.B-@0O.dONh_N&_O (@0O.dONh_N&_O O.!O0&O4_,O*O,h_*_(O&_&O,&_*_2O4W8O2O4 _4O0_0(1207Q DISJOIN-CLAUSES 1106Q SCONS-TERM 1036Q DUMB-NEGATE-LIT 1033Q SCONS-TERM 743Q ALL-PICKS 705Q STRIP-BRANCHES1 646Q DISJOIN-CLAUSES 643Q ADD-LITERAL 635Q PEGATE-LIT 576Q DISJOIN-CLAUSES 573Q ADD-LITERAL 565Q NEGATE-LIT 504Q STRIP-BRANCHES1 471Q STRIP-BRANCHES1 457Q STRIP-BRANCHES1 402Q ADD-LITERAL 373Q PEGATE-LIT 363Q \APPEND2 360Q STRIP-BRANCHES1 334Q STRIP-BRANCHES1 224Q ADD-LITERAL 215Q PEGATE-LIT 205Q \APPEND2 202Q STRIP-BRANCHES1 157Q STRIP-BRANCHES1 14Q NEGATE-LIT) (106Q IF 27Q QUOTE) () SUB-SEQUENCEP D1 (L (1 LARGER 0 SMALLER)) #@iAh@A@AbbAbNIL NIL () SUBBAGP D1 (I 1 BAG2 I 0 BAG1) "@iAh@A @@A bb(31Q DELETE1 17Q MEMBER) NIL () SUBLIS-EXPR D1 (P 0 PAIR I 1 FORM I 0 ALIST F 1 TEMP-TEMP) )@dHc @A gH (44Q SUBST-EXPR-ERROR1 27Q SUBLIS-EXPR1) (34Q QUOTE) () SUBLIS-EXPR1 D1 (P 3 ARG I 1 FORM I 0 ALIST F 4 TEMP-TEMP) ?A@ cAAgA@Ad@K IHhZH&J (74Q CONS-TERM 47Q SUBLIS-EXPR1 4 SASSOC) (24Q QUOTE) () SUBLIS-VAR D1 (P 3 ARG I 1 FORM I 0 ALIST F 4 TEMP-TEMP) <Ad@cAgA@Ad@K IHhZH&J (71Q CONS-TERM 44Q SUBLIS-VAR) (21Q QUOTE) () SUBLIS-VAR-LST D1 (P 3 TERM I 1 TERMLST I 0 ALIST) !@Ad@K IHhZH&J(15Q SUBLIS-VAR) NIL () SUB-PAIR-EXPR D1 (P 0 X I 2 TERM I 1 NEWLST I 0 OLDLST F 1 TEMP-TEMP) (@dHc@AB gH (43Q SUBST-EXPR-ERROR1 27Q SUB-PAIR-EXPR1) (34Q QUOTE) () SUB-PAIR-EXPR-LST D1 (P 3 X I 2 LST I 1 NEWLST I 0 OLDLST) "@Bd@AK IHhZH&J(16Q SUB-PAIR-EXPR) NIL () SUB-PAIR-EXPR1 D1 (P 4 ARG I 2 TERM I 1 NEWLST I 0 OLDLST F 5 TEMP-TEMP) cA@"IHhUJBKc JiIHBBgB@Bd@AL JIh[I&K (140Q CONS-TERM 113Q SUB-PAIR-EXPR1) (67Q QUOTE) () SUB-PAIR-VAR D1 (P 4 ARG I 2 TERM I 1 NEWLST I 0 OLDLST F 5 TEMP-TEMP) cB2A@"IHhUJBKc JiIHBgB@Bd@AL JIh[I&K (140Q CONS-TERM 113Q SUB-PAIR-VAR) (67Q QUOTE) () SUB-PAIR-VAR-LST D1 (P 3 X I 2 LST I 1 NEWLST I 0 OLDLST) "@Bd@AK IHhZH&J(16Q SUB-PAIR-VAR) NIL () SUBSETP D1 (P 1 ELE I 1 Y I 0 X) @HiYA hHX(17Q MEMBER) NIL () SUBST-EXPR D1 (I 2 FORM I 1 OLD I 0 NEW) A @AB gA @AB (33Q SUBST-EXPR1 24Q SUBST-EXPR-ERROR1 11Q SUBST-VAR) (16Q QUOTE) () SUBST-EXPR-ERROR1 D1 (I 0 OLD) og@hg (20Q ERROR1) (15Q HARD 6 OLD) ( 3 (PROGN ATTEMPT TO SUBSTITUTE FOR THE EXPLICIT CONSTANT (!PPR OLD NIL) %. THE SUBSTITUTION FUNCTIONS WERE OPTIMIZED TO DISALLOW THIS %.)) SUBST-EXPR-LST D1 (P 3 X I 2 LST I 1 OLD I 0 NEW) "@Bd@AK IHhZH&J(16Q SUBST-EXPR) NIL () SUBST-EXPR1 D1 (P 3 ARG I 2 FORM I 1 OLD I 0 NEW) ;AB@BBgB@Bd@AK IHhZH&J (70Q CONS-TERM 43Q SUBST-EXPR1) (17Q QUOTE) () SUBST-FN D1 (P 3 ARG I 2 TERM I 1 OLD I 0 NEW) cBBgAB)@0Bd@AK IHhZH&JB0Bd@AK IHhZH&J(114Q SUBST-FN 44Q SUBST-FN) (11Q QUOTE) () SUBST-VAR D1 (P 3 ARG I 2 FORM I 1 OLD I 0 NEW) ;BddA2@gBB@Bd@AK IHhZH&J (70Q CONS-TERM 43Q SUBST-VAR) (16Q QUOTE) () SUBST-VAR-LST D1 (P 3 TERM I 2 TERMLST I 1 OLD I 0 NEW) "@Bd@AK IHhZH&J(16Q SUBST-VAR) NIL () SUBSTITUTE D1 (I 2 FORM I 1 OLD I 0 NEW) A@AB @AB (17Q SUBST-EXPR 10Q SUBST-VAR) NIL () SUBSUMES D1 (P 0 UNIFY-SUBST I 1 CL2 I 0 CL1) @ (6 SUBSUMES1) NIL () SUBSUMES-REWRITE-RULE D1 (P 1 UNIFY-SUBST P 0 CL2 I 1 REWRITE-RULE2 I 0 REWRITE-RULE1) %A@A @ (42Q SUBSUMES1 27Q ONE-WAY-UNIFY1) (35Q REWRITE-RULE 22Q REWRITE-RULE 14Q REWRITE-RULE 3 REWRITE-RULE) () SUBSUMES1 D1 (P 1 LIT I 0 CL1 F 2 CL2 F 3 UNIFY-SUBST) @RHhY@S IiHX(23Q SUBSUMES11) NIL () SUBSUMES11 D1 (I 2 UNIFY-SUBST I 1 CL1 I 0 LIT) A@ A (14Q SUBSUMES1 5 ONE-WAY-UNIFY1) NIL () SUM-STATS-ALIST D1 (L (0 ALIST)) #0jXdY@dZHظJIعHIhNIL NIL () TABULATE D1 (I 1 FILE I 0 N) @A A (11Q ISPACES 4 IPOSITION) NIL () TERM-ORDER D1 (P 3 NUMBER-OF-VARIABLES2 P 2 NUMBER-OF-VARIABLES1 P 1 FORM-COUNT2 P 0 FORM-COUNT1 I 1 TERM2 I 0 TERM1 F 4 NUMBER-OF-VARIABLES) .@@ XTZA YT[dJiJKhIHHI@A (53Q LEXORDER 15Q FORM-COUNT 6 FORM-COUNT) NIL () TERMINATION-MACHINE D1 (P 3 ARGLIST I 2 TESTS I 1 TERM I 0 FNNAME) A Adghga0@A #d`dBdKIHhZH&J@ABAh @ABA h 0@A #d`dBdKIHhZH&J(173Q ALL-ARGLISTS 162Q \NCONC2 157Q \NCONC2 154Q TERMINATION-MACHINE 151Q \APPEND2 144Q NEGATE-LIT 127Q TERMINATION-MACHINE 124Q \APPEND2 36Q ALL-ARGLISTS) (205Q TESTS-AND-CASETYPE# 50Q TESTS-AND-CASETYPE# 21Q IF 11Q QUOTE) () TP-EXPLODEN1 D1 (P 3 N I 0 SYM F 4 #/- F 5 #/0 F 6 #/Z F 7 #/9 F 10Q #/A) W0@ JdKdTj/UKKWK"WKKVKl ٰog@hg IHhZH&J(102Q ERROR1 6 OUR-EXPLODEN) (77Q SOFT 70Q X) ( 65Q (PROGN QUOTED LITERAL ATOMS MUST BE IN LOWER CASE AND (!PPR X NIL) IS NOT %.)) TP-GETCHARN1 D1 (P 0 A I 1 N I 0 SYM F 1 #/- F 2 #/0 F 3 #/Z F 4 #/9 F 5 #/A) :@A HdQjRHHTHUHHSHl og@hg (67Q ERROR1 4 OUR-GETCHARN) (64Q HARD 55Q X) ( 52Q (PROGN QUOTED LITERAL ATOMS MUST BE IN LOWER CASE AND (!PPR X NIL) IS NOT %.)) TP-IMPLODE1 D1 (P 3 N I 0 L F 4 #/- F 5 #/0 F 6 #/Z F 7 #/9 F 10Q #/A) r@@dd[k TjUKk Kk WKk 2WKk Kk VKk l ذog@ hg IHhZH&J (157Q OUR-IMPLODE 132Q ERROR1 121Q OUR-IMPLODE 101Q OUR-GETCHARN 71Q OUR-GETCHARN 61Q OUR-GETCHARN 50Q OUR-GETCHARN 37Q OUR-GETCHARN 30Q OUR-GETCHARN 14Q OUR-GETCHARN) (127Q HARD 115Q X) ( 112Q (PROGN QUOTED LITERAL ATOMS MUST BE IN LOWER CASE AND (!PPR X NIL) IS NOT %.)) TO-BE-IGNOREDP D1 (L (0 POLY) F 4 LITS-TO-BE-IGNORED-BY-LINEAR) /@@X@YTZh[dH I KiJ(43Q MEMB 36Q MEMB) (15Q POLY 6 POLY) () TOO-MANY-IFS D1 (P 4 ARG P 1 LHS P 0 RHS I 1 VAL I 0 ARGS F 5 TEMP-TEMP) f @jJ"KXjYHjH @Kh hKL ԻJZ\ c jUd K[ULA IYHLi(127Q OCCUR-CNT 113Q \FZEROP 76Q COUNT-IFS 62Q COUNT-IFS 47Q \FZEROP) NIL () TOP-FNNAME D1 (I 0 CONCL F 0 TEMP-TEMP) I@ddgddddgdddbh@cdg (106Q FN-SYMB0) (75Q QUOTE 34Q EQUAL 10Q NOT) () TOTAL-FUNCTIONP D1 (P 0 TEMP I 0 FNNAME F 1 TEMP-TEMP F 2 TEMPORARILY-DISABLED-LEMMAS F 3 DISABLED-LEMMAS) 2@gXd kjHh@cR QShh(44Q MEMB 14Q LENGTH) (27Q JUSTIFICATION 6 JUSTIFICATIONS) () TRANSITIVE-CLOSURE D1 (P 7 TAIL P 2 RESULT P 1 NEW P 0 ALIVE I 1 PRED I 0 SET) 00@diLKh]K&MXd YI H1KtLiHN_h[dOdOOdh4OdIh(IlAZJiOhOJIhIJiOOIYdMNh]\K[yN&](43Q COPYLIST) NIL () TRANSLATE D1 (I 0 X F 3 TRUE F 4 FALSE F 5 IN-BOOT-STRAP-FLG F 6 BOOT-STRAP-MACRO-FNS) @W@d3 g@hl1@diSgT@do og@hg @og@hg og@hg @ og@hg @dlog@hg log@hg @ @dgRSgRTQShgRTQh RTQ RWS Q VdHH hh(132Q SET 106Q DEPEND 103Q UNIONQ 100Q UNIONQ 75Q ALL-FNNAMES 72Q TRANSLATE 66Q EXTRACT-DEPENDENCIES-FROM-HINTS 56Q ADD-LEMMA0 47Q MAKE-EVENT 7 PROVE 4 APPLY-HINTS) (34Q PROVE-LEMMA 21Q PROVE-LEMMA) () PROVE-LEMMA D1 (P 6 MAIN-EVENT-NAME P 5 PROVE-ANS P 4 IN-PROVE-LEMMA-FLG P 3 HINTS P 2 TERM P 1 TYPES P 0 NAME I 0 $FEXPR$ F 7 IN-REDO-UNDONE-EVENTS-FLG) Q@@b@b@b@biWgHIJKhhighid  HIJ K o (116Q PROVE-LEMMAA0001 107Q CHK-ACCEPTABLE-HINTS 103Q CHK-ACCEPTABLE-LEMMA 70Q REDO-UNDONE-EVENTS) (61Q C 41Q PROVE-LEMMA) ( 113Q (PROVE-LEMMAA0001)) PROVE-LEMMA& D1 (I 0 NAME) g@dg (14Q APPLY) (7 PROVE-LEMMA 2 PROVE-LEMMA) () REFLECT D1 (P 6 LOOP-ANS P 5 TEMP P 3 MAIN-EVENT-NAME P 2 RELATION-MEASURE-LST P 1 SATISFACTION-LEMMA-NAME P 0 NAME I 0 $FEXPR$ F 7 IN-REDO-UNDONE-EVENTS-FLG F 10Q ALL-LEMMAS-USED) @@b@b@bWgHIJhhighid gHIJh HIJ HJgHIJhgHIh HIJ HdIWHg!L*N Hdg H H H]hM MM N L\(312Q UNIONQ 306Q UNIONQ 303Q ADD-TO-SET 264Q ALL-FNNAMES 234Q TOTAL-FUNCTIONP 230Q DEFN-WRAPUP 225Q TOTAL-FUNCTIONP 221Q PRINT-DEFN-MSG 206Q DEPEND 203Q REMOVE 200Q ADD-TO-SET 175Q UNION-EQUAL 147Q REFLECT0 141Q MAKE-EVENT 110Q CHK-ACCEPTABLE-REFLECT 102Q DEFN-SETUP 57Q REDO-UNDONE-EVENTS) (276Q JUSTIFICATION 270Q JUSTIFICATION 257Q JUSTIFICATION 245Q JUSTIFICATION 213Q SDEFN 160Q JUSTIFICATIONS 130Q REFLECT 116Q REFLECT 67Q REFLECT 50Q C 32Q REFLECT) () TOGGLE D1 (P 3 MAIN-EVENT-NAME P 2 FLG P 1 OLDNAME P 0 NAME I 0 $FEXPR$ F 4 IN-REDO-UNDONE-EVENTS-FLG) b@@b@b@bTgHIJhhighid HIJ HgHIJh hgIHJ HI h H(136Q DEPEND 131Q MAIN-EVENT-OF 124Q ADD-FACT 110Q MAKE-EVENT 71Q CHK-ACCEPTABLE-TOGGLE 56Q REDO-UNDONE-EVENTS) (114Q DISABLED-LEMMAS 75Q TOGGLE 47Q C 31Q TOGGLE) () GENERATE-ADD-FACT-PART D1 (P 3 !SINGLE-VARS! P 2 !ADDITIVE-VARS! P 1 !ADDITIVE-PROPS! P 0 !SINGLE-PROPS! I 0 ALIST F 11Q PROP) 6 @@ALiMX@ALMY@ALMZ@ALM[gggghggggggggggghdhggghhggghhghhggghggghghgghhhhggHgggghgggggggggggggghhggghhghhggghggghghgghhhhgggghhIggggggghhghhgggghggggggggggggggghhghhggghghgghhhiggghhhhJggghgggggggggggggggggggggggggghhhgghhhgggggghhhhKggghgggggggggggggggggggggggggghhhgghhhggghgggggggggW ghhggghghgghhhhggghhggggggggggggggW ggggghhggghghgghhhh_gOdg_NOh^]L\lO&^_gOdg_NOh^]L\KO&^_gOdg_NOh^]L\*O&^_gOdg_NOh^]L\ O&^(2040Q !PPR 1650Q !PPR) (2430Q VARIABLE 2414Q SINGLE 2350Q VARIABLE 2334Q ADDITIVE 2270Q PROPERTY 2254Q ADDITIVE 2210Q PROPERTY 2174Q SINGLE 2136Q HARD 2133Q QUOTE 2124Q PROP 2116Q PROP 2113Q QUOTE 2110Q BINDINGS 2057Q ! 2054Q DECLARED 2051Q NOT 2046Q WAS 2043Q THAT 2033Q NAMELY 2030Q NAME 2025Q VARIABLE 2022Q OR 2017Q PROPERTY 2014Q A 2011Q ON 2006Q CALLED 2003Q BEEN 2000Q HAS 1775Q ADD-SUB-FACT 1772Q PROGN 1767Q PQUOTE 1764Q ERROR1 1750Q VAL 1745Q PROP 1742Q SET 1721Q HARD 1716Q QUOTE 1707Q PROP 1701Q PROP 1676Q QUOTE 1673Q BINDINGS 1653Q %. 1643Q VARIABLE 1640Q SINGLE 1635Q EXISTING 1632Q SMASH 1627Q TO 1624Q ATTEMPT 1621Q PROGN 1616Q PQUOTE 1613Q ERROR1 1605Q PROP 1602Q BOUNDP 1577Q COND 1560Q HARD 1555Q QUOTE 1515Q %. 1512Q INFORMATION 1507Q UNDO 1504Q THE 1501Q CONFUSES 1476Q IT 1473Q BECAUSE 1470Q NON-NIL 1465Q IS 1462Q ATM 1457Q WHILE 1454Q NAME 1451Q VARIABLE 1446Q A 1443Q TO 1440Q SET 1435Q PROP 1432Q WITH 1427Q CALLED 1424Q BE 1421Q NOT 1416Q MUST 1413Q ADD-SUB-FACT 1410Q PROGN 1405Q PQUOTE 1402Q ERROR1 1374Q ATM 1371Q NULL 1366Q OR 1343Q PROP 1340Q EVALV 1335Q VAL 1332Q CONS 1327Q PROP 1324Q SET 1305Q HARD 1302Q QUOTE 1242Q %. 1237Q INFORMATION 1234Q UNDO 1231Q THE 1226Q CONFUSES 1223Q IT 1220Q BECAUSE 1215Q NON-NIL 1212Q IS 1207Q ATM 1204Q WHILE 1201Q NAME 1176Q VARIABLE 1173Q A 1170Q TO 1165Q SET 1162Q PROP 1157Q WITH 1154Q CALLED 1151Q BE 1146Q NOT 1143Q MUST 1140Q ADD-SUB-FACT 1135Q PROGN 1132Q PQUOTE 1127Q ERROR1 1121Q ATM 1116Q NULL 1113Q OR 1071Q VAL 1066Q ATM 1063Q PUTD1 1044Q HARD 1041Q QUOTE 1032Q ATM 1024Q ATM 1021Q QUOTE 1016Q BINDINGS 772Q %. 762Q ATM 757Q !PPR 754Q FUNCTION 751Q THE 746Q OF 743Q CELL 740Q DEFINITION 735Q LISP 732Q EXISTING 727Q SMASH 724Q TO 721Q ATTEMPT 716Q PROGN 713Q PQUOTE 710Q ERROR1 702Q ATM 677Q GETD 674Q COND 671Q DCELL 656Q PROP 643Q PROP 640Q ATM 635Q GETPROP 632Q VAL 627Q CONS 624Q ATM 621Q PUT1 604Q PROP 601Q VAL 576Q ATM 573Q PUT1 552Q HARD 547Q QUOTE 536Q ATM 530Q ATM 525Q QUOTE 522Q PROP 514Q PROP 511Q QUOTE 506Q BINDINGS 461Q %. 451Q ATM 446Q !PPR 443Q OF 433Q PROP 430Q !PPR 425Q UNDER 422Q HUNG 417Q FACT 414Q PROPERTY 411Q SINGLE 406Q EXISTING 403Q SMASH 400Q TO 375Q ATTEMPT 372Q PROGN 367Q PQUOTE 364Q ERROR1 355Q PROP 352Q ATM 347Q GETPROP 344Q COND 340Q PROP 335Q SELECTQ 314Q HARD 311Q QUOTE 300Q ATM 272Q ATM 267Q QUOTE 264Q PROP 256Q PROP 253Q QUOTE 250Q BINDINGS 223Q %. 213Q ATM 210Q !PPR 205Q AND 175Q PROP 172Q !PPR 167Q ON 156Q !PPR 153Q VALUE 150Q WITH 145Q ADD-FACT 142Q AN 137Q DO 134Q TO 131Q ATTEMPT 126Q PROGN 123Q PQUOTE 120Q ERROR1 112Q VAL 107Q NULL 104Q COND 101Q PROGN) () GENERATE-ADD-SUB-FACT1 D1 (P 1 X I 0 ALIST F 6 MATCH-TEMP F 7 TEMP-TEMP) oHig@c ;o Y@cdc VgVVgVhHXgVVgVVgV@J;io@1JFK @1JXK@ @ @ ho [gKo hJZdgL Mh\[JZM&\dgL Mh\[JZM&\(316Q MEMB 273Q SUB-PAIR 256Q GENERATE-ADD-FACT-PART 252Q GENERATE-UNDO-TUPLE-PART 246Q GENERATE-SUB-FACT-PART 230Q DREVERSE 36Q ERROR) (376Q VARIABLE 337Q PROPERTY 303Q HIDDEN 162Q VARIABLE 142Q HIDDEN 124Q CHRONOLOGY 101Q PROPERTY 63Q HIDDEN 20Q CHRONOLOGY) ( 313Q (IDATE SATELLITES MAIN-EVENT EVENT LOCAL-UNDO-TUPLES CHRONOLOGY) 270Q (COND (INIT (INIT-LIB (QUOTE !LIB-PROPS!) (QUOTE !LIBVARS!))) (TUPLE !SUBTRACT-FACT!) (T (COND ((OR (EQ MAIN-EVENT-NAME (QUOTE GROUND-ZERO)) (AND (OR (EQ MAIN-EVENT-NAME ATM) (AND ATM (EQ MAIN-EVENT-NAME (GETPROP ATM (QUOTE MAIN-EVENT))))) (NEQ PROP (QUOTE DCELL)))) NIL) (T (PUT1 MAIN-EVENT-NAME (CONS !UNDO-TUPLE! (GETPROP MAIN-EVENT-NAME (QUOTE LOCAL-UNDO-TUPLES))) (QUOTE LOCAL-UNDO-TUPLES)))) !ADD-FACT!)) 213Q (!LIB-PROPS! !LIBVARS! !SUBTRACT-FACT! !UNDO-TUPLE! !ADD-FACT!) 33Q (THE USER MUST DECLARE ALL THE BUILT-IN EVENT LEVEL PROPERTIES AND VARIABLES AS HIDDEN AND MUST NOT DECLARE ANY OTHER HIDDEN DATA.) 3 (IDATE SATELLITES MAIN-EVENT EVENT LOCAL-UNDO-TUPLES)) GENERATE-SUB-FACT-PART D1 (I 0 ALIST) Lgg@AHIhh go \dgLhJ KhZYHXK&Z(41Q SUBST 25Q \NCONC2) (52Q ADDITIVE 32Q !VAL-NAME! 5 PROP 2 SELECTQ) ( 36Q (LET (ATM PROP VAL-NAME VAL TEMP) (COND ((NLISTP TUPLE) (SETQ PROP TUPLE) (SET PROP NIL)) ((NLISTP (CDR TUPLE)) (SETQ PROP (CAR TUPLE)) (SETQ ATM (CDR TUPLE)) (COND ((EQ PROP (QUOTE DCELL)) (PUTD1 ATM NIL)) (T (PUTPROP ATM NIL PROP)))) (T (SETQ PROP (CAR TUPLE)) (SETQ ATM (CADR TUPLE)) (SETQ VAL-NAME (CDDR TUPLE)) (* In the following (and in the LET above) TEMP was introduced to skirt a bug in the Release 5.0 compiler. *) (SETQ TEMP (FOR VAL IN (COND ((NULL ATM) (EVALV PROP)) (T (GETPROP ATM PROP))) WHEN (EQUAL !VAL-NAME! VAL-NAME) DO (RETURN VAL))) (COND ((NULL TEMP) (ERROR1 (PQUOTE (PROGN IN UNDOING AN ADDITIVE ADD-FACT ON (!PPR ATM NIL) AND (!PPR PROP NIL) THE VALUE TO BE REMOVED WAS NOT FOUND %.)) (BINDINGS (QUOTE PROP) PROP (QUOTE ATM) ATM) (QUOTE WARNING)))) (COND ((NULL ATM) (SET PROP (REMOVE1 TEMP (EVALV PROP)))) (T (PUTPROP ATM (REMOVE1 TEMP (GETPROP ATM PROP)) PROP))))) NIL)) GENERATE-UNDO-TUPLE-PART D1 (P 7 X P 2 !SINGLE-VARS! P 1 !---ADDITIVE-LST---! P 0 !ADDITIVE! I 0 ALIST) 0oX@AKPLY@A OvOZggIJghgggghghhggghh _goOOhH M Nh]K[N&_gOdg_OOh__O_]O&_(174Q SUB-PAIR 132Q \APPEND2) (243Q VARIABLE 227Q SINGLE 145Q ADDITIVE 117Q ATM 114Q PROP 111Q CONS 77Q ATM 71Q DCELL 66Q QUOTE 63Q CONS 60Q DCELL 52Q PROP 45Q PROP 42Q SELECTQ) ( 154Q (!ADDITIVE-TYPE! !VAL-NAME!) 6 (!ADDITIVE-TYPE! (CONS PROP (CONS ATM !VAL-NAME!)))) !CLAUSE-SET D1 (P 0 *INDENT* I 1 INDENT I 0 CL-SET F 4 *INDENT* F 5 LAST-CLAUSE F 6 LAST-PRINEVAL-CHAR F 7 TRUE F 10Q *FILE*) QAT@c dW,@ #g0@d JIh[I&KjHjjHkkW hc (113Q PPRINDENT 47Q PRETTYIFY-CLAUSE 27Q PRETTYIFY-CLAUSE) (34Q AND) () !CLAUSE D1 (P 0 *INDENT* I 1 INDENT I 0 CL F 1 *INDENT* F 2 LAST-CLAUSE F 3 *FILE* F 4 LAST-PRINEVAL-CHAR) #AQ@cd jHjjHkkS hc(35Q PPRINDENT 15Q PRETTYIFY-CLAUSE) NIL () EQUALITY-HYP-NO D1 (L (1 CL 0 TERM)) AjH IdkjHhZjd_Pdgi_BgOPKOPO_O.W cO.O8 ogIggO:gO8gOgKgOBgO.  gO<gO>gOgOgO2gO$gHgO.gIkO.j>OxOzjhgO. gWgWgWgW~gOlhOW WWW_