PROGRAM RETRPROV;

(****************************************************************************  
*                                                                           *  
*            RETRIEVAL P R O V E R LOOKING FOR AXIOMS                       *  
*            		All rights reserved                                 *  
*									    *
****************************************************************************)





(***************************************************************************)
(* CONSTANTS, VARIABLES AND OBJECTS USED IN PROGRAM                        *)
(***************************************************************************)

(* CONST *)

CONST

(* CHARACTER CODES <IN ASCII> *)

CHRNEG = 78,    (* NEGATION 'N' *)
CHREQU = 69,    (* EXISTENTIAL QUANTIFIER : 'E' *)
CHRITG = 64,    (* ITERATION GREAT QUANTIFIER: '@' *)   
CHRGQU = 65,    (* GLOBAL QUANTIFIER : 'A' *) 
CHRITE = 85,    (* EXISTENTIAL ITERATION QUANTIFIER: 'U' *)   
CHROR  = 86,    (* DISJUNCTION : 'V' *)   
CHRAND = 38,    (* CONJUNCTION : '&' *)   
CHRCOM = 44,    (* COMMA *)   
CHRLPA = 40,    (* LEFT PARENTHESIS *)
CHRRPA = 41,    (* RIGHT PARENTHESIS *)   
CHRBLK = 32,    (* BLANK *)   
CHREND = 63,    (* FORMULA TERMINATOR : '?' *)
CHRCRT = 10,    (* CARRIAGE RETURN *) 
CHREQS = 61,    (* "EQUALS" SIGN - FOR IMPLICATION *) 
CHRGTR = 62,    (* "GREATER" SIGN - ALSO FOR IMPLICATION *)   
CHRLSS = 60,    (* "<" -SIGN FOR EQUIVALENCE *)   

(* FORMULA NODE TYPES *)

LOGKIND = 01,   (* LOGICAL CONSTANT *)
VARKIND = 02,   (* VARIABLE *)
EQVKIND = 03,   (* EQUIVALENCE *) 
CONKIND = 04,   (* CONJUNCTION *) 
DISKIND = 05,   (* DISJUNCTION *) 
IMPKIND = 06,   (* IMPLICATION *) 
NEGKIND = 07,   (* NEGATION *)
IGQKIND = 08,   (* ITERATION GREAT QUANTIFIER *)  
ITEKIND = 09,   (* ITERATION EXISTENTIAL QUANTIFIER *)
IFFKIND = 10,   (* BRANCHING *)   
BEGKIND = 11,   (* BEGINNING OF A COMPOSITION *)  
WHIKIND = 12,   (* CONDITIONAL ITERATION *)   
QUAKIND = 13,   (* QUANTIFIER *)  
ENDKIND = 14,   (* END OF COMPOSITION *)  
THNKIND = 15,   (* POSITIVE CHOICE *) 
ELSKIND = 16,   (* NEGATIVE CHOICE *) 
FIFKIND = 17,   (* END OF BRANCHING *)
DOFKIND = 18,   (* POSITIVE CONDITIONAL ITERATION *)  
ODFKIND = 19,   (* END OF CONDITIONAL ITERATION *)
SEMKIND = 20,   (* SEMICOLON *)   
VARPROG = 21,   (* SUBSTITUTION FOR TERMS X:=TERM *)  
BVARPRO = 22,   (* SUBSTITUTION FOR BOOLEAN VARIABLE A:=FORMULA *)
LITKIND = 23,   (* LITERAL *) 
LT1KIND = 24,   (* RELATION DEFINED BY PROCEDURE *)
FUNKIND = 25,   (* FUNCTION OR CONSTANT *)
FN1KIND = 26,   (* FUNCTION DEFINED BY PROCEDURE *) 
CNTKIND = 27,   (* CONSTANT - NUMBER *)   
CN1KIND = 28,   (* FALSE CONSTANT *)  
VRUKIND = 29,   (* SPECIAL KIND OF VARIABLE - U *)
SUBKIND = 30,   (* VARIABLE TO BE SUBSTITUTED ON *)   
CN2KIND = 31,   (* CONSTANT -NOT NUMBER -OF THE FORM N *) 
ARIKIND = 32,   (* ARITHMETIC OPERATORS *)
BVAKIND = 33,   (* LOGICAL VARIABLE TO BE SUBSTITUTED ON *)
EQUKIND = 34,   (* EQUALITY *)
SIGNTRM = 35,   (* TRACE OF TERM *)

LINLNG  = 80;

UNIT TNODE:CLASS;   
VAR KIND,IDENT:INTEGER, 
    LEFT,RIGHT:TNODE;   
END;

UNIT SEQUENT:CLASS; 
VAR PLEAF,LLEAF:TNODE,  
    NEXT:SEQUENT;   
END;

UNIT POINTER:CLASS; 
VAR NEXT:SEQUENT,   
    DOWN:POINTER,   
    USED:INTEGER;   
END;

UNIT LIST_TERM:CLASS;   
VAR T:TNODE,
    NEXT:LIST_TERM; 
END;

UNIT LIST_AXIOMS:CLASS; 
VAR AXIOM:TNODE,
    NEXT:LIST_AXIOMS;   
END;

UNIT DEF : CLASS;
VAR FUN_REL : TNODE,
    NEXT : DEF;
END;

VAR M : POINTER,   
    M1 : DEF,
    TERM:LIST_TERM, 
    AX:LIST_AXIOMS, 
    SQNT:SEQUENT,   
    G:FILE, 
    ALFA:BOOLEAN,
    DEF_LIT : INTEGER,
    EQU_NUMBER:INTEGER,      (* CURRENT EQUATION *) 
    K_MN_K:INTEGER,          (* CURRENT NUMBER OF ITERATIONS *) 
    LAST_S:INTEGER,          (* MAXIMAL NUMBER OF VARPROG *)
    LAST_Q:INTEGER,          (* MAXIMAL NUMBER OF BVARPRO *)
    LAST_X:INTEGER,          (* MAXIMAL NUMBER OF VARKIND *)
    LAST_D:INTEGER,          (* MAXIMAL NUMBER OF TERM SIGN *)
    C,PEEKCH:INTEGER,        (* CODES OF CURRENT CHAR FROM INPUT FILE *)
    L:INTEGER,               (* NUMBER OF LAST READ CHAR FROM INPUT FILE *) 
    CHARSH:INTEGER,          (* CURRENT NUMBER IN LINE *)   
    DIF:INTEGER,             (* DISTINGUISH KINDS OF FORMULAS TO PROVE *)   
    CHI:BOOLEAN,             (* SHOW IF FORMULA FROM WHILE WAS PROVED  *)   
    LOGIC:BOOLEAN,           (* TELLS WHETHER WHILE HAS ALREADY BEEN USED *)
    LL,LR:INTEGER;           (* COUNTS LEFT AND RIGHT PROGRAM BRACKETS *)    
    
(***************************************************************************)


(***************************************************************************)
(*                     GENERATE TREE OF THE FORMULA 		 	   *)
(***************************************************************************)
  
(***************************************************************************)
(* LOOKS AT NEXT NON-BLANK ON INPUT *)  

UNIT PNC:FUNCTION:INTEGER;  
VAR D : CHARACTER;  
BEGIN   
   PEEKCH:=0;
(* FILL PEEKCHAR IGNORING BLANKS AND CR'S *)  
   WHILE PEEKCH=0 OR  PEEKCH=CHRBLK OR PEEKCH=CHRCRT 
   DO
     READ(G,D);  
     PEEKCH:=ORD(D);
     L:=L+1;  
   OD;   
   RESULT := PEEKCH; 
END PNC;

(****************************************************************************)  
(* MOVES FORWARD N STEPS AND READS CHARACTER *) 

UNIT LOOKN:PROCEDURE(N:INTEGER);
VAR I:INTEGER;  
BEGIN   
   FOR I:=1 TO N
   DO   
     C:=PNC;  
   OD;  
END LOOKN;  

(****************************************************************************)  
(* READS N-TH POSITION IN FILE *)   
UNIT RETN:PROCEDURE(N:INTEGER); 
VAR I:INTEGER;  
BEGIN   
   L:=0;
   CALL RESET(G);   
   FOR I:=1 TO N
   DO   
     C:=PNC;   
   OD;  
END RETN;   

(****************************************************************************)  
(* DISTINGUISH PROGRAMS WRITTEN IN LOGLAN *)

UNIT PRKEY : FUNCTION(N:INTEGER) : INTEGER; 
VAR V,W : ARRAYOF CHARACTER,
    I,C : INTEGER;  
BEGIN   
   ARRAY V DIM(1:26);
   ARRAY W DIM(1:N); 
   V(1):='I';V(2):='F';V(3):='T';V(4):='H';V(5):='E';V(6):='N';
   V(7):= 'L'; V(8):= 'S'; V(9):= 'B'; V(10):= 'G'; V(11):= 'D'; 
   V(12):= 'W'; V(13):= 'O';V(14):= 'i'; V(15):= 'f'; V(16):= 't';   
   V(17):= 'h'; V(18):= 'e'; V(19):= 'n'; V(20):= 'l'; V(21):= 's';  
   V(22):= 'b'; V(23):= 'g'; V(24):= 'd'; V(25):='w'; V(26):= 'o';   
   FOR I:=1 TO N 
   DO 
     IF NOT EOF(G) THEN 
        C:=PNC 
     ELSE 
        RESULT:=0;
	L:=L+N-I+1;
	RETURN;
     FI;	   
     W(I):=CHR(C); 
   OD; 
   CASE N
   WHEN  
       2:IF V(1) = W(1) OR V(14) = W(1) THEN 
            IF V(2) = W(2) OR V(15) = W(2) THEN RESULT:=1 FI   (* 'IF' *)
	 FI;
	 IF V(2) = W(1) OR V(15) = W(1) THEN 
	    IF V(1) = W(2) OR V(14) = W(2) THEN RESULT:=2 FI   (* 'FI' *)
	 FI;
	 IF V(11) = W(1) OR V(24) = W(1) THEN
	    IF V(13) = W(2) OR V(26) = W(2) THEN RESULT:=3 FI  (* 'DO' *)
	 FI;   
	 IF V(13) = W(1) OR V(26) = W(1) THEN
	    IF V(11) = W(2) OR V(24) = W(2) THEN RESULT:=4 FI  (* 'OD' *)
	 FI;   
    WHEN
        3:IF V(5) = W(1) OR V(18) = W(1) THEN 
	     IF ((V(6) = W(2)) OR (V(19) = W(2))) AND ((V(11)=W(3)) 
	         OR (V(24)=W(3)))  THEN RESULT:=5 FI           (* 'END' *)
	  FI;   
    WHEN
        4:IF V(3) = W(1) OR V(16) = W(1) THEN 
             IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(5)=W(3))
	        OR (V(18)=W(3))) THEN
                IF V(6) = W(4) OR V(19) = W(4) THEN RESULT:=6 FI (* 'THEN' *) 
	     FI
	  FI;
          IF V(5) =  W(1) OR V(18) = W(1) THEN
	     IF ((V(7) = W(2)) OR (V(20)=W(2))) AND ((V(8)=W(3)) 
	        OR (V(21)=W(3))) THEN IF V(5) = W(4) OR V(18) = W(4) THEN 
		                         RESULT:=7 FI            (* 'ELSE' *)
	     FI
	  FI;
     WHEN
         5:IF V(9) = W(1) OR V(22) = W(1) THEN 
	      IF ((V(5) = W(2)) OR (V(18)=W(2))) AND ((V(10)=W(3)) 
	         OR (V(23)=W(3))) THEN 
		   IF ((V(1)=W(4)) OR (V(14)=W(4))) AND ((V(6)=W(5)) 
		     OR (V(19)=W(5))) THEN RESULT:=8 FI        (* 'BEGIN' *)   
	      FI
	    FI;
            IF V(12) = W(1) OR V(25) = W(1) THEN
	       IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(1)=W(3))
	          OR (V(14)=W(3))) THEN 
		    IF ((V(7)=W(4)) OR (V(20)=W(4))) AND ((V(5)=W(5)) 
		       OR (V(18)=W(5))) THEN RESULT:=9         (* 'WHILE' *)
		    FI 
		FI;
             FI;
   ESAC;   
   KILL(W);
   KILL(V);
END PRKEY;  

(*****************************************************************************) 
(* READS FORMULA FROM INPUT AND CONSTRUCT A TNODE *)

UNIT GEN_TREE : FUNCTION : TNODE;   

VAR T,S:TNODE;
      
BEGIN   
   T:=ARG_TREE;                                  (* READ FIRST ARGUMENT *) 
   C:=PNC;                                       (* NEXT INPUT CHARACTER *) 
   WHILE C=CHROR OR C=CHRAND OR C=CHREQS OR C=CHRLSS OR C=118
   DO                                            (* LOOP FOR MORE *)    
     S:=NEW TNODE;                               (* ARGUMENTS *)  
     IF T=NONE THEN CALL EXCEPTIONS(1) FI;       (* NULL ARGUMENT *)
     CASE C  
       WHEN CHROR,118 : S.KIND:=DISKIND;  
       WHEN CHRAND: S.KIND:=CONKIND;  
       WHEN CHRLSS: IF PNC<>61 ORIF PNC<>62 THEN CALL EXCEPTIONS(1) FI; 
                    S.KIND:=EQVKIND;  
       WHEN CHREQS: IF PNC<>CHRGTR THEN CALL EXCEPTIONS(1) FI;   
                    S.KIND:=IMPKIND;  
     ESAC;   
     S.RIGHT:=ARG_TREE;                          (* NEXT ARGUMENT *)
     S.LEFT:=T;  
     IF S.RIGHT=NONE THEN CALL EXCEPTIONS(1) FI; 
     T:=S;   
     C:=PNC; 
   OD;   
   RESULT := T;
END GEN_TREE;   

(****************************************************************************)
(* READS ONE ARGUMENT OF INPUT FORMULA *)   

UNIT ARG_TREE : FUNCTION : TNODE;   

VAR T,S,U : TNODE,
    Q : BOOLEAN;   
    
BEGIN   
   C:=PNC;
   IF C=CHREND THEN RETURN FI;                    (* RETURN NONE *) 
   T:=NEW TNODE; 
   RESULT:=T;
   Q:=TRUE;  
   CASE C
      WHEN CHRNEG,110 :T.KIND:=NEGKIND;           (* NEGATION *)
      WHEN CHRGQU :T.KIND:=QUAKIND;               (* GLOBAL QUANTIFIER *)
                   C:=PNC;                        (* FOLLOWING VARIABLE *)  
		   CALL SEARCH_NUM(T.IDENT,TRUE); (* NUMBER *)  
      WHEN CHREQU :S:=NEW TNODE;                  (* EXISTENTIAL QUANTIFIER *)
                   U:=NEW TNODE;                  (* CONVERT TO -'A'- *)
		   S.KIND:=NEGKIND;  
		   S.LEFT:=U;
		   U.KIND:=QUAKIND;  
		   C:=PNC;                        (* VARIABLE NAME *)   
		   CALL SEARCH_NUM(U.IDENT,TRUE); (* VARIABLE NUMBER *) 
		   U.LEFT:=T;
		   T.KIND:=NEGKIND;  
		   RESULT := S   
       OTHERWISE   Q:=FALSE 
    ESAC; 
    IF Q THEN 
       T.LEFT:=ARG_TREE;                          (* CONTINUE DEPTH SEARCH *)
       IF T.LEFT=NONE THEN CALL EXCEPTIONS(1) FI;  
       RETURN  
    FI;   
    IF C=CHROR ORIF C=CHRRPA ORIF C=CHRAND ORIF C=CHREQS ORIF C=CHRGTR ORIF   
       C=CHRLSS THEN  
       IF C=CHREQS THEN
          C:=PNC;
          IF C<>CHRGTR THEN 
             CALL RETN(L-1);
          ELSE 
	     CALL EXCEPTIONS(1);
	  FI
       ELSE
          CALL EXCEPTIONS(1);	  
       FI;
    FI;   
    IF C=CHRLPA THEN  
       RESULT := GEN_TREE  
    ELSE                                         (* LITERAL ONLY *)
       RESULT := LIT_ARG                         (* SO READ IT *)
    FI;   
    KILL (T)  
END ARG_TREE;   

(****************************************************************************)
(* SEARCH FOR A NUMBER *)

UNIT SEARCH_NUM:PROCEDURE(INOUT B:INTEGER;ALEF:BOOLEAN);
BEGIN
   C:=PNC;  
   IF C<48 OR C>57 THEN 
      IF ALEF THEN
         B:=-1
      ELSE 
         CALL RETN(L-1); 
	 B:=VAL(CHR(C));
	 RETURN;
      FI;
   FI;    
   IF NOT ALEF THEN CALL RETN(L-1) FI;
   WHILE C>47 AND C<58  
   DO  
     B:=B*10+C-48; 
     C:=PNC;
   OD; 
   IF ALEF THEN B:=B+1 FI;
   CALL RETN(L-1);
END SEARCH_NUM;
  
(****************************************************************************)
(* CONSTRUCT PREDICATE *)

UNIT PRED : PROCEDURE ( INOUT A, B : INTEGER ; ALEF : BOOLEAN );
BEGIN
   CASE C
     WHEN 61 : A := EQUKIND;
     WHEN 33 : A := LT1KIND; 
     OTHERWISE A := LITKIND;
               CALL SEARCH_NUM ( B, ALEF );         (* SEARCH A NUMBER OF *)
   ESAC;                                            (* PREDICATE *)
END PRED;

(***************************************************************************)
(* CONSTRUCT TERM *)

UNIT MAKE_TERM : PROCEDURE ( INOUT A, B : INTEGER; C : INTEGER, ALEF : BOOLEAN );
BEGIN
   A := C;
   CALL SEARCH_NUM ( B, ALEF );                     (* SEARCH A NUMBER OF *)
END MAKE_TERM;                                      (* TERM *)

(***************************************************************************)
(* GIVES A LENGTH OF PATTERN OF 'S' *)

UNIT LEN_SUB : FUNCTION : INTEGER;
VAR I,J : INTEGER,
    ALFA : BOOLEAN;
BEGIN
  IF C=83 OR C=115 OR C=81 OR C=113 THEN          (* CHECK -S:=... OR -Q:=... *)
   FOR I := 1 TO 3 
   DO
     FOR J := 1 TO I 
     DO
      IF NOT EOF(G) THEN 
       C:=PNC
      ELSE
       CALL RETN(L-J+1);
       ALFA:=TRUE;
       RESULT:=0;
       RETURN
      FI;
     OD;
     IF ALFA THEN EXIT FI;    
     IF C=ORD(':') THEN 
        RESULT:=I;   
        CALL RETN(L-I); 
	RETURN
     FI;
     CALL RETN(L-I);
   OD;
   FI;
   RESULT:=0;
END LEN_SUB;

(***************************************************************************)
(* MAKES A SUBSTITUTION *)

UNIT SUBSTITUTION:FUNCTION:TNODE;
VAR T:TNODE;
BEGIN
      T:=NEW TNODE;
      IF C=83 OR C=115 THEN
           T.KIND:=VARPROG                       (* READ S *)
      ELSE                         
           T.KIND:=BVARPRO                       (* READ A *)
      FI;
      CALL SEARCH_NUM(T.IDENT,TRUE);             (* NUMBER OF 'S' *)
      CALL LOOKN(3);
      CASE T.KIND
         WHEN VARPROG:T.LEFT:=LIT_ARG;
         WHEN BVARPRO:CALL RETN(L-1);T.LEFT:=GEN_TREE;CALL RETN(L-1);
      ESAC;
      RESULT:=T;
END SUBSTITUTION;

(***************************************************************************)
(* CONSTRUCT IF-ALFA-THEN-K-ELSE-M-FI PROGRAM *)

UNIT PROG_IF:FUNCTION:TNODE;
VAR U,S,P,T:TNODE;
BEGIN
   T:=NEW TNODE;	      
   T.KIND:=IFFKIND;                              (* 'IF' *)
   LL:=LL+1;
   T.LEFT:=GEN_TREE;                             (* ALFA *)
   CALL RETN(L-1);                               (* BACK BEFORE 'T' *)
   IF PRKEY(4)<>6 THEN CALL EXCEPTIONS(1) FI;
   S:=NEW TNODE;
   T.RIGHT:=S;
   S.KIND:=THNKIND;                              (* 'THEN '*)
   C:=PNC;
   S.LEFT:=CONSUB;                               (* PROGRAM 'K' *)
   U:=NEW TNODE;
   S.RIGHT:=U;
   IF PRKEY(4)=7 THEN                            (* 'ELSE' *)
      U.KIND:=ELSKIND;
      C:=PNC;
      U.LEFT:=CONSUB                             (* PROGRAM 'M' *)
   ELSE 
      CALL RETN(L-4);
   FI;
   IF PRKEY(2)<>2 THEN CALL EXCEPTIONS(1) FI;
   U.IDENT:=FIFKIND;
   LR:=LR+1;
   IF LL=LR THEN                                 (* AFTER NESTING  DO *)
                                                 (* 'WHILE ETC ' PROGRAM ON *)
      U.RIGHT:=GEN_TREE;                         (* FORMULA BETA *)
      CALL RETN(L-1)
   FI;                                           (* OR TERM TAU *)
   RESULT:=T;			      
END PROG_IF;

(***************************************************************************) 

(* CONSTRUCT BEGIN-K;M;N; -OR MORE PROGRAMS- END PROGRAM *)

UNIT PROG_BEGIN:FUNCTION:TNODE;
VAR V,T,S:TNODE;
BEGIN
   T:=NEW TNODE;
   T.KIND:=BEGKIND;                              (* 'BEGIN' *)
   LL:=LL+1;
   IF PRKEY(3)<>5 THEN                           (* IF NOT 'END' *)
     CALL RETN(L-3);
     V:=NEW TNODE;
     T.LEFT:=V;
     C:=PNC;
     V.LEFT:=CONSUB;                             (* FIRST PROGRAM *)
     WRITELN("1");
     writeln("pekch=", peekch);
     WHILE (PNC=59 OR PEEKCH = 36 )              (* LOOP FOR PROGRAMS *)
     DO
     WRITELN("2");
       IF PEEKCH = 36 THEN V.IDENT := 1 FI;	 (* UNIQUELY SUBSTITUTION *)
       C:=PNC;
       V.RIGHT:=CONSUB;                          (* NEXT PROGRAM *)      
       V.KIND:=SEMKIND;                          (* 'SEMICOLON' *)
       IF PNC=59 THEN 
          S:=NEW TNODE;
	  S.LEFT:=V.RIGHT;
	  V.RIGHT:=S;
	  V:=V.RIGHT
       FI;
       CALL RETN(L-1);
     OD;
     writeln (peekch );
   FI;
   CALL RETN(L-1);
   WRITELN("3");
   IF PRKEY(3)<>5 THEN CALL EXCEPTIONS(1) FI;
   WRITELN("4");
   T.IDENT:=ENDKIND;                             (* 'END' *)
   LR:=LR+1;
   IF LL=LR THEN                                 (* AFTER NESTING  DO *)
                                                 (* 'WHILE ETC ' PROGRAM ON *)
      T.RIGHT:=GEN_TREE;                         (* FORMULA BETA *)
      CALL RETN(L-1)
   FI;                                           (* OR TERM TAU *)
   RESULT:=T;
END PROG_BEGIN;

(***************************************************************************)
(* CONSTRUCT WHILE-ALFA-D0-K-OD PROGRAM *)

UNIT PROG_WHILE:FUNCTION:TNODE;
VAR V,T:TNODE;
BEGIN
    T:=NEW TNODE;
    T.KIND:=WHIKIND;                             (* 'WHILE' *)
    T.LEFT:=GEN_TREE;                            (*  ALFA *)
    CALL RETN(L-1);                              (* BACK BEFORE 'D' *)        
    V:=NEW TNODE;
    T.RIGHT:=V;
    IF PRKEY(2)<>3 THEN CALL EXCEPTIONS(1) FI;
    V.KIND:=DOFKIND;                             (* 'DO' *)
    C:=PNC;
    LL:=LL+1;
    V.LEFT:=CONSUB;                              (* PROGRAM 'K' *)
    IF PRKEY(2)<>4 THEN CALL EXCEPTIONS(1) FI;
    V.IDENT:=ODFKIND;                            (* 'OD' *)
    LR:=LR+1;             
    IF LL=LR THEN                                (* AFTER NESTING  DO *)
                                                 (* 'WHILE ETC ' PROGRAM ON *)
       V.RIGHT:=GEN_TREE;                        (* FORMULA BETA *)
       CALL RETN(L-1);
    FI;                                          (* OR TERM TAU *)
    RESULT:=T;
END PROG_WHILE;
    
(***************************************************************************)
(* SEARCH FOR PROGRAMS *)

UNIT PROG:FUNCTION:TNODE;
BEGIN
   IF PRKEY(2)=1 THEN RESULT:=PROG_IF 
   ELSE 
        CALL RETN(L-2);
        CASE PRKEY(5)
          WHEN  8: RESULT:=PROG_BEGIN;
          WHEN  9: RESULT:=PROG_WHILE;
          OTHERWISE CALL RETN(L-5);
        ESAC;
    FI;
END PROG;

(***************************************************************************)
(* CONSTRUCT ITERATION EXISTENTIAL QUANTIFIER *)

UNIT ITE_EX_Q:FUNCTION:TNODE;
VAR T:TNODE;
BEGIN
   T:=NEW TNODE;
   T.KIND:=ITEKIND;                            (* T.IDENT=0-IT MEANS *)
   C:=PNC;                                     (* THAT RULE WAS NOT ACTIVE *)
   T.RIGHT:=LIT_ARG;
   RESULT:=T;
END ITE_EX_Q;

(***************************************************************************)
(* CONSTRUCT ITERATION GREAT QUANTIFIER *)
 
UNIT ITE_GR_Q:FUNCTION:TNODE;
VAR T:TNODE;
BEGIN
     T:=NEW TNODE;
     T.KIND:=IGQKIND;                            (* T.IDENT=0-IT MEANS *)
     C:=PNC;                                     (* THAT RULE WAS NOT ACTIVE *)
     T.RIGHT:=LIT_ARG;
     RESULT:=T;
END ITE_GR_Q;

(*****************************************************************************)
(* CONSTRUCT SUBSTITUTION AND READS NUMBER OF S *)

UNIT CONSUB:FUNCTION:TNODE;
VAR T:TNODE,
    I,J:INTEGER;
  BEGIN
     T:=NEW TNODE;
     IF C=83 ORIF C=115 ORIF C=81 ORIF C=113 THEN
	  CASE C
	       WHEN 83,115: T.KIND:=VARPROG;
	       WHEN 81,113: T.KIND:=BVARPRO;
	  ESAC;
	  CALL SEARCH_NUM(T.IDENT,TRUE);
	  CALL LOOKN(3);
	  CASE T.KIND
	       WHEN VARPROG : T.LEFT:=LIT_ARG;
	       WHEN BVARPRO : CALL RETN(L-1);
	                      T.LEFT:=GEN_TREE;
			      CALL RETN(L-1);
	  ESAC;
	  FOR I:=2 TO 4                          (* IF NOT 'FI' AND NOT 'OD' *)
	  DO                                     (* AND NOT 'END' AND *)
	    J:=PRKEY(I);
	    CALL RETN(L-I);
	    IF J<>0 THEN EXIT FI;               (* NOT 'ELSE' THEN REPEAT *)
          OD;                                    (* CONSUB *)
          IF (PNC<>59 AND PEEKCH<>36) THEN
             IF J=0 THEN T.RIGHT:=CONSUB ELSE CALL RETN(L-1); FI
	  ELSE
	     CALL RETN(L-1)
	  FI   
     ELSE                               
	  T:=LIT_ARG;                            (* IF NOT SUB THEN PROGRAM *)
     FI;
     RESULT:=T;
END CONSUB;
     
(***************************************************************************)
(* READS INPUT LITERAL *)   

UNIT LIT_ARG : FUNCTION : TNODE;
VAR T,U:TNODE;
        
BEGIN   
   T:=NEW TNODE;                                 (* RESERVE NODE *)
   IF LEN_SUB<>0 THEN 
      T:=SUBSTITUTION;
      C:=PNC;                                    (* OMITED LEFT PAR  *)
      T.RIGHT:=GEN_TREE;
      RESULT:=T;
      RETURN
   ELSE
     CASE C
      WHEN 67,99 : CALL MAKE_TERM(T.KIND,T.IDENT,CN2KIND,TRUE);
		    RESULT:=T;
		    RETURN;                      (* CONSTANT 'C' *)
      WHEN 85     : T:=ITE_EX_Q;  
                    RESULT:=T;
		    RETURN;                      (* ITEKIND 'U' *)
      WHEN 64     : T:=ITE_GR_Q;
                    RESULT:=T;
		    RETURN;                      (* IGQKIND '@' *)
      WHEN 88,120 : CALL MAKE_TERM(T.KIND,T.IDENT,VARKIND,TRUE);
                    RESULT:=T;
		    RETURN;                      (* VARIABLE 'X' *)
      WHEN 117    : CALL MAKE_TERM(T.KIND,T.IDENT,VRUKIND,TRUE);
       		    RESULT:=T;
		    RETURN;			 (* VRUKIND 'u' *)
      WHEN 81,113 : CALL MAKE_TERM(T.KIND,T.IDENT,BVAKIND,TRUE);
	            RESULT:=T;               
		    RETURN;   			 (* BVAKIND 'Q'*)
      WHEN 83,115 : CALL MAKE_TERM(T.KIND,T.IDENT,SUBKIND,TRUE);
	            RESULT:=T;
	            RETURN;                      (* SUBKIND 'S' *)
      WHEN 61,33,                                (* EQUKIND '=' *)
           80,112 : CALL PRED(T.KIND,T.IDENT,TRUE);
                                                 (* LITKIND 'P' *)
						 (* LT1KIND '!' *)
      WHEN 71,103 : CALL MAKE_TERM ( T.KIND, T.IDENT, FUNKIND, TRUE );
                                                 (* FUNKIND 'G' *)
      WHEN 35     : CALL MAKE_TERM ( T.KIND, T.IDENT, FN1KIND, TRUE );
      						 (* FN1KIND '#' *)
      WHEN 70,102 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );
      		    T.IDENT := 0;		 (* LOGICAL FALSE 'F' *)
		    RESULT := T;
		    RETURN;
      WHEN 84,116 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );
      		    T.IDENT := 1;		 (* LOGICAL TRUE 'T' *)
		    RESULT := T;
		    RETURN;		  
      WHEN 48,49,50,51,52,53,54,55,56,57
                  : CALL MAKE_TERM(T.KIND,T.IDENT,CNTKIND,FALSE);
		    RESULT:=T;
		    RETURN;                      (* DIGITS E.G. '2' *)
      WHEN 42,43,45,47,94                        (* '*','+','-','/,'^' *)
                  : CALL MAKE_TERM(T.KIND,T.IDENT,ARIKIND,TRUE);
		    T.IDENT:=C;
      WHEN 37     : CALL MAKE_TERM ( T.KIND, T.IDENT, CN1KIND, TRUE );
		    RESULT := T;
		    RETURN;			 (* FALSE CONSTANT *)        
      WHEN 68,100 : CALL MAKE_TERM ( T.KIND, T.IDENT, SIGNTRM, TRUE );
      						 (* DUMKIND 'D' *)
      OTHERWISE     CALL RETN(L-1);
                    T:=PROG;                     (* PROGRAMS *)
		    RESULT:=T;
		    RETURN;
     ESAC;
     C:=PNC;
     IF C=CHRLPA THEN                            (* LEFT PAR '(' *)
        C:=PNC;                                  (* EXPECT SOME ARGUMENTS *)
        T.LEFT:=LIT_ARG;                         (* READ ARGUMENTS *)
        U:=T.LEFT;                               (* FIRST ON LEFT *)
        WHILE PNC=CHRCOM                         (* COMMA *)
        DO                   
          C:=PNC;                                (* LOOP FOR MORE *) 
	  WHILE U.RIGHT<>NONE                    (* OMIT PROGRAMS ON RIGHT *)
	  DO
	    U:=U.RIGHT;
	  OD;
          U.RIGHT:=LIT_ARG;                      (* NEXT ON RIGHT *)
          U:=U.RIGHT
        OD;                       
        C:=PEEKCH;
	IF C<>CHRRPA THEN CALL EXCEPTIONS(1) FI;(* EXPECT ')' *)
     ELSE 
        CALL RETN(L-1);  
     FI;
     RESULT:=T;    
     RETURN;
   FI;
END LIT_ARG;

(****************************************************************************)
(* STOPS EXECUTION IF THERE IS AN ERROR *)

UNIT EXCEPTIONS:PROCEDURE(N:INTEGER);
BEGIN
   CASE N
      WHEN 1:WRITELN("SYNTAX ERROR");
      WHEN 2:WRITELN("0/0");
      WHEN 3:WRITELN("DIVISION BY ZERO");
      WHEN 4:WRITELN("0^0");
   ESAC;
   RAISE ENDRUN
END EXCEPTIONS;

(***************************************************************************) 
(*		   PRINT FORMULA ON SCREEN AND TO FILE			   *)
(***************************************************************************)
 
(***************************************************************************)
(* PRINT FORMULA ON SCREEN *)
UNIT WR_FOR : PROCEDURE ( C : TNODE );
BEGIN
   IF C = NONE THEN RETURN FI;
   CASE C.KIND 
     WHEN CONKIND : CALL WR_FOR_HELP ( C, '&' ); (* CONJUCTION *)
     WHEN DISKIND : CALL WR_FOR_HELP ( C, 'v' ); (* DISJUNCTION *)
     WHEN IMPKIND : CALL WR_FOR_HELP ( C, '=' ); (* IMPLICATION *)
     WHEN EQVKIND : CALL WR_FOR_HELP ( C, '<' ); (* EQUIVALENCE *)
     WHEN NEGKIND : CALL PUTCH ( 'n' );		 
     		    CALL WR_FOR ( C.LEFT );      (* NEGATION *)
     WHEN LOGKIND : IF C.IDENT = 0 THEN CALL PUTCH ( 'F' ) 
       			           ELSE CALL PUTCH ( 'T' ); (* LOGICAL CONSTANTS *)
		    FI;
     WHEN VARKIND : CALL PUTCH ( 'x' );		 (* VARIABLE *)
     		    CALL PNUM ( C.IDENT );       (* AND ITS IDENTIFIER *)
     WHEN IGQKIND : CALL PUTCH ( '@' );		 (* ITERATION GREAT QUANTIFIER *)
     		    CALL WR_FOR ( C.RIGHT );		
     WHEN ITEKIND : CALL PUTCH ( 'U' );		 (* EXISTENTIAL ITERATION QUANTIFIER *)
     		    CALL WR_FOR ( C.RIGHT );
     WHEN IFFKIND : CALL PUTCH ( 'I' );		 (* IF *)
     		    CALL PUTCH ( 'F' );
		    CALL WR_FOR ( C.LEFT );      (* ALFA *)
		    CALL PUTCH ( 'T' );	    	 (* THEN *)
		    CALL PUTCH ( 'H' );
		    CALL PUTCH ( 'E' );
		    CALL PUTCH ( 'N' );
		    CALL WR_FOR ( C.RIGHT.LEFT ); (* K *)
		    IF C.RIGHT.RIGHT.KIND = ELSKIND THEN 
		       CALL PUTCH ( 'E' );
		       CALL PUTCH ( 'L' );
		       CALL PUTCH ( 'S' );
		       CALL PUTCH ( 'E' ); 	 (* ELSE *)
		       CALL WR_FOR ( C.RIGHT.RIGHT.LEFT ); (* M *)
		    FI;
		    CALL PUTCH ( 'F' );          (* FI *)
		    CALL PUTCH ( 'I' );
		    CALL WR_FOR ( C.RIGHT.RIGHT.RIGHT ); (* BETA *)
     WHEN BEGKIND : CALL PUTCH ( 'B' );
     		    CALL PUTCH ( 'E' );
		    CALL PUTCH ( 'G' );
		    CALL PUTCH ( 'I' );
		    CALL PUTCH ( 'N' );		 (* BEGIN *)
		    CALL WR_FOR ( C.LEFT ); 	 (* K *)
		    CALL PUTCH ( 'E' );
		    CALL PUTCH ( 'N' );
		    CALL PUTCH ( 'D' );		 (* END *)
		    CALL WR_FOR ( C.RIGHT );	 (* BETA *)
     WHEN SEMKIND : CALL WR_FOR ( C.LEFT ); 	 (* K1 *)
                    IF C.IDENT = 1 THEN 
		       CALL PUTCH ( '$' )   	 (* UNIQUELY SUBSTITUTION *)
     		                   ELSE 
		       CALL PUTCH ( ';' )	 (* SEMICOLON *)
		    FI;
		    CALL WR_FOR ( C.RIGHT );	 (* K2 *)
     WHEN WHIKIND : CALL PUTCH ( 'W' );
     		    CALL PUTCH ( 'H' );
		    CALL PUTCH ( 'I' );
		    CALL PUTCH ( 'L' );
		    CALL PUTCH ( 'E' );		 (* WHILE *)
		    CALL WR_FOR ( C.LEFT );	 (* ALFA *)
 		    CALL PUTCH ( 'D' );
		    CALL PUTCH ( 'O' );		 (* DO *)
		    CALL WR_FOR ( C.RIGHT.LEFT );(* K *)
		    CALL PUTCH ( 'O' );
		    CALL PUTCH ( 'D' ); 	 (* OD *)
		    CALL WR_FOR ( C.RIGHT.RIGHT ); (* BETA *)
     WHEN QUAKIND : CALL PUTCH ( 'A' );		 (* GREAT QUANTIFIER *)
     		    CALL PUTCH ( 'x' );		 (* VARIABLE *)
		    CALL PNUM ( C.IDENT );	 (* ITS NUMBER *)
		    CALL WR_FOR ( C.LEFT );	 (* ALFA *)
     WHEN EQUKIND,
          LITKIND,
          FUNKIND,
	  LT1KIND,
	  FN1KIND : CASE C.KIND 
	              WHEN EQUKIND : CALL PUTCH ( '=' );
	              WHEN LITKIND : CALL PUTCH ( 'P' ); 
	  	      WHEN FUNKIND : CALL PUTCH ( 'G' );
		      WHEN LT1KIND : CALL PUTCH ( '!' );
		      WHEN FN1KIND : CALL PUTCH ( '#' );
		    ESAC; 			 (* PREDICATE OR FUNCTION *)
		    CALL PNUM ( C.IDENT );
     		    IF C.LEFT = NONE THEN RETURN FI;
		    CALL PUTCH ( '(' );
		    C := C.LEFT;
		    WHILE C <> NONE 
		    DO
		      CALL WR_FOR ( C );	 (* ARGUMENT *)
		      C := C.RIGHT;		 (* TAKE NEXT ARGUMENT *)
		      IF C <> NONE THEN CALL PUTCH ( ',' ) FI;
		    OD;
		    CALL PUTCH ( ')' );
     WHEN CNTKIND : CALL PNUM ( C.IDENT + 1 );   (* NUMERIC CONSTANT *)
     WHEN CN1KIND : CALL PUTCH ( '%' );		 (* FALSE CONSTANT *)
     		    CALL PNUM ( C.IDENT + 1 );
     WHEN CN2KIND : CALL PUTCH ( 'C' );		 (* CONSTANT OF THE FORM 'C' *)
     		    CALL PNUM ( C.IDENT );
     WHEN ARIKIND : CALL PUTCH ( CHR ( C.IDENT ) ); (* ARITHMETIC OPERATION *)
		    IF C.LEFT.RIGHT = NONE THEN 
		       CALL WR_FOR ( C.LEFT );
		       RETURN 
		    FI;
		    CALL PUTCH ( '(' );
		    CALL WR_FOR ( C.LEFT );
		    CALL PUTCH ( ',' );
		    CALL WR_FOR ( C.LEFT.RIGHT );
		    CALL PUTCH ( ')' );
     WHEN VRUKIND : CALL PUTCH ( 'u' );		 (* SPECIAL KIND OF VARIABLE *)
     		    CALL PNUM ( C.IDENT );
     WHEN BVAKIND : CALL PUTCH ( 'Q' );		 (* LOGICAL VARIABLE *)
     		    CALL PNUM ( C.IDENT );
     WHEN SUBKIND : CALL PUTCH ( 'S' );		 (* VARABLE TO BE SUBSTITUTED ON *)
     		    CALL PNUM ( C.IDENT );
     WHEN VARPROG,
          BVARPRO : IF C.KIND = VARPROG THEN 
	  	       CALL PUTCH ( 'S' )	 (* SUBSTITUTION S:= *)
		    ELSE 
		       CALL PUTCH ( 'Q' );	 (* Q:= *)
		    FI;
     		    CALL PNUM ( C.IDENT );
		    CALL PUTCH ( ':' );
		    CALL PUTCH ( '=' );
		    CALL WR_FOR ( C.LEFT );	 (* TAU OR ALFA*)
		    IF C.RIGHT = NONE THEN RETURN FI;
		    CALL PUTCH ( '(' );		 (* NEXT FORMULA *)
		    CALL WR_FOR ( C.RIGHT );
		    CALL PUTCH ( ')' );
     WHEN SIGNTRM : CALL PUTCH ( 'D' );		 (* DUMKIND *)
     		    CALL PNUM ( C.IDENT );
   ESAC; 
END WR_FOR;     

(***************************************************************************)
(* HELP FOR WR_FOR PROCEDURE *)

UNIT WR_FOR_HELP : PROCEDURE ( C : TNODE, CH : CHARACTER );
BEGIN
   CALL PUTCH ( '(' );
   CALL WR_FOR ( C.LEFT );
   CALL PUTCH ( CH );
   CASE CH
      WHEN '=' : CALL PUTCH ( '>' );
      WHEN '<' : CALL PUTCH ( '=' );
      		 CALL PUTCH ( '>' );
   ESAC;	
   CALL WR_FOR ( C.RIGHT );
   CALL PUTCH ( ')' );
END WR_FOR_HELP;

(***************************************************************************)
(*                 ADDITIONAL PROCEDURES AND FUNCTIONS			   *)
(***************************************************************************)

(***************************************************************************)
(* GIVES A VALUE OF CHARACTER *)

UNIT VAL:FUNCTION(A:CHARACTER):INTEGER; 
BEGIN   
   RESULT:=ORD(A)-48   
END VAL;

(*****************************************************************************)
(* PRINTS ALL TREES IN A SEQUENT *)

UNIT SHOW_SEQ : PROCEDURE ( A : SEQUENT );
BEGIN
   IF A <> NONE THEN 
      WRITELN("P");
      CALL WR_FOR ( A.PLEAF ); (* SHOW_TREE ( A.PLEAF); *)
      WRITELN("L");
      CALL WR_FOR ( A.LLEAF );  (* SHOW_TREE ( A.LLEAF ); *)
      WRITELN;
      CALL SHOW_SEQ ( A.NEXT );
   FI;
END SHOW_SEQ;
   
(*****************************************************************************)
(* PRINTS TREE *)

UNIT SHOW_TREE : PROCEDURE ( A : TNODE );
BEGIN
   IF A<>NONE THEN
      WRITELN(A.KIND,"=K",A.IDENT,"=I");
      CALL SHOW_TREE(A.LEFT);
      CALL SHOW_TREE(A.RIGHT);
   FI;
END SHOW_TREE;

(****************************************************************************)
(* MOVE UP I TNODES FROM RIGHT (P=1) OR LEFT (P=0) SIDE *)

UNIT LIFT : PROCEDURE ( T : TNODE; I, P : INTEGER );
VAR A : TNODE;
BEGIN
   WHILE I>0
   DO
     CASE P
       WHEN 1: A := T.RIGHT;
       WHEN 0: A := T.LEFT;
     ESAC;
     T.KIND  := A.KIND;
     T.IDENT := A.IDENT;
     T.RIGHT := A.RIGHT;
     T.LEFT  := A.LEFT;
     KILL ( A );
     I := I - 1
  OD;
END LIFT;

(****************************************************************************)
(* MOVE UP POINTER *)

UNIT LIFT_PNTR : PROCEDURE ( INOUT M1 : POINTER );
VAR M2 : POINTER;
BEGIN
    IF M1 <> NONE THEN
       M2 := M1.DOWN;
       CALL ERASE_SEQ ( M1.NEXT );
       IF M1.DOWN <> NONE THEN
          M1.NEXT := M1.DOWN.NEXT;
	  M1.DOWN := M1.DOWN.DOWN;
          KILL ( M2 )
       ELSE
          KILL ( M1 )
       FI;	
    FI;
END LIFT_PNTR;
    
(****************************************************************************)
(* MOVE LAST NON-EMPTY RIGHT OR LEFT TNODE OF A SEQUENT TO THE BEGINNING *)

UNIT MOVE : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER);
VAR HEAD1,TAIL : SEQUENT,
    S : INTEGER;
BEGIN
    HEAD1 := NEW SEQUENT;
    TAIL := LAST ( M , P );
    IF P=1 THEN R := R + 1 FI;
    S := R + P;
    CASE S
       WHEN 0:HEAD1.LLEAF:=TAIL.LLEAF;           (* LEFT TO LEFT *)
              TAIL.LLEAF:=NONE ;                 (* P=0,R=0 *)
       WHEN 3:HEAD1.PLEAF:=TAIL.PLEAF;           (* RIGHT TO RIGHT *)
              TAIL.PLEAF:=NONE;                  (* P=1,R=1 *)
       WHEN 1:HEAD1.PLEAF:=TAIL.LLEAF;           (* LEFT TO RIGHT *)
              TAIL.LLEAF:=NONE;                  (* P=0,R=1 *)
       WHEN 2:HEAD1.LLEAF:=TAIL.PLEAF;           (* RIGHT TO LEFT *)
              TAIL.PLEAF:=NONE;                  (* P=1,R=0 *)
    ESAC;
    HEAD1.NEXT := M.NEXT;
    M.NEXT := HEAD1;
END MOVE;

(****************************************************************************)
(* GIVES THE LAST NON EMPTY P-SIDE SEQUENT *)

UNIT LAST:FUNCTION(M:POINTER;P:INTEGER):SEQUENT;
VAR HEAD1:SEQUENT;
BEGIN
   IF M=NONE ORIF M.NEXT=NONE THEN 
      RESULT:=NONE;
      RETURN;
   FI;
   IF P=1 THEN
      HEAD1:=M.NEXT;
      IF HEAD1.PLEAF<>NONE THEN RESULT:=HEAD1 FI;
      WHILE HEAD1.NEXT<>NONE
      DO
      IF HEAD1.NEXT.PLEAF<>NONE THEN
         RESULT:=HEAD1.NEXT
      FI;
      HEAD1:=HEAD1.NEXT
      OD;
   ELSE
      HEAD1:=M.NEXT;
      IF HEAD1.LLEAF<>NONE THEN RESULT:=HEAD1 FI;
      WHILE HEAD1.NEXT<>NONE
      DO
        IF HEAD1.NEXT.LLEAF<>NONE THEN
            RESULT:=HEAD1.NEXT;
        FI;
        HEAD1:=HEAD1.NEXT
      OD;
   FI;
END LAST;

(****************************************************************************)
(* GO TO THE END OF A PROGRAM WITH TAU *)

UNIT END_OF_PRG : PROCEDURE ( INOUT C : TNODE );
BEGIN
   IF C = NONE THEN RETURN FI;
   WHILE C.RIGHT <> NONE 
   DO 
     C := C.RIGHT;
   OD;
END END_OF_PRG;

(*****************************************************************************)
(* GO TO THE END OF PROGRAM *)

UNIT END_OF_P : PROCEDURE ( INOUT C : TNODE );
VAR D : TNODE;
BEGIN
   IF C = NONE THEN RETURN FI;
   WHILE C.RIGHT <> NONE 
   DO
     D := C;
     C := C.RIGHT;
   OD;
   C := D;
END END_OF_P;

(*****************************************************************************)
(* GO TO THE END OF AXIOMS LIST *)
 
UNIT END_OF_AX : PROCEDURE ( INOUT AX1 : LIST_AXIOMS );
BEGIN
    IF AX = NONE THEN RETURN FI;
    AX1 := AX;
    WHILE AX1.NEXT <> NONE
    DO
       AX1 := AX1.NEXT;
    OD;
END END_OF_AX;
    
(*****************************************************************************)
(* GO TO THE END OF POINTERS *)

UNIT END_OF_M : PROCEDURE ( INOUT M : POINTER , A : SEQUENT );
VAR M1 : POINTER;
BEGIN
    IF M = NONE THEN RETURN FI;
    M.NEXT := NONE;
    WHILE M.DOWN <> NONE 
    DO
      M := M.DOWN;
    OD;
    M1 := NEW POINTER;
    M.DOWN := M1;
    CALL SQUEEZE ( M1 , 0 );
    CALL SQUEEZE ( M1 , 1 );
    M1.NEXT := A;
    CALL CUT_SEQ ( M1.NEXT );
    M1.DOWN := NONE;
END END_OF_M;
       
(*****************************************************************************)
(* ERASE A TREE *)

UNIT ERASE : PROCEDURE ( A : TNODE );
BEGIN
   IF A <> NONE THEN
      CALL ERASE ( A.LEFT );			 (* GO TO LAST LEFT TNODE *)
      CALL ERASE ( A.RIGHT );			 (* GO TO LAST RIGHT TNODE *)
      KILL ( A );				 (* REMOVE TNODE *)
   FI;
END ERASE;

(*****************************************************************************)
(* ERASE A SEQUENT *)

UNIT ERASE_SEQ : PROCEDURE ( A : SEQUENT );
BEGIN
   IF A <> NONE THEN
      CALL ERASE_SEQ ( A.NEXT );		 (* GO TO THE LAST SEQUENT *)
      CALL ERASE ( A.LLEAF );			 (* REMOVE LEFT TREE *)
      CALL ERASE ( A.PLEAF );			 (* REMOVE RIGHT TREE *)
      KILL ( A );				 (* REMOVE SEQUENT *)
   FI;
END ERASE_SEQ;

(*****************************************************************************)
(* ERASE AN EMPTY POINTER, I.E. LINKED TO THE EMPTY FORMULA ' |- ' *)

UNIT ERASE_PNTR : PROCEDURE ( INOUT M1 : POINTER );
BEGIN
   IF M1 = NONE THEN RETURN FI;			 (* SEQUENT IS EMPTY *)
   CALL LIFT_PNTR ( M1 );			 (* REMOVE POINTER *)
   CALL ERASE_PNTR ( M1 );	  		 (* REMOVE NEXT POINTER *)
END ERASE_PNTR;

(*****************************************************************************)
(* REMOVE LIST OF AXIOMS *)

UNIT ERASE_AX : PROCEDURE ( AX : LIST_AXIOMS );
BEGIN
   IF AX = NONE THEN RETURN FI;
   CALL ERASE_AX ( AX.NEXT );
   CALL ERASE ( AX.AXIOM );
END;

(*****************************************************************************)
(* GO TO THE END OF SUBSTITUTION *)

UNIT END_OF_S : PROCEDURE ( INOUT A , B : TNODE );
BEGIN
   IF A = NONE THEN RETURN FI;
   WHILE A.KIND=VARPROG OR A.KIND=BVARPRO 
   DO
     B:=A;
     A:=A.RIGHT;
     IF A = NONE THEN EXIT FI ;
   OD;
END END_OF_S;

(****************************************************************************)
(* MAKES A COPY OF TNODE TREE *)

UNIT COPYTNODE : FUNCTION ( X : TNODE ) : TNODE;
BEGIN
   IF X <> NONE THEN
      RESULT := COPY ( X );
      RESULT.LEFT  := COPYTNODE ( X.LEFT );
      RESULT.RIGHT := COPYTNODE ( X.RIGHT );
   FI;
END COPYTNODE;

(****************************************************************************)
(* MAKES A COPY OF ALL SEQUENTS IN A TREE , INCLUDING TNODES *)

UNIT COPYSEQUENT : FUNCTION ( X : SEQUENT ) : SEQUENT;
BEGIN
   IF X <> NONE THEN 
      RESULT := COPY ( X );
      RESULT.PLEAF := COPYTNODE ( X.PLEAF );
      RESULT.LLEAF := COPYTNODE ( X.LLEAF );
      RESULT.NEXT := COPYSEQUENT ( X.NEXT );
   FI;
END COPYSEQUENT;

(*****************************************************************************)
(* UPDATE THE GREATEST NUMBER OF VARIABLE *)
 
UNIT LAST1_X : PROCEDURE ( A : TNODE );
BEGIN
     IF A=NONE THEN RETURN FI;
     IF A.KIND=VARKIND THEN
        IF LAST_X < A.IDENT THEN LAST_X := A.IDENT FI;
     FI;
     CALL LAST1_X ( A.LEFT );
     CALL LAST1_X ( A.RIGHT );
END  LAST1_X;

(****************************************************************************)
(* LOOKING FOR THE GREATEST BVARPRO SUBSTITUTION *)

UNIT LAST1_Q:PROCEDURE(A:TNODE);
BEGIN
     IF A=NONE THEN RETURN FI;
     IF A.KIND=BVARPRO THEN
	IF LAST_Q < A.IDENT THEN LAST_Q:=A.IDENT FI;
     FI;
     CALL LAST1_Q(A.RIGHT);
     CALL LAST1_Q(A.LEFT);
END  LAST1_Q;

(****************************************************************************)
(* UPDATE THE GREATEST NUMBER OF VARPROG *)

UNIT LAST1_S : PROCEDURE ( A : TNODE );
BEGIN 
     IF A=NONE THEN RETURN FI;
     IF A.KIND=VARPROG THEN
        IF LAST_S < A.IDENT THEN LAST_S := A.IDENT FI;
     FI;
     CALL LAST1_S ( A.LEFT );
     CALL LAST1_S ( A.RIGHT );   
END LAST1_S;

(****************************************************************************)
(* UPDATE THE GREATEST NUMBER OF VARKIND IN THE DIFINITION TREE AND CHANGE IT 
   INTO SUBKIND *)
   
UNIT LAST2_S : FUNCTION ( A1 : TNODE, I : INTEGER ) : INTEGER;
VAR A : TNODE,
    K : INTEGER;
BEGIN
     A := M1.FUN_REL.LEFT;
     FOR K := 1 TO I
     DO
       IF K=1 THEN A := A.LEFT
              ELSE A := A.RIGHT;
       FI;
     OD;
     IF A.KIND=SUBKIND THEN RESULT := A.IDENT
                       ELSE LAST_S := LAST_S+1;
		      	    RESULT := LAST_S;
                            CALL RENAME ( A1,A.KIND,A.IDENT );
     FI;
END LAST2_S;

(****************************************************************************)
(* CHANGE VARKIND TO SUBKIND RESPECTIVELY *)

UNIT RENAME : PROCEDURE ( A1 : TNODE, I,J : INTEGER );
BEGIN
     IF A1=NONE THEN RETURN FI;
     IF A1.KIND=I AND A1.IDENT=J THEN A1.KIND := SUBKIND;
                                      A1.IDENT := LAST_S
     FI;
     CALL RENAME ( A1.LEFT,I,J );
     CALL RENAME ( A1.RIGHT,I,J );
END RENAME;

(****************************************************************************)
(* REMOVE ALL EMPTY SEQUENTS AFTER CALLING SQUEEZE PROCEDURE *)

UNIT CUT_SEQ : PROCEDURE ( A : SEQUENT );
BEGIN
   IF A <> NONE THEN CALL CUT_SEQ ( A.NEXT ) ELSE RETURN FI; (* GO TO THE LAST 
   							        SEQUENT *)
   IF A.PLEAF = NONE AND A.LLEAF = NONE THEN KILL ( A ) FI;  (* WHEN EMPTY 
   								REMOVE IT *)
END CUT_SEQ;

(****************************************************************************)
(* FIND A CONNECTIVE NUMBER 'R' *)

UNIT FINDCONN : FUNCTION ( A : SEQUENT , R , P : INTEGER ) : TNODE;
VAR B : TNODE;
BEGIN
     IF A = NONE THEN RETURN FI;
     CASE P
     WHEN 1: IF A.PLEAF = NONE THEN RETURN FI;
             B := A.PLEAF;
     	     CALL FUNCTOR ( R , B );
	     RESULT := B;
     WHEN 0: IF A.LLEAF = NONE THEN RETURN FI;
             B := A.LLEAF;
   	     CALL FUNCTOR ( R , B );
	     RESULT := B;
     ESAC;
END FINDCONN;

(****************************************************************************)
(* SEARCH FOR A FUNCTOR *)

UNIT FUNCTOR : PROCEDURE ( R : INTEGER ; INOUT B : TNODE );
     
BEGIN
   IF B.KIND = BEGKIND ANDIF B.LEFT <> NONE ANDIF B.LEFT.IDENT = 1 ANDIF
      B.LEFT.KIND = SEMKIND THEN
      B := B.RIGHT;
   FI;
   WHILE B.KIND = VARPROG OR B.KIND = BVARPRO
   DO
      B := B.RIGHT;
   OD;
   IF B.KIND <> R THEN B := NONE FI;
END FUNCTOR;

(****************************************************************************)
(* LOOK FOR MORE THAN ONE EQUALITIES IN A SEQUENT OF TYPE U=TERM *)

UNIT SEARCH_U : FUNCTION ( A : SEQUENT ) : BOOLEAN;
VAR I : INTEGER;
BEGIN
   WHILE A <> NONE 
   DO
     IF A.PLEAF <> NONE THEN
     IF A.PLEAF.KIND = EQUKIND ANDIF
        ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND ) THEN
	I := I + 1 ;
     FI;
     IF I = 2 THEN 
        RESULT := TRUE; 
	RETURN;
     FI;
     FI;
     A := A.NEXT;
   OD;
END SEARCH_U;

(****************************************************************************)
(* CHECK WHETHER THERE IS IN A SEQUENT THE DEFINITION SYMBOL LIKE: FUNCTION, 
   LITERAL ; OR PROGRAM *)

UNIT CHECK_L_F_P : FUNCTION ( A : SEQUENT ) : BOOLEAN;
BEGIN
    IF A <> NONE AND NOT ALFA THEN 
       ALFA := CHECK_L_F_P_TN ( A.PLEAF ) OR CHECK_L_F_P_TN ( A.LLEAF );
       RESULT := ALFA OR CHECK_L_F_P ( A.NEXT );
    FI;
END CHECK_L_F_P;

(*****************************************************************************)
(* CHECK WHETHER THERE IS IN A TNODE THE DEFINITION SYMBOL LIKE: FUNCTION, 
   LITERAL ; OR PROGRAM *)

UNIT CHECK_L_F_P_TN : FUNCTION ( C : TNODE ) : BOOLEAN;
VAR BETA : BOOLEAN ;
BEGIN
    IF C <> NONE THEN
       BETA := ( C.KIND > 2 AND C.KIND < 23 ) OR C.KIND = LT1KIND OR
  	       C.KIND = FN1KIND OR C.KIND = 4;
     RESULT := BETA OR CHECK_L_F_P_TN ( C.LEFT ) OR CHECK_L_F_P_TN ( C.RIGHT );
    FI;
END;

(****************************************************************************)
(* WRITES A CHARACTER TO FILE *)

UNIT PUTCH : PROCEDURE ( A : CHARACTER );
BEGIN
    IF CHARSH >= LINLNG THEN 
       WRITELN ;
       CHARSH := 0 
    FI;
    WRITE ( A );
    CHARSH := CHARSH + 1 
END PUTCH;

(****************************************************************************)


(****************************************************************************)
(* PRIMARY RULES AND FIRSTLY PROCEDURES AND FUNCTIONS APPLIED IN THE TREE   *) 
(****************************************************************************)

(****************************************************************************)
(* REPLACE IN SEQUENT A ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)

UNIT REP_F_SEQ : PROCEDURE ( A : SEQUENT , N : INTEGER );
BEGIN
    IF A = NONE THEN RETURN FI;
    CALL REP_FUN_N ( A.LLEAF , N );
    CALL REP_FUN_N ( A.PLEAF , N );
    CALL REP_F_SEQ ( A.NEXT , N );
END REP_F_SEQ;

(****************************************************************************)
(* REPLACE IN TNODE C ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)

UNIT REP_FUN_N : PROCEDURE ( C : TNODE , N : INTEGER );
BEGIN
    IF C = NONE THEN RETURN FI;
    IF C.KIND=FUNKIND AND C.IDENT = N THEN C.KIND := FN1KIND FI;
    CALL REP_FUN_N ( C.LEFT , N );
    CALL REP_FUN_N ( C.RIGHT , N );
END REP_FUN_N;

(****************************************************************************)
(* REPLACE IN TNODE C ALL FUNKIND TO FN1KIND *)

UNIT REP_FUN : PROCEDURE ( C : TNODE );
BEGIN
   IF C = NONE THEN RETURN FI;
   IF C.KIND = FUNKIND THEN C.KIND := FN1KIND FI;
   CALL REP_FUN ( C.LEFT );
   CALL REP_FUN ( C.RIGHT );
END REP_FUN;

(****************************************************************************)
(* REPLACE ALL LITKIND WITH NUMBER N IN SEQUENT A TO LT1KIND *)

UNIT REP_L_SEQ : PROCEDURE ( A :SEQUENT , N :INTEGER );
BEGIN
    IF A = NONE THEN RETURN FI;
    CALL REP_LIT_N ( A.PLEAF , N );
    CALL REP_LIT_N ( A.LLEAF , N );
    CALL REP_L_SEQ ( A.NEXT , N );
END REP_L_SEQ;

(****************************************************************************)
(* REPLACE ALL LITKIND IN TNODE C TO LT1KIND *)

UNIT REP_LIT : PROCEDURE ( C : TNODE );
BEGIN
   IF C = NONE THEN RETURN FI;
   IF C.KIND = LITKIND THEN C.KIND := LT1KIND FI;
   CALL REP_LIT ( C.LEFT );
   CALL REP_LIT ( C.RIGHT );
END REP_LIT;

(****************************************************************************)
(* REPLACE ALL LITKIND WITH NUMBER N IN TNODE C TO LT1KIND *)

UNIT REP_LIT_N : PROCEDURE ( C : TNODE , N : INTEGER );
BEGIN
   IF C = NONE THEN RETURN FI;
   IF C.KIND = LITKIND AND C.IDENT = N  THEN C.KIND := LT1KIND FI;
   CALL REP_LIT_N ( C.LEFT , N );
   CALL REP_LIT_N ( C.RIGHT , N );
END REP_LIT_N;

(*****************************************************************************)
(* REPLACE DEFINITION SYMBOL LIKE : FUNKIND AND LITKIND INTO FN1KIND AND 
   LT1KIND RESPECTIVELY *)

UNIT REP_F_L : PROCEDURE ( M3 : DEF );
VAR M2 : DEF ;
BEGIN
  M2 := M3;
  DO 
    CASE M3.FUN_REL.KIND 
      WHEN EQUKIND : CALL REP_FUN_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT ); 
      				 (* REPLACE FUNKIND WITH PROPER NUMBERS *)
				 (* INTO FN1KIND IN A DEFINITION TREE *)
		     CALL REP_F_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );
		     		 (* DO THE SAME BUT IN DATA TREE *)
      WHEN EQVKIND : CALL REP_LIT_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT );
      				 (* REPLACE LITKIND WITH PROPER NUMBERS *)
				 (* INTO LT1KIND IN A DEFINITION TREE *) 
		     CALL REP_L_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );
		     		 (* DO THE SAME BUT IN DATA TREE *)
    ESAC;
    IF M2 = M3 THEN EXIT FI;
    M2 := M2.NEXT;
  OD;
END REP_F_L;

(*****************************************************************************)
(* USE THE DEFINITION OF FUNCTION *)

UNIT RULEDF_F : PROCEDURE ( M : POINTER, P : INTEGER, F_NUMBER : INTEGER );
VAR A , A1 , ALR , C , B1 : TNODE,
    ALFA : BOOLEAN,
    B : SEQUENT;
BEGIN
     B:=M.NEXT;
     CASE P
     WHEN 1:
          IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;
          A := B.PLEAF;
          DO
            WHILE A.KIND <> EQUKIND
            DO
              IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
              B := B.NEXT;
              A := B.PLEAF;
            OD;
            IF FOUND_F ( B.PLEAF , B.PLEAF , A , ALR , ALFA , F_NUMBER ) THEN 
	       EXIT FI;
            IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
            B := B.NEXT;
            A := B.PLEAF;          OD;
     WHEN 0:
          IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;
          A := B.LLEAF;
          DO
            WHILE A.KIND <> EQUKIND
            DO
              IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
              B := B.NEXT;
              A := B.LLEAF;
            OD;
            IF FOUND_F ( B.LLEAF , B.LLEAF , A , ALR , ALFA , F_NUMBER ) THEN 
	       EXIT 
	    FI;
            IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
            B := B.NEXT;
            A := B.LLEAF;
          OD;
     ESAC;
     C := ALR.RIGHT;				 (* C STORES RIGHT SIDE OF *)
     						 (* OPERATION CONTAINING FUNCTION *)
     A1 := COPYTNODE ( M1.FUN_REL.LEFT.RIGHT );  (* REMEMBER K -TAU *)
     IF ALR.LEFT = NONE THEN    		 (* IF THERE IS NO ARGUMENT *)
	B1 := A1
     ELSE
        B1 := NEW TNODE;
	CALL MAKE_SUB ( ALR.LEFT , A1 , B1 );    (* ALR.LEFT REFERS TO FIRST ARG *)
	CALL LIFT ( B1 , 1 , 0 );
     FI;
     CALL END_OF_P ( A1 );			 (* A1 REFERS TO THE END OF PROGRAM *)
						 (* BEFORE TAU *)
     IF A.LEFT = ALR THEN			 (* FUNCTION IS ON LEFT *)
        KILL ( A.LEFT );
        A.LEFT := A1.RIGHT			 (* JOIN TAU *)
     ELSE					 (* FUNCTION IS ON RIGHT *) 
        KILL ( A.RIGHT );
        A.RIGHT := A1.RIGHT;			 (* JOIN TAU *)
     FI;
     A1.RIGHT.RIGHT := C;			 (* JOIN U OR SOMETHING ELSE *)
     A1.RIGHT := NONE;
     CASE P
	   WHEN 1 : A1 := B.PLEAF;		 (* MOVE '=' BEYOND PROGRAM *)
	   	    B.PLEAF := B1;		 (* ON RIGHT *)
		    CALL END_OF_PRG ( B1 );
		    B1.RIGHT := A1;
   	   WHEN 0 : A1 := B.LLEAF;		 (* OR ON LEFT SIDE *)
	   	    B.LLEAF := B1;
		    CALL END_OF_PRG ( B1 );
		    B1.RIGHT := A1;
     ESAC
END RULEDF_F;

(*****************************************************************************)
(* SEARCH FUNCTION FN1KIND IN A TREE TO BE SUBSTITUTED ON *)

UNIT FOUND_F : FUNCTION ( B , B1 : TNODE ; INOUT C , D : TNODE , ALFA : BOOLEAN ;
	                 F_NUMBER : INTEGER ) : BOOLEAN;
BEGIN
   IF B <> NONE THEN
      IF B.KIND = FN1KIND AND B.IDENT = F_NUMBER  THEN 
         RESULT := TRUE ; 
	 IF NOT ALFA THEN 
	    ALFA := TRUE;
       	    D := B;
	    C := B1;
	 FI;
	 RETURN 
      ELSE
    RESULT := FOUND_F ( B.LEFT , B , C , D , ALFA , F_NUMBER ) 
              OR FOUND_F ( B.RIGHT , B , C , D , ALFA , F_NUMBER )
      FI;
   FI;
END FOUND_F;      
       
(****************************************************************************)
(* MAKE THE SUBSTITUTION *)

UNIT MAKE_SUB:PROCEDURE ( D , A1 , A : TNODE );
VAR F,G,E:TNODE,
    I : INTEGER;
BEGIN    
     IF D.RIGHT = NONE THEN			 (* ONLY ONE ARGUMENT *)
     	E := NEW TNODE;
	A.LEFT:=E;
	E.KIND := VARPROG;
	E.LEFT := D;
	E.IDENT :=LAST2_S ( A1 , 1 );
	E.RIGHT := A1;
	RETURN;
     FI;
     F := NEW TNODE;				 (* MORE THAN ONE ARGUMENTS *)
     F.KIND := BEGKIND;
     F.IDENT := ENDKIND;     
     WHILE D <> NONE
     DO			 			 (* VIEW ALL ARGUMENTS AND *)
     						 (* MAKE RELEVANT SUBSTITUTION *)
        					 (* CREATE SUBSTITUTION CELLS *)
     						 (* FILL THEM *) 
     						 (* AND JOIN THEM- XI:=TI *)
       G := NEW TNODE;
       G.KIND := SEMKIND;
       G.IDENT := 1;				 (* SIGN THAT SUBSTITUTION *)
       						 (* SHOULD BE DONE SIMULTANEOUSLY *)
       E:=NEW TNODE;
       G.LEFT := E;
       E.KIND := VARPROG;				
       E.LEFT := D;				 (* ASSOCIATE VARIABLE WITH ITS term XI:=TI *)       
       E.RIGHT := D.RIGHT;			 
       D.RIGHT := NONE;
       IF I=0 THEN 
          A.LEFT := F; 
          I := 1; 
	  F.LEFT := G;
       ELSE 
          A.RIGHT := G;
	  I := I+1;
       FI;
       E.IDENT := LAST2_S ( A1 , I );		 (* ASSIGN VARPROG NEW NUMBER 
       						    AND UPDATE LIST OF VARPROG'S *)
       A := G;
       D := E.RIGHT;
       E.RIGHT := NONE;
     OD;
     CALL LIFT ( G , 1 , 0 );
     F.RIGHT := A1;
END MAKE_SUB;     

(****************************************************************************)
(* USE A DEFINITION OF RELATION *)

UNIT RULEDF_L : PROCEDURE ( M : POINTER , P : INTEGER , N : INTEGER );
VAR A,A1,D : TNODE,
    B : SEQUENT;
BEGIN
     B := M.NEXT;
     CASE P
     WHEN 1:
          IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;
          A := B.PLEAF;
          WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND
          DO
            IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;
            B := B.NEXT;
            A := B.PLEAF;
          OD;
     WHEN 0:
          IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;
          A := B.LLEAF;
          WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND
          DO
            IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;
            B := B.NEXT;
            A := B.LLEAF;
          OD;
     ESAC;
     IF A.KIND = EQVKIND THEN A := A.LEFT FI;
     D := A.LEFT;				 (* FIRST ARGUMENT *)
     A1 := COPY ( M1.FUN_REL.RIGHT );	         (* REMEMBER K-ALFA *)
     IF D=NONE THEN
     	A.RIGHT := A1;
	CALL LIFT ( A , 1 , 1 );
	CALL SWEEP ( A );
	RETURN;
     FI;
     CALL MAKE_SUB ( D , A1 , A );
     CASE P
        WHEN 0 : CALL LIFT ( B.LLEAF.LEFT, 1, 0 );
	         CALL SWEEP ( B.LLEAF );
	WHEN 1 : CALL LIFT ( B.PLEAF.LEFT, 1, 0 );
    	         CALL SWEEP ( B.PLEAF );
     ESAC;	
          CASE P 
        WHEN 0 : A := B.LLEAF;
	WHEN 1 : A := B.PLEAF;
     ESAC;
     IF A.LEFT.KIND = BEGKIND ANDIF A.LEFT.LEFT <> NONE ANDIF 
        A.LEFT.LEFT.KIND = SEMKIND ANDIF A.LEFT.LEFT.IDENT = 1 THEN
	D := A.LEFT;	   		         (* MOVE OUT PARALLEL *)
	A.LEFT := D.RIGHT;			 (* SUBSTITUTION BEYOND *)
	D.RIGHT := A;				 (* EQUIVALENCE *)
	CASE P 
	   WHEN 0 : B.LLEAF := D;
	   WHEN 1 : B.PLEAF := D;
	ESAC;
     FI;

END RULEDF_L;

(*****************************************************************************)


(*****************************************************************************)
(* 				AID RULES 				     *)
(*****************************************************************************)

(****************************************************************************)
(* THROWING AWAY THE SEQUENCE OF SEQUENTS INCLUDING 0 ON LEFT SIDE
   OR 1 ON RIGHT SIDE *)

UNIT THROW_RUBBISH : PROCEDURE ( M : POINTER );
VAR A : SEQUENT;
BEGIN
     IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
     A := M.NEXT;
     WHILE A<>NONE
     DO
       IF A.PLEAF<>NONE THEN
          IF A.PLEAF.IDENT=1 ANDIF A.PLEAF.KIND=LOGKIND THEN
	     CALL ERASE_SEQ ( M.NEXT ); 	 (* IF THERE IS TRUE ON RIGHT *)
	     EXIT;				 (* SIDE, THEN REMOVE ALL SEQUENTS *)
	  FI;
	  IF DEF_LIT = 1 ANDIF A.PLEAF.KIND = LOGKIND ANDIF A.PLEAF.IDENT = 0 THEN
	     KILL ( A.PLEAF );
	  FI;
       FI;
       IF A.LLEAF<>NONE THEN
          IF A.LLEAF.IDENT=0 ANDIF A.LLEAF.KIND=LOGKIND THEN 
	     CALL ERASE_SEQ ( M.NEXT ); 	 (* IF THERE IS FALSE ON LEFT *) 
	     EXIT;				 (* SIDE, THEN REMOVE ALL SEQUENTS *)
	  FI;
	  IF DEF_LIT = 1 ANDIF A.LLEAF.KIND = LOGKIND ANDIF A.LLEAF.IDENT = 1 THEN
	     KILL ( A.LLEAF );
	  FI;					
       FI;
       A := A.NEXT;				 (* OTHERWISE GO ON FURTHER *)
     OD;
END THROW_RUBBISH;

(****************************************************************************)
(* CALCULATE STANDARD FUNCTIONS *,+,-,^,/ *)

UNIT RULEVAL : PROCEDURE ( A:TNODE; INOUT ALFA:BOOLEAN );
VAR BETA : BOOLEAN,
    B,C  : TNODE;
BEGIN
     BETA := TRUE;						
     IF A=NONE THEN RETURN FI;			
     IF A.KIND=ARIKIND THEN 			 (* MUST BEGIN WITH FUNCTOR *)
        CALL CHECKCHAR ( A.LEFT , BETA );	 (* CHECK WHETHER IN THE FOLLOWING
						    TREE THERE ARE ONLY STANDARD
						    FUNCTORS AND DIGITS *)
        IF BETA THEN 				 (* IF YES *)
	   BETA := FALSE;
	   CALL FUNCHECK ( A , BETA );
	   A.IDENT := COUNT ( A ) ; 		 (* COUNT THIS EXPRESSION *)
	   IF BETA THEN 
	      A.KIND := CN1KIND
	   ELSE 
	      A.KIND := CNTKIND;
  	   FI;
	   CALL ERASE ( A.LEFT );		 (* WHEN DONE REMOVE IT *)
	   ALFA := TRUE;
	   RETURN
	ELSE					 (* MAKE SPECIAL ARITHMETIC *)
	   BETA := TRUE;			 (* OPERATIONS LIKE : X+X A.S.O. *)
	   B := COPYTNODE ( A.LEFT );
	   C := B.RIGHT;
	   B.RIGHT := NONE;
	   CALL COMPARE ( B , C , BETA );	 (* COMPARE TWO TREES *)
	   IF BETA THEN 			 (* THEY ARE EQUAL *)
	      B.RIGHT := C;
	      CALL ERASE ( B );
	      CASE A.IDENT 
	         WHEN 42 : A.IDENT := 94;	 (* TERM*TERM -> TERM^2 *)
		 	   A.LEFT.RIGHT.KIND := CNTKIND;
			   A.LEFT.RIGHT.IDENT := 2;
			   CALL ERASE ( A.LEFT.RIGHT.LEFT );
		 WHEN 43 : A.IDENT := 42;	 (* TERM+TERM -> 2*TERM *)
		 	   A.LEFT.KIND := CNTKIND;
			   A.LEFT.IDENT := 2;
			   CALL ERASE ( A.LEFT.LEFT );
	      ESAC;		   
	   FI;
	FI;
     FI;
     CALL RULEVAL ( A.LEFT,ALFA );
     CALL RULEVAL ( A.RIGHT,ALFA );
END RULEVAL;

(****************************************************************************)
(* CALLS COUNT_0_1 UNTIL IT IS NOT USELESS *)

UNIT ZEROS_AND_ONES : PROCEDURE ( A : TNODE ; ALFA : BOOLEAN );
VAR BETA : BOOLEAN;         (* BETA MEANS THAT COUNT_0_1 IS STILL WORKING *)
BEGIN
     BETA := TRUE;
     WHILE BETA
     DO
       BETA := FALSE;
       CALL COUNT_0_1 ( A , BETA );
       ALFA := ALFA OR BETA;
     OD;
END ZEROS_AND_ONES;

(****************************************************************************)
(* DOES ALL ARITHMETIC OPERATIONS *)

UNIT COUNT_0_1 : PROCEDURE ( B : TNODE ; INOUT ALEF : BOOLEAN );
VAR BETA : BOOLEAN;
BEGIN
     IF B=NONE THEN RETURN FI;
     IF B.KIND=ARIKIND THEN
        BETA := FALSE;
	IF B.LEFT.KIND = CNTKIND OR B.LEFT.KIND = CN1KIND THEN
        CASE B.LEFT.IDENT
             WHEN 0: CASE B.IDENT
                          WHEN 42,94:CALL FUNCHECK ( B.LEFT.RIGHT , BETA );
			   	  IF B.IDENT = 94 AND B.LEFT.RIGHT.IDENT = 0 
				     AND B.LEFT.RIGHT.KIND = CNTKIND THEN
				     CALL EXCEPTIONS ( 4 )
				  ELSE
                                  IF BETA THEN
                                     B.KIND := CN1KIND
                                  ELSE
                                     B.KIND := CNTKIND;
                                  FI;
                                  B.IDENT := 0;
                                  CALL ERASE ( B.LEFT );
                                  ALEF := TRUE;
				  RETURN;
				  FI;
                          WHEN 43:B.LEFT.RIGHT.RIGHT := B.RIGHT;
			  	  CALL LIFT ( B,1,0 );
                                  CALL LIFT ( B,1,1 );
                                  ALEF := TRUE;
				  RETURN;
	 	  	  WHEN 47:IF B.LEFT.RIGHT.KIND=CNTKIND AND
			                  B.LEFT.RIGHT.IDENT = 0 THEN
			             CALL EXCEPTIONS ( 2 )
				  ELSE
				     CALL FUNCHECK ( B.LEFT.RIGHT,BETA );
                                     IF BETA THEN
                                        B.KIND := CN1KIND;
                                     ELSE
                                        B.KIND := CNTKIND;
                                     FI;
                                     B.IDENT := 0;
                                     CALL ERASE ( B.LEFT );
                                     ALEF := TRUE;
				     RETURN;
				  FI;
			  WHEN 45:CALL LIFT ( B.LEFT,1,1 );
			  	  ALEF := TRUE;
				  RETURN;
                     ESAC;
             WHEN 1: CASE B.IDENT
                          WHEN 42:B.LEFT.RIGHT.RIGHT := B.RIGHT;
			  	  CALL LIFT ( B,1,0 );
                                  CALL LIFT ( B,1,1 );
                                  ALEF := TRUE;
				  RETURN;
                          WHEN 94:CALL FUNCHECK ( B.LEFT.RIGHT,BETA );
                                  IF BETA THEN
                                     B.KIND := CN1KIND;
                                  ELSE
                                     B.KIND := CNTKIND;
                                  FI;
                                  B.IDENT := 1;
                                  CALL ERASE ( B.LEFT );
                                  ALEF := TRUE;
				  RETURN;
			  WHEN 47:IF B.LEFT.RIGHT.IDENT=1 THEN
			             B.KIND := CNTKIND;
				     B.IDENT := 1;
				     CALL ERASE ( B.LEFT );
				     ALEF := TRUE;
				  FI;
				  RETURN;
                     ESAC;
        ESAC
       ELSE
        IF B.LEFT.RIGHT.KIND = CNTKIND OR B.LEFT.RIGHT.KIND = CN1KIND THEN
        CASE B.LEFT.RIGHT.IDENT
             WHEN 0: CASE B.IDENT
                          WHEN 42:CALL FUNCHECK ( B.LEFT , BETA );
                                  IF BETA THEN
                                     B.KIND := CN1KIND;
                                  ELSE
                                     B.KIND := CNTKIND;
                                  FI;
                                  B.IDENT := 0;
                                  CALL ERASE ( B.LEFT );
                                  ALEF := TRUE;
				  RETURN;
                          WHEN 43:CALL ERASE ( B.LEFT.RIGHT );
			      	  B.LEFT.RIGHT := B.RIGHT;
			          CALL LIFT ( B,1,0 );
                                  ALEF := TRUE;
				  RETURN;
                          WHEN 94:CALL FUNCHECK ( B.LEFT,BETA );
                                  IF BETA THEN
                                     B.KIND := CN1KIND;
                                  ELSE
                                     B.KIND := CNTKIND;
                                  FI;
                                  B.IDENT := 1;
                                  CALL ERASE ( B.LEFT );
                                  ALEF := TRUE;
				  RETURN;
			  WHEN 47:CALL EXCEPTIONS ( 3 );
			  WHEN 45:KILL ( B.LEFT.RIGHT );
			  	  B.LEFT.RIGHT := B.RIGHT;
				  CALL LIFT ( B,1,0 );
				  ALEF := TRUE;
				  RETURN;
                     ESAC;
	     WHEN 1: CASE B.IDENT
                        WHEN 42,47,94:B.LEFT.RIGHT.RIGHT := B.RIGHT;
	                              CALL LIFT ( B,1,0 );
		    		      CALL LIFT ( B.RIGHT,1,1 );
                                      ALEF := TRUE;
				      RETURN;
                        ESAC;
         ESAC;
	 FI;
        FI;
      FI;
        CALL COUNT_0_1 ( B.LEFT,ALEF );
        CALL COUNT_0_1 ( B.RIGHT,ALEF );
END COUNT_0_1;

(****************************************************************************)
(* CHECK WHETHER THERE IS A FN1KIND OR CN1KIND IN A TREE *)
(* FN1KIND MEANS THE NAME OF FUNCTION DEFINED BY A PROCEDURE OF THE
   FORM F(X)=KT *)

UNIT FUNCHECK : PROCEDURE ( C : TNODE ; INOUT BETA : BOOLEAN );
BEGIN
     IF C = NONE THEN RETURN FI;
     IF C.KIND = FN1KIND OR C.KIND = CN1KIND THEN 
        BETA := TRUE;
	RETURN; 
     FI;
     CALL FUNCHECK ( C.LEFT , BETA );
     CALL FUNCHECK ( C.RIGHT , BETA );
END FUNCHECK;      	    

(****************************************************************************)
(* TERM=TERM CONVERTS TO LOGICAL 1 *)

UNIT RULEIDE : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
VAR A,B  : TNODE,
    BETA : BOOLEAN;
BEGIN
  IF C=NONE THEN RETURN FI;
  BETA := TRUE;
  IF C.KIND=EQUKIND THEN 
     CASE C.LEFT.KIND 
        WHEN VARPROG , 
	     BVARPRO : A := C.LEFT;
	     	       CALL END_OF_S ( A,B );
     	 	       B := A.RIGHT;
		       A.RIGHT := NONE;
       	 	       CALL COMPARE ( C.LEFT,B,BETA );
		       A.RIGHT := B;
	WHEN IFFKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT ;
		       C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := NONE;
		       CALL COMPARE ( C.LEFT , A , BETA );
		       C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := A;		       
	WHEN BEGKIND : A := C.LEFT.RIGHT.RIGHT;
		       C.LEFT.RIGHT.RIGHT := NONE;
		       CALL COMPARE ( C.LEFT, A ,BETA );
		       C.LEFT.RIGHT.RIGHT := A;
	WHEN WHIKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT;
		       C.LEFT.RIGHT.RIGHT.RIGHT := NONE;
		       CALL COMPARE ( C.LEFT , A , BETA );
		       C.LEFT.RIGHT.RIGHT.RIGHT := A;
        OTHERWISE      A := C.LEFT.RIGHT;	 (* STORE RIGHT ARGUMENT *)
		       C.LEFT.RIGHT := NONE;
		       CALL COMPARE ( C.LEFT , A , BETA );
		       C.LEFT.RIGHT := A;
     ESAC;
     IF BETA THEN 
        C.KIND  := LOGKIND;
        C.IDENT := 1;
        CALL ERASE ( C.LEFT );
        ALFA := TRUE;
    FI;
  FI;
END RULEIDE;

(*****************************************************************************)
(* COMPARE THOROUGHLY TWO TREES *)

UNIT COMPARE : PROCEDURE ( A,B : TNODE ; INOUT BETA : BOOLEAN );
BEGIN
        IF A <> NONE AND B <> NONE THEN
           IF A.KIND=B.KIND AND A.IDENT=B.IDENT THEN 
              CALL COMPARE ( A.LEFT,B.LEFT,BETA );
              CALL COMPARE ( A.RIGHT,B.RIGHT,BETA )
	   ELSE
              BETA := FALSE;
	      RETURN
           FI
 	ELSE
	   IF A <> NONE OR B <> NONE THEN BETA := FALSE FI;  
  	FI
END COMPARE;      

(****************************************************************************)
(* TERM1 <> TERM2 IN THE STANDARD INTERPRETATION CONVERTS TO 0 *)

UNIT RULEIDT : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
VAR BETA : BOOLEAN;
BEGIN
     BETA := TRUE;
     IF C = NONE THEN RETURN FI;
     IF C.KIND = EQUKIND THEN  
     	CALL CHECKCHAR ( C.LEFT,BETA );
     	IF BETA THEN 
	   IF COUNT( C.LEFT ) <> COUNT( C.LEFT.RIGHT ) THEN
	      C.KIND := LOGKIND;
	      C.IDENT := 0;
              CALL ERASE ( C.LEFT );
	      ALFA := TRUE;
	   FI;
	FI;
     FI;
END RULEIDT;

(****************************************************************************)
(* CALCULATOR *)

UNIT COUNT : FUNCTION ( A : TNODE ) : INTEGER;
VAR BASIS,I,POWER,LIMIT : INTEGER;
BEGIN
    IF A.KIND <> ARIKIND THEN
       RESULT := A.IDENT
    ELSE
       CASE A.IDENT
         WHEN 42 : RESULT := COUNT( A.LEFT ) * COUNT( A.LEFT.RIGHT );
	 WHEN 43 : RESULT := COUNT( A.LEFT ) + COUNT( A.LEFT.RIGHT );
	 WHEN 47 : RESULT := COUNT( A.LEFT ) DIV COUNT( A.LEFT.RIGHT );
	 WHEN 45 : RESULT := COUNT( A.LEFT ) - COUNT( A.LEFT.RIGHT );
         WHEN 94 : IF A.LEFT.RIGHT.IDENT=0 THEN 
	              RESULT := 1
                   ELSE
		      POWER := 1;
                      BASIS := COUNT ( A.LEFT );
		      LIMIT := COUNT ( A.LEFT.RIGHT );
                      FOR I:=1 TO LIMIT
                      DO
                        POWER := POWER * BASIS;
                      OD;
		      RESULT := POWER;
                   FI;
       ESAC
    FI; 
END COUNT;

(****************************************************************************)
(* CHECK WHETHER TERM IS BUILT ONLY BY STANDARD FUNCTORS *)

UNIT CHECKCHAR : PROCEDURE ( A : TNODE ; INOUT BETA : BOOLEAN );
BEGIN
     IF A<>NONE THEN
	IF A.KIND=ARIKIND OR A.KIND=CNTKIND OR A.KIND=CN1KIND THEN
           CALL CHECKCHAR ( A.LEFT , BETA );
           CALL CHECKCHAR ( A.RIGHT , BETA )
	ELSE
	   BETA := FALSE;
	   RETURN
	FI;   
     FI;
END CHECKCHAR;

(****************************************************************************)
(* A HELP FOR DUST_BIN PROCEDURE , MANAGE THE VERY SIMPLE BOOLEAN OPERATIONS *)

UNIT DUST : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
BEGIN
     CASE C.KIND
          WHEN CONKIND: IF C.LEFT.KIND=LOGKIND THEN
	                   CASE C.LEFT.IDENT
                             WHEN 1: CALL ERASE ( C.LEFT );
			     	     CALL LIFT ( C,1,1 );
				     ALFA := TRUE;
                             WHEN 0: CALL ERASE ( C.RIGHT );
			     	     CALL LIFT ( C,1,0 );
				     ALFA := TRUE;
                           ESAC;
			   RETURN;
			FI;
			IF C.RIGHT.KIND=LOGKIND THEN
                           CASE C.RIGHT.IDENT
                             WHEN 1: CALL ERASE ( C.RIGHT );
			     	     CALL LIFT ( C,1,0 );
				     ALFA := TRUE;
                             WHEN 0: CALL ERASE ( C.LEFT );
			     	     CALL LIFT ( C,1,1 );
				     ALFA := TRUE;
                           ESAC;
			   RETURN;
			FI;			
          WHEN DISKIND: IF C.LEFT.KIND=LOGKIND THEN
	  		   CASE C.LEFT.IDENT
                             WHEN 1: CALL ERASE ( C.RIGHT );
			     	     CALL LIFT ( C,1,0 );
				     ALFA := TRUE;
                             WHEN 0: CALL ERASE ( C.LEFT );
			     	     CALL LIFT ( C,1,1 );
				     ALFA := TRUE;
                           ESAC;
			   RETURN;
			FI;
			IF C.RIGHT.KIND=LOGKIND THEN
                           CASE C.RIGHT.IDENT
                             WHEN 1: CALL ERASE ( C.LEFT );
			     	     CALL LIFT ( C,1,1 );
				     ALFA := TRUE;
                             WHEN 0: CALL ERASE ( C.RIGHT );
			     	     CALL LIFT ( C,1,0 );
				     ALFA := TRUE; 
                           ESAC;
			   RETURN;
			FI;
          WHEN NEGKIND: IF C.LEFT.KIND=LOGKIND THEN
	  		   CASE C.LEFT.IDENT
                             WHEN NEGKIND: CALL LIFT ( C,2,0 );
			     		   ALFA := TRUE;
                             WHEN 1: CALL LIFT ( C,1,0 );
                                     C.IDENT:=0;
				     ALFA := TRUE;
                             WHEN 0: CALL LIFT ( C,1,0 );
                                     C.IDENT:=1;
				     ALFA := TRUE;
                           ESAC;
			   RETURN;
			FI;
          WHEN IMPKIND : IF C.LEFT.KIND=LOGKIND THEN 
	  		   CASE C.LEFT.IDENT
                             WHEN 1: CALL ERASE ( C.LEFT );
			     	     CALL LIFT ( C,1,1 );
				     ALFA := TRUE;
                             WHEN 0: C.KIND := LOGKIND;
			     	     C.IDENT:=1;
                                     CALL ERASE ( C.LEFT );
                                     CALL ERASE ( C.RIGHT );
				     ALFA := TRUE;
                           ESAC;
			   RETURN;
			FI;
                        IF C.RIGHT.KIND=LOGKIND THEN
			   CASE C.RIGHT.IDENT
                             WHEN 1: C.KIND := LOGKIND;
			     	     C.IDENT := 1;
                                     CALL ERASE ( C.LEFT );
                                     CALL ERASE ( C.RIGHT );
				     ALFA := TRUE;
                             WHEN 0: C.KIND:=NEGKIND;
                                     CALL ERASE ( C.RIGHT );
				     ALFA := TRUE;
                           ESAC;
   			   RETURN;
		       FI;
     ESAC;
END DUST;

(****************************************************************************)
(* CALLED BY SWEEP PROCEDURE *)

UNIT DUST_BIN : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );
BEGIN
     IF C = NONE THEN RETURN FI;
     CALL RULEVAL ( C,ALFA );			 (* COUNT ARITHMETIC EXPRESSIONS : '1+2 -> 3' *)
     CALL ZEROS_AND_ONES ( C,ALFA );		 (* COUNT EXPRESSIONS E.G. 0*X *)
     CALL RULEIDT ( C,ALFA );			 (* TERM1 <> TERM2 -> FALSE *)
     CALL RULEIDE ( C,ALFA );			 (* TERM1 IDENTICAL WITH TERM2 -> TRUE *)
     CALL DUST ( C,ALFA );			 (* SIMPLIFY BOOLEAN EXPRESSIONS *)
     CALL DUST_BIN ( C.LEFT,ALFA );
     CALL DUST_BIN ( C.RIGHT,ALFA );
 END DUST_BIN;

(****************************************************************************)
(* MANAGE THE SWEEPING SYSTEM IN A TREE , CALL DUST_BIN PROCEDURE *)

UNIT SWEEP : PROCEDURE ( C : TNODE );
VAR ALFA : BOOLEAN;
BEGIN
    ALFA := TRUE;
    WHILE ALFA		
    DO						 (* SWEEP IF IT IS POSSIBLE *)
      ALFA := FALSE;
      CALL DUST_BIN ( C , ALFA );		 (* MAKE IT AND UPDATE ALFA *)
    OD;
END SWEEP;

(****************************************************************************)
(* SQUEEZE A LIST OF SEQUENTS BY GETTING RID OF ALL THE HOLES *)

UNIT SQUEEZE : PROCEDURE ( M : POINTER , P : INTEGER );
VAR A,B : SEQUENT;
BEGIN
     IF M=NONE ORIF M.NEXT=NONE ORIF LAST (M,P)=NONE THEN RETURN FI;
     A := FIRSTHOLE ( M , P );
     B := NEXTNODE ( A , P );
     WHILE LAST(M,P).NEXT <> A
     DO
       CASE P
               WHEN 1: A.PLEAF := B.PLEAF;
                       B.PLEAF := NONE;
               WHEN 0: A.LLEAF := B.LLEAF;
                       B.LLEAF := NONE;
       ESAC;
       B := NEXTNODE ( A.NEXT , P );
       A := FIRSTHOLE ( M , P );
     OD;
END SQUEEZE;

(****************************************************************************)
(* SEARCH FOR THE FIRST NON-EMPTY TNODE AFTER THE FIRST HOLE *)

UNIT NEXTNODE : FUNCTION ( U : SEQUENT , P : INTEGER ) : SEQUENT;
VAR ALFA : BOOLEAN;
BEGIN
     IF U=NONE THEN RETURN FI;
     WHILE U <> NONE AND NOT ALFA
     DO
       CASE P
            WHEN 1:IF U.PLEAF <> NONE THEN
                      RESULT := U;
                      ALFA := TRUE
                   ELSE
                      U := U.NEXT;
                   FI;
            WHEN 0:IF U.LLEAF <> NONE THEN
                      RESULT := U;
                      ALFA := TRUE
                   ELSE
                      U := U.NEXT
                   FI;
       ESAC;
     OD;
END NEXTNODE;

(****************************************************************************)
(* SEARCH FOR THE FIRST HOLE *)

UNIT FIRSTHOLE : FUNCTION ( M : POINTER , P : INTEGER ) : SEQUENT;
VAR ALFA : BOOLEAN,
    A : SEQUENT;
BEGIN
     IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
     A := M.NEXT;
     WHILE A <> NONE AND NOT ALFA
     DO
       CASE P
            WHEN 1: IF A.PLEAF=NONE THEN
                       RESULT := A;
                       ALFA := TRUE
                    ELSE
                       A := A.NEXT;
                    FI;
            WHEN 0: IF A.LLEAF=NONE THEN
                       RESULT := A;
                       ALFA := TRUE
                    ELSE
                       A := A.NEXT;
                    FI;
       ESAC;
     OD;
END FIRSTHOLE;

(****************************************************************************)

(****************************************************************************)
(* 			     ESSENTIAL RULES 				    *)
(****************************************************************************)

(****************************************************************************)
(* SENDS TO PROPER RULES *)

UNIT RULES : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER );
VAR C : TNODE;
BEGIN
      C := FINDCONN ( LAST ( M , P ) , R , P );
      IF C=NONE THEN RETURN FI;
      CASE R
	   WHEN 03: CALL RULEEQU ( M,C,P );
           WHEN 04: CALL RULECON ( M,C,P );
           WHEN 05: CALL RULEDIS ( M,C,P );
	   WHEN 06: CALL RULEIMP ( M,C,P );
	   WHEN 07: CALL RULENEG ( M,C,P );
	   WHEN 09: IF P=1 THEN CALL RULEEXIST ( M,C,P )
                       ELSE CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC );
                    FI;
           WHEN 08: IF P=1 THEN CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC )
                       ELSE CALL RULEEXIST ( M,C,P )
                    FI;
           WHEN 10: CALL RULEIF ( M,C,P );		    
           WHEN 11: CALL RULEBEG ( M, C, P );
           WHEN 12: CALL RULEWHL ( M,C,P );
           WHEN 13: CALL RULEQUAN ( M,P );		  
      ESAC;
END RULES;

(****************************************************************************)
(* RULE FOR THE PROGRAM BEGIN-END *)

UNIT RULEBEG : PROCEDURE ( INOUT M : POINTER, C : TNODE, P : INTEGER );
VAR A,B,D,E,F : TNODE;
BEGIN
     A := C.RIGHT;                               (* HOLD BETA *)
     IF C.LEFT.IDENT = 1 THEN			 (* SIMULTANEOUSLY SUBSTITUTION *)
        CALL BEG_SUB ( C ) ;
	CALL MOVE ( M, P, P );
	RETURN;
     FI;
     IF C.LEFT<>NONE THEN
        CALL LIFT ( C, 1, 0 );                   (* THROW 'BEGIN' AND 'END' *)
	IF C.KIND=0 THEN                         (* ONLY ONE PROGRAM *)
	   CALL LIFT ( C, 1, 0 );
	   CALL END_OF_PRG ( C );                (* GO TO THE END OF IT *)
	   C.RIGHT := A                          (* REFERS TO 'BETA' *)
	ELSE                                     (* MORE THAN ONE PROGRAM *)
	   WHILE C.KIND=SEMKIND                  (* LOOP FOR NEXT PROGRAMS *)
	   DO
	     B := C.RIGHT;                       (* HOLD NEXT PROGRAM *)
	     CALL LIFT ( C, 1, 0 );              (* THROW SEMICOLON *)
	     CALL END_OF_PRG ( C );              (* GO TO THE END OF PROGRAM *)
	     C.RIGHT := B;                        	     C:=B;
	   OD;
	   CALL END_OF_PRG ( C );                (* END OF LAST PROGRAM *)
	   C.RIGHT := A;                         (* REFERS TO 'BETA' *)
	FI
     ELSE                                        (* NO PROGRAM *)
        CALL LIFT ( C, 1, 1 )                         
     FI;
     CALL MOVE ( M, P, P );
END RULEBEG;

(****************************************************************************)
(* DO SIMULTANEOUS SUBSTITUTIONS, MADE BY RULEDF_F AND RULEDF_L 
   PROCEDURES, WHEN ONLY ATOMS LEFT *)

UNIT BEG_SUB : PROCEDURE ( C : TNODE );
BEGIN
   IF C.RIGHT.KIND = LITKIND OR C.RIGHT.KIND = EQUKIND 
      OR C.RIGHT.KIND = LOGKIND OR C.RIGHT.KIND = BVAKIND THEN	
   						 (* MAKE ONLY IN ATOMS AND *)
						 (* LOGICAL CONTANTS *)
      CALL SUB ( C, C.RIGHT );
      CALL ERASE ( C.LEFT );			 (* WHEN DONE ERASE SUBSTITUTIONS *)
      CALL LIFT ( C, 1, 1 );
   FI;
END BEG_SUB;
						
(*****************************************************************************)
(* CALLED BY BEG_SUB PROCEDURES *)

UNIT SUB : PROCEDURE ( A, A1 : TNODE );
VAR B,C,D : TNODE;
BEGIN
   IF A1 = NONE THEN RETURN FI;
   IF A1.KIND = SUBKIND THEN			 (* MIGHT BE CHANGED *)
      B := A.LEFT;		 	         (* REFERS TO SEMICOLON *)
      WHILE B <> NONE 				 (* VIEW THE WHOLE LIST *)
      DO
        IF B.KIND <> SEMKIND THEN
	   C := B
	ELSE
           C := B.LEFT;				 (* C REFERS TO NEXT ARG *)
	FI;
        IF C.IDENT = A1.IDENT THEN		 (* WILL BE CHANGED *)
           A1.LEFT := COPYTNODE ( C.LEFT ); 	 (* S/TAU *)
           D := A1.RIGHT;			 (* STORES TEMPORARILY NEXT ARG *)
           CALL LIFT ( A1, 1, 0 );		 (* REMOVE S *)
   	   A1.RIGHT := D;			 (* LINK STORED ARG *)
   	   CALL SUB ( A, A1.RIGHT );		 (* REALIZE SIMULTANEOUS *)
						 (* SUBSTITUTION *)
           RETURN;						 
        FI;
        B := B.RIGHT;
      OD;
    FI;
    CALL SUB ( A, A1.LEFT );
    CALL SUB ( A, A1.RIGHT );
END SUB;

(****************************************************************************)
(* RULE FOR A PROGRAM WHILE-DO-OD *)

UNIT RULEWHL : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
VAR B,D,E,F,G,S,T,U,V : TNODE;
BEGIN
     B := C.LEFT;                                (* HOLD 'ALFA' *)
     D := C.RIGHT.LEFT;                          (* HOLD PROGRAM 'K' *)
     E := C.RIGHT.RIGHT;                         (* HOLD 'BETA' *)
     C.KIND := BVARPRO;                          (* Q:=... *)
     C.IDENT := -LAST_Q-1;
     G := NEW TNODE;
     C.LEFT := G;
     G.KIND := LOGKIND;                          (* ...1 *)
     G.IDENT := 1;
     C.RIGHT.KIND := ITEKIND;                    (* ITER. GREAT QUANT. *)
     C.RIGHT.IDENT := 0;
     G := NEW TNODE;                             (* 'BEGIN' - 'END' *)
     C := C.RIGHT;
     C.LEFT := NONE;
     C.RIGHT := G;
     G.KIND := BEGKIND;
     G.IDENT := ENDKIND;
     U := NEW TNODE;                     
     G.LEFT := U;
     U.KIND := SEMKIND;                          (* SEMICOLON *)
     V := NEW TNODE;
     U.LEFT := V;
     V.KIND := BVARPRO;                          (* Q:=... *)
     V.IDENT := -LAST_Q-1;
     T := NEW TNODE;
     V.LEFT := T;
     T.KIND := CONKIND;                          (* CONJUNCTION *)
     S := NEW TNODE;
     T.LEFT := S;
     S.KIND := BVAKIND;                          (* Q *)
     S.IDENT := -LAST_Q-1;
     T.RIGHT := B;                               (* REFERS TO 'ALFA' *)
     U.RIGHT := D;                               (* REFERS TO PROGRAM 'K' *)
     T := NEW TNODE;
     G.RIGHT := T;
     T.KIND := CONKIND;                          (* CONJUNCTION *)
     U := NEW TNODE;
     T.LEFT := U;
     U.KIND := BVAKIND;                          (* Q *)
     U.IDENT := -LAST_Q-1;
     G := NEW TNODE;                             (* CONJUNCTION *)
     T.RIGHT := G;
     G.KIND := CONKIND;
     G.RIGHT := E;                               (* REFERS TO 'BETA' *)
     T := NEW TNODE;
     G.LEFT := T;
     T.KIND := NEGKIND;                          (* NEGATION *)
     T.LEFT := COPYTNODE ( B );                  (* OF 'ALFA' *)
     LAST_Q := LAST_Q+1;
     CALL MOVE ( M,P,P );
END RULEWHL;

(****************************************************************************)
(* SEARCH FOR A VARIABLE NUMBER I IN FORMULA AND CHANGE IT INTO SUBKIND *)

UNIT SEARCH_X : PROCEDURE ( A : TNODE , I : INTEGER );
BEGIN
   IF A <> NONE THEN
      IF A.IDENT = I AND A.KIND = VARKIND THEN 
         A.KIND := SUBKIND;
         A.IDENT := LAST_S;
      FI;
      CALL SEARCH_X ( A.LEFT , I );
      CALL SEARCH_X ( A.RIGHT , I );
   FI;
END SEARCH_X;

(*****************************************************************************)
(* BOTH RULES FOR QUANTIFIERS   AX-ALFA *)

UNIT RULEQUAN : PROCEDURE ( M : POINTER , P : INTEGER );
VAR A,C,C1,D,E,F : TNODE;
BEGIN
     IF P=0 THEN                                 (* QUAN ON LEFT SIDE *)
        IF LAST (M,0).NEXT = NONE THEN           (* BOTTOM LONGER THAN TOP *)
	   LAST (M,0).NEXT := COPYSEQUENT( LAST(M,0) );  (* COPY A QUANTIFIER *)
	   CALL ERASE ( LAST(M,0).PLEAF )     (* ERASE UPPER SIDE OF SEQUENT *)
	ELSE                                     (* OTHERWISE *)
	   LAST(M,1).NEXT := COPYSEQUENT( LAST(M,0) );  (* COPY A QUANTIFIER *)
	   CALL ERASE ( LAST(M,0).PLEAF );    (* ERASE UPPER SIDE OF SEQUENT *)
	FI;
     FI;
     CASE P
          WHEN 1: A := LAST (M,1).PLEAF;
          WHEN 0: A := LAST (M,0).LLEAF;
     ESAC;
     C := A;
     WHILE C.KIND=VARPROG OR C.KIND=BVARPRO
     DO
       C1 := C;                                  (* C1 POINTS TO LAST S *)
       C := C.RIGHT;                             (* C POINTS TO QUAN *)
     OD;
     D := NEW TNODE;                             (* NEW SUBSTITUTION *)
     D.KIND := VARPROG;                          (* S:=... *)
     LAST_S := LAST_S+1;   
     D.IDENT := LAST_S;
     F := NEW TNODE;                 
     D.LEFT := F;
     F.KIND := SUBKIND;                          (* ...:=Y *)
     IF LAST_X <= LAST_S THEN 
        LAST_X := LAST_S + 1
     ELSE 
        LAST_X := LAST_X + 1
     FI;
     F.IDENT := LAST_X;
     IF C1 = NONE THEN     
        A.RIGHT := D
     ELSE
        C1.RIGHT := D;
     FI;
     D.RIGHT := C.LEFT;                          (* REFERS TO FORMULA 'ALFA' *)
     CALL SEARCH_X ( C.LEFT , C.IDENT );         (* UPDATE NUMBERS OF BOUND *)
                                                 (* VARIABLE *)
     IF A.KIND = QUAKIND THEN 
        A.LEFT := NONE;
        CALL LIFT ( A , 1 , 1 );
	D := A
     ELSE 
        KILL ( C )
     FI;                                         (* ERASE QUANTIFIER TNODE *)
     
(* NEXT LINES ARE ONLY CONNECTED WITH THE LEFT SIDE QUANTIFIER *)

     IF P=0 THEN
        E := NEW TNODE;                          (* NEW SUBSTITUTION *)
	E.KIND := VARPROG;                       (* Y:=... *)
	E.IDENT := LAST_X; 	
	LAST_S := LAST_X; 	                 (* UPDATE NUMBER OF LAST *)
				                 (* SUBSTITUTION *)
	F := NEW TNODE;                          (* ...:=TERM *)
	E.LEFT := F;
	F.KIND := SIGNTRM;			 (* JOKER TERM *)
	LAST_D := LAST_D+1;
	F.IDENT := LAST_D;
	E.RIGHT := A;                            (* REFERS TO SUBSTITUTIONS *)
	LAST ( M , 0 ).LLEAF := E;
	CALL MOVE ( M , P , P );                 (* MOVES THE LAST SEQUENT *)
	                                         (* WITHOUT QUANTIFIER  *)   
	CALL SWEEP ( M.NEXT.LLEAF );
     FI;
     CALL MOVE ( M , P , P );                    (* MOVES SEQUENT *)
                        			 (* WITH QUANTIFIER *)
END RULEQUAN;

(***************************************************************************)
(* HELP FOR RULEITE - MAKE COPY AND INSERT IT DOWN TO CURRENT POINTER M  *)

UNIT K_MN_K_DOWN : PROCEDURE ( M : POINTER, E : TNODE );
VAR M2 : POINTER, 
    A1 : SEQUENT;
BEGIN
    M2 := NEW POINTER;
    M2.NEXT := COPYSEQUENT ( M.NEXT );
    M2.DOWN := M.DOWN;
    M.DOWN := M2;
    A1 := LAST ( M2 , 0 );
    CALL ERASE ( A1.LLEAF );
    A1.LLEAF := COPYTNODE ( E );               
    CALL SWEEP ( A1.LLEAF );
    CALL SQUEEZE ( M2 , 0 );
    CALL MOVE ( M2 , 0 , 0 )
END K_MN_K_DOWN;
 
(***************************************************************************)
(* ITERATIONAL QUANTIFIER CONNECTED WITH WHILE *)

UNIT RULEITE : PROCEDURE ( INOUT M : POINTER , LOGIC : BOOLEAN );
(* K_MN_K MEANS k IN Mn(k) *)

VAR A,B,C,D,E:TNODE,
    M2,M3:POINTER,
    A1,B2,F:SEQUENT,
    I:INTEGER;

BEGIN
     C := COPYTNODE ( LAST ( M , 0 ).LLEAF );
     E := C;					 (* E HOLDS BEGINNING OF Mn(0) *)
     WHILE C.KIND <> ITEKIND
     DO						 (* MAKE THE SAME IN FAKE TREE *)
       D := C;
       C := C.RIGHT;
     OD;					 (* C POINTS TO ITERATION *)
     A := COPYTNODE  ( E );     
     CALL LIFT ( C , 1 , 1);			 (* EXPELL ITERATION QUANTIFIER *)
     IF NOT LOGIC THEN
        B := A;
        WHILE B .KIND <> ITEKIND 
	DO 
	  B := B.RIGHT;
	OD;
	CALL LIFT ( B, 1, 1 );			 (* EXPELL ITERATION QUANTIFIER *)
        CALL ERASE ( B.LEFT );
	CALL LIFT ( B, 1, 1 ); 
        WHILE B.KIND <> CONKIND
	DO					 (* GO DOWN UNTIL C CONTAINS CONJUNCTION *)	  
          B := B.RIGHT;
        OD;
        M2 := NEW POINTER;			 (* CREATES NEW BRANCH *)
	M2.NEXT := COPYSEQUENT ( M.NEXT );
        M2.DOWN := M.DOWN;
        M.DOWN := M2;
	F := LAST ( M2 , 0 );
	CALL ERASE ( F.LLEAF );
	F.LLEAF := A;
        CALL SWEEP ( F.LLEAF );
        CALL SQUEEZE ( M2 , 0 );
     FI;
     IF NOT LOGIC OR K_MN_K=1 THEN 		 (* CONSTRUCT Mn(1) *)
        M2 := NEW POINTER;			 (* AND INSERT IT INTO *)
	M2.NEXT := COPYSEQUENT ( M.NEXT );	 (* THE SEQUENT *)
	F := LAST ( M2 , 0 );
	CALL ERASE ( F.LLEAF );
	F.LLEAF := COPYTNODE ( E );
	M2.DOWN := M.DOWN;
	M.DOWN := M2;
	CALL SWEEP ( F.LLEAF );
	CALL SQUEEZE ( M2 , 0 );
     FI;
     FOR I := 0 TO K_MN_K-2
     DO                    
     						 (* CREATE kMn(K_MN_K)ALFA *)
        B := C;            			 (* B POINTS TO BEGIN-END PROGRAM AFTER 'U' *)	 
        WHILE B.KIND <> CONKIND
	DO                                       (* GOES DOWN UNTIL B CONTAINS CONJUNCTION *)	  
          A := B;
          B := B.RIGHT;
        OD;					 (* B POINTS TO CONJUNCTION, A PRECEED B *)	  
        D := COPYTNODE ( C ); 			 (* D CONTAINS ONLY ONE PROGRAM K *)
						 (* AND CONJUCTION AS WELL *) 	  
	CALL ERASE ( A.RIGHT );
        A.RIGHT := D;
        C := D;
        IF NOT LOGIC THEN               	 (* LOGIC=TRUE MEANS THAT WHILE HAS *)
   	   CALL K_MN_K_DOWN ( M, E );		 (* ALREADY BEEN USED *)
        FI;
	
     OD;
     IF LOGIC AND K_MN_K > 1 THEN		 (* INSERT Mn(K) INTO *)
        CALL K_MN_K_DOWN ( M, E );
     FI;
     K_MN_K:=K_MN_K+1;
     						 (* PREPARE THREE NEW FORMULAS TO PROVE FOR 'WHILE' *)
     FOR I := 1 TO 3
     DO
           M3 := NEW POINTER;
	   SQNT := COPYSEQUENT ( LAST ( M.DOWN , 0 ) );
	   CALL ERASE_SEQ ( SQNT.NEXT );
	   CALL ERASE ( SQNT.PLEAF );
	   A := SQNT.LLEAF;
	   WHILE A.KIND <> CONKIND
	   DO
	     A := A.RIGHT;
	   OD;
	   CASE I
              WHEN 1 : CALL ERASE ( A.RIGHT );
	      	       CALL LIFT ( A , 1 , 0 );  (* M(l) p *)
              WHEN 2 : CALL ERASE ( A.LEFT );  	 (* M(l) NOT ALFA *)
	      	       CALL LIFT ( A , 1 , 1 );
		       CALL ERASE ( A.RIGHT );
		       CALL LIFT ( A , 1 , 0 );
              WHEN 3 : CALL ERASE ( A.LEFT );    (* M(l) BETA *)
	      	       CALL LIFT ( A , 1 , 1 );
		       CALL ERASE ( A.LEFT );
		       CALL LIFT ( A , 1 , 1 );
	   ESAC;  
	   M3.NEXT := SQNT;
	   CHI := TRUE; 
	   DIF := 1;				 (* VARIABLE DIF MEANS THAT *)
	   					 (* PROVE PROCEDURE WAS CALLED *)
 						 (* FROM WHILE *)	   
	   CALL PROVE ( M3 , DIF );              (* PROOF FOR M(l)p, *)
	                                         (* M(l)NOT ALFA, *)
	   					 (* AND M(l)BETA *)
	   CALL ERASE_PNTR ( M3 );	
	   					 (* IF ONE CAN PROVE CURRENT *)
						 (* SEQUENT E.G. Mn(l)p |- GENERATED *)
						 (* BY 'WHILE ' CHI IS NOT CHANGED *)
						 (* OTHERWISE CHI := FALSE IN PROVE *)
	   IF CHI THEN EXIT FI; 		 (* FINISHED PROOF BY M(l)p *)
	   					 (* OR M(l)NOT ALFA *)
						 (* OR BY M(l)BETA *)	   
      OD;
      IF CHI THEN
         CALL ERASE_SEQ ( M.NEXT );
	 CALL LIFT_PNTR ( M );
         CALL ERASE_SEQ ( M.NEXT );
	 CALL LIFT_PNTR ( M );
      FI;
END RULEITE;

(****************************************************************************)
(* RULE FOR ITERATION QUANTIFIERS *)

UNIT RULE_EX_GEN:PROCEDURE(INOUT M:POINTER;P,K_MN_K:INTEGER,C:TNODE,LOGIC:BOOLEAN);
VAR I : INTEGER,
    A,B,C2,D : TNODE,
    A2 : SEQUENT,
    M3,M2 : POINTER;
BEGIN
     IF C.RIGHT.KIND = BEGKIND ANDIF C.RIGHT.LEFT <> NONE ANDIF
         C.RIGHT.LEFT.LEFT <> NONE ANDIF C.RIGHT.LEFT.LEFT.IDENT < 0 THEN
        CALL RULEITE ( M , LOGIC );		 (* WHILE - ITERATION *)
        LOGIC := TRUE;
        RETURN;
     FI;
     A2 := COPYSEQUENT ( M.NEXT );                    
     M2 := NEW POINTER;                          (* CREATE NEW BRANCH *)
     M2.NEXT := A2;
     CASE P
          WHEN 0: A := LAST (M2,0).LLEAF;
          WHEN 1: A := LAST (M2,1).PLEAF;
     ESAC;     
     IF C.IDENT = 0 THEN                         (* THE FIRST STEP OF ITERATION *)
        CALL END_OF_S ( A,B );
        CALL LIFT ( A, 1, 1 );                   (* REMOVE ITERATION SIGN *)
	I := A.KIND;
        CALL ERASE ( A.LEFT );
	CALL LIFT ( A, 1, 1 );  		 (* REMOVE SUBSTITUTION OR *)
						 (* BEGINNING OF ANOTHER PROGRAM *)
	IF I <> VARPROG AND I <> BVARPRO THEN
   	   CASE A.KIND
	      WHEN WHIKIND : CALL ERASE ( A.LEFT );
	      		     CALL LIFT ( A,1,1 );
	      WHEN IFFKIND : CALL ERASE ( A.LEFT );
	      		     CALL LIFT ( A,1,1 );
			     CALL ERASE ( A.LEFT );
	      		     CALL LIFT ( A,1,1 );
	   ESAC;
	FI;
	C.IDENT := 1;
     ELSE	                                 (* NEXT STEPS OF ITERATION *)
        WHILE A.KIND=VARPROG OR A.KIND=BVARPRO   (* OMITS SUBSTITUTION *)
        DO
          D := A; 
          A := A.RIGHT;
        OD;
        A := A.RIGHT;                            (* A REFERS TO PROGRAM 'K' *)
        IF A.KIND=VARPROG OR A.KIND=BVARPRO THEN (* CONSISTING OF SUBSTITUTION *)
           C2 := COPYTNODE ( A );
	   CALL ERASE ( A.RIGHT );
           A.RIGHT := C2
        ELSE                                     (* OR ANOTHER PROGRAM *)
           D := A;
           WHILE A.IDENT<>ENDKIND AND A.IDENT<>ODFKIND AND A.IDENT<>FIFKIND
           DO
             A := A.RIGHT;
           OD;                                   (* A OMITS PROGRAM 'K' *)
           C2 := COPYTNODE ( D );
       	   CALL ERASE ( A.RIGHT );
           A.RIGHT := C2;
        FI;
     FI;	
     M3 := M2;                                   (* ITERATION PUSHED TO *)
     M2 := M;                                    (* THE END OF A TREE *)
     M := M3;
     M.DOWN := M2;
     CALL MOVE ( M , P , P );
END RULE_EX_GEN;

(****************************************************************************)
(* EXISTENTIAL ITERATION QUANTIFIER *)

UNIT RULEEXIST : PROCEDURE ( M : POINTER, C : TNODE, P : INTEGER );
VAR B,D,E : TNODE,
    A     : SEQUENT;
BEGIN
     B := C;
     E := COPYTNODE ( C.RIGHT );
     IF B.RIGHT.KIND=VARPROG OR B.RIGHT.KIND=BVARPRO THEN
        D := B.RIGHT.RIGHT;
        B.RIGHT.RIGHT := E
     ELSE
         WHILE B.IDENT<>FIFKIND AND B.IDENT<>ODFKIND AND B.IDENT<>ENDKIND
         DO
           B := B.RIGHT;
         OD;
         D := B.RIGHT;
         B.RIGHT := E;
     FI;
     CASE P
        WHEN 0 : IF LAST (M,0).NEXT = NONE THEN
                    LAST (M,0).NEXT  :=  COPYSEQUENT ( LAST(M,P) )
                 ELSE 
                    LAST (M,1).NEXT  :=  COPYSEQUENT ( LAST(M,P) )
                 FI;
		 E := FINDCONN ( LAST(M,0) , IGQKIND , 0 );
                 CALL ERASE ( LAST(M,0).PLEAF );
        WHEN 1 : IF LAST (M,1).NEXT = NONE THEN
                    LAST (M,1).NEXT  :=  COPYSEQUENT ( LAST(M,P) )
                 ELSE 
                    LAST (M,0).NEXT  :=  COPYSEQUENT ( LAST(M,P) )
                 FI;
		 E := FINDCONN ( LAST(M,1) , ITEKIND , 1 );
                 CALL ERASE ( LAST(M,1).LLEAF );
     ESAC;
     CALL ERASE ( E.RIGHT );
     E.RIGHT := D;
     CALL LIFT ( E , 1 , 1 );
     CASE P
          WHEN 0: CALL MOVE ( M , 0 , 0 );
                  CALL SWEEP ( M.NEXT.LLEAF );
                  CALL MOVE ( M , 0 , 0 );
          WHEN 1: CALL MOVE ( M , 1 , 1 );
                  CALL SWEEP ( M.NEXT.PLEAF ); 
                  CALL MOVE ( M , 1 , 1 );
     ESAC;
END RULEEXIST;

(****************************************************************************)
(* RULE FOR IF-ALFA-THEN-K-ELSE-M-FI-BETA OR WITHOUT 'ELSE' PROGRAM *)

UNIT RULEIF : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
VAR B,D,E,G,H,K : TNODE;
BEGIN
     B := C.LEFT;                                (* HOLD 'ALFA' *)
     C.LEFT := NONE;
     D := C.RIGHT.RIGHT.RIGHT;                   (* HOLD BETA *)
     C.RIGHT.RIGHT.RIGHT := NONE;
     IF C.RIGHT.RIGHT.KIND <> ELSKIND THEN       (* WITHOUT 'ELSE' *)
        C.LEFT := B;                             (* REFERS TO 'ALFA' *)
        C.KIND := CONKIND;
	C := C.RIGHT;
	CALL LIFT ( C , 1 , 0 );                 (* THROW 'THNKIND' *)
	CALL END_OF_PRG ( C );                   (* GO TO THE END OF 'K' *)
	C.RIGHT := D                             (* REFERS TO 'BETA' *)
     ELSE                                        (* WITH 'ELSE' *)
        C.KIND := DISKIND;          
	G := NEW TNODE;
        G.KIND := CONKIND;
	C.LEFT := G;
	G.LEFT := B;                             (* REFERS TO 'ALFA' *)
	K := C.RIGHT.RIGHT.LEFT;                 (* HOLD PROGRAM 'M' *)
	E := C.RIGHT;
	KILL ( E.RIGHT );
	CALL LIFT ( E , 1 , 0 );                 (* THROW 'THNKIND' *)
	G.RIGHT := E;
	CALL END_OF_PRG ( G );                   (* GO TO THE END OF 'K' *)
	G.RIGHT := D;                            (* REFERS TO 'BETA' *)
        H := NEW TNODE;                          (* 2ND ARG OF DISJUNCTION *)
        C.RIGHT := H;
        H.KIND := CONKIND;
	G := NEW TNODE;
	G.KIND := NEGKIND;
	H.LEFT := G;
	G.LEFT := COPYTNODE ( B );               (* REFERS TO 'ALFA' *)
	H.RIGHT := K;
	CALL END_OF_PRG ( H );
	H.RIGHT := COPYTNODE ( D );              (* REFERS TO 'BETA' *)
	H := C.LEFT;				 (* CHANGE FORMULA *)
	C.LEFT := C.RIGHT;
	C.RIGHT := H;
      FI;
      CALL MOVE ( M , P , P );
END RULEIF;

(****************************************************************************)
(* RULE FOR IMPLICATION *)

UNIT RULEIMP : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
VAR U,V : TNODE,
    D   : SEQUENT;
BEGIN
     CASE P
          WHEN 1: D:= NEW SEQUENT;		 (* |- P => Q CONVERT TO *)
	          D.NEXT := M.NEXT;		 (* P |- Q *)
		  M.NEXT := D;
                  U := COPYTNODE ( LAST ( M,1 ).PLEAF );
		  D.LLEAF := U;
    	          CALL ERASE ( C.LEFT );
                  CALL LIFT ( C , 1 , 1 );
		  V := FINDCONN ( D, IMPKIND, 0 );
		  CALL ERASE ( V.RIGHT );
		  CALL LIFT ( V, 1, 0 );
		  CALL MOVE ( M, 1, 1 );
          WHEN 0: C.KIND := DISKIND;		 (* IMPLICATION CHANGE TO *)
                  U := NEW TNODE;		 (* DISJUNCTION *)
                  U.KIND := NEGKIND;
                  U.LEFT := C.LEFT;
                  C.LEFT := U;
                  CALL RULEDIS ( M , C , P );
     ESAC;
END RULEIMP;

(****************************************************************************)
(* RULE FOR EQUIVALENCE *)

UNIT RULEEQU : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
VAR T,U,V,W : TNODE;

BEGIN
  C.KIND := CONKIND;
  U := COPYTNODE ( C.LEFT );
  V := COPYTNODE ( C.RIGHT );
  W := NEW TNODE;
  T := NEW TNODE;
  W.KIND := IMPKIND;
  T.KIND := IMPKIND;
  W.LEFT := V;
  W.RIGHT := U;
  T.LEFT := C.LEFT;
  T.RIGHT := C.RIGHT;
  C.LEFT := W;
  C.RIGHT := T;
  CALL MOVE ( M , P , P );
END RULEEQU;

(*****************************************************************************)
(* MAKE SERIAL OR PARALLEL SUBSTITUTION ON ATOMS *)

UNIT SUBAT : PROCEDURE ( M : POINTER , P : INTEGER );
VAR A : SEQUENT,
    B : TNODE;
BEGIN
     A := LAST(M,P);
     IF A=NONE THEN RETURN FI;
     CASE P
          WHEN 1: B := A.PLEAF;
          WHEN 0: B := A.LLEAF;
     ESAC;
     IF B = NONE THEN RETURN FI;
     IF B.KIND = BEGKIND AND B.LEFT.IDENT <> 1 THEN RETURN FI;
     IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = LITKIND 
        OR B.RIGHT.KIND = EQUKIND ) THEN CALL BEG_SUB ( B ); RETURN FI;
     IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = BVARPRO
        OR B.RIGHT.KIND = VARPROG ) THEN CALL SER_INSERT ( B.RIGHT );RETURN 
     FI;
     CALL SER_INSERT ( B );
END SUBAT;

(*****************************************************************************)
(* DO SERIAL SUBSTITUTITON *)

UNIT SER_INSERT : PROCEDURE ( A : TNODE );
VAR B : TNODE;
BEGIN
    CALL END_OF_S ( A, B ); 			 (* GO TO LAST SUBSTITUTION *)
    IF B.RIGHT.KIND = BVAKIND THEN 
       CALL SERIAL_Q ( B, B.RIGHT )		 (* MAKE SERIAL SUBSTITUION *)
       						 (* FOR LOGICAL VARIABLES *)
    ELSE					 
       CALL SERIAL_SUB ( B, B.RIGHT ); 		 (* MAKE SERIAL SUBSTITUTION *)
    FI;						 (* FOR LITERALS OR EQUALITIES *)
    CALL ERASE ( B.LEFT );			 (* REMOVE TAU *)
    CALL LIFT ( B, 1, 1 );			 (* REMOVE SUBSTITUTION *)
END SER_INSERT;
 
(*****************************************************************************)
(* DO SERIAL SUBSTITUTION FOR ON LOGICAL VARIABLES - BVAKINS'S *)

UNIT SERIAL_Q : PROCEDURE ( C, D : TNODE );
BEGIN
    IF D = NONE THEN RETURN FI;
    IF D.IDENT = C.IDENT THEN
       D.LEFT := COPYTNODE ( C.LEFT );		 (* COPY TAU *)
       CALL LIFT ( D , 1 , 0 );			 (* REMOVE S *)
    FI;
END SERIAL_Q;

(*****************************************************************************)
(* CALLED BY SER_INSERT *)

UNIT SERIAL_SUB : PROCEDURE ( C,D : TNODE );
VAR E : TNODE;
BEGIN
    IF D = NONE THEN RETURN FI;
    IF ( D.KIND = SUBKIND OR D.KIND = BVAKIND ) AND D.IDENT = C.IDENT THEN
       E := D.RIGHT;				 (* STORE TEMPORARILY NEXT ARG *)
       D.LEFT := COPYTNODE ( C.LEFT );		 (* COPY TAU *)
       CALL LIFT ( D , 1 , 0 );			 (* REMOVE S *)
       D.RIGHT := E;				 (* LINK NEXT ARG *)
       CALL SERIAL_SUB ( C , D.RIGHT );		 (* SEARCH FOR NEXT SUBKIND *)
       RETURN;
    FI;
    CALL SERIAL_SUB ( C , D.LEFT );  
    CALL SERIAL_SUB ( C , D.RIGHT );
END SERIAL_SUB;

(****************************************************************************)
(* MOVES ALL ATOMS FROM THE END TO THE BEGINNING *)

UNIT RULEAT : PROCEDURE ( M : POINTER , P : INTEGER ; INOUT BET : BOOLEAN );
VAR A , B : SEQUENT;
BEGIN
     IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;
     A := M.NEXT;
     CASE P
          WHEN 0 : WHILE A <> NONE
                   DO
		     IF A.LLEAF <> NONE THEN 
                        IF A.LLEAF.KIND <> LITKIND AND A.LLEAF.KIND <> EQUKIND 
		           AND A.LLEAF.KIND <> LOGKIND AND
			   A.LLEAF.KIND <> BVAKIND THEN 
		           B := A 
		        FI;
		     FI;
                     A := A.NEXT;
                   OD;
          WHEN 1 : WHILE A <> NONE 
                   DO
		     IF A.PLEAF <> NONE THEN
                        IF A.PLEAF.KIND <> LITKIND AND A.PLEAF.KIND <> EQUKIND 
		           AND A.PLEAF.KIND <> LOGKIND AND 
			   A.PLEAF.KIND <> BVAKIND THEN 
		           B := A 
		        FI;
		     FI;
                     A := A.NEXT;
                   OD;
     ESAC;
     IF B = NONE THEN RETURN FI;
     WHILE B <> LAST ( M , P )
     DO
        CALL MOVE ( M , P , P );
     OD;
     BET := TRUE;
END RULEAT;

(****************************************************************************)
(* RULE FOR NEGATION *)

UNIT RULENEG : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
BEGIN
     CALL LIFT ( C , 1 , 0 );
     CALL MOVE ( M , P , 1 - P );
END RULENEG;

(****************************************************************************)
(* DIVIDE A SEQUENT INTO TWO PIECES AND DEPENDING ON 'S' RE-CONSTRUCT A LIST:
S=1-ONE LIST; S=0-TWO LISTS *)

UNIT BRANCH : PROCEDURE ( M : POINTER , P , R , S : INTEGER , C : TNODE );
VAR M2  : POINTER,
    A,B,D : SEQUENT,
    E,F,E1,F1 : TNODE;
BEGIN
     D := NEW SEQUENT;
     B := NEW SEQUENT;
     E := COPYTNODE( C.LEFT  );
     F := COPYTNODE( C.RIGHT );
     A := LAST ( M , P );
     CALL ERASE ( C );
     CASE P
       WHEN 0 : D.LLEAF := COPYTNODE ( A.LLEAF );
	        B.LLEAF := COPYTNODE ( A.LLEAF );
		E1 := B.LLEAF;
		CALL END_OF_PRG ( E1 );
		IF E1 <> NONE THEN
		   E1.RIGHT := E
		ELSE
		   B.LLEAF := E;
		FI;
		E1 := D.LLEAF;
		CALL END_OF_PRG ( E1 );
		IF E1 <> NONE THEN 
		   E1.RIGHT := F
		ELSE 
		   D.LLEAF := F;
		FI;
		CALL ERASE ( A.LLEAF );
       WHEN 1 : D.PLEAF := COPYTNODE ( A.PLEAF );
		B.PLEAF := COPYTNODE ( A.PLEAF );
		E1 := B.PLEAF;
		CALL END_OF_PRG ( E1 );
		IF E1 <> NONE THEN
		   E1.RIGHT := E
		ELSE
		   B.PLEAF := E;
		FI;
		E1 := D.PLEAF;
		CALL END_OF_PRG ( E1 );
		IF E1 <> NONE THEN 
		   E1.RIGHT := F
		ELSE 
		   D.PLEAF := F;
		FI;
		CALL ERASE ( A.PLEAF );
     ESAC;
     CASE S
          WHEN 0: D.NEXT := M.NEXT;
                  M2 := NEW POINTER;
                  M2.DOWN := M.DOWN;
                  M.DOWN := M2;
                  M2.NEXT := B;
                  M.NEXT := D;
                  B.NEXT := COPYSEQUENT ( D.NEXT );
          WHEN 1: B.NEXT := M.NEXT;
                  D.NEXT := B;
                  M.NEXT := D;
     ESAC;
END BRANCH;

(****************************************************************************)
(* RULE FOR CONJUNCTION *)

UNIT RULECON : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
BEGIN
     CALL BRANCH ( M,P,4,1-P,C );
     CASE P
          WHEN 1 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );
          WHEN 0 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );
     ESAC;
END RULECON;

(****************************************************************************)
(* RULE FOR DISJUNCTION *)

UNIT RULEDIS : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );
BEGIN
     CALL BRANCH ( M , P , 5 , P , C );
     CASE P
          WHEN 0 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );
          WHEN 1 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );
     ESAC;
END RULEDIS;

(*****************************************************************************)


(*****************************************************************************)
(* 			MAIN BODY OF THIS PROVER 			     *)
(*****************************************************************************)

(*****************************************************************************)
(* PROVE AND RETRIEVE AXIOMS OF ALL INPUT FORMULAS *)

UNIT PROVE : PROCEDURE ( INOUT M : POINTER; DIF : INTEGER );
VAR BETA : BOOLEAN;
BEGIN
  CALL SWEEP ( M.NEXT.PLEAF );
  CALL THROW_RUBBISH ( M );
  WHILE M <> NONE
  DO
    ALFA := FALSE;
    BETA := FALSE;
    WHILE CHECK_L_F_P ( M.NEXT )
    DO
      WRITELN("DR");
      CALL SHOW_SEQ ( M.NEXT );
      CALL PROVE_P ( M , 1 );
      CALL MAKE_ORDER ( M );
      CALL PROVE_P ( M , 0 );
      CALL MAKE_ORDER ( M );
      IF AX <> NONE THEN
        IF SEARCH_AXIOMS ( M ) THEN 
           CALL ERASE_SEQ ( M.NEXT );
	   BETA := TRUE;			 (* FOUND AXIOM *)
	   EXIT 
        FI;
      FI;
      ALFA := FALSE;
    OD; 
    write("*");
    WRITELN("SEQ");
    CALL SHOW_SEQ ( M.NEXT );
    IF AX = NONE THEN
       IF SEARCH_AXIOMS ( M ) THEN
          CALL ERASE_SEQ ( M.NEXT );
	  BETA := TRUE;
       FI;
    FI;
    IF AX <> NONE THEN 
      WRITELN( "AX");
      CALL SHOW_TREE ( AX.AXIOM );
      WRITELN("KONIEC");
    FI;
    IF BETA ORIF M.NEXT=NONE ORIF SEARCH_AXIOMS ( M ) THEN
       CALL LIFT_PNTR ( M );
       BETA := FALSE
    ELSE
       IF DIF<>1 THEN 
          WRITE("THERE IS NO MODEL TO PROVE THIS EQUIVALENCE");
          RAISE ENDRUN
       ELSE 
          CHI:=FALSE;
          RETURN 
       FI; 
    FI;
  OD;
  IF AX = NONE THEN WRITELN ( " THE FORMULA IS A THEOREM "); FI;
END PROVE;

(*****************************************************************************)
(* DO THE RULES FOR P - SIDE UNTIL IT HAS NO USE *)
 
UNIT PROVE_P : PROCEDURE ( INOUT M : POINTER; P : INTEGER );
VAR R,I : INTEGER,
    A   : TNODE,
    BET : BOOLEAN;
BEGIN
  R := 0;
  IF LAST ( M , P ) <> NONE THEN
     FOR I := 3 TO 13 
     DO
       IF FINDCONN ( LAST ( M , P ) , I , P ) <> NONE THEN
          R := I;
          EXIT
       FI;
     OD;
     IF R <> 0 THEN
        CALL RULES ( M, P, R )
     ELSE 
        CASE P
	   WHEN 0 : A := LAST ( M, P ).LLEAF;
	   WHEN 1 : A := LAST ( M, P ).PLEAF;
	ESAC;
        IF A.KIND = BEGKIND ANDIF A.LEFT.KIND = SEMKIND ANDIF
           A.LEFT.IDENT = 1 THEN
           IF A.RIGHT.KIND <> VARPROG  AND  A.RIGHT.KIND <> BVARPRO THEN
   	      CASE P
	         WHEN 1 : CALL RULEBEG ( M, A , P );
		 WHEN 0 : CALL RULEBEG ( M, A , P );
	      ESAC;
	      RETURN;
	   FI;
	FI;
	IF A.RIGHT <> NONE THEN
	 IF A.KIND = VARPROG ORIF A.KIND = BVARPRO ORIF A.RIGHT.KIND = VARPROG
	   ORIF A.RIGHT.KIND = BVARPRO THEN
           CALL SUBAT ( M, P );
	   CASE P 
	     WHEN 0 : CALL SWEEP ( LAST ( M, P ).LLEAF );
	     WHEN 1 : CALL SWEEP ( LAST ( M, P ).PLEAF );
	   ESAC;
	   CALL MOVE ( M, P, P );
	 FI;
	FI;
        BET := FALSE;
        CALL RULEAT ( M, P, BET );
        IF NOT BET AND DEF_LIT = 1 THEN
           M1 := M1.NEXT;
	   CASE M1.FUN_REL.KIND
  	      WHEN LITKIND : CALL RULEDF_L ( M, P, M1.FUN_REL.IDENT );
 	      WHEN EQUKIND : CALL RULEDF_F ( M, P, M1.FUN_REL.LEFT.IDENT );
	   ESAC;
	FI;
      FI;
   FI;
END PROVE_P;

(*****************************************************************************)
(* DO ORDER PROCEDURES IN WHOLE SEQUENT *)

UNIT MAKE_ORDER : PROCEDURE ( M : POINTER );
BEGIN
   IF M = NONE ORIF M.NEXT = NONE THEN RETURN FI;
   CALL SQUEEZE ( M, 0 );			 (* REMOVE HOLES *)
   CALL SQUEEZE ( M, 1 );			 
   CALL SWEEP ( M.NEXT.PLEAF );  		 (* MAKE SIMPLE OPERATION *)
   CALL SWEEP ( M.NEXT.LLEAF );
   CALL CLAS_AX ( M );				 (* SEARCH CLASSICAL AXIOMS *)
   CALL THROW_RUBBISH ( M );			 (* REMOVE SEQUENT CONTAINING *)
     						 (* LOGICAL CONSTANTS *)
   IF M.NEXT <> NONE THEN CALL CUT_SEQ ( M.NEXT ) FI;
      						 (* REMOVE EMPTY FORMULAS *)
END MAKE_ORDER;

(*****************************************************************************)
(* SEARCH EXTRA AXIOMS  *)

UNIT SEARCH_AXIOMS : FUNCTION ( INOUT M : POINTER ) : BOOLEAN;
BEGIN
     IF SEARCH_CN1 ( M.NEXT ) THEN 
        CALL END_OF_M ( M, M.NEXT );
        RETURN;
     FI;
     IF LOOK_NQ ( M, 0 ) OR LOOK_NQ ( M, 1 ) OR LOOK_IDE ( M.NEXT ) THEN
        RESULT := TRUE;
        CALL ERASE_SEQ ( M.NEXT );
     FI;
END SEARCH_AXIOMS;

(****************************************************************************)
(* SEARCH FOR FALSE CONSTANTS IN WHOLE SEQUENT *)

UNIT SEARCH_CN1 : FUNCTION ( A : SEQUENT ) : BOOLEAN;
VAR ALFA : BOOLEAN;
BEGIN
   WHILE A <> NONE 
   DO
     CALL FUNCHECK ( A.PLEAF, ALFA );
     CALL FUNCHECK ( A.LLEAF, ALFA );
     IF ALFA THEN 
        RESULT := TRUE;
	RETURN;
     FI;
     A := A.NEXT;
  OD;
END SEARCH_CN1;
     
(****************************************************************************)
(* SEARCH CLASSICAL AXIOMS *)

UNIT CLAS_AX : PROCEDURE ( M : POINTER );
VAR A, A1 : SEQUENT,
      AX1 : LIST_AXIOMS,
     ALFA : BOOLEAN;
BEGIN
   IF M.NEXT=NONE THEN RETURN FI;
     A := M.NEXT;
     WHILE A <> NONE
     DO						 (* SEARCH FOR THE IDENTICAL *)
       A1 := M.NEXT;
       IF A.PLEAF <> NONE THEN			 (* FORMULAS IN A SEQUENT *)
          WHILE A1 <> NONE			 
          DO					 (* ON BOTH SIDES *)
            IF A1.LLEAF <> NONE THEN             (* I.E. ...beta...|-...beta... *)
	       ALFA := TRUE;
               CALL COMPARE ( A.PLEAF, A1.LLEAF, ALFA);
               IF ALFA THEN
                  CALL ERASE_SEQ ( M.NEXT );	 (* WHEN FOUND - ERASE SEQUENT *)
                  RETURN;
               FI;
            FI;
            A1 := A1.NEXT;
          OD;
       FI;
       A := A.NEXT;
     OD;
     A := M.NEXT;
     WHILE A <> NONE
     DO
       A1 := M.NEXT;
       IF A.PLEAF <> NONE THEN
          WHILE A1 <> NONE
          DO
            IF A1.LLEAF <> NONE THEN
	      IF A.PLEAF.KIND = LITKIND OR A.PLEAF.KIND = EQUKIND THEN
               IF A.PLEAF.KIND=A1.LLEAF.KIND AND A.PLEAF.IDENT=A1.LLEAF.IDENT
               THEN
                  IF SYL_AXIOMS ( M , A1.LLEAF.LEFT , A.PLEAF.LEFT ) THEN
                     CALL ERASE_SEQ ( M.NEXT );
                     RETURN;
                  FI;
               FI;
	      FI;
            FI;
            A1 := A1.NEXT;
          OD;
       FI;
       A := A.NEXT;
     OD;
END CLAS_AX;

(****************************************************************************)
(* LOOK FOR AXIOM OF THE FORM Xi=Yi and P(X1,...,Xn) |- P(Y1,...,Yn)  *)

UNIT SYL_AXIOMS : FUNCTION ( M : POINTER, E, F : TNODE ) : BOOLEAN;
VAR          A : SEQUENT,
       B, C, D : TNODE,
    BETA, ALFA : BOOLEAN;
BEGIN
     WHILE E<>NONE AND F<>NONE
     DO
       B := COPYTNODE ( E );
       C := COPYTNODE ( F );
       CALL ERASE ( C.RIGHT );
       CALL ERASE ( B.RIGHT );
       B.RIGHT := C;				 (* CREATE PAIR Xi->Yi *)
       A := M.NEXT;
       WHILE A<>NONE 
       DO 
         IF A.LLEAF<>NONE ANDIF A.LLEAF.KIND=EQUKIND THEN
            D := A.LLEAF.LEFT;
	    ALFA := TRUE;
            CALL COMPARE ( D, B, ALFA );	 (* SEARCH FOR RESPECTIVE PAIR *)
            IF ALFA THEN
               BETA := TRUE;
               EXIT;
            FI;
         FI;
         A := A.NEXT;
       OD;
       CALL ERASE ( B );
       IF NOT BETA THEN RETURN FI;		 (* IF NOT FOUND THEN RESULT := FALSE *)
       E := E.RIGHT;				 (* SEARCH FURTHER *)
       F := F.RIGHT;				 (* FOR NEXT PAIR *)
     OD;
     RESULT := TRUE;
END SYL_AXIOMS;

(****************************************************************************)
(* LOOKING FOR NQ OR Q AXIOM *)

UNIT LOOK_NQ : FUNCTION ( M : POINTER, P : INTEGER ) : BOOLEAN;
VAR A   : SEQUENT,
    AX2 : LIST_AXIOMS,
      C : TNODE ;
BEGIN
     A := M.NEXT;
     WHILE A <> NONE
     DO						 (* VIEW WHOLE SEQUENT *)
     						 (* LOOKING FOR Q *)
       CASE P 
          WHEN 0 : IF A.LLEAF <> NONE THEN
	             IF A.LLEAF.KIND = BVAKIND THEN   (* FOUND Q ON LEFT SIDE *)
	  	      IF SRCH_Q_AX ( A.LLEAF.IDENT, AX2 ) THEN 
		         IF AX2.AXIOM.KIND = NEGKIND THEN
			    RESULT := TRUE;
			    RETURN
			 ELSE
			    RESULT := FALSE 	 (* FOUND NEGATION OF EXISTED *)
			    			 (* AXIOM Q *)
			 FI
		      ELSE			 (* AXIOM NOT FOUND *)
		         AX2 := MAKE_AXIOM ( AX );
			 IF AX = NONE THEN AX := AX2 FI;
     		         C := NEW TNODE;	 (* AXIOM := NOT Q *)
 		         C.KIND := NEGKIND;
		         C.LEFT := COPYTNODE ( A.LLEAF );
		         AX2.AXIOM := C;         
		         RESULT := TRUE;
		         RETURN;       
		      FI;
		     FI;
		   FI;
	  WHEN 1 : IF A.PLEAF <> NONE THEN
	             IF A.PLEAF.KIND = BVAKIND THEN   (* FOUND Q ON RIGHT SIDE *)
	  	      IF SRCH_Q_AX ( A.PLEAF.IDENT, AX2 ) THEN 
		         IF AX2.AXIOM.KIND = NEGKIND THEN
			    RESULT := FALSE;	 (* FOUND NEGATION OF EXISTED *)
			    			 (* AXIOM Q *)
			 ELSE
			    RESULT := TRUE;	 (* FOUND CORRECT AXIOM *)
			 FI
		      ELSE			 (* AXIOM NOT FOUND *)
			 AX2 := MAKE_AXIOM ( AX );
			 IF AX = NONE THEN AX := AX2 FI;
		         AX2.AXIOM := COPYTNODE ( A.PLEAF );         
		         RESULT := TRUE;
		      FI;
		      RETURN;
		     FI;
		   FI;
       ESAC;
       A := A.NEXT;
     OD;
END LOOK_NQ;

(*****************************************************************************)
(* SEARCH FOR A BVAKIND IN THE SET OF AXIOMS *)

UNIT SRCH_Q_AX : FUNCTION ( N : INTEGER; INOUT AX2 : LIST_AXIOMS ) : BOOLEAN;
BEGIN
   AX2 := AX;
   WHILE AX2 <> NONE 
   DO
     IF AX2.AXIOM.KIND = BVAKIND AND AX2.AXIOM.IDENT = N THEN
        RESULT := TRUE;
	RETURN
     ELSE
        IF AX2.AXIOM.KIND = NEGKIND ANDIF AX2.AXIOM.LEFT.KIND = BVAKIND
	   AND AX2.AXIOM.LEFT.IDENT = N THEN
	   RESULT := TRUE;
	   RETURN;
	FI;
     FI;
     AX2 := AX2.NEXT;
   OD;
   RESULT := FALSE;
END SRCH_Q_AX;

(*****************************************************************************)
(* CREATE A NEW AXIOM *)

UNIT MAKE_AXIOM : FUNCTION ( AX1 : LIST_AXIOMS ) : LIST_AXIOMS ;
BEGIN
   IF AX1 = NONE THEN
      RESULT := NEW LIST_AXIOMS;
   ELSE
      CALL END_OF_AX ( AX1 );
      AX1.NEXT := NEW LIST_AXIOMS;
      RESULT := AX1.NEXT;
   FI;
END MAKE_AXIOM;

(*****************************************************************************)
(* LOOKING FOR IDENTITY AXIOM U=TAU *)

UNIT LOOK_IDE:FUNCTION ( A : SEQUENT ) : BOOLEAN;
VAR AX1 : LIST_AXIOMS,
    ALFA : BOOLEAN;
BEGIN
     WHILE A <> NONE 
     DO
        IF A.PLEAF <> NONE ANDIF A.PLEAF.KIND = EQUKIND ANDIF 
           ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND )
        THEN 			 	  	 (* FOUND U=TAU *)
	  CALL FUNCHECK ( A.PLEAF, ALFA );
	  IF NOT ALFA THEN 
           AX1 := AX;
	   RESULT := TRUE;
           WHILE AX1 <> NONE
           DO
	      ALFA := TRUE;
              CALL COMPARE ( A.PLEAF, AX1.AXIOM, ALFA );
              IF ALFA THEN RETURN FI;		 (* THIS AXIOM HAS ALREADY *)
              AX1 := AX1.NEXT;			 (* BEEN WRITTEN TO THE LIST *)
           OD;
	   IF SEARCH_U ( A ) THEN 
              CALL END_OF_M ( M, A );
	      RETURN;
	   FI;
	   CALL END_OF_AX ( AX1 );		 (* AXIOM NOT FOUND *)
	   IF AX = NONE THEN 
	      AX1 := NEW LIST_AXIOMS;
	      AX := AX1
	   ELSE
    	      AX1.NEXT := NEW LIST_AXIOMS;	 (* SO, THE LIST MUST BE *)
	      AX1 :=AX1.NEXT;
	   FI;
	   AX1.AXIOM := COPYTNODE ( A.PLEAF );	 (* UPDATED *)
           RETURN
	 ELSE
	   ALFA := FALSE
	 FI;
	FI;
	A := A.NEXT;   
     OD;
END LOOK_IDE;

(*****************************************************************************)


(*****************************************************************************)
(* 			      OUTPUT OF AXIOMS 				     *)
(*****************************************************************************)

(*****************************************************************************)
(* PRINTS ALL LIST OF AXIOMS *)

UNIT SHOW_AX : PROCEDURE ( AX1 : LIST_AXIOMS );
BEGIN
    IF AX1 <> NONE THEN
       CALL SHOW_TREE ( AX1.AXIOM );
       CALL SHOW_AX ( AX1.NEXT );
    FI;
END SHOW_AX;
      
(****************************************************************************)
(* WRITES AXIOMS *)

UNIT WRITE_AXIOMS : PROCEDURE;
VAR AX1 : LIST_AXIOMS;
BEGIN
   AX1 := AX;
   IF AX = NONE THEN 
      WRITE ( "IT IS TRUE WITHOUT ADDITIONAL AXIOMS" ); 
      RETURN 
   FI;
   WHILE AX1 <> NONE 
   DO 
     IF AX1.AXIOM.KIND = EQUKIND THEN
        WRITE (" U = ");
        IF AX1.AXIOM.LEFT.KIND = VRUKIND THEN
  	   CALL WRITE_EXPR ( AX1.AXIOM.LEFT.RIGHT )
        ELSE
	   CALL WRITE_EXPR ( AX1.AXIOM.LEFT );
        FI
     ELSE
        CASE AX1.AXIOM.KIND
	  WHEN 7  : CALL PUTCH ( 'Q' );
		    CALL PNUM ( AX1.AXIOM.LEFT.IDENT );
		    WRITE ( " <=> FALSE" );
          WHEN 33 : CALL PUTCH ( 'Q');
	            CALL PNUM ( AX1.AXIOM.IDENT );
		    WRITE ( " <=> TRUE" );
        ESAC
      FI;
      AX1 := AX1.NEXT;
      WRITELN;
    OD;
    CALL ERASE_AX ( AX );
END WRITE_AXIOMS;    
      
(****************************************************************************)
(* PRINT BRACKETS *)
 	
UNIT PUT_BRACKET : PROCEDURE ( C : TNODE );
VAR K : INTEGER;
BEGIN
    K := C.KIND;
    IF K=LITKIND ORIF K=FUNKIND ORIF K=42 ORIF K=43
       ORIF K=47 ORIF K=45 ORIF K=94 THEN
       CALL PUTCH ( '(' );
       CALL WRITE_EXPR ( C );
       CALL PUTCH ( ')' )
    ELSE
       CALL WRITE_EXPR ( C );
    FI;
END PUT_BRACKET;

(****************************************************************************)
(* PRINT TERM *)

UNIT WRITE_EXPR : PROCEDURE ( C : TNODE );
BEGIN
     IF C=NONE THEN RETURN FI;
     CASE C.KIND
       WHEN CN2KIND:CALL PUTCH ( 'C' );
       		    CALL PNUM ( C.IDENT );
                    RETURN;
       WHEN CNTKIND:CALL PNUM ( C.IDENT + 1 );
                    RETURN;
       WHEN LITKIND:CALL PUTCH ( 'P' );
                    CALL PNUM ( C.IDENT );
		    C := C.LEFT;
		    IF C <> NONE THEN 
		       CALL PUTCH ( '(' );
		    FI;
		    RETURN;
       WHEN FUNKIND:CALL PUTCH ( 'F' );
                    CALL PNUM ( C.IDENT );
                    IF C.LEFT <> NONE THEN 
		       CALL PUTCH ( '(' );
       		       CALL WRITE_EXPR ( C.LEFT );  
		    FI;
		    C := C.RIGHT;
		    IF C = NONE THEN 
		       CALL PUTCH ( ')' )
		    ELSE 
		       CALL PUTCH ( ',' );
		    FI;
		    RETURN;
	WHEN ARIKIND:
  	 CASE C.IDENT
    	   WHEN 42 :CALL PUT_BRACKET ( C.LEFT );
	            CALL PUTCH ( '*' );
		    CALL PUT_BRACKET ( C.LEFT.RIGHT );
		    RETURN;
           WHEN 43 :CALL PUT_BRACKET ( C.LEFT );
	            CALL PUTCH ( '+' );
		    CALL PUT_BRACKET ( C.LEFT.RIGHT );
		    RETURN;	
	   WHEN 45 :CALL PUT_BRACKET ( C.LEFT );
	            CALL PUTCH ( '-' );
		    CALL PUT_BRACKET ( C.LEFT.RIGHT );
		    RETURN;	
           WHEN 47 :CALL PUT_BRACKET ( C.LEFT );
	            CALL PUTCH ( '/' );
		    CALL PUT_BRACKET ( C.LEFT.RIGHT );
		    RETURN;    
           WHEN 94 :CALL PUT_BRACKET ( C.LEFT );
	            CALL PUTCH ( '^' );
		    CALL PUT_BRACKET ( C.LEFT.RIGHT );
                    RETURN;
        ESAC;
     ESAC;
END WRITE_EXPR;

(****************************************************************************)
(* PRINT NUMBER WITHOUT SPACES OR ZEROS CONTROLLING END OF LINE *)
     		 
UNIT PNUM : PROCEDURE ( N : INTEGER );
VAR I:INTEGER;
BEGIN
   N := N-1;
   IF N > -1 THEN
      I := 1;
      IF N>9 THEN I := I+1 FI;
      IF N>99 THEN I := I+1 FI;
      IF N>999 THEN I := I+1 FI;
      IF N>9999 THEN I := I+1 FI;
      IF CHARSH+1>LINLNG THEN WRITELN; CHARSH := 0 FI;
      IF CHARSH=0 THEN WRITE(' '); FI;
      WRITE ( N:I );
      CHARSH := CHARSH+1;
   FI;
END PNUM;

(****************************************************************************)
(* SERVES SPECIAL EXCEPTIONS - HARD EXIT FROM PROGRAM *)

SIGNAL ENDRUN;
HANDLERS
   WHEN ENDRUN: TERMINATE;
END HANDLERS;

(****************************************************************************)

BEGIN
   L := 0;
   OPEN ( G , TEXT , UNPACK ( "RETRPROV.DAT" ) );
   M := NEW POINTER;
   SQNT := NEW SEQUENT;
   M.NEXT := SQNT;
   CALL RESET ( G );
   SQNT.PLEAF := GEN_TREE;
   CALL LAST1_S ( SQNT.PLEAF );
   CALL LAST1_X ( SQNT.PLEAF );
  (* M contains f(t1,...,tn)=u or relation *)
  WRITELN ( "PROVE WITH DEFINITION    ------- 1 " );
  WRITELN ( "PROVE WITHOUT DEFINITION ------- 2 " );
  READ ( DEF_LIT );
  IF DEF_LIT = 1 THEN 
   (* M1 contains f(x1,...,xn)=Ktau  or relation *)
   OPEN ( G , TEXT , UNPACK ( "RETRPROV.DEF" ) );
   M1 := NEW DEF;
   M1.NEXT := M1;
   CALL RESET ( G );
   L := 0;
   M1.FUN_REL := GEN_TREE;
   CALL LAST1_S ( M1.FUN_REL );
   CALL LAST1_X ( M1.FUN_REL );
   CALL REP_F_L ( M1 );				 (* FUNKIND -> FN1KIND *)
   						 (* LITKIND -> LT1KIND *)
   CALL RULEDF_L ( M , 1 , M1.FUN_REL.LEFT.IDENT );
   CALL RULEDF_F ( M , 1 , M1.FUN_REL.LEFT.IDENT );  
  FI;
  K_MN_K := 2;
  LOGIC := FALSE;
  CALL PROVE ( M , 0 );
  CALL WRITE_AXIOMS;
END RETRPROV; 

(****************************************************************************)