(SET-EQUIV-IMPLIES-EQUAL-NOT-INTERSECTP-LIST-2
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (5 5 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 )
(FLATTEN-EQUIV)
(FLATTEN-EQUIV-IS-AN-EQUIVALENCE)
(FLATTEN-EQUIV-IMPLIES-EQUAL-NOT-INTERSECTP-LIST-2-LEMMA-1
 (3799 70 (:DEFINITION TRUE-LIST-LISTP))
 (2572 15 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (2335 112 (:DEFINITION TRUE-LISTP))
 (2281 107 (:DEFINITION MEMBER-EQUAL))
 (2163 20 (:DEFINITION INTERSECTP-EQUAL))
 (2068 19 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (2047 112 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (1792 113 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (1702 218 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1548 218 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1507 45 (:REWRITE REMOVE-WHEN-ABSENT))
 (1125 154 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1110 190 (:DEFINITION STRING-LISTP))
 (926 926 (:TYPE-PRESCRIPTION STRING-LISTP))
 (884 34 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (715 661 (:REWRITE DEFAULT-CDR))
 (633 510 (:REWRITE DEFAULT-CAR))
 (511 4 (:REWRITE SUBSETP-OF-REMOVE1))
 (450 450 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (420 15 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (383 154 (:REWRITE SUBSETP-MEMBER . 4))
 (380 380 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (380 190 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (380 190 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (304 231 (:REWRITE SUBSETP-MEMBER . 2))
 (286 3 (:REWRITE MEMBER-OF-CONS))
 (271 157 (:REWRITE MEMBER-WHEN-ATOM))
 (231 231 (:REWRITE SUBSETP-MEMBER . 1))
 (220 179 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (210 15 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (190 190 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (190 190 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (190 190 (:REWRITE SET::IN-SET))
 (189 189 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (164 164 (:REWRITE SUBSETP-TRANS2))
 (164 164 (:REWRITE SUBSETP-TRANS))
 (159 159 (:REWRITE INTERSECTP-MEMBER . 3))
 (159 159 (:REWRITE INTERSECTP-MEMBER . 2))
 (156 155 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (154 154 (:REWRITE SUBSETP-MEMBER . 3))
 (135 1 (:REWRITE SUBSETP-CONS-2))
 (129 3 (:REWRITE MEMBER-OF-REMOVE))
 (128 20 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (121 121 (:REWRITE CONSP-OF-TRUE-LIST-LIST-FIX))
 (75 15 (:DEFINITION LEN))
 (46 46 (:REWRITE INTERSECTP-MEMBER . 1))
 (46 46 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (43 43 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (41 41 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (31 31 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (31 31 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (30 30 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (30 30 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (30 30 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (30 30 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (30 15 (:REWRITE DEFAULT-+-2))
 (26 26 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (23 1 (:REWRITE EQUAL-OF-LIST-FIX-AND-SELF))
 (15 15 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (15 15 (:REWRITE DEFAULT-+-1))
 (15 15 (:LINEAR POSITION-WHEN-MEMBER))
 (15 15 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (7 7 (:REWRITE CONSP-OF-LIST-FIX))
 (6 2 (:REWRITE CDR-OF-LIST-FIX))
 (4 2 (:REWRITE CAR-OF-LIST-FIX))
 )
(FLATTEN-EQUIV-IMPLIES-EQUAL-NOT-INTERSECTP-LIST-2
 (97 3 (:REWRITE REMOVE-WHEN-ABSENT))
 (57 3 (:DEFINITION MEMBER-EQUAL))
 (55 1 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (51 1 (:DEFINITION TRUE-LIST-LISTP))
 (22 1 (:DEFINITION TRUE-LISTP))
 (18 2 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (16 2 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (15 15 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (14 8 (:REWRITE DEFAULT-CAR))
 (12 9 (:REWRITE DEFAULT-CDR))
 (12 6 (:REWRITE MEMBER-WHEN-ATOM))
 (12 2 (:DEFINITION STRING-LISTP))
 (10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
 (7 7 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (7 6 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (6 6 (:REWRITE SUBSETP-MEMBER . 4))
 (6 6 (:REWRITE SUBSETP-MEMBER . 3))
 (6 6 (:REWRITE SUBSETP-MEMBER . 2))
 (6 6 (:REWRITE SUBSETP-MEMBER . 1))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 3))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 2))
 (4 4 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (4 4 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (4 2 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (4 2 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (2 2 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (2 2 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (2 2 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (2 2 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (2 2 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (2 2 (:REWRITE SET::IN-SET))
 (2 1 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (2 1 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (1 1 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (1 1 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 )
(FLATTEN-EQUIV-IMPLIES-EQUAL-MEMBER-INTERSECTP-EQUAL-1-LEMMA-1
 (2936 24 (:DEFINITION INTERSECTP-EQUAL))
 (2931 50 (:DEFINITION TRUE-LIST-LISTP))
 (2123 13 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (2087 87 (:DEFINITION MEMBER-EQUAL))
 (1914 87 (:DEFINITION TRUE-LISTP))
 (1648 87 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (1509 15 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (1487 126 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1382 174 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1313 39 (:REWRITE REMOVE-WHEN-ABSENT))
 (1248 48 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (1231 174 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1186 76 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (906 151 (:DEFINITION STRING-LISTP))
 (840 120 (:REWRITE SUBSETP-CAR-MEMBER))
 (755 755 (:TYPE-PRESCRIPTION STRING-LISTP))
 (635 598 (:REWRITE DEFAULT-CDR))
 (550 52 (:REWRITE INTERSECTP-WHEN-SUBSETP))
 (548 460 (:REWRITE DEFAULT-CAR))
 (411 411 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (374 374 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (364 13 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (302 302 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (302 151 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (302 151 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (257 257 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (222 126 (:REWRITE MEMBER-WHEN-ATOM))
 (210 198 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (207 198 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (198 198 (:REWRITE SUBSETP-TRANS2))
 (198 198 (:REWRITE SUBSETP-TRANS))
 (198 198 (:REWRITE SUBSETP-MEMBER . 2))
 (198 198 (:REWRITE SUBSETP-MEMBER . 1))
 (182 13 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (168 24 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (151 151 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (151 151 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (151 151 (:REWRITE SET::IN-SET))
 (128 128 (:REWRITE INTERSECTP-MEMBER . 3))
 (128 128 (:REWRITE INTERSECTP-MEMBER . 2))
 (126 126 (:REWRITE SUBSETP-MEMBER . 4))
 (126 126 (:REWRITE SUBSETP-MEMBER . 3))
 (110 109 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (106 34 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (98 98 (:TYPE-PRESCRIPTION REMOVE-EQUAL))
 (84 84 (:REWRITE CONSP-OF-TRUE-LIST-LIST-FIX))
 (82 2 (:REWRITE MEMBER-OF-CONS))
 (65 13 (:DEFINITION LEN))
 (64 49 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (52 52 (:REWRITE INTERSECTP-MEMBER . 1))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 12))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 11))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 10))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 9))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 8))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 7))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 6))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 5))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 4))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 3))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 2))
 (52 52 (:REWRITE INTERSECT-WITH-SUBSET . 1))
 (52 52 (:REWRITE FLATTEN-SUBSET-NO-DUPLICATESP-LEMMA-1))
 (49 49 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (49 49 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (49 49 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (49 49 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (38 38 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (34 34 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (26 13 (:REWRITE DEFAULT-+-2))
 (17 17 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (17 17 (:REWRITE CONSP-OF-LIST-FIX))
 (13 13 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (13 13 (:REWRITE DEFAULT-+-1))
 (13 13 (:LINEAR POSITION-WHEN-MEMBER))
 (13 13 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (12 4 (:REWRITE CDR-OF-LIST-FIX))
 (8 4 (:REWRITE CAR-OF-LIST-FIX))
 )
(SET-EQUIV-IMPLIES-EQUAL-MEMBER-INTERSECTP-EQUAL-1
 (10 10 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (5 5 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (5 5 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (5 5 (:REWRITE DEFAULT-CDR))
 (5 5 (:REWRITE DEFAULT-CAR))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (3 3 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (3 3 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(SET-EQUIV-IMPLIES-EQUAL-MEMBER-INTERSECTP-EQUAL-2
 (18 18 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (9 9 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (9 9 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (9 9 (:REWRITE DEFAULT-CDR))
 (9 9 (:REWRITE DEFAULT-CAR))
 (7 7 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (7 7 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (7 7 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (4 4 (:REWRITE SUBSETP-TRANS))
 )
(FLATTEN-EQUIV-IMPLIES-EQUAL-MEMBER-INTERSECTP-EQUAL-1
 (194 6 (:REWRITE REMOVE-WHEN-ABSENT))
 (114 6 (:DEFINITION MEMBER-EQUAL))
 (110 2 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (102 2 (:DEFINITION TRUE-LIST-LISTP))
 (44 2 (:DEFINITION TRUE-LISTP))
 (36 4 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (32 20 (:REWRITE DEFAULT-CAR))
 (32 4 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (30 30 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (28 22 (:REWRITE DEFAULT-CDR))
 (24 12 (:REWRITE MEMBER-WHEN-ATOM))
 (24 4 (:DEFINITION STRING-LISTP))
 (20 20 (:TYPE-PRESCRIPTION STRING-LISTP))
 (20 8 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (14 14 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (14 12 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (12 12 (:TYPE-PRESCRIPTION REMOVE-EQUAL))
 (12 12 (:REWRITE SUBSETP-MEMBER . 4))
 (12 12 (:REWRITE SUBSETP-MEMBER . 3))
 (12 12 (:REWRITE SUBSETP-MEMBER . 2))
 (12 12 (:REWRITE SUBSETP-MEMBER . 1))
 (12 12 (:REWRITE INTERSECTP-MEMBER . 3))
 (12 12 (:REWRITE INTERSECTP-MEMBER . 2))
 (10 10 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (8 8 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (8 8 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (8 8 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (8 4 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (8 4 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (4 4 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (4 4 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (4 4 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (4 4 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (4 4 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (4 4 (:REWRITE SET::IN-SET))
 (4 2 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (4 2 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (2 2 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (2 2 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 )
(FLATTEN-EQUIV-IMPLIES-EQUAL-MEMBER-INTERSECTP-EQUAL-2
 (387 12 (:REWRITE REMOVE-WHEN-ABSENT))
 (228 12 (:DEFINITION MEMBER-EQUAL))
 (220 4 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (204 4 (:DEFINITION TRUE-LIST-LISTP))
 (88 4 (:DEFINITION TRUE-LISTP))
 (72 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (64 8 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (62 38 (:REWRITE DEFAULT-CAR))
 (60 60 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (54 42 (:REWRITE DEFAULT-CDR))
 (48 24 (:REWRITE MEMBER-WHEN-ATOM))
 (48 8 (:DEFINITION STRING-LISTP))
 (40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
 (28 28 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (27 24 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (24 24 (:REWRITE SUBSETP-MEMBER . 4))
 (24 24 (:REWRITE SUBSETP-MEMBER . 3))
 (24 24 (:REWRITE SUBSETP-MEMBER . 2))
 (24 24 (:REWRITE SUBSETP-MEMBER . 1))
 (24 24 (:REWRITE INTERSECTP-MEMBER . 3))
 (24 24 (:REWRITE INTERSECTP-MEMBER . 2))
 (24 12 (:REWRITE MEMBER-INTERSECTP-IS-COMMUTATIVE-LEMMA-2))
 (16 16 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (16 16 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (16 16 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-3))
 (16 8 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (16 8 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (12 12 (:TYPE-PRESCRIPTION REMOVE-EQUAL))
 (12 12 (:REWRITE MEMBER-INTERSECTP-WITH-SUBSET))
 (8 8 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (8 8 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (8 8 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (8 8 (:REWRITE SET::IN-SET))
 (8 4 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (8 4 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-2))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-WHEN-SUBSETP-1))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-WHEN-ATOM))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 2))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-2 . 1))
 (6 6 (:REWRITE NOT-INTERSECTP-LIST-OF-SET-DIFFERENCE$-LEMMA-1))
 (6 6 (:REWRITE INTERSECTP-MEMBER-WHEN-NOT-MEMBER-INTERSECTP))
 (4 4 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (3 3 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 )
(SET-EQUIV-IMPLIES-EQUAL-TRUE-LIST-LISTP-OF-LIST-FIX-1-LEMMA-1
 (1868 43 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (1739 43 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (968 115 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (843 115 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (648 107 (:DEFINITION STRING-LISTP))
 (526 526 (:TYPE-PRESCRIPTION STRING-LISTP))
 (505 215 (:REWRITE SUBSETP-MEMBER . 2))
 (433 433 (:REWRITE DEFAULT-CDR))
 (401 76 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (359 359 (:REWRITE DEFAULT-CAR))
 (259 175 (:REWRITE SUBSETP-TRANS2))
 (221 215 (:REWRITE SUBSETP-MEMBER . 1))
 (217 175 (:REWRITE SUBSETP-TRANS))
 (215 215 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (208 208 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (208 104 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (208 104 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (175 175 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (175 175 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (140 34 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (104 104 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (104 104 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (104 104 (:REWRITE SET::IN-SET))
 (71 43 (:REWRITE SUBSETP-MEMBER . 3))
 (43 43 (:REWRITE SUBSETP-MEMBER . 4))
 (43 43 (:REWRITE MEMBER-WHEN-ATOM))
 (43 43 (:REWRITE INTERSECTP-MEMBER . 3))
 (43 43 (:REWRITE INTERSECTP-MEMBER . 2))
 (34 34 (:REWRITE SUBSETP-REFL))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (18 18 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(SET-EQUIV-IMPLIES-EQUAL-TRUE-LIST-LISTP-OF-LIST-FIX-1
 (546 5 (:DEFINITION TRUE-LIST-LISTP))
 (321 15 (:DEFINITION TRUE-LISTP))
 (258 3 (:REWRITE CDR-OF-LIST-FIX))
 (230 30 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (210 5 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (205 30 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (150 25 (:DEFINITION STRING-LISTP))
 (141 6 (:REWRITE TRUE-LIST-LISTP-OF-LIST-FIX))
 (135 5 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (125 125 (:TYPE-PRESCRIPTION STRING-LISTP))
 (70 5 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (58 58 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (50 50 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (50 50 (:REWRITE DEFAULT-CDR))
 (50 25 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (50 25 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (34 19 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (30 30 (:REWRITE DEFAULT-CAR))
 (25 25 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (25 25 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (25 25 (:REWRITE SET::IN-SET))
 (25 5 (:DEFINITION LEN))
 (19 5 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (19 5 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (10 5 (:REWRITE DEFAULT-+-2))
 (8 8 (:REWRITE CONSP-OF-LIST-FIX))
 (6 3 (:REWRITE CAR-OF-LIST-FIX))
 (5 5 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (1 1 (:REWRITE SUBSETP-WHEN-ATOM-LEFT))
 (1 1 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (1 1 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (1 1 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (1 1 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 )
(COMMUTATIVITY-2-OF-CONS-UNDER-FLATTEN-EQUIV-LEMMA-1
 (6 6 (:REWRITE INTERSECTP-MEMBER . 3))
 (6 6 (:REWRITE INTERSECTP-MEMBER . 2))
 )
(COMMUTATIVITY-2-OF-CONS-UNDER-FLATTEN-EQUIV
 (1500 42 (:REWRITE REMOVE-WHEN-ABSENT))
 (864 41 (:DEFINITION MEMBER-EQUAL))
 (814 37 (:DEFINITION TRUE-LISTP))
 (716 14 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (663 13 (:DEFINITION TRUE-LIST-LISTP))
 (570 74 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (508 74 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (506 14 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (375 10 (:REWRITE MEMBER-OF-CONS))
 (372 62 (:DEFINITION STRING-LISTP))
 (326 14 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (310 310 (:TYPE-PRESCRIPTION STRING-LISTP))
 (255 144 (:REWRITE DEFAULT-CAR))
 (229 193 (:REWRITE DEFAULT-CDR))
 (205 205 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (181 82 (:REWRITE MEMBER-WHEN-ATOM))
 (172 172 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (170 14 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (124 124 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (124 62 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (124 62 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (107 82 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (99 99 (:REWRITE CONSP-OF-TRUE-LIST-LIST-FIX))
 (92 92 (:REWRITE INTERSECTP-MEMBER . 3))
 (92 92 (:REWRITE INTERSECTP-MEMBER . 2))
 (91 91 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (82 82 (:REWRITE SUBSETP-MEMBER . 4))
 (82 82 (:REWRITE SUBSETP-MEMBER . 3))
 (82 82 (:REWRITE SUBSETP-MEMBER . 2))
 (82 82 (:REWRITE SUBSETP-MEMBER . 1))
 (62 62 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (62 62 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (62 62 (:REWRITE SET::IN-SET))
 (60 12 (:DEFINITION LEN))
 (26 26 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (26 13 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (26 13 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (25 25 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (25 25 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (24 12 (:REWRITE DEFAULT-+-2))
 (14 14 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (12 12 (:REWRITE DEFAULT-+-1))
 (12 12 (:LINEAR POSITION-WHEN-MEMBER))
 (12 12 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(FLATTEN-EQUIV-IMPLIES-FLATTEN-EQUIV-APPEND-2
 (541 18 (:REWRITE REMOVE-WHEN-ABSENT))
 (318 17 (:DEFINITION MEMBER-EQUAL))
 (276 6 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (255 5 (:DEFINITION TRUE-LIST-LISTP))
 (110 5 (:DEFINITION TRUE-LISTP))
 (90 10 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (87 48 (:REWRITE DEFAULT-CAR))
 (85 85 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (80 10 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (77 53 (:REWRITE DEFAULT-CDR))
 (67 34 (:REWRITE MEMBER-WHEN-ATOM))
 (60 10 (:DEFINITION STRING-LISTP))
 (58 4 (:DEFINITION BINARY-APPEND))
 (50 50 (:TYPE-PRESCRIPTION STRING-LISTP))
 (36 34 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (35 35 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (34 34 (:REWRITE SUBSETP-MEMBER . 4))
 (34 34 (:REWRITE SUBSETP-MEMBER . 3))
 (34 34 (:REWRITE SUBSETP-MEMBER . 2))
 (34 34 (:REWRITE SUBSETP-MEMBER . 1))
 (34 34 (:REWRITE INTERSECTP-MEMBER . 3))
 (34 34 (:REWRITE INTERSECTP-MEMBER . 2))
 (29 8 (:REWRITE APPEND-ATOM-UNDER-LIST-EQUIV))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (20 20 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (20 10 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (20 10 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (20 8 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (16 16 (:TYPE-PRESCRIPTION REMOVE-EQUAL))
 (10 10 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (10 10 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (10 10 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (10 10 (:REWRITE SET::IN-SET))
 (10 5 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (10 5 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (5 5 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (2 2 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 )
(FLATTEN-EQUIV-OF-REMOVE-OF-NIL
 (5633 110 (:DEFINITION TRUE-LIST-LISTP))
 (5458 57 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (3698 200 (:DEFINITION MEMBER-EQUAL))
 (2628 118 (:DEFINITION TRUE-LISTP))
 (2020 236 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (1861 236 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1563 152 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (1338 223 (:DEFINITION STRING-LISTP))
 (1115 1115 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1075 16 (:REWRITE TRUE-LIST-LISTP-OF-REMOVE))
 (1034 698 (:REWRITE DEFAULT-CAR))
 (985 826 (:REWRITE DEFAULT-CDR))
 (830 116 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (821 8 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (482 482 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (446 446 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (446 223 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (446 223 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (436 399 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (406 406 (:REWRITE INTERSECTP-MEMBER . 3))
 (406 406 (:REWRITE INTERSECTP-MEMBER . 2))
 (399 399 (:REWRITE SUBSETP-MEMBER . 4))
 (399 399 (:REWRITE SUBSETP-MEMBER . 3))
 (399 399 (:REWRITE SUBSETP-MEMBER . 2))
 (399 399 (:REWRITE SUBSETP-MEMBER . 1))
 (269 220 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (223 223 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (223 223 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (223 223 (:REWRITE SET::IN-SET))
 (141 7 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (90 4 (:REWRITE MEMBER-OF-CONS))
 (59 59 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (37 37 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (12 12 (:REWRITE-QUOTED-CONSTANT TRUE-LIST-LIST-FIX-UNDER-TRUE-LIST-LIST-EQUIV))
 (10 5 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (5 5 (:REWRITE DEFAULT-+-1))
 (5 5 (:LINEAR POSITION-WHEN-MEMBER))
 (5 5 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(FLATTEN-EQUIV-OF-CONS-WHEN-ATOM
 (239 8 (:REWRITE REMOVE-WHEN-ABSENT))
 (138 7 (:DEFINITION MEMBER-EQUAL))
 (57 3 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (51 1 (:DEFINITION TRUE-LIST-LISTP))
 (36 36 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (31 15 (:REWRITE DEFAULT-CAR))
 (29 14 (:REWRITE MEMBER-WHEN-ATOM))
 (24 3 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (23 16 (:REWRITE DEFAULT-CDR))
 (23 2 (:DEFINITION TRUE-LISTP))
 (21 3 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (17 14 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (15 15 (:REWRITE INTERSECTP-MEMBER . 3))
 (15 15 (:REWRITE INTERSECTP-MEMBER . 2))
 (15 15 (:REWRITE CONSP-OF-TRUE-LIST-LIST-FIX))
 (14 14 (:REWRITE SUBSETP-MEMBER . 4))
 (14 14 (:REWRITE SUBSETP-MEMBER . 3))
 (14 14 (:REWRITE SUBSETP-MEMBER . 2))
 (14 14 (:REWRITE SUBSETP-MEMBER . 1))
 (14 1 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (13 3 (:DEFINITION STRING-LISTP))
 (11 11 (:TYPE-PRESCRIPTION STRING-LISTP))
 (7 7 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (6 6 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (6 3 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (6 3 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (3 3 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (3 3 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (3 3 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (3 3 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (3 3 (:REWRITE SET::IN-SET))
 (2 2 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (2 1 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (2 1 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (2 1 (:REWRITE MEMBER-OF-CONS))
 )
(FLATTEN-EQUIV-IMPLIES-FLATTEN-EQUIV-CONS-2
 (827 24 (:REWRITE REMOVE-WHEN-ABSENT))
 (486 24 (:DEFINITION MEMBER-EQUAL))
 (440 8 (:REWRITE TRUE-LIST-LIST-FIX-WHEN-TRUE-LIST-LISTP))
 (408 8 (:DEFINITION TRUE-LIST-LISTP))
 (308 14 (:DEFINITION TRUE-LISTP))
 (228 28 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (203 28 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (150 25 (:DEFINITION STRING-LISTP))
 (131 73 (:REWRITE DEFAULT-CAR))
 (127 4 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (125 125 (:TYPE-PRESCRIPTION STRING-LISTP))
 (120 120 (:TYPE-PRESCRIPTION MEMBER-EQUAL))
 (112 90 (:REWRITE DEFAULT-CDR))
 (102 48 (:REWRITE MEMBER-WHEN-ATOM))
 (82 4 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (82 2 (:REWRITE MEMBER-OF-CONS))
 (62 62 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (59 48 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (56 56 (:TYPE-PRESCRIPTION TRUE-LIST-LISTP))
 (54 54 (:REWRITE CONSP-OF-TRUE-LIST-LIST-FIX))
 (50 50 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (50 50 (:REWRITE INTERSECTP-MEMBER . 3))
 (50 50 (:REWRITE INTERSECTP-MEMBER . 2))
 (50 25 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (50 25 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (48 48 (:REWRITE SUBSETP-MEMBER . 4))
 (48 48 (:REWRITE SUBSETP-MEMBER . 3))
 (48 48 (:REWRITE SUBSETP-MEMBER . 2))
 (48 48 (:REWRITE SUBSETP-MEMBER . 1))
 (43 4 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (25 25 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (25 25 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (25 25 (:REWRITE SET::IN-SET))
 (16 16 (:REWRITE TRUE-LIST-LISTP-WHEN-NOT-CONSP))
 (16 8 (:REWRITE TRUE-LISTP-OF-CAR-WHEN-TRUE-LIST-LISTP))
 (16 8 (:REWRITE TRUE-LIST-LISTP-OF-CDR-WHEN-TRUE-LIST-LISTP))
 (15 3 (:DEFINITION LEN))
 (12 12 (:REWRITE TRUE-LIST-LIST-FIX-UNDER-IFF))
 (11 11 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (6 3 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (3 3 (:REWRITE DEFAULT-+-1))
 (3 3 (:LINEAR POSITION-WHEN-MEMBER))
 (3 3 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(CONS-EQUAL-UNDER-SET-EQUIV-1
 (8177 275 (:DEFINITION MEMBER-EQUAL))
 (7431 306 (:REWRITE NO-DUPLICATESP-OF-MEMBER))
 (6597 261 (:DEFINITION NO-DUPLICATESP-EQUAL))
 (3132 450 (:REWRITE SUBSETP-CAR-MEMBER))
 (2064 298 (:REWRITE SUBSETP-MEMBER . 3))
 (1358 198 (:REWRITE SUBSETP-IMPLIES-SUBSETP-CDR))
 (1311 1311 (:TYPE-PRESCRIPTION NO-DUPLICATESP-EQUAL))
 (887 887 (:REWRITE DEFAULT-CDR))
 (862 854 (:REWRITE SUBSETP-WHEN-ATOM-RIGHT))
 (848 848 (:REWRITE SUBSETP-TRANS))
 (786 696 (:REWRITE SUBSETP-MEMBER . 2))
 (644 644 (:REWRITE DEFAULT-CAR))
 (518 298 (:REWRITE SUBSETP-MEMBER . 4))
 (314 314 (:REWRITE INTERSECTP-MEMBER . 3))
 (314 314 (:REWRITE INTERSECTP-MEMBER . 2))
 (44 44 (:REWRITE INTERSECT-WITH-SUBSET . 16))
 (44 44 (:REWRITE INTERSECT-WITH-SUBSET . 15))
 (44 44 (:REWRITE INTERSECT-WITH-SUBSET . 14))
 (44 44 (:REWRITE INTERSECT-WITH-SUBSET . 13))
 (4 2 (:REWRITE SUBSETP-CONS-SAME))
 )
(FLATTEN-EQUIV-OF-APPEND-OF-CONS-1)