(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 ISQRT-CODE NIL '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 32 1 36 46 255 252 78 94 78 117)) From the definition we can conclude that (LISTP (ISQRT-CODE)) is a theorem. [ 0.0 0.0 0.0 ] ISQRT-CODE (PROVE-LEMMA MEAN-LESSP-1 (REWRITE) (EQUAL (LESSP (QUOTIENT (PLUS B A) 2) B) (LESSP A B)) ((DISABLE QUOTIENT-TIMES-LESSP))) WARNING: the previously added lemma, MEAN-LESSP, could be applied whenever the newly proposed MEAN-LESSP-1 could! WARNING: the previously added lemma, QUOTIENT-TIMES-LESSP, could be applied whenever the newly proposed MEAN-LESSP-1 could! This formula can be simplified, using the abbreviation MEAN-LESSP, to the new conjecture: (EQUAL (LESSP A B) (LESSP A B)), which simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] MEAN-LESSP-1 (DEFN ISQRT1 (I J) (IF (ZEROP J) (FIX I) (IF (LESSP (QUOTIENT I J) J) (ISQRT1 I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (FIX J)))) The lemmas MEAN-LESSP-1, COUNT-NUMBERP, and QUOTIENT-TIMES-LESSP and the definition of ZEROP establish that the measure (COUNT J) decreases according to the well-founded relation LESSP in each recursive call. Hence, ISQRT1 is accepted under the definitional principle. Note that (NUMBERP (ISQRT1 I J)) is a theorem. [ 0.0 0.1 0.0 ] ISQRT1 (DEFN ISQRT (I) (ISQRT1 I (QUOTIENT I 2))) Note that (NUMBERP (ISQRT I)) is a theorem. [ 0.0 0.0 0.0 ] ISQRT (DEFN ISQRT1-T (I J) (IF (ZEROP J) 0 (IF (LESSP (QUOTIENT I J) J) (SPLUS 10 (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))) 8))) The lemmas MEAN-LESSP-1, COUNT-NUMBERP, and QUOTIENT-TIMES-LESSP and the definition of ZEROP can be used to show that the measure (COUNT J) decreases according to the well-founded relation LESSP in each recursive call. Hence, ISQRT1-T is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (ISQRT1-T I J)) is a theorem. [ 0.0 0.1 0.0 ] ISQRT1-T (DEFN ISQRT-T (I) (SPLUS 8 (ISQRT1-T I (QUOTIENT I 2)))) Observe that (NUMBERP (ISQRT-T I)) is a theorem. [ 0.0 0.0 0.0 ] ISQRT-T (ENABLE IPLUS) [ 0.0 0.0 0.0 ] IPLUS-ON (ENABLE INTEGERP) [ 0.0 0.0 0.0 ] INTEGERP-ON (ENABLE IQUOTIENT) [ 0.0 0.0 0.0 ] IQUOTIENT-ON (ENABLE ILESSP) [ 0.0 0.0 0.0 ] ILESSP-ON (DISABLE REMAINDER) [ 0.0 0.0 0.0 ] REMAINDER-OFF (DISABLE QUOTIENT) [ 0.0 0.0 0.0 ] QUOTIENT-OFF (PROVE-LEMMA ISQRT-NO-OVERFLOW (REWRITE) (IMPLIES (AND (INT-RANGEP (TIMES 2 J) N) (LESSP (QUOTIENT I J) J)) (INT-RANGEP (PLUS J (QUOTIENT I J)) N))) This simplifies, using linear arithmetic, rewriting with QUOTIENT-TIMES-LESSP and ABS-LESSP-INT-RANGEP, and expanding the functions EQUAL, ABS, and NEGP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ISQRT-NO-OVERFLOW (PROVE-LEMMA J-NONZEROP (REWRITE) (IMPLIES (AND (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0)))) This formula simplifies, rewriting with PLUS-EQUAL-0, LESSP-OF-1, SUB1-OF-1, and QUOTIENT-EQUAL-0, and opening up the functions EQUAL, LESSP, NUMBERP, and SUB1, to the new formula: (IMPLIES (AND (LESSP 1 I) (NOT (EQUAL J 0)) (NUMBERP J)) (NOT (EQUAL (PLUS J (QUOTIENT I J)) 1))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by (PLUS Z (TIMES J X)) to eliminate (QUOTIENT I J) and (REMAINDER I J). 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 two new goals: Case 2. (IMPLIES (AND (NOT (NUMBERP I)) (LESSP 1 I) (NOT (EQUAL J 0)) (NUMBERP J)) (NOT (EQUAL (PLUS J (QUOTIENT I J)) 1))). This further simplifies, opening up the function LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z J) (NOT (ZEROP J))) (LESSP 1 (PLUS Z (TIMES J X))) (NOT (EQUAL J 0)) (NUMBERP J)) (NOT (EQUAL (PLUS J X) 1))), which further simplifies, opening up the functions ZEROP and NOT, to: (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (LESSP Z J) (LESSP 1 (PLUS Z (TIMES J X))) (NOT (EQUAL J 0)) (NUMBERP J)) (NOT (EQUAL (PLUS J X) 1))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (IMPLIES (AND (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))). We gave this the name *1 above. Perhaps we can prove it by induction. There are three plausible inductions. They merge into two likely candidate inductions, both of which are unflawed. However, one of these is more likely than the other. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL J 0) (NOT (NUMBERP J))) (p J I)) (IMPLIES (AND (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (p J I)) (IMPLIES (AND (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (p (SUB1 J) I)) (p J I))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT J) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following four new formulas: Case 4. (IMPLIES (AND (OR (EQUAL J 0) (NOT (NUMBERP J))) (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))). This simplifies, expanding the functions NOT, OR, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (OR (EQUAL 0 0) (NOT (NUMBERP 0))) (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))). This simplifies, applying QUOTIENT-ADD1, and opening up the definitions of NOT, OR, EQUAL, NUMBERP, LESSP, PLUS, and SUB1, to two new conjectures: Case 3.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP 1 I) (NOT (EQUAL (REMAINDER (PLUS (SUB1 J) (QUOTIENT I J)) 2) 1))) (NOT (EQUAL (QUOTIENT (PLUS (SUB1 J) (QUOTIENT I J)) 2) 0))), which again simplifies, applying SUB1-OF-1, LESSP-OF-1, QUOTIENT-EQUAL-0, and PLUS-EQUAL-0, and unfolding the definitions of EQUAL, NUMBERP, SUB1, and LESSP, to the following three new goals: Case 3.2.3. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP 1 I) (NOT (EQUAL (REMAINDER (PLUS (SUB1 J) (QUOTIENT I J)) 2) 1)) (EQUAL J 1)) (NUMBERP I)). However this again simplifies, unfolding the functions EQUAL, NUMBERP, and LESSP, to: T. Case 3.2.2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP 1 I) (NOT (EQUAL (REMAINDER (PLUS (SUB1 J) (QUOTIENT I J)) 2) 1)) (EQUAL J 1)) (NOT (EQUAL I 0))), which again simplifies, using linear arithmetic, to: T. Case 3.2.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP 1 I) (NOT (EQUAL (REMAINDER (PLUS (SUB1 J) (QUOTIENT I J)) 2) 1))) (NOT (EQUAL (PLUS (SUB1 J) (QUOTIENT I J)) 1))), which again simplifies, opening up REMAINDER and EQUAL, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP 1 I) (EQUAL (REMAINDER (PLUS (SUB1 J) (QUOTIENT I J)) 2) 1)) (NOT (EQUAL (ADD1 (QUOTIENT (PLUS (SUB1 J) (QUOTIENT I J)) 2)) 0))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 J))) (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))), which simplifies, using linear arithmetic, to two new formulas: Case 2.2. (IMPLIES (AND (NOT (NUMBERP J)) (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 J))) (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))), which again simplifies, unfolding NOT and OR, to: T. Case 2.1. (IMPLIES (AND (NUMBERP J) (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (LESSP 0 (SUB1 1))) (LESSP 1 I) (LESSP 0 1)) (NOT (EQUAL (QUOTIENT (PLUS 1 (QUOTIENT I 1)) 2) 0))), which again simplifies, opening up the definitions of EQUAL, NUMBERP, NOT, and OR, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL J 0) (NOT (NUMBERP J)))) (NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0)))) (NOT (EQUAL (QUOTIENT (PLUS (SUB1 J) (QUOTIENT I (SUB1 J))) 2) 0)) (LESSP 1 I) (LESSP 0 J)) (NOT (EQUAL (QUOTIENT (PLUS J (QUOTIENT I J)) 2) 0))), which simplifies, opening up the functions NOT, OR, EQUAL, and NUMBERP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.1 ] J-NONZEROP (PROVE-LEMMA J-INT-RANGEP (REWRITE) (IMPLIES (AND (INT-RANGEP (TIMES 2 J) N) (LESSP (QUOTIENT I J) J)) (INT-RANGEP (TIMES 2 (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) N))) This formula simplifies, applying QUOTIENT-TIMES-LESSP, MEAN-LESSP-1, CORRECTNESS-OF-CANCEL-LESSP-TIMES, and ABS-LESSP-INT-RANGEP, and expanding the functions EQUAL, AND, FIX, NOT, ZEROP, ABS, and NEGP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] J-INT-RANGEP (DEFN ISQRT-INDUCT (S I J) (IF (ZEROP J) T (IF (LESSP (QUOTIENT I J) J) (ISQRT-INDUCT (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) T))) The lemmas MEAN-LESSP-1, COUNT-NUMBERP, and QUOTIENT-TIMES-LESSP and the definition of ZEROP inform us that the measure (COUNT J) decreases according to the well-founded relation LESSP in each recursive call. Hence, ISQRT-INDUCT is accepted under the principle of definition. Note that: (TRUEP (ISQRT-INDUCT S I J)) is a theorem. [ 0.0 0.0 0.0 ] ISQRT-INDUCT (DEFN ISQRT-STATEP (S I) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (ISQRT-CODE)) (RAM-ADDRP (SUB 32 8 (READ-SP S)) (MC-MEM S) 16) (EQUAL I (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (ILESSP 1 I))) From the definition we can conclude that: (OR (FALSEP (ISQRT-STATEP S I)) (TRUEP (ISQRT-STATEP S I))) is a theorem. [ 0.0 0.0 0.0 ] ISQRT-STATEP (DEFN ISQRT-S0P (S I J) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) (ISQRT-CODE)) (RAM-ADDRP (SUB 32 4 (READ-AN 32 6 S)) (MC-MEM S) 16) (EQUAL I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J))) Observe that (OR (FALSEP (ISQRT-S0P S I J)) (TRUEP (ISQRT-S0P S I J))) is a theorem. [ 0.0 0.0 0.0 ] ISQRT-S0P (PROVE-LEMMA INITIAL-J-INT-RANGEP (REWRITE) (IMPLIES (INT-RANGEP I N) (INT-RANGEP (TIMES 2 (QUOTIENT I 2)) N)) ((ENABLE INT-RANGEP))) This conjecture simplifies, applying QUOTIENT-EQUAL-0, TIMES-ZERO, and INT-RANGEP-OF-0, and expanding the functions FIX-INT, NEGP, NEGATIVE-GUTS, INTEGERP, INT-RANGEP, OR, ZEROP, QUOTIENT, and TIMES, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NEGATIVEP I)) (LESSP I (EXP 2 (SUB1 N)))) (LESSP (TIMES 2 (QUOTIENT I 2)) (EXP 2 (SUB1 N)))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace I by (PLUS Z (TIMES 2 X)) to eliminate (QUOTIENT I 2) and (REMAINDER I 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 constrain the new variables. This generates four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP I)) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NEGATIVEP I)) (LESSP I (EXP 2 (SUB1 N)))) (LESSP (TIMES 2 (QUOTIENT I 2)) (EXP 2 (SUB1 N)))), which further simplifies, using linear arithmetic, applying QUOTIENT-LEQ and EXP-OF-2-0, and opening up the function EQUAL, to: T. Case 3. (IMPLIES (AND (EQUAL 2 0) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NEGATIVEP I)) (LESSP I (EXP 2 (SUB1 N)))) (LESSP (TIMES 2 (QUOTIENT I 2)) (EXP 2 (SUB1 N)))). However this further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP 2)) (NOT (EQUAL N 0)) (NUMBERP N) (NOT (NEGATIVEP I)) (LESSP I (EXP 2 (SUB1 N)))) (LESSP (TIMES 2 (QUOTIENT I 2)) (EXP 2 (SUB1 N)))), which further simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z 2) (NOT (ZEROP 2))) (NOT (EQUAL 2 0)) (NOT (EQUAL N 0)) (NUMBERP N) (LESSP (PLUS Z (TIMES 2 X)) (EXP 2 (SUB1 N)))) (LESSP (TIMES 2 X) (EXP 2 (SUB1 N)))). This further simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] INITIAL-J-INT-RANGEP (PROVE-LEMMA ISQRT-S-S0 (REWRITE) (IMPLIES (ISQRT-STATEP S I) (AND (ISQRT-S0P (STEPN S 8) I (QUOTIENT I 2)) (EQUAL (LINKED-RTS-ADDR (STEPN S 8)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 8)) (READ-AN 32 6 S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (SUB 32 4 (READ-SP S))) (EQUAL (RN-SAVED (STEPN S 8)) (READ-DN 32 2 S))))) WARNING: Note that the rewrite rule ISQRT-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol ISQRT-S0P. WARNING: Note that the rewrite rule ISQRT-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that ISQRT-S-S0 contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). WARNING: Note that the rewrite rule ISQRT-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that ISQRT-S-S0 contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). WARNING: Note that ISQRT-S-S0 contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). WARNING: Note that the rewrite rule ISQRT-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol RN-SAVED. WARNING: Note that ISQRT-S-S0 contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). WARNING: Note that the proposed lemma ISQRT-S-S0 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 ISQRT-CODE, ISQRT-STATEP, IMPLIES, READ-DN, SP, L, READ-SP, and READ-AN, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (ILESSP 1 I)) (AND (ISQRT-S0P (STEPN S 8) I (QUOTIENT I 2)) (EQUAL (LINKED-RTS-ADDR (STEPN S 8)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 8)) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)))) (EQUAL (RN-SAVED (STEPN S 8)) (READ-RN 32 2 (MC-RFILE S))))). This simplifies, applying the lemmas SUB-NEG, NAT-TO-INT-INTEGERP, READ-MEM-NAT-RANGEP, NEGATIVEP-GUTS0, 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, BGE-V0, MOVE-BMI, SET-CVZNX-N, MOVE-N-BITP, SET-CVZNX-V, STEPN-REWRITER0, STEPN-REWRITER, QUOTIENT-EQUAL-0, LESSP-OF-1, SUB1-OF-1, INITIAL-J-INT-RANGEP, NAT-TO-INT-RANGEP, ASR-NAT-RANGEP, ASR-INT, 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, MC-PC-RANGEP, DISJOINT-DEDUCTION1, HEAD-READ-RN, and READ-WRITE-MEM2, and unfolding the functions PLUS, NEG, TIMES, IREAD-MEM, NEGATIVE-GUTS, LESSP, NEGP, ILESSP, 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, 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, HEAD, BCC-RA-SR, COND-FIELD, BCC-GROUP, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, TST-ADDR-MODEP, TST-INS, B-NOT, FIX-BIT, BRANCH-CC, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, SUB1, EXP, IQUOTIENT, IREAD-DN, ISQRT-CODE, ISQRT-S0P, LINKED-RTS-ADDR, RTS-ADDR, UINT-RANGEP, LINKED-A6, RN-SAVED, and AND, to the following two new formulas: Case 2. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967288) (MC-MEM S) 16) (NOT (NEGATIVEP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (LESSP 1 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) 0))). This again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 32 1 36 46 255 252 78 94 78 117)) (RAM-ADDRP (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4294967288) (MC-MEM S) 16) (NOT (NEGATIVEP (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (LESSP 1 (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32))) (NOT (EQUAL (NAT-TO-INT (READ-MEM (ADD 32 (READ-RN 32 15 (MC-RFILE S)) 4) (MC-MEM S) 4) 32) 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.9 0.0 ] ISQRT-S-S0 (PROVE-LEMMA ISQRT-S-S0-RFILE (REWRITE) (IMPLIES (AND (ISQRT-STATEP S I) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 8))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that ISQRT-S-S0-RFILE contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). This formula can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, SP, L, READ-AN, READ-SP, ISQRT-CODE, ISQRT-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) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (ILESSP 1 I) (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 8))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, rewriting with SUB-NEG, NAT-TO-INT-INTEGERP, READ-MEM-NAT-RANGEP, NEGATIVEP-GUTS0, 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, BGE-V0, MOVE-BMI, SET-CVZNX-N, MOVE-N-BITP, SET-CVZNX-V, STEPN-REWRITER0, and STEPN-REWRITER, and expanding PLUS, NEG, TIMES, IREAD-MEM, NEGATIVE-GUTS, LESSP, NEGP, ILESSP, 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, 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, HEAD, BCC-RA-SR, COND-FIELD, BCC-GROUP, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, TST-ADDR-MODEP, TST-INS, B-NOT, FIX-BIT, BRANCH-CC, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, and S&R-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ISQRT-S-S0-RFILE (PROVE-LEMMA ISQRT-S-S0-MEM (REWRITE) (IMPLIES (AND (ISQRT-STATEP S I) (DISJOINT X K (SUB 32 8 (READ-SP S)) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 8)) K) (READ-MEM X (MC-MEM S) K)))) WARNING: Note that ISQRT-S-S0-MEM contains the free variable I which will be chosen by instantiating the hypothesis (ISQRT-STATEP S I). This conjecture can be simplified, using the abbreviations ISQRT-CODE, ISQRT-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) 50) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (ILESSP 1 I) (DISJOINT X K (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 8)) K) (READ-MEM X (MC-MEM S) K))). This simplifies, using linear arithmetic, rewriting with SUB-NEG, NAT-TO-INT-INTEGERP, READ-MEM-NAT-RANGEP, NEGATIVEP-GUTS0, 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, BGE-V0, MOVE-BMI, SET-CVZNX-N, MOVE-N-BITP, SET-CVZNX-V, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and opening up the functions PLUS, NEG, TIMES, IREAD-MEM, NEGATIVE-GUTS, LESSP, NEGP, ILESSP, 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, 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, HEAD, BCC-RA-SR, COND-FIELD, BCC-GROUP, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, TST-ADDR-MODEP, TST-INS, B-NOT, FIX-BIT, BRANCH-CC, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, and S&R-GROUP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] ISQRT-S-S0-MEM (PROVE-LEMMA ISQRT-S0-SN (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (NOT (LESSP (QUOTIENT I J) J))) (AND (EQUAL (MC-STATUS (STEPN S 8)) 'RUNNING) (EQUAL (MC-PC (STEPN S 8)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 8)) J) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 8))) (ADD 32 (READ-AN 32 6 S) 8))))) WARNING: Note that ISQRT-S0-SN contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that ISQRT-S0-SN contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the rewrite rule ISQRT-S0-SN will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that ISQRT-S0-SN contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that ISQRT-S0-SN contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that ISQRT-S0-SN contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the proposed lemma ISQRT-S0-SN 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 NOT, ISQRT-CODE, ISQRT-S0P, AND, IMPLIES, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (NOT (LESSP (QUOTIENT I J) J))) (AND (EQUAL (MC-STATUS (STEPN S 8)) 'RUNNING) (EQUAL (MC-PC (STEPN S 8)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 8)) J) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 8))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 8))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)))). This simplifies, applying SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, STEPN-REWRITER0, STEPN-REWRITER, and READ-MEM-NAT-RANGEP, and opening up NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, TIMES, LINKED-RTS-ADDR, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.8 0.0 ] ISQRT-S0-SN (PROVE-LEMMA ISQRT-S0-SN-D2 (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (NOT (LESSP (QUOTIENT I J) J)) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S 8))) (HEAD (RN-SAVED S) OPLEN)))) WARNING: Note that ISQRT-S0-SN-D2 contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). This formula can be simplified, using the abbreviations NOT, READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (NOT (LESSP (QUOTIENT I J) J)) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S 8))) (HEAD (RN-SAVED S) OPLEN))), which simplifies, rewriting with SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, STEPN-REWRITER0, and STEPN-REWRITER, and opening up NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, and RN-SAVED, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ISQRT-S0-SN-D2 (PROVE-LEMMA ISQRT-S0-SN-RFILE (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (NOT (LESSP (QUOTIENT I J) J)) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 8))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that ISQRT-S0-SN-RFILE contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). This formula can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, NOT, READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (NOT (LESSP (QUOTIENT I J) J)) (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 8))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, applying SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the definitions of NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, and RTS-INS, to: T. Q.E.D. [ 0.0 0.1 0.1 ] ISQRT-S0-SN-RFILE (PROVE-LEMMA ISQRT1-S0-SN-MEM (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (NOT (LESSP (QUOTIENT I J) J))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 8)) K) (READ-MEM X (MC-MEM S) K)))) WARNING: Note that ISQRT1-S0-SN-MEM contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). This conjecture can be simplified, using the abbreviations NOT, READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to the conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (NOT (LESSP (QUOTIENT I J) J))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 8)) K) (READ-MEM X (MC-MEM S) K))). This simplifies, rewriting with SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, READ-MEMP-RAM3, READ-MEMP-RAM2, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OP-SZ, W, READ-AN, ADDR-DISP, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, and RTS-INS, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ISQRT1-S0-SN-MEM (PROVE-LEMMA ISQRT-S0P-J_NONZEROP (REWRITE) (IMPLIES (ISQRT-S0P S I J) (AND (NOT (EQUAL J 0)) (NUMBERP J)))) WARNING: Note that ISQRT-S0P-J_NONZEROP contains the free variables I and S which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that ISQRT-S0P-J_NONZEROP contains the free variables I and S which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the proposed lemma ISQRT-S0P-J_NONZEROP is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and two replacement rules. This formula can be simplified, using the abbreviations READ-AN, ISQRT-CODE, ISQRT-S0P, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J)) (AND (NOT (EQUAL J 0)) (NUMBERP J))), which simplifies, rewriting with SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, and NEGATIVEP-GUTS0, and expanding the definitions of NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, NOT, and AND, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ISQRT-S0P-J_NONZEROP (PROVE-LEMMA ISQRT-S0-S0 (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (LESSP (QUOTIENT I J) J)) (AND (ISQRT-S0P (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 10))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 10)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 10)) (LINKED-RTS-ADDR S)) (EQUAL (RN-SAVED (STEPN S 10)) (RN-SAVED S)))) ((DISABLE QUOTIENT-EQUAL-0 QUOTIENT-TIMES-LESSP))) WARNING: Note that the rewrite rule ISQRT-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol ISQRT-S0P. WARNING: Note that ISQRT-S0-S0 contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the rewrite rule ISQRT-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that ISQRT-S0-S0 contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the rewrite rule ISQRT-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that ISQRT-S0-S0 contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the rewrite rule ISQRT-S0-S0 will be stored so as to apply only to terms with the nonrecursive function symbol RN-SAVED. WARNING: Note that ISQRT-S0-S0 contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). WARNING: Note that the proposed lemma ISQRT-S0-S0 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 READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (LESSP (QUOTIENT I J) J)) (AND (ISQRT-S0P (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 10))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 10)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 10)) (LINKED-RTS-ADDR S)) (EQUAL (RN-SAVED (STEPN S 10)) (RN-SAVED S)))). This simplifies, applying the lemmas SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, ADD-C-BITP, BGE-V0, MOVE-BMI, ADD-INT, ISQRT-NO-OVERFLOW, MOVE-N-BITP, ADD-0, MC-PC-RANGEP, STEPN-REWRITER0, STEPN-REWRITER, INITIAL-J-INT-RANGEP, ASR-NAT-RANGEP, ASR-INT, RAM-ADDRP-3, ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and unfolding the functions NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, ADD-CVZNX, ADD-EFFECT, ADD-GROUP, TST-SUBGROUP, TST-ADDR-MODEP, TST-INS, B-NOT, IPLUS, FIX-BIT, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, S&R-GROUP, EXP, READ-AN, ISQRT-CODE, ISQRT-S0P, LINKED-A6, LINKED-RTS-ADDR, RN-SAVED, and AND, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967266) (MC-MEM S) 50) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967266) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 (TIMES 2 (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NOT (NEGATIVEP (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32))) (LESSP 1 (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32)) (NOT (NEGATIVEP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32))) (NOT (EQUAL (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) 0)) (LESSP (QUOTIENT (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32))) (NOT (EQUAL (QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) (QUOTIENT (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32))) 2) 0))), which again simplifies, using linear arithmetic, applying QUOTIENT-LESSP-LINEAR and J-NONZEROP, and expanding LESSP, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (ADD 32 (MC-PC S) 4294967266) (MC-MEM S) 50) (MCODE-ADDRP (ADD 32 (MC-PC S) 4294967266) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 (TIMES 2 (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) 32) (NOT (NEGATIVEP (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32))) (LESSP 1 (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32)) (NOT (NEGATIVEP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32))) (NOT (EQUAL (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) 0)) (LESSP (QUOTIENT (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)) (NOT (NUMBERP (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32)))) (NOT (EQUAL (QUOTIENT (PLUS (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32) (QUOTIENT (NAT-TO-INT (READ-RN 32 2 (MC-RFILE S)) 32) (NAT-TO-INT (READ-RN 32 1 (MC-RFILE S)) 32))) 2) 0))), which again simplifies, trivially, to: T. Q.E.D. [ 0.0 0.7 0.0 ] ISQRT-S0-S0 (PROVE-LEMMA ISQRT-S0-S0-RFILE (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (LESSP (QUOTIENT I J) J) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 10))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that ISQRT-S0-S0-RFILE contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). This formula can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (LESSP (QUOTIENT I J) J) (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 10))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, applying SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, ADD-C-BITP, BGE-V0, MOVE-BMI, ADD-INT, ISQRT-NO-OVERFLOW, MOVE-N-BITP, ADD-0, MC-PC-RANGEP, STEPN-REWRITER0, and STEPN-REWRITER, and expanding NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, ADD-CVZNX, ADD-EFFECT, ADD-GROUP, TST-SUBGROUP, TST-ADDR-MODEP, TST-INS, B-NOT, IPLUS, FIX-BIT, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, and S&R-GROUP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] ISQRT-S0-S0-RFILE (PROVE-LEMMA ISQRT-S0-S0-MEM (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (LESSP (QUOTIENT I J) J)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 10)) K) (READ-MEM X (MC-MEM S) K)))) WARNING: Note that ISQRT-S0-S0-MEM contains the free variables J and I which will be chosen by instantiating the hypothesis (ISQRT-S0P S I J). This conjecture can be simplified, using the abbreviations READ-AN, ISQRT-CODE, ISQRT-S0P, AND, and IMPLIES, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) 50) (MCODE-ADDRP (SUB 32 30 (MC-PC S)) (MC-MEM S) '(78 86 0 0 47 2 34 46 0 8 36 1 96 8 32 2 76 65 8 0 210 128 74 129 108 2 82 129 226 129 32 2 76 65 8 0 178 128 110 230 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 I (IREAD-DN 32 2 S)) (EQUAL J (IREAD-DN 32 1 S)) (INT-RANGEP (TIMES 2 J) 32) (ILESSP 1 I) (ILESSP 0 J) (LESSP (QUOTIENT I J) J)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 10)) K) (READ-MEM X (MC-MEM S) K))). This simplifies, applying SUB-NEG, NAT-TO-INT-INTEGERP, READ-RN-NAT-RANGEP, NEGATIVEP-GUTS0, QUOTIENT-TIMES-LESSP, CDR-CONS, CAR-CONS, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, MC-CCR-REWRITE, MC-CCR-RANGEP, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, HEAD-READ-RN, SET-SET-CVZNX1, WRITE-WRITE-RN, SET-CVZNX-X, DIVS_3232-OVERFLOW, READ-WRITE-RN, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, IQUOT-NAT-RANGEP, HEAD-LEMMA, BITP-FIX-BIT, FIX-BIT-BITP, SUB-BGT, IQUOT-INT, NAT-TO-INT-RANGEP, QUOTIENT-INT-RANGEP, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-Z, SUB-Z-BITP, SET-CVZNX-V, SUB-V-BITP, ADD-C-BITP, BGE-V0, MOVE-BMI, ADD-INT, ISQRT-NO-OVERFLOW, MOVE-N-BITP, ADD-0, MC-PC-RANGEP, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, NEGATIVE-GUTS, NEGP, ILESSP, LESSP, EQUAL, EXECUTE-INS, OPCODE-FIELD, MOVE-INS, MOVE-ADDR-MODEP, CAR, EFFEC-ADDR, CONS, DN-DIRECT, S_RN, S_MODE, MC-INSTATE, MC-HALTP, CDR, OPERAND, MAPPING, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, INDEX-N, STEPI, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, UPDATE-CCR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, NUMBERP, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, B0P, BITN, MISC-GROUP, ADD, EVENP, OP-LEN, CMP-INS, CMP-ADDR-MODEP, CMP-CVZNX, Q, CMP-GROUP, B, HEAD, BCC-RA-SR, IQUOTIENT, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, OPMODE-FIELD, ADD-INS1, ADD-ADDR-MODEP1, ADD-CVZNX, ADD-EFFECT, ADD-GROUP, TST-SUBGROUP, TST-ADDR-MODEP, TST-INS, B-NOT, IPLUS, FIX-BIT, REGISTER-SHIFT-ROTATE, ASR-EFFECT, ASR-X, ASR-CVZNX, SR-CNT, I-DATA, REGISTER-ASR-INS, and S&R-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ISQRT-S0-S0-MEM (DISABLE ISQRT-STATEP) [ 0.0 0.0 0.0 ] ISQRT-STATEP-OFF (DISABLE ISQRT-S0P) [ 0.0 0.0 0.0 ] ISQRT-S0P-OFF (PROVE-LEMMA ISQRT1-CORRECTNESS (REWRITE) (IMPLIES (ISQRT-S0P S I J) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT1-T I J))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT1-T I J))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT1-T I J))) (ISQRT1 I J)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT1-T I J))) K) (READ-MEM X (MC-MEM S) K)))) ((INDUCT (ISQRT-INDUCT S I J)) (DISABLE QUOTIENT-TIMES-LESSP LINKED-RTS-ADDR LINKED-A6))) WARNING: Note that the rewrite rule ISQRT1-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma ISQRT1-CORRECTNESS is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, AND, and READ-AN, to the following three new conjectures: Case 3. (IMPLIES (AND (ZEROP J) (ISQRT-S0P S I J)) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT1-T I J))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT1-T I J))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT1-T I J))) (ISQRT1 I J)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT1-T I J))) K) (READ-MEM X (MC-MEM S) K)))). This simplifies, applying ISQRT-S0P-J_NONZEROP, and expanding ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (QUOTIENT I J) J) (IMPLIES (ISQRT-S0P (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)))) (LINKED-RTS-ADDR (STEPN S 10))) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)))) (ISQRT1 I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))))) (LINKED-A6 (STEPN S 10))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN S 10))) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)))) K) (READ-MEM X (MC-MEM (STEPN S 10)) K)))) (ISQRT-S0P S I J)) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT1-T I J))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT1-T I J))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT1-T I J))) (ISQRT1 I J)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT1-T I J))) K) (READ-MEM X (MC-MEM S) K)))), which simplifies, rewriting with ISQRT-S0P-J_NONZEROP, ISQRT-S0-S0, ISQRT-S0-S0-MEM, and STEPN-LEMMA, and opening up the definitions of READ-DN, IREAD-DN, PLUS, AND, IMPLIES, ISQRT1-T, EQUAL, and ISQRT1, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (QUOTIENT I J) J)) (ISQRT-S0P S I J)) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT1-T I J))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT1-T I J))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT1-T I J))) (ISQRT1 I J)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT1-T I J))) K) (READ-MEM X (MC-MEM S) K)))). This simplifies, applying ISQRT-S0P-J_NONZEROP, ISQRT-S0-SN, and ISQRT1-S0-SN-MEM, and unfolding the functions ISQRT1-T, EQUAL, ISQRT1, PLUS, READ-AN, and AND, to: T. Q.E.D. [ 0.0 0.2 0.0 ] ISQRT1-CORRECTNESS (PROVE-LEMMA ISQRT1-D2 (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (HEAD (RN-SAVED S) OPLEN))) ((INDUCT (ISQRT-INDUCT S I J)) (DISABLE RN-SAVED))) This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to the following three new goals: Case 3. (IMPLIES (AND (ZEROP J) (ISQRT-S0P S I J) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (HEAD (RN-SAVED S) OPLEN))). This simplifies, appealing to the lemma ISQRT-S0P-J_NONZEROP, and unfolding ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (QUOTIENT I J) J) (IMPLIES (AND (ISQRT-S0P (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (IF (LESSP 32 OPLEN) F T)) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))))) (HEAD (RN-SAVED (STEPN S 10)) OPLEN))) (ISQRT-S0P S I J) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (HEAD (RN-SAVED S) OPLEN))). This simplifies, using linear arithmetic, applying ISQRT-S0P-J_NONZEROP, QUOTIENT-TIMES-LESSP, ISQRT-S0-S0, and STEPN-LEMMA, and expanding the functions AND, IMPLIES, and ISQRT1-T, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (QUOTIENT I J) J)) (ISQRT-S0P S I J) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT1-T I J)))) (HEAD (RN-SAVED S) OPLEN))), which simplifies, using linear arithmetic, rewriting with ISQRT-S0P-J_NONZEROP, QUOTIENT-TIMES-LESSP, and ISQRT-S0-SN-D2, and unfolding the function ISQRT1-T, to: T. Q.E.D. [ 0.0 0.1 0.0 ] ISQRT1-D2 (PROVE-LEMMA ISQRT1-RFILE (REWRITE) (IMPLIES (AND (ISQRT-S0P S I J) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (ISQRT1-T I J)))) (READ-RN OPLEN RN (MC-RFILE S)))) ((INDUCT (ISQRT-INDUCT S I J)))) This formula can be simplified, using the abbreviations ZEROP, D2-7A2-5P, D3-7A2-5P, IMPLIES, NOT, OR, and AND, to the following three new formulas: Case 3. (IMPLIES (AND (ZEROP J) (ISQRT-S0P S I J) (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 (ISQRT1-T I J)))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, applying ISQRT-S0P-J_NONZEROP, and expanding the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (LESSP (QUOTIENT I J) J) (IMPLIES (AND (ISQRT-S0P (STEPN S 10) I (QUOTIENT (PLUS J (QUOTIENT I J)) 2)) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 10) (ISQRT1-T I (QUOTIENT (PLUS J (QUOTIENT I J)) 2))))) (READ-RN OPLEN RN (MC-RFILE (STEPN S 10))))) (ISQRT-S0P S I J) (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 (ISQRT1-T I J)))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, using linear arithmetic, applying ISQRT-S0P-J_NONZEROP, QUOTIENT-TIMES-LESSP, ISQRT-S0-S0, ISQRT-S0-S0-RFILE, and STEPN-LEMMA, and expanding D2-7A2-5P, D3-7A2-5P, AND, IMPLIES, and ISQRT1-T, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL J 0)) (NUMBERP J) (NOT (LESSP (QUOTIENT I J) J)) (ISQRT-S0P S I J) (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 (ISQRT1-T I J)))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, using linear arithmetic, rewriting with ISQRT-S0P-J_NONZEROP, QUOTIENT-TIMES-LESSP, and ISQRT-S0-SN-RFILE, and expanding the definitions of ISQRT1-T, D3-7A2-5P, and D2-7A2-5P, to: T. Q.E.D. [ 0.0 0.1 0.0 ] ISQRT1-RFILE (PROVE-LEMMA ISQRT-CORRECTNESS (REWRITE) (IMPLIES (ISQRT-STATEP S I) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT-T I))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT-T I))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT-T I))) (ISQRT I)) (EQUAL (READ-AN 32 6 (STEPN S (ISQRT-T I))) (READ-AN 32 6 S)) (EQUAL (READ-AN 32 7 (STEPN S (ISQRT-T I))) (ADD 32 (READ-AN 32 7 S) 4)))) ((DISABLE RTS-ADDR LINKED-RTS-ADDR LINKED-A6))) WARNING: Note that the rewrite rule ISQRT-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the rewrite rule ISQRT-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol READ-AN. WARNING: Note that the rewrite rule ISQRT-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol READ-AN. WARNING: Note that the proposed lemma ISQRT-CORRECTNESS 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 and READ-AN, to: (IMPLIES (ISQRT-STATEP S I) (AND (EQUAL (MC-STATUS (STEPN S (ISQRT-T I))) 'RUNNING) (EQUAL (MC-PC (STEPN S (ISQRT-T I))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (ISQRT-T I))) (ISQRT I)) (EQUAL (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN S (ISQRT-T I)))) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 (PLUS 8 7) (MC-RFILE (STEPN S (ISQRT-T I)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)))). This simplifies, rewriting with STEPN-LEMMA, ISQRT-S-S0, ISQRT1-CORRECTNESS, SUB-NEG, and ADD-ASSOCIATIVITY, and unfolding the definitions of ISQRT-T, EQUAL, ISQRT, PLUS, READ-AN, NEG, READ-SP, L, SP, ADD, and AND, to: T. Q.E.D. [ 0.0 0.1 0.0 ] ISQRT-CORRECTNESS (PROVE-LEMMA ISQRT-D2 (REWRITE) (IMPLIES (AND (ISQRT-STATEP S I) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT-T I)))) (READ-DN OPLEN 2 S))) ((DISABLE RN-SAVED))) This conjecture can be simplified, using the abbreviations AND, IMPLIES, and READ-DN, to the goal: (IMPLIES (AND (ISQRT-STATEP S I) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN S (ISQRT-T I)))) (READ-RN OPLEN 2 (MC-RFILE S)))). This simplifies, rewriting with STEPN-LEMMA, ISQRT-S-S0, HEAD-READ-RN, and ISQRT1-D2, and unfolding the functions ISQRT-T and READ-DN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ISQRT-D2 (PROVE-LEMMA ISQRT-RFILE (REWRITE) (IMPLIES (AND (ISQRT-STATEP S I) (D3-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (ISQRT-T I)))) (READ-RN OPLEN RN (MC-RFILE S))))) This formula can be simplified, using the abbreviations D2-7A2-5P, D3-7A2-5P, AND, and IMPLIES, to the new formula: (IMPLIES (AND (ISQRT-STATEP S I) (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 (ISQRT-T I)))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, rewriting with STEPN-LEMMA, ISQRT-S-S0, ISQRT-S-S0-RFILE, and ISQRT1-RFILE, and expanding ISQRT-T, D3-7A2-5P, and D2-7A2-5P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ISQRT-RFILE (PROVE-LEMMA ISQRT-READ-MEM (REWRITE) (IMPLIES (AND (ISQRT-STATEP S I) (DISJOINT X K (SUB 32 8 (READ-SP S)) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT-T I))) K) (READ-MEM X (MC-MEM S) K)))) This conjecture can be simplified, using the abbreviations AND, IMPLIES, SP, L, READ-AN, and READ-SP, to: (IMPLIES (AND (ISQRT-STATEP S I) (DISJOINT X K (SUB 32 8 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 16)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (ISQRT-T I))) K) (READ-MEM X (MC-MEM S) K))). This simplifies, using linear arithmetic, rewriting with SUB-NEG, STEPN-LEMMA, ISQRT-S-S0, DISJOINT-10, ISQRT-S-S0-MEM, and ISQRT1-CORRECTNESS, and opening up the functions PLUS, NEG, ISQRT-T, INDEX-N, LESSP, READ-SP, L, SP, and READ-AN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ISQRT-READ-MEM (DISABLE ISQRT-T) [ 0.0 0.0 0.0 ] ISQRT-T-OFF