round-trip/gold/axioms.sml

741 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") (
753 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
759 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (
771 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
778 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym
795 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair (
807 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
826 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
1665 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") (
1677 "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
2003 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
2035 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
2208 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
2457 "ASSOC-STRING-EQUAL") (mkpair (mkpair (mksym "ACL2" "STR") (mkpair (mksym
2468 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-STRING-EQUAL") (
3065 "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP" "BOOLE-ORC2") (mkpair (
3066 mksym "COMMON-LISP" "CDADAR") (mkpair (mksym "COMMON-LISP" "ASSOC-IF") (
3068 "CDADDR") (mkpair (mksym "COMMON-LISP" "ASSOC-IF-NOT") (mkpair (mksym
4600 "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
4602 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
4605 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
6492 mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "TREE") (
6561 "PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym
6564 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
6884 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
7238 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
7247 mkpair (mksym "ACL2" "L") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
7256 "KEYWORD-VALUE-LISTP-ASSOC-KEYWORD") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
7259 "KEYWORD-VALUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7265 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "CONSP-ASSOC-EQ") (
7269 "CONSP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2"
7272 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym
7275 "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "L") (mksym
7337 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7343 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7350 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7370 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7376 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7379 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
7387 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
7389 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7399 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7402 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
7410 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7412 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7422 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7424 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7433 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7435 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7441 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7444 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7454 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7456 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7465 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7467 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7504 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7506 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7515 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7517 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7523 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7526 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7535 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7538 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
7737 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7742 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7750 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7770 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7776 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7779 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
7787 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
7789 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7799 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7802 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
7811 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7813 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7821 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
7824 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7834 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7836 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7847 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7849 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7858 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7861 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
7868 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7871 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
7878 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
7880 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
7890 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
7892 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
7901 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7903 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7911 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7913 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7954 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7956 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7967 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
7969 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
7978 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
7981 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
7988 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
7991 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
7998 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
8000 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
8009 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
8012 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
8029 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
8039 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8052 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8065 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8074 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "CONSP-ASSOC") (mkpair (
8078 mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "NAME") (
8081 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2"
8084 "ASSOC") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "L") (mksym
8106 "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2"
8147 mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "I") (mkpair (mksym "ACL2"
8191 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
8302 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8304 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
9023 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
9876 "ACONS") (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP"
9890 "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym "ACL2"
10141 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
10153 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
10160 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
10172 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
10429 "ACONS") (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP"
10443 "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym "ACL2"
10695 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
10709 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
10718 "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2"
10731 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
11012 "ACONS") (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP"
11026 "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym "ACL2"
11337 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (
11386 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (
11442 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (
11590 "ACONS") (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP"
11604 "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym "ACL2"
11852 mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
12000 "ACONS") (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP"
12014 "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym "ACL2"
12262 mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
13016 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
13351 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
13601 "TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ") (mkpair (mkpair (mksym
13604 "TRUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2"
13611 "TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P") (mkpair (mkpair (mksym "ACL2"
13615 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
13636 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
13657 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
13990 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
14005 mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
14016 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym
14041 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
14066 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
14162 "ASSOC-EQUAL") (mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym
14268 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
14525 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (
14561 "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (mkpair (mksym "ACL2"
14575 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
14604 "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (mkpair (mksym "ACL2"
14646 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym
15030 "ALL-BOUNDP-PRESERVES-ASSOC") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
15039 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
15049 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
15492 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQ") (
15512 "PUT-ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
15519 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQL") (
15539 "PUT-ASSOC-EQL") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
15546 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQUAL") (
15566 "PUT-ASSOC-EQUAL") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
15578 mksym "ACL2" "PUT-ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym
15589 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (
15765 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "ASSOC-ADD-PAIR") (
15773 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "SYM1") (mkpair (mkpair (mksym
15781 "ASSOC") (mkpair (mksym "ACL2" "SYM1") (mkpair (mksym "ACL2" "ALIST") (mksym
16083 mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mkpair (mksym "ACL2"
16207 "TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL") (mkpair (mkpair (mksym
16210 "TRUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym
16613 "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
16619 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
16633 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
16678 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
16685 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
16699 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
16706 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
16729 "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
16805 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "DELETE-ASSOC-EQ") (
16819 "DELETE-ASSOC-EQ") (mkpair (mksym "ACL2" "KEY") (mkpair (mkpair (mksym
16827 "DELETE-ASSOC-EQUAL") (mkpair (mkpair (mksym "ACL2" "KEY") (mkpair (mksym
16840 "NIL"))) (mkpair (mkpair (mksym "ACL2" "DELETE-ASSOC-EQUAL") (mkpair (mksym
16860 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
16867 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
16894 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
16901 "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
16916 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
16923 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
16937 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
16957 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
16981 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
16990 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
17008 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
17035 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (