(NOTE-LIB "mc20-2" T) Loading ./yu/mc20-2.lib Finished loading ./yu/mc20-2.lib Loading ./yu/mc20-2.o Loading ./yu/0mc20-2.o Finished loading ./yu/0mc20-2.o Loading ./yu/1mc20-2.o Finished loading ./yu/1mc20-2.o Finished loading ./yu/mc20-2.o (#./yu/mc20-2.lib #./yu/mc20-2) (DEFN GT-CODE NIL '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) Observe that (LISTP (GT-CODE)) is a theorem. [ 0.0 0.0 0.0 ] GT-CODE (DEFN GT (A B) (IF (EQUAL A B) 0 (IF (ILESSP B A) 1 -1))) Observe that (OR (NUMBERP (GT A B)) (NEGATIVEP (GT A B))) is a theorem. [ 0.0 0.0 0.0 ] GT (DEFN GT-T (A B) (IF (EQUAL A B) 9 (IF (ILESSP B A) 11 10))) Observe that (NUMBERP (GT-T A B)) is a theorem. [ 0.0 0.0 0.0 ] GT-T (DEFN GT-STATEP (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (GT-CODE)) (RAM-ADDRP (SUB 32 4 (READ-SP S)) (MC-MEM S) 16) (EQUAL A (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-SP S) 8) (MC-MEM S) 4)))) Observe that (OR (FALSEP (GT-STATEP S A B)) (TRUEP (GT-STATEP S A B))) is a theorem. [ 0.0 0.0 0.0 ] GT-STATEP (DISABLE ILESSP) [ 0.0 0.0 0.0 ] ILESSP-OFF (PROVE-LEMMA GT-S-SN (REWRITE) (LET ((SN (STEPN S (GT-T A B)))) (IMPLIES (GT-STATEP S A B) (AND (EQUAL (MC-STATUS SN) 'RUNNING) (EQUAL (MC-PC SN) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE SN)) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE SN)) (ADD 32 (READ-SP S) 4)) (IMPLIES (D2-7A2-5P RN) (EQUAL (READ-RN OPLEN RN (MC-RFILE SN)) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT X K (SUB 32 4 (READ-SP S)) 4) (EQUAL (READ-MEM X (MC-MEM SN) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 SN) (GT A B)))))) WARNING: Note that the rewrite rule GT-S-SN will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma GT-S-SN is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and seven replacement rules. This conjecture can be simplified, using the abbreviations GT-CODE, GT-STATEP, IMPLIES, SP, L, READ-AN, and READ-SP, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4))) (AND (EQUAL (MC-STATUS (STEPN S (GT-T A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GT-T A B))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GT-T A B)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)) (IMPLIES (D2-7A2-5P RN) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT X K (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 4) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GT-T A B))) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (GT-T A B))) (GT A B)))). This simplifies, applying SUB-NEG, and expanding the definitions of PLUS, NEG, TIMES, IREAD-MEM, GT-T, READ-AN, RTS-ADDR, D2-7A2-5P, IMPLIES, READ-DN, IREAD-DN, GT, and AND, to 21 new goals: Case 21.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (MC-STATUS (STEPN S 11)) 'RUNNING)), which again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 20.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (MC-STATUS (STEPN S 10)) 'RUNNING)). However this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 19.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (MC-STATUS (STEPN S 9)) 'RUNNING)). But this again simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 18.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (MC-PC (STEPN S 11)) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). But this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 17.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (MC-PC (STEPN S 10)) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). This again simplifies, rewriting with the lemmas SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 16.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (MC-PC (STEPN S 9)) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))), which again simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 15.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 11))) (READ-RN 32 14 (MC-RFILE S)))). This again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 14.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 10))) (READ-RN 32 14 (MC-RFILE S)))). But this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 13.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 9))) (READ-RN 32 14 (MC-RFILE S)))). But this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and expanding EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 12.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 11))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))). But this again simplifies, rewriting with the lemmas SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 11.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 10))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))), which again simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 10.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 9))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))). However this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 9. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S)))). However this again simplifies, rewriting with the lemmas SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 8. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 10))) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 7. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 11))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 6. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 4) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) K) (READ-MEM X (MC-MEM S) K))). However this again simplifies, using linear arithmetic, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and expanding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 5. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 4) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 10)) K) (READ-MEM X (MC-MEM S) K))). This again simplifies, using linear arithmetic, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and opening up the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 4. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 4) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 11)) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, using linear arithmetic, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and expanding the functions EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, and RTS-INS, to: T. Case 3. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (EQUAL (NAT-TO-INT (READ-RN 32 0 (MC-RFILE (STEPN S 11))) 32) 1)). However this again simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, RTS-INS, and NAT-TO-INT, to: T. Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (NOT (ILESSP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)))) (EQUAL (NAT-TO-INT (READ-RN 32 0 (MC-RFILE (STEPN S 10))) 32) -1)). However this again simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-0, SET-CVZNX-Z, SUB-Z-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-N, MOVE-Z, MOVEQ-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, RTS-INS, and NAT-TO-INT, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))) (EQUAL (NAT-TO-INT (READ-RN 32 0 (MC-RFILE (STEPN S 9))) 32) 0)). But this again simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, WRITE-MEMP->READ-MEMP, WRITE-MEM-MAINTAIN-WRITE-MEMP, CAR-CONS, CDR-CONS, HEAD-LEMMA, READ-WRITE-RN, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BEQ-INT-1, SET-CVZNX-Z, SUB-Z-BITP, WRITE-WRITE-RN, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the definitions of EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, NEG, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, PLUS, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, MOVE-INS, MOVE-ADDR-MODEP, OP-SZ, EFFEC-ADDR, NUMBERP, ADDR-DISP, S_MODE, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, READ-DN, TIMES, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, B-NOT, BRANCH-CC, COND-FIELD, BCC-GROUP, CLR-SUBGROUP, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, RTS-INS, and NAT-TO-INT, to: T. Q.E.D. [ 0.0 4.5 0.4 ] GT-S-SN (DISABLE GT-T) [ 0.0 0.0 0.0 ] GT-T-OFF (DISABLE GT) [ 0.0 0.0 0.0 ] GT-OFF (CONSTRAIN P-DISJOINTNESS (REWRITE) (IMPLIES (AND (P-DISJOINT X N S) (LEQ (PLUS J (INDEX-N Y X)) N)) (P-DISJOINT Y J S)) ((P-DISJOINT (LAMBDA (X N S) F)))) WARNING: Note that P-DISJOINTNESS contains the free variables N and X which will be chosen by instantiating the hypothesis (P-DISJOINT X N S). We will verify the consistency and the conservative nature of this constraint by attempting to prove: (IMPLIES (AND F (IF (LESSP N (PLUS J (INDEX-N Y X))) F T)) F). This conjecture simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] P-DISJOINTNESS (CONSTRAIN FN*-CORRECTNESS (REWRITE) (IMPLIES (FN*-STATEP S A B) (LET ((SN (STEPN S (FN*-T A B)))) (AND (EQUAL (MC-STATUS SN) 'RUNNING) (EQUAL (MC-PC SN) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE SN)) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE SN)) (ADD 32 (READ-SP S) 4)) (IMPLIES (AND (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE SN)) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (P-DISJOINT X K S) (EQUAL (READ-MEM X (MC-MEM SN) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 SN) (FN* A B))))) ((FN*-STATEP (LAMBDA (S A B) F)) (FN*-T (LAMBDA (A B) 0)) (FN* (LAMBDA (A B) 0)))) WARNING: Note that the rewrite rule FN*-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma FN*-CORRECTNESS is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and seven replacement rules. We will verify the consistency and the conservative nature of this constraint by attempting to prove: (IMPLIES F (AND (EQUAL (MC-STATUS (STEPN S 0)) 'RUNNING) (EQUAL (MC-PC (STEPN S 0)) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 0))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 0))) (ADD 32 (READ-SP S) 4)) (IMPLIES (AND (IF (LESSP 32 OPLEN) F T) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 0))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (P-DISJOINT X K S) (EQUAL (READ-MEM X (MC-MEM (STEPN S 0)) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S 0)) 0))). This formula can be simplified, using the abbreviations IMPLIES, SP, L, READ-AN, READ-SP, and STEPN-REWRITER0, to: T, which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] FN*-CORRECTNESS (DEFN MAX-CODE NIL '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) Note that (LISTP (MAX-CODE)) is a theorem. [ 0.0 0.0 0.0 ] MAX-CODE (DEFN MAX-FN* (A B) (IF (NEGATIVEP (FN* A B)) B A)) Observe that (OR (EQUAL (MAX-FN* A B) A) (EQUAL (MAX-FN* A B) B)) is a theorem. [ 0.0 0.0 0.0 ] MAX-FN* (DEFN MAX-T0 (A B) 8) WARNING: A and B are in the arglist but not in the body of the definition of MAX-T0. Note that (NUMBERP (MAX-T0 A B)) is a theorem. [ 0.0 0.0 0.0 ] MAX-T0 (DEFN MAX-T (A B) (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) (IF (NEGATIVEP (FN* A B)) 7 6)))) From the definition we can conclude that (NUMBERP (MAX-T A B)) is a theorem. [ 0.0 0.0 0.0 ] MAX-T (DEFN MAX-SP (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (MAX-CODE)) (EQUAL A (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-SP S) 8) (MC-MEM S) 4)) (RAM-ADDRP (SUB 32 24 (READ-SP S)) (MC-MEM S) 40))) Observe that (OR (FALSEP (MAX-SP S A B)) (TRUEP (MAX-SP S A B))) is a theorem. [ 0.0 0.0 0.0 ] MAX-SP (CONSTRAIN MAX-STATE (REWRITE) (AND (IMPLIES (MAX-STATEP S A B) (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (IMPLIES (MAX-STATEP S A B) (P-DISJOINT (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40 (STEPN S (MAX-T0 A B)))) (EQUAL (MAX-STATEP S A B) (AND (MAX-SP S A B) (COMP-LOADP S A B)))) ((MAX-STATEP (LAMBDA (S A B) F)) (COMP-LOADP (LAMBDA (S A B) F)))) WARNING: Note that the proposed lemma MAX-STATE is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and three replacement rules. We will verify the consistency and the conservative nature of this constraint by attempting to prove: (AND (IMPLIES F (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (IMPLIES F (P-DISJOINT (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40 (STEPN S (MAX-T0 A B)))) (EQUAL F (AND (MAX-SP S A B) F))). This conjecture can be simplified, using the abbreviations IMPLIES, AND, and MAX-T0, to three new formulas: Case 3. T, which simplifies, obviously, to: T. Case 2. T. This simplifies, trivially, to: T. Case 1. (EQUAL F (AND (MAX-SP S A B) F)). This simplifies, applying SUB-NEG, and unfolding the definitions of NEG, IREAD-MEM, TIMES, READ-SP, L, SP, PLUS, READ-AN, MAX-CODE, MAX-SP, AND, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-STATE (DEFN MAX-S0P (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-AN 32 6 S) 16) (MC-MEM S) 4)) (EVENP (RTS-ADDR S)) (ROM-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) (MAX-CODE)) (RAM-ADDRP (READ-SP S) (MC-MEM S) 40) (EQUAL* (READ-SP S) (SUB 32 20 (READ-AN 32 6 S))) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-SP S) 8) (MC-MEM S) 4) B))) Observe that (OR (FALSEP (MAX-S0P S A B)) (TRUEP (MAX-S0P S A B))) is a theorem. [ 0.0 0.0 0.0 ] MAX-S0P (DEFN MAX-S1P (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) (MAX-CODE)) (RAM-ADDRP (SUB 32 20 (READ-AN 32 6 S)) (MC-MEM S) 40) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-DN 32 0 S) (FN* A B)))) From the definition we can conclude that: (OR (FALSEP (MAX-S1P S A B)) (TRUEP (MAX-S1P S A B))) is a theorem. [ 0.0 0.0 0.0 ] MAX-S1P (CONSTRAIN MAX-DISJOINTNESS (REWRITE) (IMPLIES (AND (MAX-STATEP S A B) (MAX-DISJOINT X K S)) (P-DISJOINT X K (STEPN S (MAX-T0 A B)))) ((MAX-DISJOINT (LAMBDA (X K S) F)))) We will verify the consistency and the conservative nature of this constraint by attempting to prove: (IMPLIES (AND (MAX-STATEP S A B) F) (P-DISJOINT X K (STEPN S (MAX-T0 A B)))). This conjecture can be simplified, using the abbreviations SP, L, READ-AN, READ-SP, MAX-CODE, MAX-SP, MAX-STATE, AND, IMPLIES, and MAX-T0, to: T. This simplifies, trivially, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-DISJOINTNESS (PROVE-LEMMA MAX-S-S0 NIL (IMPLIES (MAX-SP S A B) (MAX-S0P (STEPN S (MAX-T0 A B)) A B))) This formula can be simplified, using the abbreviations SP, L, READ-AN, READ-SP, MAX-CODE, MAX-SP, IMPLIES, and MAX-T0, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (RAM-ADDRP (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 40)) (MAX-S0P (STEPN S 8) A B)), which simplifies, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, WRITEM-MEM-MAINTAIN-WRITE-MEMP, BITP-FIX-BIT, FIX-BIT-BITP, EXT-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, EQUAL*-REFLEX, WRITEM-MEM-MAINTAIN-RAM-ADDRP, WRITE-MEM-MAINTAIN-RAM-ADDRP, RAM-ADDRP-3, WRITEM-MEM-MCODE-ADDRP, WRITE-MEM-MCODE-ADDRP, WRITEM-MEM-MAINTAIN-ROM-ADDRP, WRITE-MEM-MAINTAIN-ROM-ADDRP, ROM-ADDRP-LA2, INDEX-N-X-X, ADD-0, MC-PC-RANGEP, and READ-WRITE-MEM2, and opening up PLUS, NEG, EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, TIMES, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, READ-DN, M-MAPPING, ADDR-PREDEC, MOVEA-INS, MOVEA-ADDR-MODEP, JSR-INS, JSR-ADDR-MODEP, ADDR-INDIRECT, PUSH-SP, JMP-MAPPING, IREAD-MEM, IREAD-DN, MAX-CODE, RTS-ADDR, UINT-RANGEP, and MAX-S0P, to: T. Q.E.D. [ 0.0 0.9 0.0 ] MAX-S-S0 (PROVE-LEMMA MAX-S-S0-ELSE (REWRITE) (LET ((S0 (STEPN S (MAX-T0 A B)))) (IMPLIES (MAX-SP S A B) (AND (EQUAL (LINKED-RTS-ADDR S0) (RTS-ADDR S)) (EQUAL (LINKED-A6 S0) (READ-AN 32 6 S)) (EQUAL (READ-RN 32 14 (MC-RFILE S0)) (SUB 32 4 (READ-SP S))) (EQUAL (MOVEM-SAVED S0 4 8 2) (READM-RN 32 '(2 3) (MC-RFILE S))))))) WARNING: Note that the rewrite rule MAX-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that the rewrite rule MAX-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that the rewrite rule MAX-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol MOVEM-SAVED. WARNING: Note that the proposed lemma MAX-S-S0-ELSE is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and four replacement rules. This formula can be simplified, using the abbreviations MAX-CODE, MAX-SP, IMPLIES, SP, L, READ-SP, READ-AN, and MAX-T0, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (RAM-ADDRP (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 40)) (AND (EQUAL (LINKED-RTS-ADDR (STEPN S 8)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 8)) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)))) (EQUAL (MOVEM-SAVED (STEPN S 8) 4 8 2) (READM-RN 32 '(2 3) (MC-RFILE S))))), which simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, WRITEM-MEM-MAINTAIN-WRITE-MEMP, BITP-FIX-BIT, FIX-BIT-BITP, EXT-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, DISJOINT-DEDUCTION1, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, READM-WRITE-MEM, READM-WRITEM-MEM, and MODN-READM-RN, and expanding the definitions of PLUS, NEG, EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, TIMES, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, READ-DN, M-MAPPING, ADDR-PREDEC, MOVEA-INS, MOVEA-ADDR-MODEP, JSR-INS, JSR-ADDR-MODEP, ADDR-INDIRECT, PUSH-SP, JMP-MAPPING, LINKED-RTS-ADDR, RTS-ADDR, UINT-RANGEP, LINKED-A6, MOVEM-SAVED, and AND, to: T. Q.E.D. [ 0.0 2.5 0.0 ] MAX-S-S0-ELSE (PROVE-LEMMA MAX-S-S0-RFILE (REWRITE) (IMPLIES (AND (MAX-SP S A B) (D4-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (MAX-T0 A B)))) (READ-RN OPLEN RN (MC-RFILE S))))) This formula can be simplified, using the abbreviations D2-7A2-5P, D4-7A2-5P, SP, L, READ-AN, READ-SP, MAX-CODE, MAX-SP, AND, IMPLIES, and MAX-T0, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (RAM-ADDRP (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 40) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 8))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, applying SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, WRITEM-MEM-MAINTAIN-WRITE-MEMP, BITP-FIX-BIT, FIX-BIT-BITP, EXT-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the definitions of PLUS, NEG, EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, TIMES, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, READ-DN, M-MAPPING, ADDR-PREDEC, MOVEA-INS, MOVEA-ADDR-MODEP, JSR-INS, JSR-ADDR-MODEP, ADDR-INDIRECT, PUSH-SP, and JMP-MAPPING, to: T. Q.E.D. [ 0.0 0.5 0.0 ] MAX-S-S0-RFILE (PROVE-LEMMA MAX-S-S0-MEM (REWRITE) (IMPLIES (AND (MAX-SP S A B) (DISJOINT X K (SUB 32 24 (READ-SP S)) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (MAX-T0 A B))) K) (READ-MEM X (MC-MEM S) K)))) This conjecture can be simplified, using the abbreviations MAX-CODE, MAX-SP, AND, IMPLIES, MAX-T0, SP, L, READ-AN, and READ-SP, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (RAM-ADDRP (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 40) (DISJOINT X K (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 8)) K) (READ-MEM X (MC-MEM S) K))). This simplifies, using linear arithmetic, rewriting with SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, READ-MEM-NAT-RANGEP, WRITEM-MEM-MAINTAIN-WRITE-MEMP, BITP-FIX-BIT, FIX-BIT-BITP, EXT-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and unfolding PLUS, NEG, EXECUTE-INS, OPCODE-FIELD, EQUAL, UNLK-SUBGROUP, S_RN, LINK-MAPPING, LSZ, READ-AN, SP, READ-SP, INDEX-N, UPDATE-RFILE, WRITE-AN, WRITE-SP, UPDATE-MEM, ADD, EXT, W, LINK_W-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, STEPI, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, TIMES, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, READ-DN, M-MAPPING, ADDR-PREDEC, MOVEA-INS, MOVEA-ADDR-MODEP, JSR-INS, JSR-ADDR-MODEP, ADDR-INDIRECT, PUSH-SP, and JMP-MAPPING, to: T. Q.E.D. [ 0.0 0.7 0.0 ] MAX-S-S0-MEM (PROVE-LEMMA MAX-S0-S1 NIL (IMPLIES (AND (MAX-S0P S A B) (FN*-STATEP S A B)) (MAX-S1P (STEPN S (FN*-T A B)) A B))) This conjecture can be simplified, using the abbreviations SP, L, READ-SP, MAX-CODE, READ-AN, MAX-S0P, AND, and IMPLIES, to the goal: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (RTS-ADDR S)) (ROM-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)))) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4) B) (FN*-STATEP S A B)) (MAX-S1P (STEPN S (FN*-T A B)) A B)). This simplifies, rewriting with SUB-NEG, READ-RN-EQUAL*, ADD-ASSOCIATIVITY, STEPN-RAM-ADDRP, RAM-ADDRP-LA2, STEPN-MCODE-ADDRP, STEPN-ROM-ADDRP, ROM-ADDRP-LA2, CORRECTNESS-OF-CANCEL-LESSP-PLUS, INDEX-N-DEDUCTION2, and FN*-CORRECTNESS, and unfolding PLUS, READ-AN, RTS-ADDR, NEG, ADD, TIMES, IREAD-MEM, READ-DN, IREAD-DN, LESSP, D2-7A2-5P, LEN, MAX-CODE, INDEX-N, FIX, ZEROP, NOT, EQUAL, and MAX-S1P, to two new conjectures: Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4)) (ROM-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4) 4294967270) (MC-MEM S) 46) (MCODE-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4) 4294967270) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 15 (MC-RFILE S)) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967276)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967280) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 3 (MC-RFILE S)) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967284) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32)) (FN*-STATEP S (NAT-TO-INT (READ-RN 32 3 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32))) (EVENP (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967276) (MC-MEM S) 4))), which again simplifies, applying READ-RN-EQUAL*, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4)) (ROM-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4) 4294967270) (MC-MEM S) 46) (MCODE-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4) 4294967270) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 15 (MC-RFILE S)) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967276)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967280) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 3 (MC-RFILE S)) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967284) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32)) (FN*-STATEP S (NAT-TO-INT (READ-RN 32 3 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32))) (MCODE-ADDRP (ADD 32 (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967276) (MC-MEM S) 4) 4294967270) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117))). This again simplifies, applying READ-RN-EQUAL*, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-S0-S1 (PROVE-LEMMA MAX-S0-S1-ELSE (REWRITE) (IMPLIES (AND (MAX-S0P S A B) (FN*-STATEP S A B) (P-DISJOINT (SUB 32 20 (READ-AN 32 6 S)) 40 S)) (AND (EQUAL (LINKED-RTS-ADDR (STEPN S (FN*-T A B))) (LINKED-RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (FN*-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S (FN*-T A B))) (LINKED-A6 S)) (EQUAL (MOVEM-SAVED (STEPN S (FN*-T A B)) 4 8 2) (MOVEM-SAVED S 4 8 2))))) WARNING: Note that the rewrite rule MAX-S0-S1-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: the previously added lemma, FN*-CORRECTNESS, could be applied whenever the newly proposed MAX-S0-S1-ELSE could! WARNING: Note that the rewrite rule MAX-S0-S1-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that the rewrite rule MAX-S0-S1-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol MOVEM-SAVED. WARNING: Note that the proposed lemma MAX-S0-S1-ELSE is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and four replacement rules. This conjecture can be simplified, using the abbreviations SP, L, READ-SP, MAX-CODE, MAX-S0P, AND, IMPLIES, and READ-AN, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (RTS-ADDR S)) (ROM-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)))) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4) B) (FN*-STATEP S A B) (P-DISJOINT (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) 40 S)) (AND (EQUAL (LINKED-RTS-ADDR (STEPN S (FN*-T A B))) (LINKED-RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (FN*-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S (FN*-T A B))) (LINKED-A6 S)) (EQUAL (MOVEM-SAVED (STEPN S (FN*-T A B)) 4 8 2) (MOVEM-SAVED S 4 8 2)))). This simplifies, applying SUB-NEG, READ-RN-EQUAL*, ADD-ASSOCIATIVITY, INDEX-N-DEDUCTION2, P-DISJOINTNESS, FN*-CORRECTNESS, INDEX-N-DEDUCTION1, and STEPN-READM-MEM, and unfolding the functions PLUS, READ-AN, RTS-ADDR, NEG, ADD, TIMES, IREAD-MEM, READ-DN, IREAD-DN, LESSP, INDEX-N, LINKED-RTS-ADDR, LINKED-A6, MOVEM-SAVED, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-S0-S1-ELSE (PROVE-LEMMA MAX-S0-S1-RFILE (REWRITE) (IMPLIES (AND (MAX-S0P S A B) (FN*-STATEP S A B) (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (FN*-T A B)))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: the previously added lemma, FN*-CORRECTNESS, could be applied whenever the newly proposed MAX-S0-S1-RFILE could! This conjecture can be simplified, using the abbreviations D2-7A2-5P, SP, L, READ-SP, MAX-CODE, READ-AN, MAX-S0P, AND, and IMPLIES, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (RTS-ADDR S)) (ROM-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)))) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4) B) (FN*-STATEP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (FN*-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, rewriting with the lemmas SUB-NEG, READ-RN-EQUAL*, ADD-ASSOCIATIVITY, and FN*-CORRECTNESS, and unfolding the definitions of PLUS, READ-AN, RTS-ADDR, NEG, ADD, TIMES, IREAD-MEM, READ-DN, IREAD-DN, and D2-7A2-5P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-S0-S1-RFILE (PROVE-LEMMA MAX-S0-S1-MEM (REWRITE) (IMPLIES (AND (MAX-S0P S A B) (FN*-STATEP S A B) (P-DISJOINT X K S)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (FN*-T A B))) K) (READ-MEM X (MC-MEM S) K)))) WARNING: the previously added lemma, FN*-CORRECTNESS, could be applied whenever the newly proposed MAX-S0-S1-MEM could! This conjecture can be simplified, using the abbreviations SP, L, READ-SP, MAX-CODE, READ-AN, MAX-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EQUAL (MC-PC S) (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 16) (MC-MEM S) 4)) (EVENP (RTS-ADDR S)) (ROM-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (RTS-ADDR S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (MC-MEM S) 40) (EQUAL* (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)))) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4) B) (FN*-STATEP S A B) (P-DISJOINT X K S)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (FN*-T A B))) K) (READ-MEM X (MC-MEM S) K))). This simplifies, rewriting with SUB-NEG, READ-RN-EQUAL*, ADD-ASSOCIATIVITY, and FN*-CORRECTNESS, and expanding the functions PLUS, READ-AN, RTS-ADDR, NEG, ADD, TIMES, IREAD-MEM, READ-DN, and IREAD-DN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MAX-S0-S1-MEM (PROVE-LEMMA MAX-S1-SN-1 (REWRITE) (IMPLIES (AND (MAX-S1P S A B) (NEGATIVEP (FN* A B))) (AND (EQUAL (MC-STATUS (STEPN S 7)) 'RUNNING) (EQUAL (MC-PC (STEPN S 7)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 7)) B) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 7))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 7))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K))))) WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that the rewrite rule MAX-S1-SN-1 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that the proposed lemma MAX-S1-SN-1 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This conjecture can be simplified, using the abbreviations MAX-CODE, MAX-S1P, AND, IMPLIES, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 40) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-DN 32 0 S) (FN* A B)) (NEGATIVEP (FN* A B))) (AND (EQUAL (MC-STATUS (STEPN S 7)) 'RUNNING) (EQUAL (MC-PC (STEPN S 7)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 7)) B) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 7))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 7))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K)))). This simplifies, appealing to the lemmas SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BGE-V0, MOVE-BMI, READ-RN-NAT-RANGEP, SET-CVZNX-N, BITP-FIX-BIT, MOVE-N-BITP, SET-CVZNX-V, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, READ-MEM-NAT-RANGEP, and HEAD-READ-RN, and expanding NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT, FIX-BIT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LINKED-RTS-ADDR, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] MAX-S1-SN-1 (PROVE-LEMMA MAX-S1-SN-RFILE-1 (REWRITE) (IMPLIES (AND (MAX-S1P S A B) (NEGATIVEP (FN* A B)) (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2)))))) WARNING: Note that MAX-S1-SN-RFILE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). This formula can be simplified, using the abbreviations D2-7A2-5P, READ-AN, MAX-CODE, MAX-S1P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 40) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-DN 32 0 S) (FN* A B)) (NEGATIVEP (FN* A B)) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))), which simplifies, applying the lemmas SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BGE-V0, MOVE-BMI, READ-RN-NAT-RANGEP, SET-CVZNX-N, BITP-FIX-BIT, MOVE-N-BITP, SET-CVZNX-V, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the definitions of NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT, FIX-BIT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P, D4-7A2-5P, and MOVEM-SAVED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] MAX-S1-SN-RFILE-1 (PROVE-LEMMA MAX-S1-SN-2 (REWRITE) (IMPLIES (AND (MAX-S1P S A B) (NOT (NEGATIVEP (FN* A B)))) (AND (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) A) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K))))) WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that the rewrite rule MAX-S1-SN-2 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that MAX-S1-SN-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). WARNING: Note that the proposed lemma MAX-S1-SN-2 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This conjecture can be simplified, using the abbreviations NOT, MAX-CODE, MAX-S1P, AND, IMPLIES, and READ-AN, to the conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 40) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-DN 32 0 S) (FN* A B)) (NOT (NEGATIVEP (FN* A B)))) (AND (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) A) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K)))). This simplifies, appealing to the lemmas SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BGE-V0, MOVE-BMI, READ-RN-NAT-RANGEP, SET-CVZNX-N, BITP-FIX-BIT, MOVE-N-BITP, SET-CVZNX-V, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, READ-MEM-NAT-RANGEP, and HEAD-READ-RN, and unfolding the functions NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT, FIX-BIT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LINKED-RTS-ADDR, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] MAX-S1-SN-2 (PROVE-LEMMA MAX-S1-SN-RFILE-2 (REWRITE) (IMPLIES (AND (MAX-S1P S A B) (NOT (NEGATIVEP (FN* A B))) (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2)))))) WARNING: Note that MAX-S1-SN-RFILE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (MAX-S1P S A B). This formula can be simplified, using the abbreviations D2-7A2-5P, NOT, READ-AN, MAX-CODE, MAX-S1P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) 46) (MCODE-ADDRP (SUB 32 26 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 20 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 40) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (EQUAL (IREAD-DN 32 0 S) (FN* A B)) (NOT (NEGATIVEP (FN* A B))) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))), which simplifies, applying the lemmas SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, BGE-V0, MOVE-BMI, READ-RN-NAT-RANGEP, SET-CVZNX-N, BITP-FIX-BIT, MOVE-N-BITP, SET-CVZNX-V, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and opening up NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, B-NOT, FIX-BIT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P, D4-7A2-5P, and MOVEM-SAVED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] MAX-S1-SN-RFILE-2 (DISABLE MAX-T0) [ 0.0 0.0 0.0 ] MAX-T0-OFF (PROVE-LEMMA MAX-CORRECTNESS (REWRITE) (LET ((SN (STEPN S (MAX-T A B)))) (IMPLIES (MAX-STATEP S A B) (AND (EQUAL (MC-STATUS SN) 'RUNNING) (EQUAL (MC-PC SN) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE SN)) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE SN)) (ADD 32 (READ-SP S) 4)) (IMPLIES (AND (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE SN)) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (AND (DISJOINT X K (SUB 32 24 (READ-SP S)) 40) (MAX-DISJOINT X K S)) (EQUAL (READ-MEM X (MC-MEM SN) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 SN) (MAX-FN* A B))))) ((USE (MAX-S-S0) (MAX-S0-S1 (S (STEPN S (MAX-T0 A B))))) (DISABLE MAX-SP MAX-S0P MAX-S1P IREAD-DN LINKED-RTS-ADDR STEPN-REWRITER))) WARNING: Note that the rewrite rule MAX-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma MAX-CORRECTNESS is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and seven replacement rules. This formula can be simplified, using the abbreviations MAX-STATE, IMPLIES, AND, SP, L, READ-AN, and READ-SP, to the new goal: (IMPLIES (AND (IMPLIES (MAX-SP S A B) (MAX-S0P (STEPN S (MAX-T0 A B)) A B)) (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B)) (AND (EQUAL (MC-STATUS (STEPN S (MAX-T A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (MAX-T A B))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T A B)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)) (IMPLIES (AND (IF (LESSP 32 OPLEN) F T) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (MAX-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (AND (DISJOINT X K (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 40) (MAX-DISJOINT X K S)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (MAX-T A B))) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (MAX-T A B))) (MAX-FN* A B)))), which simplifies, applying SUB-NEG, and unfolding the functions IMPLIES, AND, MAX-T, READ-AN, PLUS, RTS-ADDR, D2-7A2-5P, NEG, and MAX-FN*, to the following 28 new goals: Case 28.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (MC-STATUS (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) 'RUNNING)). This again simplifies, rewriting with the lemma MAX-STATE, to: T. Case 27.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (MC-STATUS (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) 'RUNNING)), which again simplifies, rewriting with MAX-STATE, to: T. Case 26.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (MC-PC (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). However this again simplifies, appealing to the lemma MAX-STATE, to: T. Case 25.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (MC-PC (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))), which again simplifies, applying MAX-STATE, to: T. Case 24.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (READ-RN 32 14 (MC-RFILE S)))). However this again simplifies, applying the lemma MAX-STATE, to: T. Case 23.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (READ-RN 32 14 (MC-RFILE S)))), which again simplifies, applying the lemma MAX-STATE, to: T. Case 22.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))), which again simplifies, rewriting with the lemma MAX-STATE, to: T. Case 21.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))), which again simplifies, rewriting with MAX-STATE, to: T. Case 20.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, rewriting with the lemma MAX-STATE, to: T. Case 19.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, rewriting with MAX-STATE, to: T. Case 18.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40) (MAX-DISJOINT X K S) (NEGATIVEP (FN* A B))) (EQUAL (READ-MEM X (MC-MEM (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, applying the lemma MAX-STATE, to: T. Case 17.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40) (MAX-DISJOINT X K S) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-MEM X (MC-MEM (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) K) (READ-MEM X (MC-MEM S) K))), which again simplifies, applying MAX-STATE, to: T. Case 16.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (IREAD-DN 32 0 (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) A)). This again simplifies, applying MAX-STATE, to: T. Case 15.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (NOT (FN*-STATEP (STEPN S (MAX-T0 A B)) A B)) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (IREAD-DN 32 0 (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) B)). This again simplifies, applying MAX-STATE, to: T. Case 14.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (MC-STATUS (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) 'RUNNING)). But this again simplifies, applying STEPN-LEMMA and MAX-S1-SN-2, and unfolding EQUAL, to: T. Case 13.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (MC-STATUS (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) 'RUNNING)). This again simplifies, applying STEPN-LEMMA and MAX-S1-SN-1, and unfolding EQUAL, to: T. Case 12.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (MC-PC (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). This again simplifies, rewriting with STEPN-LEMMA, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-STATE, MAX-S0-S1-ELSE, and MAX-S1-SN-2, and expanding the definitions of ADD, READ-AN, PLUS, SP, L, READ-SP, NEG, and RTS-ADDR, to: T. Case 11.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (MC-PC (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). But this again simplifies, appealing to the lemmas STEPN-LEMMA, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-STATE, MAX-S0-S1-ELSE, and MAX-S1-SN-1, and unfolding the definitions of ADD, READ-AN, PLUS, SP, L, READ-SP, NEG, and RTS-ADDR, to: T. Case 10.(IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (READ-RN 32 14 (MC-RFILE S)))), which again simplifies, applying STEPN-LEMMA, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-STATE, MAX-S0-S1-ELSE, and MAX-S1-SN-2, and unfolding the functions ADD, READ-AN, PLUS, SP, L, READ-SP, and NEG, to: T. Case 9. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (READ-RN 32 14 (MC-RFILE S)))). But this again simplifies, rewriting with STEPN-LEMMA, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-STATE, MAX-S0-S1-ELSE, and MAX-S1-SN-1, and opening up the functions ADD, READ-AN, PLUS, SP, L, READ-SP, and NEG, to: T. Case 8. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))). This again simplifies, appealing to the lemmas STEPN-LEMMA, FN*-CORRECTNESS, MAX-S-S0-ELSE, SUB-NEG, MAX-STATE, ADD-ASSOCIATIVITY, and MAX-S1-SN-2, and expanding the definitions of NEG, READ-SP, L, SP, PLUS, READ-AN, and ADD, to: T. Case 7. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))), which again simplifies, rewriting with STEPN-LEMMA, FN*-CORRECTNESS, MAX-S-S0-ELSE, SUB-NEG, MAX-STATE, ADD-ASSOCIATIVITY, and MAX-S1-SN-1, and expanding the definitions of NEG, READ-SP, L, SP, PLUS, READ-AN, and ADD, to: T. Case 6. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NEGATIVEP (FN* A B))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7))))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, applying the lemmas STEPN-LEMMA, MAX-STATE, MAX-S0-S1-RFILE, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-S0-S1-ELSE, GET-VLST-READM-RN, and MAX-S1-SN-RFILE-1, and expanding the definitions of D2-7A2-5P, D4-7A2-5P, ADD, READ-AN, PLUS, SP, L, READ-SP, NEG, CDR, NUMBERP, CAR, LISTP, and N-MEMBER, to: (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NEGATIVEP (FN* A B)) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (MAX-T0 A B)))) (READ-RN OPLEN RN (MC-RFILE S)))). But this again simplifies, rewriting with MAX-S-S0-RFILE, and expanding the definitions of D4-7A2-5P and D2-7A2-5P, to: T. Case 5. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6))))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, applying STEPN-LEMMA, MAX-STATE, MAX-S0-S1-RFILE, ADD-ASSOCIATIVITY, SUB-NEG, MAX-S-S0-ELSE, MAX-S0-S1-ELSE, GET-VLST-READM-RN, and MAX-S1-SN-RFILE-2, and expanding D2-7A2-5P, D4-7A2-5P, ADD, READ-AN, PLUS, SP, L, READ-SP, NEG, CDR, NUMBERP, CAR, LISTP, and N-MEMBER, to: (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (NEGATIVEP (FN* A B))) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (MAX-T0 A B)))) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, rewriting with MAX-S-S0-RFILE, and unfolding the definitions of D4-7A2-5P and D2-7A2-5P, to: T. Case 4. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40) (MAX-DISJOINT X K S) (NEGATIVEP (FN* A B))) (EQUAL (READ-MEM X (MC-MEM (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) K) (READ-MEM X (MC-MEM S) K))). This again simplifies, using linear arithmetic, rewriting with STEPN-LEMMA, MAX-DISJOINTNESS, MAX-STATE, DISJOINT-10, SUB-NEG, MAX-S-S0-MEM, MAX-S0-S1-MEM, and MAX-S1-SN-1, and expanding the definitions of INDEX-N, LESSP, NEG, READ-SP, L, SP, PLUS, and READ-AN, to: T. Case 3. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40) (MAX-DISJOINT X K S) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (READ-MEM X (MC-MEM (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) K) (READ-MEM X (MC-MEM S) K))). However this again simplifies, using linear arithmetic, rewriting with the lemmas STEPN-LEMMA, MAX-DISJOINTNESS, MAX-STATE, DISJOINT-10, SUB-NEG, MAX-S-S0-MEM, MAX-S0-S1-MEM, and MAX-S1-SN-2, and unfolding INDEX-N, LESSP, NEG, READ-SP, L, SP, PLUS, and READ-AN, to: T. Case 2. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NOT (NEGATIVEP (FN* A B)))) (EQUAL (IREAD-DN 32 0 (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 6)))) A)), which again simplifies, rewriting with STEPN-LEMMA and MAX-S1-SN-2, to: T. Case 1. (IMPLIES (AND (MAX-S0P (STEPN S (MAX-T0 A B)) A B) (MAX-S1P (STEPN (STEPN S (MAX-T0 A B)) (FN*-T A B)) A B) (MAX-SP S A B) (COMP-LOADP S A B) (NEGATIVEP (FN* A B))) (EQUAL (IREAD-DN 32 0 (STEPN S (SPLUS (MAX-T0 A B) (SPLUS (FN*-T A B) 7)))) B)). But this again simplifies, applying the lemmas STEPN-LEMMA and MAX-S1-SN-1, to: T. Q.E.D. [ 0.0 0.1 0.1 ] MAX-CORRECTNESS (PROVE-LEMMA DISJOINT-LA4 (REWRITE) (IMPLIES (AND (DISJOINT A M B N) (LEQ (PLUS J (INDEX-N A1 A)) M) (LEQ (PLUS L (INDEX-N B1 B)) N)) (DISJOINT A1 J B1 L)) ((USE (DISJOINT-LA3 (I (INDEX-N A1 A)) (K (INDEX-N B1 B)))) (ENABLE INDEX-N))) WARNING: Note that DISJOINT-LA4 contains the free variables N, B, M, and A which will be chosen by instantiating the hypothesis (DISJOINT A M B N). This conjecture can be simplified, using the abbreviations AND, IMPLIES, and INDEX-N, to: (IMPLIES (AND (IMPLIES (AND (DISJOINT A M B N) (IF (LESSP M (PLUS (SUB 32 A A1) J)) F T) (IF (LESSP N (PLUS (SUB 32 B B1) L)) F T)) (DISJOINT (ADD 32 A (SUB 32 A A1)) J (ADD 32 B (SUB 32 B B1)) L)) (DISJOINT A M B N) (NOT (LESSP M (PLUS J (SUB 32 A A1)))) (NOT (LESSP N (PLUS L (SUB 32 B B1))))) (DISJOINT A1 J B1 L)). This simplifies, using linear arithmetic, applying DISJOINT-0, SUB-NEG, PLUS-COMMUTATIVITY, CORRECTNESS-OF-CANCEL-ADD-NEG, and DISJOINT-HEAD, and expanding the definitions of AND and IMPLIES, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DISJOINT-LA4 (DEFN MAX-GT-STATEP (S A B) (LET ((COMP (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4))) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (MAX-CODE)) (EQUAL A (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-SP S) 8) (MC-MEM S) 4)) (EVENP COMP) (ROM-ADDRP COMP (MC-MEM S) (LEN (GT-CODE))) (MCODE-ADDRP COMP (MC-MEM S) (GT-CODE)) (RAM-ADDRP (SUB 32 28 (READ-SP S)) (MC-MEM S) 44)))) Observe that: (OR (FALSEP (MAX-GT-STATEP S A B)) (TRUEP (MAX-GT-STATEP S A B))) is a theorem. [ 0.0 0.0 0.0 ] MAX-GT-STATEP (DEFN MAX-GT-T (A B) (SPLUS (MAX-T0 A B) (SPLUS (GT-T A B) (IF (NEGATIVEP (GT A B)) 7 6)))) From the definition we can conclude that (NUMBERP (MAX-GT-T A B)) is a theorem. [ 0.0 0.0 0.0 ] MAX-GT-T (DEFN MAX-GT (A B) (IF (NEGATIVEP (GT A B)) B A)) Observe that (OR (EQUAL (MAX-GT A B) A) (EQUAL (MAX-GT A B) B)) is a theorem. [ 0.0 0.0 0.0 ] MAX-GT (PROVE-LEMMA MAX-GT-STATEP-S0 (REWRITE) (LET ((S0 (STEPN S (MAX-T0 A B)))) (IMPLIES (MAX-GT-STATEP S A B) (AND (EQUAL (MC-STATUS S0) 'RUNNING) (EQUAL (MC-PC S0) (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4)) (EQUAL (READ-RN 32 15 (MC-RFILE S0)) (SUB 32 24 (READ-SP S))) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S0)) 4) (MC-MEM S0) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S0)) 8) (MC-MEM S0) 4) B)))) ((USE (MAX-S-S0)))) WARNING: Note that the rewrite rule MAX-GT-STATEP-S0 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-MEM. WARNING: Note that the rewrite rule MAX-GT-STATEP-S0 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-MEM. WARNING: Note that the proposed lemma MAX-GT-STATEP-S0 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and five replacement rules. This formula can be simplified, using the abbreviations GT-CODE, MAX-CODE, MAX-GT-STATEP, IMPLIES, SP, L, READ-AN, and READ-SP, to: (IMPLIES (AND (IMPLIES (MAX-SP S A B) (MAX-S0P (STEPN S (MAX-T0 A B)) A B)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) (LEN '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 44)) (AND (EQUAL (MC-STATUS (STEPN S (MAX-T0 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (MAX-T0 A B))) (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 A B)))) (SUB 32 24 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)))) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 A B)))) 4) (MC-MEM (STEPN S (MAX-T0 A B))) 4) A) (EQUAL (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 A B)))) 8) (MC-MEM (STEPN S (MAX-T0 A B))) 4) B))), which simplifies, applying the lemmas SUB-NEG, ROM-ADDRP-LA1, ADD-ASSOCIATIVITY, READ-RN-EQUAL*, STEPN-RAM-ADDRP, STEPN-MCODE-ADDRP, INDEX-N-DEDUCTION2, ROM-ADDRP-LA2, and STEPN-ROM-ADDRP, and opening up the definitions of PLUS, TIMES, IREAD-MEM, NEG, READ-SP, L, SP, READ-AN, MAX-CODE, LESSP, EQUAL, MAX-SP, ADD, IREAD-DN, READ-DN, LEN, INDEX-N, RTS-ADDR, MAX-S0P, IMPLIES, and AND, to seven new formulas: Case 7. (IMPLIES (AND (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (MC-STATUS (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 'RUNNING)), which again simplifies, rewriting with RAM-ADDRP-3, and opening up LESSP, PLUS, and INDEX-N, to: T. Case 6. (IMPLIES (AND (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (MC-PC (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4))). However this again simplifies, applying the lemma RAM-ADDRP-3, and unfolding the functions LESSP, PLUS, and INDEX-N, to: T. Case 5. (IMPLIES (AND (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272))), which again simplifies, rewriting with RAM-ADDRP-3, and expanding the functions LESSP, PLUS, and INDEX-N, to: T. Case 4. (IMPLIES (AND (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))). This again simplifies, applying RAM-ADDRP-3, and opening up the definitions of LESSP, PLUS, and INDEX-N, to: T. Case 3. (IMPLIES (AND (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 8) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))). But this again simplifies, applying RAM-ADDRP-3, and opening up the functions LESSP, PLUS, and INDEX-N, to: T. Case 2. (IMPLIES (AND (EQUAL (MC-STATUS (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 'RUNNING) (EQUAL (MC-PC (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 16) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4)) (EVENP (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4)) (ROM-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 4294967270) (MC-MEM S) 46) (MCODE-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 4294967270) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM S) 40) (EQUAL* (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967276)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 3 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967280) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967284) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (MC-PC (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4))). However this again simplifies, applying ROM-ADDRP-LA1, SUB-NEG, RAM-ADDRP-3, MAX-S-S0-ELSE, ADD-ASSOCIATIVITY, DISJOINT-DEDUCTION2, and MAX-S-S0-MEM, and unfolding the functions MAX-SP, EQUAL, LESSP, MAX-CODE, READ-AN, PLUS, SP, L, READ-SP, TIMES, IREAD-MEM, NEG, INDEX-N, ADD, and DISJOINT, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 'RUNNING) (EQUAL (MC-PC (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 16) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4)) (EVENP (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4)) (ROM-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 4294967270) (MC-MEM S) 46) (MCODE-ADDRP (ADD 32 (READ-MEM (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 4294967270) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (MC-MEM S) 40) (EQUAL* (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967276)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 3 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-RN 32 2 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967280) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32)) (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967284) (MC-MEM (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)))) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32)) (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (EQUAL (ADD 32 (READ-RN 32 14 (MC-RFILE (STEPN S (MAX-T0 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))))) 4294967276) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272))). But this again simplifies, applying ROM-ADDRP-LA1, SUB-NEG, RAM-ADDRP-3, MAX-S-S0-ELSE, ADD-ASSOCIATIVITY, DISJOINT-DEDUCTION2, MAX-S-S0-MEM, and READ-RN-EQUAL*, and unfolding MAX-SP, EQUAL, LESSP, MAX-CODE, READ-AN, PLUS, SP, L, READ-SP, TIMES, IREAD-MEM, NEG, INDEX-N, ADD, and DISJOINT, to: T. Q.E.D. [ 0.0 1.2 0.1 ] MAX-GT-STATEP-S0 (FUNCTIONALLY-INSTANTIATE MAX-GT-CORRECTNESS (REWRITE) (IMPLIES (MAX-GT-STATEP S A B) (LET ((SN (STEPN S (MAX-GT-T A B)))) (AND (EQUAL (MC-STATUS SN) 'RUNNING) (EQUAL (MC-PC SN) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE SN)) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE SN)) (ADD 32 (READ-SP S) 4)) (IMPLIES (AND (LEQ OPLEN 32) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE SN)) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (AND (DISJOINT X K (SUB 32 24 (READ-SP S)) 40) (DISJOINT X K (SUB 32 28 (READ-SP S)) 4)) (EQUAL (READ-MEM X (MC-MEM SN) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 SN) (MAX-GT A B))))) MAX-CORRECTNESS ((MAX-STATEP MAX-GT-STATEP) (MAX-DISJOINT (LAMBDA (X K S) (DISJOINT X K (SUB 32 28 (READ-SP S)) 4))) (P-DISJOINT (LAMBDA (X K S) (DISJOINT X K (SUB 32 4 (READ-SP S)) 4))) (COMP-LOADP (LAMBDA (S A B) (LET ((COMP (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4))) (AND (EVENP COMP) (ROM-ADDRP COMP (MC-MEM S) (LEN (GT-CODE))) (MCODE-ADDRP COMP (MC-MEM S) (GT-CODE)) (RAM-ADDRP (SUB 32 28 (READ-SP S)) (MC-MEM S) 44))))) (MAX-T MAX-GT-T) (MAX-FN* MAX-GT) (FN*-STATEP GT-STATEP) (FN*-T GT-T) (FN* GT)) ((DISABLE IREAD-MEM))) WARNING: Note that the rewrite rule MAX-GT-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma MAX-GT-CORRECTNESS is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and seven replacement rules. The functional instantiation of MAX-CORRECTNESS under: ((MAX-STATEP MAX-GT-STATEP) (MAX-DISJOINT (LAMBDA (X K S) (DISJOINT X K (SUB '32 '28 (READ-SP S)) '4))) (P-DISJOINT (LAMBDA (X K S) (DISJOINT X K (SUB '32 '4 (READ-SP S)) '4))) (COMP-LOADP (LAMBDA (S A B) (AND (EVENP (READ-MEM (ADD '32 (READ-SP S) '12) (MC-MEM S) '4)) (AND (ROM-ADDRP (READ-MEM (ADD '32 (READ-SP S) '12) (MC-MEM S) '4) (MC-MEM S) (LEN (GT-CODE))) (AND (MCODE-ADDRP (READ-MEM (ADD '32 (READ-SP S) '12) (MC-MEM S) '4) (MC-MEM S) (GT-CODE)) (RAM-ADDRP (SUB '32 '28 (READ-SP S)) (MC-MEM S) '44)))))) (MAX-T MAX-GT-T) (MAX-FN* MAX-GT) (FN*-STATEP GT-STATEP) (FN*-T GT-T) (FN* GT)) requires us to prove: (AND (IMPLIES (AND (MAX-GT-STATEP S A B) (DISJOINT X K (SUB 32 28 (READ-SP S)) 4)) (DISJOINT X K (SUB 32 4 (READ-SP (STEPN S (MAX-T0 A B)))) 4)) (AND (IMPLIES (MAX-GT-STATEP S A B) (GT-STATEP (STEPN S (MAX-T0 A B)) A B)) (IMPLIES (MAX-GT-STATEP S A B) (DISJOINT (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40 (SUB 32 4 (READ-SP (STEPN S (MAX-T0 A B)))) 4)) (EQUAL (MAX-GT-STATEP S A B) (AND (MAX-SP S A B) (EVENP (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4) (MC-MEM S) (LEN (GT-CODE))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-SP S) 12) (MC-MEM S) 4) (MC-MEM S) (GT-CODE)) (RAM-ADDRP (SUB 32 28 (READ-SP S)) (MC-MEM S) 44)))) (EQUAL (MAX-GT-T A B) (SPLUS (MAX-T0 A B) (SPLUS (GT-T A B) (IF (NEGATIVEP (GT A B)) 7 6)))) (EQUAL (MAX-GT A B) (IF (NEGATIVEP (GT A B)) B A)) (IMPLIES (GT-STATEP S A B) (AND (EQUAL (MC-STATUS (STEPN S (GT-T A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GT-T A B))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GT-T A B)))) (ADD 32 (READ-SP S) 4)) (IMPLIES (AND (IF (LESSP 32 OPLEN) F T) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT X K (SUB 32 4 (READ-SP S)) 4) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GT-T A B))) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (GT-T A B))) (GT A B)))) (IMPLIES (AND (DISJOINT X N (SUB 32 4 (READ-SP S)) 4) (IF (LESSP N (PLUS J (INDEX-N Y X))) F T)) (DISJOINT Y J (SUB 32 4 (READ-SP S)) 4))). This conjecture can be simplified, using the abbreviations GT-STATEP, MAX-CODE, MAX-GT-STATEP, IMPLIES, AND, GT-CODE, SP, L, READ-AN, and READ-SP, to eight new goals: Case 8. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) (LEN '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 44) (DISJOINT X K (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 4)) (DISJOINT X K (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE (STEPN S (MAX-T0 A B))))) 4)), which simplifies, using linear arithmetic, rewriting with SUB-NEG, ROM-ADDRP-LA1, INDEX-N-X-X, ROM-ADDRP-LA2, RAM-ADDRP-3, MAX-GT-STATEP-S0, ADD-ASSOCIATIVITY, and DISJOINT-10, and unfolding the functions PLUS, LEN, NEG, MAX-GT-STATEP, EQUAL, LESSP, MAX-CODE, READ-AN, SP, L, READ-SP, GT-CODE, INDEX-N, and ADD, to: T. Case 7. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) (LEN '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 44)) (GT-STATEP (STEPN S (MAX-T0 A B)) A B)). This simplifies, applying SUB-NEG, STEPN-RAM-ADDRP, STEPN-MCODE-ADDRP, STEPN-ROM-ADDRP, MAX-GT-STATEP-S0, RAM-ADDRP-3, ROM-ADDRP-LA2, INDEX-N-X-X, and ROM-ADDRP-LA1, and expanding the definitions of PLUS, LEN, NEG, INDEX-N, GT-CODE, READ-SP, L, SP, READ-AN, MAX-CODE, LESSP, EQUAL, MAX-GT-STATEP, and GT-STATEP, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE (STEPN S (MAX-T0 (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4))))) 4294967292) (MC-MEM S) 16)). But this again simplifies, applying ROM-ADDRP-LA1, INDEX-N-X-X, ROM-ADDRP-LA2, SUB-NEG, RAM-ADDRP-3, MAX-GT-STATEP-S0, and ADD-ASSOCIATIVITY, and unfolding the functions MAX-GT-STATEP, EQUAL, LESSP, MAX-CODE, READ-AN, PLUS, SP, L, READ-SP, GT-CODE, LEN, NEG, INDEX-N, and ADD, to: T. Case 6. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) (LEN '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 44)) (DISJOINT (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) 40 (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE (STEPN S (MAX-T0 A B))))) 4)). This simplifies, applying SUB-NEG, ROM-ADDRP-LA1, INDEX-N-X-X, ROM-ADDRP-LA2, RAM-ADDRP-3, MAX-GT-STATEP-S0, ADD-ASSOCIATIVITY, and DISJOINT-DEDUCTION2, and unfolding the functions PLUS, LEN, NEG, MAX-GT-STATEP, EQUAL, LESSP, MAX-CODE, READ-AN, SP, L, READ-SP, GT-CODE, INDEX-N, ADD, and DISJOINT, to: T. Case 5. (EQUAL (MAX-GT-STATEP S A B) (AND (MAX-SP S A B) (EVENP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) (LEN '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 28 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 44))), which simplifies, rewriting with SUB-NEG, and expanding NEG, LEN, GT-CODE, READ-SP, L, SP, PLUS, READ-AN, MAX-CODE, MAX-GT-STATEP, MAX-SP, and AND, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 46) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 47 2 47 3 32 110 0 16 78 144 74 128 108 4 32 2 96 2 32 3 76 238 0 12 255 248 78 94 78 117)) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4)) (NOT (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967272) (MC-MEM S) 40)) (EVENP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4)) (ROM-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) 34) (MCODE-ADDRP (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 12) (MC-MEM S) 4) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117))) (EQUAL (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967268) (MC-MEM S) 44) F)), which again simplifies, rewriting with the lemma RAM-ADDRP-3, and unfolding the functions LESSP, PLUS, and INDEX-N, to: T. Case 4. (EQUAL (MAX-GT-T A B) (SPLUS (MAX-T0 A B) (SPLUS (GT-T A B) (IF (NEGATIVEP (GT A B)) 7 6)))), which simplifies, expanding the function MAX-GT-T, to: T. Case 3. (EQUAL (MAX-GT A B) (IF (NEGATIVEP (GT A B)) B A)), which simplifies, expanding the definition of MAX-GT, to: T. Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4))) (AND (EQUAL (MC-STATUS (STEPN S (GT-T A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GT-T A B))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GT-T A B)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)) (IMPLIES (AND (IF (LESSP 32 OPLEN) F T) (D2-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GT-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT X K (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 4) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GT-T A B))) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (GT-T A B))) (GT A B)))), which simplifies, applying SUB-NEG, INDEX-N-X-X, ROM-ADDRP-LA2, RAM-ADDRP-3, and GT-S-SN, and unfolding PLUS, NEG, GT-STATEP, EQUAL, LESSP, GT-CODE, READ-AN, SP, L, READ-SP, INDEX-N, RTS-ADDR, D2-7A2-5P, AND, and IMPLIES, to the following two new formulas: Case 2.2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (NOT (LESSP 32 OPLEN)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GT-T (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4))))) (READ-RN OPLEN RN (MC-RFILE S)))). But this again simplifies, applying INDEX-N-X-X, ROM-ADDRP-LA2, SUB-NEG, RAM-ADDRP-3, and GT-S-SN, and unfolding D2-7A2-5P, GT-STATEP, EQUAL, LESSP, PLUS, GT-CODE, READ-AN, SP, L, READ-SP, NEG, and INDEX-N, to: T. Case 2.1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 34) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 34 46 0 8 32 46 0 12 176 129 102 4 66 128 96 10 176 129 108 4 112 1 96 2 112 255 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (DISJOINT X K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 4)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GT-T (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) (IREAD-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4)))) K) (READ-MEM X (MC-MEM S) K))). This again simplifies, using linear arithmetic, rewriting with the lemmas DISJOINT-10, INDEX-N-X-X, ROM-ADDRP-LA2, SUB-NEG, RAM-ADDRP-3, and GT-S-SN, and expanding GT-STATEP, EQUAL, LESSP, PLUS, GT-CODE, READ-AN, SP, L, READ-SP, NEG, and INDEX-N, to: T. Case 1. (IMPLIES (AND (DISJOINT X N (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 4) (NOT (LESSP N (PLUS J (INDEX-N Y X))))) (DISJOINT Y J (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 4)), which simplifies, rewriting with SUB-NEG, INDEX-N-DEDUCTION2, and DISJOINT-LA4, and unfolding the definitions of PLUS, NEG, LESSP, and INDEX-N, to: T. Q.E.D. [ 0.0 0.5 0.1 ] MAX-GT-CORRECTNESS