(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 LOG2-CODE NIL '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) Observe that (LISTP (LOG2-CODE)) is a theorem. [ 0.0 0.0 0.0 ] LOG2-CODE (DEFN LOG2 (N LOG2) (IF (LESSP 1 N) (LOG2 (QUOTIENT N 2) (ADD1 LOG2)) LOG2)) Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of NUMBERP and EQUAL can be used to show that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, LOG2 is accepted under the definitional principle. From the definition we can conclude that: (OR (NUMBERP (LOG2 N LOG2)) (EQUAL (LOG2 N LOG2) LOG2)) is a theorem. [ 0.0 0.0 0.0 ] LOG2 (DEFN LOG2-T0 (N) (IF (LESSP 1 N) (SPLUS 7 (LOG2-T0 (QUOTIENT N 2))) 7)) Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of NUMBERP and EQUAL can be used to establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, LOG2-T0 is accepted under the principle of definition. Note that (NUMBERP (LOG2-T0 N)) is a theorem. [ 0.0 0.0 0.0 ] LOG2-T0 (DEFN LOG2-T (N) (SPLUS 5 (LOG2-T0 N))) Observe that (NUMBERP (LOG2-T N)) is a theorem. [ 0.0 0.0 0.0 ] LOG2-T (DEFN LOG2-INDUCT (S N LOG2) (IF (LESSP 1 N) (LOG2-INDUCT (STEPN S 7) (QUOTIENT N 2) (ADD1 LOG2)) T)) Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of NUMBERP and EQUAL can be used to establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, LOG2-INDUCT is accepted under the principle of definition. Note that: (TRUEP (LOG2-INDUCT S N LOG2)) is a theorem. [ 0.0 0.0 0.0 ] LOG2-INDUCT (DEFN LOG2-STATEP (S N) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 40) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (LOG2-CODE)) (RAM-ADDRP (SUB 32 8 (READ-SP S)) (MC-MEM S) 16) (EQUAL N (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (NUMBERP N))) From the definition we can conclude that: (OR (FALSEP (LOG2-STATEP S N)) (TRUEP (LOG2-STATEP S N))) is a theorem. [ 0.0 0.0 0.0 ] LOG2-STATEP (DEFN LOG2-S0P (S N LOG2) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) (LOG2-CODE)) (RAM-ADDRP (SUB 32 4 (READ-AN 32 6 S)) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N))) Observe that: (OR (FALSEP (LOG2-S0P S N LOG2)) (TRUEP (LOG2-S0P S N LOG2))) is a theorem. [ 0.0 0.0 0.0 ] LOG2-S0P (PROVE-LEMMA LOG2-S-S0 NIL (IMPLIES (LOG2-STATEP S N) (LOG2-S0P (STEPN S 5) N 0))) This formula can be simplified, using the abbreviations SP, L, READ-AN, READ-SP, LOG2-CODE, LOG2-STATEP, and IMPLIES, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 40) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (NUMBERP N)) (LOG2-S0P (STEPN S 5) N 0)), 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, CDR-CONS, CAR-CONS, READ-WRITE-RN, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-WRITE-RN, HEAD-LEMMA, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITE-MEMP->READ-MEMP, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, STEPN-REWRITER, NAT-TO-INT-RANGEP, PLUS-0, READ-MEM-NAT-RANGEP, WRITE-MEM-MAINTAIN-RAM-ADDRP, RAM-ADDRP-3, WRITE-MEM-MCODE-ADDRP, WRITE-MEM-MAINTAIN-ROM-ADDRP, ROM-ADDRP-LA2, INDEX-N-X-X, ADD-0, and MC-PC-RANGEP, and opening up PLUS, NEG, TIMES, IREAD-MEM, 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, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, NUMBERP, CDR, OPERAND, MAPPING, M-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, PRE-EFFECT, B, OP-SZ, ADDR-PREDEC, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, ADDR-DISP, DISJOINT, D-MAPPING, CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, HEAD, BCC-RA-SR, COND-FIELD, BCC-GROUP, NAT-TO-INT, IREAD-DN, LOG2-CODE, and LOG2-S0P, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S-S0 (PROVE-LEMMA LOG2-S-S0-ELSE (REWRITE) (IMPLIES (LOG2-STATEP S N) (AND (EQUAL (LINKED-RTS-ADDR (STEPN S 5)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 5)) (READ-AN 32 6 S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 5))) (SUB 32 4 (READ-SP S))) (EQUAL (RN-SAVED (STEPN S 5)) (READ-DN 32 2 S))))) WARNING: Note that the rewrite rule LOG2-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that LOG2-S-S0-ELSE contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). WARNING: Note that the rewrite rule LOG2-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that LOG2-S-S0-ELSE contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). WARNING: Note that LOG2-S-S0-ELSE contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). WARNING: Note that the rewrite rule LOG2-S-S0-ELSE will be stored so as to apply only to terms with the nonrecursive function symbol RN-SAVED. WARNING: Note that LOG2-S-S0-ELSE contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). WARNING: Note that the proposed lemma LOG2-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 LOG2-CODE, LOG2-STATEP, IMPLIES, READ-DN, SP, L, READ-SP, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 40) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (NUMBERP N)) (AND (EQUAL (LINKED-RTS-ADDR (STEPN S 5)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 5)) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 5))) (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)))) (EQUAL (RN-SAVED (STEPN S 5)) (READ-RN 32 2 (MC-RFILE S))))), which 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, CDR-CONS, CAR-CONS, READ-WRITE-RN, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-WRITE-RN, HEAD-LEMMA, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITE-MEMP->READ-MEMP, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, STEPN-REWRITER, DISJOINT-DEDUCTION1, ADD-0, HEAD-READ-RN, and READ-WRITE-MEM2, and opening up the functions PLUS, NEG, TIMES, IREAD-MEM, 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, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, NUMBERP, CDR, OPERAND, MAPPING, M-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, PRE-EFFECT, B, OP-SZ, ADDR-PREDEC, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, ADDR-DISP, DISJOINT, D-MAPPING, CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, HEAD, BCC-RA-SR, COND-FIELD, BCC-GROUP, LINKED-RTS-ADDR, RTS-ADDR, UINT-RANGEP, LINKED-A6, RN-SAVED, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] LOG2-S-S0-ELSE (PROVE-LEMMA LOG2-S-S0-RFILE (REWRITE) (IMPLIES (AND (LOG2-STATEP S N) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 5))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that LOG2-S-S0-RFILE contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). This formula can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, SP, L, READ-AN, READ-SP, LOG2-CODE, LOG2-STATEP, AND, and IMPLIES, to the new formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 40) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (NUMBERP N) (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))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 5))) (READ-RN OPLEN RN (MC-RFILE S)))), 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, CDR-CONS, CAR-CONS, READ-WRITE-RN, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-WRITE-RN, HEAD-LEMMA, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITE-MEMP->READ-MEMP, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, and STEPN-REWRITER, and expanding PLUS, NEG, TIMES, IREAD-MEM, 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, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, NUMBERP, CDR, OPERAND, MAPPING, M-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, PRE-EFFECT, B, OP-SZ, ADDR-PREDEC, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, ADDR-DISP, DISJOINT, D-MAPPING, CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, HEAD, BCC-RA-SR, COND-FIELD, and BCC-GROUP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S-S0-RFILE (PROVE-LEMMA LOG2-S-S0-MEM (REWRITE) (IMPLIES (AND (LOG2-STATEP S N) (DISJOINT X K (SUB 32 8 (READ-SP S)) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 5)) K) (READ-MEM X (MC-MEM S) K)))) WARNING: Note that LOG2-S-S0-MEM contains the free variable N which will be chosen by instantiating the hypothesis (LOG2-STATEP S N). This conjecture can be simplified, using the abbreviations LOG2-CODE, LOG2-STATEP, AND, 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) 40) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (NUMBERP N) (DISJOINT X K (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 5)) 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, CDR-CONS, CAR-CONS, READ-WRITE-RN, WRITE-MEM-MAINTAIN-WRITE-MEMP, WRITE-WRITE-RN, HEAD-LEMMA, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITE-MEMP->READ-MEMP, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, BITP-FIX-BIT, FIX-BIT-BITP, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and opening up the functions PLUS, NEG, TIMES, IREAD-MEM, 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, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_MODE, MC-INSTATE, MC-HALTP, READ-DN, NUMBERP, CDR, OPERAND, MAPPING, M-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, PRE-EFFECT, B, OP-SZ, ADDR-PREDEC, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, EVENP, ADDR-DISP, DISJOINT, D-MAPPING, CLR-SUBGROUP, OP-LEN, Q, CLR-EFFECT, B1, CLR-CVZNX, CLR-ADDR-MODEP, CLR-INS, HEAD, BCC-RA-SR, COND-FIELD, and BCC-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] LOG2-S-S0-MEM (PROVE-LEMMA LOG2-S0-SN-BASE (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (NOT (LESSP 1 N))) (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)) LOG2) (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))))) WARNING: Note that LOG2-S0-SN-BASE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN-BASE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the rewrite rule LOG2-S0-SN-BASE will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that LOG2-S0-SN-BASE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN-BASE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN-BASE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the proposed lemma LOG2-S0-SN-BASE 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 NOT, LOG2-CODE, LOG2-S0P, AND, IMPLIES, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N) (NOT (LESSP 1 N))) (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)) LOG2) (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)))), which simplifies, appealing to the lemmas SUB-NEG, PLUS-COMMUTATIVITY, MC-STATUS-REWRITE, CAR-CONS, MC-RFILE-REWRITE, ADD-NAT-RANGEP, MC-PC-REWRITE, CDR-CONS, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, READ-WRITE-RN, SET-CVZNX-X, SET-SET-CVZNX1, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, BLT-BGE, SUB-BGE, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, FIX-BIT-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, 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, D-MAPPING, D_RN, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, EXT, HEAD, B, B0P, BITN, MOVEQ-INS, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, NUMBERP, CDR, OPERAND, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, ADD, EVENP, BCC-RA-SR, B-NOT, ILESSP, NEGP, NAT-TO-INT, NAT-RANGEP, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, MOVE-MAPPING, D_MODE, MOVE-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, UPDATE-RFILE, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, MISC-GROUP, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, TIMES, LINKED-RTS-ADDR, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] LOG2-S0-SN-BASE (PROVE-LEMMA LOG2-S0-SN-BASE-RFILE (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (NOT (LESSP 1 N)) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (RN-SAVED S) OPLEN))))) WARNING: Note that LOG2-S0-SN-BASE-RFILE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). This formula can be simplified, using the abbreviations D2-7A2-5P, NOT, READ-AN, LOG2-CODE, LOG2-S0P, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N) (NOT (LESSP 1 N)) (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 (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (RN-SAVED S) OPLEN)))), which simplifies, rewriting with SUB-NEG, PLUS-COMMUTATIVITY, MC-STATUS-REWRITE, CAR-CONS, MC-RFILE-REWRITE, ADD-NAT-RANGEP, MC-PC-REWRITE, CDR-CONS, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, READ-WRITE-RN, SET-CVZNX-X, SET-SET-CVZNX1, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, BLT-BGE, SUB-BGE, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, FIX-BIT-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and opening up NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, D-MAPPING, D_RN, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, EXT, HEAD, B, B0P, BITN, MOVEQ-INS, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, NUMBERP, CDR, OPERAND, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, ADD, EVENP, BCC-RA-SR, B-NOT, ILESSP, NEGP, NAT-TO-INT, NAT-RANGEP, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, MOVE-MAPPING, D_MODE, MOVE-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, UPDATE-RFILE, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, MISC-GROUP, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, D2-7A2-5P, D3-7A2-5P, and RN-SAVED, to the following two new conjectures: Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) 40) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (INT-RANGEP (PLUS (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NUMBERP (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (NOT (LESSP 1 (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32))) (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 (LESSP 32 OPLEN)) (NOT (EQUAL RN 2)) (EQUAL 2 RN)) (EQUAL (HEAD (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 4) OPLEN) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, obviously, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) 40) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (INT-RANGEP (PLUS (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NUMBERP (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (NOT (LESSP 1 (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32))) (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 (LESSP 32 OPLEN)) (EQUAL RN 2) (NOT (EQUAL 2 RN))) (EQUAL (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 4) OPLEN))). This again simplifies, trivially, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S0-SN-BASE-RFILE (PROVE-LEMMA LOG2-S0S-N-BASE-MEM (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (NOT (LESSP 1 N))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K)))) WARNING: Note that LOG2-S0S-N-BASE-MEM contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). This formula can be simplified, using the abbreviations NOT, READ-AN, LOG2-CODE, LOG2-S0P, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N) (NOT (LESSP 1 N))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K))), which simplifies, rewriting with SUB-NEG, PLUS-COMMUTATIVITY, MC-STATUS-REWRITE, CAR-CONS, MC-RFILE-REWRITE, ADD-NAT-RANGEP, MC-PC-REWRITE, CDR-CONS, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, READ-WRITE-RN, SET-CVZNX-X, SET-SET-CVZNX1, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, BLT-BGE, SUB-BGE, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, FIX-BIT-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, D-MAPPING, D_RN, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, EXT, HEAD, B, B0P, BITN, MOVEQ-INS, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, NUMBERP, CDR, OPERAND, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, ADD, EVENP, BCC-RA-SR, B-NOT, ILESSP, NEGP, NAT-TO-INT, NAT-RANGEP, BRANCH-CC, COND-FIELD, BCC-GROUP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, MOVE-MAPPING, D_MODE, MOVE-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, UPDATE-RFILE, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, MISC-GROUP, NOP-SUBGROUP, RTD-MAPPING, READ-SP, and RTS-INS, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S0S-N-BASE-MEM (PROVE-LEMMA LOG2-RANGEP-LA (REWRITE) (IMPLIES (AND (INT-RANGEP (PLUS M N) 32) (LESSP 1 N)) (INT-RANGEP (ADD1 (PLUS M (QUOTIENT N 2))) 32)) ((ENABLE INT-RANGEP))) This formula simplifies, rewriting with SUB1-ADD1, and opening up the functions EXP, SUB1, NUMBERP, EQUAL, INT-RANGEP, and LESSP, to the new formula: (IMPLIES (AND (LESSP (PLUS M N) 2147483648) (LESSP 1 N)) (LESSP (PLUS M (QUOTIENT N 2)) 2147483647)). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace N by (PLUS Z (TIMES 2 X)) to eliminate (QUOTIENT N 2) and (REMAINDER N 2). We employ REMAINDER-LESSP, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to restrict the new variables. This produces the following four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP N)) (LESSP (PLUS M N) 2147483648) (LESSP 1 N)) (LESSP (PLUS M (QUOTIENT N 2)) 2147483647)). This further simplifies, opening up the function LESSP, to: T. Case 3. (IMPLIES (AND (EQUAL 2 0) (LESSP (PLUS M N) 2147483648) (LESSP 1 N)) (LESSP (PLUS M (QUOTIENT N 2)) 2147483647)), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP 2)) (LESSP (PLUS M N) 2147483648) (LESSP 1 N)) (LESSP (PLUS M (QUOTIENT N 2)) 2147483647)), which further simplifies, obviously, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z 2) (NOT (ZEROP 2))) (NOT (EQUAL 2 0)) (LESSP (PLUS M Z (TIMES 2 X)) 2147483648) (LESSP 1 (PLUS Z (TIMES 2 X)))) (LESSP (PLUS M X) 2147483647)). This further simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.3 0.0 ] LOG2-RANGEP-LA (PROVE-LEMMA LOG2-S0-S0 (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (LESSP 1 N)) (AND (LOG2-S0P (STEPN S 7) (QUOTIENT N 2) (ADD1 LOG2)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 7))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 7)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 7)) (LINKED-RTS-ADDR S)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K)) (EQUAL (RN-SAVED (STEPN S 7)) (RN-SAVED S)))) ((ENABLE IQUOTIENT IPLUS))) WARNING: Note that the rewrite rule LOG2-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LOG2-S0P. WARNING: Note that LOG2-S0-S0 contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the rewrite rule LOG2-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that LOG2-S0-S0 contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the rewrite rule LOG2-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that LOG2-S0-S0 contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-S0 contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the rewrite rule LOG2-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol RN-SAVED. WARNING: Note that LOG2-S0-S0 contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the proposed lemma LOG2-S0-S0 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 READ-AN, LOG2-CODE, LOG2-S0P, AND, and IMPLIES, to the conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N) (LESSP 1 N)) (AND (LOG2-S0P (STEPN S 7) (QUOTIENT N 2) (ADD1 LOG2)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 7))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 7)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 7)) (LINKED-RTS-ADDR S)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 7)) K) (READ-MEM X (MC-MEM S) K)) (EQUAL (RN-SAVED (STEPN S 7)) (RN-SAVED S)))). This simplifies, appealing to the lemmas SUB-NEG, PLUS-COMMUTATIVITY, MC-STATUS-REWRITE, CAR-CONS, MC-RFILE-REWRITE, ADD-NAT-RANGEP, MC-PC-REWRITE, CDR-CONS, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, READ-WRITE-RN, SET-CVZNX-X, SET-SET-CVZNX1, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, BLT-BGE, SUB-BGE, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, ADD-C-BITP, BGE-V0, MOVE-BMI, MOVE-N-BITP, ADD-0, HEAD-LEMMA, MC-PC-RANGEP, STEPN-REWRITER0, STEPN-REWRITER, LOG2-RANGEP-LA, SUB1-ADD1, PLUS-ADD1, IPLUS-COMMUTATIVITY, ADD-INT, ASR-NAT-RANGEP, ASR-INT, RAM-ADDRP-3, ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and expanding the definitions of NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, D-MAPPING, D_RN, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, EXT, HEAD, B, B0P, BITN, MOVEQ-INS, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, NUMBERP, CDR, OPERAND, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, ADD, EVENP, BCC-RA-SR, B-NOT, ILESSP, NEGP, NAT-TO-INT, NAT-RANGEP, BRANCH-CC, COND-FIELD, BCC-GROUP, ADDQ-INS, ADDQ-ADDR-MODEP, AN-DIRECT-MODEP, I-DATA, MAPPING, ADD-EFFECT, ADD-CVZNX, ADD-MAPPING, SCC-GROUP, TST-SUBGROUP, TST-ADDR-MODEP, TST-INS, MISC-GROUP, FIX-BIT, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, REGISTER-ASR-INS, S&R-GROUP, IPLUS, MINUS, NEGATIVE-GUTS, EXP, IQUOTIENT, READ-AN, LOG2-CODE, LOG2-S0P, LINKED-A6, LINKED-RTS-ADDR, RN-SAVED, and AND, to the following two new goals: Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) 40) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (INT-RANGEP (PLUS (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NUMBERP (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (LESSP 1 (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (NOT (INT-RANGEP (ADD1 (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32))) (EQUAL (ADD1 (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (DIFFERENCE (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) 4294967295))). However this again simplifies, using linear arithmetic, rewriting with ABS-LESSP-INT-RANGEP, and opening up the definitions of ABS and NEGP, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) 40) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967272) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 16) (INT-RANGEP (PLUS (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NUMBERP (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (LESSP 1 (NAT-TO-INT (READ-RN 32 0 (MC-RFILE S)) 32)) (NOT (INT-RANGEP (ADD1 (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32))) (NOT (LESSP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) 4294967295))). However this again simplifies, using linear arithmetic, rewriting with ABS-LESSP-INT-RANGEP, and unfolding ABS and NEGP, to: T. Q.E.D. [ 0.0 0.4 0.1 ] LOG2-S0-S0 (PROVE-LEMMA LOG2-S0-S0-RFILE (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (LESSP 1 N) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that LOG2-S0-S0-RFILE contains the free variables LOG2 and N which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). This conjecture can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, READ-AN, LOG2-CODE, LOG2-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) 40) (MCODE-ADDRP (SUB 32 24 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 32 46 0 8 66 129 96 10 82 129 74 128 108 2 82 128 226 128 116 1 180 128 109 240 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (SUB 32 4 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 16) (EQUAL N (IREAD-DN 32 0 S)) (EQUAL LOG2 (IREAD-DN 32 1 S)) (INT-RANGEP (PLUS LOG2 N) 32) (NUMBERP LOG2) (NUMBERP N) (LESSP 1 N) (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))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, rewriting with SUB-NEG, PLUS-COMMUTATIVITY, MC-STATUS-REWRITE, CAR-CONS, MC-RFILE-REWRITE, ADD-NAT-RANGEP, MC-PC-REWRITE, CDR-CONS, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, READ-WRITE-RN, SET-CVZNX-X, SET-SET-CVZNX1, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, BLT-BGE, SUB-BGE, READ-RN-NAT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, BITP-FIX-BIT, SUB-V-BITP, ADD-C-BITP, BGE-V0, MOVE-BMI, MOVE-N-BITP, ADD-0, HEAD-LEMMA, MC-PC-RANGEP, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the definitions of NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, D-MAPPING, D_RN, MOVE-EFFECT, MOVE-N, MOVE-Z, B0, MOVE-CVZNX, EXT, HEAD, B, B0P, BITN, MOVEQ-INS, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, NUMBERP, CDR, OPERAND, CMP-CVZNX, UPDATE-CCR, Q, CMP-GROUP, ADD, EVENP, BCC-RA-SR, B-NOT, ILESSP, NEGP, NAT-TO-INT, NAT-RANGEP, BRANCH-CC, COND-FIELD, BCC-GROUP, ADDQ-INS, ADDQ-ADDR-MODEP, AN-DIRECT-MODEP, I-DATA, MAPPING, ADD-EFFECT, ADD-CVZNX, ADD-MAPPING, SCC-GROUP, TST-SUBGROUP, TST-ADDR-MODEP, TST-INS, MISC-GROUP, FIX-BIT, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, REGISTER-ASR-INS, and S&R-GROUP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S0-S0-RFILE (PROVE-LEMMA LOG2-S0-SN (REWRITE) (IMPLIES (LOG2-S0P S N LOG2) (AND (EQUAL (MC-STATUS (STEPN S (LOG2-T0 N))) 'RUNNING) (EQUAL (MC-PC (STEPN S (LOG2-T0 N))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (LOG2-T0 N))) (LOG2 N LOG2)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (LOG2-T0 N)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (LOG2-T0 N)))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (LOG2-T0 N))) K) (READ-MEM X (MC-MEM S) K)))) ((INDUCT (LOG2-INDUCT S N LOG2)) (DISABLE LOG2-S0P))) WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the rewrite rule LOG2-S0-SN will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that LOG2-S0-SN contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). WARNING: Note that the proposed lemma LOG2-S0-SN 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 IMPLIES, NOT, OR, AND, and READ-AN, to two new goals: Case 2. (IMPLIES (AND (LESSP 1 N) (IMPLIES (LOG2-S0P (STEPN S 7) (QUOTIENT N 2) (ADD1 LOG2)) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2)))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2)))) (LINKED-RTS-ADDR (STEPN S 7))) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2)))) (LOG2 (QUOTIENT N 2) (ADD1 LOG2))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2))))) (LINKED-A6 (STEPN S 7))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2))))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN S 7))) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2)))) K) (READ-MEM X (MC-MEM (STEPN S 7)) K)))) (LOG2-S0P S N LOG2)) (AND (EQUAL (MC-STATUS (STEPN S (LOG2-T0 N))) 'RUNNING) (EQUAL (MC-PC (STEPN S (LOG2-T0 N))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (LOG2-T0 N))) (LOG2 N LOG2)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (LOG2-T0 N)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (LOG2-T0 N)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (LOG2-T0 N))) K) (READ-MEM X (MC-MEM S) K)))), which simplifies, rewriting with the lemmas LOG2-S0-S0 and STEPN-LEMMA, and opening up the functions READ-AN, PLUS, LINKED-RTS-ADDR, READ-DN, IREAD-DN, LINKED-A6, AND, IMPLIES, LOG2-T0, EQUAL, and LOG2, to: T. Case 1. (IMPLIES (AND (NOT (LESSP 1 N)) (LOG2-S0P S N LOG2)) (AND (EQUAL (MC-STATUS (STEPN S (LOG2-T0 N))) 'RUNNING) (EQUAL (MC-PC (STEPN S (LOG2-T0 N))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (LOG2-T0 N))) (LOG2 N LOG2)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (LOG2-T0 N)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (LOG2-T0 N)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (LOG2-T0 N))) K) (READ-MEM X (MC-MEM S) K)))), which simplifies, rewriting with LOG2-S0-SN-BASE and LOG2-S0S-N-BASE-MEM, and unfolding the functions LOG2-T0, EQUAL, READ-AN, PLUS, LINKED-RTS-ADDR, LOG2, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.2 0.0 ] LOG2-S0-SN (PROVE-LEMMA LOG2-S0-SN-RFILE (REWRITE) (IMPLIES (AND (LOG2-S0P S N LOG2) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (LOG2-T0 N)))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (RN-SAVED S) OPLEN)))) ((INDUCT (LOG2-INDUCT S N LOG2)) (DISABLE LOG2-S0P))) WARNING: Note that LOG2-S0-SN-RFILE contains the free variable LOG2 which will be chosen by instantiating the hypothesis (LOG2-S0P S N LOG2). This formula can be simplified, using the abbreviations D2-7A2-5P, IMPLIES, NOT, OR, and AND, to the following two new goals: Case 2. (IMPLIES (AND (LESSP 1 N) (IMPLIES (AND (LOG2-S0P (STEPN S 7) (QUOTIENT N 2) (ADD1 LOG2)) (D2-7A2-5P RN) (IF (LESSP 32 OPLEN) F T)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2))))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE (STEPN S 7))) (HEAD (RN-SAVED (STEPN S 7)) OPLEN)))) (LOG2-S0P S N LOG2) (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 (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (LOG2-T0 N)))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (RN-SAVED S) OPLEN)))). This simplifies, rewriting with LOG2-S0-S0, SUB-NEG, LOG2-S0-S0-RFILE, and STEPN-LEMMA, and expanding the functions D2-7A2-5P, AND, D3-7A2-5P, NEG, READ-AN, PLUS, RN-SAVED, IMPLIES, LOG2-T0, EQUAL, and NUMBERP, to: (IMPLIES (AND (LESSP 1 N) (EQUAL RN 2) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2))))) (HEAD (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 4) OPLEN)) (LOG2-S0P S N LOG2) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN (STEPN S 7) (LOG2-T0 (QUOTIENT N 2))))) (HEAD (READ-MEM (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967292) (MC-MEM S) 4) OPLEN))). This again simplifies, clearly, to: T. Case 1. (IMPLIES (AND (NOT (LESSP 1 N)) (LOG2-S0P S N LOG2) (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 (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (LOG2-T0 N)))) (IF (D3-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (HEAD (RN-SAVED S) OPLEN)))). This simplifies, applying SUB-NEG and LOG2-S0-SN-BASE-RFILE, and expanding the definitions of LOG2-T0, D2-7A2-5P, D3-7A2-5P, NEG, READ-AN, PLUS, and RN-SAVED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-S0-SN-RFILE (PROVE-LEMMA LOG2-CORRECT (REWRITE) (IMPLIES (LOG2-STATEP S N) (AND (EQUAL (MC-STATUS (STEPN S (LOG2-T N))) 'RUNNING) (EQUAL (MC-PC (STEPN S (LOG2-T N))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (LOG2-T N))) (LOG2 N 0)) (EQUAL (READ-AN 32 6 (STEPN S (LOG2-T N))) (READ-AN 32 6 S)) (EQUAL (READ-AN 32 7 (STEPN S (LOG2-T N))) (ADD 32 (READ-AN 32 7 S) 4)))) ((USE (LOG2-S-S0)) (DISABLE LOG2-STATEP LOG2-S0P LINKED-RTS-ADDR LINKED-A6 IREAD-DN))) WARNING: Note that the rewrite rule LOG2-CORRECT will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the rewrite rule LOG2-CORRECT will be stored so as to apply only to terms with the nonrecursive function symbol READ-AN. WARNING: Note that the rewrite rule LOG2-CORRECT will be stored so as to apply only to terms with the nonrecursive function symbol READ-AN. WARNING: Note that the proposed lemma LOG2-CORRECT is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and five replacement rules. This conjecture can be simplified, using the abbreviations IMPLIES, READ-AN, STEPN-LEMMA, and LOG2-T, to: (IMPLIES (AND (IMPLIES (LOG2-STATEP S N) (LOG2-S0P (STEPN S 5) N 0)) (LOG2-STATEP S N)) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 5) (LOG2-T0 N))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 5) (LOG2-T0 N))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 5) (LOG2-T0 N))) (LOG2 N 0)) (EQUAL (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN (STEPN S 5) (LOG2-T0 N)))) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 (PLUS 8 7) (MC-RFILE (STEPN (STEPN S 5) (LOG2-T0 N)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)))). This simplifies, applying the lemmas LOG2-S0-SN, LOG2-S-S0-ELSE, SUB-NEG, and ADD-ASSOCIATIVITY, and unfolding IMPLIES, EQUAL, READ-AN, PLUS, RTS-ADDR, NEG, READ-SP, L, SP, ADD, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LOG2-CORRECT (PROVE-LEMMA LOG2-RFILE (REWRITE) (IMPLIES (AND (LOG2-STATEP S N) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (LOG2-T N)))) (READ-RN OPLEN RN (MC-RFILE S)))) ((USE (LOG2-S-S0)) (DISABLE LOG2-STATEP LOG2-S0P))) This conjecture can be simplified, using the abbreviations D2-7A2-5P, AND, IMPLIES, STEPN-LEMMA, and LOG2-T, to the goal: (IMPLIES (AND (IMPLIES (LOG2-STATEP S N) (LOG2-S0P (STEPN S 5) N 0)) (LOG2-STATEP S N) (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 (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 5) (LOG2-T0 N)))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, appealing to the lemmas LOG2-S-S0-ELSE, HEAD-READ-RN, LOG2-S-S0-RFILE, and LOG2-S0-SN-RFILE, and unfolding the functions IMPLIES, D2-7A2-5P, D3-7A2-5P, and READ-DN, to: (IMPLIES (AND (LOG2-S0P (STEPN S 5) N 0) (LOG2-STATEP S N) (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 (LESSP 32 OPLEN)) (EQUAL RN 2)) (EQUAL (READ-RN OPLEN 2 (MC-RFILE S)) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LOG2-RFILE (PROVE-LEMMA LOG2-MEM (REWRITE) (IMPLIES (AND (LOG2-STATEP S N) (DISJOINT X K (SUB 32 8 (READ-SP S)) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (LOG2-T N))) K) (READ-MEM X (MC-MEM S) K))) ((USE (LOG2-S-S0)) (DISABLE LOG2-STATEP LOG2-S0P))) This formula can be simplified, using the abbreviations AND, IMPLIES, STEPN-LEMMA, LOG2-T, SP, L, READ-AN, and READ-SP, to the new conjecture: (IMPLIES (AND (IMPLIES (LOG2-STATEP S N) (LOG2-S0P (STEPN S 5) N 0)) (LOG2-STATEP S N) (DISJOINT X K (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 5) (LOG2-T0 N))) K) (READ-MEM X (MC-MEM S) K))), which simplifies, using linear arithmetic, rewriting with SUB-NEG, DISJOINT-10, LOG2-S-S0-MEM, and LOG2-S0-SN, and opening up IMPLIES, PLUS, NEG, INDEX-N, LESSP, READ-SP, L, SP, and READ-AN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LOG2-MEM (PROVE-LEMMA LOG2-LOG (REWRITE) (IMPLIES (NUMBERP I) (EQUAL (LOG2 N I) (PLUS I (LOG 2 N))))) Name the conjecture *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (AND (LESSP 1 N) (p (QUOTIENT N 2) (ADD1 I))) (p N I)) (IMPLIES (NOT (LESSP 1 N)) (p N I))). Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of NUMBERP and EQUAL inform us that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for I. The above induction scheme leads to the following two new conjectures: Case 2. (IMPLIES (AND (LESSP 1 N) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (PLUS (ADD1 I) (LOG 2 (QUOTIENT N 2)))) (NUMBERP I)) (EQUAL (LOG2 N I) (PLUS I (LOG 2 N)))). This simplifies, rewriting with the lemmas SUB1-ADD1, LESSP-OF-1, and SUB1-OF-1, and opening up the definitions of PLUS, LOG2, LOG, EQUAL, NUMBERP, SUB1, and LESSP, to the following four new conjectures: Case 2.4. (IMPLIES (AND (LESSP 1 N) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (ADD1 (PLUS I (LOG 2 (QUOTIENT N 2))))) (NUMBERP I) (EQUAL N 0)) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (PLUS I 0))). But this again simplifies, using linear arithmetic, to: T. Case 2.3. (IMPLIES (AND (LESSP 1 N) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (ADD1 (PLUS I (LOG 2 (QUOTIENT N 2))))) (NUMBERP I) (NOT (NUMBERP N))) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (PLUS I 0))), which again simplifies, unfolding the definition of LESSP, to: T. Case 2.2. (IMPLIES (AND (LESSP 1 N) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (ADD1 (PLUS I (LOG 2 (QUOTIENT N 2))))) (NUMBERP I) (EQUAL N 1)) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (PLUS I 0))), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (LESSP 1 N) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (ADD1 (PLUS I (LOG 2 (QUOTIENT N 2))))) (NUMBERP I) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL N 1))) (EQUAL (LOG2 (QUOTIENT N 2) (ADD1 I)) (PLUS I (ADD1 (LOG 2 (QUOTIENT N 2)))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (LESSP 1 N)) (NUMBERP I)) (EQUAL (LOG2 N I) (PLUS I (LOG 2 N)))), which simplifies, applying LESSP-OF-1, SUB1-OF-1, and CORRECTNESS-OF-CANCEL-EQUAL-PLUS, and opening up the functions LOG2, LOG, EQUAL, NUMBERP, SUB1, LESSP, and FIX, to: (IMPLIES (AND (NOT (LESSP 1 N)) (NUMBERP I) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL N 1))) (EQUAL 0 (ADD1 (LOG 2 (QUOTIENT N 2))))), which again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LOG2-LOG (PROVE-LEMMA LOG2-THM1 (REWRITE) (IMPLIES (LESSP 1 N) (NOT (LESSP N (EXP 2 (LOG2 N 0)))))) WARNING: Note that the proposed lemma LOG2-THM1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula simplifies, rewriting with the lemmas PLUS-0 and LOG2-LOG, to: (IMPLIES (LESSP 1 N) (NOT (LESSP N (EXP 2 (LOG 2 N))))), which we will name *1. Perhaps we can prove it by induction. Three inductions are suggested by terms in the conjecture. They merge into two likely candidate inductions, both of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (OR (ZEROP 2) (EQUAL 2 1)) (p N)) (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (LESSP N 2)) (p N)) (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (NOT (LESSP N 2)) (p (QUOTIENT N 2))) (p N))). Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of OR and ZEROP can be used to prove that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces four new formulas: Case 4. (IMPLIES (AND (OR (ZEROP 2) (EQUAL 2 1)) (LESSP 1 N)) (NOT (LESSP N (EXP 2 (LOG 2 N))))), which simplifies, opening up the definitions of ZEROP, EQUAL, and OR, to: T. Case 3. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (LESSP N 2) (LESSP 1 N)) (NOT (LESSP N (EXP 2 (LOG 2 N))))), which simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (NOT (LESSP N 2)) (NOT (LESSP 1 (QUOTIENT N 2))) (LESSP 1 N)) (NOT (LESSP N (EXP 2 (LOG 2 N))))), which simplifies, applying LESSP-OF-1, SUB1-OF-1, and SUB1-ADD1, and expanding ZEROP, EQUAL, OR, SUB1, NUMBERP, LESSP, LOG, and EXP, to the new conjecture: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL N 1)) (NOT (LESSP 1 (QUOTIENT N 2))) (LESSP 1 N)) (NOT (LESSP N (TIMES 2 (EXP 2 (LOG 2 (QUOTIENT N 2))))))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace N by (PLUS Z (TIMES 2 X)) to eliminate (QUOTIENT N 2) and (REMAINDER N 2). We rely upon REMAINDER-LESSP, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to restrict the new variables. We thus obtain the following three new conjectures: Case 2.3. (IMPLIES (AND (EQUAL 2 0) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL N 1)) (NOT (LESSP 1 (QUOTIENT N 2))) (LESSP 1 N)) (NOT (LESSP N (TIMES 2 (EXP 2 (LOG 2 (QUOTIENT N 2))))))). However this further simplifies, using linear arithmetic, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP 2)) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (EQUAL N 1)) (NOT (LESSP 1 (QUOTIENT N 2))) (LESSP 1 N)) (NOT (LESSP N (TIMES 2 (EXP 2 (LOG 2 (QUOTIENT N 2))))))), which further simplifies, obviously, to: T. Case 2.1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z 2) (NOT (ZEROP 2))) (NOT (EQUAL 2 0)) (NOT (EQUAL (PLUS Z (TIMES 2 X)) 0)) (NOT (EQUAL (PLUS Z (TIMES 2 X)) 1)) (NOT (LESSP 1 X)) (LESSP 1 (PLUS Z (TIMES 2 X)))) (NOT (LESSP (PLUS Z (TIMES 2 X)) (TIMES 2 (EXP 2 (LOG 2 X)))))). This further simplifies, using linear arithmetic, applying LESSP-OF-1, SUB1-OF-1, PLUS-0, TIMES-EQUAL-0, TIMES-EQUAL-1, TIMES-LESSP, DIFFERENCE-0, CORRECTNESS-OF-CANCEL-LESSP-TIMES, PLUS-ADD1, ADD1-EQUAL, SUB1-ADD1, and TIMES2-ADD1-LESSP-CANCEL, and opening up the definitions of SUB1, NUMBERP, EQUAL, LESSP, ZEROP, NOT, LOG, QUOTIENT, ADD1, FIX, and AND, to the following four new formulas: Case 2.1.4. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL Z 0) (NOT (EQUAL X 0)) (NOT (LESSP 1 X)) (NOT (EQUAL X 1))) (NOT (LESSP X (EXP 2 1)))). This again simplifies, using linear arithmetic, to: T. Case 2.1.3. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL Z 0) (NOT (EQUAL X 0)) (NOT (LESSP 1 X)) (EQUAL X 1)) (NOT (LESSP X (EXP 2 0)))), which again simplifies, expanding the functions NUMBERP, EQUAL, LESSP, and EXP, to: T. Case 2.1.2. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL Z 1) (NOT (EQUAL X 0)) (NOT (LESSP 1 X)) (NOT (EQUAL X 1))) (NOT (LESSP X (EXP 2 1)))), which again simplifies, using linear arithmetic, to: T. Case 2.1.1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL Z 1) (NOT (EQUAL X 0)) (NOT (LESSP 1 X)) (EQUAL X 1)) (NOT (LESSP X (EXP 2 0)))), which again simplifies, expanding the functions NUMBERP, EQUAL, LESSP, and EXP, to: T. Case 1. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (NOT (LESSP N 2)) (NOT (LESSP (QUOTIENT N 2) (EXP 2 (LOG 2 (QUOTIENT N 2))))) (LESSP 1 N)) (NOT (LESSP N (EXP 2 (LOG 2 N))))), which simplifies, rewriting with the lemmas LESSP-OF-1, SUB1-OF-1, QUOTIENT-TIMES-LESSP, and SUB1-ADD1, and unfolding ZEROP, EQUAL, OR, SUB1, NUMBERP, LESSP, LOG, and EXP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-THM1 (PROVE-LEMMA LOG2-THM2 (REWRITE) (LESSP N (EXP 2 (ADD1 (LOG2 N 0))))) WARNING: Note that the proposed lemma LOG2-THM2 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This simplifies, rewriting with PLUS-0, LOG2-LOG, and SUB1-ADD1, and expanding EXP, to the conjecture: (LESSP N (TIMES 2 (EXP 2 (LOG 2 N)))). Give the above formula the name *1. Perhaps we can prove it by induction. There are two plausible inductions, both of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (OR (ZEROP 2) (EQUAL 2 1)) (p N)) (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (LESSP N 2)) (p N)) (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (NOT (LESSP N 2)) (p (QUOTIENT N 2))) (p N))). Linear arithmetic, the lemmas QUOTIENT-TIMES-LESSP, TIMES-LESSP, COUNT-NOT-LESSP, and COUNT-NUMBERP, and the definitions of OR and ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following three new conjectures: Case 3. (IMPLIES (OR (ZEROP 2) (EQUAL 2 1)) (LESSP N (TIMES 2 (EXP 2 (LOG 2 N))))). This simplifies, opening up the functions ZEROP, EQUAL, and OR, to: T. Case 2. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (LESSP N 2)) (LESSP N (TIMES 2 (EXP 2 (LOG 2 N))))). This simplifies, using linear arithmetic, rewriting with the lemma EXP-OF-2-0, and opening up the function EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (OR (ZEROP 2) (EQUAL 2 1))) (NOT (LESSP N 2)) (LESSP (QUOTIENT N 2) (TIMES 2 (EXP 2 (LOG 2 (QUOTIENT N 2)))))) (LESSP N (TIMES 2 (EXP 2 (LOG 2 N))))). This simplifies, rewriting with LESSP-OF-1, SUB1-OF-1, QUOTIENT-TIMES-LESSP, and SUB1-ADD1, and expanding the functions ZEROP, EQUAL, OR, SUB1, NUMBERP, LESSP, LOG, and EXP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] LOG2-THM2