1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
(MEM)
(NOTMEM)
(SUBSET)
(DEL)
(APP)
(SET-DIFF)
(SET-EQUAL)
(SUBSET-CONS
(43 43 (:REWRITE DEFAULT-CAR))
(22 22 (:REWRITE DEFAULT-CDR))
)
(SUBSET-REFLEXIVE
(22 22 (:REWRITE DEFAULT-CAR))
(19 19 (:REWRITE DEFAULT-CDR))
)
(MEM-SUBSET
(28 28 (:REWRITE DEFAULT-CAR))
(16 16 (:REWRITE DEFAULT-CDR))
)
(SUBSET-TRANSITIVE
(70 16 (:DEFINITION MEM))
(36 36 (:REWRITE DEFAULT-CAR))
(25 25 (:REWRITE DEFAULT-CDR))
)
(SET-EQUAL-TRANSITIVE
(74 6 (:DEFINITION SUBSET))
(30 6 (:DEFINITION MEM))
(14 14 (:TYPE-PRESCRIPTION MEM))
(12 12 (:REWRITE MEM-SUBSET))
(12 12 (:REWRITE DEFAULT-CDR))
(12 12 (:REWRITE DEFAULT-CAR))
)
(SET-EQUAL-IS-AN-EQUIVALENCE
(94 8 (:DEFINITION SUBSET))
(38 8 (:DEFINITION MEM))
(16 16 (:TYPE-PRESCRIPTION MEM))
(16 16 (:REWRITE MEM-SUBSET))
(16 16 (:REWRITE DEFAULT-CDR))
(16 16 (:REWRITE DEFAULT-CAR))
(2 2 (:REWRITE SET-EQUAL-TRANSITIVE))
)
(SET-EQUAL-IMPLIES-EQUAL-MEM-2
(60 60 (:REWRITE DEFAULT-CAR))
(45 45 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE SUBSET-REFLEXIVE))
)
(SET-EQUAL-CONS
(22 22 (:TYPE-PRESCRIPTION MEM))
(14 14 (:REWRITE MEM-SUBSET))
(14 14 (:REWRITE DEFAULT-CAR))
(12 12 (:REWRITE DEFAULT-CDR))
(1 1 (:REWRITE SET-EQUAL-TRANSITIVE))
)
(SET-EQUAL-MEM-CONS-2
(5 5 (:REWRITE SUBSET-TRANSITIVE))
(4 1 (:DEFINITION MEM))
(2 2 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE SET-EQUAL-TRANSITIVE))
(1 1 (:REWRITE SET-EQUAL-CONS))
)
(SET-DIFF-CONG-INDUCT)
(SET-EQUAL-CONS-F
(30 30 (:TYPE-PRESCRIPTION MEM))
(22 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
(14 14 (:REWRITE MEM-SUBSET))
(12 12 (:REWRITE DEFAULT-CAR))
(10 10 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE SET-EQUAL-CONS))
(1 1 (:REWRITE SET-EQUAL-TRANSITIVE))
)
(SET-EQUAL-IMPLIES-EQUAL-SET-DIFF-2
(103 101 (:REWRITE DEFAULT-CAR))
(75 73 (:REWRITE DEFAULT-CDR))
(11 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
(2 2 (:REWRITE SUBSET-TRANSITIVE))
)
(SUBSET-SET-DIFF-INDUCT)
(SUBSET-SET-DIFF
(210 207 (:REWRITE DEFAULT-CAR))
(165 163 (:REWRITE DEFAULT-CDR))
(31 31 (:REWRITE SET-EQUAL-CONS))
)
(NODUP-SET)
(MEM-SET-DIFF
(556 30 (:DEFINITION SUBSET))
(94 91 (:REWRITE DEFAULT-CAR))
(74 72 (:REWRITE DEFAULT-CDR))
(64 64 (:REWRITE SUBSET-TRANSITIVE))
(48 6 (:REWRITE SET-EQUAL-MEM-CONS-2))
(6 6 (:REWRITE SET-EQUAL-CONS))
)
(SET-DIFF-IS-A-NODUP-SET
(29 28 (:REWRITE DEFAULT-CAR))
(28 26 (:REWRITE DEFAULT-CDR))
(2 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
(2 2 (:REWRITE SET-EQUAL-CONS))
(1 1 (:REWRITE SUBSET-TRANSITIVE))
)
(SUBSET-NODUP-SET-SIZE-INDUCT)
(DEL-SET-LEN
(28 15 (:REWRITE DEFAULT-+-2))
(16 16 (:REWRITE DEFAULT-CAR))
(15 15 (:REWRITE DEFAULT-+-1))
(14 14 (:REWRITE DEFAULT-CDR))
(8 8 (:REWRITE MEM-SUBSET))
)
(MEM-DEL
(77 7 (:REWRITE SET-EQUAL-MEM-CONS-2))
(42 42 (:REWRITE DEFAULT-CAR))
(41 41 (:REWRITE MEM-SUBSET))
(32 32 (:REWRITE DEFAULT-CDR))
(7 7 (:REWRITE SET-EQUAL-CONS))
)
(DEL-NODUPS
(34 34 (:REWRITE DEFAULT-CDR))
(32 32 (:REWRITE DEFAULT-CAR))
(22 22 (:REWRITE MEM-SUBSET))
)
(DEL-NODUP-SET-SUBSET
(171 96 (:REWRITE SUBSET-TRANSITIVE))
(153 153 (:REWRITE DEFAULT-CAR))
(138 12 (:DEFINITION DEL))
(136 136 (:REWRITE DEFAULT-CDR))
(72 6 (:REWRITE SET-EQUAL-MEM-CONS-2))
(6 6 (:REWRITE SET-EQUAL-CONS))
)
(SUBSET-NODUP-SET-SIZE
(114 114 (:REWRITE DEFAULT-CDR))
(87 87 (:REWRITE DEFAULT-CAR))
(30 6 (:DEFINITION DEL))
(26 13 (:REWRITE DEFAULT-+-2))
(13 13 (:REWRITE DEFAULT-+-1))
(8 4 (:REWRITE DEFAULT-<-1))
(7 4 (:REWRITE DEFAULT-<-2))
(1 1 (:REWRITE MEM-DEL))
)
(LEN-SET-EQUAL-NODUP-SET-X-INDUCT)
(LEN-SET-EQUAL-NODUP-SET-X
(244 244 (:REWRITE DEFAULT-CDR))
(197 197 (:REWRITE DEFAULT-CAR))
(106 16 (:DEFINITION DEL))
(77 39 (:REWRITE DEFAULT-+-2))
(39 39 (:REWRITE DEFAULT-+-1))
(24 2 (:REWRITE SET-EQUAL-MEM-CONS-2))
(9 5 (:REWRITE DEFAULT-<-2))
(9 5 (:REWRITE DEFAULT-<-1))
(2 2 (:REWRITE SET-EQUAL-CONS))
(1 1 (:REWRITE CDR-CONS))
(1 1 (:REWRITE CAR-CONS))
)
(MEM-SET-DIFF-X
(1046 55 (:DEFINITION SUBSET))
(217 211 (:REWRITE DEFAULT-CAR))
(156 154 (:REWRITE DEFAULT-CDR))
(114 114 (:REWRITE SUBSET-TRANSITIVE))
(17 17 (:REWRITE SET-EQUAL-CONS))
)
(LEN-SET-DIFF-MEM
(238 8 (:DEFINITION SET-DIFF))
(103 52 (:REWRITE MEM-SUBSET))
(100 14 (:REWRITE SET-EQUAL-MEM-CONS-2))
(65 65 (:REWRITE DEFAULT-CAR))
(50 2 (:DEFINITION SUBSET))
(49 49 (:REWRITE DEFAULT-CDR))
(24 2 (:DEFINITION NODUP-SET))
(16 16 (:TYPE-PRESCRIPTION SET-DIFF))
(14 14 (:REWRITE SET-EQUAL-CONS))
(14 2 (:DEFINITION LEN))
(9 9 (:REWRITE CDR-CONS))
(7 7 (:REWRITE SUBSET-TRANSITIVE))
(4 2 (:REWRITE DEFAULT-+-2))
(2 2 (:REWRITE DEL-SET-LEN))
(2 2 (:REWRITE DEFAULT-+-1))
(2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
(2 1 (:REWRITE DEFAULT-<-2))
(2 1 (:REWRITE DEFAULT-<-1))
(1 1 (:REWRITE LEN-SET-EQUAL-NODUP-SET-X))
)
|
