examples/biela/r.log

   1 PROGRAM RETRPROV;\r
   2 \r
   3 (****************************************************************************  \r
   4 *                                                                           *  \r
   5 *            RETRIEVAL P R O V E R LOOKING FOR AXIOMS                       *  \r
   6 *                       All rights reserved                                 *  \r
   7 *                                                                           *\r
   8 ****************************************************************************)\r
   9 \r
  10 \r
  11 \r
  12 \r
  13 \r
  14 (***************************************************************************)\r
  15 (* CONSTANTS, VARIABLES AND OBJECTS USED IN PROGRAM                        *)\r
  16 (***************************************************************************)\r
  17 \r
  18 (* CONST *)\r
  19 \r
  20 CONST\r
  21 \r
  22 (* CHARACTER CODES <IN ASCII> *)\r
  23 \r
  24 CHRNEG = 78,    (* NEGATION 'N' *)\r
  25 CHREQU = 69,    (* EXISTENTIAL QUANTIFIER : 'E' *)\r
  26 CHRITG = 64,    (* ITERATION GREAT QUANTIFIER: '@' *)   \r
  27 CHRGQU = 65,    (* GLOBAL QUANTIFIER : 'A' *) \r
  28 CHRITE = 85,    (* EXISTENTIAL ITERATION QUANTIFIER: 'U' *)   \r
  29 CHROR  = 86,    (* DISJUNCTION : 'V' *)   \r
  30 CHRAND = 38,    (* CONJUNCTION : '&' *)   \r
  31 CHRCOM = 44,    (* COMMA *)   \r
  32 CHRLPA = 40,    (* LEFT PARENTHESIS *)\r
  33 CHRRPA = 41,    (* RIGHT PARENTHESIS *)   \r
  34 CHRBLK = 32,    (* BLANK *)   \r
  35 CHREND = 63,    (* FORMULA TERMINATOR : '?' *)\r
  36 CHRCRT = 10,    (* CARRIAGE RETURN *) \r
  37 CHREQS = 61,    (* "EQUALS" SIGN - FOR IMPLICATION *) \r
  38 CHRGTR = 62,    (* "GREATER" SIGN - ALSO FOR IMPLICATION *)   \r
  39 CHRLSS = 60,    (* "<" -SIGN FOR EQUIVALENCE *)   \r
  40 \r
  41 (* FORMULA NODE TYPES *)\r
  42 \r
  43 LOGKIND = 01,   (* LOGICAL CONSTANT *)\r
  44 VARKIND = 02,   (* VARIABLE *)\r
  45 EQVKIND = 03,   (* EQUIVALENCE *) \r
  46 CONKIND = 04,   (* CONJUNCTION *) \r
  47 DISKIND = 05,   (* DISJUNCTION *) \r
  48 IMPKIND = 06,   (* IMPLICATION *) \r
  49 NEGKIND = 07,   (* NEGATION *)\r
  50 IGQKIND = 08,   (* ITERATION GREAT QUANTIFIER *)  \r
  51 ITEKIND = 09,   (* ITERATION EXISTENTIAL QUANTIFIER *)\r
  52 IFFKIND = 10,   (* BRANCHING *)   \r
  53 BEGKIND = 11,   (* BEGINNING OF A COMPOSITION *)  \r
  54 WHIKIND = 12,   (* CONDITIONAL ITERATION *)   \r
  55 QUAKIND = 13,   (* QUANTIFIER *)  \r
  56 ENDKIND = 14,   (* END OF COMPOSITION *)  \r
  57 THNKIND = 15,   (* POSITIVE CHOICE *) \r
  58 ELSKIND = 16,   (* NEGATIVE CHOICE *) \r
  59 FIFKIND = 17,   (* END OF BRANCHING *)\r
  60 DOFKIND = 18,   (* POSITIVE CONDITIONAL ITERATION *)  \r
  61 ODFKIND = 19,   (* END OF CONDITIONAL ITERATION *)\r
  62 SEMKIND = 20,   (* SEMICOLON *)   \r
  63 VARPROG = 21,   (* SUBSTITUTION FOR TERMS X:=TERM *)  \r
  64 BVARPRO = 22,   (* SUBSTITUTION FOR BOOLEAN VARIABLE A:=FORMULA *)\r
  65 LITKIND = 23,   (* LITERAL *) \r
  66 LT1KIND = 24,   (* RELATION DEFINED BY PROCEDURE *)\r
  67 FUNKIND = 25,   (* FUNCTION OR CONSTANT *)\r
  68 FN1KIND = 26,   (* FUNCTION DEFINED BY PROCEDURE *) \r
  69 CNTKIND = 27,   (* CONSTANT - NUMBER *)   \r
  70 CN1KIND = 28,   (* FALSE CONSTANT *)  \r
  71 VRUKIND = 29,   (* SPECIAL KIND OF VARIABLE - U *)\r
  72 SUBKIND = 30,   (* VARIABLE TO BE SUBSTITUTED ON *)   \r
  73 CN2KIND = 31,   (* CONSTANT -NOT NUMBER -OF THE FORM N *) \r
  74 ARIKIND = 32,   (* ARITHMETIC OPERATORS *)\r
  75 BVAKIND = 33,   (* LOGICAL VARIABLE TO BE SUBSTITUTED ON *)\r
  76 EQUKIND = 34,   (* EQUALITY *)\r
  77 SIGNTRM = 35,   (* TRACE OF TERM *)\r
  78 \r
  79 LINLNG  = 80;\r
  80 \r
  81 UNIT TNODE:CLASS;   \r
  82 VAR KIND,IDENT:INTEGER, \r
  83     LEFT,RIGHT:TNODE;   \r
  84 END;\r
  85 \r
  86 UNIT SEQUENT:CLASS; \r
  87 VAR PLEAF,LLEAF:TNODE,  \r
  88     NEXT:SEQUENT;   \r
  89 END;\r
  90 \r
  91 UNIT POINTER:CLASS; \r
  92 VAR NEXT:SEQUENT,   \r
  93     DOWN:POINTER,   \r
  94     USED:INTEGER;   \r
  95 END;\r
  96 \r
  97 UNIT LIST_TERM:CLASS;   \r
  98 VAR T:TNODE,\r
  99     NEXT:LIST_TERM; \r
 100 END;\r
 101 \r
 102 UNIT LIST_AXIOMS:CLASS; \r
 103 VAR AXIOM:TNODE,\r
 104     NEXT:LIST_AXIOMS;   \r
 105 END;\r
 106 \r
 107 UNIT DEF : CLASS;\r
 108 VAR FUN_REL : TNODE,\r
 109     NEXT : DEF;\r
 110 END;\r
 111 \r
 112 VAR M : POINTER,   \r
 113     M1 : DEF,\r
 114     TERM:LIST_TERM, \r
 115     AX:LIST_AXIOMS, \r
 116     SQNT:SEQUENT,   \r
 117     G:FILE, \r
 118     ALFA:BOOLEAN,\r
 119     DEF_LIT : INTEGER,\r
 120     EQU_NUMBER:INTEGER,      (* CURRENT EQUATION *) \r
 121     K_MN_K:INTEGER,          (* CURRENT NUMBER OF ITERATIONS *) \r
 122     LAST_S:INTEGER,          (* MAXIMAL NUMBER OF VARPROG *)\r
 123     LAST_Q:INTEGER,          (* MAXIMAL NUMBER OF BVARPRO *)\r
 124     LAST_X:INTEGER,          (* MAXIMAL NUMBER OF VARKIND *)\r
 125     LAST_D:INTEGER,          (* MAXIMAL NUMBER OF TERM SIGN *)\r
 126     C,PEEKCH:INTEGER,        (* CODES OF CURRENT CHAR FROM INPUT FILE *)\r
 127     L:INTEGER,               (* NUMBER OF LAST READ CHAR FROM INPUT FILE *) \r
 128     CHARSH:INTEGER,          (* CURRENT NUMBER IN LINE *)   \r
 129     DIF:INTEGER,             (* DISTINGUISH KINDS OF FORMULAS TO PROVE *)   \r
 130     CHI:BOOLEAN,             (* SHOW IF FORMULA FROM WHILE WAS PROVED  *)   \r
 131     LOGIC:BOOLEAN,           (* TELLS WHETHER WHILE HAS ALREADY BEEN USED *)\r
 132     LL,LR:INTEGER;           (* COUNTS LEFT AND RIGHT PROGRAM BRACKETS *)    \r
 133     \r
 134 (***************************************************************************)\r
 135 \r
 136 \r
 137 (***************************************************************************)\r
 138 (*                     GENERATE TREE OF THE FORMULA                        *)\r
 139 (***************************************************************************)\r
 140   \r
 141 (***************************************************************************)\r
 142 (* LOOKS AT NEXT NON-BLANK ON INPUT *)  \r
 143 \r
 144 UNIT PNC:FUNCTION:INTEGER;  \r
 145 VAR D : CHARACTER;  \r
 146 BEGIN   \r
 147    PEEKCH:=0;\r
 148 (* FILL PEEKCHAR IGNORING BLANKS AND CR'S *)  \r
 149    WHILE PEEKCH=0 OR  PEEKCH=CHRBLK OR PEEKCH=CHRCRT \r
 150    DO\r
 151      READ(G,D);  \r
 152      PEEKCH:=ORD(D);\r
 153      L:=L+1;  \r
 154    OD;   \r
 155    RESULT := PEEKCH; \r
 156 END PNC;\r
 157 \r
 158 (****************************************************************************)  \r
 159 (* MOVES FORWARD N STEPS AND READS CHARACTER *) \r
 160 \r
 161 UNIT LOOKN:PROCEDURE(N:INTEGER);\r
 162 VAR I:INTEGER;  \r
 163 BEGIN   \r
 164    FOR I:=1 TO N\r
 165    DO   \r
 166      C:=PNC;  \r
 167    OD;  \r
 168 END LOOKN;  \r
 169 \r
 170 (****************************************************************************)  \r
 171 (* READS N-TH POSITION IN FILE *)   \r
 172 UNIT RETN:PROCEDURE(N:INTEGER); \r
 173 VAR I:INTEGER;  \r
 174 BEGIN   \r
 175    L:=0;\r
 176    CALL RESET(G);   \r
 177    FOR I:=1 TO N\r
 178    DO   \r
 179      C:=PNC;   \r
 180    OD;  \r
 181 END RETN;   \r
 182 \r
 183 (****************************************************************************)  \r
 184 (* DISTINGUISH PROGRAMS WRITTEN IN LOGLAN *)\r
 185 \r
 186 UNIT PRKEY : FUNCTION(N:INTEGER) : INTEGER; \r
 187 VAR V,W : ARRAYOF CHARACTER,\r
 188     I,C : INTEGER;  \r
 189 BEGIN   \r
 190    ARRAY V DIM(1:26);\r
 191    ARRAY W DIM(1:N); \r
 192    V(1):='I';V(2):='F';V(3):='T';V(4):='H';V(5):='E';V(6):='N';\r
 193    V(7):= 'L'; V(8):= 'S'; V(9):= 'B'; V(10):= 'G'; V(11):= 'D'; \r
 194    V(12):= 'W'; V(13):= 'O';V(14):= 'i'; V(15):= 'f'; V(16):= 't';   \r
 195    V(17):= 'h'; V(18):= 'e'; V(19):= 'n'; V(20):= 'l'; V(21):= 's';  \r
 196    V(22):= 'b'; V(23):= 'g'; V(24):= 'd'; V(25):='w'; V(26):= 'o';   \r
 197    FOR I:=1 TO N \r
 198    DO \r
 199      IF NOT EOF(G) THEN \r
 200         C:=PNC \r
 201      ELSE \r
 202         RESULT:=0;\r
 203         L:=L+N-I+1;\r
 204         RETURN;\r
 205      FI;           \r
 206      W(I):=CHR(C); \r
 207    OD; \r
 208    CASE N\r
 209    WHEN  \r
 210        2:IF V(1) = W(1) OR V(14) = W(1) THEN \r
 211             IF V(2) = W(2) OR V(15) = W(2) THEN RESULT:=1 FI   (* 'IF' *)\r
 212          FI;\r
 213          IF V(2) = W(1) OR V(15) = W(1) THEN \r
 214             IF V(1) = W(2) OR V(14) = W(2) THEN RESULT:=2 FI   (* 'FI' *)\r
 215          FI;\r
 216          IF V(11) = W(1) OR V(24) = W(1) THEN\r
 217             IF V(13) = W(2) OR V(26) = W(2) THEN RESULT:=3 FI  (* 'DO' *)\r
 218          FI;   \r
 219          IF V(13) = W(1) OR V(26) = W(1) THEN\r
 220             IF V(11) = W(2) OR V(24) = W(2) THEN RESULT:=4 FI  (* 'OD' *)\r
 221          FI;   \r
 222     WHEN\r
 223         3:IF V(5) = W(1) OR V(18) = W(1) THEN \r
 224              IF ((V(6) = W(2)) OR (V(19) = W(2))) AND ((V(11)=W(3)) \r
 225                  OR (V(24)=W(3)))  THEN RESULT:=5 FI           (* 'END' *)\r
 226           FI;   \r
 227     WHEN\r
 228         4:IF V(3) = W(1) OR V(16) = W(1) THEN \r
 229              IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(5)=W(3))\r
 230                 OR (V(18)=W(3))) THEN\r
 231                 IF V(6) = W(4) OR V(19) = W(4) THEN RESULT:=6 FI (* 'THEN' *) \r
 232              FI\r
 233           FI;\r
 234           IF V(5) =  W(1) OR V(18) = W(1) THEN\r
 235              IF ((V(7) = W(2)) OR (V(20)=W(2))) AND ((V(8)=W(3)) \r
 236                 OR (V(21)=W(3))) THEN IF V(5) = W(4) OR V(18) = W(4) THEN \r
 237                                          RESULT:=7 FI            (* 'ELSE' *)\r
 238              FI\r
 239           FI;\r
 240      WHEN\r
 241          5:IF V(9) = W(1) OR V(22) = W(1) THEN \r
 242               IF ((V(5) = W(2)) OR (V(18)=W(2))) AND ((V(10)=W(3)) \r
 243                  OR (V(23)=W(3))) THEN \r
 244                    IF ((V(1)=W(4)) OR (V(14)=W(4))) AND ((V(6)=W(5)) \r
 245                      OR (V(19)=W(5))) THEN RESULT:=8 FI        (* 'BEGIN' *)   \r
 246               FI\r
 247             FI;\r
 248             IF V(12) = W(1) OR V(25) = W(1) THEN\r
 249                IF ((V(4) = W(2)) OR (V(17)=W(2))) AND ((V(1)=W(3))\r
 250                   OR (V(14)=W(3))) THEN \r
 251                     IF ((V(7)=W(4)) OR (V(20)=W(4))) AND ((V(5)=W(5)) \r
 252                        OR (V(18)=W(5))) THEN RESULT:=9         (* 'WHILE' *)\r
 253                     FI \r
 254                 FI;\r
 255              FI;\r
 256    ESAC;   \r
 257    KILL(W);\r
 258    KILL(V);\r
 259 END PRKEY;  \r
 260 \r
 261 (*****************************************************************************) \r
 262 (* READS FORMULA FROM INPUT AND CONSTRUCT A TNODE *)\r
 263 \r
 264 UNIT GEN_TREE : FUNCTION : TNODE;   \r
 265 \r
 266 VAR T,S:TNODE;\r
 267       \r
 268 BEGIN   \r
 269    T:=ARG_TREE;                                  (* READ FIRST ARGUMENT *) \r
 270    C:=PNC;                                       (* NEXT INPUT CHARACTER *) \r
 271    WHILE C=CHROR OR C=CHRAND OR C=CHREQS OR C=CHRLSS OR C=118\r
 272    DO                                            (* LOOP FOR MORE *)    \r
 273      S:=NEW TNODE;                               (* ARGUMENTS *)  \r
 274      IF T=NONE THEN CALL EXCEPTIONS(1) FI;       (* NULL ARGUMENT *)\r
 275      CASE C  \r
 276        WHEN CHROR,118 : S.KIND:=DISKIND;  \r
 277        WHEN CHRAND: S.KIND:=CONKIND;  \r
 278        WHEN CHRLSS: IF PNC<>61 ORIF PNC<>62 THEN CALL EXCEPTIONS(1) FI; \r
 279                     S.KIND:=EQVKIND;  \r
 280        WHEN CHREQS: IF PNC<>CHRGTR THEN CALL EXCEPTIONS(1) FI;   \r
 281                     S.KIND:=IMPKIND;  \r
 282      ESAC;   \r
 283      S.RIGHT:=ARG_TREE;                          (* NEXT ARGUMENT *)\r
 284      S.LEFT:=T;  \r
 285      IF S.RIGHT=NONE THEN CALL EXCEPTIONS(1) FI; \r
 286      T:=S;   \r
 287      C:=PNC; \r
 288    OD;   \r
 289    RESULT := T;\r
 290 END GEN_TREE;   \r
 291 \r
 292 (****************************************************************************)\r
 293 (* READS ONE ARGUMENT OF INPUT FORMULA *)   \r
 294 \r
 295 UNIT ARG_TREE : FUNCTION : TNODE;   \r
 296 \r
 297 VAR T,S,U : TNODE,\r
 298     Q : BOOLEAN;   \r
 299     \r
 300 BEGIN   \r
 301    C:=PNC;\r
 302    IF C=CHREND THEN RETURN FI;                    (* RETURN NONE *) \r
 303    T:=NEW TNODE; \r
 304    RESULT:=T;\r
 305    Q:=TRUE;  \r
 306    CASE C\r
 307       WHEN CHRNEG,110 :T.KIND:=NEGKIND;           (* NEGATION *)\r
 308       WHEN CHRGQU :T.KIND:=QUAKIND;               (* GLOBAL QUANTIFIER *)\r
 309                    C:=PNC;                        (* FOLLOWING VARIABLE *)  \r
 310                    CALL SEARCH_NUM(T.IDENT,TRUE); (* NUMBER *)  \r
 311       WHEN CHREQU :S:=NEW TNODE;                  (* EXISTENTIAL QUANTIFIER *)\r
 312                    U:=NEW TNODE;                  (* CONVERT TO -'A'- *)\r
 313                    S.KIND:=NEGKIND;  \r
 314                    S.LEFT:=U;\r
 315                    U.KIND:=QUAKIND;  \r
 316                    C:=PNC;                        (* VARIABLE NAME *)   \r
 317                    CALL SEARCH_NUM(U.IDENT,TRUE); (* VARIABLE NUMBER *) \r
 318                    U.LEFT:=T;\r
 319                    T.KIND:=NEGKIND;  \r
 320                    RESULT := S   \r
 321        OTHERWISE   Q:=FALSE \r
 322     ESAC; \r
 323     IF Q THEN \r
 324        T.LEFT:=ARG_TREE;                          (* CONTINUE DEPTH SEARCH *)\r
 325        IF T.LEFT=NONE THEN CALL EXCEPTIONS(1) FI;  \r
 326        RETURN  \r
 327     FI;   \r
 328     IF C=CHROR ORIF C=CHRRPA ORIF C=CHRAND ORIF C=CHREQS ORIF C=CHRGTR ORIF   \r
 329        C=CHRLSS THEN  \r
 330        IF C=CHREQS THEN\r
 331           C:=PNC;\r
 332           IF C<>CHRGTR THEN \r
 333              CALL RETN(L-1);\r
 334           ELSE \r
 335              CALL EXCEPTIONS(1);\r
 336           FI\r
 337        ELSE\r
 338           CALL EXCEPTIONS(1);     \r
 339        FI;\r
 340     FI;   \r
 341     IF C=CHRLPA THEN  \r
 342        RESULT := GEN_TREE  \r
 343     ELSE                                         (* LITERAL ONLY *)\r
 344        RESULT := LIT_ARG                         (* SO READ IT *)\r
 345     FI;   \r
 346     KILL (T)  \r
 347 END ARG_TREE;   \r
 348 \r
 349 (****************************************************************************)\r
 350 (* SEARCH FOR A NUMBER *)\r
 351 \r
 352 UNIT SEARCH_NUM:PROCEDURE(INOUT B:INTEGER;ALEF:BOOLEAN);\r
 353 BEGIN\r
 354    C:=PNC;  \r
 355    IF C<48 OR C>57 THEN \r
 356       IF ALEF THEN\r
 357          B:=-1\r
 358       ELSE \r
 359          CALL RETN(L-1); \r
 360          B:=VAL(CHR(C));\r
 361          RETURN;\r
 362       FI;\r
 363    FI;    \r
 364    IF NOT ALEF THEN CALL RETN(L-1) FI;\r
 365    WHILE C>47 AND C<58  \r
 366    DO  \r
 367      B:=B*10+C-48; \r
 368      C:=PNC;\r
 369    OD; \r
 370    IF ALEF THEN B:=B+1 FI;\r
 371    CALL RETN(L-1);\r
 372 END SEARCH_NUM;\r
 373   \r
 374 (****************************************************************************)\r
 375 (* CONSTRUCT PREDICATE *)\r
 376 \r
 377 UNIT PRED : PROCEDURE ( INOUT A, B : INTEGER ; ALEF : BOOLEAN );\r
 378 BEGIN\r
 379    CASE C\r
 380      WHEN 61 : A := EQUKIND;\r
 381      WHEN 33 : A := LT1KIND; \r
 382      OTHERWISE A := LITKIND;\r
 383                CALL SEARCH_NUM ( B, ALEF );         (* SEARCH A NUMBER OF *)\r
 384    ESAC;                                            (* PREDICATE *)\r
 385 END PRED;\r
 386 \r
 387 (***************************************************************************)\r
 388 (* CONSTRUCT TERM *)\r
 389 \r
 390 UNIT MAKE_TERM : PROCEDURE ( INOUT A, B : INTEGER; C : INTEGER, ALEF : BOOLEAN );\r
 391 BEGIN\r
 392    A := C;\r
 393    CALL SEARCH_NUM ( B, ALEF );                     (* SEARCH A NUMBER OF *)\r
 394 END MAKE_TERM;                                      (* TERM *)\r
 395 \r
 396 (***************************************************************************)\r
 397 (* GIVES A LENGTH OF PATTERN OF 'S' *)\r
 398 \r
 399 UNIT LEN_SUB : FUNCTION : INTEGER;\r
 400 VAR I,J : INTEGER,\r
 401     ALFA : BOOLEAN;\r
 402 BEGIN\r
 403   IF C=83 OR C=115 OR C=81 OR C=113 THEN          (* CHECK -S:=... OR -Q:=... *)\r
 404    FOR I := 1 TO 3 \r
 405    DO\r
 406      FOR J := 1 TO I \r
 407      DO\r
 408       IF NOT EOF(G) THEN \r
 409        C:=PNC\r
 410       ELSE\r
 411        CALL RETN(L-J+1);\r
 412        ALFA:=TRUE;\r
 413        RESULT:=0;\r
 414        RETURN\r
 415       FI;\r
 416      OD;\r
 417      IF ALFA THEN EXIT FI;    \r
 418      IF C=ORD(':') THEN \r
 419         RESULT:=I;   \r
 420         CALL RETN(L-I); \r
 421         RETURN\r
 422      FI;\r
 423      CALL RETN(L-I);\r
 424    OD;\r
 425    FI;\r
 426    RESULT:=0;\r
 427 END LEN_SUB;\r
 428 \r
 429 (***************************************************************************)\r
 430 (* MAKES A SUBSTITUTION *)\r
 431 \r
 432 UNIT SUBSTITUTION:FUNCTION:TNODE;\r
 433 VAR T:TNODE;\r
 434 BEGIN\r
 435       T:=NEW TNODE;\r
 436       IF C=83 OR C=115 THEN\r
 437            T.KIND:=VARPROG                       (* READ S *)\r
 438       ELSE                         \r
 439            T.KIND:=BVARPRO                       (* READ A *)\r
 440       FI;\r
 441       CALL SEARCH_NUM(T.IDENT,TRUE);             (* NUMBER OF 'S' *)\r
 442       CALL LOOKN(3);\r
 443       CASE T.KIND\r
 444          WHEN VARPROG:T.LEFT:=LIT_ARG;\r
 445          WHEN BVARPRO:CALL RETN(L-1);T.LEFT:=GEN_TREE;CALL RETN(L-1);\r
 446       ESAC;\r
 447       RESULT:=T;\r
 448 END SUBSTITUTION;\r
 449 \r
 450 (***************************************************************************)\r
 451 (* CONSTRUCT IF-ALFA-THEN-K-ELSE-M-FI PROGRAM *)\r
 452 \r
 453 UNIT PROG_IF:FUNCTION:TNODE;\r
 454 VAR U,S,P,T:TNODE;\r
 455 BEGIN\r
 456    T:=NEW TNODE;              \r
 457    T.KIND:=IFFKIND;                              (* 'IF' *)\r
 458    LL:=LL+1;\r
 459    T.LEFT:=GEN_TREE;                             (* ALFA *)\r
 460    CALL RETN(L-1);                               (* BACK BEFORE 'T' *)\r
 461    IF PRKEY(4)<>6 THEN CALL EXCEPTIONS(1) FI;\r
 462    S:=NEW TNODE;\r
 463    T.RIGHT:=S;\r
 464    S.KIND:=THNKIND;                              (* 'THEN '*)\r
 465    C:=PNC;\r
 466    S.LEFT:=CONSUB;                               (* PROGRAM 'K' *)\r
 467    U:=NEW TNODE;\r
 468    S.RIGHT:=U;\r
 469    IF PRKEY(4)=7 THEN                            (* 'ELSE' *)\r
 470       U.KIND:=ELSKIND;\r
 471       C:=PNC;\r
 472       U.LEFT:=CONSUB                             (* PROGRAM 'M' *)\r
 473    ELSE \r
 474       CALL RETN(L-4);\r
 475    FI;\r
 476    IF PRKEY(2)<>2 THEN CALL EXCEPTIONS(1) FI;\r
 477    U.IDENT:=FIFKIND;\r
 478    LR:=LR+1;\r
 479    IF LL=LR THEN                                 (* AFTER NESTING  DO *)\r
 480                                                  (* 'WHILE ETC ' PROGRAM ON *)\r
 481       U.RIGHT:=GEN_TREE;                         (* FORMULA BETA *)\r
 482       CALL RETN(L-1)\r
 483    FI;                                           (* OR TERM TAU *)\r
 484    RESULT:=T;                         \r
 485 END PROG_IF;\r
 486 \r
 487 (***************************************************************************) \r
 488 \r
 489 (* CONSTRUCT BEGIN-K;M;N; -OR MORE PROGRAMS- END PROGRAM *)\r
 490 \r
 491 UNIT PROG_BEGIN:FUNCTION:TNODE;\r
 492 VAR V,T,S:TNODE;\r
 493 BEGIN\r
 494    T:=NEW TNODE;\r
 495    T.KIND:=BEGKIND;                              (* 'BEGIN' *)\r
 496    LL:=LL+1;\r
 497    IF PRKEY(3)<>5 THEN                           (* IF NOT 'END' *)\r
 498      CALL RETN(L-3);\r
 499      V:=NEW TNODE;\r
 500      T.LEFT:=V;\r
 501      C:=PNC;\r
 502      V.LEFT:=CONSUB;                             (* FIRST PROGRAM *)\r
 503      WRITELN("1");\r
 504      writeln("pekch=", peekch);\r
 505      WHILE (PNC=59 OR PEEKCH = 36 )              (* LOOP FOR PROGRAMS *)\r
 506      DO\r
 507      WRITELN("2");\r
 508        IF PEEKCH = 36 THEN V.IDENT := 1 FI;      (* UNIQUELY SUBSTITUTION *)\r
 509        C:=PNC;\r
 510        V.RIGHT:=CONSUB;                          (* NEXT PROGRAM *)      \r
 511        V.KIND:=SEMKIND;                          (* 'SEMICOLON' *)\r
 512        IF PNC=59 THEN \r
 513           S:=NEW TNODE;\r
 514           S.LEFT:=V.RIGHT;\r
 515           V.RIGHT:=S;\r
 516           V:=V.RIGHT\r
 517        FI;\r
 518        CALL RETN(L-1);\r
 519      OD;\r
 520      writeln (peekch );\r
 521    FI;\r
 522    CALL RETN(L-1);\r
 523    WRITELN("3");\r
 524    IF PRKEY(3)<>5 THEN CALL EXCEPTIONS(1) FI;\r
 525    WRITELN("4");\r
 526    T.IDENT:=ENDKIND;                             (* 'END' *)\r
 527    LR:=LR+1;\r
 528    IF LL=LR THEN                                 (* AFTER NESTING  DO *)\r
 529                                                  (* 'WHILE ETC ' PROGRAM ON *)\r
 530       T.RIGHT:=GEN_TREE;                         (* FORMULA BETA *)\r
 531       CALL RETN(L-1)\r
 532    FI;                                           (* OR TERM TAU *)\r
 533    RESULT:=T;\r
 534 END PROG_BEGIN;\r
 535 \r
 536 (***************************************************************************)\r
 537 (* CONSTRUCT WHILE-ALFA-D0-K-OD PROGRAM *)\r
 538 \r
 539 UNIT PROG_WHILE:FUNCTION:TNODE;\r
 540 VAR V,T:TNODE;\r
 541 BEGIN\r
 542     T:=NEW TNODE;\r
 543     T.KIND:=WHIKIND;                             (* 'WHILE' *)\r
 544     T.LEFT:=GEN_TREE;                            (*  ALFA *)\r
 545     CALL RETN(L-1);                              (* BACK BEFORE 'D' *)        \r
 546     V:=NEW TNODE;\r
 547     T.RIGHT:=V;\r
 548     IF PRKEY(2)<>3 THEN CALL EXCEPTIONS(1) FI;\r
 549     V.KIND:=DOFKIND;                             (* 'DO' *)\r
 550     C:=PNC;\r
 551     LL:=LL+1;\r
 552     V.LEFT:=CONSUB;                              (* PROGRAM 'K' *)\r
 553     IF PRKEY(2)<>4 THEN CALL EXCEPTIONS(1) FI;\r
 554     V.IDENT:=ODFKIND;                            (* 'OD' *)\r
 555     LR:=LR+1;             \r
 556     IF LL=LR THEN                                (* AFTER NESTING  DO *)\r
 557                                                  (* 'WHILE ETC ' PROGRAM ON *)\r
 558        V.RIGHT:=GEN_TREE;                        (* FORMULA BETA *)\r
 559        CALL RETN(L-1);\r
 560     FI;                                          (* OR TERM TAU *)\r
 561     RESULT:=T;\r
 562 END PROG_WHILE;\r
 563     \r
 564 (***************************************************************************)\r
 565 (* SEARCH FOR PROGRAMS *)\r
 566 \r
 567 UNIT PROG:FUNCTION:TNODE;\r
 568 BEGIN\r
 569    IF PRKEY(2)=1 THEN RESULT:=PROG_IF \r
 570    ELSE \r
 571         CALL RETN(L-2);\r
 572         CASE PRKEY(5)\r
 573           WHEN  8: RESULT:=PROG_BEGIN;\r
 574           WHEN  9: RESULT:=PROG_WHILE;\r
 575           OTHERWISE CALL RETN(L-5);\r
 576         ESAC;\r
 577     FI;\r
 578 END PROG;\r
 579 \r
 580 (***************************************************************************)\r
 581 (* CONSTRUCT ITERATION EXISTENTIAL QUANTIFIER *)\r
 582 \r
 583 UNIT ITE_EX_Q:FUNCTION:TNODE;\r
 584 VAR T:TNODE;\r
 585 BEGIN\r
 586    T:=NEW TNODE;\r
 587    T.KIND:=ITEKIND;                            (* T.IDENT=0-IT MEANS *)\r
 588    C:=PNC;                                     (* THAT RULE WAS NOT ACTIVE *)\r
 589    T.RIGHT:=LIT_ARG;\r
 590    RESULT:=T;\r
 591 END ITE_EX_Q;\r
 592 \r
 593 (***************************************************************************)\r
 594 (* CONSTRUCT ITERATION GREAT QUANTIFIER *)\r
 595  \r
 596 UNIT ITE_GR_Q:FUNCTION:TNODE;\r
 597 VAR T:TNODE;\r
 598 BEGIN\r
 599      T:=NEW TNODE;\r
 600      T.KIND:=IGQKIND;                            (* T.IDENT=0-IT MEANS *)\r
 601      C:=PNC;                                     (* THAT RULE WAS NOT ACTIVE *)\r
 602      T.RIGHT:=LIT_ARG;\r
 603      RESULT:=T;\r
 604 END ITE_GR_Q;\r
 605 \r
 606 (*****************************************************************************)\r
 607 (* CONSTRUCT SUBSTITUTION AND READS NUMBER OF S *)\r
 608 \r
 609 UNIT CONSUB:FUNCTION:TNODE;\r
 610 VAR T:TNODE,\r
 611     I,J:INTEGER;\r
 612   BEGIN\r
 613      T:=NEW TNODE;\r
 614      IF C=83 ORIF C=115 ORIF C=81 ORIF C=113 THEN\r
 615           CASE C\r
 616                WHEN 83,115: T.KIND:=VARPROG;\r
 617                WHEN 81,113: T.KIND:=BVARPRO;\r
 618           ESAC;\r
 619           CALL SEARCH_NUM(T.IDENT,TRUE);\r
 620           CALL LOOKN(3);\r
 621           CASE T.KIND\r
 622                WHEN VARPROG : T.LEFT:=LIT_ARG;\r
 623                WHEN BVARPRO : CALL RETN(L-1);\r
 624                               T.LEFT:=GEN_TREE;\r
 625                               CALL RETN(L-1);\r
 626           ESAC;\r
 627           FOR I:=2 TO 4                          (* IF NOT 'FI' AND NOT 'OD' *)\r
 628           DO                                     (* AND NOT 'END' AND *)\r
 629             J:=PRKEY(I);\r
 630             CALL RETN(L-I);\r
 631             IF J<>0 THEN EXIT FI;               (* NOT 'ELSE' THEN REPEAT *)\r
 632           OD;                                    (* CONSUB *)\r
 633           IF (PNC<>59 AND PEEKCH<>36) THEN\r
 634              IF J=0 THEN T.RIGHT:=CONSUB ELSE CALL RETN(L-1); FI\r
 635           ELSE\r
 636              CALL RETN(L-1)\r
 637           FI   \r
 638      ELSE                               \r
 639           T:=LIT_ARG;                            (* IF NOT SUB THEN PROGRAM *)\r
 640      FI;\r
 641      RESULT:=T;\r
 642 END CONSUB;\r
 643      \r
 644 (***************************************************************************)\r
 645 (* READS INPUT LITERAL *)   \r
 646 \r
 647 UNIT LIT_ARG : FUNCTION : TNODE;\r
 648 VAR T,U:TNODE;\r
 649         \r
 650 BEGIN   \r
 651    T:=NEW TNODE;                                 (* RESERVE NODE *)\r
 652    IF LEN_SUB<>0 THEN \r
 653       T:=SUBSTITUTION;\r
 654       C:=PNC;                                    (* OMITED LEFT PAR  *)\r
 655       T.RIGHT:=GEN_TREE;\r
 656       RESULT:=T;\r
 657       RETURN\r
 658    ELSE\r
 659      CASE C\r
 660       WHEN 67,99 : CALL MAKE_TERM(T.KIND,T.IDENT,CN2KIND,TRUE);\r
 661                     RESULT:=T;\r
 662                     RETURN;                      (* CONSTANT 'C' *)\r
 663       WHEN 85     : T:=ITE_EX_Q;  \r
 664                     RESULT:=T;\r
 665                     RETURN;                      (* ITEKIND 'U' *)\r
 666       WHEN 64     : T:=ITE_GR_Q;\r
 667                     RESULT:=T;\r
 668                     RETURN;                      (* IGQKIND '@' *)\r
 669       WHEN 88,120 : CALL MAKE_TERM(T.KIND,T.IDENT,VARKIND,TRUE);\r
 670                     RESULT:=T;\r
 671                     RETURN;                      (* VARIABLE 'X' *)\r
 672       WHEN 117    : CALL MAKE_TERM(T.KIND,T.IDENT,VRUKIND,TRUE);\r
 673                     RESULT:=T;\r
 674                     RETURN;                      (* VRUKIND 'u' *)\r
 675       WHEN 81,113 : CALL MAKE_TERM(T.KIND,T.IDENT,BVAKIND,TRUE);\r
 676                     RESULT:=T;               \r
 677                     RETURN;                      (* BVAKIND 'Q'*)\r
 678       WHEN 83,115 : CALL MAKE_TERM(T.KIND,T.IDENT,SUBKIND,TRUE);\r
 679                     RESULT:=T;\r
 680                     RETURN;                      (* SUBKIND 'S' *)\r
 681       WHEN 61,33,                                (* EQUKIND '=' *)\r
 682            80,112 : CALL PRED(T.KIND,T.IDENT,TRUE);\r
 683                                                  (* LITKIND 'P' *)\r
 684                                                  (* LT1KIND '!' *)\r
 685       WHEN 71,103 : CALL MAKE_TERM ( T.KIND, T.IDENT, FUNKIND, TRUE );\r
 686                                                  (* FUNKIND 'G' *)\r
 687       WHEN 35     : CALL MAKE_TERM ( T.KIND, T.IDENT, FN1KIND, TRUE );\r
 688                                                  (* FN1KIND '#' *)\r
 689       WHEN 70,102 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );\r
 690                     T.IDENT := 0;                (* LOGICAL FALSE 'F' *)\r
 691                     RESULT := T;\r
 692                     RETURN;\r
 693       WHEN 84,116 : CALL MAKE_TERM ( T.KIND,T.IDENT,LOGKIND,TRUE );\r
 694                     T.IDENT := 1;                (* LOGICAL TRUE 'T' *)\r
 695                     RESULT := T;\r
 696                     RETURN;               \r
 697       WHEN 48,49,50,51,52,53,54,55,56,57\r
 698                   : CALL MAKE_TERM(T.KIND,T.IDENT,CNTKIND,FALSE);\r
 699                     RESULT:=T;\r
 700                     RETURN;                      (* DIGITS E.G. '2' *)\r
 701       WHEN 42,43,45,47,94                        (* '*','+','-','/,'^' *)\r
 702                   : CALL MAKE_TERM(T.KIND,T.IDENT,ARIKIND,TRUE);\r
 703                     T.IDENT:=C;\r
 704       WHEN 37     : CALL MAKE_TERM ( T.KIND, T.IDENT, CN1KIND, TRUE );\r
 705                     RESULT := T;\r
 706                     RETURN;                      (* FALSE CONSTANT *)        \r
 707       WHEN 68,100 : CALL MAKE_TERM ( T.KIND, T.IDENT, SIGNTRM, TRUE );\r
 708                                                  (* DUMKIND 'D' *)\r
 709       OTHERWISE     CALL RETN(L-1);\r
 710                     T:=PROG;                     (* PROGRAMS *)\r
 711                     RESULT:=T;\r
 712                     RETURN;\r
 713      ESAC;\r
 714      C:=PNC;\r
 715      IF C=CHRLPA THEN                            (* LEFT PAR '(' *)\r
 716         C:=PNC;                                  (* EXPECT SOME ARGUMENTS *)\r
 717         T.LEFT:=LIT_ARG;                         (* READ ARGUMENTS *)\r
 718         U:=T.LEFT;                               (* FIRST ON LEFT *)\r
 719         WHILE PNC=CHRCOM                         (* COMMA *)\r
 720         DO                   \r
 721           C:=PNC;                                (* LOOP FOR MORE *) \r
 722           WHILE U.RIGHT<>NONE                    (* OMIT PROGRAMS ON RIGHT *)\r
 723           DO\r
 724             U:=U.RIGHT;\r
 725           OD;\r
 726           U.RIGHT:=LIT_ARG;                      (* NEXT ON RIGHT *)\r
 727           U:=U.RIGHT\r
 728         OD;                       \r
 729         C:=PEEKCH;\r
 730         IF C<>CHRRPA THEN CALL EXCEPTIONS(1) FI;(* EXPECT ')' *)\r
 731      ELSE \r
 732         CALL RETN(L-1);  \r
 733      FI;\r
 734      RESULT:=T;    \r
 735      RETURN;\r
 736    FI;\r
 737 END LIT_ARG;\r
 738 \r
 739 (****************************************************************************)\r
 740 (* STOPS EXECUTION IF THERE IS AN ERROR *)\r
 741 \r
 742 UNIT EXCEPTIONS:PROCEDURE(N:INTEGER);\r
 743 BEGIN\r
 744    CASE N\r
 745       WHEN 1:WRITELN("SYNTAX ERROR");\r
 746       WHEN 2:WRITELN("0/0");\r
 747       WHEN 3:WRITELN("DIVISION BY ZERO");\r
 748       WHEN 4:WRITELN("0^0");\r
 749    ESAC;\r
 750    RAISE ENDRUN\r
 751 END EXCEPTIONS;\r
 752 \r
 753 (***************************************************************************) \r
 754 (*                 PRINT FORMULA ON SCREEN AND TO FILE                     *)\r
 755 (***************************************************************************)\r
 756  \r
 757 (***************************************************************************)\r
 758 (* PRINT FORMULA ON SCREEN *)\r
 759 UNIT WR_FOR : PROCEDURE ( C : TNODE );\r
 760 BEGIN\r
 761    IF C = NONE THEN RETURN FI;\r
 762    CASE C.KIND \r
 763      WHEN CONKIND : CALL WR_FOR_HELP ( C, '&' ); (* CONJUCTION *)\r
 764      WHEN DISKIND : CALL WR_FOR_HELP ( C, 'v' ); (* DISJUNCTION *)\r
 765      WHEN IMPKIND : CALL WR_FOR_HELP ( C, '=' ); (* IMPLICATION *)\r
 766      WHEN EQVKIND : CALL WR_FOR_HELP ( C, '<' ); (* EQUIVALENCE *)\r
 767      WHEN NEGKIND : CALL PUTCH ( 'n' );          \r
 768                     CALL WR_FOR ( C.LEFT );      (* NEGATION *)\r
 769      WHEN LOGKIND : IF C.IDENT = 0 THEN CALL PUTCH ( 'F' ) \r
 770                                    ELSE CALL PUTCH ( 'T' ); (* LOGICAL CONSTANTS *)\r
 771                     FI;\r
 772      WHEN VARKIND : CALL PUTCH ( 'x' );          (* VARIABLE *)\r
 773                     CALL PNUM ( C.IDENT );       (* AND ITS IDENTIFIER *)\r
 774      WHEN IGQKIND : CALL PUTCH ( '@' );          (* ITERATION GREAT QUANTIFIER *)\r
 775                     CALL WR_FOR ( C.RIGHT );            \r
 776      WHEN ITEKIND : CALL PUTCH ( 'U' );          (* EXISTENTIAL ITERATION QUANTIFIER *)\r
 777                     CALL WR_FOR ( C.RIGHT );\r
 778      WHEN IFFKIND : CALL PUTCH ( 'I' );          (* IF *)\r
 779                     CALL PUTCH ( 'F' );\r
 780                     CALL WR_FOR ( C.LEFT );      (* ALFA *)\r
 781                     CALL PUTCH ( 'T' );          (* THEN *)\r
 782                     CALL PUTCH ( 'H' );\r
 783                     CALL PUTCH ( 'E' );\r
 784                     CALL PUTCH ( 'N' );\r
 785                     CALL WR_FOR ( C.RIGHT.LEFT ); (* K *)\r
 786                     IF C.RIGHT.RIGHT.KIND = ELSKIND THEN \r
 787                        CALL PUTCH ( 'E' );\r
 788                        CALL PUTCH ( 'L' );\r
 789                        CALL PUTCH ( 'S' );\r
 790                        CALL PUTCH ( 'E' );       (* ELSE *)\r
 791                        CALL WR_FOR ( C.RIGHT.RIGHT.LEFT ); (* M *)\r
 792                     FI;\r
 793                     CALL PUTCH ( 'F' );          (* FI *)\r
 794                     CALL PUTCH ( 'I' );\r
 795                     CALL WR_FOR ( C.RIGHT.RIGHT.RIGHT ); (* BETA *)\r
 796      WHEN BEGKIND : CALL PUTCH ( 'B' );\r
 797                     CALL PUTCH ( 'E' );\r
 798                     CALL PUTCH ( 'G' );\r
 799                     CALL PUTCH ( 'I' );\r
 800                     CALL PUTCH ( 'N' );          (* BEGIN *)\r
 801                     CALL WR_FOR ( C.LEFT );      (* K *)\r
 802                     CALL PUTCH ( 'E' );\r
 803                     CALL PUTCH ( 'N' );\r
 804                     CALL PUTCH ( 'D' );          (* END *)\r
 805                     CALL WR_FOR ( C.RIGHT );     (* BETA *)\r
 806      WHEN SEMKIND : CALL WR_FOR ( C.LEFT );      (* K1 *)\r
 807                     IF C.IDENT = 1 THEN \r
 808                        CALL PUTCH ( '$' )        (* UNIQUELY SUBSTITUTION *)\r
 809                                    ELSE \r
 810                        CALL PUTCH ( ';' )        (* SEMICOLON *)\r
 811                     FI;\r
 812                     CALL WR_FOR ( C.RIGHT );     (* K2 *)\r
 813      WHEN WHIKIND : CALL PUTCH ( 'W' );\r
 814                     CALL PUTCH ( 'H' );\r
 815                     CALL PUTCH ( 'I' );\r
 816                     CALL PUTCH ( 'L' );\r
 817                     CALL PUTCH ( 'E' );          (* WHILE *)\r
 818                     CALL WR_FOR ( C.LEFT );      (* ALFA *)\r
 819                     CALL PUTCH ( 'D' );\r
 820                     CALL PUTCH ( 'O' );          (* DO *)\r
 821                     CALL WR_FOR ( C.RIGHT.LEFT );(* K *)\r
 822                     CALL PUTCH ( 'O' );\r
 823                     CALL PUTCH ( 'D' );          (* OD *)\r
 824                     CALL WR_FOR ( C.RIGHT.RIGHT ); (* BETA *)\r
 825      WHEN QUAKIND : CALL PUTCH ( 'A' );          (* GREAT QUANTIFIER *)\r
 826                     CALL PUTCH ( 'x' );          (* VARIABLE *)\r
 827                     CALL PNUM ( C.IDENT );       (* ITS NUMBER *)\r
 828                     CALL WR_FOR ( C.LEFT );      (* ALFA *)\r
 829      WHEN EQUKIND,\r
 830           LITKIND,\r
 831           FUNKIND,\r
 832           LT1KIND,\r
 833           FN1KIND : CASE C.KIND \r
 834                       WHEN EQUKIND : CALL PUTCH ( '=' );\r
 835                       WHEN LITKIND : CALL PUTCH ( 'P' ); \r
 836                       WHEN FUNKIND : CALL PUTCH ( 'G' );\r
 837                       WHEN LT1KIND : CALL PUTCH ( '!' );\r
 838                       WHEN FN1KIND : CALL PUTCH ( '#' );\r
 839                     ESAC;                        (* PREDICATE OR FUNCTION *)\r
 840                     CALL PNUM ( C.IDENT );\r
 841                     IF C.LEFT = NONE THEN RETURN FI;\r
 842                     CALL PUTCH ( '(' );\r
 843                     C := C.LEFT;\r
 844                     WHILE C <> NONE \r
 845                     DO\r
 846                       CALL WR_FOR ( C );         (* ARGUMENT *)\r
 847                       C := C.RIGHT;              (* TAKE NEXT ARGUMENT *)\r
 848                       IF C <> NONE THEN CALL PUTCH ( ',' ) FI;\r
 849                     OD;\r
 850                     CALL PUTCH ( ')' );\r
 851      WHEN CNTKIND : CALL PNUM ( C.IDENT + 1 );   (* NUMERIC CONSTANT *)\r
 852      WHEN CN1KIND : CALL PUTCH ( '%' );          (* FALSE CONSTANT *)\r
 853                     CALL PNUM ( C.IDENT + 1 );\r
 854      WHEN CN2KIND : CALL PUTCH ( 'C' );          (* CONSTANT OF THE FORM 'C' *)\r
 855                     CALL PNUM ( C.IDENT );\r
 856      WHEN ARIKIND : CALL PUTCH ( CHR ( C.IDENT ) ); (* ARITHMETIC OPERATION *)\r
 857                     IF C.LEFT.RIGHT = NONE THEN \r
 858                        CALL WR_FOR ( C.LEFT );\r
 859                        RETURN \r
 860                     FI;\r
 861                     CALL PUTCH ( '(' );\r
 862                     CALL WR_FOR ( C.LEFT );\r
 863                     CALL PUTCH ( ',' );\r
 864                     CALL WR_FOR ( C.LEFT.RIGHT );\r
 865                     CALL PUTCH ( ')' );\r
 866      WHEN VRUKIND : CALL PUTCH ( 'u' );          (* SPECIAL KIND OF VARIABLE *)\r
 867                     CALL PNUM ( C.IDENT );\r
 868      WHEN BVAKIND : CALL PUTCH ( 'Q' );          (* LOGICAL VARIABLE *)\r
 869                     CALL PNUM ( C.IDENT );\r
 870      WHEN SUBKIND : CALL PUTCH ( 'S' );          (* VARABLE TO BE SUBSTITUTED ON *)\r
 871                     CALL PNUM ( C.IDENT );\r
 872      WHEN VARPROG,\r
 873           BVARPRO : IF C.KIND = VARPROG THEN \r
 874                        CALL PUTCH ( 'S' )        (* SUBSTITUTION S:= *)\r
 875                     ELSE \r
 876                        CALL PUTCH ( 'Q' );       (* Q:= *)\r
 877                     FI;\r
 878                     CALL PNUM ( C.IDENT );\r
 879                     CALL PUTCH ( ':' );\r
 880                     CALL PUTCH ( '=' );\r
 881                     CALL WR_FOR ( C.LEFT );      (* TAU OR ALFA*)\r
 882                     IF C.RIGHT = NONE THEN RETURN FI;\r
 883                     CALL PUTCH ( '(' );          (* NEXT FORMULA *)\r
 884                     CALL WR_FOR ( C.RIGHT );\r
 885                     CALL PUTCH ( ')' );\r
 886      WHEN SIGNTRM : CALL PUTCH ( 'D' );          (* DUMKIND *)\r
 887                     CALL PNUM ( C.IDENT );\r
 888    ESAC; \r
 889 END WR_FOR;     \r
 890 \r
 891 (***************************************************************************)\r
 892 (* HELP FOR WR_FOR PROCEDURE *)\r
 893 \r
 894 UNIT WR_FOR_HELP : PROCEDURE ( C : TNODE, CH : CHARACTER );\r
 895 BEGIN\r
 896    CALL PUTCH ( '(' );\r
 897    CALL WR_FOR ( C.LEFT );\r
 898    CALL PUTCH ( CH );\r
 899    CASE CH\r
 900       WHEN '=' : CALL PUTCH ( '>' );\r
 901       WHEN '<' : CALL PUTCH ( '=' );\r
 902                  CALL PUTCH ( '>' );\r
 903    ESAC;        \r
 904    CALL WR_FOR ( C.RIGHT );\r
 905    CALL PUTCH ( ')' );\r
 906 END WR_FOR_HELP;\r
 907 \r
 908 (***************************************************************************)\r
 909 (*                 ADDITIONAL PROCEDURES AND FUNCTIONS                     *)\r
 910 (***************************************************************************)\r
 911 \r
 912 (***************************************************************************)\r
 913 (* GIVES A VALUE OF CHARACTER *)\r
 914 \r
 915 UNIT VAL:FUNCTION(A:CHARACTER):INTEGER; \r
 916 BEGIN   \r
 917    RESULT:=ORD(A)-48   \r
 918 END VAL;\r
 919 \r
 920 (*****************************************************************************)\r
 921 (* PRINTS ALL TREES IN A SEQUENT *)\r
 922 \r
 923 UNIT SHOW_SEQ : PROCEDURE ( A : SEQUENT );\r
 924 BEGIN\r
 925    IF A <> NONE THEN \r
 926       WRITELN("P");\r
 927       CALL WR_FOR ( A.PLEAF ); (* SHOW_TREE ( A.PLEAF); *)\r
 928       WRITELN("L");\r
 929       CALL WR_FOR ( A.LLEAF );  (* SHOW_TREE ( A.LLEAF ); *)\r
 930       WRITELN;\r
 931       CALL SHOW_SEQ ( A.NEXT );\r
 932    FI;\r
 933 END SHOW_SEQ;\r
 934    \r
 935 (*****************************************************************************)\r
 936 (* PRINTS TREE *)\r
 937 \r
 938 UNIT SHOW_TREE : PROCEDURE ( A : TNODE );\r
 939 BEGIN\r
 940    IF A<>NONE THEN\r
 941       WRITELN(A.KIND,"=K",A.IDENT,"=I");\r
 942       CALL SHOW_TREE(A.LEFT);\r
 943       CALL SHOW_TREE(A.RIGHT);\r
 944    FI;\r
 945 END SHOW_TREE;\r
 946 \r
 947 (****************************************************************************)\r
 948 (* MOVE UP I TNODES FROM RIGHT (P=1) OR LEFT (P=0) SIDE *)\r
 949 \r
 950 UNIT LIFT : PROCEDURE ( T : TNODE; I, P : INTEGER );\r
 951 VAR A : TNODE;\r
 952 BEGIN\r
 953    WHILE I>0\r
 954    DO\r
 955      CASE P\r
 956        WHEN 1: A := T.RIGHT;\r
 957        WHEN 0: A := T.LEFT;\r
 958      ESAC;\r
 959      T.KIND  := A.KIND;\r
 960      T.IDENT := A.IDENT;\r
 961      T.RIGHT := A.RIGHT;\r
 962      T.LEFT  := A.LEFT;\r
 963      KILL ( A );\r
 964      I := I - 1\r
 965   OD;\r
 966 END LIFT;\r
 967 \r
 968 (****************************************************************************)\r
 969 (* MOVE UP POINTER *)\r
 970 \r
 971 UNIT LIFT_PNTR : PROCEDURE ( INOUT M1 : POINTER );\r
 972 VAR M2 : POINTER;\r
 973 BEGIN\r
 974     IF M1 <> NONE THEN\r
 975        M2 := M1.DOWN;\r
 976        CALL ERASE_SEQ ( M1.NEXT );\r
 977        IF M1.DOWN <> NONE THEN\r
 978           M1.NEXT := M1.DOWN.NEXT;\r
 979           M1.DOWN := M1.DOWN.DOWN;\r
 980           KILL ( M2 )\r
 981        ELSE\r
 982           KILL ( M1 )\r
 983        FI;      \r
 984     FI;\r
 985 END LIFT_PNTR;\r
 986     \r
 987 (****************************************************************************)\r
 988 (* MOVE LAST NON-EMPTY RIGHT OR LEFT TNODE OF A SEQUENT TO THE BEGINNING *)\r
 989 \r
 990 UNIT MOVE : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER);\r
 991 VAR HEAD1,TAIL : SEQUENT,\r
 992     S : INTEGER;\r
 993 BEGIN\r
 994     HEAD1 := NEW SEQUENT;\r
 995     TAIL := LAST ( M , P );\r
 996     IF P=1 THEN R := R + 1 FI;\r
 997     S := R + P;\r
 998     CASE S\r
 999        WHEN 0:HEAD1.LLEAF:=TAIL.LLEAF;           (* LEFT TO LEFT *)\r
1000               TAIL.LLEAF:=NONE ;                 (* P=0,R=0 *)\r
1001        WHEN 3:HEAD1.PLEAF:=TAIL.PLEAF;           (* RIGHT TO RIGHT *)\r
1002               TAIL.PLEAF:=NONE;                  (* P=1,R=1 *)\r
1003        WHEN 1:HEAD1.PLEAF:=TAIL.LLEAF;           (* LEFT TO RIGHT *)\r
1004               TAIL.LLEAF:=NONE;                  (* P=0,R=1 *)\r
1005        WHEN 2:HEAD1.LLEAF:=TAIL.PLEAF;           (* RIGHT TO LEFT *)\r
1006               TAIL.PLEAF:=NONE;                  (* P=1,R=0 *)\r
1007     ESAC;\r
1008     HEAD1.NEXT := M.NEXT;\r
1009     M.NEXT := HEAD1;\r
1010 END MOVE;\r
1011 \r
1012 (****************************************************************************)\r
1013 (* GIVES THE LAST NON EMPTY P-SIDE SEQUENT *)\r
1014 \r
1015 UNIT LAST:FUNCTION(M:POINTER;P:INTEGER):SEQUENT;\r
1016 VAR HEAD1:SEQUENT;\r
1017 BEGIN\r
1018    IF M=NONE ORIF M.NEXT=NONE THEN \r
1019       RESULT:=NONE;\r
1020       RETURN;\r
1021    FI;\r
1022    IF P=1 THEN\r
1023       HEAD1:=M.NEXT;\r
1024       IF HEAD1.PLEAF<>NONE THEN RESULT:=HEAD1 FI;\r
1025       WHILE HEAD1.NEXT<>NONE\r
1026       DO\r
1027       IF HEAD1.NEXT.PLEAF<>NONE THEN\r
1028          RESULT:=HEAD1.NEXT\r
1029       FI;\r
1030       HEAD1:=HEAD1.NEXT\r
1031       OD;\r
1032    ELSE\r
1033       HEAD1:=M.NEXT;\r
1034       IF HEAD1.LLEAF<>NONE THEN RESULT:=HEAD1 FI;\r
1035       WHILE HEAD1.NEXT<>NONE\r
1036       DO\r
1037         IF HEAD1.NEXT.LLEAF<>NONE THEN\r
1038             RESULT:=HEAD1.NEXT;\r
1039         FI;\r
1040         HEAD1:=HEAD1.NEXT\r
1041       OD;\r
1042    FI;\r
1043 END LAST;\r
1044 \r
1045 (****************************************************************************)\r
1046 (* GO TO THE END OF A PROGRAM WITH TAU *)\r
1047 \r
1048 UNIT END_OF_PRG : PROCEDURE ( INOUT C : TNODE );\r
1049 BEGIN\r
1050    IF C = NONE THEN RETURN FI;\r
1051    WHILE C.RIGHT <> NONE \r
1052    DO \r
1053      C := C.RIGHT;\r
1054    OD;\r
1055 END END_OF_PRG;\r
1056 \r
1057 (*****************************************************************************)\r
1058 (* GO TO THE END OF PROGRAM *)\r
1059 \r
1060 UNIT END_OF_P : PROCEDURE ( INOUT C : TNODE );\r
1061 VAR D : TNODE;\r
1062 BEGIN\r
1063    IF C = NONE THEN RETURN FI;\r
1064    WHILE C.RIGHT <> NONE \r
1065    DO\r
1066      D := C;\r
1067      C := C.RIGHT;\r
1068    OD;\r
1069    C := D;\r
1070 END END_OF_P;\r
1071 \r
1072 (*****************************************************************************)\r
1073 (* GO TO THE END OF AXIOMS LIST *)\r
1074  \r
1075 UNIT END_OF_AX : PROCEDURE ( INOUT AX1 : LIST_AXIOMS );\r
1076 BEGIN\r
1077     IF AX = NONE THEN RETURN FI;\r
1078     AX1 := AX;\r
1079     WHILE AX1.NEXT <> NONE\r
1080     DO\r
1081        AX1 := AX1.NEXT;\r
1082     OD;\r
1083 END END_OF_AX;\r
1084     \r
1085 (*****************************************************************************)\r
1086 (* GO TO THE END OF POINTERS *)\r
1087 \r
1088 UNIT END_OF_M : PROCEDURE ( INOUT M : POINTER , A : SEQUENT );\r
1089 VAR M1 : POINTER;\r
1090 BEGIN\r
1091     IF M = NONE THEN RETURN FI;\r
1092     M.NEXT := NONE;\r
1093     WHILE M.DOWN <> NONE \r
1094     DO\r
1095       M := M.DOWN;\r
1096     OD;\r
1097     M1 := NEW POINTER;\r
1098     M.DOWN := M1;\r
1099     CALL SQUEEZE ( M1 , 0 );\r
1100     CALL SQUEEZE ( M1 , 1 );\r
1101     M1.NEXT := A;\r
1102     CALL CUT_SEQ ( M1.NEXT );\r
1103     M1.DOWN := NONE;\r
1104 END END_OF_M;\r
1105        \r
1106 (*****************************************************************************)\r
1107 (* ERASE A TREE *)\r
1108 \r
1109 UNIT ERASE : PROCEDURE ( A : TNODE );\r
1110 BEGIN\r
1111    IF A <> NONE THEN\r
1112       CALL ERASE ( A.LEFT );                     (* GO TO LAST LEFT TNODE *)\r
1113       CALL ERASE ( A.RIGHT );                    (* GO TO LAST RIGHT TNODE *)\r
1114       KILL ( A );                                (* REMOVE TNODE *)\r
1115    FI;\r
1116 END ERASE;\r
1117 \r
1118 (*****************************************************************************)\r
1119 (* ERASE A SEQUENT *)\r
1120 \r
1121 UNIT ERASE_SEQ : PROCEDURE ( A : SEQUENT );\r
1122 BEGIN\r
1123    IF A <> NONE THEN\r
1124       CALL ERASE_SEQ ( A.NEXT );                 (* GO TO THE LAST SEQUENT *)\r
1125       CALL ERASE ( A.LLEAF );                    (* REMOVE LEFT TREE *)\r
1126       CALL ERASE ( A.PLEAF );                    (* REMOVE RIGHT TREE *)\r
1127       KILL ( A );                                (* REMOVE SEQUENT *)\r
1128    FI;\r
1129 END ERASE_SEQ;\r
1130 \r
1131 (*****************************************************************************)\r
1132 (* ERASE AN EMPTY POINTER, I.E. LINKED TO THE EMPTY FORMULA ' |- ' *)\r
1133 \r
1134 UNIT ERASE_PNTR : PROCEDURE ( INOUT M1 : POINTER );\r
1135 BEGIN\r
1136    IF M1 = NONE THEN RETURN FI;                  (* SEQUENT IS EMPTY *)\r
1137    CALL LIFT_PNTR ( M1 );                        (* REMOVE POINTER *)\r
1138    CALL ERASE_PNTR ( M1 );                       (* REMOVE NEXT POINTER *)\r
1139 END ERASE_PNTR;\r
1140 \r
1141 (*****************************************************************************)\r
1142 (* REMOVE LIST OF AXIOMS *)\r
1143 \r
1144 UNIT ERASE_AX : PROCEDURE ( AX : LIST_AXIOMS );\r
1145 BEGIN\r
1146    IF AX = NONE THEN RETURN FI;\r
1147    CALL ERASE_AX ( AX.NEXT );\r
1148    CALL ERASE ( AX.AXIOM );\r
1149 END;\r
1150 \r
1151 (*****************************************************************************)\r
1152 (* GO TO THE END OF SUBSTITUTION *)\r
1153 \r
1154 UNIT END_OF_S : PROCEDURE ( INOUT A , B : TNODE );\r
1155 BEGIN\r
1156    IF A = NONE THEN RETURN FI;\r
1157    WHILE A.KIND=VARPROG OR A.KIND=BVARPRO \r
1158    DO\r
1159      B:=A;\r
1160      A:=A.RIGHT;\r
1161      IF A = NONE THEN EXIT FI ;\r
1162    OD;\r
1163 END END_OF_S;\r
1164 \r
1165 (****************************************************************************)\r
1166 (* MAKES A COPY OF TNODE TREE *)\r
1167 \r
1168 UNIT COPYTNODE : FUNCTION ( X : TNODE ) : TNODE;\r
1169 BEGIN\r
1170    IF X <> NONE THEN\r
1171       RESULT := COPY ( X );\r
1172       RESULT.LEFT  := COPYTNODE ( X.LEFT );\r
1173       RESULT.RIGHT := COPYTNODE ( X.RIGHT );\r
1174    FI;\r
1175 END COPYTNODE;\r
1176 \r
1177 (****************************************************************************)\r
1178 (* MAKES A COPY OF ALL SEQUENTS IN A TREE , INCLUDING TNODES *)\r
1179 \r
1180 UNIT COPYSEQUENT : FUNCTION ( X : SEQUENT ) : SEQUENT;\r
1181 BEGIN\r
1182    IF X <> NONE THEN \r
1183       RESULT := COPY ( X );\r
1184       RESULT.PLEAF := COPYTNODE ( X.PLEAF );\r
1185       RESULT.LLEAF := COPYTNODE ( X.LLEAF );\r
1186       RESULT.NEXT := COPYSEQUENT ( X.NEXT );\r
1187    FI;\r
1188 END COPYSEQUENT;\r
1189 \r
1190 (*****************************************************************************)\r
1191 (* UPDATE THE GREATEST NUMBER OF VARIABLE *)\r
1192  \r
1193 UNIT LAST1_X : PROCEDURE ( A : TNODE );\r
1194 BEGIN\r
1195      IF A=NONE THEN RETURN FI;\r
1196      IF A.KIND=VARKIND THEN\r
1197         IF LAST_X < A.IDENT THEN LAST_X := A.IDENT FI;\r
1198      FI;\r
1199      CALL LAST1_X ( A.LEFT );\r
1200      CALL LAST1_X ( A.RIGHT );\r
1201 END  LAST1_X;\r
1202 \r
1203 (****************************************************************************)\r
1204 (* LOOKING FOR THE GREATEST BVARPRO SUBSTITUTION *)\r
1205 \r
1206 UNIT LAST1_Q:PROCEDURE(A:TNODE);\r
1207 BEGIN\r
1208      IF A=NONE THEN RETURN FI;\r
1209      IF A.KIND=BVARPRO THEN\r
1210         IF LAST_Q < A.IDENT THEN LAST_Q:=A.IDENT FI;\r
1211      FI;\r
1212      CALL LAST1_Q(A.RIGHT);\r
1213      CALL LAST1_Q(A.LEFT);\r
1214 END  LAST1_Q;\r
1215 \r
1216 (****************************************************************************)\r
1217 (* UPDATE THE GREATEST NUMBER OF VARPROG *)\r
1218 \r
1219 UNIT LAST1_S : PROCEDURE ( A : TNODE );\r
1220 BEGIN \r
1221      IF A=NONE THEN RETURN FI;\r
1222      IF A.KIND=VARPROG THEN\r
1223         IF LAST_S < A.IDENT THEN LAST_S := A.IDENT FI;\r
1224      FI;\r
1225      CALL LAST1_S ( A.LEFT );\r
1226      CALL LAST1_S ( A.RIGHT );   \r
1227 END LAST1_S;\r
1228 \r
1229 (****************************************************************************)\r
1230 (* UPDATE THE GREATEST NUMBER OF VARKIND IN THE DIFINITION TREE AND CHANGE IT \r
1231    INTO SUBKIND *)\r
1232    \r
1233 UNIT LAST2_S : FUNCTION ( A1 : TNODE, I : INTEGER ) : INTEGER;\r
1234 VAR A : TNODE,\r
1235     K : INTEGER;\r
1236 BEGIN\r
1237      A := M1.FUN_REL.LEFT;\r
1238      FOR K := 1 TO I\r
1239      DO\r
1240        IF K=1 THEN A := A.LEFT\r
1241               ELSE A := A.RIGHT;\r
1242        FI;\r
1243      OD;\r
1244      IF A.KIND=SUBKIND THEN RESULT := A.IDENT\r
1245                        ELSE LAST_S := LAST_S+1;\r
1246                             RESULT := LAST_S;\r
1247                             CALL RENAME ( A1,A.KIND,A.IDENT );\r
1248      FI;\r
1249 END LAST2_S;\r
1250 \r
1251 (****************************************************************************)\r
1252 (* CHANGE VARKIND TO SUBKIND RESPECTIVELY *)\r
1253 \r
1254 UNIT RENAME : PROCEDURE ( A1 : TNODE, I,J : INTEGER );\r
1255 BEGIN\r
1256      IF A1=NONE THEN RETURN FI;\r
1257      IF A1.KIND=I AND A1.IDENT=J THEN A1.KIND := SUBKIND;\r
1258                                       A1.IDENT := LAST_S\r
1259      FI;\r
1260      CALL RENAME ( A1.LEFT,I,J );\r
1261      CALL RENAME ( A1.RIGHT,I,J );\r
1262 END RENAME;\r
1263 \r
1264 (****************************************************************************)\r
1265 (* REMOVE ALL EMPTY SEQUENTS AFTER CALLING SQUEEZE PROCEDURE *)\r
1266 \r
1267 UNIT CUT_SEQ : PROCEDURE ( A : SEQUENT );\r
1268 BEGIN\r
1269    IF A <> NONE THEN CALL CUT_SEQ ( A.NEXT ) ELSE RETURN FI; (* GO TO THE LAST \r
1270                                                                 SEQUENT *)\r
1271    IF A.PLEAF = NONE AND A.LLEAF = NONE THEN KILL ( A ) FI;  (* WHEN EMPTY \r
1272                                                                 REMOVE IT *)\r
1273 END CUT_SEQ;\r
1274 \r
1275 (****************************************************************************)\r
1276 (* FIND A CONNECTIVE NUMBER 'R' *)\r
1277 \r
1278 UNIT FINDCONN : FUNCTION ( A : SEQUENT , R , P : INTEGER ) : TNODE;\r
1279 VAR B : TNODE;\r
1280 BEGIN\r
1281      IF A = NONE THEN RETURN FI;\r
1282      CASE P\r
1283      WHEN 1: IF A.PLEAF = NONE THEN RETURN FI;\r
1284              B := A.PLEAF;\r
1285              CALL FUNCTOR ( R , B );\r
1286              RESULT := B;\r
1287      WHEN 0: IF A.LLEAF = NONE THEN RETURN FI;\r
1288              B := A.LLEAF;\r
1289              CALL FUNCTOR ( R , B );\r
1290              RESULT := B;\r
1291      ESAC;\r
1292 END FINDCONN;\r
1293 \r
1294 (****************************************************************************)\r
1295 (* SEARCH FOR A FUNCTOR *)\r
1296 \r
1297 UNIT FUNCTOR : PROCEDURE ( R : INTEGER ; INOUT B : TNODE );\r
1298      \r
1299 BEGIN\r
1300    IF B.KIND = BEGKIND ANDIF B.LEFT <> NONE ANDIF B.LEFT.IDENT = 1 ANDIF\r
1301       B.LEFT.KIND = SEMKIND THEN\r
1302       B := B.RIGHT;\r
1303    FI;\r
1304    WHILE B.KIND = VARPROG OR B.KIND = BVARPRO\r
1305    DO\r
1306       B := B.RIGHT;\r
1307    OD;\r
1308    IF B.KIND <> R THEN B := NONE FI;\r
1309 END FUNCTOR;\r
1310 \r
1311 (****************************************************************************)\r
1312 (* LOOK FOR MORE THAN ONE EQUALITIES IN A SEQUENT OF TYPE U=TERM *)\r
1313 \r
1314 UNIT SEARCH_U : FUNCTION ( A : SEQUENT ) : BOOLEAN;\r
1315 VAR I : INTEGER;\r
1316 BEGIN\r
1317    WHILE A <> NONE \r
1318    DO\r
1319      IF A.PLEAF <> NONE THEN\r
1320      IF A.PLEAF.KIND = EQUKIND ANDIF\r
1321         ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND ) THEN\r
1322         I := I + 1 ;\r
1323      FI;\r
1324      IF I = 2 THEN \r
1325         RESULT := TRUE; \r
1326         RETURN;\r
1327      FI;\r
1328      FI;\r
1329      A := A.NEXT;\r
1330    OD;\r
1331 END SEARCH_U;\r
1332 \r
1333 (****************************************************************************)\r
1334 (* CHECK WHETHER THERE IS IN A SEQUENT THE DEFINITION SYMBOL LIKE: FUNCTION, \r
1335    LITERAL ; OR PROGRAM *)\r
1336 \r
1337 UNIT CHECK_L_F_P : FUNCTION ( A : SEQUENT ) : BOOLEAN;\r
1338 BEGIN\r
1339     IF A <> NONE AND NOT ALFA THEN \r
1340        ALFA := CHECK_L_F_P_TN ( A.PLEAF ) OR CHECK_L_F_P_TN ( A.LLEAF );\r
1341        RESULT := ALFA OR CHECK_L_F_P ( A.NEXT );\r
1342     FI;\r
1343 END CHECK_L_F_P;\r
1344 \r
1345 (*****************************************************************************)\r
1346 (* CHECK WHETHER THERE IS IN A TNODE THE DEFINITION SYMBOL LIKE: FUNCTION, \r
1347    LITERAL ; OR PROGRAM *)\r
1348 \r
1349 UNIT CHECK_L_F_P_TN : FUNCTION ( C : TNODE ) : BOOLEAN;\r
1350 VAR BETA : BOOLEAN ;\r
1351 BEGIN\r
1352     IF C <> NONE THEN\r
1353        BETA := ( C.KIND > 2 AND C.KIND < 23 ) OR C.KIND = LT1KIND OR\r
1354                C.KIND = FN1KIND OR C.KIND = 4;\r
1355      RESULT := BETA OR CHECK_L_F_P_TN ( C.LEFT ) OR CHECK_L_F_P_TN ( C.RIGHT );\r
1356     FI;\r
1357 END;\r
1358 \r
1359 (****************************************************************************)\r
1360 (* WRITES A CHARACTER TO FILE *)\r
1361 \r
1362 UNIT PUTCH : PROCEDURE ( A : CHARACTER );\r
1363 BEGIN\r
1364     IF CHARSH >= LINLNG THEN \r
1365        WRITELN ;\r
1366        CHARSH := 0 \r
1367     FI;\r
1368     WRITE ( A );\r
1369     CHARSH := CHARSH + 1 \r
1370 END PUTCH;\r
1371 \r
1372 (****************************************************************************)\r
1373 \r
1374 \r
1375 (****************************************************************************)\r
1376 (* PRIMARY RULES AND FIRSTLY PROCEDURES AND FUNCTIONS APPLIED IN THE TREE   *) \r
1377 (****************************************************************************)\r
1378 \r
1379 (****************************************************************************)\r
1380 (* REPLACE IN SEQUENT A ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)\r
1381 \r
1382 UNIT REP_F_SEQ : PROCEDURE ( A : SEQUENT , N : INTEGER );\r
1383 BEGIN\r
1384     IF A = NONE THEN RETURN FI;\r
1385     CALL REP_FUN_N ( A.LLEAF , N );\r
1386     CALL REP_FUN_N ( A.PLEAF , N );\r
1387     CALL REP_F_SEQ ( A.NEXT , N );\r
1388 END REP_F_SEQ;\r
1389 \r
1390 (****************************************************************************)\r
1391 (* REPLACE IN TNODE C ALL FUNKIND WITH NUMBER N TO FN1KIND WITH NUMBER N *)\r
1392 \r
1393 UNIT REP_FUN_N : PROCEDURE ( C : TNODE , N : INTEGER );\r
1394 BEGIN\r
1395     IF C = NONE THEN RETURN FI;\r
1396     IF C.KIND=FUNKIND AND C.IDENT = N THEN C.KIND := FN1KIND FI;\r
1397     CALL REP_FUN_N ( C.LEFT , N );\r
1398     CALL REP_FUN_N ( C.RIGHT , N );\r
1399 END REP_FUN_N;\r
1400 \r
1401 (****************************************************************************)\r
1402 (* REPLACE IN TNODE C ALL FUNKIND TO FN1KIND *)\r
1403 \r
1404 UNIT REP_FUN : PROCEDURE ( C : TNODE );\r
1405 BEGIN\r
1406    IF C = NONE THEN RETURN FI;\r
1407    IF C.KIND = FUNKIND THEN C.KIND := FN1KIND FI;\r
1408    CALL REP_FUN ( C.LEFT );\r
1409    CALL REP_FUN ( C.RIGHT );\r
1410 END REP_FUN;\r
1411 \r
1412 (****************************************************************************)\r
1413 (* REPLACE ALL LITKIND WITH NUMBER N IN SEQUENT A TO LT1KIND *)\r
1414 \r
1415 UNIT REP_L_SEQ : PROCEDURE ( A :SEQUENT , N :INTEGER );\r
1416 BEGIN\r
1417     IF A = NONE THEN RETURN FI;\r
1418     CALL REP_LIT_N ( A.PLEAF , N );\r
1419     CALL REP_LIT_N ( A.LLEAF , N );\r
1420     CALL REP_L_SEQ ( A.NEXT , N );\r
1421 END REP_L_SEQ;\r
1422 \r
1423 (****************************************************************************)\r
1424 (* REPLACE ALL LITKIND IN TNODE C TO LT1KIND *)\r
1425 \r
1426 UNIT REP_LIT : PROCEDURE ( C : TNODE );\r
1427 BEGIN\r
1428    IF C = NONE THEN RETURN FI;\r
1429    IF C.KIND = LITKIND THEN C.KIND := LT1KIND FI;\r
1430    CALL REP_LIT ( C.LEFT );\r
1431    CALL REP_LIT ( C.RIGHT );\r
1432 END REP_LIT;\r
1433 \r
1434 (****************************************************************************)\r
1435 (* REPLACE ALL LITKIND WITH NUMBER N IN TNODE C TO LT1KIND *)\r
1436 \r
1437 UNIT REP_LIT_N : PROCEDURE ( C : TNODE , N : INTEGER );\r
1438 BEGIN\r
1439    IF C = NONE THEN RETURN FI;\r
1440    IF C.KIND = LITKIND AND C.IDENT = N  THEN C.KIND := LT1KIND FI;\r
1441    CALL REP_LIT_N ( C.LEFT , N );\r
1442    CALL REP_LIT_N ( C.RIGHT , N );\r
1443 END REP_LIT_N;\r
1444 \r
1445 (*****************************************************************************)\r
1446 (* REPLACE DEFINITION SYMBOL LIKE : FUNKIND AND LITKIND INTO FN1KIND AND \r
1447    LT1KIND RESPECTIVELY *)\r
1448 \r
1449 UNIT REP_F_L : PROCEDURE ( M3 : DEF );\r
1450 VAR M2 : DEF ;\r
1451 BEGIN\r
1452   M2 := M3;\r
1453   DO \r
1454     CASE M3.FUN_REL.KIND \r
1455       WHEN EQUKIND : CALL REP_FUN_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT ); \r
1456                                  (* REPLACE FUNKIND WITH PROPER NUMBERS *)\r
1457                                  (* INTO FN1KIND IN A DEFINITION TREE *)\r
1458                      CALL REP_F_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );\r
1459                                  (* DO THE SAME BUT IN DATA TREE *)\r
1460       WHEN EQVKIND : CALL REP_LIT_N ( M2.FUN_REL , M2.FUN_REL.LEFT.IDENT );\r
1461                                  (* REPLACE LITKIND WITH PROPER NUMBERS *)\r
1462                                  (* INTO LT1KIND IN A DEFINITION TREE *) \r
1463                      CALL REP_L_SEQ ( M.NEXT , M2.FUN_REL.LEFT.IDENT );\r
1464                                  (* DO THE SAME BUT IN DATA TREE *)\r
1465     ESAC;\r
1466     IF M2 = M3 THEN EXIT FI;\r
1467     M2 := M2.NEXT;\r
1468   OD;\r
1469 END REP_F_L;\r
1470 \r
1471 (*****************************************************************************)\r
1472 (* USE THE DEFINITION OF FUNCTION *)\r
1473 \r
1474 UNIT RULEDF_F : PROCEDURE ( M : POINTER, P : INTEGER, F_NUMBER : INTEGER );\r
1475 VAR A , A1 , ALR , C , B1 : TNODE,\r
1476     ALFA : BOOLEAN,\r
1477     B : SEQUENT;\r
1478 BEGIN\r
1479      B:=M.NEXT;\r
1480      CASE P\r
1481      WHEN 1:\r
1482           IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;\r
1483           A := B.PLEAF;\r
1484           DO\r
1485             WHILE A.KIND <> EQUKIND\r
1486             DO\r
1487               IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;\r
1488               B := B.NEXT;\r
1489               A := B.PLEAF;\r
1490             OD;\r
1491             IF FOUND_F ( B.PLEAF , B.PLEAF , A , ALR , ALFA , F_NUMBER ) THEN \r
1492                EXIT FI;\r
1493             IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;\r
1494             B := B.NEXT;\r
1495             A := B.PLEAF;          OD;\r
1496      WHEN 0:\r
1497           IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;\r
1498           A := B.LLEAF;\r
1499           DO\r
1500             WHILE A.KIND <> EQUKIND\r
1501             DO\r
1502               IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;\r
1503               B := B.NEXT;\r
1504               A := B.LLEAF;\r
1505             OD;\r
1506             IF FOUND_F ( B.LLEAF , B.LLEAF , A , ALR , ALFA , F_NUMBER ) THEN \r
1507                EXIT \r
1508             FI;\r
1509             IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;\r
1510             B := B.NEXT;\r
1511             A := B.LLEAF;\r
1512           OD;\r
1513      ESAC;\r
1514      C := ALR.RIGHT;                             (* C STORES RIGHT SIDE OF *)\r
1515                                                  (* OPERATION CONTAINING FUNCTION *)\r
1516      A1 := COPYTNODE ( M1.FUN_REL.LEFT.RIGHT );  (* REMEMBER K -TAU *)\r
1517      IF ALR.LEFT = NONE THEN                     (* IF THERE IS NO ARGUMENT *)\r
1518         B1 := A1\r
1519      ELSE\r
1520         B1 := NEW TNODE;\r
1521         CALL MAKE_SUB ( ALR.LEFT , A1 , B1 );    (* ALR.LEFT REFERS TO FIRST ARG *)\r
1522         CALL LIFT ( B1 , 1 , 0 );\r
1523      FI;\r
1524      CALL END_OF_P ( A1 );                       (* A1 REFERS TO THE END OF PROGRAM *)\r
1525                                                  (* BEFORE TAU *)\r
1526      IF A.LEFT = ALR THEN                        (* FUNCTION IS ON LEFT *)\r
1527         KILL ( A.LEFT );\r
1528         A.LEFT := A1.RIGHT                       (* JOIN TAU *)\r
1529      ELSE                                        (* FUNCTION IS ON RIGHT *) \r
1530         KILL ( A.RIGHT );\r
1531         A.RIGHT := A1.RIGHT;                     (* JOIN TAU *)\r
1532      FI;\r
1533      A1.RIGHT.RIGHT := C;                        (* JOIN U OR SOMETHING ELSE *)\r
1534      A1.RIGHT := NONE;\r
1535      CASE P\r
1536            WHEN 1 : A1 := B.PLEAF;               (* MOVE '=' BEYOND PROGRAM *)\r
1537                     B.PLEAF := B1;               (* ON RIGHT *)\r
1538                     CALL END_OF_PRG ( B1 );\r
1539                     B1.RIGHT := A1;\r
1540            WHEN 0 : A1 := B.LLEAF;               (* OR ON LEFT SIDE *)\r
1541                     B.LLEAF := B1;\r
1542                     CALL END_OF_PRG ( B1 );\r
1543                     B1.RIGHT := A1;\r
1544      ESAC\r
1545 END RULEDF_F;\r
1546 \r
1547 (*****************************************************************************)\r
1548 (* SEARCH FUNCTION FN1KIND IN A TREE TO BE SUBSTITUTED ON *)\r
1549 \r
1550 UNIT FOUND_F : FUNCTION ( B , B1 : TNODE ; INOUT C , D : TNODE , ALFA : BOOLEAN ;\r
1551                          F_NUMBER : INTEGER ) : BOOLEAN;\r
1552 BEGIN\r
1553    IF B <> NONE THEN\r
1554       IF B.KIND = FN1KIND AND B.IDENT = F_NUMBER  THEN \r
1555          RESULT := TRUE ; \r
1556          IF NOT ALFA THEN \r
1557             ALFA := TRUE;\r
1558             D := B;\r
1559             C := B1;\r
1560          FI;\r
1561          RETURN \r
1562       ELSE\r
1563     RESULT := FOUND_F ( B.LEFT , B , C , D , ALFA , F_NUMBER ) \r
1564               OR FOUND_F ( B.RIGHT , B , C , D , ALFA , F_NUMBER )\r
1565       FI;\r
1566    FI;\r
1567 END FOUND_F;      \r
1568        \r
1569 (****************************************************************************)\r
1570 (* MAKE THE SUBSTITUTION *)\r
1571 \r
1572 UNIT MAKE_SUB:PROCEDURE ( D , A1 , A : TNODE );\r
1573 VAR F,G,E:TNODE,\r
1574     I : INTEGER;\r
1575 BEGIN    \r
1576      IF D.RIGHT = NONE THEN                      (* ONLY ONE ARGUMENT *)\r
1577         E := NEW TNODE;\r
1578         A.LEFT:=E;\r
1579         E.KIND := VARPROG;\r
1580         E.LEFT := D;\r
1581         E.IDENT :=LAST2_S ( A1 , 1 );\r
1582         E.RIGHT := A1;\r
1583         RETURN;\r
1584      FI;\r
1585      F := NEW TNODE;                             (* MORE THAN ONE ARGUMENTS *)\r
1586      F.KIND := BEGKIND;\r
1587      F.IDENT := ENDKIND;     \r
1588      WHILE D <> NONE\r
1589      DO                                          (* VIEW ALL ARGUMENTS AND *)\r
1590                                                  (* MAKE RELEVANT SUBSTITUTION *)\r
1591                                                  (* CREATE SUBSTITUTION CELLS *)\r
1592                                                  (* FILL THEM *) \r
1593                                                  (* AND JOIN THEM- XI:=TI *)\r
1594        G := NEW TNODE;\r
1595        G.KIND := SEMKIND;\r
1596        G.IDENT := 1;                             (* SIGN THAT SUBSTITUTION *)\r
1597                                                  (* SHOULD BE DONE SIMULTANEOUSLY *)\r
1598        E:=NEW TNODE;\r
1599        G.LEFT := E;\r
1600        E.KIND := VARPROG;                               \r
1601        E.LEFT := D;                              (* ASSOCIATE VARIABLE WITH ITS term XI:=TI *)       \r
1602        E.RIGHT := D.RIGHT;                       \r
1603        D.RIGHT := NONE;\r
1604        IF I=0 THEN \r
1605           A.LEFT := F; \r
1606           I := 1; \r
1607           F.LEFT := G;\r
1608        ELSE \r
1609           A.RIGHT := G;\r
1610           I := I+1;\r
1611        FI;\r
1612        E.IDENT := LAST2_S ( A1 , I );            (* ASSIGN VARPROG NEW NUMBER \r
1613                                                     AND UPDATE LIST OF VARPROG'S *)\r
1614        A := G;\r
1615        D := E.RIGHT;\r
1616        E.RIGHT := NONE;\r
1617      OD;\r
1618      CALL LIFT ( G , 1 , 0 );\r
1619      F.RIGHT := A1;\r
1620 END MAKE_SUB;     \r
1621 \r
1622 (****************************************************************************)\r
1623 (* USE A DEFINITION OF RELATION *)\r
1624 \r
1625 UNIT RULEDF_L : PROCEDURE ( M : POINTER , P : INTEGER , N : INTEGER );\r
1626 VAR A,A1,D : TNODE,\r
1627     B : SEQUENT;\r
1628 BEGIN\r
1629      B := M.NEXT;\r
1630      CASE P\r
1631      WHEN 1:\r
1632           IF B=NONE ORIF B.PLEAF=NONE THEN RETURN FI;\r
1633           A := B.PLEAF;\r
1634           WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND\r
1635           DO\r
1636             IF B.NEXT=NONE ORIF B.NEXT.PLEAF=NONE THEN RETURN FI;\r
1637             B := B.NEXT;\r
1638             A := B.PLEAF;\r
1639           OD;\r
1640      WHEN 0:\r
1641           IF B=NONE ORIF B.LLEAF=NONE THEN RETURN FI;\r
1642           A := B.LLEAF;\r
1643           WHILE ( A.KIND <> LT1KIND OR A.IDENT <> N ) AND A.KIND <> EQVKIND\r
1644           DO\r
1645             IF B.NEXT=NONE ORIF B.NEXT.LLEAF=NONE THEN RETURN FI;\r
1646             B := B.NEXT;\r
1647             A := B.LLEAF;\r
1648           OD;\r
1649      ESAC;\r
1650      IF A.KIND = EQVKIND THEN A := A.LEFT FI;\r
1651      D := A.LEFT;                                (* FIRST ARGUMENT *)\r
1652      A1 := COPY ( M1.FUN_REL.RIGHT );            (* REMEMBER K-ALFA *)\r
1653      IF D=NONE THEN\r
1654         A.RIGHT := A1;\r
1655         CALL LIFT ( A , 1 , 1 );\r
1656         CALL SWEEP ( A );\r
1657         RETURN;\r
1658      FI;\r
1659      CALL MAKE_SUB ( D , A1 , A );\r
1660      CASE P\r
1661         WHEN 0 : CALL LIFT ( B.LLEAF.LEFT, 1, 0 );\r
1662                  CALL SWEEP ( B.LLEAF );\r
1663         WHEN 1 : CALL LIFT ( B.PLEAF.LEFT, 1, 0 );\r
1664                  CALL SWEEP ( B.PLEAF );\r
1665      ESAC;      \r
1666           CASE P \r
1667         WHEN 0 : A := B.LLEAF;\r
1668         WHEN 1 : A := B.PLEAF;\r
1669      ESAC;\r
1670      IF A.LEFT.KIND = BEGKIND ANDIF A.LEFT.LEFT <> NONE ANDIF \r
1671         A.LEFT.LEFT.KIND = SEMKIND ANDIF A.LEFT.LEFT.IDENT = 1 THEN\r
1672         D := A.LEFT;                             (* MOVE OUT PARALLEL *)\r
1673         A.LEFT := D.RIGHT;                       (* SUBSTITUTION BEYOND *)\r
1674         D.RIGHT := A;                            (* EQUIVALENCE *)\r
1675         CASE P \r
1676            WHEN 0 : B.LLEAF := D;\r
1677            WHEN 1 : B.PLEAF := D;\r
1678         ESAC;\r
1679      FI;\r
1680 \r
1681 END RULEDF_L;\r
1682 \r
1683 (*****************************************************************************)\r
1684 \r
1685 \r
1686 (*****************************************************************************)\r
1687 (*                              AID RULES                                    *)\r
1688 (*****************************************************************************)\r
1689 \r
1690 (****************************************************************************)\r
1691 (* THROWING AWAY THE SEQUENCE OF SEQUENTS INCLUDING 0 ON LEFT SIDE\r
1692    OR 1 ON RIGHT SIDE *)\r
1693 \r
1694 UNIT THROW_RUBBISH : PROCEDURE ( M : POINTER );\r
1695 VAR A : SEQUENT;\r
1696 BEGIN\r
1697      IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;\r
1698      A := M.NEXT;\r
1699      WHILE A<>NONE\r
1700      DO\r
1701        IF A.PLEAF<>NONE THEN\r
1702           IF A.PLEAF.IDENT=1 ANDIF A.PLEAF.KIND=LOGKIND THEN\r
1703              CALL ERASE_SEQ ( M.NEXT );          (* IF THERE IS TRUE ON RIGHT *)\r
1704              EXIT;                               (* SIDE, THEN REMOVE ALL SEQUENTS *)\r
1705           FI;\r
1706           IF DEF_LIT = 1 ANDIF A.PLEAF.KIND = LOGKIND ANDIF A.PLEAF.IDENT = 0 THEN\r
1707              KILL ( A.PLEAF );\r
1708           FI;\r
1709        FI;\r
1710        IF A.LLEAF<>NONE THEN\r
1711           IF A.LLEAF.IDENT=0 ANDIF A.LLEAF.KIND=LOGKIND THEN \r
1712              CALL ERASE_SEQ ( M.NEXT );          (* IF THERE IS FALSE ON LEFT *) \r
1713              EXIT;                               (* SIDE, THEN REMOVE ALL SEQUENTS *)\r
1714           FI;\r
1715           IF DEF_LIT = 1 ANDIF A.LLEAF.KIND = LOGKIND ANDIF A.LLEAF.IDENT = 1 THEN\r
1716              KILL ( A.LLEAF );\r
1717           FI;                                   \r
1718        FI;\r
1719        A := A.NEXT;                              (* OTHERWISE GO ON FURTHER *)\r
1720      OD;\r
1721 END THROW_RUBBISH;\r
1722 \r
1723 (****************************************************************************)\r
1724 (* CALCULATE STANDARD FUNCTIONS *,+,-,^,/ *)\r
1725 \r
1726 UNIT RULEVAL : PROCEDURE ( A:TNODE; INOUT ALFA:BOOLEAN );\r
1727 VAR BETA : BOOLEAN,\r
1728     B,C  : TNODE;\r
1729 BEGIN\r
1730      BETA := TRUE;                                              \r
1731      IF A=NONE THEN RETURN FI;                  \r
1732      IF A.KIND=ARIKIND THEN                      (* MUST BEGIN WITH FUNCTOR *)\r
1733         CALL CHECKCHAR ( A.LEFT , BETA );        (* CHECK WHETHER IN THE FOLLOWING\r
1734                                                     TREE THERE ARE ONLY STANDARD\r
1735                                                     FUNCTORS AND DIGITS *)\r
1736         IF BETA THEN                             (* IF YES *)\r
1737            BETA := FALSE;\r
1738            CALL FUNCHECK ( A , BETA );\r
1739            A.IDENT := COUNT ( A ) ;              (* COUNT THIS EXPRESSION *)\r
1740            IF BETA THEN \r
1741               A.KIND := CN1KIND\r
1742            ELSE \r
1743               A.KIND := CNTKIND;\r
1744            FI;\r
1745            CALL ERASE ( A.LEFT );                (* WHEN DONE REMOVE IT *)\r
1746            ALFA := TRUE;\r
1747            RETURN\r
1748         ELSE                                     (* MAKE SPECIAL ARITHMETIC *)\r
1749            BETA := TRUE;                         (* OPERATIONS LIKE : X+X A.S.O. *)\r
1750            B := COPYTNODE ( A.LEFT );\r
1751            C := B.RIGHT;\r
1752            B.RIGHT := NONE;\r
1753            CALL COMPARE ( B , C , BETA );        (* COMPARE TWO TREES *)\r
1754            IF BETA THEN                          (* THEY ARE EQUAL *)\r
1755               B.RIGHT := C;\r
1756               CALL ERASE ( B );\r
1757               CASE A.IDENT \r
1758                  WHEN 42 : A.IDENT := 94;        (* TERM*TERM -> TERM^2 *)\r
1759                            A.LEFT.RIGHT.KIND := CNTKIND;\r
1760                            A.LEFT.RIGHT.IDENT := 2;\r
1761                            CALL ERASE ( A.LEFT.RIGHT.LEFT );\r
1762                  WHEN 43 : A.IDENT := 42;        (* TERM+TERM -> 2*TERM *)\r
1763                            A.LEFT.KIND := CNTKIND;\r
1764                            A.LEFT.IDENT := 2;\r
1765                            CALL ERASE ( A.LEFT.LEFT );\r
1766               ESAC;                \r
1767            FI;\r
1768         FI;\r
1769      FI;\r
1770      CALL RULEVAL ( A.LEFT,ALFA );\r
1771      CALL RULEVAL ( A.RIGHT,ALFA );\r
1772 END RULEVAL;\r
1773 \r
1774 (****************************************************************************)\r
1775 (* CALLS COUNT_0_1 UNTIL IT IS NOT USELESS *)\r
1776 \r
1777 UNIT ZEROS_AND_ONES : PROCEDURE ( A : TNODE ; ALFA : BOOLEAN );\r
1778 VAR BETA : BOOLEAN;         (* BETA MEANS THAT COUNT_0_1 IS STILL WORKING *)\r
1779 BEGIN\r
1780      BETA := TRUE;\r
1781      WHILE BETA\r
1782      DO\r
1783        BETA := FALSE;\r
1784        CALL COUNT_0_1 ( A , BETA );\r
1785        ALFA := ALFA OR BETA;\r
1786      OD;\r
1787 END ZEROS_AND_ONES;\r
1788 \r
1789 (****************************************************************************)\r
1790 (* DOES ALL ARITHMETIC OPERATIONS *)\r
1791 \r
1792 UNIT COUNT_0_1 : PROCEDURE ( B : TNODE ; INOUT ALEF : BOOLEAN );\r
1793 VAR BETA : BOOLEAN;\r
1794 BEGIN\r
1795      IF B=NONE THEN RETURN FI;\r
1796      IF B.KIND=ARIKIND THEN\r
1797         BETA := FALSE;\r
1798         IF B.LEFT.KIND = CNTKIND OR B.LEFT.KIND = CN1KIND THEN\r
1799         CASE B.LEFT.IDENT\r
1800              WHEN 0: CASE B.IDENT\r
1801                           WHEN 42,94:CALL FUNCHECK ( B.LEFT.RIGHT , BETA );\r
1802                                   IF B.IDENT = 94 AND B.LEFT.RIGHT.IDENT = 0 \r
1803                                      AND B.LEFT.RIGHT.KIND = CNTKIND THEN\r
1804                                      CALL EXCEPTIONS ( 4 )\r
1805                                   ELSE\r
1806                                   IF BETA THEN\r
1807                                      B.KIND := CN1KIND\r
1808                                   ELSE\r
1809                                      B.KIND := CNTKIND;\r
1810                                   FI;\r
1811                                   B.IDENT := 0;\r
1812                                   CALL ERASE ( B.LEFT );\r
1813                                   ALEF := TRUE;\r
1814                                   RETURN;\r
1815                                   FI;\r
1816                           WHEN 43:B.LEFT.RIGHT.RIGHT := B.RIGHT;\r
1817                                   CALL LIFT ( B,1,0 );\r
1818                                   CALL LIFT ( B,1,1 );\r
1819                                   ALEF := TRUE;\r
1820                                   RETURN;\r
1821                           WHEN 47:IF B.LEFT.RIGHT.KIND=CNTKIND AND\r
1822                                           B.LEFT.RIGHT.IDENT = 0 THEN\r
1823                                      CALL EXCEPTIONS ( 2 )\r
1824                                   ELSE\r
1825                                      CALL FUNCHECK ( B.LEFT.RIGHT,BETA );\r
1826                                      IF BETA THEN\r
1827                                         B.KIND := CN1KIND;\r
1828                                      ELSE\r
1829                                         B.KIND := CNTKIND;\r
1830                                      FI;\r
1831                                      B.IDENT := 0;\r
1832                                      CALL ERASE ( B.LEFT );\r
1833                                      ALEF := TRUE;\r
1834                                      RETURN;\r
1835                                   FI;\r
1836                           WHEN 45:CALL LIFT ( B.LEFT,1,1 );\r
1837                                   ALEF := TRUE;\r
1838                                   RETURN;\r
1839                      ESAC;\r
1840              WHEN 1: CASE B.IDENT\r
1841                           WHEN 42:B.LEFT.RIGHT.RIGHT := B.RIGHT;\r
1842                                   CALL LIFT ( B,1,0 );\r
1843                                   CALL LIFT ( B,1,1 );\r
1844                                   ALEF := TRUE;\r
1845                                   RETURN;\r
1846                           WHEN 94:CALL FUNCHECK ( B.LEFT.RIGHT,BETA );\r
1847                                   IF BETA THEN\r
1848                                      B.KIND := CN1KIND;\r
1849                                   ELSE\r
1850                                      B.KIND := CNTKIND;\r
1851                                   FI;\r
1852                                   B.IDENT := 1;\r
1853                                   CALL ERASE ( B.LEFT );\r
1854                                   ALEF := TRUE;\r
1855                                   RETURN;\r
1856                           WHEN 47:IF B.LEFT.RIGHT.IDENT=1 THEN\r
1857                                      B.KIND := CNTKIND;\r
1858                                      B.IDENT := 1;\r
1859                                      CALL ERASE ( B.LEFT );\r
1860                                      ALEF := TRUE;\r
1861                                   FI;\r
1862                                   RETURN;\r
1863                      ESAC;\r
1864         ESAC\r
1865        ELSE\r
1866         IF B.LEFT.RIGHT.KIND = CNTKIND OR B.LEFT.RIGHT.KIND = CN1KIND THEN\r
1867         CASE B.LEFT.RIGHT.IDENT\r
1868              WHEN 0: CASE B.IDENT\r
1869                           WHEN 42:CALL FUNCHECK ( B.LEFT , BETA );\r
1870                                   IF BETA THEN\r
1871                                      B.KIND := CN1KIND;\r
1872                                   ELSE\r
1873                                      B.KIND := CNTKIND;\r
1874                                   FI;\r
1875                                   B.IDENT := 0;\r
1876                                   CALL ERASE ( B.LEFT );\r
1877                                   ALEF := TRUE;\r
1878                                   RETURN;\r
1879                           WHEN 43:CALL ERASE ( B.LEFT.RIGHT );\r
1880                                   B.LEFT.RIGHT := B.RIGHT;\r
1881                                   CALL LIFT ( B,1,0 );\r
1882                                   ALEF := TRUE;\r
1883                                   RETURN;\r
1884                           WHEN 94:CALL FUNCHECK ( B.LEFT,BETA );\r
1885                                   IF BETA THEN\r
1886                                      B.KIND := CN1KIND;\r
1887                                   ELSE\r
1888                                      B.KIND := CNTKIND;\r
1889                                   FI;\r
1890                                   B.IDENT := 1;\r
1891                                   CALL ERASE ( B.LEFT );\r
1892                                   ALEF := TRUE;\r
1893                                   RETURN;\r
1894                           WHEN 47:CALL EXCEPTIONS ( 3 );\r
1895                           WHEN 45:KILL ( B.LEFT.RIGHT );\r
1896                                   B.LEFT.RIGHT := B.RIGHT;\r
1897                                   CALL LIFT ( B,1,0 );\r
1898                                   ALEF := TRUE;\r
1899                                   RETURN;\r
1900                      ESAC;\r
1901              WHEN 1: CASE B.IDENT\r
1902                         WHEN 42,47,94:B.LEFT.RIGHT.RIGHT := B.RIGHT;\r
1903                                       CALL LIFT ( B,1,0 );\r
1904                                       CALL LIFT ( B.RIGHT,1,1 );\r
1905                                       ALEF := TRUE;\r
1906                                       RETURN;\r
1907                         ESAC;\r
1908          ESAC;\r
1909          FI;\r
1910         FI;\r
1911       FI;\r
1912         CALL COUNT_0_1 ( B.LEFT,ALEF );\r
1913         CALL COUNT_0_1 ( B.RIGHT,ALEF );\r
1914 END COUNT_0_1;\r
1915 \r
1916 (****************************************************************************)\r
1917 (* CHECK WHETHER THERE IS A FN1KIND OR CN1KIND IN A TREE *)\r
1918 (* FN1KIND MEANS THE NAME OF FUNCTION DEFINED BY A PROCEDURE OF THE\r
1919    FORM F(X)=KT *)\r
1920 \r
1921 UNIT FUNCHECK : PROCEDURE ( C : TNODE ; INOUT BETA : BOOLEAN );\r
1922 BEGIN\r
1923      IF C = NONE THEN RETURN FI;\r
1924      IF C.KIND = FN1KIND OR C.KIND = CN1KIND THEN \r
1925         BETA := TRUE;\r
1926         RETURN; \r
1927      FI;\r
1928      CALL FUNCHECK ( C.LEFT , BETA );\r
1929      CALL FUNCHECK ( C.RIGHT , BETA );\r
1930 END FUNCHECK;               \r
1931 \r
1932 (****************************************************************************)\r
1933 (* TERM=TERM CONVERTS TO LOGICAL 1 *)\r
1934 \r
1935 UNIT RULEIDE : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );\r
1936 VAR A,B  : TNODE,\r
1937     BETA : BOOLEAN;\r
1938 BEGIN\r
1939   IF C=NONE THEN RETURN FI;\r
1940   BETA := TRUE;\r
1941   IF C.KIND=EQUKIND THEN \r
1942      CASE C.LEFT.KIND \r
1943         WHEN VARPROG , \r
1944              BVARPRO : A := C.LEFT;\r
1945                        CALL END_OF_S ( A,B );\r
1946                        B := A.RIGHT;\r
1947                        A.RIGHT := NONE;\r
1948                        CALL COMPARE ( C.LEFT,B,BETA );\r
1949                        A.RIGHT := B;\r
1950         WHEN IFFKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT ;\r
1951                        C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := NONE;\r
1952                        CALL COMPARE ( C.LEFT , A , BETA );\r
1953                        C.LEFT.RIGHT.RIGHT.RIGHT.RIGHT := A;                    \r
1954         WHEN BEGKIND : A := C.LEFT.RIGHT.RIGHT;\r
1955                        C.LEFT.RIGHT.RIGHT := NONE;\r
1956                        CALL COMPARE ( C.LEFT, A ,BETA );\r
1957                        C.LEFT.RIGHT.RIGHT := A;\r
1958         WHEN WHIKIND : A := C.LEFT.RIGHT.RIGHT.RIGHT;\r
1959                        C.LEFT.RIGHT.RIGHT.RIGHT := NONE;\r
1960                        CALL COMPARE ( C.LEFT , A , BETA );\r
1961                        C.LEFT.RIGHT.RIGHT.RIGHT := A;\r
1962         OTHERWISE      A := C.LEFT.RIGHT;        (* STORE RIGHT ARGUMENT *)\r
1963                        C.LEFT.RIGHT := NONE;\r
1964                        CALL COMPARE ( C.LEFT , A , BETA );\r
1965                        C.LEFT.RIGHT := A;\r
1966      ESAC;\r
1967      IF BETA THEN \r
1968         C.KIND  := LOGKIND;\r
1969         C.IDENT := 1;\r
1970         CALL ERASE ( C.LEFT );\r
1971         ALFA := TRUE;\r
1972     FI;\r
1973   FI;\r
1974 END RULEIDE;\r
1975 \r
1976 (*****************************************************************************)\r
1977 (* COMPARE THOROUGHLY TWO TREES *)\r
1978 \r
1979 UNIT COMPARE : PROCEDURE ( A,B : TNODE ; INOUT BETA : BOOLEAN );\r
1980 BEGIN\r
1981         IF A <> NONE AND B <> NONE THEN\r
1982            IF A.KIND=B.KIND AND A.IDENT=B.IDENT THEN \r
1983               CALL COMPARE ( A.LEFT,B.LEFT,BETA );\r
1984               CALL COMPARE ( A.RIGHT,B.RIGHT,BETA )\r
1985            ELSE\r
1986               BETA := FALSE;\r
1987               RETURN\r
1988            FI\r
1989         ELSE\r
1990            IF A <> NONE OR B <> NONE THEN BETA := FALSE FI;  \r
1991         FI\r
1992 END COMPARE;      \r
1993 \r
1994 (****************************************************************************)\r
1995 (* TERM1 <> TERM2 IN THE STANDARD INTERPRETATION CONVERTS TO 0 *)\r
1996 \r
1997 UNIT RULEIDT : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );\r
1998 VAR BETA : BOOLEAN;\r
1999 BEGIN\r
2000      BETA := TRUE;\r
2001      IF C = NONE THEN RETURN FI;\r
2002      IF C.KIND = EQUKIND THEN  \r
2003         CALL CHECKCHAR ( C.LEFT,BETA );\r
2004         IF BETA THEN \r
2005            IF COUNT( C.LEFT ) <> COUNT( C.LEFT.RIGHT ) THEN\r
2006               C.KIND := LOGKIND;\r
2007               C.IDENT := 0;\r
2008               CALL ERASE ( C.LEFT );\r
2009               ALFA := TRUE;\r
2010            FI;\r
2011         FI;\r
2012      FI;\r
2013 END RULEIDT;\r
2014 \r
2015 (****************************************************************************)\r
2016 (* CALCULATOR *)\r
2017 \r
2018 UNIT COUNT : FUNCTION ( A : TNODE ) : INTEGER;\r
2019 VAR BASIS,I,POWER,LIMIT : INTEGER;\r
2020 BEGIN\r
2021     IF A.KIND <> ARIKIND THEN\r
2022        RESULT := A.IDENT\r
2023     ELSE\r
2024        CASE A.IDENT\r
2025          WHEN 42 : RESULT := COUNT( A.LEFT ) * COUNT( A.LEFT.RIGHT );\r
2026          WHEN 43 : RESULT := COUNT( A.LEFT ) + COUNT( A.LEFT.RIGHT );\r
2027          WHEN 47 : RESULT := COUNT( A.LEFT ) DIV COUNT( A.LEFT.RIGHT );\r
2028          WHEN 45 : RESULT := COUNT( A.LEFT ) - COUNT( A.LEFT.RIGHT );\r
2029          WHEN 94 : IF A.LEFT.RIGHT.IDENT=0 THEN \r
2030                       RESULT := 1\r
2031                    ELSE\r
2032                       POWER := 1;\r
2033                       BASIS := COUNT ( A.LEFT );\r
2034                       LIMIT := COUNT ( A.LEFT.RIGHT );\r
2035                       FOR I:=1 TO LIMIT\r
2036                       DO\r
2037                         POWER := POWER * BASIS;\r
2038                       OD;\r
2039                       RESULT := POWER;\r
2040                    FI;\r
2041        ESAC\r
2042     FI; \r
2043 END COUNT;\r
2044 \r
2045 (****************************************************************************)\r
2046 (* CHECK WHETHER TERM IS BUILT ONLY BY STANDARD FUNCTORS *)\r
2047 \r
2048 UNIT CHECKCHAR : PROCEDURE ( A : TNODE ; INOUT BETA : BOOLEAN );\r
2049 BEGIN\r
2050      IF A<>NONE THEN\r
2051         IF A.KIND=ARIKIND OR A.KIND=CNTKIND OR A.KIND=CN1KIND THEN\r
2052            CALL CHECKCHAR ( A.LEFT , BETA );\r
2053            CALL CHECKCHAR ( A.RIGHT , BETA )\r
2054         ELSE\r
2055            BETA := FALSE;\r
2056            RETURN\r
2057         FI;   \r
2058      FI;\r
2059 END CHECKCHAR;\r
2060 \r
2061 (****************************************************************************)\r
2062 (* A HELP FOR DUST_BIN PROCEDURE , MANAGE THE VERY SIMPLE BOOLEAN OPERATIONS *)\r
2063 \r
2064 UNIT DUST : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );\r
2065 BEGIN\r
2066      CASE C.KIND\r
2067           WHEN CONKIND: IF C.LEFT.KIND=LOGKIND THEN\r
2068                            CASE C.LEFT.IDENT\r
2069                              WHEN 1: CALL ERASE ( C.LEFT );\r
2070                                      CALL LIFT ( C,1,1 );\r
2071                                      ALFA := TRUE;\r
2072                              WHEN 0: CALL ERASE ( C.RIGHT );\r
2073                                      CALL LIFT ( C,1,0 );\r
2074                                      ALFA := TRUE;\r
2075                            ESAC;\r
2076                            RETURN;\r
2077                         FI;\r
2078                         IF C.RIGHT.KIND=LOGKIND THEN\r
2079                            CASE C.RIGHT.IDENT\r
2080                              WHEN 1: CALL ERASE ( C.RIGHT );\r
2081                                      CALL LIFT ( C,1,0 );\r
2082                                      ALFA := TRUE;\r
2083                              WHEN 0: CALL ERASE ( C.LEFT );\r
2084                                      CALL LIFT ( C,1,1 );\r
2085                                      ALFA := TRUE;\r
2086                            ESAC;\r
2087                            RETURN;\r
2088                         FI;                     \r
2089           WHEN DISKIND: IF C.LEFT.KIND=LOGKIND THEN\r
2090                            CASE C.LEFT.IDENT\r
2091                              WHEN 1: CALL ERASE ( C.RIGHT );\r
2092                                      CALL LIFT ( C,1,0 );\r
2093                                      ALFA := TRUE;\r
2094                              WHEN 0: CALL ERASE ( C.LEFT );\r
2095                                      CALL LIFT ( C,1,1 );\r
2096                                      ALFA := TRUE;\r
2097                            ESAC;\r
2098                            RETURN;\r
2099                         FI;\r
2100                         IF C.RIGHT.KIND=LOGKIND THEN\r
2101                            CASE C.RIGHT.IDENT\r
2102                              WHEN 1: CALL ERASE ( C.LEFT );\r
2103                                      CALL LIFT ( C,1,1 );\r
2104                                      ALFA := TRUE;\r
2105                              WHEN 0: CALL ERASE ( C.RIGHT );\r
2106                                      CALL LIFT ( C,1,0 );\r
2107                                      ALFA := TRUE; \r
2108                            ESAC;\r
2109                            RETURN;\r
2110                         FI;\r
2111           WHEN NEGKIND: IF C.LEFT.KIND=LOGKIND THEN\r
2112                            CASE C.LEFT.IDENT\r
2113                              WHEN NEGKIND: CALL LIFT ( C,2,0 );\r
2114                                            ALFA := TRUE;\r
2115                              WHEN 1: CALL LIFT ( C,1,0 );\r
2116                                      C.IDENT:=0;\r
2117                                      ALFA := TRUE;\r
2118                              WHEN 0: CALL LIFT ( C,1,0 );\r
2119                                      C.IDENT:=1;\r
2120                                      ALFA := TRUE;\r
2121                            ESAC;\r
2122                            RETURN;\r
2123                         FI;\r
2124           WHEN IMPKIND : IF C.LEFT.KIND=LOGKIND THEN \r
2125                            CASE C.LEFT.IDENT\r
2126                              WHEN 1: CALL ERASE ( C.LEFT );\r
2127                                      CALL LIFT ( C,1,1 );\r
2128                                      ALFA := TRUE;\r
2129                              WHEN 0: C.KIND := LOGKIND;\r
2130                                      C.IDENT:=1;\r
2131                                      CALL ERASE ( C.LEFT );\r
2132                                      CALL ERASE ( C.RIGHT );\r
2133                                      ALFA := TRUE;\r
2134                            ESAC;\r
2135                            RETURN;\r
2136                         FI;\r
2137                         IF C.RIGHT.KIND=LOGKIND THEN\r
2138                            CASE C.RIGHT.IDENT\r
2139                              WHEN 1: C.KIND := LOGKIND;\r
2140                                      C.IDENT := 1;\r
2141                                      CALL ERASE ( C.LEFT );\r
2142                                      CALL ERASE ( C.RIGHT );\r
2143                                      ALFA := TRUE;\r
2144                              WHEN 0: C.KIND:=NEGKIND;\r
2145                                      CALL ERASE ( C.RIGHT );\r
2146                                      ALFA := TRUE;\r
2147                            ESAC;\r
2148                            RETURN;\r
2149                        FI;\r
2150      ESAC;\r
2151 END DUST;\r
2152 \r
2153 (****************************************************************************)\r
2154 (* CALLED BY SWEEP PROCEDURE *)\r
2155 \r
2156 UNIT DUST_BIN : PROCEDURE ( C : TNODE ; INOUT ALFA : BOOLEAN );\r
2157 BEGIN\r
2158      IF C = NONE THEN RETURN FI;\r
2159      CALL RULEVAL ( C,ALFA );                    (* COUNT ARITHMETIC EXPRESSIONS : '1+2 -> 3' *)\r
2160      CALL ZEROS_AND_ONES ( C,ALFA );             (* COUNT EXPRESSIONS E.G. 0*X *)\r
2161      CALL RULEIDT ( C,ALFA );                    (* TERM1 <> TERM2 -> FALSE *)\r
2162      CALL RULEIDE ( C,ALFA );                    (* TERM1 IDENTICAL WITH TERM2 -> TRUE *)\r
2163      CALL DUST ( C,ALFA );                       (* SIMPLIFY BOOLEAN EXPRESSIONS *)\r
2164      CALL DUST_BIN ( C.LEFT,ALFA );\r
2165      CALL DUST_BIN ( C.RIGHT,ALFA );\r
2166  END DUST_BIN;\r
2167 \r
2168 (****************************************************************************)\r
2169 (* MANAGE THE SWEEPING SYSTEM IN A TREE , CALL DUST_BIN PROCEDURE *)\r
2170 \r
2171 UNIT SWEEP : PROCEDURE ( C : TNODE );\r
2172 VAR ALFA : BOOLEAN;\r
2173 BEGIN\r
2174     ALFA := TRUE;\r
2175     WHILE ALFA          \r
2176     DO                                           (* SWEEP IF IT IS POSSIBLE *)\r
2177       ALFA := FALSE;\r
2178       CALL DUST_BIN ( C , ALFA );                (* MAKE IT AND UPDATE ALFA *)\r
2179     OD;\r
2180 END SWEEP;\r
2181 \r
2182 (****************************************************************************)\r
2183 (* SQUEEZE A LIST OF SEQUENTS BY GETTING RID OF ALL THE HOLES *)\r
2184 \r
2185 UNIT SQUEEZE : PROCEDURE ( M : POINTER , P : INTEGER );\r
2186 VAR A,B : SEQUENT;\r
2187 BEGIN\r
2188      IF M=NONE ORIF M.NEXT=NONE ORIF LAST (M,P)=NONE THEN RETURN FI;\r
2189      A := FIRSTHOLE ( M , P );\r
2190      B := NEXTNODE ( A , P );\r
2191      WHILE LAST(M,P).NEXT <> A\r
2192      DO\r
2193        CASE P\r
2194                WHEN 1: A.PLEAF := B.PLEAF;\r
2195                        B.PLEAF := NONE;\r
2196                WHEN 0: A.LLEAF := B.LLEAF;\r
2197                        B.LLEAF := NONE;\r
2198        ESAC;\r
2199        B := NEXTNODE ( A.NEXT , P );\r
2200        A := FIRSTHOLE ( M , P );\r
2201      OD;\r
2202 END SQUEEZE;\r
2203 \r
2204 (****************************************************************************)\r
2205 (* SEARCH FOR THE FIRST NON-EMPTY TNODE AFTER THE FIRST HOLE *)\r
2206 \r
2207 UNIT NEXTNODE : FUNCTION ( U : SEQUENT , P : INTEGER ) : SEQUENT;\r
2208 VAR ALFA : BOOLEAN;\r
2209 BEGIN\r
2210      IF U=NONE THEN RETURN FI;\r
2211      WHILE U <> NONE AND NOT ALFA\r
2212      DO\r
2213        CASE P\r
2214             WHEN 1:IF U.PLEAF <> NONE THEN\r
2215                       RESULT := U;\r
2216                       ALFA := TRUE\r
2217                    ELSE\r
2218                       U := U.NEXT;\r
2219                    FI;\r
2220             WHEN 0:IF U.LLEAF <> NONE THEN\r
2221                       RESULT := U;\r
2222                       ALFA := TRUE\r
2223                    ELSE\r
2224                       U := U.NEXT\r
2225                    FI;\r
2226        ESAC;\r
2227      OD;\r
2228 END NEXTNODE;\r
2229 \r
2230 (****************************************************************************)\r
2231 (* SEARCH FOR THE FIRST HOLE *)\r
2232 \r
2233 UNIT FIRSTHOLE : FUNCTION ( M : POINTER , P : INTEGER ) : SEQUENT;\r
2234 VAR ALFA : BOOLEAN,\r
2235     A : SEQUENT;\r
2236 BEGIN\r
2237      IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;\r
2238      A := M.NEXT;\r
2239      WHILE A <> NONE AND NOT ALFA\r
2240      DO\r
2241        CASE P\r
2242             WHEN 1: IF A.PLEAF=NONE THEN\r
2243                        RESULT := A;\r
2244                        ALFA := TRUE\r
2245                     ELSE\r
2246                        A := A.NEXT;\r
2247                     FI;\r
2248             WHEN 0: IF A.LLEAF=NONE THEN\r
2249                        RESULT := A;\r
2250                        ALFA := TRUE\r
2251                     ELSE\r
2252                        A := A.NEXT;\r
2253                     FI;\r
2254        ESAC;\r
2255      OD;\r
2256 END FIRSTHOLE;\r
2257 \r
2258 (****************************************************************************)\r
2259 \r
2260 (****************************************************************************)\r
2261 (*                           ESSENTIAL RULES                                *)\r
2262 (****************************************************************************)\r
2263 \r
2264 (****************************************************************************)\r
2265 (* SENDS TO PROPER RULES *)\r
2266 \r
2267 UNIT RULES : PROCEDURE ( INOUT M : POINTER; P , R : INTEGER );\r
2268 VAR C : TNODE;\r
2269 BEGIN\r
2270       C := FINDCONN ( LAST ( M , P ) , R , P );\r
2271       IF C=NONE THEN RETURN FI;\r
2272       CASE R\r
2273            WHEN 03: CALL RULEEQU ( M,C,P );\r
2274            WHEN 04: CALL RULECON ( M,C,P );\r
2275            WHEN 05: CALL RULEDIS ( M,C,P );\r
2276            WHEN 06: CALL RULEIMP ( M,C,P );\r
2277            WHEN 07: CALL RULENEG ( M,C,P );\r
2278            WHEN 09: IF P=1 THEN CALL RULEEXIST ( M,C,P )\r
2279                        ELSE CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC );\r
2280                     FI;\r
2281            WHEN 08: IF P=1 THEN CALL RULE_EX_GEN ( M,P,K_MN_K,C,LOGIC )\r
2282                        ELSE CALL RULEEXIST ( M,C,P )\r
2283                     FI;\r
2284            WHEN 10: CALL RULEIF ( M,C,P );                  \r
2285            WHEN 11: CALL RULEBEG ( M, C, P );\r
2286            WHEN 12: CALL RULEWHL ( M,C,P );\r
2287            WHEN 13: CALL RULEQUAN ( M,P );                \r
2288       ESAC;\r
2289 END RULES;\r
2290 \r
2291 (****************************************************************************)\r
2292 (* RULE FOR THE PROGRAM BEGIN-END *)\r
2293 \r
2294 UNIT RULEBEG : PROCEDURE ( INOUT M : POINTER, C : TNODE, P : INTEGER );\r
2295 VAR A,B,D,E,F : TNODE;\r
2296 BEGIN\r
2297      A := C.RIGHT;                               (* HOLD BETA *)\r
2298      IF C.LEFT.IDENT = 1 THEN                    (* SIMULTANEOUSLY SUBSTITUTION *)\r
2299         CALL BEG_SUB ( C ) ;\r
2300         CALL MOVE ( M, P, P );\r
2301         RETURN;\r
2302      FI;\r
2303      IF C.LEFT<>NONE THEN\r
2304         CALL LIFT ( C, 1, 0 );                   (* THROW 'BEGIN' AND 'END' *)\r
2305         IF C.KIND=0 THEN                         (* ONLY ONE PROGRAM *)\r
2306            CALL LIFT ( C, 1, 0 );\r
2307            CALL END_OF_PRG ( C );                (* GO TO THE END OF IT *)\r
2308            C.RIGHT := A                          (* REFERS TO 'BETA' *)\r
2309         ELSE                                     (* MORE THAN ONE PROGRAM *)\r
2310            WHILE C.KIND=SEMKIND                  (* LOOP FOR NEXT PROGRAMS *)\r
2311            DO\r
2312              B := C.RIGHT;                       (* HOLD NEXT PROGRAM *)\r
2313              CALL LIFT ( C, 1, 0 );              (* THROW SEMICOLON *)\r
2314              CALL END_OF_PRG ( C );              (* GO TO THE END OF PROGRAM *)\r
2315              C.RIGHT := B;                                   C:=B;\r
2316            OD;\r
2317            CALL END_OF_PRG ( C );                (* END OF LAST PROGRAM *)\r
2318            C.RIGHT := A;                         (* REFERS TO 'BETA' *)\r
2319         FI\r
2320      ELSE                                        (* NO PROGRAM *)\r
2321         CALL LIFT ( C, 1, 1 )                         \r
2322      FI;\r
2323      CALL MOVE ( M, P, P );\r
2324 END RULEBEG;\r
2325 \r
2326 (****************************************************************************)\r
2327 (* DO SIMULTANEOUS SUBSTITUTIONS, MADE BY RULEDF_F AND RULEDF_L \r
2328    PROCEDURES, WHEN ONLY ATOMS LEFT *)\r
2329 \r
2330 UNIT BEG_SUB : PROCEDURE ( C : TNODE );\r
2331 BEGIN\r
2332    IF C.RIGHT.KIND = LITKIND OR C.RIGHT.KIND = EQUKIND \r
2333       OR C.RIGHT.KIND = LOGKIND OR C.RIGHT.KIND = BVAKIND THEN  \r
2334                                                  (* MAKE ONLY IN ATOMS AND *)\r
2335                                                  (* LOGICAL CONTANTS *)\r
2336       CALL SUB ( C, C.RIGHT );\r
2337       CALL ERASE ( C.LEFT );                     (* WHEN DONE ERASE SUBSTITUTIONS *)\r
2338       CALL LIFT ( C, 1, 1 );\r
2339    FI;\r
2340 END BEG_SUB;\r
2341                                                 \r
2342 (*****************************************************************************)\r
2343 (* CALLED BY BEG_SUB PROCEDURES *)\r
2344 \r
2345 UNIT SUB : PROCEDURE ( A, A1 : TNODE );\r
2346 VAR B,C,D : TNODE;\r
2347 BEGIN\r
2348    IF A1 = NONE THEN RETURN FI;\r
2349    IF A1.KIND = SUBKIND THEN                     (* MIGHT BE CHANGED *)\r
2350       B := A.LEFT;                               (* REFERS TO SEMICOLON *)\r
2351       WHILE B <> NONE                            (* VIEW THE WHOLE LIST *)\r
2352       DO\r
2353         IF B.KIND <> SEMKIND THEN\r
2354            C := B\r
2355         ELSE\r
2356            C := B.LEFT;                          (* C REFERS TO NEXT ARG *)\r
2357         FI;\r
2358         IF C.IDENT = A1.IDENT THEN               (* WILL BE CHANGED *)\r
2359            A1.LEFT := COPYTNODE ( C.LEFT );      (* S/TAU *)\r
2360            D := A1.RIGHT;                        (* STORES TEMPORARILY NEXT ARG *)\r
2361            CALL LIFT ( A1, 1, 0 );               (* REMOVE S *)\r
2362            A1.RIGHT := D;                        (* LINK STORED ARG *)\r
2363            CALL SUB ( A, A1.RIGHT );             (* REALIZE SIMULTANEOUS *)\r
2364                                                  (* SUBSTITUTION *)\r
2365            RETURN;                                               \r
2366         FI;\r
2367         B := B.RIGHT;\r
2368       OD;\r
2369     FI;\r
2370     CALL SUB ( A, A1.LEFT );\r
2371     CALL SUB ( A, A1.RIGHT );\r
2372 END SUB;\r
2373 \r
2374 (****************************************************************************)\r
2375 (* RULE FOR A PROGRAM WHILE-DO-OD *)\r
2376 \r
2377 UNIT RULEWHL : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
2378 VAR B,D,E,F,G,S,T,U,V : TNODE;\r
2379 BEGIN\r
2380      B := C.LEFT;                                (* HOLD 'ALFA' *)\r
2381      D := C.RIGHT.LEFT;                          (* HOLD PROGRAM 'K' *)\r
2382      E := C.RIGHT.RIGHT;                         (* HOLD 'BETA' *)\r
2383      C.KIND := BVARPRO;                          (* Q:=... *)\r
2384      C.IDENT := -LAST_Q-1;\r
2385      G := NEW TNODE;\r
2386      C.LEFT := G;\r
2387      G.KIND := LOGKIND;                          (* ...1 *)\r
2388      G.IDENT := 1;\r
2389      C.RIGHT.KIND := ITEKIND;                    (* ITER. GREAT QUANT. *)\r
2390      C.RIGHT.IDENT := 0;\r
2391      G := NEW TNODE;                             (* 'BEGIN' - 'END' *)\r
2392      C := C.RIGHT;\r
2393      C.LEFT := NONE;\r
2394      C.RIGHT := G;\r
2395      G.KIND := BEGKIND;\r
2396      G.IDENT := ENDKIND;\r
2397      U := NEW TNODE;                     \r
2398      G.LEFT := U;\r
2399      U.KIND := SEMKIND;                          (* SEMICOLON *)\r
2400      V := NEW TNODE;\r
2401      U.LEFT := V;\r
2402      V.KIND := BVARPRO;                          (* Q:=... *)\r
2403      V.IDENT := -LAST_Q-1;\r
2404      T := NEW TNODE;\r
2405      V.LEFT := T;\r
2406      T.KIND := CONKIND;                          (* CONJUNCTION *)\r
2407      S := NEW TNODE;\r
2408      T.LEFT := S;\r
2409      S.KIND := BVAKIND;                          (* Q *)\r
2410      S.IDENT := -LAST_Q-1;\r
2411      T.RIGHT := B;                               (* REFERS TO 'ALFA' *)\r
2412      U.RIGHT := D;                               (* REFERS TO PROGRAM 'K' *)\r
2413      T := NEW TNODE;\r
2414      G.RIGHT := T;\r
2415      T.KIND := CONKIND;                          (* CONJUNCTION *)\r
2416      U := NEW TNODE;\r
2417      T.LEFT := U;\r
2418      U.KIND := BVAKIND;                          (* Q *)\r
2419      U.IDENT := -LAST_Q-1;\r
2420      G := NEW TNODE;                             (* CONJUNCTION *)\r
2421      T.RIGHT := G;\r
2422      G.KIND := CONKIND;\r
2423      G.RIGHT := E;                               (* REFERS TO 'BETA' *)\r
2424      T := NEW TNODE;\r
2425      G.LEFT := T;\r
2426      T.KIND := NEGKIND;                          (* NEGATION *)\r
2427      T.LEFT := COPYTNODE ( B );                  (* OF 'ALFA' *)\r
2428      LAST_Q := LAST_Q+1;\r
2429      CALL MOVE ( M,P,P );\r
2430 END RULEWHL;\r
2431 \r
2432 (****************************************************************************)\r
2433 (* SEARCH FOR A VARIABLE NUMBER I IN FORMULA AND CHANGE IT INTO SUBKIND *)\r
2434 \r
2435 UNIT SEARCH_X : PROCEDURE ( A : TNODE , I : INTEGER );\r
2436 BEGIN\r
2437    IF A <> NONE THEN\r
2438       IF A.IDENT = I AND A.KIND = VARKIND THEN \r
2439          A.KIND := SUBKIND;\r
2440          A.IDENT := LAST_S;\r
2441       FI;\r
2442       CALL SEARCH_X ( A.LEFT , I );\r
2443       CALL SEARCH_X ( A.RIGHT , I );\r
2444    FI;\r
2445 END SEARCH_X;\r
2446 \r
2447 (*****************************************************************************)\r
2448 (* BOTH RULES FOR QUANTIFIERS   AX-ALFA *)\r
2449 \r
2450 UNIT RULEQUAN : PROCEDURE ( M : POINTER , P : INTEGER );\r
2451 VAR A,C,C1,D,E,F : TNODE;\r
2452 BEGIN\r
2453      IF P=0 THEN                                 (* QUAN ON LEFT SIDE *)\r
2454         IF LAST (M,0).NEXT = NONE THEN           (* BOTTOM LONGER THAN TOP *)\r
2455            LAST (M,0).NEXT := COPYSEQUENT( LAST(M,0) );  (* COPY A QUANTIFIER *)\r
2456            CALL ERASE ( LAST(M,0).PLEAF )     (* ERASE UPPER SIDE OF SEQUENT *)\r
2457         ELSE                                     (* OTHERWISE *)\r
2458            LAST(M,1).NEXT := COPYSEQUENT( LAST(M,0) );  (* COPY A QUANTIFIER *)\r
2459            CALL ERASE ( LAST(M,0).PLEAF );    (* ERASE UPPER SIDE OF SEQUENT *)\r
2460         FI;\r
2461      FI;\r
2462      CASE P\r
2463           WHEN 1: A := LAST (M,1).PLEAF;\r
2464           WHEN 0: A := LAST (M,0).LLEAF;\r
2465      ESAC;\r
2466      C := A;\r
2467      WHILE C.KIND=VARPROG OR C.KIND=BVARPRO\r
2468      DO\r
2469        C1 := C;                                  (* C1 POINTS TO LAST S *)\r
2470        C := C.RIGHT;                             (* C POINTS TO QUAN *)\r
2471      OD;\r
2472      D := NEW TNODE;                             (* NEW SUBSTITUTION *)\r
2473      D.KIND := VARPROG;                          (* S:=... *)\r
2474      LAST_S := LAST_S+1;   \r
2475      D.IDENT := LAST_S;\r
2476      F := NEW TNODE;                 \r
2477      D.LEFT := F;\r
2478      F.KIND := SUBKIND;                          (* ...:=Y *)\r
2479      IF LAST_X <= LAST_S THEN \r
2480         LAST_X := LAST_S + 1\r
2481      ELSE \r
2482         LAST_X := LAST_X + 1\r
2483      FI;\r
2484      F.IDENT := LAST_X;\r
2485      IF C1 = NONE THEN     \r
2486         A.RIGHT := D\r
2487      ELSE\r
2488         C1.RIGHT := D;\r
2489      FI;\r
2490      D.RIGHT := C.LEFT;                          (* REFERS TO FORMULA 'ALFA' *)\r
2491      CALL SEARCH_X ( C.LEFT , C.IDENT );         (* UPDATE NUMBERS OF BOUND *)\r
2492                                                  (* VARIABLE *)\r
2493      IF A.KIND = QUAKIND THEN \r
2494         A.LEFT := NONE;\r
2495         CALL LIFT ( A , 1 , 1 );\r
2496         D := A\r
2497      ELSE \r
2498         KILL ( C )\r
2499      FI;                                         (* ERASE QUANTIFIER TNODE *)\r
2500      \r
2501 (* NEXT LINES ARE ONLY CONNECTED WITH THE LEFT SIDE QUANTIFIER *)\r
2502 \r
2503      IF P=0 THEN\r
2504         E := NEW TNODE;                          (* NEW SUBSTITUTION *)\r
2505         E.KIND := VARPROG;                       (* Y:=... *)\r
2506         E.IDENT := LAST_X;      \r
2507         LAST_S := LAST_X;                        (* UPDATE NUMBER OF LAST *)\r
2508                                                  (* SUBSTITUTION *)\r
2509         F := NEW TNODE;                          (* ...:=TERM *)\r
2510         E.LEFT := F;\r
2511         F.KIND := SIGNTRM;                       (* JOKER TERM *)\r
2512         LAST_D := LAST_D+1;\r
2513         F.IDENT := LAST_D;\r
2514         E.RIGHT := A;                            (* REFERS TO SUBSTITUTIONS *)\r
2515         LAST ( M , 0 ).LLEAF := E;\r
2516         CALL MOVE ( M , P , P );                 (* MOVES THE LAST SEQUENT *)\r
2517                                                  (* WITHOUT QUANTIFIER  *)   \r
2518         CALL SWEEP ( M.NEXT.LLEAF );\r
2519      FI;\r
2520      CALL MOVE ( M , P , P );                    (* MOVES SEQUENT *)\r
2521                                                  (* WITH QUANTIFIER *)\r
2522 END RULEQUAN;\r
2523 \r
2524 (***************************************************************************)\r
2525 (* HELP FOR RULEITE - MAKE COPY AND INSERT IT DOWN TO CURRENT POINTER M  *)\r
2526 \r
2527 UNIT K_MN_K_DOWN : PROCEDURE ( M : POINTER, E : TNODE );\r
2528 VAR M2 : POINTER, \r
2529     A1 : SEQUENT;\r
2530 BEGIN\r
2531     M2 := NEW POINTER;\r
2532     M2.NEXT := COPYSEQUENT ( M.NEXT );\r
2533     M2.DOWN := M.DOWN;\r
2534     M.DOWN := M2;\r
2535     A1 := LAST ( M2 , 0 );\r
2536     CALL ERASE ( A1.LLEAF );\r
2537     A1.LLEAF := COPYTNODE ( E );               \r
2538     CALL SWEEP ( A1.LLEAF );\r
2539     CALL SQUEEZE ( M2 , 0 );\r
2540     CALL MOVE ( M2 , 0 , 0 )\r
2541 END K_MN_K_DOWN;\r
2542  \r
2543 (***************************************************************************)\r
2544 (* ITERATIONAL QUANTIFIER CONNECTED WITH WHILE *)\r
2545 \r
2546 UNIT RULEITE : PROCEDURE ( INOUT M : POINTER , LOGIC : BOOLEAN );\r
2547 (* K_MN_K MEANS k IN Mn(k) *)\r
2548 \r
2549 VAR A,B,C,D,E:TNODE,\r
2550     M2,M3:POINTER,\r
2551     A1,B2,F:SEQUENT,\r
2552     I:INTEGER;\r
2553 \r
2554 BEGIN\r
2555      C := COPYTNODE ( LAST ( M , 0 ).LLEAF );\r
2556      E := C;                                     (* E HOLDS BEGINNING OF Mn(0) *)\r
2557      WHILE C.KIND <> ITEKIND\r
2558      DO                                          (* MAKE THE SAME IN FAKE TREE *)\r
2559        D := C;\r
2560        C := C.RIGHT;\r
2561      OD;                                         (* C POINTS TO ITERATION *)\r
2562      A := COPYTNODE  ( E );     \r
2563      CALL LIFT ( C , 1 , 1);                     (* EXPELL ITERATION QUANTIFIER *)\r
2564      IF NOT LOGIC THEN\r
2565         B := A;\r
2566         WHILE B .KIND <> ITEKIND \r
2567         DO \r
2568           B := B.RIGHT;\r
2569         OD;\r
2570         CALL LIFT ( B, 1, 1 );                   (* EXPELL ITERATION QUANTIFIER *)\r
2571         CALL ERASE ( B.LEFT );\r
2572         CALL LIFT ( B, 1, 1 ); \r
2573         WHILE B.KIND <> CONKIND\r
2574         DO                                       (* GO DOWN UNTIL C CONTAINS CONJUNCTION *)       \r
2575           B := B.RIGHT;\r
2576         OD;\r
2577         M2 := NEW POINTER;                       (* CREATES NEW BRANCH *)\r
2578         M2.NEXT := COPYSEQUENT ( M.NEXT );\r
2579         M2.DOWN := M.DOWN;\r
2580         M.DOWN := M2;\r
2581         F := LAST ( M2 , 0 );\r
2582         CALL ERASE ( F.LLEAF );\r
2583         F.LLEAF := A;\r
2584         CALL SWEEP ( F.LLEAF );\r
2585         CALL SQUEEZE ( M2 , 0 );\r
2586      FI;\r
2587      IF NOT LOGIC OR K_MN_K=1 THEN               (* CONSTRUCT Mn(1) *)\r
2588         M2 := NEW POINTER;                       (* AND INSERT IT INTO *)\r
2589         M2.NEXT := COPYSEQUENT ( M.NEXT );       (* THE SEQUENT *)\r
2590         F := LAST ( M2 , 0 );\r
2591         CALL ERASE ( F.LLEAF );\r
2592         F.LLEAF := COPYTNODE ( E );\r
2593         M2.DOWN := M.DOWN;\r
2594         M.DOWN := M2;\r
2595         CALL SWEEP ( F.LLEAF );\r
2596         CALL SQUEEZE ( M2 , 0 );\r
2597      FI;\r
2598      FOR I := 0 TO K_MN_K-2\r
2599      DO                    \r
2600                                                  (* CREATE kMn(K_MN_K)ALFA *)\r
2601         B := C;                                  (* B POINTS TO BEGIN-END PROGRAM AFTER 'U' *)   \r
2602         WHILE B.KIND <> CONKIND\r
2603         DO                                       (* GOES DOWN UNTIL B CONTAINS CONJUNCTION *)     \r
2604           A := B;\r
2605           B := B.RIGHT;\r
2606         OD;                                      (* B POINTS TO CONJUNCTION, A PRECEED B *)       \r
2607         D := COPYTNODE ( C );                    (* D CONTAINS ONLY ONE PROGRAM K *)\r
2608                                                  (* AND CONJUCTION AS WELL *)     \r
2609         CALL ERASE ( A.RIGHT );\r
2610         A.RIGHT := D;\r
2611         C := D;\r
2612         IF NOT LOGIC THEN                        (* LOGIC=TRUE MEANS THAT WHILE HAS *)\r
2613            CALL K_MN_K_DOWN ( M, E );            (* ALREADY BEEN USED *)\r
2614         FI;\r
2615         \r
2616      OD;\r
2617      IF LOGIC AND K_MN_K > 1 THEN                (* INSERT Mn(K) INTO *)\r
2618         CALL K_MN_K_DOWN ( M, E );\r
2619      FI;\r
2620      K_MN_K:=K_MN_K+1;\r
2621                                                  (* PREPARE THREE NEW FORMULAS TO PROVE FOR 'WHILE' *)\r
2622      FOR I := 1 TO 3\r
2623      DO\r
2624            M3 := NEW POINTER;\r
2625            SQNT := COPYSEQUENT ( LAST ( M.DOWN , 0 ) );\r
2626            CALL ERASE_SEQ ( SQNT.NEXT );\r
2627            CALL ERASE ( SQNT.PLEAF );\r
2628            A := SQNT.LLEAF;\r
2629            WHILE A.KIND <> CONKIND\r
2630            DO\r
2631              A := A.RIGHT;\r
2632            OD;\r
2633            CASE I\r
2634               WHEN 1 : CALL ERASE ( A.RIGHT );\r
2635                        CALL LIFT ( A , 1 , 0 );  (* M(l) p *)\r
2636               WHEN 2 : CALL ERASE ( A.LEFT );    (* M(l) NOT ALFA *)\r
2637                        CALL LIFT ( A , 1 , 1 );\r
2638                        CALL ERASE ( A.RIGHT );\r
2639                        CALL LIFT ( A , 1 , 0 );\r
2640               WHEN 3 : CALL ERASE ( A.LEFT );    (* M(l) BETA *)\r
2641                        CALL LIFT ( A , 1 , 1 );\r
2642                        CALL ERASE ( A.LEFT );\r
2643                        CALL LIFT ( A , 1 , 1 );\r
2644            ESAC;  \r
2645            M3.NEXT := SQNT;\r
2646            CHI := TRUE; \r
2647            DIF := 1;                             (* VARIABLE DIF MEANS THAT *)\r
2648                                                  (* PROVE PROCEDURE WAS CALLED *)\r
2649                                                  (* FROM WHILE *)          \r
2650            CALL PROVE ( M3 , DIF );              (* PROOF FOR M(l)p, *)\r
2651                                                  (* M(l)NOT ALFA, *)\r
2652                                                  (* AND M(l)BETA *)\r
2653            CALL ERASE_PNTR ( M3 );      \r
2654                                                  (* IF ONE CAN PROVE CURRENT *)\r
2655                                                  (* SEQUENT E.G. Mn(l)p |- GENERATED *)\r
2656                                                  (* BY 'WHILE ' CHI IS NOT CHANGED *)\r
2657                                                  (* OTHERWISE CHI := FALSE IN PROVE *)\r
2658            IF CHI THEN EXIT FI;                  (* FINISHED PROOF BY M(l)p *)\r
2659                                                  (* OR M(l)NOT ALFA *)\r
2660                                                  (* OR BY M(l)BETA *)      \r
2661       OD;\r
2662       IF CHI THEN\r
2663          CALL ERASE_SEQ ( M.NEXT );\r
2664          CALL LIFT_PNTR ( M );\r
2665          CALL ERASE_SEQ ( M.NEXT );\r
2666          CALL LIFT_PNTR ( M );\r
2667       FI;\r
2668 END RULEITE;\r
2669 \r
2670 (****************************************************************************)\r
2671 (* RULE FOR ITERATION QUANTIFIERS *)\r
2672 \r
2673 UNIT RULE_EX_GEN:PROCEDURE(INOUT M:POINTER;P,K_MN_K:INTEGER,C:TNODE,LOGIC:BOOLEAN);\r
2674 VAR I : INTEGER,\r
2675     A,B,C2,D : TNODE,\r
2676     A2 : SEQUENT,\r
2677     M3,M2 : POINTER;\r
2678 BEGIN\r
2679      IF C.RIGHT.KIND = BEGKIND ANDIF C.RIGHT.LEFT <> NONE ANDIF\r
2680          C.RIGHT.LEFT.LEFT <> NONE ANDIF C.RIGHT.LEFT.LEFT.IDENT < 0 THEN\r
2681         CALL RULEITE ( M , LOGIC );              (* WHILE - ITERATION *)\r
2682         LOGIC := TRUE;\r
2683         RETURN;\r
2684      FI;\r
2685      A2 := COPYSEQUENT ( M.NEXT );                    \r
2686      M2 := NEW POINTER;                          (* CREATE NEW BRANCH *)\r
2687      M2.NEXT := A2;\r
2688      CASE P\r
2689           WHEN 0: A := LAST (M2,0).LLEAF;\r
2690           WHEN 1: A := LAST (M2,1).PLEAF;\r
2691      ESAC;     \r
2692      IF C.IDENT = 0 THEN                         (* THE FIRST STEP OF ITERATION *)\r
2693         CALL END_OF_S ( A,B );\r
2694         CALL LIFT ( A, 1, 1 );                   (* REMOVE ITERATION SIGN *)\r
2695         I := A.KIND;\r
2696         CALL ERASE ( A.LEFT );\r
2697         CALL LIFT ( A, 1, 1 );                   (* REMOVE SUBSTITUTION OR *)\r
2698                                                  (* BEGINNING OF ANOTHER PROGRAM *)\r
2699         IF I <> VARPROG AND I <> BVARPRO THEN\r
2700            CASE A.KIND\r
2701               WHEN WHIKIND : CALL ERASE ( A.LEFT );\r
2702                              CALL LIFT ( A,1,1 );\r
2703               WHEN IFFKIND : CALL ERASE ( A.LEFT );\r
2704                              CALL LIFT ( A,1,1 );\r
2705                              CALL ERASE ( A.LEFT );\r
2706                              CALL LIFT ( A,1,1 );\r
2707            ESAC;\r
2708         FI;\r
2709         C.IDENT := 1;\r
2710      ELSE                                        (* NEXT STEPS OF ITERATION *)\r
2711         WHILE A.KIND=VARPROG OR A.KIND=BVARPRO   (* OMITS SUBSTITUTION *)\r
2712         DO\r
2713           D := A; \r
2714           A := A.RIGHT;\r
2715         OD;\r
2716         A := A.RIGHT;                            (* A REFERS TO PROGRAM 'K' *)\r
2717         IF A.KIND=VARPROG OR A.KIND=BVARPRO THEN (* CONSISTING OF SUBSTITUTION *)\r
2718            C2 := COPYTNODE ( A );\r
2719            CALL ERASE ( A.RIGHT );\r
2720            A.RIGHT := C2\r
2721         ELSE                                     (* OR ANOTHER PROGRAM *)\r
2722            D := A;\r
2723            WHILE A.IDENT<>ENDKIND AND A.IDENT<>ODFKIND AND A.IDENT<>FIFKIND\r
2724            DO\r
2725              A := A.RIGHT;\r
2726            OD;                                   (* A OMITS PROGRAM 'K' *)\r
2727            C2 := COPYTNODE ( D );\r
2728            CALL ERASE ( A.RIGHT );\r
2729            A.RIGHT := C2;\r
2730         FI;\r
2731      FI;        \r
2732      M3 := M2;                                   (* ITERATION PUSHED TO *)\r
2733      M2 := M;                                    (* THE END OF A TREE *)\r
2734      M := M3;\r
2735      M.DOWN := M2;\r
2736      CALL MOVE ( M , P , P );\r
2737 END RULE_EX_GEN;\r
2738 \r
2739 (****************************************************************************)\r
2740 (* EXISTENTIAL ITERATION QUANTIFIER *)\r
2741 \r
2742 UNIT RULEEXIST : PROCEDURE ( M : POINTER, C : TNODE, P : INTEGER );\r
2743 VAR B,D,E : TNODE,\r
2744     A     : SEQUENT;\r
2745 BEGIN\r
2746      B := C;\r
2747      E := COPYTNODE ( C.RIGHT );\r
2748      IF B.RIGHT.KIND=VARPROG OR B.RIGHT.KIND=BVARPRO THEN\r
2749         D := B.RIGHT.RIGHT;\r
2750         B.RIGHT.RIGHT := E\r
2751      ELSE\r
2752          WHILE B.IDENT<>FIFKIND AND B.IDENT<>ODFKIND AND B.IDENT<>ENDKIND\r
2753          DO\r
2754            B := B.RIGHT;\r
2755          OD;\r
2756          D := B.RIGHT;\r
2757          B.RIGHT := E;\r
2758      FI;\r
2759      CASE P\r
2760         WHEN 0 : IF LAST (M,0).NEXT = NONE THEN\r
2761                     LAST (M,0).NEXT  :=  COPYSEQUENT ( LAST(M,P) )\r
2762                  ELSE \r
2763                     LAST (M,1).NEXT  :=  COPYSEQUENT ( LAST(M,P) )\r
2764                  FI;\r
2765                  E := FINDCONN ( LAST(M,0) , IGQKIND , 0 );\r
2766                  CALL ERASE ( LAST(M,0).PLEAF );\r
2767         WHEN 1 : IF LAST (M,1).NEXT = NONE THEN\r
2768                     LAST (M,1).NEXT  :=  COPYSEQUENT ( LAST(M,P) )\r
2769                  ELSE \r
2770                     LAST (M,0).NEXT  :=  COPYSEQUENT ( LAST(M,P) )\r
2771                  FI;\r
2772                  E := FINDCONN ( LAST(M,1) , ITEKIND , 1 );\r
2773                  CALL ERASE ( LAST(M,1).LLEAF );\r
2774      ESAC;\r
2775      CALL ERASE ( E.RIGHT );\r
2776      E.RIGHT := D;\r
2777      CALL LIFT ( E , 1 , 1 );\r
2778      CASE P\r
2779           WHEN 0: CALL MOVE ( M , 0 , 0 );\r
2780                   CALL SWEEP ( M.NEXT.LLEAF );\r
2781                   CALL MOVE ( M , 0 , 0 );\r
2782           WHEN 1: CALL MOVE ( M , 1 , 1 );\r
2783                   CALL SWEEP ( M.NEXT.PLEAF ); \r
2784                   CALL MOVE ( M , 1 , 1 );\r
2785      ESAC;\r
2786 END RULEEXIST;\r
2787 \r
2788 (****************************************************************************)\r
2789 (* RULE FOR IF-ALFA-THEN-K-ELSE-M-FI-BETA OR WITHOUT 'ELSE' PROGRAM *)\r
2790 \r
2791 UNIT RULEIF : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
2792 VAR B,D,E,G,H,K : TNODE;\r
2793 BEGIN\r
2794      B := C.LEFT;                                (* HOLD 'ALFA' *)\r
2795      C.LEFT := NONE;\r
2796      D := C.RIGHT.RIGHT.RIGHT;                   (* HOLD BETA *)\r
2797      C.RIGHT.RIGHT.RIGHT := NONE;\r
2798      IF C.RIGHT.RIGHT.KIND <> ELSKIND THEN       (* WITHOUT 'ELSE' *)\r
2799         C.LEFT := B;                             (* REFERS TO 'ALFA' *)\r
2800         C.KIND := CONKIND;\r
2801         C := C.RIGHT;\r
2802         CALL LIFT ( C , 1 , 0 );                 (* THROW 'THNKIND' *)\r
2803         CALL END_OF_PRG ( C );                   (* GO TO THE END OF 'K' *)\r
2804         C.RIGHT := D                             (* REFERS TO 'BETA' *)\r
2805      ELSE                                        (* WITH 'ELSE' *)\r
2806         C.KIND := DISKIND;          \r
2807         G := NEW TNODE;\r
2808         G.KIND := CONKIND;\r
2809         C.LEFT := G;\r
2810         G.LEFT := B;                             (* REFERS TO 'ALFA' *)\r
2811         K := C.RIGHT.RIGHT.LEFT;                 (* HOLD PROGRAM 'M' *)\r
2812         E := C.RIGHT;\r
2813         KILL ( E.RIGHT );\r
2814         CALL LIFT ( E , 1 , 0 );                 (* THROW 'THNKIND' *)\r
2815         G.RIGHT := E;\r
2816         CALL END_OF_PRG ( G );                   (* GO TO THE END OF 'K' *)\r
2817         G.RIGHT := D;                            (* REFERS TO 'BETA' *)\r
2818         H := NEW TNODE;                          (* 2ND ARG OF DISJUNCTION *)\r
2819         C.RIGHT := H;\r
2820         H.KIND := CONKIND;\r
2821         G := NEW TNODE;\r
2822         G.KIND := NEGKIND;\r
2823         H.LEFT := G;\r
2824         G.LEFT := COPYTNODE ( B );               (* REFERS TO 'ALFA' *)\r
2825         H.RIGHT := K;\r
2826         CALL END_OF_PRG ( H );\r
2827         H.RIGHT := COPYTNODE ( D );              (* REFERS TO 'BETA' *)\r
2828         H := C.LEFT;                             (* CHANGE FORMULA *)\r
2829         C.LEFT := C.RIGHT;\r
2830         C.RIGHT := H;\r
2831       FI;\r
2832       CALL MOVE ( M , P , P );\r
2833 END RULEIF;\r
2834 \r
2835 (****************************************************************************)\r
2836 (* RULE FOR IMPLICATION *)\r
2837 \r
2838 UNIT RULEIMP : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
2839 VAR U,V : TNODE,\r
2840     D   : SEQUENT;\r
2841 BEGIN\r
2842      CASE P\r
2843           WHEN 1: D:= NEW SEQUENT;               (* |- P => Q CONVERT TO *)\r
2844                   D.NEXT := M.NEXT;              (* P |- Q *)\r
2845                   M.NEXT := D;\r
2846                   U := COPYTNODE ( LAST ( M,1 ).PLEAF );\r
2847                   D.LLEAF := U;\r
2848                   CALL ERASE ( C.LEFT );\r
2849                   CALL LIFT ( C , 1 , 1 );\r
2850                   V := FINDCONN ( D, IMPKIND, 0 );\r
2851                   CALL ERASE ( V.RIGHT );\r
2852                   CALL LIFT ( V, 1, 0 );\r
2853                   CALL MOVE ( M, 1, 1 );\r
2854           WHEN 0: C.KIND := DISKIND;             (* IMPLICATION CHANGE TO *)\r
2855                   U := NEW TNODE;                (* DISJUNCTION *)\r
2856                   U.KIND := NEGKIND;\r
2857                   U.LEFT := C.LEFT;\r
2858                   C.LEFT := U;\r
2859                   CALL RULEDIS ( M , C , P );\r
2860      ESAC;\r
2861 END RULEIMP;\r
2862 \r
2863 (****************************************************************************)\r
2864 (* RULE FOR EQUIVALENCE *)\r
2865 \r
2866 UNIT RULEEQU : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
2867 VAR T,U,V,W : TNODE;\r
2868 \r
2869 BEGIN\r
2870   C.KIND := CONKIND;\r
2871   U := COPYTNODE ( C.LEFT );\r
2872   V := COPYTNODE ( C.RIGHT );\r
2873   W := NEW TNODE;\r
2874   T := NEW TNODE;\r
2875   W.KIND := IMPKIND;\r
2876   T.KIND := IMPKIND;\r
2877   W.LEFT := V;\r
2878   W.RIGHT := U;\r
2879   T.LEFT := C.LEFT;\r
2880   T.RIGHT := C.RIGHT;\r
2881   C.LEFT := W;\r
2882   C.RIGHT := T;\r
2883   CALL MOVE ( M , P , P );\r
2884 END RULEEQU;\r
2885 \r
2886 (*****************************************************************************)\r
2887 (* MAKE SERIAL OR PARALLEL SUBSTITUTION ON ATOMS *)\r
2888 \r
2889 UNIT SUBAT : PROCEDURE ( M : POINTER , P : INTEGER );\r
2890 VAR A : SEQUENT,\r
2891     B : TNODE;\r
2892 BEGIN\r
2893      A := LAST(M,P);\r
2894      IF A=NONE THEN RETURN FI;\r
2895      CASE P\r
2896           WHEN 1: B := A.PLEAF;\r
2897           WHEN 0: B := A.LLEAF;\r
2898      ESAC;\r
2899      IF B = NONE THEN RETURN FI;\r
2900      IF B.KIND = BEGKIND AND B.LEFT.IDENT <> 1 THEN RETURN FI;\r
2901      IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = LITKIND \r
2902         OR B.RIGHT.KIND = EQUKIND ) THEN CALL BEG_SUB ( B ); RETURN FI;\r
2903      IF B.KIND = BEGKIND AND B.LEFT.IDENT = 1 AND (B.RIGHT.KIND = BVARPRO\r
2904         OR B.RIGHT.KIND = VARPROG ) THEN CALL SER_INSERT ( B.RIGHT );RETURN \r
2905      FI;\r
2906      CALL SER_INSERT ( B );\r
2907 END SUBAT;\r
2908 \r
2909 (*****************************************************************************)\r
2910 (* DO SERIAL SUBSTITUTITON *)\r
2911 \r
2912 UNIT SER_INSERT : PROCEDURE ( A : TNODE );\r
2913 VAR B : TNODE;\r
2914 BEGIN\r
2915     CALL END_OF_S ( A, B );                      (* GO TO LAST SUBSTITUTION *)\r
2916     IF B.RIGHT.KIND = BVAKIND THEN \r
2917        CALL SERIAL_Q ( B, B.RIGHT )              (* MAKE SERIAL SUBSTITUION *)\r
2918                                                  (* FOR LOGICAL VARIABLES *)\r
2919     ELSE                                         \r
2920        CALL SERIAL_SUB ( B, B.RIGHT );           (* MAKE SERIAL SUBSTITUTION *)\r
2921     FI;                                          (* FOR LITERALS OR EQUALITIES *)\r
2922     CALL ERASE ( B.LEFT );                       (* REMOVE TAU *)\r
2923     CALL LIFT ( B, 1, 1 );                       (* REMOVE SUBSTITUTION *)\r
2924 END SER_INSERT;\r
2925  \r
2926 (*****************************************************************************)\r
2927 (* DO SERIAL SUBSTITUTION FOR ON LOGICAL VARIABLES - BVAKINS'S *)\r
2928 \r
2929 UNIT SERIAL_Q : PROCEDURE ( C, D : TNODE );\r
2930 BEGIN\r
2931     IF D = NONE THEN RETURN FI;\r
2932     IF D.IDENT = C.IDENT THEN\r
2933        D.LEFT := COPYTNODE ( C.LEFT );           (* COPY TAU *)\r
2934        CALL LIFT ( D , 1 , 0 );                  (* REMOVE S *)\r
2935     FI;\r
2936 END SERIAL_Q;\r
2937 \r
2938 (*****************************************************************************)\r
2939 (* CALLED BY SER_INSERT *)\r
2940 \r
2941 UNIT SERIAL_SUB : PROCEDURE ( C,D : TNODE );\r
2942 VAR E : TNODE;\r
2943 BEGIN\r
2944     IF D = NONE THEN RETURN FI;\r
2945     IF ( D.KIND = SUBKIND OR D.KIND = BVAKIND ) AND D.IDENT = C.IDENT THEN\r
2946        E := D.RIGHT;                             (* STORE TEMPORARILY NEXT ARG *)\r
2947        D.LEFT := COPYTNODE ( C.LEFT );           (* COPY TAU *)\r
2948        CALL LIFT ( D , 1 , 0 );                  (* REMOVE S *)\r
2949        D.RIGHT := E;                             (* LINK NEXT ARG *)\r
2950        CALL SERIAL_SUB ( C , D.RIGHT );          (* SEARCH FOR NEXT SUBKIND *)\r
2951        RETURN;\r
2952     FI;\r
2953     CALL SERIAL_SUB ( C , D.LEFT );  \r
2954     CALL SERIAL_SUB ( C , D.RIGHT );\r
2955 END SERIAL_SUB;\r
2956 \r
2957 (****************************************************************************)\r
2958 (* MOVES ALL ATOMS FROM THE END TO THE BEGINNING *)\r
2959 \r
2960 UNIT RULEAT : PROCEDURE ( M : POINTER , P : INTEGER ; INOUT BET : BOOLEAN );\r
2961 VAR A , B : SEQUENT;\r
2962 BEGIN\r
2963      IF M=NONE ORIF M.NEXT=NONE THEN RETURN FI;\r
2964      A := M.NEXT;\r
2965      CASE P\r
2966           WHEN 0 : WHILE A <> NONE\r
2967                    DO\r
2968                      IF A.LLEAF <> NONE THEN \r
2969                         IF A.LLEAF.KIND <> LITKIND AND A.LLEAF.KIND <> EQUKIND \r
2970                            AND A.LLEAF.KIND <> LOGKIND AND\r
2971                            A.LLEAF.KIND <> BVAKIND THEN \r
2972                            B := A \r
2973                         FI;\r
2974                      FI;\r
2975                      A := A.NEXT;\r
2976                    OD;\r
2977           WHEN 1 : WHILE A <> NONE \r
2978                    DO\r
2979                      IF A.PLEAF <> NONE THEN\r
2980                         IF A.PLEAF.KIND <> LITKIND AND A.PLEAF.KIND <> EQUKIND \r
2981                            AND A.PLEAF.KIND <> LOGKIND AND \r
2982                            A.PLEAF.KIND <> BVAKIND THEN \r
2983                            B := A \r
2984                         FI;\r
2985                      FI;\r
2986                      A := A.NEXT;\r
2987                    OD;\r
2988      ESAC;\r
2989      IF B = NONE THEN RETURN FI;\r
2990      WHILE B <> LAST ( M , P )\r
2991      DO\r
2992         CALL MOVE ( M , P , P );\r
2993      OD;\r
2994      BET := TRUE;\r
2995 END RULEAT;\r
2996 \r
2997 (****************************************************************************)\r
2998 (* RULE FOR NEGATION *)\r
2999 \r
3000 UNIT RULENEG : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
3001 BEGIN\r
3002      CALL LIFT ( C , 1 , 0 );\r
3003      CALL MOVE ( M , P , 1 - P );\r
3004 END RULENEG;\r
3005 \r
3006 (****************************************************************************)\r
3007 (* DIVIDE A SEQUENT INTO TWO PIECES AND DEPENDING ON 'S' RE-CONSTRUCT A LIST:\r
3008 S=1-ONE LIST; S=0-TWO LISTS *)\r
3009 \r
3010 UNIT BRANCH : PROCEDURE ( M : POINTER , P , R , S : INTEGER , C : TNODE );\r
3011 VAR M2  : POINTER,\r
3012     A,B,D : SEQUENT,\r
3013     E,F,E1,F1 : TNODE;\r
3014 BEGIN\r
3015      D := NEW SEQUENT;\r
3016      B := NEW SEQUENT;\r
3017      E := COPYTNODE( C.LEFT  );\r
3018      F := COPYTNODE( C.RIGHT );\r
3019      A := LAST ( M , P );\r
3020      CALL ERASE ( C );\r
3021      CASE P\r
3022        WHEN 0 : D.LLEAF := COPYTNODE ( A.LLEAF );\r
3023                 B.LLEAF := COPYTNODE ( A.LLEAF );\r
3024                 E1 := B.LLEAF;\r
3025                 CALL END_OF_PRG ( E1 );\r
3026                 IF E1 <> NONE THEN\r
3027                    E1.RIGHT := E\r
3028                 ELSE\r
3029                    B.LLEAF := E;\r
3030                 FI;\r
3031                 E1 := D.LLEAF;\r
3032                 CALL END_OF_PRG ( E1 );\r
3033                 IF E1 <> NONE THEN \r
3034                    E1.RIGHT := F\r
3035                 ELSE \r
3036                    D.LLEAF := F;\r
3037                 FI;\r
3038                 CALL ERASE ( A.LLEAF );\r
3039        WHEN 1 : D.PLEAF := COPYTNODE ( A.PLEAF );\r
3040                 B.PLEAF := COPYTNODE ( A.PLEAF );\r
3041                 E1 := B.PLEAF;\r
3042                 CALL END_OF_PRG ( E1 );\r
3043                 IF E1 <> NONE THEN\r
3044                    E1.RIGHT := E\r
3045                 ELSE\r
3046                    B.PLEAF := E;\r
3047                 FI;\r
3048                 E1 := D.PLEAF;\r
3049                 CALL END_OF_PRG ( E1 );\r
3050                 IF E1 <> NONE THEN \r
3051                    E1.RIGHT := F\r
3052                 ELSE \r
3053                    D.PLEAF := F;\r
3054                 FI;\r
3055                 CALL ERASE ( A.PLEAF );\r
3056      ESAC;\r
3057      CASE S\r
3058           WHEN 0: D.NEXT := M.NEXT;\r
3059                   M2 := NEW POINTER;\r
3060                   M2.DOWN := M.DOWN;\r
3061                   M.DOWN := M2;\r
3062                   M2.NEXT := B;\r
3063                   M.NEXT := D;\r
3064                   B.NEXT := COPYSEQUENT ( D.NEXT );\r
3065           WHEN 1: B.NEXT := M.NEXT;\r
3066                   D.NEXT := B;\r
3067                   M.NEXT := D;\r
3068      ESAC;\r
3069 END BRANCH;\r
3070 \r
3071 (****************************************************************************)\r
3072 (* RULE FOR CONJUNCTION *)\r
3073 \r
3074 UNIT RULECON : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
3075 BEGIN\r
3076      CALL BRANCH ( M,P,4,1-P,C );\r
3077      CASE P\r
3078           WHEN 1 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );\r
3079           WHEN 0 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );\r
3080      ESAC;\r
3081 END RULECON;\r
3082 \r
3083 (****************************************************************************)\r
3084 (* RULE FOR DISJUNCTION *)\r
3085 \r
3086 UNIT RULEDIS : PROCEDURE ( M : POINTER , C : TNODE , P : INTEGER );\r
3087 BEGIN\r
3088      CALL BRANCH ( M , P , 5 , P , C );\r
3089      CASE P\r
3090           WHEN 0 : CALL SWEEP ( M.DOWN.NEXT.PLEAF );\r
3091           WHEN 1 : CALL SWEEP ( M.NEXT.NEXT.PLEAF );\r
3092      ESAC;\r
3093 END RULEDIS;\r
3094 \r
3095 (*****************************************************************************)\r
3096 \r
3097 \r
3098 (*****************************************************************************)\r
3099 (*                      MAIN BODY OF THIS PROVER                             *)\r
3100 (*****************************************************************************)\r
3101 \r
3102 (*****************************************************************************)\r
3103 (* PROVE AND RETRIEVE AXIOMS OF ALL INPUT FORMULAS *)\r
3104 \r
3105 UNIT PROVE : PROCEDURE ( INOUT M : POINTER; DIF : INTEGER );\r
3106 VAR BETA : BOOLEAN;\r
3107 BEGIN\r
3108   CALL SWEEP ( M.NEXT.PLEAF );\r
3109   CALL THROW_RUBBISH ( M );\r
3110   WHILE M <> NONE\r
3111   DO\r
3112     ALFA := FALSE;\r
3113     BETA := FALSE;\r
3114     WHILE CHECK_L_F_P ( M.NEXT )\r
3115     DO\r
3116       WRITELN("DR");\r
3117       CALL SHOW_SEQ ( M.NEXT );\r
3118       CALL PROVE_P ( M , 1 );\r
3119       CALL MAKE_ORDER ( M );\r
3120       CALL PROVE_P ( M , 0 );\r
3121       CALL MAKE_ORDER ( M );\r
3122       IF AX <> NONE THEN\r
3123         IF SEARCH_AXIOMS ( M ) THEN \r
3124            CALL ERASE_SEQ ( M.NEXT );\r
3125            BETA := TRUE;                         (* FOUND AXIOM *)\r
3126            EXIT \r
3127         FI;\r
3128       FI;\r
3129       ALFA := FALSE;\r
3130     OD; \r
3131     write("*");\r
3132     WRITELN("SEQ");\r
3133     CALL SHOW_SEQ ( M.NEXT );\r
3134     IF AX = NONE THEN\r
3135        IF SEARCH_AXIOMS ( M ) THEN\r
3136           CALL ERASE_SEQ ( M.NEXT );\r
3137           BETA := TRUE;\r
3138        FI;\r
3139     FI;\r
3140     IF AX <> NONE THEN \r
3141       WRITELN( "AX");\r
3142       CALL SHOW_TREE ( AX.AXIOM );\r
3143       WRITELN("KONIEC");\r
3144     FI;\r
3145     IF BETA ORIF M.NEXT=NONE ORIF SEARCH_AXIOMS ( M ) THEN\r
3146        CALL LIFT_PNTR ( M );\r
3147        BETA := FALSE\r
3148     ELSE\r
3149        IF DIF<>1 THEN \r
3150           WRITE("THERE IS NO MODEL TO PROVE THIS EQUIVALENCE");\r
3151           RAISE ENDRUN\r
3152        ELSE \r
3153           CHI:=FALSE;\r
3154           RETURN \r
3155        FI; \r
3156     FI;\r
3157   OD;\r
3158   IF AX = NONE THEN WRITELN ( " THE FORMULA IS A THEOREM "); FI;\r
3159 END PROVE;\r
3160 \r
3161 (*****************************************************************************)\r
3162 (* DO THE RULES FOR P - SIDE UNTIL IT HAS NO USE *)\r
3163  \r
3164 UNIT PROVE_P : PROCEDURE ( INOUT M : POINTER; P : INTEGER );\r
3165 VAR R,I : INTEGER,\r
3166     A   : TNODE,\r
3167     BET : BOOLEAN;\r
3168 BEGIN\r
3169   R := 0;\r
3170   IF LAST ( M , P ) <> NONE THEN\r
3171      FOR I := 3 TO 13 \r
3172      DO\r
3173        IF FINDCONN ( LAST ( M , P ) , I , P ) <> NONE THEN\r
3174           R := I;\r
3175           EXIT\r
3176        FI;\r
3177      OD;\r
3178      IF R <> 0 THEN\r
3179         CALL RULES ( M, P, R )\r
3180      ELSE \r
3181         CASE P\r
3182            WHEN 0 : A := LAST ( M, P ).LLEAF;\r
3183            WHEN 1 : A := LAST ( M, P ).PLEAF;\r
3184         ESAC;\r
3185         IF A.KIND = BEGKIND ANDIF A.LEFT.KIND = SEMKIND ANDIF\r
3186            A.LEFT.IDENT = 1 THEN\r
3187            IF A.RIGHT.KIND <> VARPROG  AND  A.RIGHT.KIND <> BVARPRO THEN\r
3188               CASE P\r
3189                  WHEN 1 : CALL RULEBEG ( M, A , P );\r
3190                  WHEN 0 : CALL RULEBEG ( M, A , P );\r
3191               ESAC;\r
3192               RETURN;\r
3193            FI;\r
3194         FI;\r
3195         IF A.RIGHT <> NONE THEN\r
3196          IF A.KIND = VARPROG ORIF A.KIND = BVARPRO ORIF A.RIGHT.KIND = VARPROG\r
3197            ORIF A.RIGHT.KIND = BVARPRO THEN\r
3198            CALL SUBAT ( M, P );\r
3199            CASE P \r
3200              WHEN 0 : CALL SWEEP ( LAST ( M, P ).LLEAF );\r
3201              WHEN 1 : CALL SWEEP ( LAST ( M, P ).PLEAF );\r
3202            ESAC;\r
3203            CALL MOVE ( M, P, P );\r
3204          FI;\r
3205         FI;\r
3206         BET := FALSE;\r
3207         CALL RULEAT ( M, P, BET );\r
3208         IF NOT BET AND DEF_LIT = 1 THEN\r
3209            M1 := M1.NEXT;\r
3210            CASE M1.FUN_REL.KIND\r
3211               WHEN LITKIND : CALL RULEDF_L ( M, P, M1.FUN_REL.IDENT );\r
3212               WHEN EQUKIND : CALL RULEDF_F ( M, P, M1.FUN_REL.LEFT.IDENT );\r
3213            ESAC;\r
3214         FI;\r
3215       FI;\r
3216    FI;\r
3217 END PROVE_P;\r
3218 \r
3219 (*****************************************************************************)\r
3220 (* DO ORDER PROCEDURES IN WHOLE SEQUENT *)\r
3221 \r
3222 UNIT MAKE_ORDER : PROCEDURE ( M : POINTER );\r
3223 BEGIN\r
3224    IF M = NONE ORIF M.NEXT = NONE THEN RETURN FI;\r
3225    CALL SQUEEZE ( M, 0 );                        (* REMOVE HOLES *)\r
3226    CALL SQUEEZE ( M, 1 );                        \r
3227    CALL SWEEP ( M.NEXT.PLEAF );                  (* MAKE SIMPLE OPERATION *)\r
3228    CALL SWEEP ( M.NEXT.LLEAF );\r
3229    CALL CLAS_AX ( M );                           (* SEARCH CLASSICAL AXIOMS *)\r
3230    CALL THROW_RUBBISH ( M );                     (* REMOVE SEQUENT CONTAINING *)\r
3231                                                  (* LOGICAL CONSTANTS *)\r
3232    IF M.NEXT <> NONE THEN CALL CUT_SEQ ( M.NEXT ) FI;\r
3233                                                  (* REMOVE EMPTY FORMULAS *)\r
3234 END MAKE_ORDER;\r
3235 \r
3236 (*****************************************************************************)\r
3237 (* SEARCH EXTRA AXIOMS  *)\r
3238 \r
3239 UNIT SEARCH_AXIOMS : FUNCTION ( INOUT M : POINTER ) : BOOLEAN;\r
3240 BEGIN\r
3241      IF SEARCH_CN1 ( M.NEXT ) THEN \r
3242         CALL END_OF_M ( M, M.NEXT );\r
3243         RETURN;\r
3244      FI;\r
3245      IF LOOK_NQ ( M, 0 ) OR LOOK_NQ ( M, 1 ) OR LOOK_IDE ( M.NEXT ) THEN\r
3246         RESULT := TRUE;\r
3247         CALL ERASE_SEQ ( M.NEXT );\r
3248      FI;\r
3249 END SEARCH_AXIOMS;\r
3250 \r
3251 (****************************************************************************)\r
3252 (* SEARCH FOR FALSE CONSTANTS IN WHOLE SEQUENT *)\r
3253 \r
3254 UNIT SEARCH_CN1 : FUNCTION ( A : SEQUENT ) : BOOLEAN;\r
3255 VAR ALFA : BOOLEAN;\r
3256 BEGIN\r
3257    WHILE A <> NONE \r
3258    DO\r
3259      CALL FUNCHECK ( A.PLEAF, ALFA );\r
3260      CALL FUNCHECK ( A.LLEAF, ALFA );\r
3261      IF ALFA THEN \r
3262         RESULT := TRUE;\r
3263         RETURN;\r
3264      FI;\r
3265      A := A.NEXT;\r
3266   OD;\r
3267 END SEARCH_CN1;\r
3268      \r
3269 (****************************************************************************)\r
3270 (* SEARCH CLASSICAL AXIOMS *)\r
3271 \r
3272 UNIT CLAS_AX : PROCEDURE ( M : POINTER );\r
3273 VAR A, A1 : SEQUENT,\r
3274       AX1 : LIST_AXIOMS,\r
3275      ALFA : BOOLEAN;\r
3276 BEGIN\r
3277    IF M.NEXT=NONE THEN RETURN FI;\r
3278      A := M.NEXT;\r
3279      WHILE A <> NONE\r
3280      DO                                          (* SEARCH FOR THE IDENTICAL *)\r
3281        A1 := M.NEXT;\r
3282        IF A.PLEAF <> NONE THEN                   (* FORMULAS IN A SEQUENT *)\r
3283           WHILE A1 <> NONE                       \r
3284           DO                                     (* ON BOTH SIDES *)\r
3285             IF A1.LLEAF <> NONE THEN             (* I.E. ...beta...|-...beta... *)\r
3286                ALFA := TRUE;\r
3287                CALL COMPARE ( A.PLEAF, A1.LLEAF, ALFA);\r
3288                IF ALFA THEN\r
3289                   CALL ERASE_SEQ ( M.NEXT );     (* WHEN FOUND - ERASE SEQUENT *)\r
3290                   RETURN;\r
3291                FI;\r
3292             FI;\r
3293             A1 := A1.NEXT;\r
3294           OD;\r
3295        FI;\r
3296        A := A.NEXT;\r
3297      OD;\r
3298      A := M.NEXT;\r
3299      WHILE A <> NONE\r
3300      DO\r
3301        A1 := M.NEXT;\r
3302        IF A.PLEAF <> NONE THEN\r
3303           WHILE A1 <> NONE\r
3304           DO\r
3305             IF A1.LLEAF <> NONE THEN\r
3306               IF A.PLEAF.KIND = LITKIND OR A.PLEAF.KIND = EQUKIND THEN\r
3307                IF A.PLEAF.KIND=A1.LLEAF.KIND AND A.PLEAF.IDENT=A1.LLEAF.IDENT\r
3308                THEN\r
3309                   IF SYL_AXIOMS ( M , A1.LLEAF.LEFT , A.PLEAF.LEFT ) THEN\r
3310                      CALL ERASE_SEQ ( M.NEXT );\r
3311                      RETURN;\r
3312                   FI;\r
3313                FI;\r
3314               FI;\r
3315             FI;\r
3316             A1 := A1.NEXT;\r
3317           OD;\r
3318        FI;\r
3319        A := A.NEXT;\r
3320      OD;\r
3321 END CLAS_AX;\r
3322 \r
3323 (****************************************************************************)\r
3324 (* LOOK FOR AXIOM OF THE FORM Xi=Yi and P(X1,...,Xn) |- P(Y1,...,Yn)  *)\r
3325 \r
3326 UNIT SYL_AXIOMS : FUNCTION ( M : POINTER, E, F : TNODE ) : BOOLEAN;\r
3327 VAR          A : SEQUENT,\r
3328        B, C, D : TNODE,\r
3329     BETA, ALFA : BOOLEAN;\r
3330 BEGIN\r
3331      WHILE E<>NONE AND F<>NONE\r
3332      DO\r
3333        B := COPYTNODE ( E );\r
3334        C := COPYTNODE ( F );\r
3335        CALL ERASE ( C.RIGHT );\r
3336        CALL ERASE ( B.RIGHT );\r
3337        B.RIGHT := C;                             (* CREATE PAIR Xi->Yi *)\r
3338        A := M.NEXT;\r
3339        WHILE A<>NONE \r
3340        DO \r
3341          IF A.LLEAF<>NONE ANDIF A.LLEAF.KIND=EQUKIND THEN\r
3342             D := A.LLEAF.LEFT;\r
3343             ALFA := TRUE;\r
3344             CALL COMPARE ( D, B, ALFA );         (* SEARCH FOR RESPECTIVE PAIR *)\r
3345             IF ALFA THEN\r
3346                BETA := TRUE;\r
3347                EXIT;\r
3348             FI;\r
3349          FI;\r
3350          A := A.NEXT;\r
3351        OD;\r
3352        CALL ERASE ( B );\r
3353        IF NOT BETA THEN RETURN FI;               (* IF NOT FOUND THEN RESULT := FALSE *)\r
3354        E := E.RIGHT;                             (* SEARCH FURTHER *)\r
3355        F := F.RIGHT;                             (* FOR NEXT PAIR *)\r
3356      OD;\r
3357      RESULT := TRUE;\r
3358 END SYL_AXIOMS;\r
3359 \r
3360 (****************************************************************************)\r
3361 (* LOOKING FOR NQ OR Q AXIOM *)\r
3362 \r
3363 UNIT LOOK_NQ : FUNCTION ( M : POINTER, P : INTEGER ) : BOOLEAN;\r
3364 VAR A   : SEQUENT,\r
3365     AX2 : LIST_AXIOMS,\r
3366       C : TNODE ;\r
3367 BEGIN\r
3368      A := M.NEXT;\r
3369      WHILE A <> NONE\r
3370      DO                                          (* VIEW WHOLE SEQUENT *)\r
3371                                                  (* LOOKING FOR Q *)\r
3372        CASE P \r
3373           WHEN 0 : IF A.LLEAF <> NONE THEN\r
3374                      IF A.LLEAF.KIND = BVAKIND THEN   (* FOUND Q ON LEFT SIDE *)\r
3375                       IF SRCH_Q_AX ( A.LLEAF.IDENT, AX2 ) THEN \r
3376                          IF AX2.AXIOM.KIND = NEGKIND THEN\r
3377                             RESULT := TRUE;\r
3378                             RETURN\r
3379                          ELSE\r
3380                             RESULT := FALSE      (* FOUND NEGATION OF EXISTED *)\r
3381                                                  (* AXIOM Q *)\r
3382                          FI\r
3383                       ELSE                       (* AXIOM NOT FOUND *)\r
3384                          AX2 := MAKE_AXIOM ( AX );\r
3385                          IF AX = NONE THEN AX := AX2 FI;\r
3386                          C := NEW TNODE;         (* AXIOM := NOT Q *)\r
3387                          C.KIND := NEGKIND;\r
3388                          C.LEFT := COPYTNODE ( A.LLEAF );\r
3389                          AX2.AXIOM := C;         \r
3390                          RESULT := TRUE;\r
3391                          RETURN;       \r
3392                       FI;\r
3393                      FI;\r
3394                    FI;\r
3395           WHEN 1 : IF A.PLEAF <> NONE THEN\r
3396                      IF A.PLEAF.KIND = BVAKIND THEN   (* FOUND Q ON RIGHT SIDE *)\r
3397                       IF SRCH_Q_AX ( A.PLEAF.IDENT, AX2 ) THEN \r
3398                          IF AX2.AXIOM.KIND = NEGKIND THEN\r
3399                             RESULT := FALSE;     (* FOUND NEGATION OF EXISTED *)\r
3400                                                  (* AXIOM Q *)\r
3401                          ELSE\r
3402                             RESULT := TRUE;      (* FOUND CORRECT AXIOM *)\r
3403                          FI\r
3404                       ELSE                       (* AXIOM NOT FOUND *)\r
3405                          AX2 := MAKE_AXIOM ( AX );\r
3406                          IF AX = NONE THEN AX := AX2 FI;\r
3407                          AX2.AXIOM := COPYTNODE ( A.PLEAF );         \r
3408                          RESULT := TRUE;\r
3409                       FI;\r
3410                       RETURN;\r
3411                      FI;\r
3412                    FI;\r
3413        ESAC;\r
3414        A := A.NEXT;\r
3415      OD;\r
3416 END LOOK_NQ;\r
3417 \r
3418 (*****************************************************************************)\r
3419 (* SEARCH FOR A BVAKIND IN THE SET OF AXIOMS *)\r
3420 \r
3421 UNIT SRCH_Q_AX : FUNCTION ( N : INTEGER; INOUT AX2 : LIST_AXIOMS ) : BOOLEAN;\r
3422 BEGIN\r
3423    AX2 := AX;\r
3424    WHILE AX2 <> NONE \r
3425    DO\r
3426      IF AX2.AXIOM.KIND = BVAKIND AND AX2.AXIOM.IDENT = N THEN\r
3427         RESULT := TRUE;\r
3428         RETURN\r
3429      ELSE\r
3430         IF AX2.AXIOM.KIND = NEGKIND ANDIF AX2.AXIOM.LEFT.KIND = BVAKIND\r
3431            AND AX2.AXIOM.LEFT.IDENT = N THEN\r
3432            RESULT := TRUE;\r
3433            RETURN;\r
3434         FI;\r
3435      FI;\r
3436      AX2 := AX2.NEXT;\r
3437    OD;\r
3438    RESULT := FALSE;\r
3439 END SRCH_Q_AX;\r
3440 \r
3441 (*****************************************************************************)\r
3442 (* CREATE A NEW AXIOM *)\r
3443 \r
3444 UNIT MAKE_AXIOM : FUNCTION ( AX1 : LIST_AXIOMS ) : LIST_AXIOMS ;\r
3445 BEGIN\r
3446    IF AX1 = NONE THEN\r
3447       RESULT := NEW LIST_AXIOMS;\r
3448    ELSE\r
3449       CALL END_OF_AX ( AX1 );\r
3450       AX1.NEXT := NEW LIST_AXIOMS;\r
3451       RESULT := AX1.NEXT;\r
3452    FI;\r
3453 END MAKE_AXIOM;\r
3454 \r
3455 (*****************************************************************************)\r
3456 (* LOOKING FOR IDENTITY AXIOM U=TAU *)\r
3457 \r
3458 UNIT LOOK_IDE:FUNCTION ( A : SEQUENT ) : BOOLEAN;\r
3459 VAR AX1 : LIST_AXIOMS,\r
3460     ALFA : BOOLEAN;\r
3461 BEGIN\r
3462      WHILE A <> NONE \r
3463      DO\r
3464         IF A.PLEAF <> NONE ANDIF A.PLEAF.KIND = EQUKIND ANDIF \r
3465            ( A.PLEAF.LEFT.KIND = VRUKIND OR A.PLEAF.LEFT.RIGHT.KIND = VRUKIND )\r
3466         THEN                                     (* FOUND U=TAU *)\r
3467           CALL FUNCHECK ( A.PLEAF, ALFA );\r
3468           IF NOT ALFA THEN \r
3469            AX1 := AX;\r
3470            RESULT := TRUE;\r
3471            WHILE AX1 <> NONE\r
3472            DO\r
3473               ALFA := TRUE;\r
3474               CALL COMPARE ( A.PLEAF, AX1.AXIOM, ALFA );\r
3475               IF ALFA THEN RETURN FI;            (* THIS AXIOM HAS ALREADY *)\r
3476               AX1 := AX1.NEXT;                   (* BEEN WRITTEN TO THE LIST *)\r
3477            OD;\r
3478            IF SEARCH_U ( A ) THEN \r
3479               CALL END_OF_M ( M, A );\r
3480               RETURN;\r
3481            FI;\r
3482            CALL END_OF_AX ( AX1 );               (* AXIOM NOT FOUND *)\r
3483            IF AX = NONE THEN \r
3484               AX1 := NEW LIST_AXIOMS;\r
3485               AX := AX1\r
3486            ELSE\r
3487               AX1.NEXT := NEW LIST_AXIOMS;       (* SO, THE LIST MUST BE *)\r
3488               AX1 :=AX1.NEXT;\r
3489            FI;\r
3490            AX1.AXIOM := COPYTNODE ( A.PLEAF );   (* UPDATED *)\r
3491            RETURN\r
3492          ELSE\r
3493            ALFA := FALSE\r
3494          FI;\r
3495         FI;\r
3496         A := A.NEXT;   \r
3497      OD;\r
3498 END LOOK_IDE;\r
3499 \r
3500 (*****************************************************************************)\r
3501 \r
3502 \r
3503 (*****************************************************************************)\r
3504 (*                            OUTPUT OF AXIOMS                               *)\r
3505 (*****************************************************************************)\r
3506 \r
3507 (*****************************************************************************)\r
3508 (* PRINTS ALL LIST OF AXIOMS *)\r
3509 \r
3510 UNIT SHOW_AX : PROCEDURE ( AX1 : LIST_AXIOMS );\r
3511 BEGIN\r
3512     IF AX1 <> NONE THEN\r
3513        CALL SHOW_TREE ( AX1.AXIOM );\r
3514        CALL SHOW_AX ( AX1.NEXT );\r
3515     FI;\r
3516 END SHOW_AX;\r
3517       \r
3518 (****************************************************************************)\r
3519 (* WRITES AXIOMS *)\r
3520 \r
3521 UNIT WRITE_AXIOMS : PROCEDURE;\r
3522 VAR AX1 : LIST_AXIOMS;\r
3523 BEGIN\r
3524    AX1 := AX;\r
3525    IF AX = NONE THEN \r
3526       WRITE ( "IT IS TRUE WITHOUT ADDITIONAL AXIOMS" ); \r
3527       RETURN \r
3528    FI;\r
3529    WHILE AX1 <> NONE \r
3530    DO \r
3531      IF AX1.AXIOM.KIND = EQUKIND THEN\r
3532         WRITE (" U = ");\r
3533         IF AX1.AXIOM.LEFT.KIND = VRUKIND THEN\r
3534            CALL WRITE_EXPR ( AX1.AXIOM.LEFT.RIGHT )\r
3535         ELSE\r
3536            CALL WRITE_EXPR ( AX1.AXIOM.LEFT );\r
3537         FI\r
3538      ELSE\r
3539         CASE AX1.AXIOM.KIND\r
3540           WHEN 7  : CALL PUTCH ( 'Q' );\r
3541                     CALL PNUM ( AX1.AXIOM.LEFT.IDENT );\r
3542                     WRITE ( " <=> FALSE" );\r
3543           WHEN 33 : CALL PUTCH ( 'Q');\r
3544                     CALL PNUM ( AX1.AXIOM.IDENT );\r
3545                     WRITE ( " <=> TRUE" );\r
3546         ESAC\r
3547       FI;\r
3548       AX1 := AX1.NEXT;\r
3549       WRITELN;\r
3550     OD;\r
3551     CALL ERASE_AX ( AX );\r
3552 END WRITE_AXIOMS;    \r
3553       \r
3554 (****************************************************************************)\r
3555 (* PRINT BRACKETS *)\r
3556         \r
3557 UNIT PUT_BRACKET : PROCEDURE ( C : TNODE );\r
3558 VAR K : INTEGER;\r
3559 BEGIN\r
3560     K := C.KIND;\r
3561     IF K=LITKIND ORIF K=FUNKIND ORIF K=42 ORIF K=43\r
3562        ORIF K=47 ORIF K=45 ORIF K=94 THEN\r
3563        CALL PUTCH ( '(' );\r
3564        CALL WRITE_EXPR ( C );\r
3565        CALL PUTCH ( ')' )\r
3566     ELSE\r
3567        CALL WRITE_EXPR ( C );\r
3568     FI;\r
3569 END PUT_BRACKET;\r
3570 \r
3571 (****************************************************************************)\r
3572 (* PRINT TERM *)\r
3573 \r
3574 UNIT WRITE_EXPR : PROCEDURE ( C : TNODE );\r
3575 BEGIN\r
3576      IF C=NONE THEN RETURN FI;\r
3577      CASE C.KIND\r
3578        WHEN CN2KIND:CALL PUTCH ( 'C' );\r
3579                     CALL PNUM ( C.IDENT );\r
3580                     RETURN;\r
3581        WHEN CNTKIND:CALL PNUM ( C.IDENT + 1 );\r
3582                     RETURN;\r
3583        WHEN LITKIND:CALL PUTCH ( 'P' );\r
3584                     CALL PNUM ( C.IDENT );\r
3585                     C := C.LEFT;\r
3586                     IF C <> NONE THEN \r
3587                        CALL PUTCH ( '(' );\r
3588                     FI;\r
3589                     RETURN;\r
3590        WHEN FUNKIND:CALL PUTCH ( 'F' );\r
3591                     CALL PNUM ( C.IDENT );\r
3592                     IF C.LEFT <> NONE THEN \r
3593                        CALL PUTCH ( '(' );\r
3594                        CALL WRITE_EXPR ( C.LEFT );  \r
3595                     FI;\r
3596                     C := C.RIGHT;\r
3597                     IF C = NONE THEN \r
3598                        CALL PUTCH ( ')' )\r
3599                     ELSE \r
3600                        CALL PUTCH ( ',' );\r
3601                     FI;\r
3602                     RETURN;\r
3603         WHEN ARIKIND:\r
3604          CASE C.IDENT\r
3605            WHEN 42 :CALL PUT_BRACKET ( C.LEFT );\r
3606                     CALL PUTCH ( '*' );\r
3607                     CALL PUT_BRACKET ( C.LEFT.RIGHT );\r
3608                     RETURN;\r
3609            WHEN 43 :CALL PUT_BRACKET ( C.LEFT );\r
3610                     CALL PUTCH ( '+' );\r
3611                     CALL PUT_BRACKET ( C.LEFT.RIGHT );\r
3612                     RETURN;     \r
3613            WHEN 45 :CALL PUT_BRACKET ( C.LEFT );\r
3614                     CALL PUTCH ( '-' );\r
3615                     CALL PUT_BRACKET ( C.LEFT.RIGHT );\r
3616                     RETURN;     \r
3617            WHEN 47 :CALL PUT_BRACKET ( C.LEFT );\r
3618                     CALL PUTCH ( '/' );\r
3619                     CALL PUT_BRACKET ( C.LEFT.RIGHT );\r
3620                     RETURN;    \r
3621            WHEN 94 :CALL PUT_BRACKET ( C.LEFT );\r
3622                     CALL PUTCH ( '^' );\r
3623                     CALL PUT_BRACKET ( C.LEFT.RIGHT );\r
3624                     RETURN;\r
3625         ESAC;\r
3626      ESAC;\r
3627 END WRITE_EXPR;\r
3628 \r
3629 (****************************************************************************)\r
3630 (* PRINT NUMBER WITHOUT SPACES OR ZEROS CONTROLLING END OF LINE *)\r
3631                  \r
3632 UNIT PNUM : PROCEDURE ( N : INTEGER );\r
3633 VAR I:INTEGER;\r
3634 BEGIN\r
3635    N := N-1;\r
3636    IF N > -1 THEN\r
3637       I := 1;\r
3638       IF N>9 THEN I := I+1 FI;\r
3639       IF N>99 THEN I := I+1 FI;\r
3640       IF N>999 THEN I := I+1 FI;\r
3641       IF N>9999 THEN I := I+1 FI;\r
3642       IF CHARSH+1>LINLNG THEN WRITELN; CHARSH := 0 FI;\r
3643       IF CHARSH=0 THEN WRITE(' '); FI;\r
3644       WRITE ( N:I );\r
3645       CHARSH := CHARSH+1;\r
3646    FI;\r
3647 END PNUM;\r
3648 \r
3649 (****************************************************************************)\r
3650 (* SERVES SPECIAL EXCEPTIONS - HARD EXIT FROM PROGRAM *)\r
3651 \r
3652 SIGNAL ENDRUN;\r
3653 HANDLERS\r
3654    WHEN ENDRUN: TERMINATE;\r
3655 END HANDLERS;\r
3656 \r
3657 (****************************************************************************)\r
3658 \r
3659 BEGIN\r
3660    L := 0;\r
3661    OPEN ( G , TEXT , UNPACK ( "RETRPROV.DAT" ) );\r
3662    M := NEW POINTER;\r
3663    SQNT := NEW SEQUENT;\r
3664    M.NEXT := SQNT;\r
3665    CALL RESET ( G );\r
3666    SQNT.PLEAF := GEN_TREE;\r
3667    CALL LAST1_S ( SQNT.PLEAF );\r
3668    CALL LAST1_X ( SQNT.PLEAF );\r
3669   (* M contains f(t1,...,tn)=u or relation *)\r
3670   WRITELN ( "PROVE WITH DEFINITION    ------- 1 " );\r
3671   WRITELN ( "PROVE WITHOUT DEFINITION ------- 2 " );\r
3672   READ ( DEF_LIT );\r
3673   IF DEF_LIT = 1 THEN \r
3674    (* M1 contains f(x1,...,xn)=Ktau  or relation *)\r
3675    OPEN ( G , TEXT , UNPACK ( "RETRPROV.DEF" ) );\r
3676    M1 := NEW DEF;\r
3677    M1.NEXT := M1;\r
3678    CALL RESET ( G );\r
3679    L := 0;\r
3680    M1.FUN_REL := GEN_TREE;\r
3681    CALL LAST1_S ( M1.FUN_REL );\r
3682    CALL LAST1_X ( M1.FUN_REL );\r
3683    CALL REP_F_L ( M1 );                          (* FUNKIND -> FN1KIND *)\r
3684                                                  (* LITKIND -> LT1KIND *)\r
3685    CALL RULEDF_L ( M , 1 , M1.FUN_REL.LEFT.IDENT );\r
3686    CALL RULEDF_F ( M , 1 , M1.FUN_REL.LEFT.IDENT );  \r
3687   FI;\r
3688   K_MN_K := 2;\r
3689   LOGIC := FALSE;\r
3690   CALL PROVE ( M , 0 );\r
3691   CALL WRITE_AXIOMS;\r
3692 END RETRPROV; \r
3693 \r
3694 (****************************************************************************)\1a