-LIST LEFT * Principia Mathemematica Proof Checker * By Daniel J. O'Leary * Copyright (c) 1982 Daniel J. O'Leary * Reentered with permission from printouts by Dennis J. Darland - 2017 * * * Principia Mathathenatica Proof Checker * * By Dan J. O'Leary * * Copyright (c) 1982 DAniel J. O'Leary * * Re-entered with changes from printout * * by Dennis J. Darland * * Copyright (C) 2017 Dennis J. Darland * * This file is part of Dan J. O'Leary's proof checker for PM * * It is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * It is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with it. If not, see . * DATE LAST CHANGED July 23, 1982 by O'Leary * Reentered starting June 2, 2017 by Darland * Dennis J. Daland making many changes. * * The Defined Functions come first. * The Program starts at the Label START * sub_line is the text into which thr substitution is made * subs is the string with the substitutions in it.' * Fill up the substitution table. * Start by setting it to the Identity Substitution * * DJD NOTES: * I have used mixed case - the original was all upper case. * Mostly Upper for Snobol4 keywords & labels. * Lover for user variables. * Also used '[' and ']' instead of '<' and '>'. * * 6/20/2017 DJD - Trying to make line numbers match. * Will initially br one off bcause of goto START which is necessary * * substitution(sub_line,subs)s1,s2,s3,n1 * DJD :(START) added - line numbers 1 large uniil 1 :(START) 2 F1 SENVAR = 'pqrstuv' 3 F1.1 SENVAR LEN(1) . S1 = :F(F1.2) 4 SUB[S1] = S1 :(F1.1) * Now get the indicated substitution into the table. * First append a comma and a blank to show the end 5 F1.2 SUBS = SUBS ', ' 6 F1.3 SUBS (BREAK('/') . S1 ) '/' (BREAK(',') . S2) 6 + ',' (SPAN(' ') . S3) :F(F1.4) 7 SUB[S1] = S2 8 SUBS S1 '/' S2 ',' S3 = :(F1.3) * * Now we actually make the substitution and print. 9 F1.4 SENVAR = 'pqrstuv' 10 NUM = '1234567' * Change the sentenial variables to numbers 11 F1.5 SENVAR LEN(1) . S1 = :F(F1.7) 12 NUM LEN(1) . N1 = 13 F1.6 SUB_LINE S1 = N1 :S(F1.6)F(F1.5) * Now replace the numbers by their substitutions 14 F1.7 SENVAR = 'pqrstuv' 15 NUM = '1234567' 16 F1.8 SENVAR LEN(1) . S1 = :F(F1END) 17 NUM LEN(1) . N1 = 18 F1.9 SUB_LINE N1 = SUB[S1] :S(F1.9)F(F1.8) 19 F1END SUBSTITUTION = SUB_LINE :(RETURN) * * * skip(in),n1 20 F2 GE(IN,0) :F(FRETURN) 21 N1 = 0 22 F2.1 N1 = N1 + 1 23 PAGE_OUT = 24 F2END GE(N1,IN) :F(F2.1)S(RETURN) * * * put_page() 25 F3 SPACES = 50 * DJD omition of 'PAGE = ' gets line numbers correct 26 PAGE_OUT = CENTER(HEADING) 27 PAGE_OUT = 28 PAGE_OUT = DUPL(' ',SPACES) THS_NUM 29 PAGE_OUT = DUPL(' ',SPACES) DATE_PM 30 SKIP(1) 31 F3END PAGE_LINES = 10 :(RETURN) * * * arabic(in),n 32 F4 ARABIC = ROMAN_TO_ARABIC[IN] 33 F4END NE(ARABIC,0) :S(RETURN)F(FRETURN) * * 34 35 * DJD - GOT RID OF F5 - no need to limit printing. * * DJD - GOT RID OF F6 - REVERSE is built in. * * DJD - Will leave blank lines - they create line numbers * 36 37 38 39 40 41 42 * implication(string) 43 F7 STRING POS(0) 'C' | POS(0) 'E' :F(FRETURN) 44 STACK_COUNT = 1 45 STRING POS(0) 'C' = '#' 46 STRING POS(0) 'E' = '#' 47 STRING = REVERSE(STRING) 48 ONECH = LEN(1) . CH 49 F7.1 STRING ONECH = :F(FRETURN) * If it is a sentential variable push it onto the stack. 50 CH NOTANY('#NCAKE') :F(F7.2) 51 STACK[STACK_COUNT] = CH 52 STACK_COUNT = STACK_COUNT + 1 :(F7.1) * If it is a unary connective pop, concatenate, and push. 53 F7.2 CH 'N' :F(F7.3) 54 STACK[STACK_COUNT - 1] = STACK[STACK_COUNT - 1] CH :(F7.1) * If it is a binary connective pop, pop, concat, and push. 55 F7.3 CH ANY('CAKE') :F(F7.4) 56 STACK[STACK_COUNT - 2] = STACK[STACK_COUNT - 2] 56 + STACK[STACK_COUNT - 1] 56 + CH 57 STACK_COUNT = STACK_COUNT - 1 :(F7.1) * If it is the "C" or "E" from the beginning we are done. 58 F7.4 CH '#' :F(FRETURN) 59 IMPLICATION = REVERSE(STACK[2]) '#' REVERSE(STACK[1]) 60 F7END :(RETURN) * * * Controls the spacing of line numbers and internal * line numbers to keep the proof left justified * sp(in) 61 F8 SP = IN ' ' 62 SP PARENS :F(F8.2) * Internal line numbrs. They have a constant width of 7 * if they are used. Otherwise they are null. 63 EQ(NUM_PF_LINES,1) :F(F8.1) 64 SP = :(RETURN) 65 F8.1 * Right justify at line 7 66 SP '()' = 67 SP = DUPL(' ',7 - SIZE(SP)) SP :(RETURN) * Line numbers 68 F8.2 GE(IN,10) :S(RETURN) 69 F8END SP = ' ' SP :(RETURN) * * * center(in) 70 F9 EXCESS = PAGE_WIDTH - SIZE(IN) 71 GT(EXCESS,0) :F(FRETURN) 72 EQ(REMDR(EXCESS,2),0) :S(F9.1)F(F9END) 73 F9.1 CENTER = DUPL(' ',EXCESS / 2) IN :(RETURN) 74 F9END CENTER = DUPL(' ',(EXCESS + 1) / 2) IN :(RETURN) * * * abs(in) 75 F10 IN = INTEGER(IN) :F(FRETURN) 76 ABS = IN 77 ABS = LT(IN,0) -ABS 78 F10END :(RETURN) * * * cont_page() 79 F11 SPACES = 50 * WAS PAGE = 80 81 PAGE_OUT = 82 PAGE_OUT = CENTER(HEADING) 83 PAGE_OUT = 84 PAGE_OUT = DUPL(' ',SPACES) THS_NUM '(CONT.)' 85 SKIP(1) 86 F11END PAGE_LINES = 10 :(RETURN) -EJECT * * 87 START 88 DEFINE('initio()','INITIO1') 89 INITIO() 90 &STLIMIT = 1000000 91 &ERRLIMIT = 100 92 &TRIM = 1 93 &OUTPUT = 1 94 &INPUT = 1 95 &TRACE = 0 96 &DUMP = 1 97 &FTRACE = 0 * * 98 THEOREM = TABLE(300,20) 99 NAME = TABLE(220,10) 100 LINE = TABLE(70,5) 101 PART = TABLE(32,4) 102 SUB = TABLE(10,10) 103 ROMAN_TO_ARABIC = TABLE(5) 104 ROMAN_TO_ARABIC['I'] = 1 105 ROMAN_TO_ARABIC['II'] = 2 106 ROMAN_TO_ARABIC['III'] = 3 107 STACK = TABLE(8,2) 108 PF_LINE = TABLE(32,2) * * 109 MP_MARK = POS(0) 'C' 110 PM = (POS(0) '*1.01') 110 + | (POS(0) '*2.33') 110 + | (POS(0) '*3.01') 110 + | (POS(0) '*3.02') 110 + | (POS(0) '*4.01') 110 + | (POS(0) '*4.02') 110 + | (POS(0) '*4.34') 111 TI = (POS(0) '*4.1') 111 + | (POS(0) '*4.11') 111 + | (POS(0) '*4.12') 111 + | (POS(0) '*4.13') 111 + | (POS(0) '*4.14') 112 ASSUMP_MARK = 'ASSUMP' 113 CONJ_MARK = POS(0) '*3.03' 114 SYLL_MARK = (POS(0) 'Syll') | (POS(0) 'SYLL') 115 SUB_MARK = '/' 116 SE_MARK = POS(0) 'SE' 117 DE_MARK = POS(0) 'DE' | POS(0) 'DER' 118 MULTI_LINE_PF_MARK = '&' 119 COMMENT_MARK = POS(0) '+' 120 DIGIT = SPAN('()#*.0123456789') 121 DIGIT_SP = SPAN(' ()#.0123456789') 122 PARENS = ANY('()') * * 123 PAGE_NUM = 2 124 PAGE_WIDTH = 80 125 PAGE_LENGTH = 55 * * 126 DEFINE('substitution(sub_line,subs)s1,s2,s3,n1','F1') 127 DEFINE('skip(in)n1','F2') 128 DEFINE('put_page()','F3') 129 DEFINE('arabic(in)n','F4') * DJD Got Rid of OUTPUT_CONTROL() 130 131 DEFINE('init_trace()','INTR') * DJD NOTE: There is built in 'REVERSE' funtion (do not need F6) 132 DEFINE('implication(string)','F7') 133 DEFINE('sp(in)','F8') 134 DEFINE('center(in)excess','F9') 135 DEFINE('abs(in)','F10') 136 DEFINE('cont_page()','F11') * * * 137 INIT_TRACE() * BLANK LINES for moved TRACE calls - line numbers 138 139 140 141 142 143 144 * Read in a Title Page * skip(15) 145 T1 TITLE_PAGE = CENTER(INPUT) 146 TITLE_PAGE 'END_OF_TITLE' :S(T2) 147 PAGE_OUT = TITLE_PAGE :(T1) 148 T2 149 150 151 152 -EJECT * * * Read in a heading for each page. * Use it to determine the set of definitions to use. 153 HEADING = CENTER(INPUT) 154 HEADING 'PRINCIPIA MATHEMATICA' :F(HEAD1) 155 REP_MARK = PM :(PRINT) 156 HEAD1 HEADING 'THE THEORY OF IMPLICATION' :F(ERROR1) 157 REP_MARK = TI :(PRINT) * * * Get the date 158 PRINT DATE_PM = DATE() * * * DJD REMOVED PRINTER CONTROL 159 160 161 * * Read in the proof line abbreviation and the thesis. 162 READ 163 &INPUT = 1 * Set up the initial conditions on the proof * abbreviation to be read in and the full proof * to be generated. 164 LINE_NUM = 0 165 NUM_PF_LINES = 1 166 JUST = 0 167 READ4 PROOF = INPUT :F(TABLE_DJD) 168 PROOF COMMENT_MARK :F(READ1) 169 PROOF COMMENT_MARK = 170 PAGE_OUT = PROOF :(READ4) 171 READ1 PF_LINE[1] = PROOF 172 PROOF MULTI_LINE_PF_MARK :F(READ2) 173 JUST = 7 174 PROOF BREAK(MULTI_LINE_PF_MARK) . NUM_PF_LINES 175 PROOF NUM_PF_LINES MULTI_LINE_PF_MARK = :F(ERROR1) 176 PF_LINE[1] = PROOF 177 PF_LINE_NUM = 1 178 READ3 PF_LINE_NUM = PF_LINE_NUM + 1 179 PF_LINE[PF_LINE_NUM] = INPUT 180 GE(PF_LINE_NUM,NUM_PF_LINES) :F(READ3) 181 READ2 THESIS = INPUT :F(ERROR1) 182 THESIS DIGIT . THS_NUM * DJD PRINT CONTROL REMOVED 183 184 PUT_PAGE() * If &OUTPUT is not positive don't construct the proof. * DJD & OUTPUT is now always positive 185 GE(&OUTPUT,1) :S(THM) * Put the thesis to be proved in the theorem table. 186 THESIS DIGIT_SP REM . THEOREM[THS_NUM] * If the theorem has a blank there is a name. 187 THEOREM[THS_NUM] BREAK(' ') . THEOREM[THS_NUM] 187 + SPAN(' ') REM . NAME[THS_NUM] 187 + :F(READ) 188 NAME[THS_NUM] = '(' NAME[THS_NUM] ')' 189 :(READ) -EJECT * * * Now analyze the proof line. * If the proof doesn't contain 'AX', 'DEF', or 'INF' it is a theorem. 190 THM PROOF 'AX' | 'DEF' | 'INF' :S(AX) 191 DELIM = ANY('+-;') * Put the thesis to be proved in the theorem table. 192 THESIS DIGIT . THM_NUM SPAN(' ') . B 193 THESIS DIGIT_SP REM . THEOREM[THM_NUM] * If the theorem has a blank there is a name. 194 THEOREM[THM_NUM] BREAK(' ') . THEOREM[THM_NUM] 194 + SPAN(' ') REM . NAME[THM_NUM] 194 + :F(THM.1) 195 NAME[THM_NUM] = '(' NAME[THM_NUM] ')' 196 THM.1 197 PAGE_OUT = THM_NUM ' ' THEOREM[THM_NUM] ' ' NAME[THM_NUM] 198 SKIP(1) * * Print the proof abbreviation. 199 PAGE_OUT = 'PROOF ABBREVIATION' 200 PF_LINE_NUM = 0 201 PF1 PF_LINE_NUM = PF_LINE_NUM + 1 202 PAGE_OUT = PF_LINE[PF_LINE_NUM] 203 GE(PF_LINE_NUM,NUM_PF_LINES) :F(PF1) * * Print the full proof. 204 SKIP(1) 205 PAGE_OUT = 'PROOF' 206 PAGE_LINES = PAGE_LINES + NUM_PF_LINES + 2 * Get the parts out of the proof line. 207 PF_LINE_NUM = 0 208 PF2 PF_LINE_NUM = PF_LINE_NUM + 1 209 PROOF = PF_LINE[PF_LINE_NUM] 210 GT(PF_LINE_NUM,NUM_PF_LINES) :S(ERROR6) 211 PROOF = PROOF '+' 212 PART_NUM = 0 213 LOOP1 PART_NUM = PART_NUM + 1 214 PROOF BREAK('+-;') . PART[PART_NUM] :F(THS) 215 PROOF PART[PART_NUM] DELIM = :(LOOP1) * * * If the proof contains 'AX' it is an axiom. 216 AX PROOF 'AX' :F(DEF) 217 THESIS DIGIT . AX_NUM 218 THESIS DIGIT_SP REM . THEOREM[AX_NUM] 219 THEOREM[AX_NUM] BREAK(' ') . THEOREM[AX_NUM] 219 + SPAN(' ') REM . NAME[AX_NUM] 219 + :F(AX.1) 220 NAME[AX_NUM] = '(' NAME[AX_NUM] ')' * Leave parens off axiom name in input 221 AX.1 SKIP(2) 222 PAGE_OUT = AX_NUM ' ' THEOREM[AX_NUM] ' Pp. ' NAME[AX_NUM] 223 :(READ) * * * If the proof contains 'DEF' it is a definition. 224 DEF PROOF 'DEF' :F(INF) 225 THESIS DIGIT . DEF_NUM 226 THESIS DIGIT_SP REM . THEOREM[DEF_NUM] * If the definition has a blank there is a name. 227 THEOREM[DEF_NUM] BREAK(' ') . THEOREM[DEF_NUM] 227 + SPAN(' ') REM . NAME[DEF_NUM] 227 + :F(DEF.1) * DJD Leave parens off name input!!! 228 NAME[DEF_NUM] = '(' NAME[DEF_NUM] ')' * ABOVE LINE RE-COMMENTED 6/13/17 DJD 229 DEF.1 SKIP(2) * LINE MISSING FROM BOTTOM OF PAGE DJD 6/12/17 - fixed 6/13/17 230 PAGE_OUT = DEF_NUM ' ' THEOREM[DEF_NUM] ' Df. ' NAME[DEF_NUM] 231 :(READ) * * * If the proof contains 'INF' just read in the words. * Note that '#' is an end of text marker. 232 INF PROOF 'INF' :F(ERROR1) 233 SKIP(2) 234 INF.1 THESIS '#' :S(INF.2) 235 PAGE_OUT = THESIS 236 THESIS = INPUT :(INF.1) 237 INF.2 THESIS '#' = ' Pp.' 238 PAGE_OUT = THESIS 239 :(READ) -EJECT * * * Parse each part and construct the line. * First turn off input for efficiency. See Griswold, * Poage, and Polonsky section 11.5. 240 THS &INPUT = 1 241 BIGGEST_PART_NUM = PART_NUM - 1 * The line number is set to zero up at read, so that * it will be incremented through the whole proof as * each proof line is analyzed. * I wish to print the line numbers used in the proof * abbreviations. They are at the end of each proof * abbreviation and they contain left and right * parenthesis. They will be called internal line numbers. 242 PART_NUM = 0 243 INT_LINE_NUM = '()' * DJD 6/19/17 - removed spaces around () above I had added * seemed to make no difference * cannot tell from printout. 244 PARSE PART_NUM = PART_NUM + 1 245 EQ(PART_NUM,BIGGEST_PART_NUM - 1) :F(PARSE1) 246 PART[BIGGEST_PART_NUM] PARENS :F(PARSE1) 247 INT_LINE_NUM = PART[BIGGEST_PART_NUM] 248 PARSE1 * Check for skip to a new page because the proof is too long. 249 GE(PAGE_LINES,PAGE_LENGTH) CONT_PAGE() 250 LINE_NUM = LINE_NUM + 1 251 GT(PART_NUM,BIGGEST_PART_NUM) :S(ERROR6) * The part must call for modus ponens, substitution, * replacement, syll, sub. Of EQ, * Or placing a previously proved theorem * on a line. The line to be proved must be in the * last part; all other single numbers are placements * on a line. 252 PART[PART_NUM] MP_MARK :S(MP) 253 PART[PART_NUM] CONJ_MARK :S(CONJ) 254 PART[PART_NUM] ASSUMP_MARK :S(ASSUMP) 255 PART[PART_NUM] REP_MARK :S(REP) 256 PART[PART_NUM] SYLL_MARK :S(SYLL) 257 PART[PART_NUM] SE_MARK :S(SE) 258 PART[PART_NUM] SUB_MARK :S(SUB) 259 PART[PART_NUM] DE_MARK :S(DE) 260 EQ(PART_NUM,BIGGEST_PART_NUM) :F(PLACE)S(COMP) * * * Substutution rule * Get the theorem number 261 SUB PART[PART_NUM] DIGIT . THM_NUM SPAN(' ') . B :F(ERROR2) * Print the theorem and, if any, the substitutions. 262 PART[PART_NUM] PARENS :F(SUB.1) 263 LINE_NUM = LINE_NUM - 1 :(SUB.2) 264 SUB.1 LINE[LINE_NUM] = THEOREM[THM_NUM] 265 PAGE_OUT = DUPL(' ',JUST) SP(LINE_NUM) LINE[LINE_NUM] 265 + ' ' THM_NUM ' ' NAME[THM_NUM] 266 SUB.2 PART[PART_NUM] THM_NUM B = 267 PAGE_OUT = DUPL(' ',JUST + 6) PART[PART_NUM] * Now perform the substitution and print the result. 268 LINE[LINE_NUM + 1] = SUBSTITUTION(LINE[LINE_NUM], 268 + PART[PART_NUM]) 269 LINE_NUM = LINE_NUM + 1 270 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] ' SUB' 271 PAGE_LINES = PAGE_LINES + 3 272 :(PARSE) * * 273 MP * MODUS PONENS * CPQ, The antecedant p, and the consequent q. The proof * part gives us the antecedant only. The antecedant is * constructed first, then we back up through the proof to * the implication, and finally pull out the consequent. * First construct the antecedant. 274 PART[PART_NUM] 'C' DIGIT . THM_NUM * The implication could already be in the proof. This is * true iff the theorem number has left and right parens. 275 THM_NUM PARENS :F(LMP4) * Back up through the proof until we get the antecedant. * Decrement the line number because we do not generate * a new line. 276 LINE_NUM = LINE_NUM - 1 277 ANT_NUM = LINE_NUM 278 LMP5 LINE[ANT_NUM] POS(0) THEOREM[THM_NUM] RPOS(0) :S(LMP1) 279 ANT_NUM = ANT_NUM - 1 280 EQ(ANT_NUM,0) :S(ERROR5)F(LMP5) * The implication is not already in the proof. 281 LMP4 LINE[LINE_NUM] = THEOREM[THM_NUM] 282 ANT_NUM = LINE_NUM 283 PAGE_OUT = DUPL(' ',JUST) SP(LINE_NUM) LINE[LINE_NUM] 283 + ' ' THM_NUM ' ' NAME[THM_NUM] 284 PAGE_LINES = PAGE_LINES + 1 * Test for a substitution. 285 PART[PART_NUM] '/' :F(LMP1) 286 PART[PART_NUM] 'C' THM_NUM SPAN(' ') REM . TEMP 287 PAGE_OUT = DUPL(' ',JUST + 6) TEMP 288 LINE[LINE_NUM + 1] = SUBSTITUTION(LINE[LINE_NUM],TEMP) 289 LINE_NUM = LINE_NUM + 1 290 ANT_NUM = LINE_NUM 291 PAGE_OUT = DUPL(' ',JUST) SP(LINE_NUM) LINE[LINE_NUM] 291 + ' SUB' 292 PAGE_LINES = PAGE_LINES + 2 * Now find the implication. 293 LMP1 IMP_NUM = LINE_NUM * The implication can be in one of three forms: CPQ, EPQ, or EQP. * In each case we know only p. When it may be EQP then the * length of q must be computed so that it may be skipped. * q itself is not known. * PAGE_OUT = 'line[ant_num] =' line[ant_num] * PAGE_OUT = 'ant_num = ' ant_num * LMP3 PAGE_OUT = 'line[imp_num] =' line[imp_num] * PAGE_OUT = 'imp_num = ' imp_num 294 LMP3 LINE[IMP_NUM] POS(0) ('C' | 'E') LINE[ANT_NUM] REM . CONCLUSION 294 + :S(LMP2) 295 LINE[IMP_NUM] POS(0) ('E' ARB . CONCLUSION LINE[ANT_NUM]) RPOS(0) 295 + :S(LMP2) 296 IMP_NUM = GT(IMP_NUM,1) IMP_NUM - 1 :F(ERROR5)S(LMP3) * Now pull out the consequent. 297 LMP2 LINE_NUM = LINE_NUM + 1 * PAGE_OUT = 'CONCLUSION = ' conclusion 298 LINE[LINE_NUM] = LINE[IMP_NUM] * Check the result. * Allow either 'C' or 'E' on the front. 299 LINE[LINE_NUM] POS(0) ('C' | 'E') LINE[ANT_NUM] = :S(LMP6) * This will allow p to be derived from EPQ and q. 300 LINE[LINE_NUM] = IMPLICATION(LINE[LINE_NUM]) 301 LINE[LINE_NUM] '#' LINE[ANT_NUM] = :F(ERROR5) 302 LMP6 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 302 + ' MP: ' IMP_NUM ', ' ANT_NUM 303 PAGE_LINES = PAGE_LINES + 1 304 :(PARSE) * * * Replacement rule * Get the definition number. 305 REP PART[PART_NUM] DIGIT . DEF_NUM 306 TEMP = THEOREM[DEF_NUM] 307 PAGE_OUT = DUPL(' ',JUST + 6) TEMP ' Df. ' DEF_NUM 307 + ' ' NAME[DEF_NUM] 308 PAGE_LINES = PAGE_LINES + 1 * * 309 REPLACEMENT_SPOT = 1 310 SPOT = * Test for a roman numeral. 311 PART[PART_NUM] 'I' :F(LREP1) 312 PART[PART_NUM] BREAK('I') SPAN('I') . SPOT :F(ERROR3) 313 PART[PART_NUM] SPOT = :F(ERROR3) 314 REPLACEMENT_SPOT = ARABIC(SPOT) :F(ERROR3) 315 PART[PART_NUM] = TRIM(PART[PART_NUM]) * Test for a substitution. 316 LREP1 PART[PART_NUM] SUB_MARK :F(LREP2) 317 PART[PART_NUM] DEF_NUM SPAN(' ') = :F(ERROR3) 318 TEMP = SUBSTITUTION(TEMP,PART[PART_NUM]) 319 PAGE_OUT = DUPL(' ',JUST + 9) PART[PART_NUM] 320 PAGE_OUT = DUPL(' ',JUST + 6) TEMP ' Df.' 321 PAGE_LINES = PAGE_LINES + 2 322 LREP2 TEMP (BREAK('=') . LHS) '=' (REM . RHS) :F(ERROR3) 323 LINE[LINE_NUM] = LINE[LINE_NUM - 1] * Assume the right side of the definition is to be replaced * by the left side. If not we reverse the right and left * sides of the definition and proceed. 324 LINE[LINE_NUM] RHS :S(LREP6) 325 S = RHS 326 RHS = LHS 327 LHS = S * Determine the place for the replacement. * If replacement spot is one, snobol4 * Will do the job automatically. * Use '#' to mark the places we don't want to touch. 328 LREP6 EQ(REPLACEMENT_SPOT,1) :S(LREP4) 329 N = 0 330 LREP3 N = N + 1 331 LINE[LINE_NUM] RHS = '#' :F(ERROR3) 332 EQ(N,REPLACEMENT_SPOT - 1) :F(LREP3) 333 LREP4 LINE[LINE_NUM] RHS = LHS :F(ERROR3) 334 LREP5 LINE[LINE_NUM] '#' = RHS :S(LREP5) 335 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 335 + ' REP ' SPOT 336 PAGE_LINES = PAGE_LINES + 1 337 :(PARSE) * * * Place a previously proved theorem on a line * unless it is there already. It is iff the theorem' * number has left and right parens. If this is true * we also give back the new line number we got. 338 PLACE PART[PART_NUM] PARENS :F(PLACE1) 339 LINE_NUM = LINE_NUM - 1 :(PARSE) 340 PLACE1 LINE[LINE_NUM] = THEOREM[PART[PART_NUM]] :F(ERROR4) 341 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 341 + ' ' PART[PART_NUM] ' ' 341 + NAME[PART[PART_NUM]] 342 PAGE_LINES = PAGE_LINES + 1 343 :(PARSE) * * * This places an assumption on a proof line. 344 ASSUMP 345 PART[PART_NUM] 'ASSUMP' SPAN(' ') = :F(ERROR4) 346 LINE[LINE_NUM] = PART[PART_NUM] 347 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 347 + ' ASSUMP' 348 PAGE_LINES = PAGE_LINES + 1 349 :(PARSE) * This is a binary rule which takes in previously proved * formulas of the form CPQ, CQR and gives as result CPR. 350 SYLL * Get out the theorem numbers 351 PART[PART_NUM] 'SYLL' SPAN(' ') DIGIT . THM1 351 + SPAN(', ') DIGIT . THM2 :F(ERROR7) * Back up through the proof until the theorems are found. 352 BACK_UP = LINE_NUM - 1 353 MATCH = 0 354 SYLL1 LINE[BACK_UP] POS(0) THEOREM[THM1] RPOS(0) :S(SYLL2) 355 LINE[BACK_UP] POS(0) THEOREM[THM2] RPOS(0) 355 + :S(SYLL3)F(SYLL4) 356 SYLL2 NUM_THM1 = BACK_UP 357 MATCH = MATCH + 1 :(SYLL4) 358 SYLL3 NUM_THM2 = BACK_UP 359 MATCH = MATCH + 1 360 SYLL4 BACK_UP = BACK_UP - 1 361 EQ(MATCH,2) :S(SYLL5) 362 EQ(BACK_UP,0) :F(SYLL1) 363 SYLL5 THM1 = IMPLICATION(LINE[NUM_THM1]) :F(ERROR7) 364 THM2 = IMPLICATION(LINE[NUM_THM2]) :F(ERROR7) 365 THM1 BREAK('#') . ANT1 '#' REM . CONS1 366 THM2 BREAK('#') . ANT2 '#' REM . CONS2 367 CONS1 ANT2 :F(SYLL6) 368 LINE[LINE_NUM] = 'C' ANT1 CONS2 :(SYLL7) 369 SYLL6 ANT1 CONS2 :F(ERROR7) 370 LINE[LINE_NUM] = 'C' ANT2 CONS1 371 SYLL7 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 371 + ' SYLL: ' NUM_THM1 ', ' NUM_THM2 372 PAGE_LINES = PAGE_LINES + 1 373 :(PARSE) * * * Substivity of equivalence' 374 SE 375 PART[PART_NUM] ':' :F(SEE) 376 PART[PART_NUM] SE_MARK SPAN(' (') BREAK(':') . S1 376 + ':' BREAK(')') . S2 :F(ERROR9) * Get the theorem numbers out and print the theorems. 377 S1 DIGIT . THM_NUM_LHS 378 S2 DIGIT . THM_NUM_RHS 379 LHS = THEOREM[THM_NUM_LHS] 380 RHS = THEOREM[THM_NUM_RHS] 381 PAGE_OUT = DUPL(' ',JUST + 6) LHS ' ' THM_NUM_LHS ' : ' 381 + RHS ' ' THM_NUM_RHS 382 PAGE_LINES = PAGE_LINES + 1 383 SUB_LHS = 384 SUB_RHS = * Test for substitutions on the lhs. 385 S1 SUB_MARK :F(SE1) 386 S1 THM_NUM_LHS SPAN(' ') = :F(ERROR9) 387 SUB_LHS = S1 388 LHS = SUBSTITUTION(LHS,SUB_LHS) * Test for substitutions on the rhs. 389 SE1 S2 SUB_MARK :F(SE2) 390 S2 THM_NUM_RHS SPAN(' ') = :F(ERROR9) 391 SUB_RHS = S2 392 RHS = SUBSTITUTION(RHS,SUB_RHS) * If there are substitutions, then print them and their result. 393 SE2 EQ(SIZE(SUB_LHS) + SIZE(SUB_RHS),0) :S(SE3) 394 PAGE_OUT = DUPL(' ',JUST + 9) SUB_LHS ' : ' SUB_RHS 395 PAGE_OUT = DUPL(' ',JUST + 6) LHS ' : ' RHS 396 PAGE_LINES = PAGE_LINES + 2 * Verify that the anrecedants and consequents match properly. 397 SE3 LHS = IMPLICATION(LHS) :F(ERROR9) 398 RHS = IMPLICATION(RHS) :F(ERROR9) 399 LHS BREAK('#') . ANT_LHS '#' REM . CONS_LHS :F(ERROR9) 400 RHS BREAK('#') . ANT_RHS '#' REM . CONS_RHS :F(ERROR9) 401 ANT_LHS CONS_RHS :F(ERROR9) 402 ANT_RHS CONS_LHS :F(ERROR9) * Now make the replacement. 403 LINE[LINE_NUM] = LINE[LINE_NUM - 1] 404 LINE[LINE_NUM] ANT_LHS = CONS_LHS :S(SE4) 405 LINE[LINE_NUM] CONS_LHS = ANT_LHS :F(ERROR9) 406 SE4 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] ' SE' 407 PAGE_LINES = PAGE_LINES + 1 408 :(PARSE) * * 409 SEE PART[PART_NUM] SE_MARK SPAN(' (') BREAK(')') . S1 :F(ERROR11) * Get the theorem number. 410 S1 DIGIT . THM_NUM 411 THM = THEOREM[THM_NUM] 412 PAGE_OUT = DUPL(' ',JUST + 6) THM ' ' THM_NUM 413 PAGE_LINES = PAGE_LINES + 1 * Test for implication. 414 THM POS(0) 'E' :F(ERROR11) * Test for substitutions. 415 S1 SUB_MARK :F(SEE1) 416 S1 THM_NUM SPAN(' ') = :F(ERROR11) 417 PAGE_OUT = DUPL(' ',JUST + 9) S1 418 THM = SUBSTITUTION(THM,S1) 419 PAGE_OUT = DUPL(' ',JUST + 6) THM 420 PAGE_LINES = PAGE_LINES + 2 421 SEE1 THM = IMPLICATION(THM) :F(ERROR11) 422 THM BREAK('#') . S1 '#' REM . S2 :F(ERROR11) * Make the replacement. * It is made in this order since the most common use is * to change NNP to P using EPNNP. 423 LINE[LINE_NUM] = LINE[LINE_NUM - 1] 424 LINE[LINE_NUM] S2 = S1 :S(SEE2) * If it didn't work, try the other way. 425 LINE[LINE_NUM] S1 = S2 :F(ERROR11) 426 SEE2 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) 426 + LINE[LINE_NUM] ' SE' 427 PAGE_LINES = PAGE_LINES + 1 428 PAGE_LINES = PAGE_LINES + 1 429 :(PARSE) * * * PM rule called "CONJ" * This is a binary rule which takes in previously proved * formulas and returns their conjunction. 430 CONJ * Get out the theorem numbers. 431 PART[PART_NUM] '*3.03' SPAN(' ') DIGIT . THM1 431 + SPAN(', ') DIGIT . THM2 :F(ERROR10) * Back up through the proof until the theorems are found. 432 BACK_UP = LINE_NUM - 1 433 MATCH = 0 434 CONJ1 LINE[BACK_UP] POS(0) THEOREM[THM1] RPOS(0) :S(CONJ2) 435 LINE[BACK_UP] POS(0) THEOREM[THM2] RPOS(0) 435 + :S(CONJ3)F(CONJ4) 436 CONJ2 NUM_THM1 = BACK_UP 437 MATCH = MATCH + 1 :(CONJ4) 438 CONJ3 NUM_THM2 = BACK_UP 439 MATCH = MATCH + 1 440 CONJ4 BACK_UP = BACK_UP - 1 441 EQ(MATCH,2) :S(CONJ5) 442 EQ(BACK_UP,0) :F(CONJ1) 443 CONJ5 LINE[LINE_NUM] = 'K' LINE[NUM_THM1] LINE[NUM_THM2] 444 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] 444 + ' *3.03: ' NUM_THM1 ', ' NUM_THM2 445 PAGE_LINES = PAGE_LINES + 1 446 :(PARSE) * * * This rule takes a theorem of the form EPQ and returns * either CPQ or CQP (for DER). 447 DE 448 PART[PART_NUM] DE_MARK :F(ERROR12) 449 PART[PART_NUM] POS(0) 'DER' :S(DE1) 450 LINE[LINE_NUM] = LINE[LINE_NUM - 1] 451 LINE[LINE_NUM] POS(0) 'E' = 'C' :F(ERROR12) 452 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] ' DE' 453 PAGE_LINES = PAGE_LINES + 1 454 :(PARSE) 455 DE1 TEMP = IMPLICATION(LINE[LINE_NUM - 1]) 456 TEMP BREAK('#') . S1 '#' REM . S2 :F(ERROR12) 457 LINE[LINE_NUM] = 'C' S2 S1 458 PAGE_OUT = SP(INT_LINE_NUM) SP(LINE_NUM) LINE[LINE_NUM] ' DER' 459 PAGE_LINES = PAGE_LINES + 1 460 :(PARSE) * * * Compare the theorem proved with that which was read in. 461 COMP THESIS DIGIT . THM_NUM * The line number which had been incremented in anticipation * of another inference rule. 462 LINE_NUM = LINE_NUM - 1 * First see if this is the last line of the proof * or just of the proof abbreviation. 463 PART[PART_NUM] (THM_NUM | 'PROP' | 'Prop') :S(COMP1) * Save the proved line for later use. 464 THEOREM[PART[PART_NUM]] = LINE[LINE_NUM] :(PF2) 465 COMP1 LINE[LINE_NUM] POS(0) THEOREM[THM_NUM] RPOS(0) :F(PROB) 466 :(READ) 467 PROB PAGE_OUT = DUPL('*',60) 468 PAGE_OUT = 'The last line of the proof and the thesis' 469 PAGE_OUT = 'which was read in do not agree!' 470 PAGE_OUT = 'The program takes the thesis which was' 471 PAGE_OUT = 'read in to be correct;' 472 PAGE_OUT = THM_NUM ' ' THEOREM THEOREM[THM_NUM] 473 PAGE_OUT = DUPL('*',60) 474 :(READ) * * * This section prints out theorems and definitions read in. 475 TABLE_DJD 476 THS_NUM = ' ' 477 DATE_DJD = DATE() 478 HEADING = 'SUMMARY OF THEOREMS AND DEFINITIONS' 479 PUT_PAGE() 480 THEOREMS = CONVERT(THEOREM,'ARRAY') 481 J = 0 482 I = 1 483 TABLE1 * In the next step failure could mean the end of the array. 484 TABLE2 THEOREMS[I,1] POS(0) '*' :F(TABLE3) 485 PAGE_OUT = THEOREMS[I,1] DUPL(' ',8 - SIZE(THEOREMS[I,1])) 485 + THEOREMS[I,2] ' ' NAME[THEOREMS[I,1]] :F(END) 486 J = J + 1 * See if the array has ended. If yes, finish. 487 TABLE3 THEOREMS[I,1] :F(END) 488 I = I + 1 489 EQ(0,REMDR(J,50)) :F(TABLE2) 490 CONT_PAGE() :(TABLE1) -EJECT * ERROR OUTPUT SECTION 491 ERROR1 ST_NUM = &LASTNO 492 SKIP(2) 493 PAGE_OUT = DUPL('*',60) 494 PAGE_OUT = 'READ ERROR' 495 PAGE_OUT = 'PROOF IS ' PROOF 496 PAGE_OUT = 'THESIS IS ' THESIS 497 PAGE_OUT = 'HEADING IS ' HEADING 498 PAGE_OUT = 'ST. NUM IS ' ST_NUM 499 :(READ) 500 ERROR2 ST_NUM = &LASTNO 501 SKIP(2) 502 PAGE_OUT = DUPL('*',60) 503 PAGE_OUT = 'SUBSTITUTION ERROR' 504 PAGE_OUT = 'THESIS IS ' THESIS 505 PAGE_OUT = 'P/N ' PART_NUM ' ' PART[PART_NUM] 506 PAGE_OUT = 'L/N ' LINE_NUM ' ' LINE[LINE_NUM] 507 PAGE_OUT = 'ST. NUM IS ' ST_NUM 508 :(READ) 509 ERROR3 ST_NUM = &LASTNO 510 SKIP(2) 511 PAGE_OUT = DUPL('*',60) 512 PAGE_OUT = 'REPLACEMENT ERROR' 513 PAGE_OUT = 'P/N ' PART_NUM ' ' PART[PART_NUM] 514 PAGE_OUT = 'DEF ' DEF_NUM ' ' THEOREM[DEF_NUM] 515 PAGE_OUT = 'TEMP ' TEMP 516 PAGE_OUT = 'RHS ' RHS 517 PAGE_OUT = 'LHS ' LHS 518 PAGE_OUT = 'REPLACEMENT SPOT ' REPLACEMENT_SPOT 519 PAGE_OUT = 'SPOT ' SPOT 520 PAGE_OUT = 'ST. NUM IS ' ST_NUM 521 :(READ) 522 ERROR4 ST_NUM = &LASTNO 523 SKIP(2) 524 PAGE_OUT = DUPL('*',60) 525 PAGE_OUT = 'PLACE ERROR' 526 PAGE_OUT = 'L/N ' LINE_NUM 527 PAGE_OUT = 'P/N ' PART_NUM 528 PAGE_OUT = 'PART ' PART[PART_NUM] 529 PAGE_OUT = 'ST. NUM IS ' ST_NUM 530 :(READ) 531 ERROR5 ST_NUM = &LASTNO 532 SKIP(2) 533 PAGE_OUT = DUPL('*',60) 534 PAGE_OUT = 'MODUS PONENS ERROR' 535 PAGE_OUT = 'ST. NUM IS ' ST_NUM 536 PAGE_OUT = 'IMP_NUM IS ' IMP_NUM 537 PAGE_OUT = 'LINE[IMP_NUM] IS ' LINE[IMP_NUM] 538 PAGE_OUT = 'ANT_NUM IS ' ANT_NUM 539 PAGE_OUT = 'LINE[ANT_NUM] IS ' LINE[ANT_NUM] 540 :(READ) 541 ERROR6 ST_NUM = &LASTNO 542 SKIP(2) 543 PAGE_OUT = DUPL('*',60) 544 PAGE_OUT = 'PF LINE OR PART ERROR' 545 PAGE_OUT = 'ST. NUM IS ' ST_NUM 546 :(READ) 547 ERROR7 ST_NUM = &LASTNO 548 SKIP(2) 549 PAGE_OUT = DUPL('*',60) 550 PAGE_OUT = 'SYLL ERROR' 551 PAGE_OUT = 'THM1 IS ' THM1 552 PAGE_OUT = 'THM2 IS ' THM2 553 PAGE_OUT = 'ST. NUM IS ' ST_NUM 554 PAGE_OUT = 'ANT1 IS ' ANT1 555 PAGE_OUT = 'CONS1 IS ' CONS1 556 PAGE_OUT = 'ANT2 IS ' ANT2 557 PAGE_OUT = 'CONS2 IS ' CONS2 558 :(READ) 559 ERROR8 ST_NUM = &LASTNO 560 SKIP(2) 561 PAGE_OUT = DUPL('*',60) 562 PAGE_OUT = 'SE ERROR' 563 PAGE_OUT = 'ST. NUM IS ' ST_NUM 564 PAGE_OUT = 'LINE IS ' LINE[LINE_NUM] 565 PAGE_OUT = 'LINE NUMBER IS ' LINE_NUM 566 PAGE_OUT = 'LHS ' LHS 567 PAGE_OUT = 'RHS ' RHS 568 :(READ) 569 ERROR9 ST_NUM = &LASTNO 570 SKIP(2) 571 PAGE_OUT = DUPL('*',60) 572 PAGE_OUT = 'SE ERROR' 573 PAGE_OUT = 'PART IS ' PART[PART_NUM] 574 PAGE_OUT = 'S1 IS ' S1 575 PAGE_OUT = 'S2 IS ' S2 576 PAGE_OUT = 'LHS ' LHS 577 PAGE_OUT = 'RHS ' RHS 578 PAGE_OUT = 'SUB_LHS IS ' SUB_LHS 579 PAGE_OUT = 'SUB_RHS IS ' SUB_RHS 580 PAGE_OUT = 'ST. NUM IS ' ST_NUM 581 :(READ) 582 ERROR10 ST_NUM = &LASTNO 583 SKIP(2) 584 PAGE_OUT = DUPL('*',60) 585 PAGE_OUT = 'CONJ ERROR' 586 PAGE_OUT = 'THM1 IS ' THM1 587 PAGE_OUT = 'THM2 IS ' THM2 588 PAGE_OUT = 'ST. NUM IS ' ST_NUM 589 :(READ) 590 ERROR11 ST_NUM = &LASTNO 591 SKIP(2) 592 PAGE_OUT = DUPL('*',60) 593 PAGE_OUT = 'SE (EQUIV.) ERROR' 594 PAGE_OUT = 'PART IS ' PART[PART_NUM] 595 PAGE_OUT = 'S1 IS ' S1 596 PAGE_OUT = 'S2 IS ' S2 597 PAGE_OUT = 'THM IS ' THM 598 PAGE_OUT = 'ST. NUM IS ' ST_NUM 599 :(READ) 600 ERROR12 ST_NUM = &LASTNO 601 SKIP(2) 602 PAGE_OUT = DUPL('*',60) 603 PAGE_OUT = 'DE OR DER ERROR' 604 PAGE_OUT = 'PART IS ' PART[PART_NUM] 605 PAGE_OUT = 'S1 IS ' S1 606 PAGE_OUT = 'S2 IS ' S2 607 PAGE_OUT = 'ST. NUM IS ' ST_NUM 608 :(READ) 609 610 INITIO1 INPUT('INPUT',5,4096,'data_in00.txt') 611 OUTPUT('OUTPUT',6,4096,'data_out00.txt') 612 OUTPUT('page_out',7,4096,'page_out00.txt') 613 INITIO2 OUTPUT('debug_out',8,4096,'debug_out00.txt') :(RETURN) 614 615 616 INTR TRACE('HEAD1','LABEL') 617 TRACE('PRINT','LABEL') 618 TRACE('READ','LABEL') 619 TRACE('THM','LABEL') 620 TRACE('THM.1','LABEL') 621 TRACE('PF1','LABEL') 622 TRACE('PF2','LABEL') 623 TRACE('LOOP1','LABEL') 624 TRACE('AX','LABEL') 625 TRACE('AX1','LABEL') 626 TRACE('INF','LABEL') 627 TRACE('INF.1','LABEL') 628 TRACE('INF.2','LABEL') 629 TRACE('THS','LABEL') 630 TRACE('PARSE','LABEL') 631 TRACE('PARSE1','LABEL') 632 TRACE('SUB','LABEL') 633 TRACE('SUB.1','LABEL') 634 TRACE('SUB.2','LABEL') 635 TRACE('MP','LABEL') 636 TRACE('LMP5','LABEL') 637 TRACE('LMP4','LABEL') 638 TRACE('LMP1','LABEL') 639 TRACE('LMP3','LABEL') 640 TRACE('LMP2','LABEL') 641 TRACE('LMP6','LABEL') 642 TRACE('REP','LABEL') 643 TRACE('LREP1','LABEL') 644 TRACE('LREP2','LABEL') 645 TRACE('LREP6','LABEL') 646 TRACE('LREP3','LABEL') 647 TRACE('LREP4','LABEL') 648 TRACE('LREP5','LABEL') 649 TRACE('PLACE','LABEL') 650 TRACE('PLACE1','LABEL') 651 TRACE('ASSUMP','LABEL') 652 TRACE('SYLL','LABEL') 653 TRACE('SYLL1','LABEL') 654 TRACE('SYLL2','LABEL') 655 TRACE('SYLL3','LABEL') 656 TRACE('SYLL4','LABEL') 657 TRACE('SYLL5','LABEL') 658 TRACE('SYLL6','LABEL') 659 TRACE('SYLL7','LABEL') 660 TRACE('SE','LABEL') 661 TRACE('SE1','LABEL') 662 TRACE('SE2','LABEL') 663 TRACE('SE3','LABEL') 664 TRACE('SE4','LABEL') 665 TRACE('SEE','LABEL') 666 TRACE('SEE1','LABEL') 667 TRACE('SEE2','LABEL') 668 TRACE('CONJ','LABEL') 669 TRACE('CONJ1','LABEL') 670 TRACE('CONJ2','LABEL') 671 TRACE('CONJ3','LABEL') 672 TRACE('CONJ4','LABEL') 673 TRACE('CONJ5','LABEL') 674 TRACE('DE','LABEL') 675 TRACE('DE1','LABEL') 676 TRACE('COMP','LABEL') 677 TRACE('COMP1','LABEL') 678 TRACE('TABLE_DJD','LABEL') 679 TRACE('TABLE1','LABEL') 680 TRACE('TABLE2','LABEL') 681 TRACE('TABLE3','LABEL') 682 TRACE('ERROR1','LABEL') 683 TRACE('ERROR2','LABEL') 684 TRACE('ERROR3','LABEL') 685 TRACE('ERROR4','LABEL') 686 TRACE('ERROR5','LABEL') 687 TRACE('ERROR6','LABEL') 688 TRACE('ERROR7','LABEL') 689 TRACE('ERROR8','LABEL') 690 TRACE('ERROR9','LABEL') 691 TRACE('ERROR10','LABEL') 692 TRACE('ERROR11','LABEL') 693 TRACE('ERROR12','LABEL') 694 695 TRACE('PROOF','VALUE') 696 TRACE('THS_NUM','VALUE') 697 TRACE('PF_LINE_NUM','VALUE') 698 TRACE('PART_NUM','VALUE') 699 TRACE('THESIS','VALUE') 700 TRACE('AX_NUM','VALUE') 701 TRACE('DEF_NUM','VALUE') 702 TRACE('BIGGEST_PART_NUM','VALUE') 703 TRACE('INT_LINE_NUM','VALUE') 704 TRACE('LINE_NUM','VALUE') 705 TRACE('ANT_NUM','VALUE') 706 TRACE('IMP_NUM','VALUE') 707 TRACE('REPLACEMENT_SPOT','VALUE') 708 TRACE('SPOT','VALUE') 709 TRACE('TEMP','VALUE') 710 TRACE('RHS','VALUE') 711 TRACE('LHS','VALUE') 712 TRACE('S','VALUE') 713 TRACE('N','VALUE') 714 TRACE('BACK_UP','VALUE') 715 TRACE('NUM_THM1','VALUE') 716 TRACE('NUM_THM2','VALUE') 717 TRACE('MATCH','VALUE') 718 TRACE('THM1','VALUE') 719 TRACE('THM2','VALUE') 720 TRACE('ANT1','VALUE') 721 TRACE('ANT2','VALUE') 722 TRACE('CONS1','VALUE') 723 TRACE('CONS2','VALUE') 724 TRACE('THM_NUM_RHS','VALUE') 725 TRACE('THM_NUM_LHS','VALUE') 726 TRACE('SUB_RHS','VALUE') 727 TRACE('SUB_LHS','VALUE') 728 TRACE('PROOF','VALUE') 729 TRACE('PROOF','VALUE') 730 TRACE('PROOF','VALUE') 731 INTREND TRACE('PROOF','VALUE') :(RETURN) 732 733 734 735 END