(NOTE-LIB "unsolv") (DEFINE (^BM^SYMBOL X) (^BM^MEMBER X (^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))))))))) (DEFINE (^BM^HALF-TAPE X) (IF (^BM^NLISTP X) (EQUAL X (^INT (^BM^ZERO))) (^BM^AND (^BM^SYMBOL (^BM^CAR X)) (^BM^HALF-TAPE (^BM^CDR X))))) (DEFINE (^BM^TAPE X) (^BM^AND (^BM^LISTP X) (^BM^AND (^BM^HALF-TAPE (^BM^CAR X)) (^BM^HALF-TAPE (^BM^CDR X))))) (DEFINE (^BM^OPERATION X) (^BM^MEMBER X (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^ZERO))) (^BM^CONS (^BM^PACK (^BM^CONS (^R) (^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))))))))))) (DEFINE (^BM^STATE X) (^BM^LITATOM X)) (DEFINE (^BM^TURING-4TUPLE X) (^BM^AND (^BM^LISTP X) (^BM^AND (^BM^STATE (^BM^CAR X)) (^BM^AND (^BM^SYMBOL (^BM^CAR (^BM^CDR X))) (^BM^AND (^BM^OPERATION (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^AND (^BM^STATE (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR X))))) (EQUAL (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR X)))) (^NIL)))))))) (DEFINE (^BM^TURING-MACHINE X) (IF (^BM^NLISTP X) (EQUAL X (^NIL)) (^BM^AND (^BM^TURING-4TUPLE (^BM^CAR X)) (^BM^TURING-MACHINE (^BM^CDR X))))) (DEFINE (^BM^INSTR ST SYM TM) (IF (^BM^LISTP TM) (IF (EQUAL ST (^BM^CAR (^BM^CAR TM))) (IF (EQUAL SYM (^BM^CAR (^BM^CDR (^BM^CAR TM)))) (^BM^CDR (^BM^CDR (^BM^CAR TM))) (^BM^INSTR ST SYM (^BM^CDR TM))) (^BM^INSTR ST SYM (^BM^CDR TM))) (^BM^FALSE))) (DEFINE (^BM^NEW-TAPE OP TAPE) (IF (EQUAL OP (^BM^PACK (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^CDR (^BM^CAR TAPE)) (^BM^CONS (^BM^CAR (^BM^CAR TAPE)) (^BM^CDR TAPE))) (IF (EQUAL OP (^BM^PACK (^BM^CONS (^R) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^CAR (^BM^CDR TAPE)) (^BM^CAR TAPE)) (^BM^CDR (^BM^CDR TAPE))) (^BM^CONS (^BM^CAR TAPE) (^BM^CONS OP (^BM^CDR (^BM^CDR TAPE))))))) (DEFINE (^BM^TMI ST TAPE TM N) (IF (^BM^ZEROP N) (^BM^BTM) (IF (^BM^INSTR ST (^BM^CAR (^BM^CDR TAPE)) TM) (^BM^TMI (^BM^CAR (^BM^CDR (^BM^INSTR ST (^BM^CAR (^BM^CDR TAPE)) TM))) (^BM^NEW-TAPE (^BM^CAR (^BM^INSTR ST (^BM^CAR (^BM^CDR TAPE)) TM)) TAPE) TM (^BM^SUB1 N)) TAPE))) (DEFINE (^BM^INSTR-DEFN) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^P) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^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)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^F) (^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^NEW-TAPE-DEFN) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^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)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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)))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^R) (^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)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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 (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^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)))))))) (^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))))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (DEFINE (^BM^TMI-DEFN) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^CONS (^I) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^E) (^BM^CONS (^W) (^BM^CONS (^-) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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^KWOTE X) (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS X (^NIL)))) (DEFINE (^BM^TMI-FA TM) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^CONS (^NIL) (^BM^CONS (^BM^KWOTE TM) (^NIL)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^INSTR-DEFN)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^E) (^BM^CONS (^W) (^BM^CONS (^-) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))))))) (^BM^NEW-TAPE-DEFN)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^CONS (^I) (^BM^ZERO))))) (^BM^TMI-DEFN)) (^NIL)))))) (DEFINE (^BM^TMI-X ST TAPE) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^CONS (^I) (^BM^ZERO))))) (^BM^CONS (^BM^KWOTE ST) (^BM^CONS (^BM^KWOTE TAPE) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))) (^NIL)))))) (DEFINE (^BM^LENGTH X) (IF (^BM^NLISTP X) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^LENGTH (^BM^CDR X))))) (DEFINE (^BM^TMI-K ST TAPE TM N) (^BM^DIFFERENCE N (^BM^ADD1 (^BM^LENGTH TM)))) (DEFINE (^BM^TMI-N ST TAPE TM K) (^BM^PLUS K (^BM^ADD1 (^BM^LENGTH TM)))) (LEMMA (EQUAL (EQUAL (^BM^LENGTH X) (^INT (^BM^ZERO))) (^BM^NLISTP X))) (LEMMA (EQUAL (EQUAL (^BM^PLUS I J) (^INT (^BM^ZERO))) (^BM^AND (^BM^ZEROP I) (^BM^ZEROP J)))) (LEMMA (EQUAL (^BM^PLUS (^BM^DIFFERENCE I J) J) (IF (^BM^LEQ I J) (^BM^FIX J) I))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^ZEROP N) (^BM^AND (^BM^NOT (EQUAL FN (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))))) (^BM^AND (^BM^NOT (EQUAL FN (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))))) (^BM^AND (^BM^NOT (^BM^UNSOLV-SUBRP FN)) (EQUAL VARGS (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) ARGS VA FA N)))))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS FN ARGS) VA FA N) (^BM^BTM)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP N)) (^BM^AND (^BM^NOT (EQUAL FN (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))))) (^BM^AND (^BM^NOT (EQUAL FN (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))))) (^BM^AND (^BM^NOT (^BM^UNSOLV-SUBRP FN)) (EQUAL VARGS (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) ARGS VA FA N)))))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS FN ARGS) VA FA N) (IF (^BM^BTMP VARGS) (^BM^BTM) (IF (^BM^BTMP (^BM^GET FN FA)) (^BM^BTM) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^GET FN FA))) (^BM^PAIRLIST (^BM^CAR (^BM^GET FN FA)) VARGS) FA (^BM^SUB1 N))))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^UNSOLV-SUBRP FN) (EQUAL VARGS (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) ARGS VA FA N))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS FN ARGS) VA FA N) (IF (^BM^BTMP VARGS) (^BM^BTM) (^BM^UNSOLV-APPLY-SUBR FN VARGS))))) (LEMMA (^BM^IMPLIES (EQUAL VX1 (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X1 VA FA N)) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS X1 (^BM^CONS X2 (^BM^CONS X3 (^NIL))))) VA FA N) (IF (^BM^BTMP VX1) (^BM^BTM) (IF VX1 (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X2 VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X3 VA FA N)))))) (LEMMA (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS X (^NIL))) VA FA N) X)) (LEMMA (^BM^AND (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^INT (^BM^ZERO)) VA FA N) (^INT (^BM^ZERO))) (^BM^AND (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^ADD1 N) VA FA N) (^BM^ADD1 N)) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^PACK X) VA FA N) (IF (EQUAL (^BM^PACK X) (^BM^PACK (^BM^CONS (^T) (^BM^ZERO)))) (^BM^TRUE) (IF (EQUAL (^BM^PACK X) (^BM^PACK (^BM^CONS (^F) (^BM^ZERO)))) (^BM^FALSE) (IF (EQUAL (^BM^PACK X) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))) (^NIL) (^BM^GET (^BM^PACK X) VA)))))))) (LEMMA (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^NIL) VA FA N) (^NIL))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL VX (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X VA FA N)) (EQUAL VL (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) L VA FA N))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CONS X L) VA FA N) (IF (^BM^BTMP VX) (^BM^BTM) (IF (^BM^BTMP VL) (^BM^BTM) (^BM^CONS VX VL)))))) (DEFINE (^BM^CNB X) (IF (^BM^LISTP X) (^BM^AND (^BM^CNB (^BM^CAR X)) (^BM^CNB (^BM^CDR X))) (^BM^NOT (^BM^BTMP X)))) (LEMMA (^BM^IMPLIES (^BM^CNB X) (EQUAL (^BM^BTMP X) (^BM^FALSE)))) (LEMMA (^BM^AND (EQUAL (^BM^CNB (^BM^CONS A B)) (^BM^AND (^BM^CNB A) (^BM^CNB B))) (^BM^AND (^BM^IMPLIES (^BM^CNB X) (^BM^CNB (^BM^CAR X))) (^BM^IMPLIES (^BM^CNB X) (^BM^CNB (^BM^CDR X)))))) (LEMMA (^BM^IMPLIES (^BM^LITATOM X) (^BM^CNB X))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP X) (^BM^CNB X))) (LEMMA (^BM^AND (EQUAL (^BM^GET (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^TMI-FA TM)) (^BM^CONS (^NIL) (^BM^CONS (^BM^KWOTE TM) (^NIL)))) (^BM^AND (EQUAL (^BM^GET (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^TMI-FA TM)) (^BM^INSTR-DEFN)) (^BM^AND (EQUAL (^BM^GET (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^E) (^BM^CONS (^W) (^BM^CONS (^-) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))))))) (^BM^TMI-FA TM)) (^BM^NEW-TAPE-DEFN)) (EQUAL (^BM^GET (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^CONS (^I) (^BM^ZERO))))) (^BM^TMI-FA TM)) (^BM^TMI-DEFN)))))) (DEFINE (^BM^INSTRN ST SYM TM N) (IF (^BM^ZEROP N) (^BM^BTM) (IF (^BM^LISTP TM) (IF (EQUAL ST (^BM^CAR (^BM^CAR TM))) (IF (EQUAL SYM (^BM^CAR (^BM^CDR (^BM^CAR TM)))) (^BM^CDR (^BM^CDR (^BM^CAR TM))) (^BM^INSTRN ST SYM (^BM^CDR TM) (^BM^SUB1 N))) (^BM^INSTRN ST SYM (^BM^CDR TM) (^BM^SUB1 N))) (^BM^FALSE)))) (DEFINE (^BM^PR-EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N) (IF (^BM^ZEROP N) (^BM^TRUE) (^BM^PR-EVAL-INSTR-INDUCTION-SCHEME (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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 (^T) (^BM^ZERO)))) (^BM^PR-EVAL ST VA (^BM^TMI-FA TM) N)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^Y) (^BM^CONS (^M) (^BM^ZERO))))) (^BM^PR-EVAL SYM VA (^BM^TMI-FA TM) N)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^PR-EVAL TM-- VA (^BM^TMI-FA TM) N)) (^NIL)))) TM (^BM^SUB1 N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) ST VA (^BM^TMI-FA TM) N)) (^BM^AND (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) SYM VA (^BM^TMI-FA TM) N)) (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TM-- VA (^BM^TMI-FA TM) N)))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS ST (^BM^CONS SYM (^BM^CONS TM-- (^NIL))))) VA (^BM^TMI-FA TM) N) (^BM^INSTRN (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) ST VA (^BM^TMI-FA TM) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) SYM VA (^BM^TMI-FA TM) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TM-- VA (^BM^TMI-FA TM) N) N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) OP VA (^BM^TMI-FA TM) N)) (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TAPE VA (^BM^TMI-FA TM) N))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^E) (^BM^CONS (^W) (^BM^CONS (^-) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))))))) (^BM^CONS OP (^BM^CONS TAPE (^NIL)))) VA (^BM^TMI-FA TM) N) (IF (^BM^ZEROP N) (^BM^BTM) (^BM^NEW-TAPE (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) OP VA (^BM^TMI-FA TM) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TAPE VA (^BM^TMI-FA TM) N)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^BTMP (^BM^INSTRN ST SYM TM N))) (^BM^CNB TM)) (^BM^CNB (^BM^INSTRN ST SYM TM N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^CNB OP) (^BM^CNB TAPE)) (^BM^CNB (^BM^NEW-TAPE OP TAPE)))) (DEFINE (^BM^TMIN ST TAPE TM N) (IF (^BM^ZEROP N) (^BM^BTM) (IF (^BM^BTMP (^BM^INSTRN ST (^BM^CAR (^BM^CDR TAPE)) TM (^BM^SUB1 N))) (^BM^BTM) (IF (^BM^INSTRN ST (^BM^CAR (^BM^CDR TAPE)) TM (^BM^SUB1 N)) (^BM^TMIN (^BM^CAR (^BM^CDR (^BM^INSTRN ST (^BM^CAR (^BM^CDR TAPE)) TM (^BM^SUB1 N)))) (^BM^NEW-TAPE (^BM^CAR (^BM^INSTRN ST (^BM^CAR (^BM^CDR TAPE)) TM (^BM^SUB1 N))) TAPE) TM (^BM^SUB1 N)) TAPE)))) (DEFINE (^BM^PR-EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N) (IF (^BM^ZEROP N) (^BM^TRUE) (^BM^PR-EVAL-TMI-INDUCTION-SCHEME (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^E) (^BM^CONS (^W) (^BM^CONS (^-) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^R) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^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))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) ST VA (^BM^TMI-FA TM) N)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^P) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TAPE VA (^BM^TMI-FA TM) N)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^ZERO)))) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TM-- VA (^BM^TMI-FA TM) N)) (^NIL)))) TM (^BM^SUB1 N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) ST VA (^BM^TMI-FA TM) N)) (^BM^AND (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TAPE VA (^BM^TMI-FA TM) N)) (^BM^CNB (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TM-- VA (^BM^TMI-FA TM) N)))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^M) (^BM^CONS (^I) (^BM^ZERO))))) (^BM^CONS ST (^BM^CONS TAPE (^BM^CONS TM-- (^NIL))))) VA (^BM^TMI-FA TM) N) (^BM^TMIN (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) ST VA (^BM^TMI-FA TM) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TAPE VA (^BM^TMI-FA TM) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) TM-- VA (^BM^TMI-FA TM) N) N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^CNB ST) (^BM^AND (^BM^CNB TAPE) (^BM^CNB TM))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^TMI-X ST TAPE) (^NIL) (^BM^TMI-FA TM) N) (IF (^BM^ZEROP N) (^BM^BTM) (^BM^TMIN ST TAPE TM N))))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^LENGTH TM) N) (EQUAL (^BM^INSTRN ST SYM TM N) (^BM^INSTR ST SYM TM)))) (LEMMA (^BM^IMPLIES (^BM^TURING-MACHINE TM) (^BM^NOT (^BM^BTMP (^BM^INSTR ST SYM TM))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^TURING-MACHINE TM) (^BM^LEQ N (^BM^LENGTH TM))) (^BM^INSTRN ST SYM TM N))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^TURING-MACHINE TM) (^BM^LEQ N (^BM^LENGTH TM))) (EQUAL (^BM^TMIN ST TAPE TM N) (^BM^BTM)))) (LEMMA (^BM^IMPLIES (^BM^TURING-MACHINE TM) (EQUAL (^BM^TMI ST TAPE TM K) (^BM^TMIN ST TAPE TM (^BM^PLUS K (^BM^ADD1 (^BM^LENGTH TM))))))) (LEMMA (^BM^IMPLIES (^BM^SYMBOL SYM) (^BM^CNB SYM))) (LEMMA (^BM^IMPLIES (^BM^HALF-TAPE X) (^BM^CNB X))) (LEMMA (^BM^IMPLIES (^BM^TAPE X) (^BM^CNB X))) (LEMMA (^BM^IMPLIES (^BM^OPERATION OP) (^BM^CNB OP))) (LEMMA (^BM^IMPLIES (^BM^TURING-MACHINE TM) (^BM^CNB TM))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^STATE ST) (^BM^AND (^BM^TAPE TAPE) (^BM^TURING-MACHINE TM))) (^BM^AND (^BM^IMPLIES (^BM^NOT (^BM^BTMP (^BM^PR-EVAL (^BM^TMI-X ST TAPE) (^NIL) (^BM^TMI-FA TM) N))) (^BM^NOT (^BM^BTMP (^BM^TMI ST TAPE TM (^BM^TMI-K ST TAPE TM N))))) (^BM^IMPLIES (^BM^NOT (^BM^BTMP (^BM^TMI ST TAPE TM K))) (EQUAL (^BM^TMI ST TAPE TM K) (^BM^PR-EVAL (^BM^TMI-X ST TAPE) (^NIL) (^BM^TMI-FA TM) (^BM^TMI-N ST TAPE TM K)))))))