acl2/ml/defaxioms.lisp.trans.ml

592 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ") (
604 "ASSOC-EQ") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
610 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQUAL") (
622 "ASSOC-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
629 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2" "X") (mksym
646 "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL-ALISTP") (mkpair (
658 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
677 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ-EQUAL") (
901 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "COMMON-LISP" "ASSOC") (
913 "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym "COMMON-LISP"
1188 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
1220 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mkpair (mksym
1306 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
1507 "ASSOC-STRING-EQUAL") (mkpair (mkpair (mksym "ACL2" "STR") (mkpair (mksym
1518 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-STRING-EQUAL") (
3627 mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "TREE") (
3966 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
4252 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
4261 mkpair (mksym "ACL2" "L") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
4324 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
4330 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
4337 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
4535 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
4540 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
4548 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
4562 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
4572 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
4585 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
4598 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
4622 "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2"
4663 mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "I") (mkpair (mksym "ACL2"
5240 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
5841 mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
5853 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
5860 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
5872 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
6120 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (
6169 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (
6877 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
6898 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
7015 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
7040 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
7089 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (
7155 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (
7191 "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (mkpair (mksym "ACL2"
7205 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
7234 "ASSOC-EQ") (mkpair (mksym "ACL2" "CHANNEL") (mkpair (mkpair (mksym "ACL2"
7276 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym
7740 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQ") (
7760 "PUT-ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
7767 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQL") (
7787 "PUT-ASSOC-EQL") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
7794 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PUT-ASSOC-EQUAL") (
7814 "PUT-ASSOC-EQUAL") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "VAL") (
7826 mksym "ACL2" "PUT-ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym
7837 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (
7975 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (
8219 "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8225 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8239 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
8251 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
8258 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
8272 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
8279 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
8308 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8385 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "DELETE-ASSOC-EQ") (
8399 "DELETE-ASSOC-EQ") (mkpair (mksym "ACL2" "KEY") (mkpair (mkpair (mksym
8407 "DELETE-ASSOC-EQUAL") (mkpair (mkpair (mksym "ACL2" "KEY") (mkpair (mksym
8420 "NIL"))) (mkpair (mkpair (mksym "ACL2" "DELETE-ASSOC-EQUAL") (mkpair (mksym
8430 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
8437 "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
8451 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
8458 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8473 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
8480 "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym
8494 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
8514 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
8538 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8547 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8565 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
8592 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
10553 "COMMON-LISP" "ASSOC") (mkpair (mksym "COMMON-LISP" "BOOLE-ORC2") (mkpair (
10554 mksym "COMMON-LISP" "CDADAR") (mkpair (mksym "COMMON-LISP" "ASSOC-IF") (
10556 "CDADDR") (mkpair (mksym "COMMON-LISP" "ASSOC-IF-NOT") (mkpair (mksym
11342 "WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP") (mkpair (mkpair (mksym "ACL2"
11345 "ASSOC-EQ-EQUAL-ALISTP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
11400 "KEYWORD-VALUE-LISTP-ASSOC-KEYWORD") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
11403 "KEYWORD-VALUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11409 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "CONSP-ASSOC-EQ") (
11413 "CONSP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2"
11416 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym
11419 "ASSOC-EQ") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "L") (mksym
11435 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11441 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11444 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
11452 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
11454 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11464 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11467 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11475 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11477 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11487 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11489 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11498 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11500 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11506 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11509 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11519 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11521 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11530 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11532 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11569 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11571 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11580 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11582 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11588 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11591 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11600 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11603 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11624 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11630 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11633 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
11641 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
11643 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11653 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11656 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11665 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11667 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11675 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (
11678 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11688 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11690 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11701 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11703 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11712 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11715 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
11722 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11725 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11732 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
11734 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
11744 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
11746 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
11755 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11757 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11765 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11767 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11808 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11810 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11821 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11823 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
11832 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (
11835 mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP"
11842 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11845 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11852 "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (
11854 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
11863 mkpair (mkpair (mksym "ACL2" "ASSOC-KEYWORD") (mkpair (mkpair (mksym
11866 mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (
11880 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "CONSP-ASSOC") (mkpair (
11884 mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "NAME") (
11887 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2"
11890 "ASSOC") (mkpair (mksym "ACL2" "NAME") (mkpair (mksym "ACL2" "L") (mksym
11902 "ASSOC-KEYWORD") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym
11904 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
12302 "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (
12316 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
12325 "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "ACL2"
12338 mkpair (mksym "COMMON-LISP" "ASSOC") (mkpair (mkpair (mksym "COMMON-LISP"
12658 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
12712 "TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ") (mkpair (mkpair (mksym
12715 "TRUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (mksym "ACL2"
12722 "TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P") (mkpair (mkpair (mksym "ACL2"
12726 mksym "COMMON-LISP" "CDR") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (mkpair (
12939 (mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "ASSOC-ADD-PAIR") (
12947 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "SYM1") (mkpair (mkpair (mksym
12955 "ASSOC") (mkpair (mksym "ACL2" "SYM1") (mkpair (mksym "ACL2" "ALIST") (mksym
13001 "ALL-BOUNDP-PRESERVES-ASSOC") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
13010 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "ASSOC-EQ") (
13020 "COMMON-LISP" "ASSOC") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
13066 "TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQUAL") (mkpair (mkpair (mksym
13069 "TRUE-LISTP") (mkpair (mkpair (mksym "ACL2" "ASSOC-EQUAL") (mkpair (mksym