(NOTE-LIB "nqthm-boot") (DEFINE (^BM^BTMP X) (IF (CONSP X) (IF (EQUAL (CAR X) '^BM^BTM) (EQUAL (CDR X) 'NIL) 'FALSE) 'FALSE)) (DEFINE (^BM^BTM) (CONS '^BM^BTM 'NIL)) (DEFINE (^BM^GET X ALIST) (IF (^BM^NLISTP ALIST) (^BM^BTM) (IF (EQUAL X (^BM^CAR (^BM^CAR ALIST))) (^BM^CDR (^BM^CAR ALIST)) (^BM^GET X (^BM^CDR ALIST))))) (DEFINE (^BM^UNSOLV-SUBRP FN) (^BM^MEMBER FN (^BM^CONS (^BM^PACK (^BM^CONS (^Z) (^BM^CONS (^E) (^BM^CONS (^R) (^BM^CONS (^O) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^R) (^BM^CONS (^U) (^BM^CONS (^E) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^F) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^S) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^CONS (^N1) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^N1) (^BM^ZERO)))))) (^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^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO))))) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO))))) (^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 (^P) (^BM^CONS (^A) (^BM^CONS (^C) (^BM^CONS (^K) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^U) (^BM^CONS (^N) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^CONS (^C) (^BM^CONS (^K) (^BM^ZERO)))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^T) (^BM^CONS (^O) (^BM^CONS (^M) (^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^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))))))))))))))) (DEFINE (^BM^UNSOLV-APPLY-SUBR FN LST) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^Z) (^BM^CONS (^E) (^BM^CONS (^R) (^BM^CONS (^O) (^BM^ZERO))))))) (^BM^ZERO) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^T) (^BM^CONS (^R) (^BM^CONS (^U) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^TRUE) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^F) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^S) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^FALSE) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^D) (^BM^CONS (^D) (^BM^CONS (^N1) (^BM^ZERO))))))) (^BM^ADD1 (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^S) (^BM^CONS (^U) (^BM^CONS (^B) (^BM^CONS (^N1) (^BM^ZERO))))))) (^BM^SUB1 (^BM^CAR LST)) (IF (EQUAL FN (^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^NUMBERP (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^O) (^BM^CONS (^N) (^BM^CONS (^S) (^BM^ZERO))))))) (^BM^CONS (^BM^CAR LST) (^BM^CAR (^BM^CDR LST))) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO))))))) LST (IF (EQUAL FN (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^A) (^BM^CONS (^R) (^BM^ZERO)))))) (^BM^CAR (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^D) (^BM^CONS (^R) (^BM^ZERO)))))) (^BM^CDR (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^CONS (^P) (^BM^ZERO)))))))) (^BM^LISTP (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^P) (^BM^CONS (^A) (^BM^CONS (^C) (^BM^CONS (^K) (^BM^ZERO))))))) (^BM^PACK (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^U) (^BM^CONS (^N) (^BM^CONS (^P) (^BM^CONS (^A) (^BM^CONS (^C) (^BM^CONS (^K) (^BM^ZERO))))))))) (^BM^UNPACK (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^T) (^BM^CONS (^A) (^BM^CONS (^T) (^BM^CONS (^O) (^BM^CONS (^M) (^BM^ZERO)))))))))) (^BM^LITATOM (^BM^CAR LST)) (IF (EQUAL FN (^BM^PACK (^BM^CONS (^E) (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))))))) (EQUAL (^BM^CAR LST) (^BM^CAR (^BM^CDR LST))) (^INT (^BM^ZERO)))))))))))))))))) (DEFINE (^BM^EV FLG X VA FA N) (IF (EQUAL FLG (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO))))) (IF (^BM^NLISTP X) (IF (^BM^NUMBERP X) X (IF (EQUAL X (^BM^PACK (^BM^CONS (^T) (^BM^ZERO)))) (^BM^TRUE) (IF (EQUAL X (^BM^PACK (^BM^CONS (^F) (^BM^ZERO)))) (^BM^FALSE) (IF (EQUAL X (^NIL)) (^NIL) (^BM^GET X VA))))) (IF (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO)))))))) (^BM^CAR (^BM^CDR X)) (IF (EQUAL (^BM^CAR X) (^BM^PACK (^BM^CONS (^I) (^BM^CONS (^F) (^BM^ZERO))))) (IF (^BM^BTMP (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR X)) VA FA N)) (^BM^BTM) (IF (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR X)) VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^CDR X))) VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CDR X)))) VA FA N))) (IF (^BM^BTMP (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CDR X) VA FA N)) (^BM^BTM) (IF (^BM^UNSOLV-SUBRP (^BM^CAR X)) (^BM^UNSOLV-APPLY-SUBR (^BM^CAR X) (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CDR X) VA FA N)) (IF (^BM^BTMP (^BM^GET (^BM^CAR X) FA)) (^BM^BTM) (IF (^BM^ZEROP N) (^BM^BTM) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^GET (^BM^CAR X) FA))) (^BM^PAIRLIST (^BM^CAR (^BM^GET (^BM^CAR X) FA)) (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CDR X) VA FA N)) FA (^BM^SUB1 N))))))))) (IF (^BM^LISTP X) (IF (^BM^BTMP (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR X) VA FA N)) (^BM^BTM) (IF (^BM^BTMP (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CDR X) VA FA N)) (^BM^BTM) (^BM^CONS (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR X) VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CDR X) VA FA N)))) (^NIL)))) (DEFINE (^BM^PR-EVAL X VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X VA FA N)) (DEFINE (^BM^EVLIST X VA FA N) (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) X VA FA N)) (DEFINE (^BM^SUBLIS ALIST X) (IF (^BM^NLISTP X) (IF (^BM^ASSOC X ALIST) (^BM^CDR (^BM^ASSOC X ALIST)) X) (^BM^CONS (^BM^SUBLIS ALIST (^BM^CAR X)) (^BM^SUBLIS ALIST (^BM^CDR X))))) (DEFINE (^BM^X FA) (^BM^SUBLIS (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^I) (^BM^CONS (^R) (^BM^CONS (^C) (^BM^ZERO)))))) (^BM^CONS FA (^INT (^BM^ZERO)))) (^NIL)) (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^I) (^BM^CONS (^R) (^BM^CONS (^C) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (DEFINE (^BM^FA FA) (^BM^APPEND (^BM^SUBLIS (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^I) (^BM^CONS (^R) (^BM^CONS (^C) (^BM^ZERO)))))) (^BM^CONS FA (^INT (^BM^ZERO)))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^O) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^CONS FA (^INT (^BM^CONS (^1) (^BM^ZERO))))) (^NIL))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^I) (^BM^CONS (^R) (^BM^CONS (^C) (^BM^ZERO)))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^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 (^H) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^T) (^BM^CONS (^S) (^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^CONS (^BM^PACK (^BM^CONS (^C) (^BM^CONS (^I) (^BM^CONS (^R) (^BM^CONS (^C) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^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 (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^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 (^Q) (^BM^CONS (^U) (^BM^CONS (^O) (^BM^CONS (^T) (^BM^CONS (^E) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^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 (^A) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^O) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^T) (^BM^ZERO))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))))))) (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^O) (^BM^CONS (^O) (^BM^CONS (^P) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO))))) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^O) (^BM^CONS (^O) (^BM^CONS (^P) (^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)))))))) FA)) (DEFINE (^BM^VA FA) (^BM^CONS (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^BM^ZERO))) (^BM^FA FA)) (^NIL))) (DEFINE (^BM^K N) (^BM^ADD1 N)) (DEFINE (^BM^OCCUR X Y) (IF (EQUAL X Y) (^BM^TRUE) (IF (^BM^NLISTP Y) (^BM^FALSE) (^BM^OR (^BM^OCCUR X (^BM^CAR Y)) (^BM^OCCUR X (^BM^CDR Y)))))) (DEFINE (^BM^OCCUR-IN-DEFNS X LST) (IF (^BM^NLISTP LST) (^BM^FALSE) (^BM^OR (^BM^OCCUR X (^BM^CAR (^BM^CDR (^BM^CDR (^BM^CAR LST))))) (^BM^OCCUR-IN-DEFNS X (^BM^CDR LST))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^OCCUR-IN-DEFNS FN FA)) (^BM^NOT (^BM^BTMP (^BM^GET X FA)))) (^BM^NOT (^BM^OCCUR FN (^BM^CAR (^BM^CDR (^BM^GET X FA))))))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^OCCUR FN X)) (^BM^NOT (^BM^OCCUR-IN-DEFNS FN FA))) (EQUAL (^BM^EV FLG X VA (^BM^CONS (^BM^CONS FN DEF) FA) N) (^BM^EV FLG X VA FA N)))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^COUNT Y) (^BM^COUNT X)) (^BM^NOT (^BM^OCCUR X Y)))) (LEMMA (^BM^LESSP (^BM^COUNT (^BM^CAR (^BM^CDR (^BM^GET FN FA)))) (^BM^ADD1 (^BM^COUNT FA)))) (LEMMA (^BM^IMPLIES (^BM^LESSP (^BM^COUNT FA) (^BM^COUNT X)) (^BM^NOT (^BM^OCCUR-IN-DEFNS X FA)))) (LEMMA (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^GET (^BM^PACK (^BM^CONS (^H) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^T) (^BM^CONS (^S) (^BM^ZERO))))))) FA))) VA (^BM^CONS (^BM^CONS (^BM^CONS FA (^INT (^BM^ZERO))) DEF0) (^BM^CONS (^BM^CONS (^BM^CONS FA (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^CONS (^NIL) (^BM^CONS (^BM^CONS (^BM^CONS FA (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^NIL)) (^NIL)))) FA)) N) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^GET (^BM^PACK (^BM^CONS (^H) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^T) (^BM^CONS (^S) (^BM^ZERO))))))) FA))) VA FA N))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^BTMP (^BM^EV FLG X VA FA N))) (^BM^NOT (^BM^BTMP (^BM^EV FLG X VA FA K)))) (EQUAL (^BM^EV FLG X VA FA N) (^BM^EV FLG X VA FA K)))) (LEMMA (^BM^IMPLIES (EQUAL (^BM^EV FLG X VA FA N) (^BM^TRUE)) (^BM^EV FLG X VA FA K))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^LISTP X) (^BM^AND (^BM^LISTP (^BM^CAR X)) (^BM^AND (^BM^NLISTP (^BM^CDR X)) (^BM^AND (^BM^LISTP (^BM^GET (^BM^CAR X) FA)) (^BM^AND (EQUAL (^BM^CAR (^BM^GET (^BM^CAR X) FA)) (^NIL)) (EQUAL (^BM^CAR (^BM^CDR (^BM^GET (^BM^CAR X) FA))) X)))))) (^BM^BTMP (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) X VA FA N)))) (LEMMA (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^BTMP VAL)) (^BM^NOT (^BM^BTMP (^BM^GET (^BM^CONS FN (^INT (^BM^ZERO))) FA)))) (EQUAL (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CONS (^BM^CONS FN (^INT (^BM^ZERO))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^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^ZERO))) VAL) (^NIL)) FA J) (IF (^BM^ZEROP J) (^BM^BTM) (^BM^EV (^BM^PACK (^BM^CONS (^A) (^BM^CONS (^L) (^BM^ZERO)))) (^BM^CAR (^BM^CDR (^BM^GET (^BM^CONS FN (^INT (^BM^ZERO))) FA))) (^BM^PAIRLIST (^BM^CAR (^BM^GET (^BM^CONS FN (^INT (^BM^ZERO))) FA)) (^BM^EV (^BM^PACK (^BM^CONS (^L) (^BM^CONS (^I) (^BM^CONS (^S) (^BM^CONS (^T) (^BM^ZERO)))))) (^BM^CONS (^BM^PACK (^BM^CONS (^A) (^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^ZERO))) VAL) (^NIL)) FA J)) FA (^BM^SUB1 J)))))) (DEFINE (^BM^SEXP X) (IF (EQUAL X (^BM^TRUE)) (^BM^TRUE) (IF (EQUAL X (^BM^FALSE)) (^BM^TRUE) (IF (^BM^NUMBERP X) (^BM^TRUE) (IF (^BM^LISTP X) (^BM^AND (^BM^SEXP (^BM^CAR X)) (^BM^SEXP (^BM^CDR X))) (IF (^BM^LITATOM X) (^BM^SEXP (^BM^UNPACK X)) (^BM^FALSE))))))) (LEMMA (^BM^AND (^BM^IMPLIES (EQUAL H (^BM^PR-EVAL (^BM^CONS (^BM^PACK (^BM^CONS (^H) (^BM^CONS (^A) (^BM^CONS (^L) (^BM^CONS (^T) (^BM^CONS (^S) (^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^X FA) (^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^VA FA) (^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^FA FA) (^NIL))) (^NIL))))) (^NIL) FA N)) (^BM^AND (^BM^IMPLIES (EQUAL H (^BM^FALSE)) (^BM^NOT (^BM^BTMP (^BM^PR-EVAL (^BM^X FA) (^BM^VA FA) (^BM^FA FA) (^BM^K N))))) (^BM^IMPLIES (EQUAL H (^BM^TRUE)) (^BM^BTMP (^BM^PR-EVAL (^BM^X FA) (^BM^VA FA) (^BM^FA FA) K))))) (^BM^IMPLIES (^BM^SEXP FA) (^BM^AND (^BM^SEXP (^BM^X FA)) (^BM^AND (^BM^SEXP (^BM^VA FA)) (^BM^SEXP (^BM^FA FA)))))))