COMMENT
*****************************************************************
[ADDEFS]  TRACK  9                                   [ 21.16 14 SEPT 1973]
CREATED   20.03   14 9 1973
;




FUNCTION ADDEFS X;
VARS CUCHAROUT U V;

DIN([/DEFS])->U;
DOUT([/DEFS])->CUCHAROUT;
APPLIST(X,LAMBDA X;
PRSTRING('DEFINE
(`);
PPRIND([% X, PROP("DEFN",X) %], 1 , 2);
PRSTRING(');
`);
END);
DOIO(U,CUCHAROUT);
END;
ADDEFS();


COMMENT
************************************************************
[/ INPUT]  TRACK  9                                   [ 21.16 14 SEPT 1973]
CREATED   20.03   14 9 1973
;


COMMENT 'THIS FILE CREATES THE FUNCTION "DEFINE" WHICH JUST PUTS
A FUNCTION DEFINITION ON THE PROPERTY LIST OF THE FUNCTION NAME.
THE FUNCTION "GETTHM" JUST LINKS TO OUR DISC TRACK TO FETCH
A THEOREM FROM THE STANDARD THEOREM FILE, GIVEN A THEOREM NAME.
(THIS IS NOT AN ESSENTIAL PART OF THE PROGRAM.)`;




VARS THMTRACK THMFILE;
36 -> THMTRACK;
[THEOREMS] -> THMFILE;

NIL -> ALLFNS;

FUNCTION DEFINE X;
[% "DEFN", HD(TL(X)) %] -> MEANING(HD(X));
IF MEMBER(HD(X),ALLFNS)
 THEN; ELSE HD(X) :: ALLFNS -> ALLFNS; CLOSE;
END;
FUNCTION NORMDEF X;
VARS PROVEFNS LEXPR FNNAME;
IF ISWORD(X)
 THEN X; PROP("DEFN",X);
 ELSE HD(X); HD(TL(X)); CLOSE;
-> LEXPR -> FNNAME;
NIL -> PROVEFNS;
NORMALATE(HD(TL(TL(LEXPR))))->X;
[% LOOPIF PROVEFNS /= NIL
  THEN IF HD(PROVEFNS) / = FNNAME AND
     PROP("DEFN",HD(PROVEFNS))=UNDEF
    THEN HD(PROVEFNS); CLOSE;
  TL(PROVEFNS) -> PROVEFNS;
  CLOSE %] -> PROVEFNS;
IF PROVEFNS /= NIL
 THEN NL(2); PR(FNNAME);NL(1);
 PRSTRING('UNDEFINED FUNCTIONS:  `);
 PR(PROVEFNS);
 NL(2);
 CLOSE;
DEFINE([% FNNAME, [% "LAMBDA", HD(TL(LEXPR)), X %] %]);
END;



FUNCTION GETTHM THMNAME;
VARS PROGLIST TRK;
DISCUSER->TRK;
DTRACK(THMTRACK);
IF HD(THMNAME) = "ALL"
 THEN [% COMPILE(DIN(THMFILE)) %]; DTRACK(TRK);
   -> TRK;
   IF TL(THMNAME) /= NIL
    THEN
    HD(TL(THMNAME)) -> THMNAME;
    LOOPIF NOT(EQUAL(THMNAME,HD(HD(TRK)))) THEN TL(TRK)->TRK;CLOSE;
    CLOSE;
   TRK;
     EXIT;
INCHARITEM(DIN(THMFILE)) -> LIST;
DTRACK(TRK);
FNTOLIST(LAMBDA;LOOP:LIST()->TRK;IF TRK="COMMENT"
   THEN LOOPIF LIST()/=";" THEN CLOSE; GOTO LOOP; CLOSE;
   TRK;END) -> PROGLIST;
LOOPIF NOT(NULL(PROGLIST))
 THEN
 IF EQUAL(THMNAME,LISTREAD()) THEN ERASE(ITEMREAD());LISTREAD();EXIT;
 LOOPIF ITEMREAD() /= ";" THEN CLOSE;
 CLOSE;
ERRFUN(THMNAME,57);
END;

FUNCTION ADDEFS;

DCOMP([ADDEFS]);
END;


COMMENT
************************************************************
[/ EVAL]  TRACK   9                                   [ 21.16 14 SEPT 1973]
CREATED   15.27    15  6 1973
;





VARS PROVEFNS APPLYNONPRIM BOMBOUT OTHERFAILS POCKETIT BOMBED EXPNDGFUN
     BINDVARS AUXANALY ANALYSIS;
NIL -> PROVEFNS;

COMMENT 'THIS IS THE BASIC EVAL ROUTINE. `;

FUNCTION EVAL TERM;
VARS Y X;

COMMENT 'IF TERM IS ATOM, RETURN IT OR VALUE, ACCORDING
TO WHICH ATOM.`;

IF ATOM(TERM)
 THEN
 IF TERM = NIL OR TERM = "T" OR ISNUMBER(TERM)
  THEN TERM;
 ELSEIF ASSOC(TERM,ALIST)
  THEN BACK();
  ELSE TERM; CLOSE;
 EXIT;

COMMENT 'GET FUNCTION SYMBOL`;

HD(TERM) -> X;

COMMENT 'CONSIDER THE POSSIBILITIES`;

IF X = "CAR"
 THEN
 POCKETIT -> X;
 0 -> POCKETIT;
 EVAL(HD(TL(TERM))) -> Y;
 X -> POCKETIT;
 IF Y = NIL
  THEN NIL;
 ELSEIF Y = "T"
  THEN NIL;
 ELSEIF ISNUMBER(Y)
  THEN NIL;
 ELSEIF ISNUMSKO(Y)
  THEN NIL;
 ELSEIF SHD(Y) = "CONS"
  THEN HD(TL(Y));
  ELSE BOMBOUT([% "CAR", Y %]);
  EXIT;
 STEPCNT + 1 -> STEPCNT;
 EXIT;

IF X = "CDR"
 THEN
 POCKETIT -> X;
 0 -> POCKETIT;
 EVAL(HD(TL(TERM))) -> Y;
 X -> POCKETIT;
 IF Y = NIL
  THEN NIL;
 ELSEIF Y = "T"
  THEN NIL;
 ELSEIF ISNUMBER(Y)
  THEN Y - 1;
 ELSEIF SHD(Y) = "CONS"
  THEN HD(TL(TL(Y)));
  ELSE BOMBOUT([% "CDR", Y %]);
  EXIT;
 STEPCNT + 1 -> STEPCNT;
 EXIT;

IF X = "CONS"
 THEN
 COMMENT '[% "CONS", EVAL(HD(TL(TERM))), EVAL(HD(TL(TL(TERM)))) %]`;
EVAL(HD(TL(TERM)))->X;
EVAL(HD(TL(TL(TERM))))->Y;
[% "CONS", X , Y %];

 EXIT;

IF X = "EQUAL"
 THEN
 EVAL(HD(TL(TERM))) -> X;
 EVAL(HD(TL(TL(TERM)))) -> Y;
 IDENT(Y,X) -> FOO1;
 IF FOO1 = NIL
  THEN NIL;
 ELSEIF FOO1
  THEN "T";
 ELSEIF ISCONS(Y) AND ISCONS(X) 
  THEN
  APPLY(ALIST,LAMBDA ALIST;
  CONSPAIR("X",X) :: (CONSPAIR("Y",Y) :: ALIST) -> ALIST;
EVAL([COND [EQUAL [CAR X] [CAR Y]] [EQUAL [CDR X] [CDR Y]] NIL]) ;
 END);RETURN;
  STEPCNT + 1 -> STEPCNT;
  GOTO CONDRULES;
  ELSE
  [% "EQUAL", X, Y %];
  EXIT;
 STEPCNT + 1 -> STEPCNT;
 EXIT;

IF X = "COND"
 THEN
CONDRULES:
 EVAL(HD(TL(TERM))) -> Y;
 IF Y = NIL OR Y = 0
  THEN
  EVAL(HD(TL(TL(TL(TERM)))));
 ELSEIF ISCONS(Y)
  THEN
  EVAL(HD(TL(TL(TERM))));
  ELSE
  COMMENT '[%"COND",Y,EVAL(HD(TL(TL(TERM)))),
EVAL(HD(TL(TL(TL(TERM)))))%]`;
EVAL(HD(TL(TL(TERM))))->X;
EVAL(HD(TL(TL(TL(TERM)))))->FOO1;
[% "COND", Y, X, FOO1 %];
EXIT;
STEPCNT+1->STEPCNT;
EXIT;

COMMENT 'X MUST BE NON-PRIMITIVE. CAREFULLY EVAL IT`;
APPLYNONPRIM();

END;


FUNCTION BOMBOUT TERM;
IF POCKETIT
 THEN
 TERM :: POCKET -> POCKET;
 ELSE TERM :: OTHERFAILS -> OTHERFAILS;
 CLOSE;
TERM;
END;

FUNCTION EVALARGS;
VARS POCKET POCKETIT;
NIL -> POCKET;
(HD(TERM) = EXPNDGFUN) -> POCKETIT;
MAPLIST(TL(TERM),EVAL);
IF POCKET /= NIL
 THEN
 POCKET :: BOMBLIST -> BOMBLIST;
 1 -> BOMBED;
 CLOSE;
END

FUNCTION EXPANDCALL EXPNDGFUN ALIST;
IF NOT(MEMBER(EXPNDGFUN,PROVEFNS))
 THEN EXPNDGFUN :: PROVEFNS -> PROVEFNS; CLOSE;
PROP("DEFN",EXPNDGFUN) -> FOO1;
IF FOO1 = UNDEF
 THEN
 EXPNDGFUN :: EVALDARGS;
 EXIT;
NIL -> BOMBLIST;
NIL -> OTHERFAILS;
BINDVARS(EVALDARGS,HD(TL(FOO1)),ALIST)->ALIST;
EVAL(HD(TL(TL(FOO1))));
END;

FUNCTION BINDVARS ARGLIST VARLIST ALIST;
LOOPIF ARGLIST /= NIL
 THEN
 CONSPAIR(HD(VARLIST),HD(ARGLIST)) :: ALIST -> ALIST;
 TL(ARGLIST) -> ARGLIST;
 TL(VARLIST) -> VARLIST;
 CLOSE;
ALIST;
END;

FUNCTION APPLYNONPRIM;
VARS EVALDARGS SAVEANALY SAVEBLIST SAVEOTHER SAVEPOCK;
EVALARGS() -> EVALDARGS;
IF BOMBED THEN HD(TERM) :: EVALDARGS; EXIT;
ANALYSIS -> SAVEANALY;
BOMBLIST -> SAVEBLIST;
OTHERFAILS -> SAVEOTHER;
POCKET->SAVEPOCK;
EXPANDCALL(HD(TERM),ALIST) ->FOO1;
IF BOMBED
 THEN
 HD(TERM) :: EVALDARGS;
SAVEPOCK->POCKET;
[% "***", HD(TERM), BOMBLIST, OTHERFAILS,HD(TERM), "***" %]
:: SAVEANALY -> ANALYSIS;
 ELSE
 FOO1;
 SAVEANALY -> ANALYSIS;
 STEPCNT + 1 -> STEPCNT;
 CLOSE;
0 -> BOMBED;
SAVEBLIST -> BOMBLIST;
SAVEOTHER -> OTHERFAILS;
END;



FUNCTION EVALUATE TERM;
VARS ALIST;
NIL->ALIST;
NIL -> BOMBLIST;
NIL -> ANALYSIS;
NIL -> OTHERFAILS;
UNDEF -> EXPNDGFUN;
0 -> POCKETIT;
0 -> BOMBED;
0 -> STEPCNT;
EVAL(TERM);
END;


COMMENT
************************************************************
[/ GEN]  TRACK   9                                   [ 21.16 14 SEPT 1973]
CREATED iff-flg   15.05     1  6 1973
;



COMMENT 'THIS FILE SUPPLIES MANY LIST PROCESSING FUNCTIONS THAT 
SHOULD BE STANDARD TO POP-2. IN ADDITION, SEVERAL FUNCTIONS
FOR RECOGNIZING CERTAIN CLASSES OF LISP EXPRESSIONS ARE PROVIDED.
THESE INCLUDE SKOLEM CONSTANTS, EXPRESSIONS COMPOSED ONLY OF
"CONS" AND "NIL" (CALLED REALLINKS IN THIS PROGRAM), EXPRESSIONS
THAT START WITH "CONS" AND EXPRESSIONS STARTING WITH ANY LISP
PRIMITIVE.`;

VARS ASSOCID MEMBERID XAPPFLAG VERBOSE FOO1 FOO2 FOO3 IDENT PROP 
     ASSOC MEMBER GENSYM;

FUNCTION GENMEM X L EQFN;
LOOPIF L /= NIL
 THEN IF EQFN(X,HD(L)) THEN 1; EXIT;
 TL(L) -> L;
 CLOSE;
0;
END;

GENMEM(% EQ %) -> MEMBER;

FUNCTION NCONC L1 L2;
IF L1 = NIL
 THEN L2;
 ELSE L1;
 LOOPIF (TL(L1) /= NIL) THEN TL(L1) -> L1; CLOSE;
 L2 -> TL(L1);
 CLOSE;
END;

FUNCTION DELETE X L;
VARS L0;
L->L0;
IF L = NIL THEN NIL;
ELSEIF HD(L) = X THEN TL(L);
 ELSE
LOOP:
 IF TL(L) = NIL THEN L0; EXIT;
 IF HD(TL(L)) = X THEN TL(TL(L)) -> TL(L); L0; EXIT;
 TL(L) -> L;
 GOTO LOOP;
 CLOSE;
END;

FUNCTION XAPPLIST L FN;
0 -> XAPPFLAG;
LOOPIF L /= NIL AND NOT(XAPPFLAG)
THEN
 FN(HD(L));
 TL(L) -> L;
 CLOSE;
END;

FUNCTION GENASSOC X L EQFN;
LOOPIF L /= NIL
 THEN
 IF EQFN(X,FRONT(HD(L))) THEN HD(L); 1; EXIT;
 TL(L) -> L;
 CLOSE;
0;
END;

GENASSOC(% EQ %) -> ASSOC;


FUNCTION SHD X ;
IF ATOM(X) THEN UNDEF;
 ELSE HD(X); CLOSE;
END;

MACRO SWAP;
MACRESULTS([;TERM1;TERM2->TERM1->TERM2;]);
END;




FUNCTION ISSTAR X;
CHARWORD(X,1) = 26;
END;



FUNCTION ISREALLINK TERM;
TOP:
IF ATOM(TERM)
 THEN
 IF TERM = NIL OR TERM = "T"
  THEN 1;
  ELSE ISINTEGER(TERM); CLOSE;
 ELSEIF HD(TERM) = "CONS"
  THEN IF ISREALLINK(HD(TL(TERM)))
   THEN HD(TL(TL(TERM))) -> TERM; GOTO TOP;
   ELSE 0; CLOSE;
  ELSE 0; CLOSE;
END;

FUNCTION ISNUMSKO X;
IF ATOM(X)
 THEN
 CHARWORD(X,1)->X;
 IF X > 40 THEN X < 47; ELSE 0; CLOSE;
 ELSE 0; CLOSE;
END;

FUNCTION ISCONS TERM;
IF ISNUMBER(TERM) OR TERM ="T"
 THEN 1;
 ELSE SHD(TERM) = "CONS" CLOSE;
END;


FUNCTION SUBST X Y Z;
VARS TEMP;
IF SUBST1(Z) THEN ELSE Z;CLOSE;
END;

FUNCTION SUBST1 Z;
IF IDENT(Y,Z)=1 THEN X; 1;
ELSEIF ATOM(Z) THEN 0;
ELSE SUBST;
LOOP1: IF Z=NIL THEN ELSE Z; TL(Z)->Z; GOTO LOOP1;CLOSE;
LOOP2: ->TEMP;
  IF TEMP=SUBST THEN 0; EXIT;
  TEMP->Z;
  IF SUBST1(HD(Z)) THEN CONS(TL(Z))->Z;GOTO LOOP3;
 ELSE GOTO LOOP2;
 CLOSE;

LOOP3:
  ->TEMP;
  IF TEMP=SUBST THEN Z;1;EXIT;
  CONS(HD(TEMP),Z)->Z;
  IF SUBST1(HD(Z)) THEN ->HD(Z); CLOSE;
  GOTO LOOP3;
CLOSE;
END;


FUNCTION APPSUB1 ALIST TERM;
VARS X;
IF ASSOCID(TERM,ALIST)
 THEN BACK(); 1;
ELSEIF ATOM(TERM)
 THEN TERM; 0;
ELSE
 APPSUB1(ALIST,HD(TERM)) -> X;
 IF LOGOR(APPSUB1(ALIST,TL(TERM)), X)
  THEN CONS(); 1;
  ELSE ERASE(); ERASE(); TERM; 0; CLOSE;
 CLOSE;
END;

FUNCTION APPSUBST;
ERASE(APPSUB1());
END;

FUNCTION INTSECTP L1 L2 TESTFN;
LOOPIF L1 /= NIL
 THEN
 IF GENMEM(HD(L1),L2,TESTFN) THEN 1; EXIT;
 TL(L1)->L1;
 CLOSE;
0;
END;

FUNCTION UNION L1 L2 TESTFN;
LOOPIF L1 /= NIL
 THEN
 IF GENMEM(HD(L1),L2,TESTFN)
  THEN;
  ELSE HD(L1)::L2->L2;CLOSE;
 TL(L1)->L1;
 CLOSE;
L2;
END;


FUNCTION CONSCNT L;
IF ATOM(L)
 THEN 0;
 ELSE 1+CONSCNT(HD(L))+CONSCNT(TL(L)); CLOSE;
END;

FUNCTION PRSEQUEN STR LIST PRFN;
IF VERBOSE
 THEN
 POPTTON();
 NL(4);
 PRSTRING(STR);
LOOP:
 PRFN(HD(LIST));
 TL(LIST) -> LIST;
 IF LIST = NIL THEN PRSTRING('.`);NL(2);EXIT;
 IF TL(LIST) = NIL
  THEN PRSTRING(' AND `);
  ELSE PRSTRING(', ' );
  CLOSE;
 GOTO LOOP;
 CLOSE;
END;


FUNCTION LISPPRIM TERM;
IF ATOM(TERM)
 THEN IF TERM = NIL OR TERM = "T" THEN 1; ELSE ISNUMBER(TERM);CLOSE;
 ELSE
 HD(TERM) -> TERM;
 IF TERM = "CAR" OR TERM = "CDR" OR TERM = "CONS" OR
    TERM = "EQUAL" OR TERM = "COND"
   THEN 1;
   ELSE 0; CLOSE;
  CLOSE;
END;


MACRO PPRDEF;
PPR(PROP("DEFN",ITEMREAD()));
END;


COMMENT
************************************************************
[/ TYPE]  TRACK   9                                  [ 21.17 14 SEPT 1973] 
CREATED   24.13    31  5 1973
;




COMMENT 'THIS FILE CONTAINS THE FUNCTIONS WHICH DECIDE IF AN EXPRESSION
IS BOOLEAN, NUMERIC, OR OF SOME OTHER TYPE, THE FUNCTION "TYPEEXPR"
ACTUALLY WRITES LISP FUNCTIONS.`;


VARS EVALUATE NORMALIZE REDUCE CONSFN ATOMFN PROPNAME NUMERIC BOOLEAN;



COMMENT 'THIS IS A GENERAL FUNCTION FOR DECIDING IF AN EXPRESSION IS
BOOLEAN OR NUMERIC. THESE ARE SUCH COMMON TYPES IT WAS DECIDED TO
CHECK FOR THEM EXPLICITLY. IT IS JUST A SPECIALIZATION OF THE GENERAL
TYPE FUNCTION. ESSENTIALLY IT JUST CHECKS THAT EVERY POSSIBLE OUTPUT
FROM THE EXPRESSION SATISFIES THE APPROPRIATE PROPERTY.`;
FUNCTION GENTYPR1 TERM;
VARS FUNSYM;
IF ATOM(TERM) THEN ATOMFN(TERM); EXIT;
HD(TERM) -> FUNSYM;
IF FUNSYM = "CONS" THEN CONSFN(TERM);
ELSEIF FUNSYM = "CAR" OR FUNSYM = "CDR" THEN 0;
ELSEIF FUNSYM = "EQUAL" THEN 1;
ELSEIF FUNSYM = "COND"
 THEN
 IF GENTYPR1(HD(TL(TL(TERM))))
 THEN GENTYPR1(HD(TL(TL(TL(TERM)))));
 ELSE 0; CLOSE;
ELSE
PROP(PROPNAME,FUNSYM) -> FOO1;
IF FOO1 /= UNDEF THEN FOO1; EXIT;
PROP("DEFN",FUNSYM) -> FOO1;
IF FOO1 = UNDEF THEN 0 -> PROP(PROPNAME,FUNSYM); 0; EXIT;
1 -> PROP(PROPNAME,FUNSYM);
IF GENTYPR1(HD(TL(TL(FOO1))))
 THEN 1 ;
 ELSE 0 -> PROP(PROPNAME,FUNSYM); 0; CLOSE;
CLOSE;
END;

FUNCTION GENTYPER TERM ATOMFN CONSFN PROPNAME;
GENTYPR1(TERM);
END;

GENTYPER(% LAMBDA TERM; IF TERM = NIL OR TERM = 0 OR TERM = 1 OR TERM = "T"
            THEN 1; ELSE 0; CLOSE; END,
           LAMBDA TERM; IDENT(TERM,1) = 1 ; END,
	   "BOOLEAN" %) -> BOOLEAN;

GENTYPER(% LAMBDA TERM; IF ISNUMBER(TERM) OR ISNUMSKO(TERM) OR TERM = "T"
            THEN 1; ELSE TERM = NIL; CLOSE; END,
           LAMBDA TERM; IF IDENT(HD(TL(TERM)),NIL) = 1
            THEN NUMERIC(HD(TL(TL(TERM)))); ELSE 0; CLOSE;END,
           "NUMERIC" %) -> NUMERIC;



COMMENT 'THE FUNCTIONS "BOOLEAN" AND "NUMERIC" (ABOVE) ARE JUST INSTANCES
OF THE MORE GENERAL GENTYPER.`;

COMMENT 'THE FUNCTION NORMALATE JUST EVALS, NORMALIZES AND REDUCES AN
EXPRESSION TO DEATH.`;
FUNCTION NORMALATE TERM;
VARS L;
LOOP:
TERM -> L;
REDUCE(NORMALIZE(EVALUATE(TERM))) -> TERM;
IF EQUAL(TERM,L) THEN L; EXIT;
GOTO LOOP;
END;


COMMENT 'THIS IS THE WORKHORSE OF THE FUNCTION WHICH WRITES NEW FUNCTIONS.
FOR EVERY OUTPUT OF AN EXPRESSION, TYPEEXP1, PRODUCES A PIECE OF
CODE WHICH RECOGNIZES THAT OUTPUT.  THE VARIABLE "X" IS USED
TO REPRESENT THE STRUCTURE BEING INSPECTED.  IT WILL BECOME THE
LOCAL VARIABLE OF THE RECURSIVE FUNCTION PRODUCED.  NOTE THAT WHEN
THE FUNCTION ENCOUNTERS A NON-PRIM FUNCTION WHICH HAS NOT YET
BEEN TYPED IT GIVES THE NEW FUNCTION A TYPE FUNCTION (ON THE PROPERTY
LIST) AND THEN WRITES THE DEFINITION OF THAT FUNCTION.  THUS, RECURSIVE
CALLS OF THE FUNCTION BEING TYPED ARE IDENTIFIED AS ALREADY HAVING A
TYPE FUNCTION -- NAMELY, THE ONE BEING WRITTEN.  NOTE THAT AFTER
THE FUNCTION BODY HAS BEEN WRITTEN NORMALATE IS USED TO OPTIMIZE THE CODE.`;
FUNCTION TYPEEXP1 TERM;
VARS TYPENAME TYPEDEFN FUNSYM PROVEFNS DEFN;
IF ATOM(TERM)
 THEN
 IF ISNUMBER(TERM) OR TERM = NIL OR TERM = "T"
  THEN [% "EQUAL", "X", TERM %];
  ELSE "T"; CLOSE;
 EXIT;
HD(TERM) -> FUNSYM;
IF FUNSYM = "CAR" OR FUNSYM = "CDR"
 THEN "T";
ELSEIF FUNSYM = "CONS"
 THEN
 IF NUMERIC(TERM)
 THEN [% "EQUAL", "X", TERM %];
 ELSE [% "COND", "X", [% "COND", SUBST([CAR X],"X",
  TYPEEXP1(HD(TL(TERM)))),SUBST([CDR X],"X",
  TYPEEXP1(HD(TL(TL(TERM))))), NIL %], NIL %]; CLOSE;
ELSEIF FUNSYM = "EQUAL"
 THEN [COND X [EQUAL X T] T];
ELSEIF FUNSYM = "COND"
 THEN
 [% "COND", TYPEEXP1(HD(TL(TL(TL(TERM))))), "T",
           TYPEEXP1(HD(TL(TL(TERM)))) %];
ELSEIF BOOLEAN(TERM)
 THEN [BOOLEAN X];
ELSEIF NUMERIC(TERM)
 THEN [NUMBERP X];
ELSE
PROP("TYPEFN",FUNSYM) -> TYPENAME;
IF TYPENAME /= UNDEF THEN TYPENAME :: [X]; EXIT;
PROP("DEFN",FUNSYM) -> DEFN;
IF DEFN = UNDEF
 THEN "CONSTTRUE" -> PROP("TYPEFN",FUNSYM); "T"; EXIT;
GENSYM(FUNSYM,"TYPE") -> TYPENAME;
TYPENAME -> PROP("TYPEFN",FUNSYM);
1 -> PROP("BOOLEAN",TYPENAME);
NORMALATE(SUBST(NIL,[%TYPENAME, "X"%],TYPEEXP1(HD(TL(TL(DEFN))))))
  -> TYPEDEFN;
IF IDENT(TYPEDEFN,"T") = 1 OR EQUAL(TYPEDEFN,[CONSTTRUE X])
 THEN
 "CONSTTRUE" -> PROP("TYPEFN",FUNSYM);
 "T";
 ELSE
 DEFINE(TYPENAME::("LAMBDA"::([X]::(TYPEDEFN::NIL))::NIL));
 TYPENAME::[X];
 CLOSE;
CLOSE;
END;


COMMENT 'THIS IS THE TOP-LEVEL FUNCTION FOR TYPING.  IT LETS TYPEEXP1
DO THE WORK AND FILTERS OUT THE CONSTANT TRUE FUNCTION`;
FUNCTION TYPEEXPR TERM;
TYPEEXP1(TERM) -> TERM;
TERM;
IF NOT(ATOM(TERM)) AND LISPPRIM(TERM)
 THEN
 NORMALATE();
 CLOSE;
-> TERM;
IF IDENT(TERM,"T") = 1
 THEN [CONSTTRUE X];
 ELSE TERM; CLOSE;
END;


COMMENT
************************************************************
[/ SORTDEFS]  TRACK   9                                   [ 21.17 14 SEPT 1973]
CREATED   15.36    8   5 1973
;



VARS OLDMARG2 OLDDEFINE OLDPPRSPCHAR;
COMPILE(LIBRARY([ALLSORT]));
DEFINE -> OLDDEFINE;
IDËNTFN -> DEFINE;
PPRSPCHAR - > OLDPPRSPCHAR;
MARG2 - > OLDMARG2;
79 -> MARG2; .
16 - > PPRSPCHAR;
DTRACK(36);
DOUT([/DEFS]) -> DDF2;
D̈DF2 - > CUCHAROUT;
APPLIST(ALLSORT([% COMPILE(DIN([/DEFS])) %],
                 LAMBDA X Y; ALFER(HD(X),HD(Y));END),
        LAMBDA X;
        NL(2);PRSTRING('DEFINE`;NL(1);PRSTRING('(`);
	PPRIND(X,1,2);PRSTRING(');`);
        END);
DDF2(TERMIN);
OLDMARG2 -> MARG2;
OLDPPRSPCHAR -> PPRSPCHAR;
CHAROUT -> CUCHAROUT;
OLDDEFINE -> DEFINE;


COMMENT
************************************************************
[/ GENSYM]  TRACK   9                                   [ 21.17 14 SEPT 1973]
CREATED   10.44     8  5 1973
;




COMMENT 'THIS FILE CREATES THE GENSYM FUNCTION.  THE FUNCTION IS USED
TO GENERATE NEW ATOMS FOR SKOLEM CONSTANTS AND FUNCTION
NAMES.  THE SECOND ARGUMENT IS USUALLY 0 MEANING GENERATE THE
NEXT ATOM STARTING WITH THE TOPWORD.  IF THE SECOND ARGUMENT IS
NOT A NUMBER, THE TWO WORDS ARE CONCATENATED TO FORM THE NEW
SYMBOL.`;

VARS GENALIST GLBGENALIST;

NIL -> GLBGENALIST;
NIL -> GENALIST;

FUNCTION NOCHARS X ;
VARS R;
X//10->X->R;
IF X THEN NOCHARS(X)->X;R;X+1;
ELSE R;1; CLOSE;
END;

FUNCTION GENSYM TOPWORD BTMWORD;
VARS CNT;
IF BTMWORD = 0
 THEN
 IF ASSOC(TOPWORD,GENALIST)
 THEN
 -> CNT;
 BACK(CNT) + 1 -> BTMWORD;
 BTMWORD -> BACK(CNT);
 ELSE
 CONSPAIR(TOPWORD,1) :: GENALIST -> GENALIST;
 1 -> BTMWORD;
 CLOSE;
 CLOSE;
IF ISNUMBER(BTMWORD)
 THEN
 CONSWORD(NOCHARS(BTMWORD)) -> BTMWORD;
 CLOSE;
IF DATALENGTH(TOPWORD) + DATALENGTH(BTMWORD) > 8
 THEN
 DESTWORD(TOPWORD) -> CNT;
 LOOPIF CNT > 4 THEN CNT-1->CNT;ERASE();CLOSE;
 DESTWORD(BTMWORD)+CNT -> CNT;
 LOOPIF CNT > 8 THEN CNT-1->CNT;ERASE();CLOSE;
 ELSE
 DESTWORD(TOPWORD)->CNT;
 DESTWORD(BTMWORD)+CNT->CNT;
 CLOSE;
CONSWORD(CNT);
END;

FUNCTION GLBGENSYM;
VARS GENALIST;
GLBGENALIST -> GENALIST;
GENSYM();
GENALIST->GLBGENALIST;
END;



GENSYM -> GENSKO;


COMMENT
************************************************************
[/ PROPS] TRACK   9                                   [ 21.18 14 SEPT 1973]
CREATED   9.33     8  5 1973
;



COMMENT 'THIS FILE IMPLEMENTS PROPERTY LISTS IN POP-2 USING MEANING`;

FUNCTION PROP PROPNAME WORD;
VARS X;
MEANING(WORD) -> X;
IF X = UNDEF THEN NIL -> X; X-> MEANING(WORD);CLOSE;
LOOPIF X /= NIL
 THEN IF HD(X) = PROPNAME THEN HD(TL(X)); EXIT;
 TL(TL(X))->X;
 CLOSE;
PROPNAME :: (UNDEF :: MEANING(WORD)) -> MEANING(WORD);
UNDEF;
END;

LAMBDA VAL PROPNAME WORD;
VARS X;
MEANING(WORD) -> X;
IF X = UNDEF THEN NIL->X;X->MEANING(WORD);CLOSE;
LOOPIF X /= NIL
 THEN
 IF HD(X) = PROPNAME THEN VAL -> HD(TL(X));EXIT;
 TL(TL(X))->X;
 CLOSE;
PROPNAME :: (VAL :: MEANING(WORD))->MEANING(WORD);
END;->UPDATER(PROP);


COMMENT
************************************************************
[PPR]  TRACK  9                                   [ 21.18 14 SEPT 1973]
CREATED   18.53   7  5 1973
;





COMMENT 'THIS IS THE WORLDS BEST PRETTY PRINT ROUTINE. IT PRINTS OUT
LISP EXPRESSIONS VERY NEATLY AND VERY FAST. DO NOT BOTHER TO GET
BOGGED DOWN IN IT UNLESS YOU WANT TO KNOW ALL THERE IS TO KNOW ABOUT
PRETTY PRINTING. SEE BOB BOYERS MEMO ON IT FROM DCL. FOR THE
THEOREM PROVERS PURPOSES IT IS SUFFICIENT TO KNOW THAT PPR
PRINTS A LISP EXPRESSION.`;


VARS NILCONS X TEMP1 PPRPACK PPRDL ENDLIST STARTLIS ADDLINES REMAINDE FLATSIZE
RPARCNT SPACELEF GRECCNT PPRMAX1 PPRMAXLNS MARG2 PPRSTRIP
PPRSPCHAR PPRSP STARTLIST NEXTIND NEXTNODE PPRATOM PPRJUMP PPRLINES
PPR PPRFLAG;
NIL :: NIL ->NILCONS;

30 -> PPRSPCHAR;
16->PPRMAXLNS;
60->MARG2;
INITC(80)->PPRSTRIP;






FUNCTION PPR1 FMLA RPARCNT;
VARS NODENAME DLHDFMLA RUNFLAT MINREM L RUNSTART RUNEND;
GRECCNT->NODENAME;
GRECCNT+1->GRECCNT;
IF ATOM(HD(FMLA)) THEN PPRDL(HD(FMLA))+1->DLHDFMLA;
ELSE 0->DLHDFMLA;
   FMLA->TL(NILCONS);
   NILCONS->FMLA;
CLOSE;
IF TL(FMLA)=NIL THEN RPARCNT+DLHDFMLA->FLATSIZE;
   SPACELEFT-FLATSIZE->REMAINDER;EXIT;
DLHDFMLA->RUNFLAT;
SPACELEFT-DLHDFMLA->MINREM;
SPACELEFT-1->SPACELEFT;
FMLA -> L;
LOOPFLAT:
TL(L)->L;
IF L=NIL THEN SPACELEFT+1->SPACELEFT;
   IF RUNFLAT =< SPACELEFT THEN
      RUNFLAT->FLATSIZE;
      SPACELEFT-RUNFLAT->REMAINDER;
   ELSE PPRPACK()::NIL->STARTLIST;
      STARTLIST->ENDLIST;
      FALSE->FLATSIZE;
   CLOSE;
EXIT;
IF ATOM(HD(L)) THEN
   PPRDL(HD(L))->TEMP1; TEMP1+1+RUNFLAT->RUNFLAT;
   SPACELEFT-TEMP1->TEMP1;
   IF TL(L)=NIL THEN RPARCNT+RUNFLAT->RUNFLAT;
      TEMP1-RPARCNT->TEMP1;
    CLOSE;
    IF TEMP1<MINREM THEN TEMP1->MINREM;CLOSE;
    GOTO LOOPFLAT;
ELSE PPR1(HD(L),IF TL(L)=NIL THEN RPARCNT+1;ELSE 1;CLOSE);
IF REMAINDER<MINREM THEN REMAINDER->MINREM; CLOSE;
   IF FLATSIZE THEN FLATSIZE+1+RUNFLAT->RUNFLAT;
      GOTO LOOPFLAT;
   CLOSE;
CLOSE;
STARTLIST->RUNSTART;
ENDLIST->RUNEND;
LOOPIND:
TL(L)->L;
IF L=NIL THEN
   PPRPACK()::RUNSTART->STARTLIST;
   RUNEND->ENDLIST;
   FALSE->FLATSIZE;
   SPACELEFT+1->SPACELEFT;
EXIT;
IF ATOM(HD(L)) THEN SPACELEFT-PPRDL(HD(L))->TEMP1;
   IF TL(L)=NIL THEN TEMP1-RPARCNT->TEMP1;CLOSE;
   IF TEMP1<MINREM THEN TEMP1->MINREM;CLOSE;
   GOTO LOOPIND;
CLOSE;
PPR1(HD(L), IF TL(L)=NIL THEN RPARCNT+1;ELSE 1;CLOSE);
IF REMAINDER<MINREM THEN REMAINDER->MINREM;CLOSE;
IF FLATSIZE THEN
ELSE STARTLIST->TL(RUNEND);ENDLIST->RUNEND;
CLOSE;
GOTO LOOPIND;
END;





FUNCTION PPRPACK;
LOGOR(LOGSHIFT(IF MINREM<DLHDFMLA THEN MINREM+1;0->REMAINDER;
         ADDLINES(LENGTH(FMLA)-1);
      ELSE 17+DLHDFMLA; MINREM-DLHDFMLA->REMAINDER;
         ADDLINES(LENGTH(FMLA)-2);
      CLOSE,13),NODENAME)
END;






FUNCTION PPR2 FMLA MARG1;
VARS NONLFLAG INDFLAG PROGFLAG;
IF ATOM(FMLA) THEN PPRATOM(FMLA); EXIT;
IF HD(FMLA) ="PROG" THEN MARG1; ELSE NIL;CLOSE->PROGFLAG;
IF GRECCNT=NEXTNODE THEN
   LOGAND(NEXTIND,15)+MARG1->MARG1;
   1->INDFLAG;
   LOGAND(NEXTIND,16)->NONLFLAG;
   TL(STARTLIST)->STARTLIST;
   IF NIL = STARTLIST THEN
   ELSE LOGAND(HD(STARTLIST),2:1111111111111)->NEXTNODE;
       LOGSHIFT(HD(STARTLIST),-13)->NEXTIND;
   CLOSE;
ELSE 0->INDFLAG;1->NONLFLAG;
CLOSE;
GRECCNT+1->GRECCNT;
CUCHAROUT(59);
IF ATOM(HD(FMLA)) THEN
   PPRATOM(HD(FMLA));
   TL(FMLA)->FMLA;
   IF FMLA=NIL THEN CUCHAROUT(61);EXIT;
   IF NONLFLAG THEN CUCHAROUT(16);
   ELSE CUCHAROUT(17);PPRSP(MARG1);1->SUBSCRC(MARG1+1,PPRSTRIP);
   CLOSE;
CLOSE;
LOOP:
IF NONLFLAG THEN ELSEIF TL(FMLA)=NIL THEN 0->SUBSCRC(MARG1+1,PPRSTRIP);CLOSE;
PPR2(HD(FMLA),MARG1);
TL(FMLA)->FMLA;
IF FMLA=NIL THEN CUCHAROUT(61);
EXIT;
IF INDFLAG THEN CUCHAROUT(17);
    PPRSP(IF PROGFLAG/=NIL AND ATOM(HD(FMLA)) THEN PROGFLAG;
       ELSE MARG1; CLOSE;);
ELSE CUCHAROUT(16);CLOSE;
GOTO LOOP;
END;





FUNCTION ADDLINES CNT;
CNT+PPRLINES->PPRLINES;
IF PPRLINES>PPRMAX1 THEN PPRJUMP();CLOSE;
END;






FUNCTION PPRIND FMLA MARG1 RPARCNT;
VARS X;
IF ATOM(FMLA)THEN PR(FMLA);EXIT;
IF HD(FMLA)="COND" THEN PPRMAXLNS ELSE 1000000;CLOSE
->PPRMAX1;
JUMPOUT(LAMBDA;PRSTRING('(TOO BIG)`);END,0)->PPRJUMP;
0->PPRLINES;
0->GRECCNT;
MARG2-MARG1->SPACELEFT;
PPR1(FMLA,RPARCNT+1);
IF FLATSIZE THEN PR(FMLA);EXIT;
FORALL X 1 1 80; 0->SUBSCRC(X,PPRSTRIP);CLOSE;
LOGAND(HD(STARTLIST),2:1111111111111)->NEXTNODE;
LOGSHIFT(HD(STARTLIST),-13)->NEXTIND;
0->GRECCNT;
PPR2(FMLA,MARG1);
END;





PPRIND(% 0, 0 %)->PPR;






FUNCTION PPRDL L;
VARS CNT CUCHAROUT;
IF ISNUMBER(L) THEN -1->CNT; 
LAMBDA X;CNT+1->CNT;END->CUCHAROUT;
PR(L);
CNT;
ELSE DATALENGTH(L);CLOSE;
END;






FUNCTION PPRATOM L ;
VARS CUCHAROUT OCUCHAROUT;
IF ISNUMBER(L) THEN
   CUCHAROUT->OCUCHAROUT;
   LAMBDA X; IF X=16 THEN ELSE OCUCHAROUT(X);CLOSE;END
   ->CUCHAROUT;
ELSEIF DATAWORD(L)="CSTRIP" THEN PRSTRING(L);
EXIT;
PR(L);
END;






FUNCTION PPRSP N;
0->PPRFLAG;
FORALL X 1 1 N;
IF SUBSCRC(X,PPRSTRIP) AND NOT(PPRFLAG) THEN
   CUCHAROUT(PPRSPCHAR);1->PPRFLAG;
ELSE CUCHAROUT(16);0->PPRFLAG;
CLOSE;
CLOSE;
END;


COMMENT
************************************************************
[/ IDENT]  TRACK   9                                   [ 21.18 14 SEPT 1973] 
CREATED   19.47    17  4 1973
;




COMMENT '"IDENT" IS A FAIRLY IMPORTANT FUNCTION.  IT MERELY RECOGNIZES
WHEN TWO TERMS ARE IDENTICAL (AND THEREFORE EQUAL), WHEN THEY
CANNOT POSSIBLY BE EQUAL (E.G., A CONS VERSUS A NIL), OR OF
UNKNOWN RELATIONSHIP SYNTACTICALLY.  IT RETURNS 1 IF THEY ARE
IDENTICAL (IT KNOWS ABOUT INTEGERS BEING CONSES, ETC), 0 IF
THEY ARE OF UNKNOWN RELATIONSHIP, AND NIL IF THEY ARE DEFINATELY [sic]
UNEQUAL.`;

VARS MEMBERID ASSOCID;

FUNCTION OCCUR CONST TERM;
IF IDENT(CONST,TERM)=1 THEN 1;EXIT;
IF ATOM(TERM) THEN 0; EXIT;

LOOPIF (TL(TERM)->TERM; TERM /= NIL)
 THEN
 IF OCCUR(CONST,HD(TERM)) THEN 1; EXIT;
 CLOSE;
0;
END;

FUNCTION OCCURCONS TERM1 TERM2;
IF SHD(TERM2) /= "CONS"
 THEN IDENT(TERM1,TERM2) = 1
ELSEIF OCCURCONS(TERM1,HD(TL(TERM2)))
 THEN 1;
 ELSE OCCURCONS(TERM1,HD(TL(TL(TERM2)))); CLOSE;
END;



FUNCTION IDENT TERM1 TERM2;
VARS FUNSYM;
TOP:
IF TERM1 = TERM2 THEN 1; EXIT;
IF ATOM(TERM1)
 THEN
 IF TERM1 = NIL THEN 0 -> TERM1;
 ELSEIF TERM1 = "T" THEN 1 -> TERM1; CLOSE;
 IF ATOM(TERM2 )
 THEN
 IF TERM2 = NIL THEN 0 -> TERM2;
 ELSEIF TERM2 = "T" THEN 1 -> TERM2; CLOSE;
 IF EQ(TERM1,TERM2) THEN 1;
 ELSEIF ISNUMBER(TERM1)
  THEN IF ISNUMBER(TERM2)
   THEN NIL;
   ELSE 0; CLOSE;
  ELSE 0; CLOSE;
ELSEIF (L1: HD(TERM2) = "CONS")
 THEN
  IF TERM1
   THEN
   IF ISNUMBER(TERM1)
    THEN
    IDENT(0,HD(TL(TERM2))) -> FOO1;
    IF EQ(FOO1,1)
     THEN
          TERM1 - 1 -> TERM1;
     HD(TL(TL(TERM2))) -> TERM2;
     GOTO TOP;
     ELSE FOO1; CLOSE;
    ELSEIF OCCURCONS(TERM1,TERM2) THEN NIL; ELSE 0; CLOSE;
   ELSE NIL; CLOSE;
  ELSE 0; CLOSE;
 ELSEIF ATOM(TERM2)
  THEN
  IF TERM2 = NIL THEN 0 -> TERM2;
  ELSEIF TERM2 = "T" THEN 1 -> TERM2; CLOSE;
  SWAP;
  GOTO L1;
 ELSEIF HD(TERM1) = HD(TERM2)
 THEN
 HD(TERM1) -> FUNSYM;
 1;
 LOOPIF (TL(TERM1) -> TERM1; TERM1 /= NIL)
  THEN
  TL(TERM2) -> TERM2;
  IDENT(HD(TERM1),HD(TERM2)) -> FOO1;
  IF FOO1 /= 1
  THEN
  IF FUNSYM = "CONS"
   THEN
   IF FOO1 = NIL THEN ERASE(); NIL; EXIT;
   LOGAND(FOO1);
   ELSE ERASE(); 0; EXIT;
  CLOSE;
  CLOSE;
ELSEIF HD(TERM2) = "CONS" OR HD(TERM1) = "CONS" AND (SWAP;1;)
 THEN
 IF OCCURCONS(TERM1,TERM2)
  THEN NIL;
  ELSE 0; CLOSE;
ELSE 0; CLOSE;
END;


COMMENT 'THIS IS JUST AN EQUALITY LIKE OPERATION WHICH IS TRUE IF ITS
TWO ARGUMENTS ARE IDENT AND FALSE OTHERWISE.`;
OPERATION 7 ==;
IDENT() = 1;
END;




GENASSOC(% NONOP == %) -> ASSOCID;
GENMEM(% NONOP == %) -> MEMBERID;


COMMENT
************************************************************
[/]  TRACK  22                                  [ 21.19 14 SEPT 1973]
CREATED   20.05   14 9 1973
;

[9 22 36]->DTRS;
VARS SLASH9 SLASH22;

[[/PROPS][PPR][/GEN][/GENSYM][/INPUT][/TYPE][/IDENT][/EVAL]] -> SLASH9;

[[/REWRITE][/REDUCE][/FERTILIZE][/GENRLIZE][/IND1][/IND2][/PROVE]] -> SLASH22;

UTRACK(9);
APPLIST(SLASH9,DCOMP);

DTRACK(22);
APPLIST(SLASH22,DCOMP);

DTRACK(36); DCOMP([/DEFS]);
APPLIST(ALLFNS,NORMDEF);
DTRACK(22);


COMMENT
************************************************************
[/ REWRITE]  TRACK  22                                  [ 21.19 14 SEPT 1973] 
CREATED   10.19    1  8 1973
;




COMMENT 'THIS IS THE NORMALIZE FUNCTION.  IN-LINE COMMENTS EXPLAIN
THE REWRITE RULES APPLIED.`;

VARS REWRITEFN;

IDENTFN -> REWRITEFN;


FUNCTION REWRITE TERM;
VARS TERM1 TERM2 TERM3;

COMMENT 'IF TERM IS AN EQUALITY`;

IF HD(TERM)="EQUAL" THEN
HD(TL(TERM))->TERM1;
HD(TL(TL(TERM)))->TERM2;

COMMENT '(EQUAL KNOWN1 KNOWN2) => T OR NIL`;
IDENT(TERM1,TERM2) -> TERM3;
IF TERM3 = NIL THEN NIL; EXIT;
IF TERM3 THEN "T";EXIT;

COMMENT '(EQUAL BOOL T) => BOOL`;
IF TERM1==1 AND BOOLEAN(TERM2)THEN TERM2 EXIT;
IF TERM2==1 AND BOOLEAN(TERM1) THEN TERM1 EXIT;

COMMENT '(EQUAL (EQUAL A B) C) =>
               (COND (EQUAL A B) (EQUAL C T) (COND C NIL T))`;
IF SHD(TERM1) = "EQUAL" OR SHD(TERM2) = "EQUAL" AND (SWAP;1)
 THEN
 [% "COND", TERM1,
            REWRITE([% "EQUAL", TERM2, "T" %]),
            REWRITE([% "COND", TERM2, NIL, "T" %]) %] -> TERM;
 GOTO COND;
 CLOSE;

COMMENT '(EQUAL X NIL) => (COND X NIL T)`;
IF TERM1 == NIL OR TERM2 == NIL AND (SWAP;1)
 THEN
 [% "COND", TERM2, NIL, "T" %] -> TERM;
 GOTO COND;
 CLOSE;

COMMENT 'GO SEE IF ONE ARG IS A COND`;
GOTO CONDARG;

COMMENT 'TERM IS A COND`;

ELSEIF HD(TERM)="COND" THEN
COND:
TL(TERM)->TERM3;
HD(TERM3)->TERM1;
TL(TERM3)->TERM3;
HD(TERM3)->TERM2;
HD(TL(TERM3))->TERM3;

COMMENT'(COND KNOWN X Y) => X OR Y`;
IF TERM1 == NIL THEN TERM3; EXIT;
IF ISCONS(TERM1) THEN TERM2; EXIT;

COMMENT '(COND X Y Y) => Y`;
IF TERM2 == TERM3 THEN TERM2; EXIT;

COMMENT '(COND X X NIL) => X`;
IF TERM1 == TERM2 AND TERM3 == NIL THEN TERM1; EXIT;

COMMENT '(COND BOOL T NIL ) => BOOL`;
IF BOOLEAN(TERM1) AND TERM2 == "T" AND TERM3 == NIL
 THEN TERM1; EXIT;

COMMENT '(COND X T (COND Y NIL T)) => (COND Y (COND X T NIL) T)`;
IF TERM2=="T" AND SHD(TERM3)="COND" AND
  HD(TL(TL(TERM3))) == NIL AND HD(TL(TL(TL(TERM3)))) == "T"
  THEN
  IF BOOLEAN(TERM1)
   THEN TERM1;
   ELSE [% "COND", TERM1, "T", NIL %] CLOSE;
 -> TERM2;
  HD(TL(TERM3)) -> TERM1;
  "T" -> TERM3;
  [% "COND", TERM1, TERM2, TERM3 %] -> TERM;
 CLOSE;


COMMENT '(COND (COND A T2 T3) B C) => (COND A (COND T2 B C)
         (COND T3 B C)) WHERE T2 OR T3 ISNIL`;

IF SHD(TERM1) = "COND" AND
   HD(TL(TL(TERM1))) == NIL OR HD(TL(TL(TL(TERM1)))) == NIL
 THEN
 GOTO CONDCOND;
 CLOSE;

COMMENT '(COND (COND A B C) D E)=> (COND A (COND B C [sic] E) (COND C D E))
     WHERE D AND E ARE NOT NIL OR D AND E ARE T AND NIL`;

IF SHD(TERM1) = "COND"
 THEN
 IF TERM2 == NIL AND NOT(TERM3 == "T") THEN GOTO SKIP;
 ELSEIF TERM3 == NIL AND NOT(TERM2 =="T") THEN GOTO SKIP; CLOSE;
CONDCOND:
   IF ISSTAR(SHD(TERM2)) OR ISSTAR(SHD(TERM3)) THEN GOTO SKIP; CLOSE;
   REWRITE([%"COND", HD(TL(TL(TERM1))), TERM2,TERM3 %]);
   REWRITE([%"COND", HD(TL(TL(TL(TERM1)))),TERM2,TERM3%]);
   ->TERM3->TERM2;
   [%"COND",HD(TL(TERM1)),TERM2,TERM3%]->TERM;
   GOTO COND;
    SKIP:
CLOSE;

COMMENT 'TERM IS A NON-COND, NON-EQ FUNCTION CALL`;
ELSE

COMMENT '(FOO X (COND A B C) Y) =>
(COND A (FOO X B Y) (FOO X C Y))`;

 CONDARG:
TL(TERM) -> TERM1;
 LOOPIF TERM1 /= NIL AND SHD(HD(TERM1)) /= "COND"
  THEN
  TL(TERM1) -> TERM1;
  CLOSE;
 IF TERM1 /= NIL
  THEN
  HD(TERM1) -> TERM1;
  [% "COND", HD(TL(TERM1)) , REWRITE(SUBST(HD(TL(TL(TERM1))),TERM1,
   TERM)), REWRITE(SUBST(HD(TL(TL(TL(TERM1)))),TERM1,TERM)) %]
  -> TERM;
  GOTO COND;
  CLOSE;
CLOSE;
REWRITEFN();
TERM
END

FUNCTION NORMALIZE TERM;
IF ATOM(TERM)THEN TERM EXIT;
REWRITE(HD(TERM)::MAPLIST(TL(TERM),NORMALIZE));
END


COMMENT
************************************************************
[/ PROVE]  TRACK  22                                  [ 21.2 14 SEPT 1973] 
CREATED   10.53   27  7 1973
;




COMMENT 'THIS FILE CONTAINS THE TOP-LEVEL THEOREM PROVER, "PROVE".
"PROVE" DOES ALL THE WORK.  MOST OF THE FUNCTIONS
BETWEEN HERE AND THERE ARE CONCERNED ONLY WITH OUTPUT.`;

VARS THM THMTIME STUCKTHM AVOIDSTAR VERBOSE LASTPPRTHM REPORTFN;
1 -> AVOIDSTAR;
0 -> VERBOSE;
NIL -> SPECPROF;


COMMENT 'THIS RECOGNIZES WHEN THE THEOREM HAS BEEN BEATEN TO DEATH.`;
FUNCTION FINISHED TERM;
VARS FUNSYM;
IF ATOM(TERM)
 THEN 1;
ELSEIF (HD(TERM)->FUNSYM; FUNSYM = "EQUAL")
 OR FUNSYM = "CAR" OR FUNSYM = "CDR" OR FUNSYM = "CONS"
 THEN
 LOOPIF (TL(TERM)->TERM; TERM /= NIL)
  THEN
  IF FINISHED(HD(TERM)) THEN; ELSE 0; EXIT;
  CLOSE;
 1;
ELSE 0; CLOSE;
END;


FUNCTION GENSKOLIST LIST;
MAPLIST(LIST,LAMBDA CONST;CONSPAIR(CONST,GENSKO(CONST,0));END);
END;

IDENTFN -> REPORTFN;

FUNCTION REPORT CODE CMT BRKCMT;
VARS X;
IF CODE = NIL THEN GOTO VERB; CLOSE;
IF CHAROUT /= CUCHAROUT OR NOT(VERBOSE)
 THEN
 CUCHAROUT; CHAROUT -> CUCHAROUT; PR(CODE); -> CUCHAROUT;
 CLOSE;
CODE :: PROFILE -> PROFILE;
REPORTFN();
VERB:
THM -> LASTREPTHM;
IF ISFUNC(CMT) THEN CMT(); GOTO CHKSPEC;CLOSE;
IF VERBOSE = 1 OR VERBOSE = 0.5 AND CODE /= "E" AND CODE /= "N"
 AND CODE /= "R"

 THEN
 POPTTON();NL(4);PRSTRING(CMT);NL(2);
 IF SUBSCRC(DATALENGTH(CMT),CMT)=10 THEN
  THM->LASTPPRTHM; PPR(THM); NL(2); CLOSE;
  CLOSE;
CHKSPEC:
 IF CODE = NIL THEN EXIT;
 IF SPECPROF /= NIL
  THEN
  IF EQUAL(CODE,HD(SPECPROF))
   THEN
   TL(SPECPROF) -> SPECPROF;
   IF HD(SPECPROF) = "^"
    THEN
    HD(TL(SPECPROF)) -> X;
    TL(TL(SPECPROF)) -> SPECPROF;
    CUCHAROUT; CHAROUT -> CUCHAROUT;
    POPTTON(); NL(4); PRSTRING('INTERRUPT;  `); PR(BRKCMT);NL(1);->CUCHAROUT;
    IF ISLINK(X)
     THEN POPVAL(X<>[; GOON]);
     ELSE APPLY(VALOF(X)); CLOSE;
    CUCHAROUT;CHAROUT->CUCHAROUT;NL(1);PRSTRING('RESUMED`);NL(4);->CUCHAROUT;
    CLOSE;
   ELSE
   CHAROUT->CUCHAROUT;POPTTON(); NL(1); PRSTRING('PROFILES DIVERGE`);NL(1);SETPOP();
  CLOSE;
 CLOSE;
END;

FUNCTION REPORTIF TESTTHM;
IF EQUAL(THM,TESTTHM) THEN ERASE();ERASE();ERASE(); EXIT;
REPORT();
END;





FUNCTION SETUP;
NIL -> PROFILE;
NIL -> FERTLIST;  
NIL -> GENRLLIST; 
NIL -> BOMBLIST;  
NIL -> PROVEFNS;  
NIL -> GENALIST;  
NIL -> INDVARLIST;
UNDEF -> ENDTHM;
POPTIME -> THMTIME;
IF NOT(ATOM(HD(THM)))
 THEN
 NL(2);
 PR(HD(THM));
 TL(THM) -> THM;
 CLOSE;
THM -> LASTREPTHM;
THM -> LASTPPRTHM;
IF VERBOSE
 THEN SP(5); PR(POPDATE()); CLOSE;
NL(1);
END;


FUNCTION FINREPORT;
POPTTON();
IF VERBOSE = 1
 THEN
 IF PROVEFNS /= NIL
  THEN
  NL(5);PRSTRING('FUNCTION DEFINITIONS:');NL(2);
  APPLIST(REV(PROVEFNS),
   LAMBDA FN;
   IF ISSTAR(FN) THEN EXIT;
   PPR([% FN, PROP("DEFN",FN) %]);
   IF PROP("PROGGEND",FN) = 1
    THEN NL(1);PRSTRING('(PROGRAM GENERATED)`);CLOSE;
    NL(2);
    END);
   CLOSE;
  IF FERTLIST /= NIL
   THEN
   NL(3);PRSTRTNG('FERTILIZERS:`);NL(2);
   APPLIST(REV(FERTLIST),
    LAMBDA X;
    PR(X);PRSTRING(' = `);PPRIND(PROP("AUXDEFN",X),5,0);NL(2);
    END);
   CLOSE;
  IF GENRLLIST /= NIL
   THEN
   NL(3); PRSTRING('GENERALIZATIONS:`);NL(2);
   APPLIST(REV(GENRLLIST),
    LAMBDA X;
    PR(BACK(X)); PRSTRING(' = `); PR(FRONT(X));NL(2);
    END);
   CLOSE;
   CLOSE;
 IF VERBOSE
 THEN
 NL(3);
 PRSTRING('PROFILE:  `);PR(REV(PROFILE));NL(2);
 CLOSE;
END;


FUNCTION WRAPUP;
THM -> ENDTHM;
(POPTIME - THMTIME) / 16 -> THMTIME;
IF NOT(VERBOSE) OR CHAROUT /= CUCHAROUT
 THEN
 CUCHAROUT; CHAROUT -> CUCHAROUT;
 NL(1); PPR(THM); NL(1); PR(THMTIME); NL(1);
 -> CUCHAROUT;
CLOSE;
IF VERBOSE
 THEN
 NL(4); PRSTRING('TIME: `);PR(THMTIME);PRSTRING(' SECS.`);
 NL(5);
 CLOSE;
END;

COMMENT 'THIS FUNCTION APPLIES FERTILIZATION AND IF THAT FAILS
TRIES GENERALIZING AND INDUCTING.  IT IS CAREFUL TO WORK ONLY
ON THE FIRST CONJUNCT IF THE THEOREM IS A CONJUNCT.  FOR THIS
IT GETS THE NAME "ARTIFICIAL INTELLIGENCE", BEING ABOUT THE
SMARTEST PROGRAM IN THE THEOREM PROVER.`;
FUNCTION ARTIFINTEL THM;
IF FERTILIZE(THM)
 THEN
 1;
 EXIT;
0 -> CONJFLAG;
IF HD(THM) = "COND"
 THEN
 IF HD(TL(TL(THM))) == NIL
  THEN
  [% "COND", [% "NOT", HD(TL(THM)) %], HD(TL(TL(TL(THM)))), NIL %] -> THM;
  1 -> CONJFLAG;
 ELSEIF HD(TL(TL(TL(THM)))) == NIL
  THEN
  1 -> CONJFLAG;
  CLOSE;
 CLOSE;
IF CONJFLAG
 THEN
 HD(TL(THM));     (REPORT("&",'(WORK ON FIRST CONJUNCT ONLY)`,"ARTIFINTEL"));
 ELSE
 THM;
 CLOSE;
-> INDTERM;
GENRLIZE(INDTERM) -> INDTERM;
IF INDUCT(INDTERM)
 THEN
 -> INDTERM;
 ELSE
 INDTERM;  0; EXIT;
IF CONJFLAG
 THEN
 [% "COND", INDTERM,
            APPSUBST(GENSKOLIST(INDVARS),HD(TL(TL(THM)))),
	    NIL %];
 ELSE
 INDTERM;
 CLOSE;
1;
END;



COMMENT 'THIS IS THE THEOREM PROVER.  ASTOUNDING IN ITS SIMPLICITY.
THE OUTPUT FUNCTIONS HAVE BEEN MOVED TO THE SIDE TO REVEAL THE
ESSENCE OF THE SYSTEM:  BEAT THE THEOREM TO DEATH WITH
EVALUATION, NORMALIZE AND REDUCE.  IF THAT FAILS, TRY A LITTLE
AI AND THEN MORE VIOLENCE.`;


FUNCTION PROVE1 THM;
SETUP();                 (REPORT(NIL,'THEOREM TO BE PROVED:`,"PROVE1"));
LOOP:                    (REPORT( "/",IDENTFN,"PROVE1"));
THM -> OLDTHM;
EVALUATE(THM) -> THM;    (REPORTIF("E",'EVALUATION YIELDS:`,"PROVE1",LASTREPTHM));
NORMALIZE(THM) -> THM;   (REPORTIF("N",'WHICH NORMALIZES TO:`,"PROVE1",LASTREPTHM));
REDUCE(THM) -> THM;     (REPORTIF("R",'AND REDUCES TO:`,"PROVE1",LASTREPTHM));
IF FINISHED(THM)
 THEN                         (REPORTIF(NIL,'WHICH IS EQUIVALENT TO:`,
                          "PROVE1",LASTPPRTHM));
                   (REPORT(".",FINREPORT,"PROVE1"));
  WRAPUP();
 EXIT;
IF EQUAL(THM,OLDTHM)
 THEN
                       (REPORTIF(NIL,'WHICH IS EQUIVALENT TO:`,
                              "PROVE1",LASTPPRTHM));
 IF ARTIFINTEL(THM)
  THEN
  -> THM;               (REPORT(",",'THE THEOREM TO BE PROVED IS NOW:`,
                             "PROVE1"));
  ELSE
  -> THM;
  THM -> STUCKTHM;        (REPORT("Q",'STUCK`,"PROVE1"));
  FINREPORT();WRAPUP();
  EXIT;
 CLOSE;
GOTO LOOP;
END;









COMMENT 'THE TOP-LEVEL.  MAINLY CONCERNED WITH I/O, LIKE
RECOGNIZING WHEN THE USER WANTS ALL THE THEOREMS IN THE STANDARD
FILE PROVED, OR WHEN HE HAS GIVEN YOU A THEOREM NAME RATHER THAN
A THEOREM.`;


FUNCTION PROVE THM;
VARS TOTTIME;
IF HD(THM) = "ALL"
 THEN
 0 -> TOTTIME;
 APPLIST(GETTHM(THM),
  LAMBDA THM;
 IF AVOIDSTAR AND MEMBER("*",HD(THM)) THEN EXIT;
 PROVE1(THM);TOTTIME+THMTIME->TOTTIME;END);
 POPTTON();
 NL(10);
 PRSTRING('TOTAL TIME: `);PR(TOTTIME);PRSTRING(' SECS.`);
 NL(5);
ELSEIF HD(THM) = "T"
 THEN
 PROVE1(THM::GETTHM(THM));
 ELSE PROVE1(THM); CLOSE; 
END;


FUNCTION LPPROVE LIST;
VARS LPLNFEEDS DDF2 PPRMAXLNS MARG2 THMNAME;

180 -> PPRMAXLNS;
79 -> MARG2;
POPMESS([LP80 THEOREMS PROVED]) -> DDF2;
IF HD(LIST) = "ALL" THEN GETTHM(LIST) -> LIST; CLOSE;
APPLIST(LIST,
 LAMBDA X;
 CHAROUT -> CUCHAROUT;
 0 -> LPLNFEEDS;
  NL(2);
 IF NOT(ATOM(HD(X))) THEN HD(X);ELSE NIL; CLOSE;
 -> THMNAME;
 IF AVOIDSTAR AND MEMBER("*",THMNAME) THEN EXIT;
 PR(THMNAME);
 NL(I );
 LAMBDA X;
 DDF2(X);
 IF X = 17
  THEN
  LPLNFEEDS+1->LPLNFEEDS;
  IF LPLNFEEDS = 60
   THEN
   2 -> LPLNFEEDS;
   SP(60);IF THMNAME/=NIL THEN PR(THMNAME);CLOSE;DDF2(17);DDF2(17);
   CLOSE;
  CLOSE;
 END -> CUCHAROUT;
 DDF2(64);
 IF VERBOSE = 0 THEN 0.5 -> VERBOSE; CLOSE;
 PROVE(X);
 END;);
CHAROUT -> CUCHAROUT; 
DDF2(TERMIN)
END;


COMMENT
************************************************************
[/ IND1]  TRACK  22                                  [ 21.2 14 SEPT 1973] 
CREATED   11.06   25  7 1973
;




VARS RIDCARCDR FAILURES BOMBBAY ARGLIST SCORE DESTCAND CONSCAND;

RECORDFNS("CANDREC",[0 0 0 0])
-> FAILURES
-> BOMBBAY
-> ARGLIST
-> SCORE
-> DESTCAND
-> CONSCAND;

FUNCTION CARCDRSKO TERM;
LOOPIF ISLINK(TERM)
 THEN
 IF HD(TERM) /= "CAR" AND HD(TERM) /= "CDR"
  THEN 0; EXIT;
 HD(TL(TERM)) -> TERM;
 CLOSE;
IF TERM = NIL OR TERM = 0 THEN 0; EXIT;
TERM;
1;
END;

FUNCTION COLLARGS BOMBLIST;
VARS ARGS BOMBS POCKET CONST;
NIL -> ARGS;
NIL -> BOMBS;
LOOPIF BOMBLIST /= NIL
 THEN
 HD(BOMBLIST) -> POCKET;
 TL(BOMBLIST) -> BOMBLIST;
 POCKET <> BOMBS -> BOMBS;
 LOOPIF POCKET /= NIL
  THEN
  IF CARCDRSKO(HD(POCKET))
   THEN
   -> CONST;
   IF NOT(MEMBER(CONST,ARGS))
    THEN CONST::ARGS->ARGS; CLOSE;
   ELSE 0; EXIT;
  TL(POCKET) -> POCKET;
  CLOSE;
 CLOSE;
BOMBS;
ARGS;
1;
END;

FUNCTION GETCANDS ANALYSIS;
VARS ARGS BOMBS CANDLIST;
NIL -> CANDLIST;
APPLIST(ANALYSIS,
 LAMBDA FAULTDESC;
 IF COLLARGS(HD(TL(TL(FAULTDESC))))
  THEN
  -> ARGS -> BOMBS;
  CONSCAND(1,ARGS,BOMBS,HD(TL(TL(TL(FAULTDESC)))))
   :: CANDLIST -> CANDLIST;
   CLOSE;
  END);
 CANDLIST;
END;

FUNCTION MERGECANDS CANDLIST;
VARS CAND1;
CANDLIST;
LOOPIF TL(CANDLIST) /= NIL
 THEN
 HD(CANDLIST) -> CAND1;
 TL(CANDLIST) -> CANDLIST;
 XAPPLIST(CANDLIST,
  LAMBDA CAND2;
  IF INTSECTP(ARGLIST(CAND1),ARGLIST(CAND2),NONOP =)
   THEN
   1 -> XAPPFLAG;
   0 -> SCORE(CAND1);
   UNION(ARGLIST(CAND1),ARGLIST(CAND2),NONOP =)->ARGLIST(CAND2);
   UNION(BOMBBAY(CAND1),BOMBBAY(CAND2),EQUAL) -> BOMBBAY(CAND2);
   UNION(FAILURES(CAND1),FAILURES(CAND2),EQUAL) -> FAILURES(CAND2);
   SCORE(CAND2)+1->SCORE(CAND2);
CLOSE;
  END);
CLOSE;
END;


FUNCTION CHOOSEHIGH CANDLIST;
VARS HIGH ANS;
-10000 -> HIGH;
LOOPIF CANDLIST /= NIL
 THEN
 IF SCORE(HD(CANDLIST)) > HIGH AND SCORE(HD(CANDLIST))
  THEN
  SCORE(HD(CANDLIST)) -> HIGH;
  HD(CANDLIST) :: NIL -> ANS;
 ELSEIF SCORE(HD(CANDLIST)) = HIGH
  THEN
  HD(CANDLIST) :: ANS -> ANS;
  CLOSE;
 TL(CANDLIST) -> CANDLIST;
 CLOSE;
ANS;
END;
[[CONS RAND1 RAND2] [CONS RAND3 RAND4] [CDNS RAND5 RAND6]
  [CONS RAND7 RAND8] [CONS RAND9 RAND10] [CONS RAND11 RAND12]]
   -> RANDCONS;

FUNCTION RATECANDS CANDLIST INDTERM;
VARS X;
APPLIST(CANDLIST,
 LAMBDA CAND;
 RANDCONS -> X;
 ERASE(EVALUATE(APPSUBST(MAPLIST(ARGLIST(CAND),
   LAMBDA TERM;
   CONSPAIR(TERM,HD(X),TL(X)->X);
   END), INDTERM)));
 STEPCNT -> SCORE(CAND);
 END);
CANDLIST;
END;

FUNCTION CHOOSENEW CANDLIST;
APPLIST(CANDLIST,
 LAMBDA CAND;
 1->SCORE(CAND);
 APPLIST(ARGLIST(CAND),
  LAMBDA TERM;
  IF NOT(MEMBER(TERM,INDVARLIST))
   THEN 1 + SCORE(CAND) -> SCORE(CAND);
   CLOSE;
  END);
END);
CHOOSEHIGH(CANDLIST);
END;



CONSPAIR("CAR","CARARG")::(CONSPAIR("CDR","CDRARG")::NIL)
 -> RIDCARCDR;

FUNCTION PICKINDVARS INDTERM;
VARS CANDLIST;
ERASE(EVALUATE(APPSUBST(RIDCARCDR,INDTERM)));
GETCANDS(ANALYSIS) -> CANDLIST;
IF CANDLIST = NIL THEN 0; EXIT;
MERGECANDS(CANDLIST) -> CANDLIST;
CHOOSEHIGH(CANDLIST) -> CANDLIST;
IF TL(CANDLIST) /= NIL
 THEN
 RATECANDS(CANDLIST,INDTERM) -> CANDLIST;
 CHOOSEHIGH(CANDLIST) -> CANDLIST;
 IF TL(CANDLIST) /= NIL
  THEN
  CHOOSENEW(CANDLIST) -> CANDLIST;
  CLOSE;
 CLOSE;
HD(CANDLIST);
1;
END;


COMMENT
************************************************************
[/ IND2]  TRACK  22                                  [ 21.21 14 SEPT 1973] 
CREATED   24.15   31  5 1973
;




VARS CARCONSTS CANDREC JUSTCARSUBST CARSUBST CARCDRINFO;

FUNCTION GENCARCONST L;
MAPLIST(L,LAMBDA CONST;CONSPAIR(CONST,
  IF ISNUMSKO(CONST) THEN NIL; ELSE GENSKO(CONST,0)CLOSE;);END);
END;

FUNCTION SETUPSUBST;
VARS X Y;
NIL -> CARCDRINFO;
NIL -> CARSUBST;
NIL -> JUSTCARSUBST;
APPLIST(BOMBBAY(CANDREC),
 LAMBDA TERM;
 HD(TERM) -> X;
 HD(TL(TERM)) -> TERM;
 IF ASSOC(TERM,CARCDRINFO)
  THEN
  -> Y;
  IF X /= BACK(Y)
   THEN "BOTH" -> BACK(Y); CLOSE;
  ELSE
  CONSPAIR(TERM,X) :: CARCDRINFO -> CARCDRINFO;
  CLOSE;
 END);
APPLIST(CARCDRINFO,
 LAMBDA X;
 IF BACK(X) /= "CDR"
  THEN
  CONSPAIR(FRONT(X),BACK(ERASE(ASSOC(FRONT(X),CARCONSTS)))) -> Y;
  IF BACK(X) = "CAR"
   THEN Y :: JUSTCARSUBST -> JUSTCARSUBST; CLOSE;
  Y :: CARSUBST -> CARSUBST;
  CLOSE;
 END);
END;

FUNCTION CONJOIN L;
IF TL(L) = NIL
THEN HD(L);
ELSE [% "AND", HD(L), CONJOIN(TL(L)) %]; CLOSE;
END;

FUNCTION NILCASE;
CONJOIN(MAPLIST(INDVARS,LAMBDA X;SUBST(NIL,X,INDTERM);END));
END;





FUNCTION INDHYP;
IF CARSUBST /= NIL
 THEN
 IF LENGTH(CARSUBST) = LENGTH(JUSTCARSUBST)
  THEN APPSUBST(CARSUBST,INDTERM);
  ELSE [% "AND", APPSUBST(CARSUBST,INDTERM),
                 APPSUBST(JUSTCARSUBST,INDTERM) %]; CLOSE;
 ELSE INDTERM; CLOSE;
END;

FUNCTION INDCONCL;
APPSUBST(MAPLIST(INDVARS,
 LAMBDA VAR;
 CONSPAIR(VAR,[% "CONS", BACK(ERASE(ASSOC(VAR,CARCONSTS))), VAR %]);
 END), INDTERM);
END;

FUNCTION SIMPLEIND;
VARS X;
BOMBBAY(CANDREC) -> X;
LOOPIF X /= NIL
 THEN
 IF ISLINK(HD(TL(HD(X)))) THEN 0; EXIT;
 TL(X) -> X;
 CLOSE;
FAILURES(CANDREC) -> X;
LOOPIF X /= NIL
 THEN
 IF ISLINK(HD(TL(HD(X))))
  THEN
  IF CARCDRSKO(HD(TL(HD(X)))) AND MEMBER((),INDVARS)
   THEN 0; EXIT;
   CLOSE;
  TL(X) -> X;
 CLOSE;
1;
END;

FUNCTION SPECIAL1;
VARS X;
IF TL(INDVARS) = NIL
 THEN
 IF GENMEM([% "CDR", CONST %],BOMBLIST,
           LAMBDA;NOT(EQUAL());END)
  THEN 0; EXIT;
 FAILURES(CANDREC) -> X;
 LOOPIF X /= NIL
  THEN
  IF ISLINK(HD(TL(HD(X)))) AND CARCDRSKO(HD(TL(HD(X)))) AND
     () = CONST AND HD(HD(TL(HD(X)))) = "CAR" OR
     ISLINK(HD(TL(HD(TL(HD(X))))))
     THEN 0; EXIT;
  TL(X) -> X;
  CLOSE;
 1;
 ELSE 0; CLOSE;
END;

FUNCTION SPECIAL2;
IF TL(INDVARS) = NIL
 THEN
 IF MEMBERID ( [%"CDR",[%"CDR",CONST%]%],BOMBLIST)
  OR MEMBERID([%"CAR",[%"CDR",CONST%]%],BOMBLIST)
  THEN 1; ELSE 0; CLOSE;
 ELSE 0; CLOSE;
END;

FUNCTION SPEC2HYP;
CONJOIN([%
 IF MEMBERID([%"CAR",CONST%],BOMBLIST)
  THEN SUBST(CARCON1,CONST,INDTERM); CLOSE,
 IF MEMBERID([%"CAR",[%"CDR",CONST%] %],BOMBLIST)
  THEN SUBST(CARCON2,CONST,INDTERM);CLOSE,
 IF MEMBERID([%"CDR",[%"CDR",CONST%]%],BOMBLIST)
  THEN INDTERM; CLOSE %]);
END;

FUNCTION SPECIALMODE;
VARS CARCON1 CARCON2 CONST BOMBLIST;
HD(INDVARS) -> CONST;
BOMBBAY(CANDREC) -> BOMBLIST;
BACK(ERASE(ASSOC(CONST,CARCONSTS))) -> CARCON1;
BACK(HD(GENCARCONST([% CONST %]))) -> CARCON2;
IF SPECIAL1()
 THEN
 (REPORT("S1",'(SPECIAL CASE REQUIRED)`,"SPECIALMODE"));
 [% "AND", NILCASE(),
     [% "AND", SUBST([%"CONS",CARCON1,NIL%],CONST,INDTERM),
          [% "IMPLIES", SUBST([%"CONS",CARCON2, CONST %],
                          CONST, INDTERM),
	      SUBST([%"CONS",CARCON1,[%"CONS",CARCON2,CONST%] %],
                CONST,INDTERM) %] %] %];

ELSEIF SPECIAL2()
 THEN
 (REPORT("S2",'(SPECIAL CASE REQUIRED)`,"SPECIALMODE"));
 [% "AND", NILCASE(),
   [% "AND", SUBST([% "CONS",CARCON1,NIL%],CONST,INDTERM),
      [% "IMPLIES", SPEC2HYP(),
        SUBST([%"CONS",CARCON1,[%"CONS",CARCON2,CONST%] %],
            CONST,INDTERM) %] %] %];

 ELSE
 ERRFUN('SPECIAL CASE NOT COVERED`,10000);
 SETPOP();
 CLOSE;
END;

FUNCTION INDREPORT;
IF VERBOSE
 THEN
 POPTTON();
 PRSEQUEN('INDUCT ON `,INDVARS,PR);NL(2);
 CLOSE;
END;

FUNCTION INDUCT INDTERM;
(REPORT(NIL,'MUST TRY INDUCTION.`,"INDUCT"));
IF NOT(PICKINDVARS(INDTERM)) THEN 0; EXIT;
-> CANDREC;
ARGLIST(CANDREC) -> INDVARS;
INDVARS <> INDVARLIST -> INDVARLIST;
GENCARCONST(INDVARS) -> CARCONSTS;
IF SIMPLEIND()
 THEN
 SETUPSUBST();
 [% "AND", NILCASE(), [% "IMPLIES", INDHYP(), INDCONCL() %] %];
 ELSE SPECIALMODE(); CLOSE;
-> INDFORM;
(REPORT(INDVARS,INDREPORT,"INDUCT"));
INDFORM;
1;
END;


COMMENT
************************************************************
[/ VERB]  TRACK  22                                  [ 21.21 14 SEPT 1973]
CREATED   17.16    9  5 1973
;


FUNCTION REPORTF1;
IF ISLINK(CODE) THEN NL(2);PPR(INDTERM);NL(2);CLOSE;
END;

OPERATION 1 TALK; 1 -> VERBOSE; END;

OPERATION 1 QUIET; 0 -> VERBOSE; IDENTFN -> REPORTFN; END;

OPERATION 1 WHISPER; 0 -> VERBOSE; REPORTF1 -> REPORTFN; END;

REPORTFN -> OLDREPFN;


COMMENT
************************************************************
[/ FERTILIZ]  TRACK  22                                  [ 21.21 14 SEPT 1973]
CREATED   19.49   17  4 1973
;



COMMENT 'THIS IS THE FERTILIZATION! FUNCTION.  AGAIN, IN-LINE COMMENTS
EXPLAIN ITS BEHAVIOUR.`;

VARS FERTCODE FERTL1ST;

FUNCTION FERTREPORT;
IF VERBOSE
 THEN
 POPTTON();
 NL(4);PRSTRING('FERTILIZE WITH `);PPRIND(TERM1,15,1);
 PRSTRING('.`);NL(2);
 CLOSE;
END;

FUNCTION FERTILIZE TERM;
VARS TERM1 TERM2 TERM3 LHS1 LHS2 RHS1 RHS2 X;
IF SHD(TERM) /= "COND" THEN 0; EXIT;
HD(TL(TERM)) -> TERM1;
HD(TL(TL(TERM))) -> TERM2;
HD(TL(TL(TL(TERM)))) -> TERM3;

COMMENT 'FERTILIZE ONLY TERMS OF FORM (COND (EQUAL A B) C T)`;

IF SHD(TERM1) = "EQUAL" AND NOT(TERM3 == NIL) AND BOOLEAN(TERM2)
   AND BOOLEAN(TERM3)
 THEN
 HD(TL(TERM1)) -> LHS1;
 HD(TL(TL(TERM1))) -> RHS1;
 IF ISREALLINK(LHS1) OR ISREALLINK(RHS1)
  THEN GOTO NOFERT; CLOSE;

COMMENT '(COND (EQ A B) (EQ C D) 1) => (COND (EQ C D)X 1 FU)
 WHERE (EQ C D)X HAS BEEN CROSS FERTILIZED FROM (EQ A B)`;

IF SHD(TERM2) = "EQUAL"
 THEN
 HD(TL(TERM2)) -> LHS2;
 HD(TL(TL(TERM2))) -> RHS2;
 IF OCCUR(RHS1,RHS2)
    THEN
 IF OCCUR(LHS1,LHS2)
  THEN
  IF CONSCNT(RHS1) < CONSCNT(LHS1)
   THEN
   SUBST(RHS1,LHS1,LHS2) -> LHS2;
   ELSE
   SUBST(LHS1,RHS1,RHS2) -> RHS2;
   CLOSE;
  ELSE
  SUBST(LHS1,RHS1,RHS2) -> RHS2;
  CLOSE;
 ELSE
 IF OCCUR(LHS1,LHS2)
  THEN SUBST(RHS1,LHS1,LHS2) -> LHS2;
 ELSE GOTO NOXFERT; CLOSE;
 CLOSE;
  [% "EQUAL", LHS2, RHS2 %] -> TERM2;
 "X" -> FERTCODE;


COMMENT '(COND (EQ A B) (NON-EQ) 1) => (COND (NON-EQ)A/B 1 FU)`;

 ELSEIF (NOXFERT: "F" -> FERTCODE; OCCUR(LHS1,TERM2))
  THEN
  IF OCCUR(RHS1,TERM2)
   THEN
   IF CONSCNT(RHS1) < CONSCNT(LHS1)
    THEN SUBST(RHS1,LHS1,TERM2) -> TERM2;
    ELSE SUBST(LHS1,RHS1,TERM2) -> TERM2; CLOSE;
  ELSE SUBST(RHS1,LHS1,TERM2) -> TERM2; CLOSE;
  ELSE
 IF OCCUR(RHS1,TERM2)
  THEN SUBST(LHS1,RHS1,TERM2) -> TERM2;
  ELSE GOTO NOFERT; CLOSE;
  CLOSE;
 GENSYM("*",0) -> X;
 [% "COND", TERM1, NIL, TERM3 %] -> PROP("AUXDEFN",X);
 1 -> PROP("BOOLEAN",X);
 X :: FERTLIST -> FERTLIST;
 [% "COND", TERM2, "T", [% X %] %] -> TERM2;
      (REPORT(FERTCODE,FERTREPORT,"FERTILIZE"));
IF TERM3 == 1
  THEN TERM2;
  ELSE [% "COND", TERM2, [% "COND", TERM3, "T", TERM1%], NIL %]; CLOSE;
 1;
 EXIT;


COMMENT 'IF NO FERTILIZATION WAS POSSIBLE, RECURSE INTO
COMPONENTS FOR FIRST POSSIBLE ONE`;

NOFERT:
1 -> TERM3;
[% "COND", APPLIST(TL(TERM),
  LAMBDA TERM;
  IF TERM3 AND FERTILIZE(TERM) THEN 0 -> TERM3; ELSE TERM; CLOSE;
  END), (IF TERM3 THEN ERASE(ERASE(),ERASE(),ERASE(),ERASE()); 0; EXIT)%];
1;

END;


COMMENT
************************************************************
[/ REDUCE]  TRACK  22                                  [ 21.22 14 SEPT 1973]
CREATED   19.48   17  4 1973
;



COMMENT 'THIS IS THE REDUCE FUNCTION.  IN-LINE COMMENTS EXPLAIN
THE REWRITE RULES APPLIED.`;


VARS REDUCE;


FUNCTION REDUCE1 TERM CONSLIST;
VARS TERM1 TERM2 TERM3;
RECURSE:
COMMENT 'IF TERM IS ATOM OR NON-COND, QUIT`;
IF ATOM(TERM) OR HD(TERM) /= "COND"
 THEN
 TERM;
 EXIT;

COMMENT 'GET COMPONENTS OF THE COND`;
HD(TL(TERM)) -> TERM1;
HD(TL(TL(TERM))) -> TERM2;
HD(TL(TL(TL(TERM)))) -> TERM3;

COMMENT 'IF TERM1 IS NIL OR CONS, EVAL IT`;
IF TERM1 == NIL
 THEN
 TERM3 -> TERM;
 GOTO RECURSE;
ELSEIF ISCONS(TERM1) OR MEMBERID(TERM1,CONSLIST)
 THEN
 TERM2 -> TERM;
 GOTO RECURSE;
 CLOSE;

COMMENT '(COND ATOM A B) => (COND ATOM R(A(ATOM/CONS)) R(B(ATOM/NIL)))`;
IF ATOM(TERM1)
 THEN
 GOTO SUBSTCONS;
 CLOSE;

COMMENT '(COND (EQUAL A KNOWNLINK) B C) => (COND (EQUAL A KNOWNLINK)
  R(B(A/KNOWNLINK))
  R(C((EQUAL A KNOWNLINK)/NIL)))`;
IF HD(TERM1) = "EQUAL"
 THEN
 IF ISREALLINK(HD(TL(TERM1)))
  THEN SUBST(HD(TL(TERM1)),HD(TL(TL(TERM1))),TERM2) -> TERM2;
 ELSEIF ISREALLINK(HD(TL(TL(TERM1))))
  THEN SUBST(HD(TL(TL(TERM1))),HD(TL(TERM1)),TERM2) -> TERM2;
  ELSE GOTO SUBSTTRUE; CLOSE;
 GOTO ASSEMBOOL;
 CLOSE;

COMMENT '(COND (COND ...) A B) => (COND R(COND) R(A) R(B))`;
IF HD(TERM1) = "COND"
 THEN
 REDUCE1(TERM1,CONSLIST) -> TERM1;
 REDUCE1(TERM2,CONSLIST) -> TERM2;
 REDUCE1(TERM3,CONSLIST) -> TERM3;
 IF TERM3 == NIL THEN GOTO CONTINUE; CLOSE;
 [% "COND", TERM1, TERM2, TERM3 %];
 EXIT;

CONTINUE:

COMMENT '(COND BOOL A B) => (COND BOOL R(A(BOOL/T)) R(B(BOOL/NIL)))`;
IF BOOLEAN(TERM1)
 THEN
SUBSTTRUE:
 SUBST("T",TERM1,TERM2) -> TERM2;
ASSEMBOOL:
 [% "COND", TERM1,
            REDUCE1(TERM2,CONSLIST),
            REDUCE1(SUBST("NIL",TERM1,TERM3),CONSLIST) %];
 EXIT;	   

COMMENT '(COND RANDOM A B) => (COND RANDOM R(A(RANDOM/CONS))
                                      R(B(RANDOM/NIL)))`;
SUBSTCONS:
[% "COND", TERM1, REDUCE1(TERM2,TERM1 :: CONSLIST),
                  REDUCE1(SUBST(NIL,TERM1,TERM3),CONSLIST) %];
		  
END;

REDUCE1(% NIL %) -> REDUCE;


COMMENT
************************************************************
[/ GENRLIZE]  TRACK  22                                  [ 21.22 14 SEPT 1973] 
CREATED   17.07    5  3 1973
;




COMMENT 'THIS FILE GENERALIZES THE TERM ABOUT TO BE PROVED BY INDUCTION.
WE GENERALIZE ON THE COMMON SUBTERMS ON EITHER SIDE
OF "EQUAL" AND "IMPLIES" STMTS, AND QUALIFY THE GENERALIZATIONS
WITH TYPE STATEMENTS.`;





COMMENT 'FIND ALL COMMON NON-ATOMIC NON-PRIMITIVE SUBTERMS OF TWO TERMS`;

VARS T2 GENRLTLIST ATOMLIST;

FUNCTION COMSUBT1 T1;
VARS X;
IF ATOM(T1)
 THEN
 OCCUR(T1,T2);
 ELSE
 TL(T1) -> X;
 IF (1;LOOPIF X/=NIL THEN LOGAND(COMSUBT1(HD(X)));TL(X)->X;CLOSE;)
  THEN
  IF NOT(LISPPRIM(T1)) AND OCCUR(T1,T2)
   THEN
   IF NOT(MEMBERID(T1,GENRLTLIST))
    THEN T1 :: GENRLTLIST -> GENRLTLIST;CLOSE;
    1; EXIT;
  CLOSE;
 0;
 CLOSE;
END;

FUNCTION COMSUBTERMS T1 T2;
IF CONSCNT(T1) > CONSCNT(T2) THEN T1; T2->T1->T2; CLOSE;
ERASE(COMSUBT(T1));
END;



COMMENT 'FIND ALL COMMON SUBTERMS OCCURRING ACROSS EQS AND
IMPLIES.`;

FUNCTION GENRLT1 TERM;
IF ATOM(TERM) THEN EXIT;
IF HD(TERM) = "EQUAL"
 THEN
 COMSUBTERMS(HD(TL(TERM)),HD(TL(TL(TERM))));
ELSEIF HD(TERM) = "COND" AND HD(TL(TL(TL(TERM)))) == 1
 THEN
 IF ATOM(HD(TL(TERM)))
  THEN;
  ELSE APPLIST(TL(HD(TL(TERM))),LAMBDA;COMSUBTERMS(HD(TL(TL(TERM))));
         END); CLOSE;
 CLOSE;
APPLIST(TL(TERM),GENRLT1);
END;

FUNCTION GENRLTERMS;
VARS GENRLTLIST;
NIL -> GENRLTLIST;
GENRLT1();
GENRLTLIST;
END;


COMMENT 'QUALIFY THE GENERALIZATION BY ADDING TYPE STMTS`;

FUNCTION ADDTYPESTMTS LIST TERM;
VARS X;
IF LIST = NIL
 THEN TERM;
 ELSE
 IF OCCUR(BACK(HD(LIST)),TERM)
  THEN
 TYPEEXPR(FRONT(HD(LIST))) -> X;
 IF HD(X) /= "CONSTTRUE"
  THEN
  [% "IMPLIES", SUBST(BACK(HD(LIST)),"X",X),
        ADDTYPESTMTS(TL(LIST),TERM) %]
  ELSE
  ADDTYPESTMTS(TL(LIST),TERM);
  CLOSE;
 ELSE
 ADDTYPESTMTS(TL(LIST),TERM);
 CLOSE;
 CLOSE;
END;





COMMENT 'THIS FUNCTION MAKES A VERBOSE REPORT ON THE PROGRESS
OF GENERALIZATION.`;

FUNCTION GENREPORT;
IF VERBOSE
 THEN
 POPTTON();
 NL(2);
 PRSEQUEN('GENERALIZE COMMON SUBTERMS BY REPLACING `,
   SUBSTLIST, LAMBDA P;PR(FRONT(P));PRSTRING(' BY `);PR(BACK(P));END);
 NL(2);
 PRSTRING('THE GENERALIZED TERM IS:`);
 NL(2);
 PPR(TERM);
 NL(2);
 CLOSE;
 END;

COMMENT 'THIS IS THE TOP-LEVEL FUNCTION.  IT GENERALIZES ITS
ARGUMENT AS DESCRIBED, QUALIFIES IT, AND THEN PRINTS
A VERBOSE COMMENT IF NEEDED.`;

FUNCTION GENRLIZE TERM;
VARS X SUBSTLIST;
GENRLTERMS(TERM) -> X;
IF X = NIL THEN TERM; EXIT;
MAPLIST(X,
 LAMBDA T;
 GENSKO("GENRL",0) -> X;
 CONSPAIR(T,X);
 END) -> SUBSTLIST;
IF SUBSTLIST = NIL THEN TERM; EXIT;
SUBSTLIST <> GENRLLIST -> GENRLLIST;
ADDTYPESTMTS(SUBSTLIST,APPSUBST(SUBSTLIST,TERM))
 -> TERM;
    (REPORT("G",GENREPORT,"GENRLIZE"));
TERM;
END;


COMMENT
************************************************************
[ALAN]  TRACK  9                                   [ 21.19 14 SEPT 1973]
CREATED   16.28    16   2 1973
;


DEFINE([SLESS [LAMBDA [X Y] [NOT [LTE Y X]]]]);

DEFINE([SUC [LAMBDA [X] [CONS NIL X]]]);

DEFIIME([PRE[LAMBDA[X] [COND X [CDR X] NIL]]]);

DEFINE([DIFF [LAMBDA [X Y] [CDRN Y X]]]);

DEFINE([EQN [LAMBDA [X Y] [EQUAL [LENGTH X] [LENGTH Y]]]]);

DTRACK(256);
INCHARITEM(DIN([DATA]))->DDF1;
POPVAL(FNTOLIST(LAMBDA;VARS X1;
DDF1()->X1;
IF X1 = "EQ" THEN "EQN";
ELSEIF X1 = "LESS" THEN "LTE";
ELSEIF X1 = "ADD" THEN "APPEND";
ELSEIF X1 = "IFF" THEN "EQUAL";
ELSEIF X1 = "FUNCTION" THEN "GOON";
ELSE X1; CLOSE;
END));

DTRACK(9);