(NOTE-LIB "nqthm-boot") (DEFINE (^BM^FROM-TO I J) (IF (^BM^LESSP J I) (^NIL) (IF (EQUAL (^BM^FIX I) (^BM^FIX J)) (^BM^CONS (^BM^FIX J) (^NIL)) (^BM^APPEND (^BM^FROM-TO I (^BM^SUB1 J)) (^BM^CONS J (^NIL)))))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP Y)) (EQUAL (^BM^PLUS X Y) (^BM^FIX X)))) (LEMMA (EQUAL (^BM^PLUS X (^BM^ADD1 Y)) (IF (^BM^NUMBERP Y) (^BM^ADD1 (^BM^PLUS X Y)) (^BM^ADD1 X)))) (LEMMA (EQUAL (^BM^PLUS X (^BM^PLUS Y Z)) (^BM^PLUS Y (^BM^PLUS X Z)))) (LEMMA (EQUAL (^BM^PLUS X Y) (^BM^PLUS Y X))) (LEMMA (EQUAL (^BM^PLUS (^BM^PLUS X Y) Z) (^BM^PLUS X (^BM^PLUS Y Z)))) (LEMMA (EQUAL (EQUAL (^BM^PLUS A B) (^INT (^BM^ZERO))) (^BM^AND (^BM^ZEROP A) (^BM^ZEROP B)))) (LEMMA (EQUAL (^BM^DIFFERENCE X X) (^INT (^BM^ZERO)))) (LEMMA (^BM^AND (EQUAL (^BM^DIFFERENCE (^BM^PLUS X Y) X) (^BM^FIX Y)) (EQUAL (^BM^DIFFERENCE (^BM^PLUS Y X) X) (^BM^FIX Y)))) (LEMMA (EQUAL (EQUAL (^BM^PLUS A B) (^BM^PLUS A C)) (EQUAL (^BM^FIX B) (^BM^FIX C)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^LESSP Y X)) (EQUAL (^BM^DIFFERENCE X Y) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (EQUAL (^INT (^BM^ZERO)) (^BM^DIFFERENCE X Y)) (^BM^NOT (^BM^LESSP Y X)))) (LEMMA (EQUAL (EQUAL X (^BM^DIFFERENCE X Y)) (^BM^AND (^BM^NUMBERP X) (^BM^OR (EQUAL X (^INT (^BM^ZERO))) (^BM^ZEROP Y))))) (LEMMA (EQUAL (EQUAL (^BM^DIFFERENCE X Y) (^BM^DIFFERENCE Z Y)) (IF (^BM^LESSP X Y) (^BM^NOT (^BM^LESSP Y Z)) (IF (^BM^LESSP Z Y) (^BM^NOT (^BM^LESSP Y X)) (EQUAL (^BM^FIX X) (^BM^FIX Z)))))) (DEFINE (^BM^DELETE X Y) (IF (^BM^LISTP Y) (IF (EQUAL X (^BM^CAR Y)) (^BM^CDR Y) (^BM^CONS (^BM^CAR Y) (^BM^DELETE X (^BM^CDR Y)))) Y)) (DEFINE (^BM^SUBBAGP X Y) (IF (^BM^LISTP X) (IF (^BM^MEMBER (^BM^CAR X) Y) (^BM^SUBBAGP (^BM^CDR X) (^BM^DELETE (^BM^CAR X) Y)) (^BM^FALSE)) (^BM^TRUE))) (DEFINE (^BM^BAGDIFF X Y) (IF (^BM^LISTP Y) (IF (^BM^MEMBER (^BM^CAR Y) X) (^BM^BAGDIFF (^BM^DELETE (^BM^CAR Y) X) (^BM^CDR Y)) (^BM^BAGDIFF X (^BM^CDR Y))) X)) (DEFINE (^BM^BAGINT X Y) (IF (^BM^LISTP X) (IF (^BM^MEMBER (^BM^CAR X) Y) (^BM^CONS (^BM^CAR X) (^BM^BAGINT (^BM^CDR X) (^BM^DELETE (^BM^CAR X) Y))) (^BM^BAGINT (^BM^CDR X) Y)) (^NIL))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^MEMBER X Y)) (EQUAL (^BM^DELETE X Y) Y))) (LEMMA (^BM^IMPLIES (^BM^MEMBER X (^BM^DELETE U V)) (^BM^MEMBER X V))) (LEMMA (EQUAL (^BM^DELETE X (^BM^DELETE Y Z)) (^BM^DELETE Y (^BM^DELETE X Z)))) (LEMMA (^BM^IMPLIES (^BM^SUBBAGP X (^BM^DELETE U Y)) (^BM^SUBBAGP X Y))) (LEMMA (^BM^IMPLIES (^BM^SUBBAGP X Y) (^BM^SUBBAGP (^BM^CDR X) Y))) (LEMMA (^BM^IMPLIES (^BM^SUBBAGP X (^BM^CDR Y)) (^BM^SUBBAGP X Y))) (LEMMA (^BM^SUBBAGP (^BM^BAGINT X Y) X)) (LEMMA (^BM^SUBBAGP (^BM^BAGINT X Y) Y)) (DEFINE (^BM^PLUS-FRINGE X) (IF (^BM^AND (^BM^LISTP X) (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO)))))))) (^BM^APPEND (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X))) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X))))) (^BM^CONS X (^NIL)))) (DEFINE (^BM^PLUS-TREE L) (IF (^BM^NLISTP L) (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (IF (^BM^NLISTP (^BM^CDR L)) (^BM^CONS (^BM^PACK (^BM^CONS (^F) (^BM^CONS (^I) (^BM^CONS (^X) (^BM^ZERO))))) (^BM^CONS (^BM^CAR L) (^NIL))) (IF (^BM^NLISTP (^BM^CDR (^BM^CDR L))) (^BM^CONS (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CAR L) (^BM^CONS (^BM^CAR (^BM^CDR L)) (^NIL)))) (^BM^CONS (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CAR L) (^BM^CONS (^BM^PLUS-TREE (^BM^CDR L)) (^NIL)))))))) (DEFINE (^BM^CANCEL X) (IF (^BM^AND (^BM^LISTP X) (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))))) (IF (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR X))) (^BM^AND (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR X))) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR (^BM^CDR X)))) (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO)))))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PLUS-TREE (^BM^BAGDIFF (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X))) (^BM^BAGINT (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X))) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X))))))) (^BM^CONS (^BM^PLUS-TREE (^BM^BAGDIFF (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^BAGINT (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X))) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X))))))) (^NIL)))) (IF (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR X))) (^BM^AND (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR X))) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^MEMBER (^BM^CAR (^BM^CDR (^BM^CDR X))) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^B) (^BM^CONS (^E) (^BM^CONS (^R) (^BM^CONS (^P) (^BM^ZERO))))))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR X))) (^NIL))) (^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^PLUS-TREE (^BM^DELETE (^BM^CAR (^BM^CDR (^BM^CDR X))) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR X))))) (^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 (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^NIL)))) (^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^FALSE) (^NIL))) (^NIL))))) (IF (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^AND (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^L) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^MEMBER (^BM^CAR (^BM^CDR X)) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^B) (^BM^CONS (^E) (^BM^CONS (^R) (^BM^CONS (^P) (^BM^ZERO))))))))) (^BM^CONS (^BM^CAR (^BM^CDR X)) (^NIL))) (^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^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PLUS-TREE (^BM^DELETE (^BM^CAR (^BM^CDR X)) (^BM^PLUS-FRINGE (^BM^CAR (^BM^CDR (^BM^CDR X)))))) (^NIL)))) (^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^FALSE) (^NIL))) (^NIL))))) X))) X)) (DEFINE (^BM^REVERSE X) (IF (^BM^LISTP X) (^BM^APPEND (^BM^REVERSE (^BM^CDR X)) (^BM^CONS (^BM^CAR X) (^NIL))) (^NIL))) (LEMMA (EQUAL (^BM^APPEND (^BM^APPEND X Y) Z) (^BM^APPEND X (^BM^APPEND Y Z)))) (DEFINE (^BM^PLISTP X) (IF (^BM^NLISTP X) (EQUAL X (^NIL)) (^BM^PLISTP (^BM^CDR X)))) (LEMMA (^BM^IMPLIES (^BM^PLISTP X) (EQUAL (^BM^APPEND X (^NIL)) X))) (LEMMA (^BM^PLISTP (^BM^REVERSE X))) (LEMMA (EQUAL (^BM^REVERSE (^BM^APPEND A B)) (^BM^APPEND (^BM^REVERSE B) (^BM^REVERSE A)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP Y)) (EQUAL (^BM^TIMES X Y) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (^BM^TIMES X (^BM^PLUS Y Z)) (^BM^PLUS (^BM^TIMES X Y) (^BM^TIMES X Z)))) (LEMMA (EQUAL (^BM^TIMES X (^BM^ADD1 Y)) (IF (^BM^NUMBERP Y) (^BM^PLUS X (^BM^TIMES X Y)) (^BM^FIX X)))) (LEMMA (EQUAL (^BM^TIMES X Y) (^BM^TIMES Y X))) (LEMMA (EQUAL (^BM^TIMES X (^BM^TIMES Y Z)) (^BM^TIMES Y (^BM^TIMES X Z)))) (LEMMA (EQUAL (^BM^TIMES (^BM^TIMES X Y) Z) (^BM^TIMES X (^BM^TIMES Y Z)))) (LEMMA (EQUAL (EQUAL (^BM^TIMES X Y) (^INT (^BM^ZERO))) (^BM^OR (^BM^ZEROP X) (^BM^ZEROP Y)))) (DEFINE (^BM^STACKP X) (IF (CONSP X) (IF (EQUAL (CAR X) '^BM^PUSH) (IF (CONSP (CDR X)) (IF (^BM^NOT 'FALSE) (IF (CONSP (CDR (CDR X))) (IF (^BM^NOT 'FALSE) (EQUAL (CDR (CDR (CDR X))) 'NIL) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE)) (DEFINE (^BM^PUSH T1611 T1612) (CONS '^BM^PUSH (CONS (IF (^BM^NOT 'FALSE) T1611 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1612 (^BM^ZERO)) 'NIL)))) (DEFINE (^BM^TOP X) (IF (^BM^STACKP X) (CAR (CDR X)) (^BM^ZERO))) (DEFINE (^BM^POP X) (IF (^BM^STACKP X) (CAR (CDR (CDR X))) (^BM^ZERO))) (DEFINE (^BM^CALL FN X Y) (^INT (^BM^CONS (^1) (^BM^ZERO)))) (DEFINE (^BM^GETVALUE X Y) (^NIL)) (LEMMA (^BM^NUMBERP (^BM^CALL FN X Y))) (DEFINE (^BM^EXPRESSIONP X) (IF (^BM^LISTP X) (IF (^BM^LISTP (^BM^CAR X)) (^BM^FALSE) (IF (^BM^LISTP (^BM^CDR X)) (IF (^BM^LISTP (^BM^CDR (^BM^CDR X))) (IF (^BM^EXPRESSIONP (^BM^CAR (^BM^CDR X))) (^BM^EXPRESSIONP (^BM^CAR (^BM^CDR (^BM^CDR X)))) (^BM^FALSE)) (^BM^FALSE)) (^BM^FALSE))) (^BM^TRUE))) (LEMMA (^BM^IMPLIES (^BM^LISTP (^BM^CDR (^BM^CDR X))) (^BM^LESSP (^BM^COUNT (^BM^CAR (^BM^CDR X))) (^BM^COUNT X)))) (DEFINE (^BM^TERM-EVAL FORM ENVRN) (IF (^BM^NUMBERP FORM) FORM (IF (^BM^LISTP (^BM^CDR (^BM^CDR FORM))) (^BM^CALL (^BM^CAR FORM) (^BM^TERM-EVAL (^BM^CAR (^BM^CDR FORM)) ENVRN) (^BM^TERM-EVAL (^BM^CAR (^BM^CDR (^BM^CDR FORM))) ENVRN)) (^BM^GETVALUE FORM ENVRN)))) (DEFINE (^BM^OPTIMIZE FORM) (IF (^BM^LISTP (^BM^CDR (^BM^CDR FORM))) (IF (^BM^NUMBERP (^BM^OPTIMIZE (^BM^CAR (^BM^CDR FORM)))) (IF (^BM^NUMBERP (^BM^OPTIMIZE (^BM^CAR (^BM^CDR (^BM^CDR FORM))))) (^BM^CALL (^BM^CAR FORM) (^BM^OPTIMIZE (^BM^CAR (^BM^CDR FORM))) (^BM^OPTIMIZE (^BM^CAR (^BM^CDR (^BM^CDR FORM))))) (^BM^CONS (^BM^CAR FORM) (^BM^CONS (^BM^OPTIMIZE (^BM^CAR (^BM^CDR FORM))) (^BM^CONS (^BM^OPTIMIZE (^BM^CAR (^BM^CDR (^BM^CDR FORM)))) (^NIL))))) (^BM^CONS (^BM^CAR FORM) (^BM^CONS (^BM^OPTIMIZE (^BM^CAR (^BM^CDR FORM))) (^BM^CONS (^BM^OPTIMIZE (^BM^CAR (^BM^CDR (^BM^CDR FORM)))) (^NIL))))) FORM)) (DEFINE (^BM^CODEGEN FORM INS) (IF (^BM^NUMBERP FORM) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^CONS (^H) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS FORM (^NIL))) INS) (IF (^BM^LISTP (^BM^CDR (^BM^CDR FORM))) (^BM^CONS (^BM^CAR FORM) (^BM^CODEGEN (^BM^CAR (^BM^CDR (^BM^CDR FORM))) (^BM^CODEGEN (^BM^CAR (^BM^CDR FORM)) INS))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^CONS (^H) (^BM^CONS (^V) (^BM^ZERO))))))) (^BM^CONS FORM (^NIL))) INS)))) (DEFINE (^BM^COMPILE FORM) (^BM^REVERSE (^BM^CODEGEN (^BM^OPTIMIZE FORM) (^NIL)))) (LEMMA (^BM^IMPLIES (^BM^EXPRESSIONP X) (^BM^EXPRESSIONP (^BM^OPTIMIZE X)))) (LEMMA (^BM^IMPLIES (^BM^EXPRESSIONP X) (EQUAL (^BM^TERM-EVAL (^BM^OPTIMIZE X) ENVRN) (^BM^TERM-EVAL X ENVRN)))) (DEFINE (^BM^EXEC PC PDS ENVRN) (IF (^BM^NLISTP PC) PDS (IF (^BM^LISTP (^BM^CAR PC)) (IF (EQUAL (^BM^CAR (^BM^CAR PC)) (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^U) (^BM^CONS (^S) (^BM^CONS (^H) (^BM^CONS (^I) (^BM^ZERO)))))))) (^BM^EXEC (^BM^CDR PC) (^BM^PUSH (^BM^CAR (^BM^CDR (^BM^CAR PC))) PDS) ENVRN) (^BM^EXEC (^BM^CDR PC) (^BM^PUSH (^BM^GETVALUE (^BM^CAR (^BM^CDR (^BM^CAR PC))) ENVRN) PDS) ENVRN)) (^BM^EXEC (^BM^CDR PC) (^BM^PUSH (^BM^CALL (^BM^CAR PC) (^BM^TOP (^BM^POP PDS)) (^BM^TOP PDS)) (^BM^POP (^BM^POP PDS))) ENVRN)))) (LEMMA (EQUAL (^BM^EXEC (^BM^APPEND X Y) PDS ENVRN) (^BM^EXEC Y (^BM^EXEC X PDS ENVRN) ENVRN))) (LEMMA (^BM^IMPLIES (^BM^EXPRESSIONP X) (EQUAL (^BM^EXEC (^BM^REVERSE (^BM^CODEGEN X INS)) PDS ENVRN) (^BM^PUSH (^BM^TERM-EVAL X ENVRN) (^BM^EXEC (^BM^REVERSE INS) PDS ENVRN))))) (LEMMA (^BM^IMPLIES (^BM^EXPRESSIONP X) (EQUAL (^BM^EXEC (^BM^COMPILE X) PDS ENVRN) (^BM^PUSH (^BM^TERM-EVAL X ENVRN) PDS)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LESSP X Y) (^BM^LESSP Y Z)) (^BM^LESSP X Z))) (LEMMA (^BM^NOT (^BM^LESSP X X))) (DEFINE (^BM^EQP X Y) (EQUAL (^BM^FIX X) (^BM^FIX Y))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^EQP X Y)) (^BM^NOT (^BM^LESSP Y X))) (^BM^LESSP X Y))) (LEMMA (^BM^IMPLIES (^BM^PLISTP X) (EQUAL (^BM^REVERSE (^BM^REVERSE X)) X))) (DEFINE (^BM^FLATTEN X) (IF (^BM^LISTP X) (^BM^APPEND (^BM^FLATTEN (^BM^CAR X)) (^BM^FLATTEN (^BM^CDR X))) (^BM^CONS X (^NIL)))) (DEFINE (^BM^MC-FLATTEN X Y) (IF (^BM^LISTP X) (^BM^MC-FLATTEN (^BM^CAR X) (^BM^MC-FLATTEN (^BM^CDR X) Y)) (^BM^CONS X Y))) (LEMMA (EQUAL (^BM^MC-FLATTEN X Y) (^BM^APPEND (^BM^FLATTEN X) Y))) (LEMMA (EQUAL (^BM^MEMBER X (^BM^APPEND A B)) (^BM^OR (^BM^MEMBER X A) (^BM^MEMBER X B)))) (LEMMA (EQUAL (^BM^MEMBER X (^BM^REVERSE Y)) (^BM^MEMBER X Y))) (DEFINE (^BM^LENGTH X) (IF (^BM^LISTP X) (^BM^ADD1 (^BM^LENGTH (^BM^CDR X))) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (^BM^LENGTH (^BM^REVERSE X)) (^BM^LENGTH X))) (DEFINE (^BM^INTERSECT X Y) (IF (^BM^LISTP X) (IF (^BM^MEMBER X Y) (^BM^CONS X (^BM^INTERSECT (^BM^CDR X) Y)) (^BM^INTERSECT (^BM^CDR X) Y)) (^NIL))) (LEMMA (EQUAL (^BM^MEMBER A (^BM^UNION B C)) (^BM^OR (^BM^MEMBER A B) (^BM^MEMBER A C)))) (DEFINE (^BM^SUBSETP X Y) (IF (^BM^LISTP X) (IF (^BM^MEMBER (^BM^CAR X) Y) (^BM^SUBSETP (^BM^CDR X) Y) (^BM^FALSE)) (^BM^TRUE))) (LEMMA (^BM^IMPLIES (^BM^SUBSETP A B) (EQUAL (^BM^UNION A B) B))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^PLISTP A) (^BM^SUBSETP A B)) (EQUAL (^BM^INTERSECT A B) A))) (DEFINE (^BM^NTH X N) (IF (^BM^ZEROP N) X (^BM^NTH (^BM^CDR X) (^BM^SUB1 N)))) (DEFINE (^BM^GREATEREQP X Y) (^BM^NOT (^BM^LESSP X Y))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LEQ X Y) (^BM^LEQ Y Z)) (^BM^LEQ X Z))) (DEFINE (^BM^ORDERED L) (IF (^BM^LISTP L) (IF (^BM^LISTP (^BM^CDR L)) (IF (^BM^LESSP (^BM^CAR (^BM^CDR L)) (^BM^CAR L)) (^BM^FALSE) (^BM^ORDERED (^BM^CDR L))) (^BM^TRUE)) (^BM^TRUE))) (DEFINE (^BM^ADDTOLIST X L) (IF (^BM^LISTP L) (IF (^BM^LESSP X (^BM^CAR L)) (^BM^CONS X L) (^BM^CONS (^BM^CAR L) (^BM^ADDTOLIST X (^BM^CDR L)))) (^BM^CONS X (^NIL)))) (DEFINE (^BM^SORT L) (IF (^BM^LISTP L) (^BM^ADDTOLIST (^BM^CAR L) (^BM^SORT (^BM^CDR L))) (^NIL))) (DEFINE (^BM^BOOLEAN X) (^BM^OR (EQUAL X (^BM^TRUE)) (EQUAL X (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^BOOLEAN P) (^BM^BOOLEAN Q)) (EQUAL (^BM^IFF P Q) (EQUAL P Q)))) (LEMMA (EQUAL (^BM^NTH (^INT (^BM^ZERO)) I) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (^BM^NTH (^NIL) I) (IF (^BM^ZEROP I) (^NIL) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (^BM^NTH A (^BM^PLUS I J)) (^BM^NTH (^BM^NTH A I) J))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^BOOLEAN A) (^BM^AND (^BM^BOOLEAN B) (^BM^BOOLEAN C))) (EQUAL (EQUAL (EQUAL A B) C) (EQUAL A (EQUAL B C))))) (DEFINE (^BM^ODD X) (IF (^BM^ZEROP X) (^BM^FALSE) (IF (^BM^ZEROP (^BM^SUB1 X)) (^BM^TRUE) (^BM^ODD (^BM^SUB1 (^BM^SUB1 X)))))) (DEFINE (^BM^EVEN1 X) (IF (^BM^ZEROP X) (^BM^TRUE) (^BM^ODD (^BM^SUB1 X)))) (DEFINE (^BM^EVEN2 X) (IF (^BM^ZEROP X) (^BM^TRUE) (IF (^BM^ZEROP (^BM^SUB1 X)) (^BM^FALSE) (^BM^EVEN2 (^BM^SUB1 (^BM^SUB1 X)))))) (DEFINE (^BM^DOUBLE I) (IF (^BM^ZEROP I) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^ADD1 (^BM^DOUBLE (^BM^SUB1 I)))))) (LEMMA (^BM^EVEN1 (^BM^DOUBLE I))) (DEFINE (^BM^HALF I) (IF (^BM^ZEROP I) (^INT (^BM^ZERO)) (IF (^BM^ZEROP (^BM^SUB1 I)) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^HALF (^BM^SUB1 (^BM^SUB1 I))))))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP I) (EQUAL (^BM^HALF (^BM^DOUBLE I)) I))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I) (^BM^EVEN1 I)) (EQUAL (^BM^DOUBLE (^BM^HALF I)) I))) (LEMMA (EQUAL (^BM^DOUBLE I) (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) I))) (LEMMA (^BM^IMPLIES (^BM^SUBSETP X Y) (^BM^SUBSETP X (^BM^CONS Z Y)))) (DEFINE (^BM^LAST X) (IF (^BM^LISTP X) (IF (^BM^LISTP (^BM^CDR X)) (^BM^LAST (^BM^CDR X)) X) X)) (LEMMA (EQUAL (^BM^LAST (^BM^APPEND A B)) (IF (^BM^LISTP B) (^BM^LAST B) (IF (^BM^LISTP A) (^BM^CONS (^BM^CAR (^BM^LAST A)) B) B)))) (LEMMA (^BM^IMPLIES (^BM^LISTP A) (EQUAL (^BM^LAST (^BM^REVERSE A)) (^BM^CONS (^BM^CAR A) (^NIL))))) (DEFINE (^BM^EXP I J) (IF (^BM^ZEROP J) (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^TIMES I (^BM^EXP I (^BM^SUB1 J))))) (LEMMA (EQUAL (^BM^EXP I (^BM^PLUS J K)) (^BM^TIMES (^BM^EXP I J) (^BM^EXP I K)))) (LEMMA (EQUAL (^BM^EVEN1 X) (^BM^EVEN2 X))) (LEMMA (^BM^LEQ (^BM^LENGTH (^BM^NTH L I)) (^BM^LENGTH L))) (LEMMA (EQUAL (^BM^MEMBER A (^BM^SORT B)) (^BM^MEMBER A B))) (LEMMA (EQUAL (^BM^LENGTH (^BM^SORT A)) (^BM^LENGTH A))) (DEFINE (^BM^COUNT-LIST A L) (IF (^BM^LISTP A) (IF (^BM^MEMBER A L) (^BM^ADD1 (^BM^COUNT-LIST A (^BM^CDR L))) (^BM^COUNT-LIST A L)) (^BM^ZERO))) (LEMMA (EQUAL (^BM^COUNT-LIST A (^BM^SORT L)) (^BM^COUNT-LIST A L))) (LEMMA (^BM^IMPLIES (^BM^ORDERED (^BM^APPEND A B)) (^BM^ORDERED A))) (LEMMA (^BM^LEQ (^BM^HALF I) I)) (DEFINE (^BM^NUMBER-LISTP L) (IF (^BM^LISTP L) (^BM^AND (^BM^NUMBERP (^BM^CAR L)) (^BM^NUMBER-LISTP (^BM^CDR L))) (EQUAL L (^NIL)))) (LEMMA (^BM^ORDERED (^BM^SORT X))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^ORDERED X) (^BM^AND (^BM^NUMBER-LISTP X) (^BM^AND (^BM^NUMBERP I) (^BM^NOT (^BM^LESSP (^BM^CAR X) I))))) (EQUAL (^BM^ADDTOLIST I X) (^BM^CONS I X)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^ORDERED X) (^BM^NUMBER-LISTP X)) (EQUAL (^BM^SORT X) X))) (DEFINE (^BM^XOR P Q) (IF Q (IF P (^BM^FALSE) (^BM^TRUE)) (EQUAL P (^BM^TRUE)))) (LEMMA (^BM^IMPLIES (EQUAL X (^BM^SORT L)) (^BM^ORDERED X))) (LEMMA (^BM^IMPLIES (^BM^NUMBER-LISTP L) (EQUAL (EQUAL (^BM^SORT L) L) (^BM^ORDERED L)))) (DEFINE (^BM^SUBST X Y Z) (IF (EQUAL Y Z) X (IF (^BM^LISTP Z) (^BM^CONS (^BM^SUBST X Y (^BM^CAR Z)) (^BM^SUBST X Y (^BM^CDR Z))) Z))) (LEMMA (EQUAL (^BM^SUBST A A B) B)) (DEFINE (^BM^OCCUR X Y) (IF (EQUAL X Y) (^BM^TRUE) (IF (^BM^LISTP Y) (IF (^BM^OCCUR X (^BM^CAR Y)) (^BM^TRUE) (^BM^OCCUR X (^BM^CDR Y))) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^OCCUR A B)) (EQUAL (^BM^SUBST C A B) B))) (DEFINE (^BM^FACT I) (IF (^BM^ZEROP I) (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^TIMES I (^BM^FACT (^BM^SUB1 I))))) (DEFINE (^BM^FACT-LOOP I ANS) (IF (^BM^ZEROP I) ANS (^BM^FACT-LOOP (^BM^SUB1 I) (^BM^TIMES I ANS)))) (DEFINE (^BM^FACT- I) (^BM^FACT-LOOP I (^INT (^BM^CONS (^1) (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP I) (EQUAL (^BM^FACT-LOOP J I) (^BM^TIMES I (^BM^FACT J))))) (LEMMA (EQUAL (^BM^FACT- I) (^BM^FACT I))) (DEFINE (^BM^REVERSE-LOOP X ANS) (IF (^BM^LISTP X) (^BM^REVERSE-LOOP (^BM^CDR X) (^BM^CONS (^BM^CAR X) ANS)) ANS)) (DEFINE (^BM^REVERSE- X) (^BM^REVERSE-LOOP X (^NIL))) (LEMMA (EQUAL (^BM^REVERSE-LOOP X Y) (^BM^APPEND (^BM^REVERSE X) Y))) (LEMMA (EQUAL (^BM^REVERSE-LOOP X (^NIL)) (^BM^REVERSE X))) (LEMMA (EQUAL (^BM^REVERSE- (^BM^APPEND A B)) (^BM^APPEND (^BM^REVERSE- B) (^BM^REVERSE- A)))) (LEMMA (^BM^IMPLIES (^BM^PLISTP X) (EQUAL (^BM^REVERSE- (^BM^REVERSE- X)) X))) (DEFINE (^BM^SORT-LP X Y) (IF (^BM^LISTP X) (^BM^SORT-LP (^BM^CDR X) (^BM^ADDTOLIST (^BM^CAR X) Y)) Y)) (LEMMA (^BM^IMPLIES (^BM^ORDERED Y) (^BM^ORDERED (^BM^ADDTOLIST X Y)))) (LEMMA (^BM^IMPLIES (^BM^ORDERED Y) (^BM^ORDERED (^BM^SORT-LP X Y)))) (LEMMA (EQUAL (^BM^COUNT-LIST Z (^BM^SORT-LP X Y)) (^BM^PLUS (^BM^COUNT-LIST Z X) (^BM^COUNT-LIST Z Y)))) (LEMMA (EQUAL (EQUAL (^BM^APPEND A B) (^BM^APPEND A C)) (EQUAL B C))) (LEMMA (EQUAL (EQUAL (^BM^LESSP X Y) Z) (IF (^BM^LESSP X Y) (EQUAL (^BM^TRUE) Z) (EQUAL (^BM^FALSE) Z)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP Y) (^BM^NOT (^BM^LESSP Y X))) (EQUAL (^BM^PLUS X (^BM^DIFFERENCE Y X)) Y))) (DEFINE (^BM^POWER-EVAL L BASE) (IF (^BM^LISTP L) (^BM^PLUS (^BM^CAR L) (^BM^TIMES BASE (^BM^POWER-EVAL (^BM^CDR L) BASE))) (^INT (^BM^ZERO)))) (DEFINE (^BM^BIG-PLUS1 L I BASE) (IF (^BM^LISTP L) (IF (^BM^ZEROP I) L (^BM^CONS (^BM^REMAINDER (^BM^PLUS (^BM^CAR L) I) BASE) (^BM^BIG-PLUS1 (^BM^CDR L) (^BM^QUOTIENT (^BM^PLUS (^BM^CAR L) I) BASE) BASE))) (^BM^CONS I (^NIL)))) (LEMMA (EQUAL (^BM^PLUS (^BM^REMAINDER X Y) (^BM^TIMES Y (^BM^QUOTIENT X Y))) (^BM^FIX X))) (LEMMA (EQUAL (^BM^POWER-EVAL (^BM^BIG-PLUS1 L I BASE) BASE) (^BM^PLUS (^BM^POWER-EVAL L BASE) I))) (DEFINE (^BM^BIG-PLUS X Y I BASE) (IF (^BM^LISTP X) (IF (^BM^LISTP Y) (^BM^CONS (^BM^REMAINDER (^BM^PLUS I (^BM^PLUS (^BM^CAR X) (^BM^CAR Y))) BASE) (^BM^BIG-PLUS (^BM^CDR X) (^BM^CDR Y) (^BM^QUOTIENT (^BM^PLUS I (^BM^PLUS (^BM^CAR X) (^BM^CAR Y))) BASE) BASE)) (^BM^BIG-PLUS1 X I BASE)) (^BM^BIG-PLUS1 Y I BASE))) (LEMMA (EQUAL (^BM^POWER-EVAL (^BM^BIG-PLUS X Y I BASE) BASE) (^BM^PLUS I (^BM^PLUS (^BM^POWER-EVAL X BASE) (^BM^POWER-EVAL Y BASE))))) (LEMMA (EQUAL (^BM^REMAINDER Y (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^INT (^BM^ZERO)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP X)) (EQUAL (^BM^REMAINDER Y X) (^BM^FIX Y)))) (LEMMA (EQUAL (^BM^LESSP (^BM^REMAINDER X Y) Y) (^BM^NOT (^BM^ZEROP Y)))) (LEMMA (EQUAL (^BM^REMAINDER X X) (^INT (^BM^ZERO)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP Y)) (^BM^NUMBERP X)) (EQUAL (^BM^PLUS (^BM^REMAINDER X Y) (^BM^TIMES Y (^BM^QUOTIENT X Y))) X))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^ZEROP I)) (^BM^NOT (^BM^LESSP (^BM^TIMES I J) J)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^ZEROP I)) (^BM^NOT (^BM^LESSP (^BM^TIMES J I) J)))) (LEMMA (EQUAL (^BM^LESSP (^BM^QUOTIENT I J) I) (^BM^AND (^BM^NOT (^BM^ZEROP I)) (^BM^OR (^BM^ZEROP J) (^BM^NOT (EQUAL J (^INT (^BM^CONS (^1) (^BM^ZERO))))))))) (LEMMA (EQUAL (^BM^LESSP (^BM^REMAINDER X Y) X) (^BM^AND (^BM^NOT (^BM^ZEROP Y)) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^NOT (^BM^LESSP X Y)))))) (DEFINE (^BM^POWER-REP I BASE) (IF (^BM^ZEROP I) (^NIL) (IF (^BM^ZEROP BASE) (^BM^CONS I (^NIL)) (IF (EQUAL BASE (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^CONS I (^NIL)) (^BM^CONS (^BM^REMAINDER I BASE) (^BM^POWER-REP (^BM^QUOTIENT I BASE) BASE)))))) (LEMMA (EQUAL (^BM^POWER-EVAL (^BM^POWER-REP I BASE) BASE) (^BM^FIX I))) (LEMMA (EQUAL (^BM^POWER-EVAL (^BM^BIG-PLUS (^BM^POWER-REP I BASE) (^BM^POWER-REP J BASE) (^INT (^BM^ZERO)) BASE) BASE) (^BM^PLUS I J))) (DEFINE (^BM^GCD X Y) (IF (^BM^ZEROP X) (^BM^FIX Y) (IF (^BM^ZEROP Y) X (IF (^BM^LESSP X Y) (^BM^GCD X (^BM^DIFFERENCE Y X)) (^BM^GCD (^BM^DIFFERENCE X Y) Y))))) (LEMMA (^BM^NUMBERP (^BM^GCD X Y))) (LEMMA (EQUAL (EQUAL (^BM^GCD X Y) (^INT (^BM^ZERO))) (^BM^AND (^BM^ZEROP X) (^BM^ZEROP Y)))) (LEMMA (EQUAL (^BM^GCD (^INT (^BM^ZERO)) Y) (^BM^FIX Y))) (LEMMA (EQUAL (^BM^GCD X Y) (^BM^GCD Y X))) (LEMMA (EQUAL (^BM^NTH (^BM^APPEND A B) I) (^BM^APPEND (^BM^NTH A I) (^BM^NTH B (^BM^DIFFERENCE I (^BM^LENGTH A)))))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS X Y) X) (^BM^FIX Y))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS Y X) X) (^BM^FIX Y))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS X Y) (^BM^PLUS X Z)) (^BM^DIFFERENCE Y Z))) (LEMMA (EQUAL (^BM^TIMES X (^BM^DIFFERENCE C W)) (^BM^DIFFERENCE (^BM^TIMES C X) (^BM^TIMES W X)))) (DEFINE (^BM^DIVIDES X Y) (^BM^ZEROP (^BM^REMAINDER Y X))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^TIMES X Z) Z) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS B (^BM^PLUS A C)) A) (^BM^PLUS B C))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^ADD1 (^BM^PLUS Y Z)) Z) (^BM^ADD1 Y))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP Y)) (^BM^NOT (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO)))))) (^BM^NOT (EQUAL (^BM^REMAINDER (^BM^ADD1 (^BM^TIMES X Y)) Y) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO))) (EQUAL (^BM^REMAINDER Y Z) (^INT (^BM^ZERO)))) (EQUAL (^BM^REMAINDER (^BM^PLUS X Y) Z) (^INT (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO))) (^BM^NOT (EQUAL (^BM^REMAINDER Y Z) (^INT (^BM^ZERO))))) (^BM^NOT (EQUAL (^BM^REMAINDER (^BM^PLUS X Y) Z) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO))) (EQUAL (EQUAL (^BM^REMAINDER (^BM^PLUS X Y) Z) (^INT (^BM^ZERO))) (EQUAL (^BM^REMAINDER Y Z) (^INT (^BM^ZERO)))))) (LEMMA (EQUAL (^BM^LESSP (^BM^PLUS X Y) (^BM^PLUS X Z)) (^BM^LESSP Y Z))) (LEMMA (^BM^IMPLIES (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO))) (EQUAL (EQUAL (^BM^REMAINDER (^BM^PLUS Y X) Z) (^INT (^BM^ZERO))) (EQUAL (^BM^REMAINDER Y Z) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (EQUAL (^BM^REMAINDER X Z) (^INT (^BM^ZERO))) (EQUAL (EQUAL (^BM^REMAINDER (^BM^DIFFERENCE Y X) Z) (^INT (^BM^ZERO))) (IF (^BM^LESSP X Y) (EQUAL (^BM^REMAINDER Y Z) (^INT (^BM^ZERO))) (^BM^TRUE))))) (LEMMA (EQUAL (^BM^LESSP (^BM^TIMES X Z) (^BM^TIMES Y Z)) (^BM^AND (^BM^NOT (^BM^ZEROP Z)) (^BM^LESSP X Y)))) (LEMMA (EQUAL (^BM^LESSP Y (^BM^PLUS X Y)) (^BM^NOT (^BM^ZEROP X)))) (LEMMA (EQUAL (^BM^GCD (^BM^TIMES X Z) (^BM^TIMES Y Z)) (^BM^TIMES Z (^BM^GCD X Y)))) (LEMMA (^BM^AND (EQUAL (^BM^REMAINDER X (^BM^GCD X Y)) (^INT (^BM^ZERO))) (EQUAL (^BM^REMAINDER Y (^BM^GCD X Y)) (^INT (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (^BM^ZEROP Y)) (^BM^AND (^BM^DIVIDES Z X) (^BM^DIVIDES Z Y)))) (^BM^LEQ Z (^BM^GCD X Y)))) (DEFINE (^BM^IF-EXPRP X) (IF (CONSP X) (IF (EQUAL (CAR X) '^BM^CONS-IF) (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) (EQUAL (CDR (CDR (CDR (CDR X)))) 'NIL) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE) 'FALSE)) (DEFINE (^BM^CONS-IF T1614 T1615 T1616) (CONS '^BM^CONS-IF (CONS (IF (^BM^NOT 'FALSE) T1614 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1615 (^BM^ZERO)) (CONS (IF (^BM^NOT 'FALSE) T1616 (^BM^ZERO)) 'NIL))))) (DEFINE (^BM^TEST X) (IF (^BM^IF-EXPRP X) (CAR (CDR X)) (^BM^ZERO))) (DEFINE (^BM^LEFT-BRANCH X) (IF (^BM^IF-EXPRP X) (CAR (CDR (CDR X))) (^BM^ZERO))) (DEFINE (^BM^RIGHT-BRANCH X) (IF (^BM^IF-EXPRP X) (CAR (CDR (CDR (CDR X)))) (^BM^ZERO))) (DEFINE (^BM^ASSIGNMENT VAR ALIST) (IF (EQUAL VAR (^BM^TRUE)) (^BM^TRUE) (IF (EQUAL VAR (^BM^FALSE)) (^BM^FALSE) (IF (^BM^NLISTP ALIST) (^BM^FALSE) (IF (EQUAL VAR (^BM^CAR (^BM^CAR ALIST))) (^BM^CDR (^BM^CAR ALIST)) (^BM^ASSIGNMENT VAR (^BM^CDR ALIST))))))) (DEFINE (^BM^VALUE X ALIST) (IF (^BM^IF-EXPRP X) (IF (^BM^VALUE (^BM^TEST X) ALIST) (^BM^VALUE (^BM^LEFT-BRANCH X) ALIST) (^BM^VALUE (^BM^RIGHT-BRANCH X) ALIST)) (^BM^ASSIGNMENT X ALIST))) (DEFINE (^BM^IF-DEPTH X) (IF (^BM^IF-EXPRP X) (^BM^ADD1 (^BM^IF-DEPTH (^BM^TEST X))) (^INT (^BM^ZERO)))) (DEFINE (^BM^IF-COMPLEXITY X) (IF (^BM^IF-EXPRP X) (^BM^TIMES (^BM^IF-COMPLEXITY (^BM^TEST X)) (^BM^PLUS (^BM^IF-COMPLEXITY (^BM^LEFT-BRANCH X)) (^BM^IF-COMPLEXITY (^BM^RIGHT-BRANCH X)))) (^INT (^BM^CONS (^1) (^BM^ZERO))))) (LEMMA (^BM^NOT (EQUAL (^BM^IF-COMPLEXITY X) (^INT (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^IF-EXPRP X) (^BM^LESSP (^BM^IF-COMPLEXITY (^BM^LEFT-BRANCH X)) (^BM^IF-COMPLEXITY X)))) (LEMMA (^BM^IMPLIES (^BM^IF-EXPRP X) (^BM^LESSP (^BM^IF-COMPLEXITY (^BM^RIGHT-BRANCH X)) (^BM^IF-COMPLEXITY X)))) (DEFINE (^BM^NORMALIZE X) (IF (^BM^IF-EXPRP X) (IF (^BM^IF-EXPRP (^BM^TEST X)) (^BM^NORMALIZE (^BM^CONS-IF (^BM^TEST (^BM^TEST X)) (^BM^CONS-IF (^BM^LEFT-BRANCH (^BM^TEST X)) (^BM^LEFT-BRANCH X) (^BM^RIGHT-BRANCH X)) (^BM^CONS-IF (^BM^RIGHT-BRANCH (^BM^TEST X)) (^BM^LEFT-BRANCH X) (^BM^RIGHT-BRANCH X)))) (^BM^CONS-IF (^BM^TEST X) (^BM^NORMALIZE (^BM^LEFT-BRANCH X)) (^BM^NORMALIZE (^BM^RIGHT-BRANCH X)))) X)) (DEFINE (^BM^NORMALIZED-IF-EXPRP X) (IF (^BM^IF-EXPRP X) (^BM^AND (^BM^NOT (^BM^IF-EXPRP (^BM^TEST X))) (^BM^AND (^BM^NORMALIZED-IF-EXPRP (^BM^LEFT-BRANCH X)) (^BM^NORMALIZED-IF-EXPRP (^BM^RIGHT-BRANCH X)))) (^BM^TRUE))) (DEFINE (^BM^ASSIGNEDP VAR ALIST) (IF (EQUAL VAR (^BM^TRUE)) (^BM^TRUE) (IF (EQUAL VAR (^BM^FALSE)) (^BM^TRUE) (IF (^BM^NLISTP ALIST) (^BM^FALSE) (IF (EQUAL VAR (^BM^CAR (^BM^CAR ALIST))) (^BM^TRUE) (^BM^ASSIGNEDP VAR (^BM^CDR ALIST))))))) (DEFINE (^BM^ASSUME-TRUE VAR ALIST) (^BM^CONS (^BM^CONS VAR (^BM^TRUE)) ALIST)) (DEFINE (^BM^ASSUME-FALSE VAR ALIST) (^BM^CONS (^BM^CONS VAR (^BM^FALSE)) ALIST)) (DEFINE (^BM^TAUTOLOGYP X ALIST) (IF (^BM^IF-EXPRP X) (IF (^BM^ASSIGNEDP (^BM^TEST X) ALIST) (IF (^BM^ASSIGNMENT (^BM^TEST X) ALIST) (^BM^TAUTOLOGYP (^BM^LEFT-BRANCH X) ALIST) (^BM^TAUTOLOGYP (^BM^RIGHT-BRANCH X) ALIST)) (^BM^AND (^BM^TAUTOLOGYP (^BM^LEFT-BRANCH X) (^BM^ASSUME-TRUE (^BM^TEST X) ALIST)) (^BM^TAUTOLOGYP (^BM^RIGHT-BRANCH X) (^BM^ASSUME-FALSE (^BM^TEST X) ALIST)))) (^BM^ASSIGNMENT X ALIST))) (LEMMA (EQUAL (^BM^ASSIGNMENT X (^BM^APPEND A B)) (IF (^BM^ASSIGNEDP X A) (^BM^ASSIGNMENT X A) (^BM^ASSIGNMENT X B)))) (LEMMA (^BM^AND (^BM^IMPLIES (^BM^AND (^BM^IFF VAL (^BM^ASSIGNMENT VAR A)) (^BM^VALUE X A)) (^BM^VALUE X (^BM^CONS (^BM^CONS VAR VAL) A))) (^BM^IMPLIES (^BM^AND (^BM^IFF VAL (^BM^ASSIGNMENT VAR A)) (^BM^NOT (^BM^VALUE X A))) (^BM^NOT (^BM^VALUE X (^BM^CONS (^BM^CONS VAR VAL) A)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^IF-EXPRP X) (^BM^NORMALIZED-IF-EXPRP X)) (EQUAL (^BM^VALUE (^BM^TEST X) A) (^BM^ASSIGNMENT (^BM^TEST X) A)))) (LEMMA (^BM^IMPLIES (^BM^ASSIGNMENT X A) (^BM^ASSIGNEDP X A))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NORMALIZED-IF-EXPRP X) (^BM^TAUTOLOGYP X A1)) (^BM^VALUE X (^BM^APPEND A1 A2)))) (DEFINE (^BM^TAUTOLOGY-CHECKER X) (^BM^TAUTOLOGYP (^BM^NORMALIZE X) (^NIL))) (DEFINE (^BM^FALSIFY1 X ALIST) (IF (^BM^IF-EXPRP X) (IF (^BM^ASSIGNEDP (^BM^TEST X) ALIST) (IF (^BM^ASSIGNMENT (^BM^TEST X) ALIST) (^BM^FALSIFY1 (^BM^LEFT-BRANCH X) ALIST) (^BM^FALSIFY1 (^BM^RIGHT-BRANCH X) ALIST)) (IF (^BM^FALSIFY1 (^BM^LEFT-BRANCH X) (^BM^ASSUME-TRUE (^BM^TEST X) ALIST)) (^BM^FALSIFY1 (^BM^LEFT-BRANCH X) (^BM^ASSUME-TRUE (^BM^TEST X) ALIST)) (^BM^FALSIFY1 (^BM^RIGHT-BRANCH X) (^BM^ASSUME-FALSE (^BM^TEST X) ALIST)))) (IF (^BM^ASSIGNEDP X ALIST) (IF (^BM^ASSIGNMENT X ALIST) (^BM^FALSE) ALIST) (^BM^CONS (^BM^CONS X (^BM^FALSE)) ALIST)))) (DEFINE (^BM^FALSIFY X) (^BM^FALSIFY1 (^BM^NORMALIZE X) (^NIL))) (LEMMA (^BM^IMPLIES (^BM^ASSIGNEDP X A) (EQUAL (^BM^ASSIGNMENT X (^BM^FALSIFY1 Y A)) (IF (^BM^FALSIFY1 Y A) (^BM^ASSIGNMENT X A) (EQUAL X (^BM^TRUE)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NORMALIZED-IF-EXPRP X) (^BM^FALSIFY1 X A)) (EQUAL (^BM^VALUE X (^BM^FALSIFY1 X A)) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NORMALIZED-IF-EXPRP X) (^BM^AND (^BM^NOT (^BM^TAUTOLOGYP X A)) A)) (^BM^FALSIFY1 X A))) (LEMMA (EQUAL (^BM^VALUE (^BM^NORMALIZE X) A) (^BM^VALUE X A))) (LEMMA (^BM^NORMALIZED-IF-EXPRP (^BM^NORMALIZE X))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^VALUE Y (^BM^FALSIFY1 X A)) (^BM^VALUE X (^BM^FALSIFY1 X A))) (^BM^AND (^BM^FALSIFY1 X A) (^BM^NORMALIZED-IF-EXPRP X))) (EQUAL (^BM^VALUE Y (^BM^FALSIFY1 X A)) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^TAUTOLOGY-CHECKER X)) (EQUAL (^BM^VALUE X (^BM^FALSIFY X)) (^BM^FALSE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^TAUTOLOGYP Y A1) (^BM^AND (^BM^NORMALIZED-IF-EXPRP Y) (EQUAL (^BM^VALUE X A2) (^BM^VALUE Y (^BM^APPEND A1 A2))))) (^BM^VALUE X A2))) (LEMMA (^BM^IMPLIES (^BM^TAUTOLOGY-CHECKER X) (^BM^VALUE X A))) (LEMMA (EQUAL (EQUAL (^BM^FLATTEN X) (^BM^CONS Y (^NIL))) (^BM^AND (^BM^NLISTP X) (EQUAL X Y)))) (DEFINE (^BM^LEFTCOUNT X) (IF (^BM^NLISTP X) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^LEFTCOUNT (^BM^CAR X))))) (DEFINE (^BM^GOPHER X) (IF (^BM^OR (^BM^NLISTP X) (^BM^NLISTP (^BM^CAR X))) X (^BM^GOPHER (^BM^CONS (^BM^CAR (^BM^CAR X)) (^BM^CONS (^BM^CDR (^BM^CAR X)) (^BM^CDR X)))))) (LEMMA (^BM^NOT (^BM^LESSP (^BM^COUNT X) (^BM^COUNT (^BM^GOPHER X))))) (LEMMA (EQUAL (^BM^LISTP (^BM^GOPHER X)) (^BM^LISTP X))) (DEFINE (^BM^SAMEFRINGE X Y) (IF (^BM^OR (^BM^NLISTP X) (^BM^NLISTP Y)) (EQUAL X Y) (^BM^AND (EQUAL (^BM^CAR (^BM^GOPHER X)) (^BM^CAR (^BM^GOPHER Y))) (^BM^SAMEFRINGE (^BM^CDR (^BM^GOPHER X)) (^BM^CDR (^BM^GOPHER Y)))))) (LEMMA (EQUAL (^BM^CAR (^BM^GOPHER X)) (IF (^BM^LISTP X) (^BM^CAR (^BM^FLATTEN X)) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (^BM^FLATTEN (^BM^CDR (^BM^GOPHER X))) (IF (^BM^LISTP X) (^BM^CDR (^BM^FLATTEN X)) (^BM^CONS (^INT (^BM^ZERO)) (^NIL))))) (LEMMA (EQUAL (^BM^SAMEFRINGE X Y) (EQUAL (^BM^FLATTEN X) (^BM^FLATTEN Y)))) (DEFINE (^BM^PRIME1 X Y) (IF (^BM^ZEROP Y) (^BM^FALSE) (IF (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^TRUE) (^BM^AND (^BM^NOT (^BM^DIVIDES Y X)) (^BM^PRIME1 X (^BM^SUB1 Y)))))) (DEFINE (^BM^PRIME X) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^PRIME1 X (^BM^SUB1 X))))) (DEFINE (^BM^GREATEST-FACTOR X Y) (IF (^BM^OR (^BM^ZEROP Y) (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO))))) X (IF (^BM^DIVIDES Y X) Y (^BM^GREATEST-FACTOR X (^BM^SUB1 Y))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LESSP Y X) (^BM^AND (^BM^NOT (^BM^PRIME1 X Y)) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (EQUAL (^BM^SUB1 X) (^INT (^BM^ZERO)))) (^BM^NOT (^BM^ZEROP Y)))))) (^BM^LESSP (^BM^GREATEST-FACTOR X Y) X))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LESSP Y X) (^BM^AND (^BM^NOT (^BM^PRIME1 X Y)) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^NOT (^BM^ZEROP Y)))))) (EQUAL (^BM^REMAINDER X (^BM^GREATEST-FACTOR X Y)) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (EQUAL (^BM^GREATEST-FACTOR X Y) (^INT (^BM^ZERO))) (^BM^AND (^BM^OR (^BM^ZEROP Y) (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO))))) (EQUAL X (^INT (^BM^ZERO)))))) (LEMMA (EQUAL (^BM^REMAINDER (^INT (^BM^ZERO)) Y) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (EQUAL (^BM^GREATEST-FACTOR X Y) (^INT (^BM^CONS (^1) (^BM^ZERO)))) (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO)))))) (LEMMA (EQUAL (^BM^NUMBERP (^BM^GREATEST-FACTOR X Y)) (^BM^NOT (^BM^AND (^BM^OR (^BM^ZEROP Y) (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^NOT (^BM^NUMBERP X)))))) (DEFINE (^BM^PRIME-FACTORS X) (IF (^BM^OR (^BM^ZEROP X) (EQUAL (^BM^SUB1 X) (^INT (^BM^ZERO)))) (^NIL) (IF (^BM^PRIME1 X (^BM^SUB1 X)) (^BM^CONS X (^NIL)) (^BM^APPEND (^BM^PRIME-FACTORS (^BM^GREATEST-FACTOR X (^BM^SUB1 X))) (^BM^PRIME-FACTORS (^BM^QUOTIENT X (^BM^GREATEST-FACTOR X (^BM^SUB1 X)))))))) (DEFINE (^BM^PRIME-LIST L) (IF (^BM^NLISTP L) (^BM^TRUE) (^BM^AND (^BM^PRIME (^BM^CAR L)) (^BM^PRIME-LIST (^BM^CDR L))))) (DEFINE (^BM^TIMES-LIST L) (IF (^BM^NLISTP L) (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^TIMES (^BM^CAR L) (^BM^TIMES-LIST (^BM^CDR L))))) (LEMMA (EQUAL (^BM^TIMES-LIST (^BM^APPEND X Y)) (^BM^TIMES (^BM^TIMES-LIST X) (^BM^TIMES-LIST Y)))) (LEMMA (EQUAL (^BM^PRIME-LIST (^BM^APPEND X Y)) (^BM^AND (^BM^PRIME-LIST X) (^BM^PRIME-LIST Y)))) (LEMMA (^BM^PRIME-LIST (^BM^PRIME-FACTORS X))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP Y) (^BM^AND (^BM^NUMBERP X) (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^ZERO)))) (^BM^DIVIDES X Y)))) (EQUAL (^BM^TIMES X (^BM^QUOTIENT Y X)) Y))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^LESSP X Y)) (^BM^NOT (EQUAL (^BM^QUOTIENT Y X) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^ZEROP X)) (EQUAL (^BM^TIMES-LIST (^BM^PRIME-FACTORS X)) X))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^ZEROP X)) (^BM^AND (EQUAL (^BM^TIMES-LIST (^BM^PRIME-FACTORS X)) X) (^BM^PRIME-LIST (^BM^PRIME-FACTORS X))))) (DEFINE (^BM^GREATEREQPR W Z) (IF (^BM^ZEROP W) (^BM^ZEROP Z) (IF (EQUAL W Z) (^BM^TRUE) (^BM^GREATEREQPR (^BM^SUB1 W) Z)))) (LEMMA (EQUAL (EQUAL Z (^BM^TIMES W Z)) (^BM^AND (^BM^NUMBERP Z) (^BM^OR (EQUAL Z (^INT (^BM^ZERO))) (EQUAL W (^INT (^BM^CONS (^1) (^BM^ZERO)))))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (EQUAL Z (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^AND (^BM^NOT (EQUAL Z (^INT (^BM^ZERO)))) (^BM^AND (^BM^NUMBERP Z) (^BM^GREATEREQPR U Z)))) (^BM^NOT (^BM^PRIME1 (^BM^TIMES W Z) U)))) (LEMMA (EQUAL (^BM^GREATEREQPR X Y) (^BM^NOT (^BM^LESSP X Y)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (EQUAL Z (^BM^ADD1 V))) (^BM^DIVIDES Z (^BM^ADD1 V))) (^BM^GREATEREQPR V Z))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (EQUAL Z (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^AND (^BM^NOT (EQUAL Z X)) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^DIVIDES Z X))))) (^BM^NOT (^BM^PRIME1 X (^BM^SUB1 X))))) (LEMMA (^BM^IMPLIES (EQUAL (^BM^GCD B X) Y) (EQUAL (^BM^REMAINDER B Y) (^INT (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^NOT (EQUAL (^BM^REMAINDER B X) (^INT (^BM^ZERO)))) (^BM^NOT (EQUAL (^BM^GCD B X) X)))) (LEMMA (^BM^IMPLIES (EQUAL A (^BM^TIMES Z Y)) (EQUAL (^BM^REMAINDER A Z) (^INT (^BM^ZERO))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP Y) (^BM^AND (^BM^NOT (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^AND (^BM^NOT (EQUAL Y (^INT (^BM^ZERO)))) (^BM^NOT (EQUAL X (^INT (^BM^ZERO))))))) (^BM^NOT (EQUAL X (^BM^TIMES X Y))))) (LEMMA (EQUAL (EQUAL X (^BM^TIMES X Y)) (^BM^OR (EQUAL X (^INT (^BM^ZERO))) (^BM^AND (^BM^NUMBERP X) (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO)))))))) (LEMMA (^BM^IMPLIES (EQUAL Y (^BM^TIMES K X)) (EQUAL (^BM^GCD Y (^BM^TIMES A X)) (^BM^TIMES X (^BM^GCD A K))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^DIVIDES X A)) (EQUAL A (^BM^GCD (^BM^TIMES X A) (^BM^TIMES B A)))) (^BM^NOT (EQUAL (^BM^TIMES K X) (^BM^TIMES B A))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^DIVIDES X B)) (^BM^AND (^BM^NOT (^BM^ZEROP X)) (^BM^AND (^BM^NOT (EQUAL (^BM^SUB1 X) (^INT (^BM^ZERO)))) (^BM^PRIME1 X (^BM^SUB1 X))))) (EQUAL (EQUAL (^BM^GCD B X) (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^TRUE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP X) (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^ZERO)))) (EQUAL FREE (^BM^TIMES X Z)))) (EQUAL (^BM^GCD (^BM^TIMES B Z) FREE) (^BM^TIMES Z (^BM^GCD B X))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP Z) (^BM^AND (^BM^PRIME X) (^BM^AND (^BM^NOT (^BM^DIVIDES X Z)) (^BM^NOT (^BM^DIVIDES X B))))) (^BM^NOT (EQUAL (^BM^TIMES X K) (^BM^TIMES B Z))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP Y) (^BM^NOT (EQUAL (^BM^TIMES X (^BM^QUOTIENT Y X)) Y))) (^BM^NOT (EQUAL (^BM^REMAINDER Y X) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^PRIME X) (^BM^AND (^BM^NOT (EQUAL Y (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^BM^NOT (EQUAL X Y)))) (^BM^NOT (EQUAL (^BM^REMAINDER X Y) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^MEMBER N L) (^BM^LESSP (^BM^COUNT (^BM^DELETE N L)) (^BM^COUNT L)))) (DEFINE (^BM^PERM A B) (IF (^BM^NLISTP A) (^BM^NLISTP B) (IF (^BM^MEMBER (^BM^CAR A) B) (^BM^PERM (^BM^CDR A) (^BM^DELETE (^BM^CAR A) B)) (^BM^FALSE)))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^TIMES Y X) Y) (^INT (^BM^ZERO)))) (LEMMA (^BM^IMPLIES (^BM^PRIME-LIST L2) (^BM^PRIME-LIST (^BM^DELETE X L2)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP C)) (^BM^MEMBER C L)) (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST L) C) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (^BM^QUOTIENT (^BM^TIMES Y X) Y) (IF (^BM^ZEROP Y) (^INT (^BM^ZERO)) (^BM^FIX X)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP A)) (^BM^DIVIDES A W)) (EQUAL (^BM^TIMES C (^BM^QUOTIENT W A)) (^BM^QUOTIENT (^BM^TIMES C W) A)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP C)) (^BM^MEMBER C L)) (EQUAL (^BM^TIMES-LIST (^BM^DELETE C L)) (^BM^QUOTIENT (^BM^TIMES-LIST L) C)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^PRIME C) (^BM^AND (^BM^PRIME-LIST L2) (^BM^NOT (^BM^MEMBER C L2)))) (^BM^NOT (EQUAL (^BM^REMAINDER (^BM^TIMES-LIST L2) C) (^INT (^BM^ZERO)))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP C)) (^BM^NOT (^BM^DIVIDES C X))) (^BM^NOT (EQUAL (^BM^TIMES C Y) X)))) (LEMMA (EQUAL (EQUAL (^BM^TIMES A B) (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^AND (^BM^NOT (EQUAL A (^INT (^BM^ZERO)))) (^BM^AND (^BM^NOT (EQUAL B (^INT (^BM^ZERO)))) (^BM^AND (^BM^NUMBERP A) (^BM^AND (^BM^NUMBERP B) (^BM^AND (EQUAL (^BM^SUB1 A) (^INT (^BM^ZERO))) (EQUAL (^BM^SUB1 B) (^INT (^BM^ZERO)))))))))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL (^BM^TIMES C (^BM^TIMES-LIST L1)) (^BM^TIMES-LIST L2)) (^BM^AND (^BM^PRIME C) (^BM^PRIME-LIST L2))) (^BM^MEMBER C L2))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP A)) (^BM^AND (^BM^NUMBERP C) (EQUAL (^BM^TIMES A C) B))) (EQUAL (EQUAL C (^BM^QUOTIENT B A)) (^BM^TRUE)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^PRIME-LIST L1) (^BM^AND (^BM^PRIME-LIST L2) (EQUAL (^BM^TIMES-LIST L1) (^BM^TIMES-LIST L2)))) (^BM^PERM L1 L2))) (DEFINE (^BM^MAXIMUM L) (IF (^BM^NLISTP L) (^INT (^BM^ZERO)) (IF (^BM^LESSP (^BM^CAR L) (^BM^MAXIMUM (^BM^CDR L))) (^BM^MAXIMUM (^BM^CDR L)) (^BM^CAR L)))) (LEMMA (^BM^IMPLIES (^BM^LISTP X) (^BM^MEMBER (^BM^MAXIMUM X) X))) (LEMMA (EQUAL (^BM^LESSP (^BM^COUNT (^BM^DELETE X L)) (^BM^COUNT L)) (^BM^MEMBER X L))) (DEFINE (^BM^ORDERED2 L) (IF (^BM^LISTP L) (IF (^BM^LISTP (^BM^CDR L)) (IF (^BM^LESSP (^BM^CAR L) (^BM^CAR (^BM^CDR L))) (^BM^FALSE) (^BM^ORDERED2 (^BM^CDR L))) (^BM^TRUE)) (^BM^TRUE))) (DEFINE (^BM^DSORT L) (IF (^BM^NLISTP L) (^NIL) (^BM^CONS (^BM^MAXIMUM L) (^BM^DSORT (^BM^DELETE (^BM^MAXIMUM L) L))))) (DEFINE (^BM^ADDTOLIST2 X L) (IF (^BM^LISTP L) (IF (^BM^LESSP X (^BM^CAR L)) (^BM^CONS (^BM^CAR L) (^BM^ADDTOLIST2 X (^BM^CDR L))) (^BM^CONS X L)) (^BM^CONS X (^NIL)))) (DEFINE (^BM^SORT2 L) (IF (^BM^NLISTP L) (^NIL) (^BM^ADDTOLIST2 (^BM^CAR L) (^BM^SORT2 (^BM^CDR L))))) (LEMMA (^BM^PLISTP (^BM^SORT2 X))) (LEMMA (^BM^ORDERED2 (^BM^SORT2 X))) (LEMMA (^BM^AND (^BM^PLISTP (^BM^SORT2 X)) (^BM^ORDERED2 (^BM^SORT2 X)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^PLISTP Y) (^BM^AND (^BM^ORDERED2 Y) (^BM^NOT (EQUAL X V)))) (EQUAL (^BM^ADDTOLIST2 V (^BM^DELETE X Y)) (^BM^DELETE X (^BM^ADDTOLIST2 V Y))))) (LEMMA (^BM^IMPLIES (^BM^PLISTP Y) (EQUAL (^BM^DELETE V (^BM^ADDTOLIST2 V Y)) Y))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP V W)) (EQUAL (^BM^ADDTOLIST2 V Y) (^BM^CONS V Y))) (EQUAL (^BM^ADDTOLIST2 V (^BM^ADDTOLIST2 W Y)) (^BM^CONS V (^BM^ADDTOLIST2 W Y))))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^LESSP V (^BM^MAXIMUM Z))) (EQUAL (^BM^ADDTOLIST2 V (^BM^SORT2 Z)) (^BM^CONS V (^BM^SORT2 Z))))) (LEMMA (^BM^IMPLIES (^BM^LISTP X) (EQUAL (^BM^CONS (^BM^MAXIMUM X) (^BM^DELETE (^BM^MAXIMUM X) (^BM^SORT2 X))) (^BM^SORT2 X)))) (LEMMA (EQUAL (^BM^SORT2 (^BM^DELETE X L)) (^BM^DELETE X (^BM^SORT2 L)))) (LEMMA (EQUAL (^BM^DSORT X) (^BM^SORT2 X))) (LEMMA (EQUAL (^BM^COUNT-LIST A (^BM^SORT2 L)) (^BM^COUNT-LIST A L))) (DEFINE (^BM^SIGMA M N) (IF (^BM^LESSP M N) (^BM^PLUS N (^BM^SIGMA M (^BM^SUB1 N))) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (^BM^DIFFERENCE X (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^SUB1 X))) (DEFINE (^BM^PROG-TRANS-OF-SIGMA I AC) (IF (^BM^ZEROP I) AC (^BM^PROG-TRANS-OF-SIGMA (^BM^DIFFERENCE I (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^PLUS AC I)))) (LEMMA (^BM^IMPLIES (^BM^NUMBERP AC) (EQUAL (^BM^PROG-TRANS-OF-SIGMA I AC) (^BM^PLUS AC (^BM^SIGMA (^INT (^BM^ZERO)) I))))) (LEMMA (EQUAL (^BM^PROG-TRANS-OF-SIGMA I (^INT (^BM^ZERO))) (^BM^SIGMA (^INT (^BM^ZERO)) I))) (LEMMA (^BM^AND (EQUAL (^INT (^BM^ZERO)) (^BM^SIGMA K K)) (^BM^LEQ K K))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP I)) (^BM^LEQ I K)) (^BM^AND (EQUAL (^BM^PLUS (^BM^SIGMA I K) I) (^BM^SIGMA (^BM^SUB1 I) K)) (^BM^LEQ (^BM^SUB1 I) K)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^ZEROP I) (^BM^LEQ I K)) (EQUAL (^BM^SIGMA I K) (^BM^SIGMA (^INT (^BM^ZERO)) K)))) (DEFINE (^BM^SET ADDR VAL MEM) (IF (^BM^ZEROP ADDR) (^BM^CONS VAL (^BM^CDR MEM)) (^BM^CONS (^BM^CAR MEM) (^BM^SET (^BM^SUB1 ADDR) VAL (^BM^CDR MEM))))) (DEFINE (^BM^GET ADDR MEM) (IF (^BM^ZEROP ADDR) (^BM^CAR MEM) (^BM^GET (^BM^SUB1 ADDR) (^BM^CDR MEM)))) (LEMMA (EQUAL (^BM^GET J (^BM^SET I VAL MEM)) (IF (^BM^EQP J I) VAL (^BM^GET J MEM)))) (DEFINE (^BM^EXECUTE1 PC MEM MAX) (IF (^BM^NOT (^BM^LESSP PC MAX)) (^BM^CONS (^BM^FALSE) (^BM^CONS MEM (^NIL))) (IF (EQUAL (^BM^GET PC MEM) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^FALSE) (^BM^CONS MEM (^NIL))) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^ZERO)))))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) (^BM^CONS MEM (^NIL))) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO))))))))) (IF (^BM^ZEROP (^BM^GET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) MEM)) (^BM^EXECUTE1 (^BM^ADD1 PC) MEM MAX) (^BM^EXECUTE1 (^BM^ADD1 (^BM^ADD1 PC)) MEM MAX)) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^EXECUTE1 (^BM^ADD1 PC) (^BM^SET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) (^BM^DIFFERENCE (^BM^GET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) MEM) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^GET PC MEM))))) MEM) MAX) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^EXECUTE1 (^BM^ADD1 PC) (^BM^SET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) (^BM^PLUS (^BM^CAR (^BM^CDR (^BM^CDR (^BM^GET PC MEM)))) (^BM^GET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) MEM)) MEM) MAX) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^ZERO)))))) (^BM^EXECUTE1 (^BM^ADD1 PC) (^BM^SET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) (^BM^PLUS (^BM^GET (^BM^CAR (^BM^CDR (^BM^CDR (^BM^GET PC MEM)))) MEM) (^BM^GET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) MEM)) MEM) MAX) (IF (EQUAL (^BM^CAR (^BM^GET PC MEM)) (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO)))))))) (^BM^EXECUTE1 (^BM^ADD1 PC) (^BM^SET (^BM^CAR (^BM^CDR (^BM^GET PC MEM))) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^GET PC MEM)))) MEM) MAX) (^BM^CONS (^BM^FALSE) (^BM^CONS MEM (^NIL)))))))))))) (DEFINE (^BM^EXECUTE PC MEM CLK) (IF (^BM^ZEROP CLK) MEM (IF (^BM^NUMBERP PC) (^BM^EXECUTE (^BM^CAR (^BM^EXECUTE1 PC MEM (^BM^LENGTH MEM))) (^BM^CAR (^BM^CDR (^BM^EXECUTE1 PC MEM (^BM^LENGTH MEM)))) (^BM^SUB1 CLK)) MEM))) (DEFINE (^BM^GET-SIMPLIFIER X) (IF (^BM^AND (^BM^LISTP X) (^BM^AND (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^G) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR X))) (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR X))) (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))))))) (IF (^BM^ZEROP (^BM^CAR (^BM^CDR (^BM^CAR (^BM^CDR X))))) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR X))) (^NIL))) (^BM^CONS (^BM^PACK (^BM^CONS (^G) (^BM^CONS (^E) (^BM^CONS (^T) (^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^SUB1 (^BM^CAR (^BM^CDR (^BM^CAR (^BM^CDR X))))) (^NIL))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR X))) (^NIL))) (^NIL))))) X)) (DEFINE (^BM^SET-SIMPLIFIER X) (IF (^BM^AND (^BM^LISTP X) (^BM^AND (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^E) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^AND (^BM^LISTP (^BM^CAR (^BM^CDR X))) (EQUAL (^BM^CAR (^BM^CAR (^BM^CDR X))) (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))))))) (IF (^BM^ZEROP (^BM^CAR (^BM^CDR (^BM^CAR (^BM^CDR X))))) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR X))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR X)))) (^NIL))) (^NIL)))) (^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^CAR (^BM^CDR (^BM^CDR (^BM^CDR X)))) (^NIL))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^E) (^BM^CONS (^T) (^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^SUB1 (^BM^CAR (^BM^CDR (^BM^CAR (^BM^CDR X))))) (^NIL))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR X))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR X)))) (^NIL))) (^NIL))))) (^NIL))))) X)) (LEMMA (^BM^IMPLIES (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR X))))) (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (EQUAL (^BM^LENGTH X) (^BM^PLUS (^INT (^BM^CONS (^5) (^BM^ZERO))) (^BM^LENGTH (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR X)))))))))) (LEMMA (EQUAL (^BM^LENGTH (^BM^CONS X1 (^BM^CONS X2 (^BM^CONS X3 (^BM^CONS X4 (^BM^CONS X5 (^BM^CONS X6 X7))))))) (^BM^PLUS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^LENGTH X7)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^LESSP MAX (^INT (^BM^CONS (^6) (^BM^ZERO))))) (EQUAL (^BM^EXECUTE1 (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) L)))))) MAX) (IF (^BM^ZEROP (^BM^CAR L)) (^BM^EXECUTE1 (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) L)))))) MAX) (^BM^EXECUTE1 (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) L)))))) MAX))))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^LESSP MAX (^INT (^BM^CONS (^6) (^BM^ZERO))))) (EQUAL (^BM^EXECUTE1 (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) L)))))) MAX) (^BM^EXECUTE1 (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^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^CAR L) (^BM^CONS (^BM^PLUS (^BM^CAR L) (^BM^CAR (^BM^CDR L))) (^BM^CDR (^BM^CDR L)))))))))) MAX)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^LESSP MAX (^INT (^BM^CONS (^6) (^BM^ZERO))))) (EQUAL (^BM^EXECUTE1 (^INT (^BM^CONS (^4) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) L)))))) MAX) (^BM^EXECUTE1 (^INT (^BM^CONS (^5) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^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^DIFFERENCE (^BM^CAR L) (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^CDR L)))))))) MAX)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP MAX (^INT (^BM^CONS (^6) (^BM^ZERO))))) (^BM^AND (EQUAL (^BM^CAR MEM) (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR MEM)) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR MEM))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^ZERO))))) (^BM^CONS (^INT (^BM^CONS (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))))))) (EQUAL (^BM^EXECUTE1 (^INT (^BM^CONS (^1) (^BM^ZERO))) MEM MAX) (IF (^BM^ZEROP (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))) (^BM^CONS (^BM^FALSE) (^BM^CONS (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))))))) (^NIL))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^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^SUB1 (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))) (^BM^CONS (^BM^PLUS (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))))) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))))))) (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))))))))))) (^NIL))))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NUMBERP PC) (^BM^NOT (^BM^ZEROP CLK))) (EQUAL (^BM^EXECUTE PC MEM CLK) (^BM^EXECUTE (^BM^CAR (^BM^EXECUTE1 PC MEM (^BM^LENGTH MEM))) (^BM^CAR (^BM^CDR (^BM^EXECUTE1 PC MEM (^BM^LENGTH MEM)))) (^BM^SUB1 CLK))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP CLK (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))))))) (^BM^AND (EQUAL (^BM^CAR MEM) (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^ZERO)) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR MEM)) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR MEM))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^ZERO))))) (^BM^CONS (^INT (^BM^CONS (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^AND (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^I) (^BM^ZERO)))))) (^BM^CONS (^INT (^BM^CONS (^6) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^J) (^BM^CONS (^U) (^BM^CONS (^M) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))))))) (EQUAL (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^EXECUTE (^INT (^BM^CONS (^1) (^BM^ZERO))) MEM CLK))))))))) (IF (^BM^ZEROP (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))) (^BM^PLUS (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM)))))))) (^BM^SIGMA (^INT (^BM^ZERO)) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR MEM))))))))))))) (LEMMA (EQUAL (^BM^EXECUTE (^INT (^BM^ZERO)) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) MEM)))))) CLK) (IF (^BM^ZEROP CLK) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) MEM)))))) (^BM^EXECUTE (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^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^CAR MEM) (^BM^CONS (^INT (^BM^ZERO)) (^BM^CDR (^BM^CDR MEM)))))))))) CLK)))) (LEMMA (^BM^IMPLIES (^BM^AND (EQUAL MEM (^BM^APPEND (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^M) (^BM^CONS (^O) (^BM^CONS (^V) (^BM^CONS (^E) (^BM^CONS (^I) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^7) (^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 (^S) (^BM^CONS (^K) (^BM^CONS (^I) (^BM^CONS (^P) (^BM^CONS (^N) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CONS (^INT (^BM^CONS (^6) (^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^CONS (^O) (^BM^CONS (^P) (^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 (^7) (^BM^ZERO))) (^BM^CONS (^INT (^BM^CONS (^6) (^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 (^6) (^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 (^A) (^BM^ZERO))))))) (^BM^CONS (^INT (^BM^CONS (^1) (^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))))))))))) TL)) (^BM^AND (EQUAL I (^BM^GET (^INT (^BM^CONS (^6) (^BM^ZERO))) MEM)) (^BM^NOT (^BM^LESSP CLK I)))) (EQUAL (^BM^GET (^INT (^BM^CONS (^7) (^BM^ZERO))) (^BM^EXECUTE (^INT (^BM^ZERO)) MEM CLK)) (IF (^BM^ZEROP CLK) (^BM^GET (^INT (^BM^CONS (^7) (^BM^ZERO))) MEM) (^BM^SIGMA (^INT (^BM^ZERO)) I))))) (LEMMA (EQUAL (^BM^DIFFERENCE (^BM^ADD1 (^BM^ADD1 X)) (^INT (^BM^CONS (^2) (^BM^ZERO)))) (^BM^FIX X))) (LEMMA (EQUAL (^BM^QUOTIENT (^BM^PLUS X (^BM^PLUS X Y)) (^INT (^BM^CONS (^2) (^BM^ZERO)))) (^BM^PLUS X (^BM^QUOTIENT Y (^INT (^BM^CONS (^2) (^BM^ZERO))))))) (LEMMA (EQUAL (^BM^SIGMA (^INT (^BM^ZERO)) I) (^BM^QUOTIENT (^BM^TIMES I (^BM^ADD1 I)) (^INT (^BM^CONS (^2) (^BM^ZERO)))))) (DEFINE (^BM^H X Y) (^INT (^BM^ZERO))) (LEMMA (EQUAL (^BM^H X (^BM^H Y Z)) (^BM^H Y (^BM^H X Z)))) (DEFINE (^BM^H-PR L AC) (IF (^BM^NLISTP L) AC (^BM^H (^BM^CAR L) (^BM^H-PR (^BM^CDR L) AC)))) (DEFINE (^BM^H-AC L AC) (IF (^BM^NLISTP L) AC (^BM^H-AC (^BM^CDR L) (^BM^H (^BM^CAR L) AC)))) (LEMMA (EQUAL (^BM^H-PR X (^BM^H Z A)) (^BM^H Z (^BM^H-PR X A)))) (LEMMA (EQUAL (^BM^H-AC L AC) (^BM^H-PR L AC))) (DEFINE (^BM^F0 X) (IF (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^CONS (^0) (^BM^ZERO))))) X) (^BM^DIFFERENCE X (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))) (^INT (^BM^CONS (^9) (^BM^CONS (^1) (^BM^ZERO)))))) (DEFINE (^BM^EVEN X) (EQUAL (^INT (^BM^ZERO)) (^BM^REMAINDER X (^INT (^BM^CONS (^2) (^BM^ZERO)))))) (DEFINE (^BM^SQUARE X) (^BM^TIMES X X)) (LEMMA (EQUAL (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^ZERO))) X) (^BM^FIX X))) (LEMMA (EQUAL (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) X) (^BM^PLUS X X))) (LEMMA (EQUAL (^BM^EXP (^INT (^BM^ZERO)) K) (IF (^BM^ZEROP K) (^INT (^BM^CONS (^1) (^BM^ZERO))) (^INT (^BM^ZERO))))) (LEMMA (EQUAL (^BM^EXP (^INT (^BM^CONS (^1) (^BM^ZERO))) K) (^INT (^BM^CONS (^1) (^BM^ZERO))))) (LEMMA (EQUAL (^BM^EXP X (^INT (^BM^ZERO))) (^INT (^BM^CONS (^1) (^BM^ZERO))))) (LEMMA (EQUAL (^BM^EXP (^BM^TIMES I J) K) (^BM^TIMES (^BM^EXP I K) (^BM^EXP J K)))) (LEMMA (EQUAL (^BM^EXP (^BM^EXP I J) K) (^BM^EXP I (^BM^TIMES J K)))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^PLUS X (^BM^TIMES I J)) J) (^BM^REMAINDER X J))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^PLUS X (^BM^TIMES J I)) J) (^BM^REMAINDER X J))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^TIMES B (^BM^TIMES A C)) A) (^INT (^BM^ZERO)))) (LEMMA (EQUAL (^BM^REMAINDER (^INT (^BM^CONS (^1) (^BM^ZERO))) X) (IF (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^INT (^BM^ZERO)) (^INT (^BM^CONS (^1) (^BM^ZERO)))))) (LEMMA (EQUAL (EQUAL (^BM^LENGTH X) (^INT (^BM^ZERO))) (^BM^NLISTP X))) (LEMMA (EQUAL (^BM^LENGTH (^BM^DELETE X L)) (IF (^BM^MEMBER X L) (^BM^LENGTH (^BM^CDR L)) (^BM^LENGTH L)))) (LEMMA (EQUAL (^BM^REMAINDER (^BM^DIFFERENCE (^BM^TIMES P X) (^BM^TIMES P Y)) P) (^INT (^BM^ZERO)))) (LEMMA (^BM^IMPLIES (^BM^PRIME P) (EQUAL (EQUAL (^BM^REMAINDER (^BM^TIMES A B) P) (^INT (^BM^ZERO))) (^BM^OR (EQUAL (^BM^REMAINDER A P) (^INT (^BM^ZERO))) (EQUAL (^BM^REMAINDER B P) (^INT (^BM^ZERO))))))) (LEMMA (^BM^IMPLIES (^BM^MEMBER X L) (EQUAL (^BM^TIMES X (^BM^TIMES-LIST (^BM^DELETE X L))) (^BM^TIMES-LIST L)))) (LEMMA (^BM^IMPLIES (^BM^NOT (^BM^ZEROP Y)) (^BM^LESSP (^BM^REMAINDER X Y) Y))) (DEFINE (^BM^APPLY2 FN X Y) (CONS 'APPLY2 (CONS FN (CONS X (CONS Y 'NIL))))) (DEFINE (^BM^EVAL2 FORM ENVRN) (IF (^BM^NUMBERP FORM) FORM (IF (^BM^LITATOM FORM) (^BM^CDR (^BM^ASSOC FORM ENVRN)) (IF (^BM^LISTP FORM) (^BM^APPLY2 (^BM^CAR FORM) (^BM^EVAL2 (^BM^CAR (^BM^CDR FORM)) ENVRN) (^BM^EVAL2 (^BM^CAR (^BM^CDR (^BM^CDR FORM))) ENVRN)) FORM)))) (DEFINE (^BM^SUBST2 NEW OLD TERM) (IF (^BM^NUMBERP TERM) TERM (IF (^BM^LITATOM TERM) (IF (EQUAL OLD TERM) NEW TERM) (IF (^BM^LISTP TERM) (^BM^CONS (^BM^CAR TERM) (^BM^CONS (^BM^SUBST2 NEW OLD (^BM^CAR (^BM^CDR TERM))) (^BM^CONS (^BM^SUBST2 NEW OLD (^BM^CAR (^BM^CDR (^BM^CDR TERM)))) (^NIL)))) TERM)))) (LEMMA (EQUAL (^BM^EVAL2 (^BM^SUBST2 NEW OLD TERM) A) (^BM^EVAL2 TERM (^BM^CONS (^BM^CONS OLD (^BM^EVAL2 NEW A)) A))))