|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"count" > "count_primdef"
|
|
|
7 |
"UNIV" > "UNIV_def"
|
|
|
8 |
"UNION" > "UNION_def"
|
|
|
9 |
"SURJ" > "SURJ_def"
|
|
|
10 |
"SUBSET" > "SUBSET_def"
|
|
|
11 |
"SING" > "SING_def"
|
|
|
12 |
"RINV" > "RINV_def"
|
|
|
13 |
"REST" > "REST_def"
|
|
|
14 |
"PSUBSET" > "PSUBSET_def"
|
|
|
15 |
"LINV" > "LINV_def"
|
|
|
16 |
"ITSET_tupled" > "ITSET_tupled_def"
|
|
|
17 |
"ITSET" > "ITSET_def"
|
|
|
18 |
"INTER" > "INTER_def"
|
|
|
19 |
"INSERT" > "INSERT_def"
|
|
|
20 |
"INJ" > "INJ_def"
|
|
|
21 |
"INFINITE" > "INFINITE_def"
|
|
|
22 |
"IMAGE" > "IMAGE_def"
|
|
|
23 |
"GSPEC" > "GSPEC_def"
|
|
|
24 |
"FINITE" > "FINITE_def"
|
|
|
25 |
"EMPTY" > "EMPTY_def"
|
|
|
26 |
"DISJOINT" > "DISJOINT_def"
|
|
|
27 |
"DIFF" > "DIFF_def"
|
|
|
28 |
"DELETE" > "DELETE_def"
|
|
|
29 |
"CROSS" > "CROSS_def"
|
|
|
30 |
"COMPL" > "COMPL_def"
|
|
|
31 |
"CHOICE" > "CHOICE_def"
|
|
|
32 |
"CARD" > "CARD_def"
|
|
|
33 |
"BIJ" > "BIJ_def"
|
|
|
34 |
"BIGUNION" > "BIGUNION_def"
|
|
|
35 |
"BIGINTER" > "BIGINTER_def"
|
|
|
36 |
|
|
|
37 |
const_maps
|
|
|
38 |
"count" > "HOL4Base.pred_set.count"
|
|
|
39 |
"UNIV" > "HOL4Base.pred_set.UNIV"
|
|
|
40 |
"UNION" > "HOL4Base.pred_set.UNION"
|
|
|
41 |
"SURJ" > "HOL4Base.pred_set.SURJ"
|
|
|
42 |
"SUBSET" > "HOL4Base.pred_set.SUBSET"
|
|
|
43 |
"SING" > "HOL4Base.pred_set.SING"
|
|
|
44 |
"REST" > "HOL4Base.pred_set.REST"
|
|
|
45 |
"PSUBSET" > "HOL4Base.pred_set.PSUBSET"
|
|
|
46 |
"ITSET_tupled" > "HOL4Base.pred_set.ITSET_tupled"
|
|
|
47 |
"ITSET" > "HOL4Base.pred_set.ITSET"
|
|
|
48 |
"INTER" > "HOL4Base.pred_set.INTER"
|
|
|
49 |
"INSERT" > "HOL4Base.pred_set.INSERT"
|
|
|
50 |
"INJ" > "HOL4Base.pred_set.INJ"
|
|
|
51 |
"INFINITE" > "HOL4Base.pred_set.INFINITE"
|
|
|
52 |
"IMAGE" > "HOL4Base.pred_set.IMAGE"
|
|
|
53 |
"FINITE" > "HOL4Base.pred_set.FINITE"
|
|
|
54 |
"EMPTY" > "HOL4Base.pred_set.EMPTY"
|
|
|
55 |
"DISJOINT" > "HOL4Base.pred_set.DISJOINT"
|
|
|
56 |
"DIFF" > "HOL4Base.pred_set.DIFF"
|
|
|
57 |
"DELETE" > "HOL4Base.pred_set.DELETE"
|
|
|
58 |
"CROSS" > "HOL4Base.pred_set.CROSS"
|
|
|
59 |
"COMPL" > "HOL4Base.pred_set.COMPL"
|
|
|
60 |
"BIJ" > "HOL4Base.pred_set.BIJ"
|
|
|
61 |
"BIGUNION" > "HOL4Base.pred_set.BIGUNION"
|
|
|
62 |
"BIGINTER" > "HOL4Base.pred_set.BIGINTER"
|
|
|
63 |
|
|
|
64 |
thm_maps
|
|
|
65 |
"count_primdef" > "HOL4Base.pred_set.count_primdef"
|
|
|
66 |
"count_def" > "HOL4Base.pred_set.count_def"
|
|
|
67 |
"UNIV_def" > "HOL4Base.pred_set.UNIV_def"
|
|
|
68 |
"UNIV_SUBSET" > "HOL4Base.pred_set.UNIV_SUBSET"
|
|
|
69 |
"UNIV_NOT_EMPTY" > "HOL4Base.pred_set.UNIV_NOT_EMPTY"
|
|
|
70 |
"UNIV_DEF" > "HOL4Base.pred_set.UNIV_DEF"
|
|
|
71 |
"UNION_def" > "HOL4Base.pred_set.UNION_def"
|
|
|
72 |
"UNION_UNIV" > "HOL4Base.pred_set.UNION_UNIV"
|
|
|
73 |
"UNION_SUBSET" > "HOL4Base.pred_set.UNION_SUBSET"
|
|
|
74 |
"UNION_OVER_INTER" > "HOL4Base.pred_set.UNION_OVER_INTER"
|
|
|
75 |
"UNION_IDEMPOT" > "HOL4Base.pred_set.UNION_IDEMPOT"
|
|
|
76 |
"UNION_EMPTY" > "HOL4Base.pred_set.UNION_EMPTY"
|
|
|
77 |
"UNION_DEF" > "HOL4Base.pred_set.UNION_DEF"
|
|
|
78 |
"UNION_COMM" > "HOL4Base.pred_set.UNION_COMM"
|
|
|
79 |
"UNION_ASSOC" > "HOL4Base.pred_set.UNION_ASSOC"
|
|
|
80 |
"SURJ_def" > "HOL4Base.pred_set.SURJ_def"
|
|
|
81 |
"SURJ_ID" > "HOL4Base.pred_set.SURJ_ID"
|
|
|
82 |
"SURJ_EMPTY" > "HOL4Base.pred_set.SURJ_EMPTY"
|
|
|
83 |
"SURJ_DEF" > "HOL4Base.pred_set.SURJ_DEF"
|
|
|
84 |
"SURJ_COMPOSE" > "HOL4Base.pred_set.SURJ_COMPOSE"
|
|
|
85 |
"SUBSET_def" > "HOL4Base.pred_set.SUBSET_def"
|
|
|
86 |
"SUBSET_UNIV" > "HOL4Base.pred_set.SUBSET_UNIV"
|
|
|
87 |
"SUBSET_UNION_ABSORPTION" > "HOL4Base.pred_set.SUBSET_UNION_ABSORPTION"
|
|
|
88 |
"SUBSET_UNION" > "HOL4Base.pred_set.SUBSET_UNION"
|
|
|
89 |
"SUBSET_TRANS" > "HOL4Base.pred_set.SUBSET_TRANS"
|
|
|
90 |
"SUBSET_REFL" > "HOL4Base.pred_set.SUBSET_REFL"
|
|
|
91 |
"SUBSET_INTER_ABSORPTION" > "HOL4Base.pred_set.SUBSET_INTER_ABSORPTION"
|
|
|
92 |
"SUBSET_INTER" > "HOL4Base.pred_set.SUBSET_INTER"
|
|
|
93 |
"SUBSET_INSERT_DELETE" > "HOL4Base.pred_set.SUBSET_INSERT_DELETE"
|
|
|
94 |
"SUBSET_INSERT" > "HOL4Base.pred_set.SUBSET_INSERT"
|
|
|
95 |
"SUBSET_FINITE" > "HOL4Base.pred_set.SUBSET_FINITE"
|
|
|
96 |
"SUBSET_EMPTY" > "HOL4Base.pred_set.SUBSET_EMPTY"
|
|
|
97 |
"SUBSET_DELETE" > "HOL4Base.pred_set.SUBSET_DELETE"
|
|
|
98 |
"SUBSET_DEF" > "HOL4Base.pred_set.SUBSET_DEF"
|
|
|
99 |
"SUBSET_BIGINTER" > "HOL4Base.pred_set.SUBSET_BIGINTER"
|
|
|
100 |
"SUBSET_ANTISYM" > "HOL4Base.pred_set.SUBSET_ANTISYM"
|
|
|
101 |
"SPECIFICATION" > "HOL4Base.bool.IN_DEF"
|
|
|
102 |
"SING_def" > "HOL4Base.pred_set.SING_def"
|
|
|
103 |
"SING_IFF_EMPTY_REST" > "HOL4Base.pred_set.SING_IFF_EMPTY_REST"
|
|
|
104 |
"SING_IFF_CARD1" > "HOL4Base.pred_set.SING_IFF_CARD1"
|
|
|
105 |
"SING_FINITE" > "HOL4Base.pred_set.SING_FINITE"
|
|
|
106 |
"SING_DELETE" > "HOL4Base.pred_set.SING_DELETE"
|
|
|
107 |
"SING_DEF" > "HOL4Base.pred_set.SING_DEF"
|
|
|
108 |
"SING" > "HOL4Base.pred_set.SING"
|
|
|
109 |
"SET_MINIMUM" > "HOL4Base.pred_set.SET_MINIMUM"
|
|
|
110 |
"SET_CASES" > "HOL4Base.pred_set.SET_CASES"
|
|
|
111 |
"RINV_DEF" > "HOL4Base.pred_set.RINV_DEF"
|
|
|
112 |
"REST_def" > "HOL4Base.pred_set.REST_def"
|
|
|
113 |
"REST_SUBSET" > "HOL4Base.pred_set.REST_SUBSET"
|
|
|
114 |
"REST_SING" > "HOL4Base.pred_set.REST_SING"
|
|
|
115 |
"REST_PSUBSET" > "HOL4Base.pred_set.REST_PSUBSET"
|
|
|
116 |
"REST_DEF" > "HOL4Base.pred_set.REST_DEF"
|
|
|
117 |
"PSUBSET_def" > "HOL4Base.pred_set.PSUBSET_def"
|
|
|
118 |
"PSUBSET_UNIV" > "HOL4Base.pred_set.PSUBSET_UNIV"
|
|
|
119 |
"PSUBSET_TRANS" > "HOL4Base.pred_set.PSUBSET_TRANS"
|
|
|
120 |
"PSUBSET_MEMBER" > "HOL4Base.pred_set.PSUBSET_MEMBER"
|
|
|
121 |
"PSUBSET_IRREFL" > "HOL4Base.pred_set.PSUBSET_IRREFL"
|
|
|
122 |
"PSUBSET_INSERT_SUBSET" > "HOL4Base.pred_set.PSUBSET_INSERT_SUBSET"
|
|
|
123 |
"PSUBSET_FINITE" > "HOL4Base.pred_set.PSUBSET_FINITE"
|
|
|
124 |
"PSUBSET_DEF" > "HOL4Base.pred_set.PSUBSET_DEF"
|
|
|
125 |
"NUM_SET_WOP" > "HOL4Base.pred_set.NUM_SET_WOP"
|
|
|
126 |
"NOT_UNIV_PSUBSET" > "HOL4Base.pred_set.NOT_UNIV_PSUBSET"
|
|
|
127 |
"NOT_SING_EMPTY" > "HOL4Base.pred_set.NOT_SING_EMPTY"
|
|
|
128 |
"NOT_PSUBSET_EMPTY" > "HOL4Base.pred_set.NOT_PSUBSET_EMPTY"
|
|
|
129 |
"NOT_IN_FINITE" > "HOL4Base.pred_set.NOT_IN_FINITE"
|
|
|
130 |
"NOT_IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
|
|
|
131 |
"NOT_INSERT_EMPTY" > "HOL4Base.pred_set.NOT_INSERT_EMPTY"
|
|
|
132 |
"NOT_EQUAL_SETS" > "HOL4Base.pred_set.NOT_EQUAL_SETS"
|
|
|
133 |
"NOT_EMPTY_SING" > "HOL4Base.pred_set.NOT_EMPTY_SING"
|
|
|
134 |
"NOT_EMPTY_INSERT" > "HOL4Base.pred_set.NOT_EMPTY_INSERT"
|
|
|
135 |
"MEMBER_NOT_EMPTY" > "HOL4Base.pred_set.MEMBER_NOT_EMPTY"
|
|
|
136 |
"LINV_DEF" > "HOL4Base.pred_set.LINV_DEF"
|
|
|
137 |
"LESS_CARD_DIFF" > "HOL4Base.pred_set.LESS_CARD_DIFF"
|
|
|
138 |
"ITSET_tupled_primitive_def" > "HOL4Base.pred_set.ITSET_tupled_primitive_def"
|
|
|
139 |
"ITSET_tupled_def" > "HOL4Base.pred_set.ITSET_tupled_def"
|
|
|
140 |
"ITSET_def" > "HOL4Base.pred_set.ITSET_def"
|
|
|
141 |
"ITSET_curried_def" > "HOL4Base.pred_set.ITSET_curried_def"
|
|
|
142 |
"ITSET_THM" > "HOL4Base.pred_set.ITSET_THM"
|
|
|
143 |
"ITSET_IND" > "HOL4Base.pred_set.ITSET_IND"
|
|
|
144 |
"ITSET_EMPTY" > "HOL4Base.pred_set.ITSET_EMPTY"
|
|
|
145 |
"IN_UNIV" > "HOL4Base.pred_set.IN_UNIV"
|
|
|
146 |
"IN_UNION" > "HOL4Base.pred_set.IN_UNION"
|
|
|
147 |
"IN_SING" > "HOL4Base.pred_set.IN_SING"
|
|
|
148 |
"IN_INTER" > "HOL4Base.pred_set.IN_INTER"
|
|
|
149 |
"IN_INSERT" > "HOL4Base.pred_set.IN_INSERT"
|
|
|
150 |
"IN_INFINITE_NOT_FINITE" > "HOL4Base.pred_set.IN_INFINITE_NOT_FINITE"
|
|
|
151 |
"IN_IMAGE" > "HOL4Base.pred_set.IN_IMAGE"
|
|
|
152 |
"IN_DISJOINT" > "HOL4Base.pred_set.IN_DISJOINT"
|
|
|
153 |
"IN_DIFF" > "HOL4Base.pred_set.IN_DIFF"
|
|
|
154 |
"IN_DELETE_EQ" > "HOL4Base.pred_set.IN_DELETE_EQ"
|
|
|
155 |
"IN_DELETE" > "HOL4Base.pred_set.IN_DELETE"
|
|
|
156 |
"IN_CROSS" > "HOL4Base.pred_set.IN_CROSS"
|
|
|
157 |
"IN_COUNT" > "HOL4Base.pred_set.IN_COUNT"
|
|
|
158 |
"IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
|
|
|
159 |
"IN_BIGUNION" > "HOL4Base.pred_set.IN_BIGUNION"
|
|
|
160 |
"IN_BIGINTER" > "HOL4Base.pred_set.IN_BIGINTER"
|
|
|
161 |
"INTER_def" > "HOL4Base.pred_set.INTER_def"
|
|
|
162 |
"INTER_UNIV" > "HOL4Base.pred_set.INTER_UNIV"
|
|
|
163 |
"INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
|
|
|
164 |
"INTER_SUBSET" > "HOL4Base.pred_set.INTER_SUBSET"
|
|
|
165 |
"INTER_OVER_UNION" > "HOL4Base.pred_set.INTER_OVER_UNION"
|
|
|
166 |
"INTER_IDEMPOT" > "HOL4Base.pred_set.INTER_IDEMPOT"
|
|
|
167 |
"INTER_FINITE" > "HOL4Base.pred_set.INTER_FINITE"
|
|
|
168 |
"INTER_EMPTY" > "HOL4Base.pred_set.INTER_EMPTY"
|
|
|
169 |
"INTER_DEF" > "HOL4Base.pred_set.INTER_DEF"
|
|
|
170 |
"INTER_COMM" > "HOL4Base.pred_set.INTER_COMM"
|
|
|
171 |
"INTER_ASSOC" > "HOL4Base.pred_set.INTER_ASSOC"
|
|
|
172 |
"INSERT_def" > "HOL4Base.pred_set.INSERT_def"
|
|
|
173 |
"INSERT_UNIV" > "HOL4Base.pred_set.INSERT_UNIV"
|
|
|
174 |
"INSERT_UNION_EQ" > "HOL4Base.pred_set.INSERT_UNION_EQ"
|
|
|
175 |
"INSERT_UNION" > "HOL4Base.pred_set.INSERT_UNION"
|
|
|
176 |
"INSERT_SUBSET" > "HOL4Base.pred_set.INSERT_SUBSET"
|
|
|
177 |
"INSERT_SING_UNION" > "HOL4Base.pred_set.INSERT_SING_UNION"
|
|
|
178 |
"INSERT_INTER" > "HOL4Base.pred_set.INSERT_INTER"
|
|
|
179 |
"INSERT_INSERT" > "HOL4Base.pred_set.INSERT_INSERT"
|
|
|
180 |
"INSERT_DIFF" > "HOL4Base.pred_set.INSERT_DIFF"
|
|
|
181 |
"INSERT_DELETE" > "HOL4Base.pred_set.INSERT_DELETE"
|
|
|
182 |
"INSERT_DEF" > "HOL4Base.pred_set.INSERT_DEF"
|
|
|
183 |
"INSERT_COMM" > "HOL4Base.pred_set.INSERT_COMM"
|
|
|
184 |
"INJ_def" > "HOL4Base.pred_set.INJ_def"
|
|
|
185 |
"INJ_ID" > "HOL4Base.pred_set.INJ_ID"
|
|
|
186 |
"INJ_EMPTY" > "HOL4Base.pred_set.INJ_EMPTY"
|
|
|
187 |
"INJ_DEF" > "HOL4Base.pred_set.INJ_DEF"
|
|
|
188 |
"INJ_COMPOSE" > "HOL4Base.pred_set.INJ_COMPOSE"
|
|
|
189 |
"INFINITE_def" > "HOL4Base.pred_set.INFINITE_def"
|
|
|
190 |
"INFINITE_UNIV" > "HOL4Base.pred_set.INFINITE_UNIV"
|
|
|
191 |
"INFINITE_SUBSET" > "HOL4Base.pred_set.INFINITE_SUBSET"
|
|
|
192 |
"INFINITE_INHAB" > "HOL4Base.pred_set.INFINITE_INHAB"
|
|
|
193 |
"INFINITE_DIFF_FINITE" > "HOL4Base.pred_set.INFINITE_DIFF_FINITE"
|
|
|
194 |
"INFINITE_DEF" > "HOL4Base.pred_set.INFINITE_DEF"
|
|
|
195 |
"IMAGE_def" > "HOL4Base.pred_set.IMAGE_def"
|
|
|
196 |
"IMAGE_UNION" > "HOL4Base.pred_set.IMAGE_UNION"
|
|
|
197 |
"IMAGE_SURJ" > "HOL4Base.pred_set.IMAGE_SURJ"
|
|
|
198 |
"IMAGE_SUBSET" > "HOL4Base.pred_set.IMAGE_SUBSET"
|
|
|
199 |
"IMAGE_INTER" > "HOL4Base.pred_set.IMAGE_INTER"
|
|
|
200 |
"IMAGE_INSERT" > "HOL4Base.pred_set.IMAGE_INSERT"
|
|
|
201 |
"IMAGE_IN" > "HOL4Base.pred_set.IMAGE_IN"
|
|
|
202 |
"IMAGE_ID" > "HOL4Base.pred_set.IMAGE_ID"
|
|
|
203 |
"IMAGE_FINITE" > "HOL4Base.pred_set.IMAGE_FINITE"
|
|
|
204 |
"IMAGE_EQ_EMPTY" > "HOL4Base.pred_set.IMAGE_EQ_EMPTY"
|
|
|
205 |
"IMAGE_EMPTY" > "HOL4Base.pred_set.IMAGE_EMPTY"
|
|
|
206 |
"IMAGE_DELETE" > "HOL4Base.pred_set.IMAGE_DELETE"
|
|
|
207 |
"IMAGE_DEF" > "HOL4Base.pred_set.IMAGE_DEF"
|
|
|
208 |
"IMAGE_COMPOSE" > "HOL4Base.pred_set.IMAGE_COMPOSE"
|
|
|
209 |
"IMAGE_11_INFINITE" > "HOL4Base.pred_set.IMAGE_11_INFINITE"
|
|
|
210 |
"GSPECIFICATION" > "HOL4Base.pred_set.GSPECIFICATION"
|
|
|
211 |
"FINITE_def" > "HOL4Base.pred_set.FINITE_def"
|
|
|
212 |
"FINITE_WEAK_ENUMERATE" > "HOL4Base.pred_set.FINITE_WEAK_ENUMERATE"
|
|
|
213 |
"FINITE_UNION" > "HOL4Base.pred_set.FINITE_UNION"
|
|
|
214 |
"FINITE_SING" > "HOL4Base.pred_set.FINITE_SING"
|
|
|
215 |
"FINITE_PSUBSET_UNIV" > "HOL4Base.pred_set.FINITE_PSUBSET_UNIV"
|
|
|
216 |
"FINITE_PSUBSET_INFINITE" > "HOL4Base.pred_set.FINITE_PSUBSET_INFINITE"
|
|
|
217 |
"FINITE_ISO_NUM" > "HOL4Base.pred_set.FINITE_ISO_NUM"
|
|
|
218 |
"FINITE_INSERT" > "HOL4Base.pred_set.FINITE_INSERT"
|
|
|
219 |
"FINITE_INDUCT" > "HOL4Base.pred_set.FINITE_INDUCT"
|
|
|
220 |
"FINITE_EMPTY" > "HOL4Base.pred_set.FINITE_EMPTY"
|
|
|
221 |
"FINITE_DIFF" > "HOL4Base.pred_set.FINITE_DIFF"
|
|
|
222 |
"FINITE_DELETE" > "HOL4Base.pred_set.FINITE_DELETE"
|
|
|
223 |
"FINITE_DEF" > "HOL4Base.pred_set.FINITE_DEF"
|
|
|
224 |
"FINITE_CROSS_EQ" > "HOL4Base.pred_set.FINITE_CROSS_EQ"
|
|
|
225 |
"FINITE_CROSS" > "HOL4Base.pred_set.FINITE_CROSS"
|
|
|
226 |
"FINITE_COUNT" > "HOL4Base.pred_set.FINITE_COUNT"
|
|
|
227 |
"FINITE_COMPLETE_INDUCTION" > "HOL4Base.pred_set.FINITE_COMPLETE_INDUCTION"
|
|
|
228 |
"FINITE_BIGUNION" > "HOL4Base.pred_set.FINITE_BIGUNION"
|
|
|
229 |
"EXTENSION" > "HOL4Base.pred_set.EXTENSION"
|
|
|
230 |
"EQ_UNIV" > "HOL4Base.pred_set.EQ_UNIV"
|
|
|
231 |
"EQUAL_SING" > "HOL4Base.pred_set.EQUAL_SING"
|
|
|
232 |
"EMPTY_def" > "HOL4Base.pred_set.EMPTY_def"
|
|
|
233 |
"EMPTY_UNION" > "HOL4Base.pred_set.EMPTY_UNION"
|
|
|
234 |
"EMPTY_SUBSET" > "HOL4Base.pred_set.EMPTY_SUBSET"
|
|
|
235 |
"EMPTY_NOT_UNIV" > "HOL4Base.pred_set.EMPTY_NOT_UNIV"
|
|
|
236 |
"EMPTY_DIFF" > "HOL4Base.pred_set.EMPTY_DIFF"
|
|
|
237 |
"EMPTY_DELETE" > "HOL4Base.pred_set.EMPTY_DELETE"
|
|
|
238 |
"EMPTY_DEF" > "HOL4Base.pred_set.EMPTY_DEF"
|
|
|
239 |
"DISJOINT_def" > "HOL4Base.pred_set.DISJOINT_def"
|
|
|
240 |
"DISJOINT_UNION_BOTH" > "HOL4Base.pred_set.DISJOINT_UNION_BOTH"
|
|
|
241 |
"DISJOINT_UNION" > "HOL4Base.pred_set.DISJOINT_UNION"
|
|
|
242 |
"DISJOINT_SYM" > "HOL4Base.pred_set.DISJOINT_SYM"
|
|
|
243 |
"DISJOINT_SING_EMPTY" > "HOL4Base.pred_set.DISJOINT_SING_EMPTY"
|
|
|
244 |
"DISJOINT_INSERT" > "HOL4Base.pred_set.DISJOINT_INSERT"
|
|
|
245 |
"DISJOINT_EMPTY_REFL" > "HOL4Base.pred_set.DISJOINT_EMPTY_REFL"
|
|
|
246 |
"DISJOINT_EMPTY" > "HOL4Base.pred_set.DISJOINT_EMPTY"
|
|
|
247 |
"DISJOINT_DELETE_SYM" > "HOL4Base.pred_set.DISJOINT_DELETE_SYM"
|
|
|
248 |
"DISJOINT_DEF" > "HOL4Base.pred_set.DISJOINT_DEF"
|
|
|
249 |
"DISJOINT_BIGUNION" > "HOL4Base.pred_set.DISJOINT_BIGUNION"
|
|
|
250 |
"DISJOINT_BIGINTER" > "HOL4Base.pred_set.DISJOINT_BIGINTER"
|
|
|
251 |
"DIFF_def" > "HOL4Base.pred_set.DIFF_def"
|
|
|
252 |
"DIFF_UNIV" > "HOL4Base.pred_set.DIFF_UNIV"
|
|
|
253 |
"DIFF_INSERT" > "HOL4Base.pred_set.DIFF_INSERT"
|
|
|
254 |
"DIFF_EQ_EMPTY" > "HOL4Base.pred_set.DIFF_EQ_EMPTY"
|
|
|
255 |
"DIFF_EMPTY" > "HOL4Base.pred_set.DIFF_EMPTY"
|
|
|
256 |
"DIFF_DIFF" > "HOL4Base.pred_set.DIFF_DIFF"
|
|
|
257 |
"DIFF_DEF" > "HOL4Base.pred_set.DIFF_DEF"
|
|
|
258 |
"DELETE_def" > "HOL4Base.pred_set.DELETE_def"
|
|
|
259 |
"DELETE_SUBSET" > "HOL4Base.pred_set.DELETE_SUBSET"
|
|
|
260 |
"DELETE_NON_ELEMENT" > "HOL4Base.pred_set.DELETE_NON_ELEMENT"
|
|
|
261 |
"DELETE_INTER" > "HOL4Base.pred_set.DELETE_INTER"
|
|
|
262 |
"DELETE_INSERT" > "HOL4Base.pred_set.DELETE_INSERT"
|
|
|
263 |
"DELETE_EQ_SING" > "HOL4Base.pred_set.DELETE_EQ_SING"
|
|
|
264 |
"DELETE_DELETE" > "HOL4Base.pred_set.DELETE_DELETE"
|
|
|
265 |
"DELETE_DEF" > "HOL4Base.pred_set.DELETE_DEF"
|
|
|
266 |
"DELETE_COMM" > "HOL4Base.pred_set.DELETE_COMM"
|
|
|
267 |
"DECOMPOSITION" > "HOL4Base.pred_set.DECOMPOSITION"
|
|
|
268 |
"CROSS_def" > "HOL4Base.pred_set.CROSS_def"
|
|
|
269 |
"CROSS_SUBSET" > "HOL4Base.pred_set.CROSS_SUBSET"
|
|
|
270 |
"CROSS_SINGS" > "HOL4Base.pred_set.CROSS_SINGS"
|
|
|
271 |
"CROSS_INSERT_RIGHT" > "HOL4Base.pred_set.CROSS_INSERT_RIGHT"
|
|
|
272 |
"CROSS_INSERT_LEFT" > "HOL4Base.pred_set.CROSS_INSERT_LEFT"
|
|
|
273 |
"CROSS_EMPTY" > "HOL4Base.pred_set.CROSS_EMPTY"
|
|
|
274 |
"CROSS_DEF" > "HOL4Base.pred_set.CROSS_DEF"
|
|
|
275 |
"COUNT_ZERO" > "HOL4Base.pred_set.COUNT_ZERO"
|
|
|
276 |
"COUNT_SUC" > "HOL4Base.pred_set.COUNT_SUC"
|
|
|
277 |
"COMPONENT" > "HOL4Base.pred_set.COMPONENT"
|
|
|
278 |
"COMPL_def" > "HOL4Base.pred_set.COMPL_def"
|
|
|
279 |
"COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
|
|
|
280 |
"COMPL_EMPTY" > "HOL4Base.pred_set.COMPL_EMPTY"
|
|
|
281 |
"COMPL_DEF" > "HOL4Base.pred_set.COMPL_DEF"
|
|
|
282 |
"COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
|
|
|
283 |
"COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
|
|
|
284 |
"CHOICE_SING" > "HOL4Base.pred_set.CHOICE_SING"
|
|
|
285 |
"CHOICE_NOT_IN_REST" > "HOL4Base.pred_set.CHOICE_NOT_IN_REST"
|
|
|
286 |
"CHOICE_INSERT_REST" > "HOL4Base.pred_set.CHOICE_INSERT_REST"
|
|
|
287 |
"CHOICE_DEF" > "HOL4Base.pred_set.CHOICE_DEF"
|
|
|
288 |
"CARD_UNION" > "HOL4Base.pred_set.CARD_UNION"
|
|
|
289 |
"CARD_SUBSET" > "HOL4Base.pred_set.CARD_SUBSET"
|
|
|
290 |
"CARD_SING_CROSS" > "HOL4Base.pred_set.CARD_SING_CROSS"
|
|
|
291 |
"CARD_SING" > "HOL4Base.pred_set.CARD_SING"
|
|
|
292 |
"CARD_PSUBSET" > "HOL4Base.pred_set.CARD_PSUBSET"
|
|
|
293 |
"CARD_INTER_LESS_EQ" > "HOL4Base.pred_set.CARD_INTER_LESS_EQ"
|
|
|
294 |
"CARD_INSERT" > "HOL4Base.pred_set.CARD_INSERT"
|
|
|
295 |
"CARD_EQ_0" > "HOL4Base.pred_set.CARD_EQ_0"
|
|
|
296 |
"CARD_EMPTY" > "HOL4Base.pred_set.CARD_EMPTY"
|
|
|
297 |
"CARD_DIFF" > "HOL4Base.pred_set.CARD_DIFF"
|
|
|
298 |
"CARD_DELETE" > "HOL4Base.pred_set.CARD_DELETE"
|
|
|
299 |
"CARD_DEF" > "HOL4Base.pred_set.CARD_DEF"
|
|
|
300 |
"CARD_CROSS" > "HOL4Base.pred_set.CARD_CROSS"
|
|
|
301 |
"CARD_COUNT" > "HOL4Base.pred_set.CARD_COUNT"
|
|
|
302 |
"BIJ_def" > "HOL4Base.pred_set.BIJ_def"
|
|
|
303 |
"BIJ_ID" > "HOL4Base.pred_set.BIJ_ID"
|
|
|
304 |
"BIJ_EMPTY" > "HOL4Base.pred_set.BIJ_EMPTY"
|
|
|
305 |
"BIJ_DEF" > "HOL4Base.pred_set.BIJ_DEF"
|
|
|
306 |
"BIJ_COMPOSE" > "HOL4Base.pred_set.BIJ_COMPOSE"
|
|
|
307 |
"BIGUNION_def" > "HOL4Base.pred_set.BIGUNION_def"
|
|
|
308 |
"BIGUNION_UNION" > "HOL4Base.pred_set.BIGUNION_UNION"
|
|
|
309 |
"BIGUNION_SUBSET" > "HOL4Base.pred_set.BIGUNION_SUBSET"
|
|
|
310 |
"BIGUNION_SING" > "HOL4Base.pred_set.BIGUNION_SING"
|
|
|
311 |
"BIGUNION_INSERT" > "HOL4Base.pred_set.BIGUNION_INSERT"
|
|
|
312 |
"BIGUNION_EMPTY" > "HOL4Base.pred_set.BIGUNION_EMPTY"
|
|
|
313 |
"BIGUNION" > "HOL4Base.pred_set.BIGUNION"
|
|
|
314 |
"BIGINTER_def" > "HOL4Base.pred_set.BIGINTER_def"
|
|
|
315 |
"BIGINTER_SING" > "HOL4Base.pred_set.BIGINTER_SING"
|
|
|
316 |
"BIGINTER_INTER" > "HOL4Base.pred_set.BIGINTER_INTER"
|
|
|
317 |
"BIGINTER_INSERT" > "HOL4Base.pred_set.BIGINTER_INSERT"
|
|
|
318 |
"BIGINTER_EMPTY" > "HOL4Base.pred_set.BIGINTER_EMPTY"
|
|
|
319 |
"BIGINTER" > "HOL4Base.pred_set.BIGINTER"
|
|
|
320 |
"ABSORPTION" > "HOL4Base.pred_set.ABSORPTION"
|
|
|
321 |
|
|
|
322 |
end
|