(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 FOO-CODE NIL '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) Note that (LISTP (FOO-CODE)) is a theorem. [ 0.0 0.0 0.0 ] FOO-CODE (DEFN FOO (A B X) (IF (EQUAL X 0) A B)) Note that (OR (EQUAL (FOO A B X) A) (EQUAL (FOO A B X) B)) is a theorem. [ 0.0 0.0 0.0 ] FOO (DEFN FOO-T (X) (IF (EQUAL X 0) 7 8)) Observe that (NUMBERP (FOO-T X)) is a theorem. [ 0.0 0.0 0.0 ] FOO-T (DEFN FOO-STATEP (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (FOO-CODE)) (RAM-ADDRP (SUB 32 4 (READ-SP S)) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (SUB 32 4 (READ-SP 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 (FOO-STATEP S A B)) (TRUEP (FOO-STATEP S A B))) is a theorem. [ 0.0 0.0 0.0 ] FOO-STATEP (PROVE-LEMMA FOO-CORRECTNESS (REWRITE) (LET ((X (IREAD-MEM 10000 (MC-MEM S) 4))) (IMPLIES (FOO-STATEP S A B) (AND (EQUAL (MC-STATUS (STEPN S (FOO-T X))) 'RUNNING) (EQUAL (MC-PC (STEPN S (FOO-T X))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (FOO-T X)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (FOO-T X)))) (ADD 32 (READ-AN 32 7 S) 4)) (IMPLIES (D2-7A2-5P RN) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (FOO-T X)))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT X K (SUB 32 4 (READ-SP S)) 16) (EQUAL (READ-MEM X (MC-MEM (STEPN S (FOO-T X))) K) (READ-MEM X (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (FOO-T X))) (FOO A B X)))))) WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that the rewrite rule FOO-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that FOO-CORRECTNESS contains the free variables B and A which will be chosen by instantiating the hypothesis (FOO-STATEP S A B). WARNING: Note that the proposed lemma FOO-CORRECTNESS 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 FOO-CODE, FOO-STATEP, IMPLIES, SP, L, READ-SP, and READ-AN, to the conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE 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 (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4)))) 'RUNNING) (EQUAL (MC-PC (STEPN S (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4)))) (RTS-ADDR S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4))))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4))))) (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 (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4))))) (READ-RN OPLEN RN (MC-RFILE S)))) (IMPLIES (DISJOINT (IREAD-MEM 10000 (MC-MEM S) 4) K (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 16) (EQUAL (READ-MEM (IREAD-MEM 10000 (MC-MEM S) 4) (MC-MEM (STEPN S (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4)))) K) (READ-MEM (IREAD-MEM 10000 (MC-MEM S) 4) (MC-MEM S) K))) (EQUAL (IREAD-DN 32 0 (STEPN S (FOO-T (IREAD-MEM 10000 (MC-MEM S) 4)))) (FOO A B (IREAD-MEM 10000 (MC-MEM S) 4))))). This simplifies, rewriting with SUB-NEG, and expanding the definitions of PLUS, NEG, TIMES, IREAD-MEM, FOO-T, READ-AN, RTS-ADDR, D2-7A2-5P, IMPLIES, READ-DN, IREAD-DN, FOO, and AND, to 14 new formulas: Case 14.(IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (MC-STATUS (STEPN S 8)) '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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (MC-STATUS (STEPN S 7)) 'RUNNING)). 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (MC-PC (STEPN S 8)) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))). But this again simplifies, applying 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (MC-PC (STEPN S 7)) (READ-MEM (READ-RN 32 15 (MC-RFILE S)) (MC-MEM S) 4))), which 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (READ-RN 32 14 (MC-RFILE S)))), which again simplifies, applying 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 7))) (READ-RN 32 14 (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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 8))) (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4))). 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, ADD-0, HEAD-READ-RN, READ-WRITE-MEM2, WRITE-MEMP-RAM2, DISJOINT-DEDUCTION1, STEPN-REWRITER0, and STEPN-REWRITER, and opening up 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 7))) (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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 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 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (READ-RN OPLEN RN (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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 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 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 8))) (READ-RN OPLEN RN (MC-RFILE S)))). But this again simplifies, applying 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (DISJOINT (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (READ-MEM (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) (MC-MEM (STEPN S 7)) K) (READ-MEM (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) (MC-MEM S) K))), which 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, 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) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (DISJOINT (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) K (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (READ-MEM (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) (MC-MEM (STEPN S 8)) K) (READ-MEM (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) (MC-MEM S) K))). 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, RTD-MAPPING, and RTS-INS, to: T. Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (NOT (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0))) (EQUAL (NAT-TO-INT (READ-RN 32 0 (MC-RFILE (STEPN S 8))) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 8) (MC-MEM S) 4) 32))). This again simplifies, applying 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-0, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, JMP-INS, JMP-ADDR-MODEP, PC-DISP, JMP-MAPPING, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, RTD-MAPPING, and RTS-INS, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 30) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 74 184 39 16 103 0 0 10 32 46 0 12 78 250 0 6 32 46 0 8 78 113 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (RAM-ADDRP 10000 (MC-MEM S) 4) (DISJOINT 10000 4 (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967292) 16) (EQUAL (NAT-TO-INT (READ-MEM 10000 (MC-MEM S) 4) 32) 0)) (EQUAL (NAT-TO-INT (READ-RN 32 0 (MC-RFILE (STEPN S 7))) 32) (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))), 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, DISJOINT-10, READ-WRITE-MEM1, CAR-CONS, CDR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-MEMP-RAM0, WRITE-MEMP->READ-MEMP, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, MOVE-BEQ-INT-1, READ-MEM-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, 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, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, MC-HALTP, MC-INSTATE, S_MODE, ABSOLUTE-SHORT, CONS, EFFEC-ADDR, CAR, CDR, OP-SZ, TST-ADDR-MODEP, TST-INS, EVENP, B, HEAD, BCC-RA-SR, TIMES, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, ADDR-DISP, DISJOINT, MAPPING, D-MAPPING, MOVE-EFFECT, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, NOP-SUBGROUP, NOP-INS, LONG-READ, UINT-RANGEP, LONG-READP, UNLK-INS, RTD-MAPPING, and RTS-INS, to: T. Q.E.D. [ 0.0 3.9 0.2 ] FOO-CORRECTNESS