(NOTE-LIB "nqthm-boot") (DEFINE (^BM^STP X) (IF (CONSP X) (IF (EQUAL (CAR X) '^BM^ST) (IF (CONSP (CDR X)) (IF (^BM^NOT 'FALSE) (IF (CONSP (CDR (CDR X))) (IF (^BM^NOT 'FALSE) (IF (CONSP (CDR (CDR (CDR X)))) (IF (^BM^NOT 'FALSE) (IF (CONSP (CDR (CDR (CDR (CDR X))))) (IF (^BM^NOT 'FALSE) (IF (CONSP (CDR (CDR (CDR (CDR (CDR X)))))) (IF (^BM^NOT 'FALSE) (EQUAL (CDR (CDR (CDR (CDR (CDR (CDR X)))))) 'NIL) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE)) (DEFINE (^BM^ST T1595 T1596 T1597 T1598 T1599) (CONS '^BM^ST (CONS (IF (^BM^NOT 'FALSE) T1595 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1596 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1597 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1598 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1599 (^BM^ZERO)) 'NIL))))))) (DEFINE (^BM^PC X) (IF (^BM^STP X) (CAR (CDR X)) (^BM^ZERO))) (DEFINE (^BM^STK X) (IF (^BM^STP X) (CAR (CDR (CDR X))) (^BM^ZERO))) (DEFINE (^BM^MEM X) (IF (^BM^STP X) (CAR (CDR (CDR (CDR X)))) (^BM^ZERO))) (DEFINE (^BM^HALTEDP X) (IF (^BM^STP X) (CAR (CDR (CDR (CDR (CDR X))))) (^BM^ZERO))) (DEFINE (^BM^DEFS X) (IF (^BM^STP X) (CAR (CDR (CDR (CDR (CDR (CDR X)))))) (^BM^ZERO))) (DEFINE (^BM^ADD1-PC PC) (^BM^CONS (^BM^CAR PC) (^BM^ADD1 (^BM^CDR PC)))) (DEFINE (^BM^GET N LST) (IF (^BM^ZEROP N) (^BM^CAR LST) (^BM^GET (^BM^SUB1 N) (^BM^CDR LST)))) (DEFINE (^BM^PUT N V LST) (IF (^BM^ZEROP N) (^BM^CONS V (^BM^CDR LST)) (^BM^CONS (^BM^CAR LST) (^BM^PUT (^BM^SUB1 N) V (^BM^CDR LST))))) (DEFINE (^BM^FETCH PC DEFS) (^BM^GET (^BM^CDR PC) (^BM^CDR (^BM^ASSOC (^BM^CAR PC) DEFS)))) (DEFINE (^BM^MOVE ADDR1 ADDR2 S) (^BM^ST (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S) (^BM^PUT ADDR1 (^BM^GET ADDR2 (^BM^MEM S)) (^BM^MEM S)) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^MOVI ADDR VAL S) (^BM^ST (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S) (^BM^PUT ADDR VAL (^BM^MEM S)) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^ADD ADDR1 ADDR2 S) (^BM^ST (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S) (^BM^PUT ADDR1 (^BM^PLUS (^BM^GET ADDR1 (^BM^MEM S)) (^BM^GET ADDR2 (^BM^MEM S))) (^BM^MEM S)) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^SUBI ADDR VAL S) (^BM^ST (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S) (^BM^PUT ADDR (^BM^DIFFERENCE (^BM^GET ADDR (^BM^MEM S)) VAL) (^BM^MEM S)) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^JUMPZ ADDR PC S) (^BM^ST (IF (^BM^ZEROP (^BM^GET ADDR (^BM^MEM S))) (^BM^CONS (^BM^CAR (^BM^PC S)) PC) (^BM^ADD1-PC (^BM^PC S))) (^BM^STK S) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^JUMP PC S) (^BM^ST (^BM^CONS (^BM^CAR (^BM^PC S)) PC) (^BM^STK S) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^CALL SUBR S) (^BM^ST (^BM^CONS SUBR (^INT (^BM^ZERO))) (^BM^CONS (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S))) (DEFINE (^BM^RET S) (IF (^BM^NLISTP (^BM^STK S)) (^BM^ST (^BM^PC S) (^BM^STK S) (^BM^MEM S) (^BM^TRUE) (^BM^DEFS S)) (^BM^ST (^BM^CAR (^BM^STK S)) (^BM^CDR (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)))) (DEFINE (^BM^EXECUTE INS S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^MOVE (^BM^CAR (^BM^CDR INS)) (^BM^CAR (^BM^CDR (^BM^CDR INS))) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^MOVI (^BM^CAR (^BM^CDR INS)) (^BM^CAR (^BM^CDR (^BM^CDR INS))) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^ZERO)))))) (^BM^ADD (^BM^CAR (^BM^CDR INS)) (^BM^CAR (^BM^CDR (^BM^CDR INS))) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^SUBI (^BM^CAR (^BM^CDR INS)) (^BM^CAR (^BM^CDR (^BM^CDR INS))) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^Z) (^BM^ZERO)))))))) (^BM^JUMPZ (^BM^CAR (^BM^CDR INS)) (^BM^CAR (^BM^CDR (^BM^CDR INS))) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^ZERO))))))) (^BM^JUMP (^BM^CAR (^BM^CDR INS)) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CALL (^BM^CAR (^BM^CDR INS)) S) (IF (EQUAL (^BM^CAR INS) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^RET S) S))))))))) (DEFINE (^BM^STEP S) (IF (^BM^HALTEDP S) S (^BM^EXECUTE (^BM^FETCH (^BM^PC S) (^BM^DEFS S)) S))) (DEFINE (^BM^SM S N) (IF (^BM^ZEROP N) S (^BM^SM (^BM^STEP S) (^BM^SUB1 N)))) (LEMMA (^BM^AND (^BM^IMPLIES (^BM^HALTEDP S) (EQUAL (^BM^STEP S) S)) (^BM^IMPLIES (^BM^LISTP (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (EQUAL (^BM^STEP S) (IF (^BM^HALTEDP S) S (^BM^EXECUTE (^BM^FETCH (^BM^PC S) (^BM^DEFS S)) S)))))) (LEMMA (EQUAL (^BM^SM S (^BM^PLUS I J)) (^BM^SM (^BM^SM S I) J))) (LEMMA (EQUAL (^BM^SM S (^BM^ADD1 I)) (^BM^SM (^BM^STEP S) I))) (LEMMA (EQUAL (^BM^SM S (^INT (^BM^ZERO))) S)) (DEFINE (^BM^TIMES-PROGRAM) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^Z) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS (^INT (^BM^CONS (^5) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^ZERO))))) (^BM^CONS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))))))) (DEFINE (^BM^TIMES-FN I J ANS) (IF (^BM^ZEROP I) ANS (^BM^TIMES-FN (^BM^SUB1 I) J (^BM^PLUS ANS J)))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP ANS) (EQUAL (^BM^TIMES-FN I J ANS) (^BM^PLUS (^BM^TIMES I J) ANS)))) (LEMMA (EQUAL (^BM^PLUS X (^INT (^BM^ZERO))) (^BM^FIX X))) (DEFINE (^BM^TIMES-CLOCK I) (^BM^PLUS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PLUS (^BM^TIMES I (^INT (^BM^CONS (^4) (^BM^ZERO)))) (^INT (^BM^CONS (^2) (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I) (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM))) (EQUAL (^BM^SM (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 (^BM^CONS I (^BM^CONS J (^BM^CONS ANS (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS) (^BM^TIMES I (^INT (^BM^CONS (^4) (^BM^ZERO))))) (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS J (^BM^CONS (^BM^TIMES-FN I J ANS) (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS)))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^FETCH PC DEFS) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM)) (^BM^NUMBERP I))) (EQUAL (^BM^SM (^BM^ST PC STK (^BM^CONS I (^BM^CONS J (^BM^CONS R2 (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS) (^BM^TIMES-CLOCK I)) (^BM^ST (^BM^ADD1-PC PC) STK (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS J (^BM^CONS (^BM^TIMES I J) (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS)))) (DEFINE (^BM^EXP I J) (IF (^BM^ZEROP J) (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^TIMES (^BM^EXP I (^BM^SUB1 J)) I))) (DEFINE (^BM^EXP-PROGRAM) (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^Z) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^9) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))))))))))) (DEFINE (^BM^EXP-FN R0 R1 R2 R3 R4) (IF (^BM^ZEROP R4) R1 (^BM^EXP-FN (^INT (^BM^ZERO)) (^BM^TIMES R3 R1) (^BM^TIMES R3 R1) R3 (^BM^SUB1 R4)))) (LEMMA (EQUAL (^BM^TIMES (^BM^TIMES I J) K) (^BM^TIMES I (^BM^TIMES J K)))) (LEMMA (EQUAL (^BM^TIMES I (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^FIX I))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP R1) (EQUAL (^BM^EXP-FN R0 R1 R2 R3 R4) (^BM^TIMES (^BM^EXP R3 R4) R1)))) (DEFINE (^BM^EXP-CLOCK I J) (^BM^PLUS (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^PLUS (^BM^TIMES J (^BM^PLUS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PLUS (^BM^TIMES-CLOCK I) (^INT (^BM^CONS (^3) (^BM^ZERO)))))) (^INT (^BM^CONS (^2) (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP R3) (^BM^AND (^BM^NUMBERP R4) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) DEFS) (^BM^EXP-PROGRAM)) (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM))))) (EQUAL (^BM^SM (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) (^INT (^BM^CONS (^3) (^BM^ZERO)))) STK (^BM^CONS R0 (^BM^CONS R1 (^BM^CONS R2 (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS) (^BM^TIMES R4 (^BM^PLUS (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PLUS (^BM^TIMES-CLOCK R3) (^INT (^BM^CONS (^3) (^BM^ZERO))))))) (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) (^INT (^BM^CONS (^3) (^BM^ZERO)))) STK (IF (^BM^ZEROP R4) (^BM^CONS R0 (^BM^CONS R1 (^BM^CONS R2 (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS (^BM^TIMES (^BM^EXP R3 R4) R1) (^BM^CONS (^BM^TIMES (^BM^EXP R3 R4) R1) (^BM^CONS R3 (^BM^CONS (^INT (^BM^ZERO)) (^NIL))))))) (^BM^FALSE) DEFS)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I) (^BM^AND (^BM^NUMBERP J) (^BM^AND (EQUAL (^BM^FETCH PC DEFS) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^X) (^BM^CONS (^P) (^BM^ZERO))))) DEFS) (^BM^EXP-PROGRAM)) (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM)))))) (EQUAL (^BM^SM (^BM^ST PC STK (^BM^CONS I (^BM^CONS J (^BM^CONS R2 (^BM^CONS R3 (^BM^CONS R4 (^NIL)))))) (^BM^FALSE) DEFS) (^BM^EXP-CLOCK I J)) (^BM^ST (^BM^ADD1-PC PC) STK (IF (^BM^ZEROP J) (^BM^CONS I (^BM^CONS (^BM^EXP I J) (^BM^CONS R2 (^BM^CONS I (^BM^CONS (^INT (^BM^ZERO)) (^NIL)))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CONS (^BM^EXP I J) (^BM^CONS (^BM^EXP I J) (^BM^CONS I (^BM^CONS (^INT (^BM^ZERO)) (^NIL))))))) (^BM^FALSE) DEFS)))) (DEFINE (^BM^LENGTH LST) (IF (^BM^NLISTP LST) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^LENGTH (^BM^CDR LST))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LESSP ADDR (^BM^LENGTH MEM)) (EQUAL (^BM^GET ADDR MEM) VAL)) (EQUAL (^BM^PUT ADDR VAL MEM) MEM))) (LEMMA (EQUAL (^BM^PUT ADDR V2 (^BM^PUT ADDR V1 MEM)) (^BM^PUT ADDR V2 MEM))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP ADDR1) (^BM^AND (^BM^NUMBERP ADDR2) (^BM^NOT (EQUAL ADDR1 ADDR2)))) (EQUAL (^BM^PUT ADDR2 V2 (^BM^PUT ADDR1 V1 MEM)) (^BM^PUT ADDR1 V1 (^BM^PUT ADDR2 V2 MEM))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP ADDR1) (^BM^NUMBERP ADDR2)) (EQUAL (^BM^GET ADDR1 (^BM^PUT ADDR2 VAL MEM)) (IF (EQUAL ADDR1 ADDR2) VAL (^BM^GET ADDR1 MEM))))) (LEMMA (^BM^IMPLIES (^BM^LESSP ADDR (^BM^LENGTH MEM)) (EQUAL (^BM^LENGTH (^BM^PUT ADDR VAL MEM)) (^BM^LENGTH MEM)))) (LEMMA (EQUAL (^BM^DIFFERENCE X (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^SUB1 X))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I) (^BM^NOT (^BM^LESSP I J))) (EQUAL (^BM^PLUS J (^BM^DIFFERENCE I J)) I))) (LEMMA (EQUAL (^BM^PLUS (^BM^PLUS I J) K) (^BM^PLUS I (^BM^PLUS J K)))) (LEMMA (EQUAL (^BM^PLUS I J) (^BM^PLUS J I))) (LEMMA (EQUAL (^BM^PLUS I (^BM^PLUS K J)) (^BM^PLUS K (^BM^PLUS I J)))) (DEFINE (^BM^TIMES-MEM-FN-LOOP MEM) (IF (^BM^ZEROP (^BM^GET (^INT (^BM^ZERO)) MEM)) MEM (^BM^TIMES-MEM-FN-LOOP (^BM^PUT (^INT (^BM^ZERO)) (^BM^SUB1 (^BM^GET (^INT (^BM^ZERO)) MEM)) (^BM^PUT (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PLUS (^BM^GET (^INT (^BM^CONS (^2) (^BM^ZERO))) MEM) (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) MEM)) MEM))))) (DEFINE (^BM^TIMES-MEM-FN MEM) (^BM^TIMES-MEM-FN-LOOP (^BM^PUT (^INT (^BM^CONS (^2) (^BM^ZERO))) (^INT (^BM^ZERO)) MEM))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP (^BM^GET (^INT (^BM^ZERO)) MEM)) (^BM^AND (^BM^NUMBERP (^BM^GET (^INT (^BM^CONS (^2) (^BM^ZERO))) MEM)) (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^LENGTH MEM)))) (EQUAL (^BM^TIMES-MEM-FN-LOOP MEM) (^BM^PUT (^INT (^BM^ZERO)) (^INT (^BM^ZERO)) (^BM^PUT (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^PLUS (^BM^TIMES (^BM^GET (^INT (^BM^ZERO)) MEM) (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) MEM)) (^BM^GET (^INT (^BM^CONS (^2) (^BM^ZERO))) MEM)) MEM))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP (^BM^GET (^INT (^BM^ZERO)) MEM)) (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^LENGTH MEM))) (EQUAL (^BM^TIMES-MEM-FN MEM) (^BM^PUT (^INT (^BM^ZERO)) (^INT (^BM^ZERO)) (^BM^PUT (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^TIMES (^BM^GET (^INT (^BM^ZERO)) MEM) (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) MEM)) MEM))))) (DEFINE (^BM^TIMES-STEP S) (^BM^ST (^BM^ADD1-PC (^BM^PC S)) (^BM^STK S) (^BM^PUT (^INT (^BM^ZERO)) (^INT (^BM^ZERO)) (^BM^PUT (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^TIMES (^BM^GET (^INT (^BM^ZERO)) (^BM^MEM S)) (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^MEM S))) (^BM^MEM S))) (^BM^FALSE) (^BM^DEFS S))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP (^BM^GET (^INT (^BM^ZERO)) MEM)) (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM))) (EQUAL (^BM^SM (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 MEM (^BM^FALSE) DEFS) (^BM^TIMES (^BM^GET (^INT (^BM^ZERO)) MEM) (^INT (^BM^CONS (^4) (^BM^ZERO))))) (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 (^BM^TIMES-MEM-FN-LOOP MEM) (^BM^FALSE) DEFS)))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL R0 (^BM^GET (^INT (^BM^ZERO)) MEM)) (^BM^AND (^BM^NUMBERP (^BM^GET (^INT (^BM^ZERO)) MEM)) (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) DEFS) (^BM^TIMES-PROGRAM)))) (EQUAL (^BM^SM (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 MEM (^BM^FALSE) DEFS) (^BM^TIMES R0 (^INT (^BM^CONS (^4) (^BM^ZERO))))) (^BM^ST (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO)))) STK1 (^BM^TIMES-MEM-FN-LOOP MEM) (^BM^FALSE) DEFS)))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^FETCH (^BM^PC S) (^BM^DEFS S)) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^DEFS S)) (^BM^TIMES-PROGRAM)) (^BM^AND (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^LENGTH (^BM^MEM S))) (^BM^AND (EQUAL R0 (^BM^GET (^INT (^BM^ZERO)) (^BM^MEM S))) (^BM^AND (^BM^NUMBERP R0) (^BM^AND (^BM^NOT (^BM^LESSP N (^BM^TIMES-CLOCK R0))) (^BM^NOT (^BM^HALTEDP S)))))))) (EQUAL (^BM^SM S N) (^BM^SM (^BM^TIMES-STEP S) (^BM^DIFFERENCE N (^BM^TIMES-CLOCK R0)))))) (LEMMA (^BM^AND (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I0) (^BM^NUMBERP I1)) (^BM^AND (^BM^NUMBERP (^INT (^BM^ZERO))) (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS (^INT (^BM^ZERO)) (^BM^TIMES I0 I1))))) (^BM^AND (^BM^IMPLIES (^BM^AND (^BM^NUMBERP R2) (^BM^AND (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS R2 (^BM^TIMES R0 R1))) (^BM^NOT (^BM^ZEROP R0)))) (^BM^AND (^BM^NUMBERP (^BM^PLUS R2 R1)) (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS (^BM^PLUS R2 R1) (^BM^TIMES (^BM^SUB1 R0) R1))))) (^BM^IMPLIES (^BM^AND (^BM^NUMBERP R2) (^BM^AND (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS R2 (^BM^TIMES R0 R1))) (^BM^ZEROP R0))) (EQUAL R2 (^BM^TIMES I0 I1)))))) (DEFINE (^BM^P S) (^BM^TRUE)) (LEMMA (^BM^IMPLIES (^BM^P S) (^BM^P (^BM^STEP S)))) (LEMMA (^BM^IMPLIES (^BM^P S0) (^BM^P (^BM^SM S0 N)))) (DEFINE (^BM^R0 S) (^BM^GET (^INT (^BM^ZERO)) (^BM^MEM S))) (DEFINE (^BM^R1 S) (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^MEM S))) (DEFINE (^BM^R2 S) (^BM^GET (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^MEM S))) (DEFINE (^BM^TIMESP I0 I1 S) (^BM^AND (^BM^NUMBERP I0) (^BM^AND (^BM^NUMBERP I1) (^BM^AND (^BM^STP S) (^BM^AND (^BM^NLISTP (^BM^STK S)) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^DEFS S)) (^BM^TIMES-PROGRAM)) (^BM^AND (EQUAL I1 (^BM^R1 S)) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^ZERO)))) (EQUAL I0 (^BM^R0 S)) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^AND (^BM^NUMBERP (^BM^R2 S)) (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS (^BM^R2 S) (^BM^TIMES (^BM^R0 S) (^BM^R1 S))))) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^2) (^BM^ZERO))))) (^BM^AND (^BM^NOT (^BM^ZEROP (^BM^R0 S))) (^BM^AND (^BM^NUMBERP (^BM^R2 S)) (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS (^BM^R2 S) (^BM^TIMES (^BM^R0 S) (^BM^R1 S)))))) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^3) (^BM^ZERO))))) (^BM^AND (^BM^NOT (^BM^ZEROP (^BM^R0 S))) (^BM^AND (^BM^NUMBERP (^BM^R2 S)) (EQUAL (^BM^PLUS I1 (^BM^TIMES I0 I1)) (^BM^PLUS (^BM^R2 S) (^BM^TIMES (^BM^R0 S) (^BM^R1 S)))))) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^4) (^BM^ZERO))))) (^BM^AND (^BM^NUMBERP (^BM^R2 S)) (EQUAL (^BM^TIMES I0 I1) (^BM^PLUS (^BM^R2 S) (^BM^TIMES (^BM^R0 S) (^BM^R1 S))))) (IF (EQUAL (^BM^PC S) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^5) (^BM^ZERO))))) (EQUAL (^BM^R2 S) (^BM^TIMES I0 I1)) (^BM^FALSE)))))))))))))) (LEMMA (^BM^IMPLIES (^BM^TIMESP I0 I1 S) (^BM^TIMESP I0 I1 (^BM^STEP S)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^STP S0) (^BM^AND (^BM^NLISTP (^BM^STK S0)) (^BM^AND (EQUAL (^BM^ASSOC (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^DEFS S0)) (^BM^TIMES-PROGRAM)) (^BM^AND (EQUAL I0 (^BM^GET (^INT (^BM^ZERO)) (^BM^MEM S0))) (^BM^AND (EQUAL I1 (^BM^GET (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^MEM S0))) (^BM^AND (^BM^NUMBERP I0) (^BM^AND (^BM^NUMBERP I1) (^BM^AND (EQUAL (^BM^PC S0) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^ZERO)))) (EQUAL (^BM^PC (^BM^SM S0 N)) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^I) (^BM^CONS (^M) (^BM^CONS (^E) (^BM^CONS (^S) (^BM^ZERO))))))) (^INT (^BM^CONS (^5) (^BM^ZERO))))))))))))) (EQUAL (^BM^GET (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^MEM (^BM^SM S0 N))) (^BM^TIMES I0 I1)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^HALTEDP (^BM^STEP S))) (^BM^NOT (^BM^HALTEDP S)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^HALTEDP (^BM^SM S N))) (^BM^NOT (^BM^HALTEDP S)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S)) (^BM^AND (^BM^HALTEDP (^BM^STEP S)) (EQUAL DEFS (^BM^DEFS S)))) (EQUAL (^BM^CAR (^BM^GET (^BM^CDR (^BM^PC S)) (^BM^CDR (^BM^ASSOC (^BM^CAR (^BM^PC S)) DEFS)))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))))) (DEFINE (^BM^K S D N) (IF (^BM^ZEROP N) (^INT (^BM^ZERO)) (IF (^BM^AND (EQUAL (^BM^LENGTH (^BM^STK S)) D) (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))))) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^K (^BM^STEP S) D (^BM^SUB1 N)))))) (LEMMA (EQUAL (^BM^LENGTH (^BM^STK (^BM^STEP S))) (IF (^BM^HALTEDP S) (^BM^LENGTH (^BM^STK S)) (IF (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^SUB1 (^BM^LENGTH (^BM^STK S))) (IF (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^ADD1 (^BM^LENGTH (^BM^STK S))) (^BM^LENGTH (^BM^STK S))))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP D) (^BM^AND (^BM^NOT (^BM^LESSP (^BM^LENGTH (^BM^STK S0)) D)) (^BM^LESSP (^BM^LENGTH (^BM^STK (^BM^SM S0 N))) D))) (^BM^LESSP (^BM^K S0 D N) N))) (LEMMA (EQUAL (^BM^DEFS (^BM^STEP S)) (^BM^DEFS S))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^K S0 D N) N) (^BM^AND (EQUAL (^BM^LENGTH (^BM^STK (^BM^SM S0 (^BM^K S0 D N)))) D) (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC (^BM^SM S0 (^BM^K S0 D N))) (^BM^DEFS S0))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))))))) (LEMMA (^BM^IMPLIES (^BM^HALTEDP S) (^BM^HALTEDP (^BM^SM S N)))) (LEMMA (^BM^IMPLIES (^BM^HALTEDP S) (EQUAL (^BM^K S D N) (IF (^BM^AND (EQUAL (^BM^LENGTH (^BM^STK S)) D) (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))))) (^INT (^BM^ZERO)) (^BM^FIX N))))) (LEMMA (^BM^IMPLIES (^BM^HALTEDP (^BM^STEP S0)) (EQUAL (^BM^LENGTH (^BM^STK (^BM^STEP S0))) (^BM^LENGTH (^BM^STK S0))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S0)) (^BM^LESSP (^BM^K S0 D N) N)) (^BM^NOT (^BM^HALTEDP (^BM^SM S0 (^BM^K S0 D N)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S0)) (^BM^LESSP (^BM^LENGTH (^BM^STK (^BM^SM S0 N))) (^BM^LENGTH (^BM^STK S0)))) (^BM^AND (^BM^LESSP (^BM^K S0 (^BM^LENGTH (^BM^STK S0)) N) N) (^BM^AND (EQUAL (^BM^LENGTH (^BM^STK (^BM^SM S0 (^BM^K S0 (^BM^LENGTH (^BM^STK S0)) N)))) (^BM^LENGTH (^BM^STK S0))) (^BM^AND (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC (^BM^SM S0 (^BM^K S0 (^BM^LENGTH (^BM^STK S0)) N))) (^BM^DEFS S0))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^NOT (^BM^HALTEDP (^BM^SM S0 (^BM^K S0 (^BM^LENGTH (^BM^STK S0)) N))))))))) (DEFINE (^BM^GROW-STK S STK) (^BM^ST (^BM^PC S) (^BM^APPEND (^BM^STK S) STK) (^BM^MEM S) (^BM^HALTEDP S) (^BM^DEFS S))) (LEMMA (EQUAL (^BM^LISTP (^BM^APPEND A B)) (^BM^OR (^BM^LISTP A) (^BM^LISTP B)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^HALTEDP (^BM^STEP S))) (EQUAL (^BM^STEP (^BM^GROW-STK S STK)) (^BM^GROW-STK (^BM^STEP S) STK)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^HALTEDP (^BM^SM S N))) (EQUAL (^BM^SM (^BM^GROW-STK S STK) N) (^BM^GROW-STK (^BM^SM S N) STK)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP N K)) (^BM^HALTEDP (^BM^SM S K))) (^BM^HALTEDP (^BM^SM S N)))) (LEMMA (EQUAL (EQUAL (^BM^LENGTH X) (^INT (^BM^ZERO))) (^BM^NLISTP X))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S)) (^BM^AND (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^NLISTP (^BM^STK S)))) (^BM^HALTEDP (^BM^STEP S)))) (LEMMA (EQUAL (^BM^DEFS (^BM^SM S N)) (^BM^DEFS S))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LESSP K (^BM^SUB1 N)) (^BM^AND (^BM^NOT (^BM^HALTEDP (^BM^SM S K))) (^BM^AND (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC (^BM^SM S K)) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (EQUAL (^BM^LENGTH (^BM^STK (^BM^SM S K))) (^INT (^BM^ZERO)))))) (^BM^HALTEDP (^BM^SM S N)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^HALTEDP (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^NIL) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) K))) (EQUAL (^BM^PC (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^NIL) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) K)) (^BM^PC (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^PC S)) (^BM^ADD1 (^BM^CDR (^BM^PC S)))) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) K))))) (LEMMA (EQUAL (^BM^LENGTH (^BM^APPEND A B)) (^BM^PLUS (^BM^LENGTH A) (^BM^LENGTH B)))) (LEMMA (^BM^AND (EQUAL (^BM^PC (^BM^GROW-STK S STK)) (^BM^PC S)) (^BM^AND (EQUAL (^BM^STK (^BM^GROW-STK S STK)) (^BM^APPEND (^BM^STK S) STK)) (^BM^AND (EQUAL (^BM^MEM (^BM^GROW-STK S STK)) (^BM^MEM S)) (^BM^AND (EQUAL (^BM^HALTEDP (^BM^GROW-STK S STK)) (^BM^HALTEDP S)) (EQUAL (^BM^DEFS (^BM^GROW-STK S STK)) (^BM^DEFS S))))))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^INT (^BM^ZERO)) (^BM^LENGTH (^BM^STK S))) (EQUAL (^BM^STEP (^BM^GROW-STK S STK)) (^BM^GROW-STK (^BM^STEP S) STK)))) (LEMMA (^BM^IMPLIES (^BM^NOT (EQUAL (^BM^CAR (^BM^FETCH (^BM^PC S) (^BM^DEFS S))) (^BM^PACK (^BM^CONS (^R) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO))))))) (EQUAL (^BM^STEP (^BM^GROW-STK S STK)) (^BM^GROW-STK (^BM^STEP S) STK)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP D) (^BM^NOT (^BM^LESSP (^BM^LENGTH (^BM^STK S)) D))) (EQUAL (^BM^K (^BM^GROW-STK S STK) (^BM^PLUS D (^BM^LENGTH STK)) N) (^BM^K S D N)))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^K (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^PC S)) (^BM^ADD1 (^BM^CDR (^BM^PC S)))) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^ADD1 (^BM^LENGTH (^BM^STK S))) (^BM^SUB1 N)) (^BM^SUB1 N)) (EQUAL (^BM^LISTP (^BM^STK (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^NIL) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^K (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^PC S)) (^BM^ADD1 (^BM^CDR (^BM^PC S)))) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^ADD1 (^BM^LENGTH (^BM^STK S))) (^BM^SUB1 N))))) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^K (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^PC S)) (^BM^ADD1 (^BM^CDR (^BM^PC S)))) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^ADD1 (^BM^LENGTH (^BM^STK S))) (^BM^SUB1 N)) (^BM^SUB1 N)) (EQUAL (^BM^HALTEDP (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^NIL) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^K (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^PC S)) (^BM^ADD1 (^BM^CDR (^BM^PC S)))) (^BM^STK S)) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) (^BM^ADD1 (^BM^LENGTH (^BM^STK S))) (^BM^SUB1 N)))) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S)) (^BM^AND (EQUAL (^BM^FETCH (^BM^PC S) (^BM^DEFS S)) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS PROG (^NIL)))) (^BM^AND (^BM^NOT (^BM^ZEROP N)) (EQUAL (^BM^STK (^BM^SM S N)) (^BM^STK S))))) (^BM^HALTEDP (^BM^SM (^BM^ST (^BM^CONS PROG (^INT (^BM^ZERO))) (^NIL) (^BM^MEM S) (^BM^FALSE) (^BM^DEFS S)) N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^HALTEDP S)) (^BM^AND (EQUAL (^BM^FETCH (^BM^PC S) (^BM^DEFS S)) (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^CONS I (^NIL)))) (^BM^AND (^BM^NUMBERP I) (EQUAL (^BM^CDR (^BM^PC S)) I)))) (^BM^NOT (^BM^HALTEDP (^BM^SM S N)))))