(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 GCD-CODE NIL '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) Note that (LISTP (GCD-CODE)) is a theorem. [ 0.0 0.0 0.0 ] GCD-CODE (DEFN GCD (A B) (IF (ZEROP A) (FIX B) (IF (ZEROP B) A (IF (LESSP B A) (GCD (REMAINDER A B) B) (GCD A (REMAINDER B A))))) ((LESSP (PLUS A B)))) Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP can be used to show that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each recursive call. Hence, GCD is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (GCD A B)) is a theorem. [ 0.0 0.0 0.0 ] GCD (DEFN GCD-T1 (A B) (IF (ZEROP A) 6 (IF (ZEROP B) 9 (IF (LESSP B A) (SPLUS 9 (GCD-T1 (REMAINDER A B) B)) (SPLUS 9 (GCD-T1 A (REMAINDER B A)))))) ((LESSP (PLUS A B)))) Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP establish that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each recursive call. Hence, GCD-T1 is accepted under the principle of definition. Note that (NUMBERP (GCD-T1 A B)) is a theorem. [ 0.0 0.0 0.0 ] GCD-T1 (DEFN GCD-T (A B) (SPLUS 4 (GCD-T1 A B))) From the definition we can conclude that (NUMBERP (GCD-T A B)) is a theorem. [ 0.0 0.0 0.0 ] GCD-T (DEFN GCD-INDUCT (S A B) (IF (OR (ZEROP A) (ZEROP B)) T (IF (LESSP B A) (GCD-INDUCT (STEPN S 9) (REMAINDER A B) B) (GCD-INDUCT (STEPN S 9) A (REMAINDER B A)))) ((LESSP (PLUS A B)))) Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX, OR, and ZEROP establish that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each recursive call. Hence, GCD-INDUCT is accepted under the principle of definition. Note that: (TRUEP (GCD-INDUCT S A B)) is a theorem. [ 0.0 0.0 0.0 ] GCD-INDUCT (DEFN GCD-STATEP (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 60) (MCODE-ADDRP (MC-PC S) (MC-MEM S) (GCD-CODE)) (RAM-ADDRP (SUB 32 12 (READ-SP S)) (MC-MEM S) 24) (EQUAL A (IREAD-MEM (ADD 32 (READ-SP S) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-SP S) 8) (MC-MEM S) 4)) (NUMBERP A) (NUMBERP B))) Note that (OR (FALSEP (GCD-STATEP S A B)) (TRUEP (GCD-STATEP S A B))) is a theorem. [ 0.0 0.0 0.0 ] GCD-STATEP (DEFN GCD-S0P (S A B) (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) (GCD-CODE)) (RAM-ADDRP (SUB 32 8 (READ-AN 32 6 S)) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B))) Observe that (OR (FALSEP (GCD-S0P S A B)) (TRUEP (GCD-S0P S A B))) is a theorem. [ 0.0 0.0 0.0 ] GCD-S0P (PROVE-LEMMA GCD-S-S0 (REWRITE) (IMPLIES (GCD-STATEP S A B) (AND (GCD-S0P (STEPN S 4) A B) (EQUAL (LINKED-RTS-ADDR (STEPN S 4)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 4)) (READ-AN 32 6 S)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 4))) (SUB 32 4 (READ-SP S))) (EQUAL (MOVEM-SAVED (STEPN S 4) 4 8 2) (READM-RN 32 '(2 3) (MC-RFILE S)))))) WARNING: Note that the rewrite rule GCD-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol GCD-S0P. WARNING: Note that the rewrite rule GCD-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that GCD-S-S0 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). WARNING: Note that the rewrite rule GCD-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that GCD-S-S0 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). WARNING: Note that GCD-S-S0 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). WARNING: Note that the rewrite rule GCD-S-S0 will be stored so as to apply only to terms with the nonrecursive function symbol MOVEM-SAVED. WARNING: Note that GCD-S-S0 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). WARNING: Note that the proposed lemma GCD-S-S0 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and five replacement rules. This formula can be simplified, using the abbreviations GCD-CODE, GCD-STATEP, IMPLIES, 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) 60) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 12 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (NUMBERP A) (NUMBERP B)) (AND (GCD-S0P (STEPN S 4) A B) (EQUAL (LINKED-RTS-ADDR (STEPN S 4)) (RTS-ADDR S)) (EQUAL (LINKED-A6 (STEPN S 4)) (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 4))) (SUB 32 4 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)))) (EQUAL (MOVEM-SAVED (STEPN S 4) 4 8 2) (READM-RN 32 '(2 3) (MC-RFILE S))))), which simplifies, applying the lemmas SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, STEPN-REWRITER0, STEPN-REWRITER, READ-MEM-NAT-RANGEP, WRITEM-MEM-MAINTAIN-RAM-ADDRP, WRITE-MEM-MAINTAIN-RAM-ADDRP, RAM-ADDRP-3, WRITEM-MEM-MCODE-ADDRP, WRITE-MEM-MCODE-ADDRP, WRITEM-MEM-MAINTAIN-ROM-ADDRP, WRITE-MEM-MAINTAIN-ROM-ADDRP, ROM-ADDRP-LA2, INDEX-N-X-X, ADD-0, MC-PC-RANGEP, DISJOINT-DEDUCTION1, HEAD-READ-RN, READ-WRITE-MEM2, READM-WRITEM-MEM, and MODN-READM-RN, and unfolding the definitions of 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, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, IREAD-DN, READ-DN, GCD-CODE, GCD-S0P, LINKED-RTS-ADDR, RTS-ADDR, UINT-RANGEP, LINKED-A6, MOVEM-SAVED, and AND, to: T. Q.E.D. [ 0.0 1.4 0.0 ] GCD-S-S0 (PROVE-LEMMA GCD-S-S0-RFILE (REWRITE) (IMPLIES (AND (GCD-STATEP S A B) (D4-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 4))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that GCD-S-S0-RFILE contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). This conjecture can be simplified, using the abbreviations D2-7A2-5P, D4-7A2-5P, SP, L, READ-AN, READ-SP, GCD-CODE, GCD-STATEP, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (MC-PC S) (MC-MEM S) 60) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 12 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 4))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, applying the lemmas SUB-NEG, WRITE-MEMP-RAM3, MC-STATUS-REWRITE, MC-RFILE-REWRITE, MC-CCR-RANGEP, MC-CCR-REWRITE, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE1, PC-READ-MEMP-ROM1, MC-MEM-REWRITE, MC-PC-REWRITE, ADD-NAT-RANGEP, PC-READ-MEM-MCODE0, PC-READ-MEMP-ROM0, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, STEPN-REWRITER0, and STEPN-REWRITER, 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, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, and MOVE-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] GCD-S-S0-RFILE (PROVE-LEMMA GCD-S-S0-MEM (REWRITE) (IMPLIES (AND (GCD-STATEP S A B) (DISJOINT X L (SUB 32 12 (READ-SP S)) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 4)) L) (READ-MEM X (MC-MEM S) L)))) WARNING: Note that GCD-S-S0-MEM contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-STATEP S A B). This formula can be simplified, using the abbreviations GCD-CODE, GCD-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) 60) (MCODE-ADDRP (MC-PC S) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 12 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4) (MC-MEM S) 4)) (EQUAL B (IREAD-MEM (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 8) (MC-MEM S) 4)) (NUMBERP A) (NUMBERP B) (DISJOINT X L (SUB 32 12 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 4)) L) (READ-MEM X (MC-MEM S) L))), which simplifies, using linear arithmetic, 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, READM-WRITE-RN, CAR-CONS, WRITE-MEM-MAINTAIN-WRITE-MEMP, CDR-CONS, READ-WRITE-RN, HEAD-LEMMA, WRITE-WRITE-RN, PC-READ-MEM-WRITE-MEM, WRITE-MEM-MAINTAIN-PC-READ-MEMP, ADD-EVENP, WRITEM-MEM-MAINTAIN-READ-MEMP, WRITE-MEMP->READ-MEMP, READ-WRITEM-MEM, READ-WRITE-MEM1, DISJOINT-DEDUCTION2, PC-READ-MEM-WRITEM-MEM, READM-RN-LEN, WRITEM-MEM-MAINTAIN-PC-READ-MEMP, SET-SET-CVZNX1, SET-CVZNX-X, SET-CVZNX-NAT-RANGEP, STEPN-REWRITER0, STEPN-REWRITER, and DISJOINT-10, and expanding 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, EXT-SUBGROUP, S_MODE, N-MEMBER, MOVEM-PRE-RNLST, WRITEMP, MOVEM-PREDEC, NUMBERP, OP-SZ, B, PRE-EFFECT, MOVEM-LEN, PREDEC-MODEP, MOVEM-RN-EA-INS, EVENP, MOVE-INS, MOVE-ADDR-MODEP, EFFEC-ADDR, ADDR-DISP, MC-INSTATE, MC-HALTP, DISJOINT, OPERAND, MAPPING, CAR, CDR, D-MAPPING, MOVE-EFFECT, B0, MOVE-CVZNX, CONS, DN-DIRECT, D_RN, MOVE-MAPPING, D_MODE, and MOVE-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] GCD-S-S0-MEM (PROVE-LEMMA GCD-S0-SN-BASE-1 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (ZEROP A)) (AND (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) (FIX B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) L) (READ-MEM X (MC-MEM S) L))))) WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-SN-BASE-1 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the proposed lemma GCD-S0-SN-BASE-1 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 GCD-CODE, GCD-S0P, AND, IMPLIES, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (ZEROP A)) (AND (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) (FIX B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) L) (READ-MEM X (MC-MEM S) L)))), which simplifies, applying SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-1, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, READ-MEM-NAT-RANGEP, and HEAD-READ-RN, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, ZEROP, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LINKED-RTS-ADDR, FIX, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] GCD-S0-SN-BASE-1 (PROVE-LEMMA GCD-S0-SN-BASE-RFILE-1 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (ZEROP A) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2)))))) WARNING: Note that GCD-S0-SN-BASE-RFILE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). This conjecture can be simplified, using the abbreviations D2-7A2-5P, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to the formula: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (ZEROP A) (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 6))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))). This simplifies, applying SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-1, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, ZEROP, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P, D4-7A2-5P, and MOVEM-SAVED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-S0-SN-BASE-RFILE-1 (PROVE-LEMMA GCD-S0-SN-BASE-2 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (ZEROP B)) (AND (EQUAL (MC-STATUS (STEPN S 9)) 'RUNNING) (EQUAL (MC-PC (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 9)) (FIX A)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 9))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 9))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L))))) WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-SN-BASE-2 will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-SN-BASE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the proposed lemma GCD-S0-SN-BASE-2 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, GCD-CODE, GCD-S0P, AND, IMPLIES, and READ-AN, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (ZEROP B)) (AND (EQUAL (MC-STATUS (STEPN S 9)) 'RUNNING) (EQUAL (MC-PC (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S 9)) (FIX A)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 9))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 9))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L)))). This simplifies, rewriting with SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, MOVE-BEQ-INT-1, FIX-BIT-BITP, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, STEPN-REWRITER, READ-MEM-NAT-RANGEP, and HEAD-READ-RN, and expanding the functions NEG, PLUS, READ-DN, IREAD-DN, ZEROP, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LINKED-RTS-ADDR, FIX, LINKED-A6, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] GCD-S0-SN-BASE-2 (PROVE-LEMMA GCD-S0-SN-BASE-RFILE-2 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (ZEROP B) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2)))))) WARNING: Note that GCD-S0-SN-BASE-RFILE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). This formula can be simplified, using the abbreviations D2-7A2-5P, ZEROP, NOT, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (ZEROP B) (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 9))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))), which simplifies, applying SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, MOVE-BEQ-INT-1, FIX-BIT-BITP, READ-MEMP-RAM3, READ-WRITE-RN, READ-MEMP-RAM2, READ-WRITEM-RN, HEAD-LEMMA, STEPN-REWRITER0, and STEPN-REWRITER, and unfolding the functions NEG, PLUS, READ-DN, IREAD-DN, ZEROP, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, MOVE-INS, MOVE-ADDR-MODEP, MAPPING, D-MAPPING, MOVE-EFFECT, D_RN, MOVE-MAPPING, D_MODE, MOVE-GROUP, MOVEM-EA-RN-SUBGROUP, UPDATE-RFILE, MOVEM-RNLST, READMP, OP-SZ, MOVEM-LEN, TIMES, W, READ-AN, NUMBERP, ADDR-DISP, MOVEM-EA-RN-ADDR-MODEP, POSTINC-MODEP, MOVEM-EA-RN-INS, UNLK-SUBGROUP, WRITE-SP, SP, WRITE-AN, LONG-READ, LONG-READP, LSZ, N-MEMBER, UNLK-INS, NOP-SUBGROUP, RTD-MAPPING, READ-SP, RTS-INS, LISTP, D2-7A2-5P, D4-7A2-5P, and MOVEM-SAVED, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-S0-SN-BASE-RFILE-2 (ENABLE INTEGERP) [ 0.0 0.0 0.0 ] INTEGERP-ON (ENABLE IREMAINDER) [ 0.0 0.0 0.0 ] IREMAINDER-ON (PROVE-LEMMA GCD-S0-S0-1 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A)) (AND (GCD-S0P (STEPN S 9) (REMAINDER A B) B) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 9))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 9)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (MOVEM-SAVED (STEPN S 9) 4 8 2) (MOVEM-SAVED S 4 8 2)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L))))) WARNING: Note that the rewrite rule GCD-S0-S0-1 will be stored so as to apply only to terms with the nonrecursive function symbol GCD-S0P. WARNING: Note that GCD-S0-S0-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-1 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that GCD-S0-S0-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-1 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that GCD-S0-S0-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-1 will be stored so as to apply only to terms with the nonrecursive function symbol MOVEM-SAVED. WARNING: Note that GCD-S0-S0-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-S0-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the proposed lemma GCD-S0-S0-1 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to the goal: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (NOT (EQUAL B 0)) (LESSP B A)) (AND (GCD-S0P (STEPN S 9) (REMAINDER A B) B) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 9))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 9)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (MOVEM-SAVED (STEPN S 9) 4 8 2) (MOVEM-SAVED S 4 8 2)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L)))). This simplifies, rewriting with SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, FIX-BIT-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, DIVS_3232-OVERFLOW, IREM-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, WRITE-WRITE-RN, MC-PC-RANGEP, ADD-0, STEPN-REWRITER0, STEPN-REWRITER, IREM-INT, RAM-ADDRP-3, ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and expanding NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, CMP-INS, CMP-ADDR-MODEP, D_RN, CMP-CVZNX, CMP-GROUP, ILESSP, NEGP, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, MAPPING, D-MAPPING, MOVE-EFFECT, MOVE-MAPPING, D_MODE, MOVE-GROUP, ABS, IREMAINDER, READ-AN, GCD-CODE, GCD-S0P, LINKED-A6, LINKED-RTS-ADDR, MOVEM-SAVED, and AND, to: T. Q.E.D. [ 0.0 0.7 0.0 ] GCD-S0-S0-1 (PROVE-LEMMA GCD-S0-S0-2 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A))) (AND (GCD-S0P (STEPN S 9) A (REMAINDER B A)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 9))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 9)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (MOVEM-SAVED (STEPN S 9) 4 8 2) (MOVEM-SAVED S 4 8 2)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L))))) WARNING: Note that the rewrite rule GCD-S0-S0-2 will be stored so as to apply only to terms with the nonrecursive function symbol GCD-S0P. WARNING: Note that GCD-S0-S0-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-2 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-A6. WARNING: Note that GCD-S0-S0-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-2 will be stored so as to apply only to terms with the nonrecursive function symbol LINKED-RTS-ADDR. WARNING: Note that GCD-S0-S0-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the rewrite rule GCD-S0-S0-2 will be stored so as to apply only to terms with the nonrecursive function symbol MOVEM-SAVED. WARNING: Note that GCD-S0-S0-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that GCD-S0-S0-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). WARNING: Note that the proposed lemma GCD-S0-S0-2 is to be stored as zero type prescription rules, zero compound recognizer rules, zero linear rules, and six replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (NOT (EQUAL B 0)) (NOT (LESSP B A))) (AND (GCD-S0P (STEPN S 9) A (REMAINDER B A)) (EQUAL (READ-RN OPLEN 14 (MC-RFILE (STEPN S 9))) (READ-RN OPLEN 14 (MC-RFILE S))) (EQUAL (LINKED-A6 (STEPN S 9)) (LINKED-A6 S)) (EQUAL (LINKED-RTS-ADDR (STEPN S 9)) (LINKED-RTS-ADDR S)) (EQUAL (MOVEM-SAVED (STEPN S 9) 4 8 2) (MOVEM-SAVED S 4 8 2)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) L) (READ-MEM X (MC-MEM S) L)))). This simplifies, rewriting with SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, FIX-BIT-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, DIVS_3232-OVERFLOW, IREM-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, WRITE-WRITE-RN, MC-PC-RANGEP, ADD-0, STEPN-REWRITER0, STEPN-REWRITER, IREM-INT, RAM-ADDRP-3, ROM-ADDRP-LA2, and INDEX-N-DEDUCTION2, and opening up the functions NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, CMP-INS, CMP-ADDR-MODEP, D_RN, CMP-CVZNX, CMP-GROUP, ILESSP, NEGP, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, MAPPING, D-MAPPING, MOVE-EFFECT, MOVE-MAPPING, D_MODE, MOVE-GROUP, ABS, IREMAINDER, READ-AN, GCD-CODE, GCD-S0P, LINKED-A6, LINKED-RTS-ADDR, MOVEM-SAVED, and AND, to: T. Q.E.D. [ 0.0 0.5 0.0 ] GCD-S0-S0-2 (PROVE-LEMMA GCD-S0-S0-RFILE-1 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (D4-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that GCD-S0-S0-RFILE-1 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). This conjecture can be simplified, using the abbreviations D2-7A2-5P, D4-7A2-5P, ZEROP, NOT, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (NOT (EQUAL B 0)) (LESSP B A) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, applying SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, FIX-BIT-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, DIVS_3232-OVERFLOW, IREM-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, WRITE-WRITE-RN, MC-PC-RANGEP, ADD-0, STEPN-REWRITER0, and STEPN-REWRITER, and expanding NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, CMP-INS, CMP-ADDR-MODEP, D_RN, CMP-CVZNX, CMP-GROUP, ILESSP, NEGP, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, MAPPING, D-MAPPING, MOVE-EFFECT, MOVE-MAPPING, D_MODE, and MOVE-GROUP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-S0-S0-RFILE-1 (PROVE-LEMMA GCD-S0-S0-RFILE-2 (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (D4-7A2-5P RN)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S))))) WARNING: Note that GCD-S0-S0-RFILE-2 contains the free variables B and A which will be chosen by instantiating the hypothesis (GCD-S0P S A B). This conjecture can be simplified, using the abbreviations D2-7A2-5P, D4-7A2-5P, ZEROP, NOT, READ-AN, GCD-CODE, GCD-S0P, AND, and IMPLIES, to: (IMPLIES (AND (EQUAL (MC-STATUS S) 'RUNNING) (EVENP (MC-PC S)) (ROM-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) 60) (MCODE-ADDRP (SUB 32 16 (MC-PC S)) (MC-MEM S) '(78 86 0 0 72 231 48 0 38 46 0 8 36 46 0 12 74 131 103 28 74 130 102 4 32 3 96 22 180 131 108 8 76 66 56 0 38 0 96 232 76 67 40 0 36 0 96 224 32 2 76 238 0 12 255 248 78 94 78 117)) (RAM-ADDRP (SUB 32 8 (READ-RN 32 (PLUS 8 6) (MC-RFILE S))) (MC-MEM S) 24) (EQUAL A (IREAD-DN 32 3 S)) (EQUAL B (IREAD-DN 32 2 S)) (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (NOT (EQUAL B 0)) (NOT (LESSP B A)) (NOT (EQUAL RN 0)) (NUMBERP RN) (NOT (EQUAL RN 1)) (NOT (EQUAL RN 8)) (NOT (EQUAL RN 9)) (NOT (EQUAL RN 14)) (NOT (EQUAL RN 15)) (NOT (EQUAL RN 2)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S)))). This simplifies, applying SUB-NEG, ADD-NAT-RANGEP, MC-PC-REWRITE, MC-MEM-REWRITE, MC-CCR-REWRITE, MC-CCR-RANGEP, MC-RFILE-REWRITE, MC-STATUS-REWRITE, CAR-CONS, CDR-CONS, PC-READ-MEM-MCODE2, PC-READ-MEMP-ROM2, MOVE-BEQ-INT-0, READ-RN-NAT-RANGEP, SET-CVZNX-Z, BITP-FIX-BIT, MOVE-Z-BITP, SET-CVZNX-NAT-RANGEP, ADD-ASSOCIATIVITY, PC-READ-MEM-MCODE3, PC-READ-MEMP-ROM3, ADD-EVENP, SET-SET-CVZNX1, SET-CVZNX-X, FIX-BIT-BITP, SUB-BGE, SET-CVZNX-N, SUB-N-BITP, SET-CVZNX-V, SUB-V-BITP, DIVS_3232-OVERFLOW, IREM-NAT-RANGEP, HEAD-LEMMA, READ-WRITE-RN, WRITE-WRITE-RN, MC-PC-RANGEP, ADD-0, STEPN-REWRITER0, and STEPN-REWRITER, and expanding the definitions of NEG, PLUS, READ-DN, IREAD-DN, EXECUTE-INS, OPCODE-FIELD, EQUAL, TST-SUBGROUP, OP-LEN, Q, UPDATE-CCR, MOVE-CVZNX, B0, OPERAND, CDR, MC-HALTP, MC-INSTATE, S_MODE, S_RN, DN-DIRECT, CONS, EFFEC-ADDR, CAR, TST-ADDR-MODEP, TST-INS, B0P, BITN, MISC-GROUP, UPDATE-PC, L, CURRENT-INS, READ-LST, LEN, LST-NUMBERP, PC-WORD-READ, PC-WORD-READP, WSZ, LESSP, INDEX-N, STEPI, B, HEAD, BCC-RA-SR, BRANCH-CC, EXT, COND-FIELD, BCC-GROUP, ADD, EVENP, B-NOT, CMP-INS, CMP-ADDR-MODEP, D_RN, CMP-CVZNX, CMP-GROUP, ILESSP, NEGP, MOVEM-EA-RN-SUBGROUP, DIV_L-INS, DQ, DR, WRITE-DN, UPDATE-RFILE, DIVS-CVZNX, DIVSL_L, MUL&DIV-ADDR-MODEP, BITS, MUL-DIV_L-INS, MOVE-INS, MOVE-ADDR-MODEP, NUMBERP, MAPPING, D-MAPPING, MOVE-EFFECT, MOVE-MAPPING, D_MODE, and MOVE-GROUP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] GCD-S0-S0-RFILE-2 (PROVE-LEMMA GCD-S0-SN (REWRITE) (IMPLIES (GCD-S0P S A B) (AND (EQUAL (MC-STATUS (STEPN S (GCD-T1 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GCD-T1 A B))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (GCD-T1 A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GCD-T1 A B)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GCD-T1 A B)))) (ADD 32 (READ-AN 32 6 S) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GCD-T1 A B))) K) (READ-MEM X (MC-MEM S) K)))) ((INDUCT (GCD-INDUCT S A B)) (DISABLE GCD-S0P IREAD-DN LINKED-RTS-ADDR LINKED-A6))) WARNING: Note that the rewrite rule GCD-S0-SN will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma GCD-S0-SN 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 (OR (ZEROP A) (ZEROP B)) (GCD-S0P S A B)) (AND (EQUAL (MC-STATUS (STEPN S (GCD-T1 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GCD-T1 A B))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (GCD-T1 A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GCD-T1 A B)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GCD-T1 A B)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GCD-T1 A B))) K) (READ-MEM X (MC-MEM S) K)))). This simplifies, applying GCD-S0-SN-BASE-1, and expanding ZEROP, OR, EQUAL, GCD-T1, GCD, PLUS, READ-AN, AND, and NUMBERP, to 36 new formulas: Case 3.36. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (MC-STATUS (STEPN S 9)) 'RUNNING)), which again simplifies, appealing to the lemma GCD-S0-SN-BASE-2, and expanding ZEROP and EQUAL, to: T. Case 3.35. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING)), which again simplifies, applying GCD-S0-SN-BASE-1, and unfolding the functions ZEROP and EQUAL, to: T. Case 3.34. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING)). This again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up ZEROP and EQUAL, to: T. Case 3.33. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (MC-PC (STEPN S 9)) (LINKED-RTS-ADDR S))). This again simplifies, applying GCD-S0-SN-BASE-2, and expanding ZEROP, to: T. Case 3.32. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S))). However this again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up ZEROP, to: T. Case 3.31. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S))). However this again simplifies, rewriting with the lemma GCD-S0-SN-BASE-1, and opening up ZEROP, to: T. Case 3.30. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (IREAD-DN 32 0 (STEPN S 9)) A)), which again simplifies, applying the lemma GCD-S0-SN-BASE-2, and opening up ZEROP, to: T. Case 3.29. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) 0)), which again simplifies, applying GCD-S0-SN-BASE-1, and unfolding the definitions of ZEROP, NUMBERP, and EQUAL, to: T. Case 3.28. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) 0)). However this again simplifies, applying GCD-S0-SN-BASE-1, and opening up the definitions of ZEROP, NUMBERP, and EQUAL, to: T. Case 3.27. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 9))) (LINKED-A6 S))). However this again simplifies, appealing to the lemma GCD-S0-SN-BASE-2, and unfolding the definition of ZEROP, to: T. Case 3.26. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S))), which again simplifies, rewriting with the lemma GCD-S0-SN-BASE-1, and unfolding the function ZEROP, to: T. Case 3.25. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S))), which again simplifies, applying GCD-S0-SN-BASE-1, and opening up the definition of ZEROP, to: T. Case 3.24. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 9))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). But this again simplifies, applying GCD-S0-SN-BASE-2, and expanding the definitions of ZEROP, PLUS, and READ-AN, to: T. Case 3.23. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and unfolding the functions ZEROP, PLUS, and READ-AN, to: T. Case 3.22. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). However this again simplifies, rewriting with GCD-S0-SN-BASE-1, and expanding the functions ZEROP, PLUS, and READ-AN, to: T. Case 3.21. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) K) (READ-MEM X (MC-MEM S) K))). However this again simplifies, applying GCD-S0-SN-BASE-2, and opening up the function ZEROP, to: T. Case 3.20. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (EQUAL A 0)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up the function ZEROP, to: T. Case 3.19. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (NOT (NUMBERP A))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and expanding ZEROP, to: T. Case 3.18. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (MC-STATUS (STEPN S 9)) 'RUNNING)). But this again simplifies, rewriting with GCD-S0-SN-BASE-2, and unfolding ZEROP and EQUAL, to: T. Case 3.17. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING)). However this again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up the definitions of ZEROP and EQUAL, to: T. Case 3.16. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (MC-STATUS (STEPN S 6)) 'RUNNING)). This again simplifies, appealing to the lemma GCD-S0-SN-BASE-1, and opening up the definitions of ZEROP and EQUAL, to: T. Case 3.15. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (MC-PC (STEPN S 9)) (LINKED-RTS-ADDR S))), which again simplifies, rewriting with GCD-S0-SN-BASE-2, and opening up the function ZEROP, to: T. Case 3.14. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S))). However this again simplifies, applying GCD-S0-SN-BASE-1, and opening up the definition of ZEROP, to: T. Case 3.13. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (MC-PC (STEPN S 6)) (LINKED-RTS-ADDR S))). This again simplifies, rewriting with the lemma GCD-S0-SN-BASE-1, and expanding the function ZEROP, to: T. Case 3.12. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (IREAD-DN 32 0 (STEPN S 9)) A)), which again simplifies, rewriting with GCD-S0-SN-BASE-2, and expanding ZEROP, to: T. Case 3.11. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) 0)). This again simplifies, rewriting with GCD-S0-SN-BASE-1, and expanding the functions ZEROP and EQUAL, to: T. Case 3.10. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (IREAD-DN 32 0 (STEPN S 6)) 0)). This again simplifies, applying GCD-S0-SN-BASE-1, and unfolding the functions ZEROP and EQUAL, to: T. Case 3.9. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 9))) (LINKED-A6 S))). This again simplifies, applying GCD-S0-SN-BASE-2, and opening up ZEROP, to: T. Case 3.8. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up ZEROP, to: T. Case 3.7. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S 6))) (LINKED-A6 S))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and expanding the definition of ZEROP, to: T. Case 3.6. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 9))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). But this again simplifies, applying GCD-S0-SN-BASE-2, and unfolding ZEROP, PLUS, and READ-AN, to: T. Case 3.5. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). But this again simplifies, rewriting with GCD-S0-SN-BASE-1, and expanding ZEROP, PLUS, and READ-AN, to: T. Case 3.4. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S 6))) (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 8))). This again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up ZEROP, PLUS, and READ-AN, to: T. Case 3.3. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 9)) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, rewriting with GCD-S0-SN-BASE-2, and expanding the definition of ZEROP, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (EQUAL A 0)) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K))). However this again simplifies, rewriting with GCD-S0-SN-BASE-1, and opening up ZEROP, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (NOT (NUMBERP A))) (EQUAL (READ-MEM X (MC-MEM (STEPN S 6)) K) (READ-MEM X (MC-MEM S) K))). But this again simplifies, applying the lemma GCD-S0-SN-BASE-1, and opening up ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (IMPLIES (GCD-S0P (STEPN S 9) (REMAINDER A B) B) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B))) (LINKED-RTS-ADDR (STEPN S 9))) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B))) (GCD (REMAINDER A B) B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (LINKED-A6 (STEPN S 9))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN S 9))) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B))) K) (READ-MEM X (MC-MEM (STEPN S 9)) K)))) (GCD-S0P S A B)) (AND (EQUAL (MC-STATUS (STEPN S (GCD-T1 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GCD-T1 A B))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (GCD-T1 A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GCD-T1 A B)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GCD-T1 A B)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GCD-T1 A B))) K) (READ-MEM X (MC-MEM S) K)))), which simplifies, appealing to the lemmas GCD-S0-S0-1 and STEPN-LEMMA, and opening up PLUS, AND, IMPLIES, GCD-T1, EQUAL, and GCD, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (IMPLIES (GCD-S0P (STEPN S 9) A (REMAINDER B A)) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A)))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A)))) (LINKED-RTS-ADDR (STEPN S 9))) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A)))) (GCD A (REMAINDER B A))) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (LINKED-A6 (STEPN S 9))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE (STEPN S 9))) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A)))) K) (READ-MEM X (MC-MEM (STEPN S 9)) K)))) (GCD-S0P S A B)) (AND (EQUAL (MC-STATUS (STEPN S (GCD-T1 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GCD-T1 A B))) (LINKED-RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (GCD-T1 A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GCD-T1 A B)))) (LINKED-A6 S)) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GCD-T1 A B)))) (ADD 32 (READ-RN 32 (PLUS 8 6) (MC-RFILE S)) 8)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GCD-T1 A B))) K) (READ-MEM X (MC-MEM S) K)))), which simplifies, applying the lemmas GCD-S0-S0-2 and STEPN-LEMMA, and opening up PLUS, AND, IMPLIES, GCD-T1, EQUAL, and GCD, to: T. Q.E.D. [ 0.0 0.4 0.1 ] GCD-S0-SN (PROVE-LEMMA GCD-S0-SN-RFILE (REWRITE) (IMPLIES (AND (GCD-S0P S A B) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GCD-T1 A B)))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))) ((INDUCT (GCD-INDUCT S A B)) (DISABLE GCD-S0P))) This conjecture can be simplified, using the abbreviations ZEROP, D2-7A2-5P, IMPLIES, NOT, OR, and AND, to three new formulas: Case 3. (IMPLIES (AND (OR (ZEROP A) (ZEROP B)) (GCD-S0P S A B) (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 (GCD-T1 A B)))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))), which simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and unfolding ZEROP, OR, EQUAL, GCD-T1, D2-7A2-5P, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to the following 18 new conjectures: Case 3.18. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 3) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, rewriting with SUB-NEG and GCD-S0-SN-BASE-RFILE-2, and opening up the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.17. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). However this again simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-2, and expanding the definitions of EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.16. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and expanding the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.15. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). But this again simplifies, appealing to the lemmas SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and opening up the definitions of EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.14. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 3) (NOT (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))), which again simplifies, rewriting with SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and opening up EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.13. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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 3) (EQUAL A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). However this again simplifies, rewriting with SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and opening up the definitions of EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.12. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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)) (NOT (EQUAL RN 3)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, applying GCD-S0-SN-BASE-RFILE-2, and opening up D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 3.11. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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)) (NOT (EQUAL RN 3)) (EQUAL A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, appealing to the lemma GCD-S0-SN-BASE-RFILE-1, and expanding the functions D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 3.10. (IMPLIES (AND (EQUAL B 0) (GCD-S0P S A 0) (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)) (NOT (EQUAL RN 3)) (NOT (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, appealing to the lemma GCD-S0-SN-BASE-RFILE-1, and opening up D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 3.9. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 3) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))), which again simplifies, appealing to the lemmas SUB-NEG and GCD-S0-SN-BASE-RFILE-2, and opening up EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.8. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))), which again simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-2, and unfolding the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.7. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). But this again simplifies, rewriting with SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and expanding the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.6. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and unfolding EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.5. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 3) (NOT (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, rewriting with SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and expanding the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.4. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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 3) (EQUAL A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). But this again simplifies, applying SUB-NEG and GCD-S0-SN-BASE-RFILE-1, and opening up the functions EQUAL, NUMBERP, D2-7A2-5P, ZEROP, D4-7A2-5P, NEG, READ-AN, PLUS, and MOVEM-SAVED, to: T. Case 3.3. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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)) (NOT (EQUAL RN 3)) (NOT (EQUAL A 0)) (NUMBERP A)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (READ-RN OPLEN RN (MC-RFILE S)))). This again simplifies, appealing to the lemma GCD-S0-SN-BASE-RFILE-2, and unfolding D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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)) (NOT (EQUAL RN 3)) (EQUAL A 0)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (READ-RN OPLEN RN (MC-RFILE S)))), which again simplifies, applying GCD-S0-SN-BASE-RFILE-1, and expanding the definitions of D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP B)) (GCD-S0P S A B) (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)) (NOT (EQUAL RN 3)) (NOT (NUMBERP A))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 6))) (READ-RN OPLEN RN (MC-RFILE S)))). However this again simplifies, rewriting with GCD-S0-SN-BASE-RFILE-1, and opening up the functions D2-7A2-5P, ZEROP, and D4-7A2-5P, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (IMPLIES (AND (GCD-S0P (STEPN S 9) (REMAINDER A B) B) (D2-7A2-5P RN) (IF (LESSP 32 OPLEN) F T)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED (STEPN S 9) 4 8 2))))) (GCD-S0P S A B) (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 (GCD-T1 A B)))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))). This simplifies, applying the lemmas GCD-S0-S0-1, SUB-NEG, STEPN-LEMMA, and GCD-S0-S0-RFILE-1, and opening up the definitions of D2-7A2-5P, AND, D4-7A2-5P, NEG, READ-AN, PLUS, MOVEM-SAVED, IMPLIES, EQUAL, NUMBERP, and GCD-T1, to the following two new goals: Case 2.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (EQUAL RN 3) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2))) (GCD-S0P S A B) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 3 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (GET-VLST OPLEN 0 3 '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, obviously, to: T. Case 2.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (EQUAL RN 2) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2))) (GCD-S0P S A B) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 (REMAINDER A B) B)))) (GET-VLST OPLEN 0 2 '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, obviously, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (IMPLIES (AND (GCD-S0P (STEPN S 9) A (REMAINDER B A)) (D2-7A2-5P RN) (IF (LESSP 32 OPLEN) F T)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE (STEPN S 9))) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED (STEPN S 9) 4 8 2))))) (GCD-S0P S A B) (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 (GCD-T1 A B)))) (IF (D4-7A2-5P RN) (READ-RN OPLEN RN (MC-RFILE S)) (GET-VLST OPLEN 0 RN '(2 3) (MOVEM-SAVED S 4 8 2))))). This simplifies, applying the lemmas GCD-S0-S0-2, SUB-NEG, STEPN-LEMMA, and GCD-S0-S0-RFILE-2, and unfolding D2-7A2-5P, AND, D4-7A2-5P, NEG, READ-AN, PLUS, MOVEM-SAVED, IMPLIES, EQUAL, NUMBERP, and GCD-T1, to the following two new goals: Case 1.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (EQUAL RN 3) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2))) (GCD-S0P S A B) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 3 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (GET-VLST OPLEN 0 3 '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, obviously, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (EQUAL RN 2) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (GET-VLST OPLEN 0 RN '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2))) (GCD-S0P S A B) (NOT (LESSP 32 OPLEN))) (EQUAL (READ-RN OPLEN 2 (MC-RFILE (STEPN (STEPN S 9) (GCD-T1 A (REMAINDER B A))))) (GET-VLST OPLEN 0 2 '(2 3) (READM-MEM 4 (ADD 32 (READ-RN 32 14 (MC-RFILE S)) 4294967288) (MC-MEM S) 2)))). This again simplifies, trivially, to: T. Q.E.D. [ 0.0 0.5 0.1 ] GCD-S0-SN-RFILE (PROVE-LEMMA GCD-CORRECTNESS (REWRITE) (IMPLIES (GCD-STATEP S A B) (AND (EQUAL (MC-STATUS (STEPN S (GCD-T A B))) 'RUNNING) (EQUAL (MC-PC (STEPN S (GCD-T A B))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN S (GCD-T A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN S (GCD-T A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN S (GCD-T A B)))) (ADD 32 (READ-AN 32 7 S) 4)))) ((DISABLE GCD-STATEP GCD-S0P LINKED-RTS-ADDR LINKED-A6))) WARNING: Note that the rewrite rule GCD-CORRECTNESS will be stored so as to apply only to terms with the nonrecursive function symbol IREAD-DN. WARNING: Note that the proposed lemma GCD-CORRECTNESS 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 IMPLIES, READ-AN, STEPN-LEMMA, and GCD-T, to: (IMPLIES (GCD-STATEP S A B) (AND (EQUAL (MC-STATUS (STEPN (STEPN S 4) (GCD-T1 A B))) 'RUNNING) (EQUAL (MC-PC (STEPN (STEPN S 4) (GCD-T1 A B))) (RTS-ADDR S)) (EQUAL (IREAD-DN 32 0 (STEPN (STEPN S 4) (GCD-T1 A B))) (GCD A B)) (EQUAL (READ-RN 32 14 (MC-RFILE (STEPN (STEPN S 4) (GCD-T1 A B)))) (READ-RN 32 14 (MC-RFILE S))) (EQUAL (READ-RN 32 15 (MC-RFILE (STEPN (STEPN S 4) (GCD-T1 A B)))) (ADD 32 (READ-RN 32 (PLUS 8 7) (MC-RFILE S)) 4)))), which simplifies, rewriting with GCD-S-S0, GCD-S0-SN, SUB-NEG, and ADD-ASSOCIATIVITY, and expanding the functions 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 ] GCD-CORRECTNESS (PROVE-LEMMA GCD-RFILE (REWRITE) (IMPLIES (AND (GCD-STATEP S A B) (D2-7A2-5P RN) (LEQ OPLEN 32)) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S (GCD-T A B)))) (READ-RN OPLEN RN (MC-RFILE S)))) ((DISABLE GCD-STATEP GCD-S0P))) This formula can be simplified, using the abbreviations D2-7A2-5P, AND, IMPLIES, STEPN-LEMMA, and GCD-T, to the new goal: (IMPLIES (AND (GCD-STATEP S A B) (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 4) (GCD-T1 A B)))) (READ-RN OPLEN RN (MC-RFILE S)))), which simplifies, appealing to the lemmas GCD-S-S0, GET-VLST-READM-RN, and GCD-S0-SN-RFILE, and expanding the definitions of D2-7A2-5P, D4-7A2-5P, CDR, NUMBERP, CAR, LISTP, and N-MEMBER, to: (IMPLIES (AND (GCD-STATEP S A B) (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)) (NOT (EQUAL RN 3))) (EQUAL (READ-RN OPLEN RN (MC-RFILE (STEPN S 4))) (READ-RN OPLEN RN (MC-RFILE S)))). But this again simplifies, rewriting with GCD-S-S0-RFILE, and opening up the definitions of D4-7A2-5P and D2-7A2-5P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GCD-RFILE (PROVE-LEMMA GCD-MEM (REWRITE) (IMPLIES (AND (GCD-STATEP S A B) (DISJOINT X K (SUB 32 12 (READ-SP S)) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN S (GCD-T A B))) K) (READ-MEM X (MC-MEM S) K))) ((DISABLE GCD-STATEP GCD-S0P))) This conjecture can be simplified, using the abbreviations AND, IMPLIES, STEPN-LEMMA, GCD-T, SP, L, READ-AN, and READ-SP, to: (IMPLIES (AND (GCD-STATEP S A B) (DISJOINT X K (SUB 32 12 (READ-RN 32 (PLUS 8 7) (MC-RFILE S))) 24)) (EQUAL (READ-MEM X (MC-MEM (STEPN (STEPN S 4) (GCD-T1 A B))) K) (READ-MEM X (MC-MEM S) K))). This simplifies, using linear arithmetic, rewriting with SUB-NEG, GCD-S-S0, DISJOINT-10, GCD-S-S0-MEM, and GCD-S0-SN, and unfolding PLUS, NEG, INDEX-N, LESSP, READ-SP, L, SP, and READ-AN, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GCD-MEM (DISABLE GCD-T) [ 0.0 0.0 0.0 ] GCD-T-OFF (PROVE-LEMMA REMAINDER-REMAINDER (REWRITE) (IMPLIES (EQUAL (REMAINDER B C) 0) (EQUAL (REMAINDER (REMAINDER A B) C) (REMAINDER A C)))) . Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B) and X by (PLUS V (TIMES C W)) to eliminate (REMAINDER X C) and (QUOTIENT X C). We employ REMAINDER-LESSP, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. This produces the following six new conjectures: Case 6. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER (REMAINDER A B) C) (REMAINDER A C))). But this simplifies, rewriting with the lemma REMAINDER-0, and unfolding the functions LESSP, REMAINDER, and EQUAL, to: T. Case 5. (IMPLIES (AND (EQUAL B 0) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER (REMAINDER A B) C) (REMAINDER A C))), which simplifies, applying REMAINDER-0, and expanding the function EQUAL, to the new conjecture: (IMPLIES (NOT (NUMBERP A)) (EQUAL (REMAINDER 0 C) (REMAINDER A C))), which again simplifies, rewriting with REMAINDER-0, and expanding the definitions of LESSP, REMAINDER, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NUMBERP B)) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER (REMAINDER A B) C) (REMAINDER A C))). This simplifies, opening up the definitions of LESSP, REMAINDER, and EQUAL, to: (IMPLIES (AND (NOT (NUMBERP B)) (NOT (NUMBERP A))) (EQUAL (REMAINDER 0 C) (REMAINDER A C))). However this again simplifies, appealing to the lemma REMAINDER-0, and unfolding the definitions of LESSP, REMAINDER, and EQUAL, to: T. Case 3. (IMPLIES (AND (EQUAL C 0) (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER X C) (REMAINDER (PLUS X (TIMES B Z)) C))), which simplifies, applying REMAINDER-0, and opening up the definitions of ZEROP and NOT, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP C)) (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (EQUAL (REMAINDER B C) 0)) (EQUAL (REMAINDER X C) (REMAINDER (PLUS X (TIMES B Z)) C))). However this simplifies, expanding the definitions of ZEROP, NOT, and REMAINDER, to: T. Case 1. (IMPLIES (AND (NUMBERP V) (EQUAL (LESSP V C) (NOT (ZEROP C))) (NUMBERP W) (NUMBERP C) (NOT (EQUAL C 0)) (EQUAL (LESSP (PLUS V (TIMES C W)) B) (NOT (ZEROP B))) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (EQUAL (REMAINDER B C) 0)) (EQUAL V (REMAINDER (PLUS (PLUS V (TIMES C W)) (TIMES B Z)) C))), which simplifies, applying PLUS-COMMUTATIVITY, PLUS-ASSOCIATIVITY, REMAINDER-PLUS-PLUS-TIMES1, and REMAINDER-PLUS-CANCEL0, and opening up the definitions of ZEROP and NOT, to the new conjecture: (IMPLIES (AND (NUMBERP V) (LESSP V C) (NUMBERP W) (NUMBERP C) (NOT (EQUAL C 0)) (LESSP (PLUS V (TIMES C W)) B) (NUMBERP Z) (NUMBERP B) (NOT (EQUAL B 0)) (EQUAL (REMAINDER B C) 0)) (EQUAL 0 (REMAINDER (TIMES B Z) C))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by (PLUS X (TIMES C D)) to eliminate (REMAINDER B C) and (QUOTIENT B C). We employ REMAINDER-LESSP, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain: (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X C) (NOT (ZEROP C))) (NUMBERP D) (NUMBERP V) (LESSP V C) (NUMBERP W) (NUMBERP C) (NOT (EQUAL C 0)) (LESSP (PLUS V (TIMES C W)) (PLUS X (TIMES C D))) (NUMBERP Z) (NOT (EQUAL (PLUS X (TIMES C D)) 0)) (EQUAL X 0)) (EQUAL 0 (REMAINDER (TIMES (PLUS X (TIMES C D)) Z) C))), which further simplifies, applying the lemmas PLUS-0, TIMES-EQUAL-0, TIMES-ASSOCIATIVITY, and REMAINDER-TIMES, and unfolding the functions NUMBERP, EQUAL, LESSP, ZEROP, and NOT, to: T. Q.E.D. [ 0.0 0.2 0.0 ] REMAINDER-REMAINDER (PROVE-LEMMA GCD-IS-CD (REWRITE) (AND (EQUAL (REMAINDER A (GCD A B)) 0) (EQUAL (REMAINDER B (GCD A B)) 0))) WARNING: Note that the proposed lemma GCD-IS-CD 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 abbreviation AND, to the following two new conjectures: Case 2. (EQUAL (REMAINDER A (GCD A B)) 0). Call the above conjecture *1. Case 1. (EQUAL (REMAINDER B (GCD A B)) 0), 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: (AND (EQUAL (REMAINDER A (GCD A B)) 0) (EQUAL (REMAINDER B (GCD A B)) 0)), which we named *1 above. We will appeal to induction. The recursive terms in the conjecture suggest four inductions. They merge into three likely candidate inductions, all 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 (ZEROP A) (p B A)) (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (p B A)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (p B (REMAINDER A B))) (p B A)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (p (REMAINDER B A) A)) (p B A))). Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP inform us that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following eight new goals: Case 8. (IMPLIES (ZEROP A) (EQUAL (REMAINDER A (GCD A B)) 0)). This simplifies, rewriting with REMAINDER-0, and expanding ZEROP, EQUAL, GCD, LESSP, and REMAINDER, to: T. Case 7. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (EQUAL (REMAINDER A (GCD A B)) 0)), which simplifies, applying REMAINDER-X-X, and unfolding ZEROP, EQUAL, and GCD, to: T. Case 6. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (EQUAL (REMAINDER (REMAINDER A B) (GCD (REMAINDER A B) B)) 0) (EQUAL (REMAINDER B (GCD (REMAINDER A B) B)) 0)) (EQUAL (REMAINDER A (GCD A B)) 0)). This simplifies, rewriting with REMAINDER-REMAINDER, and opening up the functions ZEROP, GCD, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (EQUAL (REMAINDER A (GCD A (REMAINDER B A))) 0) (EQUAL (REMAINDER (REMAINDER B A) (GCD A (REMAINDER B A))) 0)) (EQUAL (REMAINDER A (GCD A B)) 0)), which simplifies, applying REMAINDER-REMAINDER, and opening up ZEROP, GCD, and EQUAL, to: T. Case 4. (IMPLIES (ZEROP A) (EQUAL (REMAINDER B (GCD A B)) 0)). This simplifies, expanding ZEROP, EQUAL, and GCD, to the following four new goals: Case 4.4. (IMPLIES (AND (EQUAL A 0) (NOT (NUMBERP B))) (EQUAL (REMAINDER B 0) 0)). This again simplifies, rewriting with the lemma REMAINDER-0, and unfolding EQUAL, to: T. Case 4.3. (IMPLIES (AND (EQUAL A 0) (NUMBERP B)) (EQUAL (REMAINDER B B) 0)), which again simplifies, applying REMAINDER-X-X, and expanding the function EQUAL, to: T. Case 4.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (NUMBERP B))) (EQUAL (REMAINDER B 0) 0)). This again simplifies, rewriting with REMAINDER-0, and unfolding the function EQUAL, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP A)) (NUMBERP B)) (EQUAL (REMAINDER B B) 0)). But this again simplifies, rewriting with REMAINDER-X-X, and expanding the definition of EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (EQUAL (REMAINDER B (GCD A B)) 0)). This simplifies, applying the lemma REMAINDER-0, and opening up the definitions of ZEROP, EQUAL, GCD, LESSP, and REMAINDER, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (EQUAL (REMAINDER (REMAINDER A B) (GCD (REMAINDER A B) B)) 0) (EQUAL (REMAINDER B (GCD (REMAINDER A B) B)) 0)) (EQUAL (REMAINDER B (GCD A B)) 0)). This simplifies, applying REMAINDER-REMAINDER, and opening up ZEROP, GCD, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (EQUAL (REMAINDER A (GCD A (REMAINDER B A))) 0) (EQUAL (REMAINDER (REMAINDER B A) (GCD A (REMAINDER B A))) 0)) (EQUAL (REMAINDER B (GCD A B)) 0)), which simplifies, rewriting with REMAINDER-REMAINDER, and expanding the definitions of ZEROP, GCD, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.1 ] GCD-IS-CD (PROVE-LEMMA GCD-THE-GREATEST (REWRITE) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD A B) X))) ((INDUCT (GCD A B)))) WARNING: When the linear lemma GCD-THE-GREATEST is stored under (GCD A B) it contains the free variable X which will be chosen by instantiating the hypothesis (EQUAL (REMAINDER A X) 0). WARNING: Note that the proposed lemma GCD-THE-GREATEST is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT, OR, and AND, to four new formulas: Case 4. (IMPLIES (AND (ZEROP A) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD A B) X))), which simplifies, opening up ZEROP, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (ZEROP B) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD A B) X))), which simplifies, opening up ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (IMPLIES (AND (NOT (ZEROP (REMAINDER A B))) (NOT (ZEROP B)) (EQUAL (REMAINDER (REMAINDER A B) X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD (REMAINDER A B) B) X))) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD A B) X))), which simplifies, applying REMAINDER-REMAINDER, and expanding the functions ZEROP, NOT, EQUAL, AND, IMPLIES, and GCD, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (EQUAL (REMAINDER A B) 0) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP B X))), which again simplifies, opening up the definition of REMAINDER, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP (REMAINDER B A))) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER (REMAINDER B A) X) 0)) (NOT (LESSP (GCD A (REMAINDER B A)) X))) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP (GCD A B) X))), which simplifies, appealing to the lemma REMAINDER-REMAINDER, and expanding the definitions of ZEROP, NOT, EQUAL, AND, IMPLIES, and GCD, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (EQUAL (REMAINDER B A) 0) (EQUAL (REMAINDER A X) 0) (EQUAL (REMAINDER B X) 0)) (NOT (LESSP A X))). However this again simplifies, expanding REMAINDER, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-THE-GREATEST (PROVE-LEMMA LESSP-TIMES-LESSP (REWRITE) (IMPLIES (AND (LESSP A B) (NOT (ZEROP C))) (LESSP A (TIMES B C)))) WARNING: When the linear lemma LESSP-TIMES-LESSP is stored under (TIMES B C) it contains the free variable A which will be chosen by instantiating the hypothesis (LESSP A B). WARNING: Note that the proposed lemma LESSP-TIMES-LESSP is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))), which we will name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C)))) (p A B C)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p A B C)) (IMPLIES (AND (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p (SUB1 A) B C)) (p A B C))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following four new conjectures: Case 4. (IMPLIES (AND (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C)))) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))). This simplifies, applying the lemma TIMES-EQUAL-0, and unfolding the definitions of NOT, OR, EQUAL, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (OR (EQUAL A 0) (NOT (NUMBERP A))) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))). This simplifies, using linear arithmetic, applying TIMES-EQUAL-0 and TIMES-LESSP, and unfolding NOT, OR, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (LESSP (SUB1 A) B)) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))), which simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (LESSP A 1) (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (NOT (LESSP (SUB1 A) B)) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))). However this again simplifies, applying LESSP-OF-1 and TIMES-EQUAL-0, and opening up the functions NOT, OR, EQUAL, and NUMBERP, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (SUB1 A) (TIMES B C)) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))). This simplifies, using linear arithmetic, to the following two new goals: Case 1.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (SUB1 A) (TIMES B C)) (LESSP A B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP A (TIMES B C))). However this again simplifies, appealing to the lemma TIMES-EQUAL-0, and expanding NOT and OR, to: T. Case 1.1. (IMPLIES (AND (NUMBERP A) (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (NOT (OR (EQUAL (TIMES B C) 0) (NOT (NUMBERP (TIMES B C))))) (LESSP (SUB1 (TIMES B C)) (TIMES B C)) (LESSP (TIMES B C) B) (NOT (EQUAL C 0)) (NUMBERP C)) (LESSP (TIMES B C) (TIMES B C))), which again simplifies, rewriting with TIMES-EQUAL-0, LESSP-SUB1, and CORRECTNESS-OF-CANCEL-LESSP-TIMES, and unfolding the functions NOT, OR, ZEROP, and AND, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-TIMES-LESSP (PROVE-LEMMA REMAINDER-SHRINK-HALF (REWRITE) (IMPLIES (AND (LEQ B A) (NOT (ZEROP B))) (NOT (LESSP (QUOTIENT A 2) (REMAINDER A B)))) ((EXPAND (TIMES 2 X)) (ENABLE QUOTIENT-GENERALIZE))) WARNING: When the linear lemma REMAINDER-SHRINK-HALF is stored under (QUOTIENT A 2) it contains the free variable B which will be chosen by instantiating the hypothesis (NOT (LESSP A B)). WARNING: Note that the proposed lemma REMAINDER-SHRINK-HALF is to be stored as zero type prescription rules, zero compound recognizer rules, two linear rules, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (QUOTIENT A 2) (REMAINDER A B)))). This simplifies, appealing to the lemma QUOTIENT-TIMES-LESSP, and unfolding EQUAL and NUMBERP, to: (IMPLIES (AND (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP A (TIMES 2 (REMAINDER A B))))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES B Z)) to eliminate (REMAINDER A B) and (QUOTIENT A B). We employ QUOTIENT-GENERALIZE, REMAINDER-LESSP, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following two new conjectures: Case 2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP A (TIMES 2 (REMAINDER A B))))). But this further simplifies, opening up the function LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X B) (NOT (ZEROP B))) (NUMBERP Z) (EQUAL (EQUAL Z 0) (IF (OR (ZEROP (PLUS X (TIMES B Z))) (ZEROP B)) T (LESSP (PLUS X (TIMES B Z)) B))) (NOT (LESSP (PLUS X (TIMES B Z)) B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (PLUS X (TIMES B Z)) (TIMES 2 X)))), which further simplifies, rewriting with PLUS-EQUAL-0, TIMES-EQUAL-0, TIMES-ZERO, TIMES-1, and CORRECTNESS-OF-CANCEL-LESSP-PLUS, and expanding the definitions of ZEROP, NOT, OR, PLUS, EQUAL, LESSP, TIMES, NUMBERP, SUB1, and FIX, to: (IMPLIES (AND (NUMBERP X) (LESSP X B) (NUMBERP Z) (NOT (EQUAL Z 0)) (NOT (LESSP (PLUS X (TIMES B Z)) B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (TIMES B Z) X))), which again simplifies, using linear arithmetic and appealing to the lemma LESSP-TIMES-LESSP, to: T. Q.E.D. [ 0.0 0.1 0.0 ] REMAINDER-SHRINK-HALF (PROVE-LEMMA GCD-T-SHRINK-1 (REWRITE) (IMPLIES (AND (LEQ B A) (NOT (ZEROP B))) (NOT (LESSP (SUB1 (LOG 2 A)) (LOG 2 (REMAINDER A B))))) ((USE (LOG-LEQ (B 2) (X (REMAINDER A B)) (Y (QUOTIENT A 2)))) (DISABLE QUOTIENT-TIMES-LESSP))) WARNING: Note that the proposed lemma GCD-T-SHRINK-1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (IMPLIES (IF (LESSP (QUOTIENT A 2) (REMAINDER A B)) F T) (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B))))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B)) (NOT (LESSP (SUB1 (LOG 2 A)) (LOG 2 (REMAINDER A B))))). This simplifies, applying SUB1-OF-1 and LESSP-OF-1, and unfolding the definitions of NOT, IMPLIES, LESSP, SUB1, NUMBERP, EQUAL, and LOG, to eight new formulas: Case 8. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL A 0)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (NUMBERP A))) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))), which again simplifies, unfolding the functions LESSP, NUMBERP, EQUAL, QUOTIENT, and REMAINDER, to: T. Case 6. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL A 1)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (QUOTIENT 1 2) (REMAINDER 1 1)) (NOT (LESSP 1 1)) (NOT (EQUAL 1 0)) (NUMBERP 1)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER 1 1))))). However this again simplifies, opening up the definitions of QUOTIENT, REMAINDER, and LESSP, to: T. Case 5. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1))) (NOT (LESSP (SUB1 (ADD1 (LOG 2 (QUOTIENT A 2)))) (LOG 2 (REMAINDER A B))))), which again simplifies, using linear arithmetic and applying REMAINDER-SHRINK-HALF, to: T. Case 4. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL A 0)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))). However this again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (NUMBERP A))) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))), which again simplifies, opening up the definitions of LESSP, NUMBERP, EQUAL, QUOTIENT, LOG, and REMAINDER, to: T. Case 2. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (EQUAL A 1)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER A B))))), which again simplifies, using linear arithmetic, to the conjecture: (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT 1 2)) (LOG 2 (REMAINDER 1 1)))) (NOT (LESSP 1 1)) (NOT (EQUAL 1 0)) (NUMBERP 1)) (NOT (LESSP (SUB1 0) (LOG 2 (REMAINDER 1 1))))). This again simplifies, opening up the functions QUOTIENT, LOG, REMAINDER, LESSP, EQUAL, NUMBERP, and SUB1, to: T. Case 1. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL A 1))) (NOT (LESSP (SUB1 (ADD1 (LOG 2 (QUOTIENT A 2)))) (LOG 2 (REMAINDER A B))))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-T-SHRINK-1 (PROVE-LEMMA GCD-T-SHRINK-2 (REWRITE) (IMPLIES (AND (LEQ B A) (NOT (ZEROP B)) (NOT (EQUAL A 1))) (NOT (LESSP (TIMES 9 (PLUS X (LOG 2 A))) (PLUS 9 (TIMES 9 (PLUS X (LOG 2 (REMAINDER A B)))))))) ((USE (LOG-LEQ (B 2) (X (REMAINDER A B)) (Y (QUOTIENT A 2)))) (DISABLE QUOTIENT-TIMES-LESSP))) WARNING: Note that the proposed lemma GCD-T-SHRINK-2 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations PLUS-LESSP-CANCEL-1, TIMES-LESSP-CANCEL-1, ZEROP, NOT, AND, and IMPLIES, to the new goal: (IMPLIES (AND (IMPLIES (IF (LESSP (QUOTIENT A 2) (REMAINDER A B)) F T) (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B))))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (NOT (EQUAL 9 0)) (NUMBERP 9)) (LESSP (LOG 2 (REMAINDER A B)) (LOG 2 A))), which simplifies, rewriting with SUB1-OF-1 and LESSP-OF-1, and unfolding the functions NOT, IMPLIES, EQUAL, NUMBERP, LESSP, SUB1, and LOG, to the following six new goals: Case 6. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (NOT (NUMBERP A))) (LESSP (LOG 2 (REMAINDER A B)) 0)). However this again simplifies, expanding the functions LESSP, NUMBERP, EQUAL, QUOTIENT, and REMAINDER, to: T. Case 5. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (EQUAL A 0)) (LESSP (LOG 2 (REMAINDER A B)) 0)), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (LESSP (QUOTIENT A 2) (REMAINDER A B)) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (NOT (EQUAL A 0)) (NUMBERP A)) (LESSP (LOG 2 (REMAINDER A B)) (ADD1 (LOG 2 (QUOTIENT A 2))))), which again simplifies, using linear arithmetic and applying the lemma REMAINDER-SHRINK-HALF, to: T. Case 3. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (NOT (NUMBERP A))) (LESSP (LOG 2 (REMAINDER A B)) 0)), which again simplifies, expanding the functions LESSP, NUMBERP, EQUAL, QUOTIENT, LOG, and REMAINDER, to: T. Case 2. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (EQUAL A 0)) (LESSP (LOG 2 (REMAINDER A B)) 0)), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (LESSP (LOG 2 (QUOTIENT A 2)) (LOG 2 (REMAINDER A B)))) (NOT (LESSP A B)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (EQUAL A 1)) (NOT (EQUAL A 0)) (NUMBERP A)) (LESSP (LOG 2 (REMAINDER A B)) (ADD1 (LOG 2 (QUOTIENT A 2))))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.2 0.0 ] GCD-T-SHRINK-2 (DEFN GCD-T2 (A B) (IF (ZEROP A) 6 (IF (ZEROP B) 9 (IF (LESSP B A) (PLUS 9 (GCD-T2 (REMAINDER A B) B)) (IF (LESSP A B) (PLUS 9 (GCD-T2 A (REMAINDER B A))) 18)))) ((LESSP (PLUS A B)))) Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP inform us that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each recursive call. Hence, GCD-T2 is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (GCD-T2 A B)) is a theorem. [ 0.0 0.0 0.0 ] GCD-T2 (PROVE-LEMMA GCD-T2-UB NIL (LEQ (GCD-T2 A B) (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))))) Give the conjecture the name *1. We will appeal to induction. There are three plausible inductions, all of which are unflawed. However, one of these is more likely than the others. We will induct according to the following scheme: (AND (IMPLIES (ZEROP A) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (p (REMAINDER A B) B)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (LESSP A B) (p A (REMAINDER B A))) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (p A B))). Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP establish that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following five new formulas: Case 5. (IMPLIES (ZEROP A) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))). This simplifies, rewriting with PLUS-0, and unfolding the definitions of ZEROP, LOG, EQUAL, GCD-T2, LESSP, and NUMBERP, to two new goals: Case 5.2. (IMPLIES (EQUAL A 0) (NOT (LESSP (PLUS 18 (TIMES 9 (LOG 2 B))) 6))), which again simplifies, using linear arithmetic, to: T. Case 5.1. (IMPLIES (NOT (NUMBERP A)) (NOT (LESSP (PLUS 18 (TIMES 9 (LOG 2 B))) 6))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))), which simplifies, applying PLUS-0 and PLUS-COMMUTATIVITY, and opening up ZEROP, LOG, EQUAL, GCD-T2, LESSP, and NUMBERP, to the following two new formulas: Case 4.2. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (EQUAL B 0)) (NOT (LESSP (PLUS 18 (TIMES 9 (LOG 2 A))) 9))). However this again simplifies, using linear arithmetic, to: T. Case 4.1. (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (NUMBERP B))) (NOT (LESSP (PLUS 18 (TIMES 9 (LOG 2 A))) 9))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 (REMAINDER A B)) (LOG 2 B)))) (GCD-T2 (REMAINDER A B) B)))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))), which simplifies, applying the lemma PLUS-COMMUTATIVITY, and expanding the functions ZEROP and GCD-T2, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (LESSP B A) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 B) (LOG 2 (REMAINDER A B))))) (GCD-T2 (REMAINDER A B) B)))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (PLUS 9 (GCD-T2 (REMAINDER A B) B))))). But this again simplifies, using linear arithmetic and applying GCD-T-SHRINK-2 and PLUS-COMMUTATIVITY, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (LESSP A B) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 (REMAINDER B A))))) (GCD-T2 A (REMAINDER B A))))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))). This simplifies, opening up ZEROP and GCD-T2, to: (IMPLIES (AND (NOT (EQUAL A 0)) (NUMBERP A) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP B A)) (LESSP A B) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 (REMAINDER B A))))) (GCD-T2 A (REMAINDER B A))))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (PLUS 9 (GCD-T2 A (REMAINDER B A)))))), which again simplifies, using linear arithmetic and rewriting with GCD-T-SHRINK-2, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))). This simplifies, using linear arithmetic, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))). However this again simplifies, expanding the definition of ZEROP, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B)))), which again simplifies, expanding ZEROP, to: T. Case 1.1. (IMPLIES (AND (NUMBERP A) (NUMBERP B) (NOT (ZEROP A)) (NOT (ZEROP A)) (NOT (LESSP A A)) (NOT (LESSP A A))) (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 A)))) (GCD-T2 A A)))), which again simplifies, rewriting with the lemma CORRECTNESS-OF-CANCEL-LESSP-PLUS, and unfolding the definitions of ZEROP and GCD-T2, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.2 0.0 ] GCD-T2-UB (PROVE-LEMMA GCD-T1-T2 (REWRITE) (EQUAL (GCD-T1 A B) (GCD-T2 A B)) ((ENABLE SPLUS))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP A) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (p (REMAINDER A B) B)) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (LESSP A B) (p A (REMAINDER B A))) (p A B)) (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (p A B))). Linear arithmetic, the lemmas CORRECTNESS-OF-CANCEL-LESSP-PLUS, PLUS-COMMUTATIVITY, and REMAINDER-LESSP-LINEAR, and the definitions of FIX and ZEROP inform us that the measure (PLUS A B) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following five new conjectures: Case 5. (IMPLIES (ZEROP A) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). This simplifies, expanding the functions ZEROP, EQUAL, GCD-T1, and GCD-T2, to: T. Case 4. (IMPLIES (AND (NOT (ZEROP A)) (ZEROP B)) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). This simplifies, opening up ZEROP, EQUAL, GCD-T1, and GCD-T2, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (LESSP B A) (EQUAL (GCD-T1 (REMAINDER A B) B) (GCD-T2 (REMAINDER A B) B))) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). This simplifies, unfolding the definitions of ZEROP, GCD-T1, SPLUS, and GCD-T2, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (LESSP A B) (EQUAL (GCD-T1 A (REMAINDER B A)) (GCD-T2 A (REMAINDER B A)))) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). This simplifies, unfolding the definitions of ZEROP, GCD-T1, SPLUS, and GCD-T2, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). This simplifies, using linear arithmetic, to the following three new goals: Case 1.3. (IMPLIES (AND (NOT (NUMBERP B)) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (EQUAL (GCD-T1 A B) (GCD-T2 A B))). However this again simplifies, unfolding the function ZEROP, to: T. Case 1.2. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (ZEROP A)) (NOT (ZEROP B)) (NOT (LESSP B A)) (NOT (LESSP A B))) (EQUAL (GCD-T1 A B) (GCD-T2 A B))), which again simplifies, expanding the definition of ZEROP, to: T. Case 1.1. (IMPLIES (AND (NUMBERP A) (NUMBERP B) (NOT (ZEROP A)) (NOT (ZEROP A)) (NOT (LESSP A A)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) (GCD-T2 A A))), which again simplifies, unfolding ZEROP and GCD-T2, to: (IMPLIES (AND (NUMBERP A) (NUMBERP B) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)). Eliminate the irrelevant term. We would thus like to prove the new conjecture: (IMPLIES (AND (NUMBERP A) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)), which we will name *1.1. Perhaps we can prove it by induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL A 0) (NOT (NUMBERP A))) (p A)) (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (p (SUB1 A))) (p A))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT can be used to establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to four new conjectures: Case 4. (IMPLIES (AND (OR (EQUAL A 0) (NOT (NUMBERP A))) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)), which simplifies, opening up the definitions of NOT and OR, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (EQUAL (SUB1 A) 0) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)), which simplifies, appealing to the lemma SUB1-OF-1, and unfolding the functions NOT, OR, NUMBERP, EQUAL, LESSP, and GCD-T1, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (LESSP (SUB1 A) (SUB1 A)) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)), which simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A)))) (EQUAL (GCD-T1 (SUB1 A) (SUB1 A)) 18) (NUMBERP A) (NOT (EQUAL A 0)) (NOT (LESSP A A))) (EQUAL (GCD-T1 A A) 18)), which simplifies, rewriting with REMAINDER-X-X, and unfolding NOT, OR, LESSP, SPLUS, GCD-T1, EQUAL, and PLUS, to: T. That finishes the proof of *1.1, which also finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] GCD-T1-T2 (PROVE-LEMMA GCD-T-UB NIL (LEQ (GCD-T A B) (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B))))) ((USE (GCD-T2-UB)) (ENABLE GCD-T SPLUS))) This conjecture can be simplified, using the abbreviations GCD-T1-T2, SPLUS, and GCD-T, to: (IMPLIES (NOT (LESSP (PLUS 18 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T2 A B))) (NOT (LESSP (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (PLUS 4 (GCD-T2 A B))))). This simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GCD-T-UB (PROVE-LEMMA GCD-T-UBOUND-LA NIL (IMPLIES (AND (LEQ A A1) (LEQ B B1)) (LEQ (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (PLUS 22 (TIMES 9 (PLUS (LOG 2 A1) (LOG 2 B1))))))) This formula can be simplified, using the abbreviations TIMES-LESSP-CANCEL, AND, IMPLIES, and PLUS-LESSP-CANCEL-1, to: (IMPLIES (AND (NOT (LESSP A1 A)) (NOT (LESSP B1 B)) (NOT (EQUAL 9 0)) (NUMBERP 9)) (NOT (LESSP (PLUS (LOG 2 A1) (LOG 2 B1)) (PLUS (LOG 2 A) (LOG 2 B))))), which simplifies, using linear arithmetic and applying the lemma LOG-LEQ, to: T. Q.E.D. [ 0.0 0.0 0.0 ] GCD-T-UBOUND-LA (PROVE-LEMMA GCD-T-UBOUND NIL (IMPLIES (AND (LESSP A (EXP 2 32)) (LESSP B (EXP 2 32))) (LEQ (GCD-T A B) 598)) ((USE (GCD-T-UBOUND-LA (A1 (EXP 2 32)) (B1 (EXP 2 32))) (GCD-T-UB)))) This formula can be simplified, using the abbreviations IMPLIES, AND, and PLUS-LESSP-CANCEL-1, to: (IMPLIES (AND (IMPLIES (AND (IF (LESSP (EXP 2 32) A) F T) (IF (LESSP (EXP 2 32) B) F T)) (IF (LESSP (TIMES 9 (PLUS (LOG 2 (EXP 2 32)) (LOG 2 (EXP 2 32)))) (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) F T)) (NOT (LESSP (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T A B))) (LESSP A (EXP 2 32)) (LESSP B (EXP 2 32))) (NOT (LESSP 598 (GCD-T A B)))), which simplifies, opening up the functions EXP, AND, LOG, PLUS, TIMES, and IMPLIES, to three new goals: Case 3. (IMPLIES (AND (LESSP 4294967296 A) (NOT (LESSP (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T A B))) (LESSP A 4294967296) (LESSP B 4294967296)) (NOT (LESSP 598 (GCD-T A B)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LESSP 4294967296 B) (NOT (LESSP (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T A B))) (LESSP A 4294967296) (LESSP B 4294967296)) (NOT (LESSP 598 (GCD-T A B)))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (LESSP 576 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B))))) (NOT (LESSP (PLUS 22 (TIMES 9 (PLUS (LOG 2 A) (LOG 2 B)))) (GCD-T A B))) (LESSP A 4294967296) (LESSP B 4294967296)) (NOT (LESSP 598 (GCD-T A B)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] GCD-T-UBOUND