17644
|
1 |
import
|
|
2 |
|
|
3 |
import_segment "hollight"
|
|
4 |
|
|
5 |
def_maps
|
|
6 |
"two_2" > "two_2_def"
|
|
7 |
"two_1" > "two_1_def"
|
|
8 |
"treal_of_num" > "treal_of_num_def"
|
|
9 |
"treal_neg" > "treal_neg_def"
|
|
10 |
"treal_mul" > "treal_mul_def"
|
|
11 |
"treal_le" > "treal_le_def"
|
|
12 |
"treal_inv" > "treal_inv_def"
|
|
13 |
"treal_eq" > "treal_eq_def"
|
|
14 |
"treal_add" > "treal_add_def"
|
|
15 |
"three_3" > "three_3_def"
|
|
16 |
"three_2" > "three_2_def"
|
|
17 |
"three_1" > "three_1_def"
|
|
18 |
"tendsto" > "tendsto_def"
|
|
19 |
"tends_real_real" > "tends_real_real_def"
|
|
20 |
"tends_num_real" > "tends_num_real_def"
|
|
21 |
"tends" > "tends_def"
|
|
22 |
"tdiv" > "tdiv_def"
|
|
23 |
"tan" > "tan_def"
|
|
24 |
"tailadmissible" > "tailadmissible_def"
|
|
25 |
"support" > "support_def"
|
|
26 |
"superadmissible" > "superadmissible_def"
|
|
27 |
"sup" > "sup_def"
|
|
28 |
"sums" > "sums_def"
|
|
29 |
"summable" > "summable_def"
|
|
30 |
"suminf" > "suminf_def"
|
|
31 |
"sum" > "sum_def"
|
|
32 |
"subseq" > "subseq_def"
|
|
33 |
"sqrt" > "sqrt_def"
|
|
34 |
"sndcart" > "sndcart_def"
|
|
35 |
"sin" > "sin_def"
|
|
36 |
"set_of_list" > "set_of_list_def"
|
|
37 |
"rsum" > "rsum_def"
|
|
38 |
"root" > "root_def"
|
|
39 |
"real_sub" > "real_sub_def"
|
|
40 |
"real_pow" > "real_pow_def"
|
|
41 |
"real_of_num" > "real_of_num_def"
|
|
42 |
"real_neg" > "real_neg_def"
|
|
43 |
"real_mul" > "real_mul_def"
|
|
44 |
"real_min" > "real_min_def"
|
|
45 |
"real_max" > "real_max_def"
|
|
46 |
"real_lt" > "real_lt_def"
|
|
47 |
"real_le" > "real_le_def"
|
|
48 |
"real_inv" > "real_inv_def"
|
|
49 |
"real_gt" > "real_gt_def"
|
|
50 |
"real_ge" > "real_ge_def"
|
|
51 |
"real_div" > "real_div_def"
|
|
52 |
"real_add" > "real_add_def"
|
|
53 |
"real_abs" > "real_abs_def"
|
|
54 |
"re_universe" > "re_universe_def"
|
|
55 |
"re_union" > "re_union_def"
|
|
56 |
"re_subset" > "re_subset_def"
|
|
57 |
"re_null" > "re_null_def"
|
|
58 |
"re_intersect" > "re_intersect_def"
|
|
59 |
"re_compl" > "re_compl_def"
|
|
60 |
"re_Union" > "re_Union_def"
|
|
61 |
"psum" > "psum_def"
|
|
62 |
"pi" > "pi_def"
|
|
63 |
"pastecart" > "pastecart_def"
|
|
64 |
"pairwise" > "pairwise_def"
|
|
65 |
"nsum" > "nsum_def"
|
|
66 |
"neutral" > "neutral_def"
|
|
67 |
"neigh" > "neigh_def"
|
|
68 |
"nadd_rinv" > "nadd_rinv_def"
|
|
69 |
"nadd_of_num" > "nadd_of_num_def"
|
|
70 |
"nadd_mul" > "nadd_mul_def"
|
|
71 |
"nadd_le" > "nadd_le_def"
|
|
72 |
"nadd_inv" > "nadd_inv_def"
|
|
73 |
"nadd_eq" > "nadd_eq_def"
|
|
74 |
"nadd_add" > "nadd_add_def"
|
|
75 |
"mtop" > "mtop_def"
|
|
76 |
"mr1" > "mr1_def"
|
|
77 |
"monoidal" > "monoidal_def"
|
|
78 |
"mono" > "mono_def"
|
|
79 |
"mod_real" > "mod_real_def"
|
|
80 |
"mod_nat" > "mod_nat_def"
|
|
81 |
"mod_int" > "mod_int_def"
|
|
82 |
"minimal" > "minimal_def"
|
|
83 |
"measure" > "measure_def"
|
|
84 |
"ln" > "ln_def"
|
|
85 |
"list_of_set" > "list_of_set_def"
|
|
86 |
"limpt" > "limpt_def"
|
|
87 |
"lim" > "lim_def"
|
|
88 |
"lambda" > "lambda_def"
|
|
89 |
"iterate" > "iterate_def"
|
|
90 |
"istopology" > "istopology_def"
|
|
91 |
"ismet" > "ismet_def"
|
|
92 |
"is_nadd" > "is_nadd_def"
|
|
93 |
"is_int" > "is_int_def"
|
|
94 |
"int_sub" > "int_sub_def"
|
|
95 |
"int_pow" > "int_pow_def"
|
|
96 |
"int_of_num" > "int_of_num_def"
|
|
97 |
"int_neg" > "int_neg_def"
|
|
98 |
"int_mul" > "int_mul_def"
|
|
99 |
"int_min" > "int_min_def"
|
|
100 |
"int_max" > "int_max_def"
|
|
101 |
"int_lt" > "int_lt_def"
|
|
102 |
"int_le" > "int_le_def"
|
|
103 |
"int_gt" > "int_gt_def"
|
|
104 |
"int_ge" > "int_ge_def"
|
|
105 |
"int_add" > "int_add_def"
|
|
106 |
"int_abs" > "int_abs_def"
|
|
107 |
"hreal_of_num" > "hreal_of_num_def"
|
|
108 |
"hreal_mul" > "hreal_mul_def"
|
|
109 |
"hreal_le" > "hreal_le_def"
|
|
110 |
"hreal_inv" > "hreal_inv_def"
|
|
111 |
"hreal_add" > "hreal_add_def"
|
|
112 |
"gauge" > "gauge_def"
|
|
113 |
"fstcart" > "fstcart_def"
|
|
114 |
"finite_index" > "finite_index_def"
|
|
115 |
"fine" > "fine_def"
|
|
116 |
"exp" > "exp_def"
|
|
117 |
"eqeq" > "eqeq_def"
|
|
118 |
"dsize" > "dsize_def"
|
|
119 |
"dotdot" > "dotdot_def"
|
|
120 |
"dorder" > "dorder_def"
|
|
121 |
"division" > "division_def"
|
|
122 |
"dist" > "dist_def"
|
|
123 |
"dimindex" > "dimindex_def"
|
|
124 |
"diffs" > "diffs_def"
|
|
125 |
"diffl" > "diffl_def"
|
|
126 |
"differentiable" > "differentiable_def"
|
|
127 |
"defint" > "defint_def"
|
|
128 |
"cos" > "cos_def"
|
|
129 |
"convergent" > "convergent_def"
|
|
130 |
"contl" > "contl_def"
|
|
131 |
"closed" > "closed_def"
|
|
132 |
"cauchy" > "cauchy_def"
|
|
133 |
"bounded" > "bounded_def"
|
|
134 |
"ball" > "ball_def"
|
|
135 |
"atn" > "atn_def"
|
|
136 |
"asn" > "asn_def"
|
|
137 |
"admissible" > "admissible_def"
|
|
138 |
"acs" > "acs_def"
|
|
139 |
"_FALSITY_" > "_FALSITY__def"
|
|
140 |
"_10314" > "_10314_def"
|
|
141 |
"_10313" > "_10313_def"
|
|
142 |
"_10312" > "_10312_def"
|
|
143 |
"_10289" > "_10289_def"
|
|
144 |
"_10288" > "_10288_def"
|
|
145 |
"ZRECSPACE" > "ZRECSPACE_def"
|
|
146 |
"ZIP" > "ZIP_def"
|
|
147 |
"ZCONSTR" > "ZCONSTR_def"
|
|
148 |
"ZBOT" > "ZBOT_def"
|
|
149 |
"WF" > "WF_def"
|
|
150 |
"UNIV" > "UNIV_def"
|
|
151 |
"UNIONS" > "UNIONS_def"
|
|
152 |
"UNION" > "UNION_def"
|
|
153 |
"UNCURRY" > "UNCURRY_def"
|
|
154 |
"TL" > "TL_def"
|
|
155 |
"SURJ" > "SURJ_def"
|
|
156 |
"SUBSET" > "SUBSET_def"
|
|
157 |
"SOME" > "SOME_def"
|
|
158 |
"SING" > "SING_def"
|
|
159 |
"SETSPEC" > "SETSPEC_def"
|
|
160 |
"REVERSE" > "REVERSE_def"
|
|
161 |
"REST" > "REST_def"
|
|
162 |
"REPLICATE" > "REPLICATE_def"
|
|
163 |
"PSUBSET" > "PSUBSET_def"
|
|
164 |
"PASSOC" > "PASSOC_def"
|
|
165 |
"PAIRWISE" > "PAIRWISE_def"
|
|
166 |
"OUTR" > "OUTR_def"
|
|
167 |
"OUTL" > "OUTL_def"
|
|
168 |
"ODD" > "ODD_def"
|
|
169 |
"NUMSUM" > "NUMSUM_def"
|
|
170 |
"NUMSND" > "NUMSND_def"
|
|
171 |
"NUMRIGHT" > "NUMRIGHT_def"
|
|
172 |
"NUMPAIR" > "NUMPAIR_def"
|
|
173 |
"NUMLEFT" > "NUMLEFT_def"
|
|
174 |
"NUMFST" > "NUMFST_def"
|
|
175 |
"NULL" > "NULL_def"
|
|
176 |
"NONE" > "NONE_def"
|
|
177 |
"NIL" > "NIL_def"
|
|
178 |
"MOD" > "MOD_def"
|
|
179 |
"MEM" > "MEM_def"
|
|
180 |
"MAP2" > "MAP2_def"
|
|
181 |
"MAP" > "MAP_def"
|
|
182 |
"LET_END" > "LET_END_def"
|
|
183 |
"LENGTH" > "LENGTH_def"
|
|
184 |
"LAST" > "LAST_def"
|
|
185 |
"ITSET" > "ITSET_def"
|
|
186 |
"ITLIST2" > "ITLIST2_def"
|
|
187 |
"ITLIST" > "ITLIST_def"
|
|
188 |
"ISO" > "ISO_def"
|
|
189 |
"INTERS" > "INTERS_def"
|
|
190 |
"INTER" > "INTER_def"
|
|
191 |
"INSERT" > "INSERT_def"
|
|
192 |
"INR" > "INR_def"
|
|
193 |
"INL" > "INL_def"
|
|
194 |
"INJP" > "INJP_def"
|
|
195 |
"INJN" > "INJN_def"
|
|
196 |
"INJF" > "INJF_def"
|
|
197 |
"INJA" > "INJA_def"
|
|
198 |
"INJ" > "INJ_def"
|
|
199 |
"INFINITE" > "INFINITE_def"
|
|
200 |
"IN" > "IN_def"
|
|
201 |
"IMAGE" > "IMAGE_def"
|
|
202 |
"HD" > "HD_def"
|
|
203 |
"HAS_SIZE" > "HAS_SIZE_def"
|
|
204 |
"GSPEC" > "GSPEC_def"
|
|
205 |
"GEQ" > "GEQ_def"
|
|
206 |
"GABS" > "GABS_def"
|
|
207 |
"FNIL" > "FNIL_def"
|
|
208 |
"FINREC" > "FINREC_def"
|
|
209 |
"FINITE" > "FINITE_def"
|
|
210 |
"FILTER" > "FILTER_def"
|
|
211 |
"FCONS" > "FCONS_def"
|
|
212 |
"FACT" > "FACT_def"
|
|
213 |
"EXP" > "EXP_def"
|
|
214 |
"EX" > "EX_def"
|
|
215 |
"EVEN" > "EVEN_def"
|
|
216 |
"EMPTY" > "EMPTY_def"
|
|
217 |
"EL" > "EL_def"
|
|
218 |
"DIV" > "DIV_def"
|
|
219 |
"DISJOINT" > "DISJOINT_def"
|
|
220 |
"DIFF" > "DIFF_def"
|
|
221 |
"DELETE" > "DELETE_def"
|
|
222 |
"DECIMAL" > "DECIMAL_def"
|
|
223 |
"CURRY" > "CURRY_def"
|
|
224 |
"COUNTABLE" > "COUNTABLE_def"
|
|
225 |
"CONSTR" > "CONSTR_def"
|
|
226 |
"CONS" > "CONS_def"
|
|
227 |
"COND" > "COND_def"
|
|
228 |
"CHOICE" > "CHOICE_def"
|
|
229 |
"CASEWISE" > "CASEWISE_def"
|
|
230 |
"CARD_LT" > "CARD_LT_def"
|
|
231 |
"CARD_LE" > "CARD_LE_def"
|
|
232 |
"CARD_GT" > "CARD_GT_def"
|
|
233 |
"CARD_GE" > "CARD_GE_def"
|
|
234 |
"CARD_EQ" > "CARD_EQ_def"
|
|
235 |
"CARD" > "CARD_def"
|
|
236 |
"BOTTOM" > "BOTTOM_def"
|
|
237 |
"BIJ" > "BIJ_def"
|
|
238 |
"ASSOC" > "ASSOC_def"
|
|
239 |
"APPEND" > "APPEND_def"
|
|
240 |
"ALL_list" > "ALL_list_def"
|
|
241 |
"ALL2" > "ALL2_def"
|
|
242 |
">=" > ">=_def"
|
|
243 |
">" > ">_def"
|
|
244 |
"<=" > "<=_def"
|
|
245 |
"<" > "<_def"
|
|
246 |
"$" > "$_def"
|
|
247 |
|
|
248 |
type_maps
|
|
249 |
"topology" > "HOLLight.hollight.topology"
|
|
250 |
"sum" > "HOLLight.hollight.sum"
|
|
251 |
"recspace" > "HOLLight.hollight.recspace"
|
|
252 |
"real" > "HOLLight.hollight.real"
|
|
253 |
"prod" > "*"
|
|
254 |
"option" > "HOLLight.hollight.option"
|
|
255 |
"num" > "nat"
|
|
256 |
"nadd" > "HOLLight.hollight.nadd"
|
|
257 |
"metric" > "HOLLight.hollight.metric"
|
|
258 |
"list" > "HOLLight.hollight.list"
|
|
259 |
"int" > "HOLLight.hollight.int"
|
|
260 |
"ind" > "Nat.ind"
|
|
261 |
"hreal" > "HOLLight.hollight.hreal"
|
|
262 |
"fun" > "fun"
|
|
263 |
"finite_sum" > "HOLLight.hollight.finite_sum"
|
|
264 |
"finite_image" > "HOLLight.hollight.finite_image"
|
|
265 |
"cart" > "HOLLight.hollight.cart"
|
|
266 |
"bool" > "bool"
|
|
267 |
"N_3" > "HOLLight.hollight.N_3"
|
|
268 |
"N_2" > "HOLLight.hollight.N_2"
|
|
269 |
"N_1" > "Product_Type.unit"
|
|
270 |
|
|
271 |
const_maps
|
|
272 |
"~" > "Not"
|
|
273 |
"two_2" > "HOLLight.hollight.two_2"
|
|
274 |
"two_1" > "HOLLight.hollight.two_1"
|
|
275 |
"treal_of_num" > "HOLLight.hollight.treal_of_num"
|
|
276 |
"treal_neg" > "HOLLight.hollight.treal_neg"
|
|
277 |
"treal_mul" > "HOLLight.hollight.treal_mul"
|
|
278 |
"treal_le" > "HOLLight.hollight.treal_le"
|
|
279 |
"treal_inv" > "HOLLight.hollight.treal_inv"
|
|
280 |
"treal_eq" > "HOLLight.hollight.treal_eq"
|
|
281 |
"treal_add" > "HOLLight.hollight.treal_add"
|
|
282 |
"three_3" > "HOLLight.hollight.three_3"
|
|
283 |
"three_2" > "HOLLight.hollight.three_2"
|
|
284 |
"three_1" > "HOLLight.hollight.three_1"
|
|
285 |
"tendsto" > "HOLLight.hollight.tendsto"
|
|
286 |
"tends_real_real" > "HOLLight.hollight.tends_real_real"
|
|
287 |
"tends_num_real" > "HOLLight.hollight.tends_num_real"
|
|
288 |
"tends" > "HOLLight.hollight.tends"
|
|
289 |
"tdiv" > "HOLLight.hollight.tdiv"
|
|
290 |
"tan" > "HOLLight.hollight.tan"
|
|
291 |
"tailadmissible" > "HOLLight.hollight.tailadmissible"
|
|
292 |
"support" > "HOLLight.hollight.support"
|
|
293 |
"superadmissible" > "HOLLight.hollight.superadmissible"
|
|
294 |
"sup" > "HOLLight.hollight.sup"
|
|
295 |
"sums" > "HOLLight.hollight.sums"
|
|
296 |
"summable" > "HOLLight.hollight.summable"
|
|
297 |
"suminf" > "HOLLight.hollight.suminf"
|
|
298 |
"sum" > "HOLLight.hollight.sum"
|
|
299 |
"subseq" > "HOLLight.hollight.subseq"
|
|
300 |
"sqrt" > "HOLLight.hollight.sqrt"
|
|
301 |
"sndcart" > "HOLLight.hollight.sndcart"
|
|
302 |
"sin" > "HOLLight.hollight.sin"
|
|
303 |
"set_of_list" > "HOLLight.hollight.set_of_list"
|
|
304 |
"rsum" > "HOLLight.hollight.rsum"
|
|
305 |
"root" > "HOLLight.hollight.root"
|
|
306 |
"real_sub" > "HOLLight.hollight.real_sub"
|
|
307 |
"real_pow" > "HOLLight.hollight.real_pow"
|
|
308 |
"real_of_num" > "HOLLight.hollight.real_of_num"
|
|
309 |
"real_neg" > "HOLLight.hollight.real_neg"
|
|
310 |
"real_mul" > "HOLLight.hollight.real_mul"
|
|
311 |
"real_min" > "HOLLight.hollight.real_min"
|
|
312 |
"real_max" > "HOLLight.hollight.real_max"
|
|
313 |
"real_lt" > "HOLLight.hollight.real_lt"
|
|
314 |
"real_le" > "HOLLight.hollight.real_le"
|
|
315 |
"real_inv" > "HOLLight.hollight.real_inv"
|
|
316 |
"real_gt" > "HOLLight.hollight.real_gt"
|
|
317 |
"real_ge" > "HOLLight.hollight.real_ge"
|
|
318 |
"real_div" > "HOLLight.hollight.real_div"
|
|
319 |
"real_add" > "HOLLight.hollight.real_add"
|
|
320 |
"real_abs" > "HOLLight.hollight.real_abs"
|
|
321 |
"re_universe" > "HOLLight.hollight.re_universe"
|
|
322 |
"re_union" > "HOLLight.hollight.re_union"
|
|
323 |
"re_subset" > "HOLLight.hollight.re_subset"
|
|
324 |
"re_null" > "HOLLight.hollight.re_null"
|
|
325 |
"re_intersect" > "HOLLight.hollight.re_intersect"
|
|
326 |
"re_compl" > "HOLLight.hollight.re_compl"
|
|
327 |
"re_Union" > "HOLLight.hollight.re_Union"
|
|
328 |
"psum" > "HOLLight.hollight.psum"
|
|
329 |
"pi" > "HOLLight.hollight.pi"
|
|
330 |
"pastecart" > "HOLLight.hollight.pastecart"
|
|
331 |
"pairwise" > "HOLLight.hollight.pairwise"
|
|
332 |
"one" > "Product_Type.Unity"
|
|
333 |
"o" > "Fun.comp"
|
|
334 |
"nsum" > "HOLLight.hollight.nsum"
|
|
335 |
"neutral" > "HOLLight.hollight.neutral"
|
|
336 |
"neigh" > "HOLLight.hollight.neigh"
|
|
337 |
"nadd_rinv" > "HOLLight.hollight.nadd_rinv"
|
|
338 |
"nadd_of_num" > "HOLLight.hollight.nadd_of_num"
|
|
339 |
"nadd_mul" > "HOLLight.hollight.nadd_mul"
|
|
340 |
"nadd_le" > "HOLLight.hollight.nadd_le"
|
|
341 |
"nadd_inv" > "HOLLight.hollight.nadd_inv"
|
|
342 |
"nadd_eq" > "HOLLight.hollight.nadd_eq"
|
|
343 |
"nadd_add" > "HOLLight.hollight.nadd_add"
|
|
344 |
"mtop" > "HOLLight.hollight.mtop"
|
|
345 |
"mr1" > "HOLLight.hollight.mr1"
|
|
346 |
"monoidal" > "HOLLight.hollight.monoidal"
|
|
347 |
"mono" > "HOLLight.hollight.mono"
|
|
348 |
"mod_real" > "HOLLight.hollight.mod_real"
|
|
349 |
"mod_nat" > "HOLLight.hollight.mod_nat"
|
|
350 |
"mod_int" > "HOLLight.hollight.mod_int"
|
|
351 |
"mk_pair" > "Product_Type.Pair_Rep"
|
|
352 |
"minimal" > "HOLLight.hollight.minimal"
|
|
353 |
"measure" > "HOLLight.hollight.measure"
|
|
354 |
"ln" > "HOLLight.hollight.ln"
|
|
355 |
"list_of_set" > "HOLLight.hollight.list_of_set"
|
|
356 |
"limpt" > "HOLLight.hollight.limpt"
|
|
357 |
"lim" > "HOLLight.hollight.lim"
|
|
358 |
"lambda" > "HOLLight.hollight.lambda"
|
|
359 |
"iterate" > "HOLLight.hollight.iterate"
|
|
360 |
"istopology" > "HOLLight.hollight.istopology"
|
|
361 |
"ismet" > "HOLLight.hollight.ismet"
|
|
362 |
"is_nadd" > "HOLLight.hollight.is_nadd"
|
|
363 |
"is_int" > "HOLLight.hollight.is_int"
|
|
364 |
"int_sub" > "HOLLight.hollight.int_sub"
|
|
365 |
"int_pow" > "HOLLight.hollight.int_pow"
|
|
366 |
"int_of_num" > "HOLLight.hollight.int_of_num"
|
|
367 |
"int_neg" > "HOLLight.hollight.int_neg"
|
|
368 |
"int_mul" > "HOLLight.hollight.int_mul"
|
|
369 |
"int_min" > "HOLLight.hollight.int_min"
|
|
370 |
"int_max" > "HOLLight.hollight.int_max"
|
|
371 |
"int_lt" > "HOLLight.hollight.int_lt"
|
|
372 |
"int_le" > "HOLLight.hollight.int_le"
|
|
373 |
"int_gt" > "HOLLight.hollight.int_gt"
|
|
374 |
"int_ge" > "HOLLight.hollight.int_ge"
|
|
375 |
"int_add" > "HOLLight.hollight.int_add"
|
|
376 |
"int_abs" > "HOLLight.hollight.int_abs"
|
|
377 |
"hreal_of_num" > "HOLLight.hollight.hreal_of_num"
|
|
378 |
"hreal_mul" > "HOLLight.hollight.hreal_mul"
|
|
379 |
"hreal_le" > "HOLLight.hollight.hreal_le"
|
|
380 |
"hreal_inv" > "HOLLight.hollight.hreal_inv"
|
|
381 |
"hreal_add" > "HOLLight.hollight.hreal_add"
|
|
382 |
"gauge" > "HOLLight.hollight.gauge"
|
|
383 |
"fstcart" > "HOLLight.hollight.fstcart"
|
|
384 |
"finite_index" > "HOLLight.hollight.finite_index"
|
|
385 |
"fine" > "HOLLight.hollight.fine"
|
|
386 |
"exp" > "HOLLight.hollight.exp"
|
|
387 |
"eqeq" > "HOLLight.hollight.eqeq"
|
|
388 |
"dsize" > "HOLLight.hollight.dsize"
|
|
389 |
"dotdot" > "HOLLight.hollight.dotdot"
|
|
390 |
"dorder" > "HOLLight.hollight.dorder"
|
|
391 |
"division" > "HOLLight.hollight.division"
|
|
392 |
"dist" > "HOLLight.hollight.dist"
|
|
393 |
"dimindex" > "HOLLight.hollight.dimindex"
|
|
394 |
"diffs" > "HOLLight.hollight.diffs"
|
|
395 |
"diffl" > "HOLLight.hollight.diffl"
|
|
396 |
"differentiable" > "HOLLight.hollight.differentiable"
|
|
397 |
"defint" > "HOLLight.hollight.defint"
|
|
398 |
"cos" > "HOLLight.hollight.cos"
|
|
399 |
"convergent" > "HOLLight.hollight.convergent"
|
|
400 |
"contl" > "HOLLight.hollight.contl"
|
|
401 |
"closed" > "HOLLight.hollight.closed"
|
|
402 |
"cauchy" > "HOLLight.hollight.cauchy"
|
|
403 |
"bounded" > "HOLLight.hollight.bounded"
|
|
404 |
"ball" > "HOLLight.hollight.ball"
|
|
405 |
"atn" > "HOLLight.hollight.atn"
|
|
406 |
"asn" > "HOLLight.hollight.asn"
|
|
407 |
"admissible" > "HOLLight.hollight.admissible"
|
|
408 |
"acs" > "HOLLight.hollight.acs"
|
|
409 |
"_FALSITY_" > "HOLLight.hollight._FALSITY_"
|
|
410 |
"_10314" > "HOLLight.hollight._10314"
|
|
411 |
"_10313" > "HOLLight.hollight._10313"
|
|
412 |
"_10312" > "HOLLight.hollight._10312"
|
|
413 |
"_10289" > "HOLLight.hollight._10289"
|
|
414 |
"_10288" > "HOLLight.hollight._10288"
|
|
415 |
"_0" > "0" :: "nat"
|
|
416 |
"\\/" > "op |"
|
|
417 |
"ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
|
|
418 |
"ZIP" > "HOLLight.hollight.ZIP"
|
|
419 |
"ZCONSTR" > "HOLLight.hollight.ZCONSTR"
|
|
420 |
"ZBOT" > "HOLLight.hollight.ZBOT"
|
|
421 |
"WF" > "HOLLight.hollight.WF"
|
|
422 |
"UNIV" > "HOLLight.hollight.UNIV"
|
|
423 |
"UNIONS" > "HOLLight.hollight.UNIONS"
|
|
424 |
"UNION" > "HOLLight.hollight.UNION"
|
|
425 |
"UNCURRY" > "HOLLight.hollight.UNCURRY"
|
|
426 |
"TL" > "HOLLight.hollight.TL"
|
|
427 |
"T" > "True"
|
|
428 |
"SURJ" > "HOLLight.hollight.SURJ"
|
|
429 |
"SUC" > "Suc"
|
|
430 |
"SUBSET" > "HOLLight.hollight.SUBSET"
|
|
431 |
"SOME" > "HOLLight.hollight.SOME"
|
|
432 |
"SND" > "snd"
|
|
433 |
"SING" > "HOLLight.hollight.SING"
|
|
434 |
"SETSPEC" > "HOLLight.hollight.SETSPEC"
|
|
435 |
"REVERSE" > "HOLLight.hollight.REVERSE"
|
|
436 |
"REST" > "HOLLight.hollight.REST"
|
|
437 |
"REP_prod" > "Rep_Prod"
|
|
438 |
"REPLICATE" > "HOLLight.hollight.REPLICATE"
|
|
439 |
"PSUBSET" > "HOLLight.hollight.PSUBSET"
|
|
440 |
"PRE" > "HOLLightCompat.Pred"
|
|
441 |
"PASSOC" > "HOLLight.hollight.PASSOC"
|
|
442 |
"PAIRWISE" > "HOLLight.hollight.PAIRWISE"
|
|
443 |
"OUTR" > "HOLLight.hollight.OUTR"
|
|
444 |
"OUTL" > "HOLLight.hollight.OUTL"
|
|
445 |
"ONTO" > "Fun.surj"
|
|
446 |
"ONE_ONE" > "HOL4Setup.ONE_ONE"
|
|
447 |
"ODD" > "HOLLight.hollight.ODD"
|
|
448 |
"NUMSUM" > "HOLLight.hollight.NUMSUM"
|
|
449 |
"NUMSND" > "HOLLight.hollight.NUMSND"
|
|
450 |
"NUMRIGHT" > "HOLLight.hollight.NUMRIGHT"
|
|
451 |
"NUMPAIR" > "HOLLight.hollight.NUMPAIR"
|
|
452 |
"NUMLEFT" > "HOLLight.hollight.NUMLEFT"
|
|
453 |
"NUMFST" > "HOLLight.hollight.NUMFST"
|
|
454 |
"NUMERAL" > "HOL4Compat.NUMERAL"
|
|
455 |
"NULL" > "HOLLight.hollight.NULL"
|
|
456 |
"NONE" > "HOLLight.hollight.NONE"
|
|
457 |
"NIL" > "HOLLight.hollight.NIL"
|
|
458 |
"MOD" > "HOLLight.hollight.MOD"
|
|
459 |
"MEM" > "HOLLight.hollight.MEM"
|
|
460 |
"MAP2" > "HOLLight.hollight.MAP2"
|
|
461 |
"MAP" > "HOLLight.hollight.MAP"
|
|
462 |
"LET_END" > "HOLLight.hollight.LET_END"
|
|
463 |
"LET" > "HOL4Compat.LET"
|
|
464 |
"LENGTH" > "HOLLight.hollight.LENGTH"
|
|
465 |
"LAST" > "HOLLight.hollight.LAST"
|
|
466 |
"ITSET" > "HOLLight.hollight.ITSET"
|
|
467 |
"ITLIST2" > "HOLLight.hollight.ITLIST2"
|
|
468 |
"ITLIST" > "HOLLight.hollight.ITLIST"
|
|
469 |
"ISO" > "HOLLight.hollight.ISO"
|
|
470 |
"INTERS" > "HOLLight.hollight.INTERS"
|
|
471 |
"INTER" > "HOLLight.hollight.INTER"
|
|
472 |
"INSERT" > "HOLLight.hollight.INSERT"
|
|
473 |
"INR" > "HOLLight.hollight.INR"
|
|
474 |
"INL" > "HOLLight.hollight.INL"
|
|
475 |
"INJP" > "HOLLight.hollight.INJP"
|
|
476 |
"INJN" > "HOLLight.hollight.INJN"
|
|
477 |
"INJF" > "HOLLight.hollight.INJF"
|
|
478 |
"INJA" > "HOLLight.hollight.INJA"
|
|
479 |
"INJ" > "HOLLight.hollight.INJ"
|
|
480 |
"INFINITE" > "HOLLight.hollight.INFINITE"
|
|
481 |
"IN" > "HOLLight.hollight.IN"
|
|
482 |
"IMAGE" > "HOLLight.hollight.IMAGE"
|
|
483 |
"I" > "Fun.id"
|
|
484 |
"HD" > "HOLLight.hollight.HD"
|
|
485 |
"HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
|
|
486 |
"GSPEC" > "HOLLight.hollight.GSPEC"
|
|
487 |
"GEQ" > "HOLLight.hollight.GEQ"
|
|
488 |
"GABS" > "HOLLight.hollight.GABS"
|
|
489 |
"FST" > "fst"
|
|
490 |
"FNIL" > "HOLLight.hollight.FNIL"
|
|
491 |
"FINREC" > "HOLLight.hollight.FINREC"
|
|
492 |
"FINITE" > "HOLLight.hollight.FINITE"
|
|
493 |
"FILTER" > "HOLLight.hollight.FILTER"
|
|
494 |
"FCONS" > "HOLLight.hollight.FCONS"
|
|
495 |
"FACT" > "HOLLight.hollight.FACT"
|
|
496 |
"F" > "False"
|
|
497 |
"EXP" > "HOLLight.hollight.EXP"
|
|
498 |
"EX" > "HOLLight.hollight.EX"
|
|
499 |
"EVEN" > "HOLLight.hollight.EVEN"
|
|
500 |
"EMPTY" > "HOLLight.hollight.EMPTY"
|
|
501 |
"EL" > "HOLLight.hollight.EL"
|
|
502 |
"DIV" > "HOLLight.hollight.DIV"
|
|
503 |
"DISJOINT" > "HOLLight.hollight.DISJOINT"
|
|
504 |
"DIFF" > "HOLLight.hollight.DIFF"
|
|
505 |
"DELETE" > "HOLLight.hollight.DELETE"
|
|
506 |
"DECIMAL" > "HOLLight.hollight.DECIMAL"
|
|
507 |
"CURRY" > "HOLLight.hollight.CURRY"
|
|
508 |
"COUNTABLE" > "HOLLight.hollight.COUNTABLE"
|
|
509 |
"CONSTR" > "HOLLight.hollight.CONSTR"
|
|
510 |
"CONS" > "HOLLight.hollight.CONS"
|
|
511 |
"COND" > "HOLLight.hollight.COND"
|
|
512 |
"CHOICE" > "HOLLight.hollight.CHOICE"
|
|
513 |
"CASEWISE" > "HOLLight.hollight.CASEWISE"
|
|
514 |
"CARD_LT" > "HOLLight.hollight.CARD_LT"
|
|
515 |
"CARD_LE" > "HOLLight.hollight.CARD_LE"
|
|
516 |
"CARD_GT" > "HOLLight.hollight.CARD_GT"
|
|
517 |
"CARD_GE" > "HOLLight.hollight.CARD_GE"
|
|
518 |
"CARD_EQ" > "HOLLight.hollight.CARD_EQ"
|
|
519 |
"CARD" > "HOLLight.hollight.CARD"
|
|
520 |
"BOTTOM" > "HOLLight.hollight.BOTTOM"
|
|
521 |
"BIT1" > "HOL4Compat.NUMERAL_BIT1"
|
|
522 |
"BIT0" > "HOLLightCompat.NUMERAL_BIT0"
|
|
523 |
"BIJ" > "HOLLight.hollight.BIJ"
|
|
524 |
"ASSOC" > "HOLLight.hollight.ASSOC"
|
|
525 |
"APPEND" > "HOLLight.hollight.APPEND"
|
|
526 |
"ALL_list" > "HOLLight.hollight.ALL_list"
|
|
527 |
"ALL2" > "HOLLight.hollight.ALL2"
|
|
528 |
"ABS_prod" > "Abs_Prod"
|
|
529 |
"@" > "Hilbert_Choice.Eps"
|
|
530 |
"?!" > "Ex1"
|
|
531 |
"?" > "Ex"
|
|
532 |
">=" > "HOLLight.hollight.>="
|
|
533 |
">" > "HOLLight.hollight.>"
|
|
534 |
"==>" > "op -->"
|
|
535 |
"=" > "op ="
|
|
536 |
"<=" > "HOLLight.hollight.<="
|
|
537 |
"<" > "HOLLight.hollight.<"
|
|
538 |
"/\\" > "op &"
|
|
539 |
"-" > "op -" :: "nat => nat => nat"
|
|
540 |
"," > "Pair"
|
|
541 |
"+" > "op +" :: "nat => nat => nat"
|
|
542 |
"*" > "op *" :: "nat => nat => nat"
|
|
543 |
"$" > "HOLLight.hollight.$"
|
|
544 |
"!" > "All"
|
|
545 |
|
|
546 |
const_renames
|
|
547 |
"ALL" > "ALL_list"
|
|
548 |
"==" > "eqeq"
|
|
549 |
".." > "dotdot"
|
|
550 |
|
|
551 |
thm_maps
|
|
552 |
"two_2_def" > "HOLLight.hollight.two_2_def"
|
|
553 |
"two_1_def" > "HOLLight.hollight.two_1_def"
|
|
554 |
"treal_of_num_def" > "HOLLight.hollight.treal_of_num_def"
|
|
555 |
"treal_neg_def" > "HOLLight.hollight.treal_neg_def"
|
|
556 |
"treal_mul_def" > "HOLLight.hollight.treal_mul_def"
|
|
557 |
"treal_le_def" > "HOLLight.hollight.treal_le_def"
|
|
558 |
"treal_inv_def" > "HOLLight.hollight.treal_inv_def"
|
|
559 |
"treal_eq_def" > "HOLLight.hollight.treal_eq_def"
|
|
560 |
"treal_add_def" > "HOLLight.hollight.treal_add_def"
|
|
561 |
"three_3_def" > "HOLLight.hollight.three_3_def"
|
|
562 |
"three_2_def" > "HOLLight.hollight.three_2_def"
|
|
563 |
"three_1_def" > "HOLLight.hollight.three_1_def"
|
|
564 |
"th_cond" > "HOLLight.hollight.th_cond"
|
|
565 |
"th" > "HOLLight.hollight.th"
|
|
566 |
"tendsto_def" > "HOLLight.hollight.tendsto_def"
|
|
567 |
"tends_real_real_def" > "HOLLight.hollight.tends_real_real_def"
|
|
568 |
"tends_num_real_def" > "HOLLight.hollight.tends_num_real_def"
|
|
569 |
"tends_def" > "HOLLight.hollight.tends_def"
|
|
570 |
"tdiv_def" > "HOLLight.hollight.tdiv_def"
|
|
571 |
"tan_def" > "HOLLight.hollight.tan_def"
|
|
572 |
"tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
|
|
573 |
"support_def" > "HOLLight.hollight.support_def"
|
|
574 |
"superadmissible_def" > "HOLLight.hollight.superadmissible_def"
|
|
575 |
"sup_def" > "HOLLight.hollight.sup_def"
|
|
576 |
"sup" > "HOLLight.hollight.sup"
|
|
577 |
"sums_def" > "HOLLight.hollight.sums_def"
|
|
578 |
"summable_def" > "HOLLight.hollight.summable_def"
|
|
579 |
"suminf_def" > "HOLLight.hollight.suminf_def"
|
|
580 |
"sum_def" > "HOLLight.hollight.sum_def"
|
|
581 |
"sum_EXISTS" > "HOLLight.hollight.sum_EXISTS"
|
|
582 |
"sum" > "HOLLight.hollight.sum"
|
|
583 |
"subseq_def" > "HOLLight.hollight.subseq_def"
|
|
584 |
"sth" > "HOLLight.hollight.sth"
|
|
585 |
"sqrt_def" > "HOLLight.hollight.sqrt_def"
|
|
586 |
"sqrt" > "HOLLight.hollight.sqrt"
|
|
587 |
"sndcart_def" > "HOLLight.hollight.sndcart_def"
|
|
588 |
"sin_def" > "HOLLight.hollight.sin_def"
|
|
589 |
"set_of_list_def" > "HOLLight.hollight.set_of_list_def"
|
|
590 |
"rsum_def" > "HOLLight.hollight.rsum_def"
|
|
591 |
"root_def" > "HOLLight.hollight.root_def"
|
|
592 |
"right_th" > "HOLLight.hollight.right_th"
|
|
593 |
"real_sub_def" > "HOLLight.hollight.real_sub_def"
|
|
594 |
"real_pow_def" > "HOLLight.hollight.real_pow_def"
|
|
595 |
"real_of_num_def" > "HOLLight.hollight.real_of_num_def"
|
|
596 |
"real_neg_def" > "HOLLight.hollight.real_neg_def"
|
|
597 |
"real_mul_def" > "HOLLight.hollight.real_mul_def"
|
|
598 |
"real_min_def" > "HOLLight.hollight.real_min_def"
|
|
599 |
"real_max_def" > "HOLLight.hollight.real_max_def"
|
|
600 |
"real_lt_def" > "HOLLight.hollight.real_lt_def"
|
|
601 |
"real_le_def" > "HOLLight.hollight.real_le_def"
|
|
602 |
"real_le" > "HOLLight.hollight.real_le"
|
|
603 |
"real_inv_def" > "HOLLight.hollight.real_inv_def"
|
|
604 |
"real_gt_def" > "HOLLight.hollight.real_gt_def"
|
|
605 |
"real_ge_def" > "HOLLight.hollight.real_ge_def"
|
|
606 |
"real_div_def" > "HOLLight.hollight.real_div_def"
|
|
607 |
"real_add_def" > "HOLLight.hollight.real_add_def"
|
|
608 |
"real_abs_def" > "HOLLight.hollight.real_abs_def"
|
|
609 |
"re_universe_def" > "HOLLight.hollight.re_universe_def"
|
|
610 |
"re_union_def" > "HOLLight.hollight.re_union_def"
|
|
611 |
"re_subset_def" > "HOLLight.hollight.re_subset_def"
|
|
612 |
"re_null_def" > "HOLLight.hollight.re_null_def"
|
|
613 |
"re_intersect_def" > "HOLLight.hollight.re_intersect_def"
|
|
614 |
"re_compl_def" > "HOLLight.hollight.re_compl_def"
|
|
615 |
"re_Union_def" > "HOLLight.hollight.re_Union_def"
|
|
616 |
"psum_def" > "HOLLight.hollight.psum_def"
|
|
617 |
"pi_def" > "HOLLight.hollight.pi_def"
|
|
618 |
"pastecart_def" > "HOLLight.hollight.pastecart_def"
|
|
619 |
"pairwise_def" > "HOLLight.hollight.pairwise_def"
|
|
620 |
"pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
|
|
621 |
"pair_INDUCT" > "Datatype.prod.induct"
|
|
622 |
"one_axiom" > "HOLLight.hollight.one_axiom"
|
|
623 |
"one_RECURSION" > "HOLLight.hollight.one_RECURSION"
|
|
624 |
"one_INDUCT" > "Datatype.unit.induct"
|
|
625 |
"one_Axiom" > "HOLLight.hollight.one_Axiom"
|
|
626 |
"one" > "HOL4Compat.one"
|
|
627 |
"o_THM" > "Fun.o_apply"
|
|
628 |
"o_ASSOC" > "HOLLight.hollight.o_ASSOC"
|
|
629 |
"num_WOP" > "HOLLight.hollight.num_WOP"
|
|
630 |
"num_WF" > "HOLLight.hollight.num_WF"
|
|
631 |
"num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
|
|
632 |
"num_MAX" > "HOLLight.hollight.num_MAX"
|
|
633 |
"num_INFINITE" > "HOLLight.hollight.num_INFINITE"
|
|
634 |
"num_INDUCTION" > "List.lexn.induct"
|
|
635 |
"num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
|
|
636 |
"num_FINITE" > "HOLLight.hollight.num_FINITE"
|
|
637 |
"num_CASES" > "Nat.nat.nchotomy"
|
|
638 |
"num_Axiom" > "HOLLight.hollight.num_Axiom"
|
|
639 |
"nsum_def" > "HOLLight.hollight.nsum_def"
|
|
640 |
"neutral_def" > "HOLLight.hollight.neutral_def"
|
|
641 |
"neigh_def" > "HOLLight.hollight.neigh_def"
|
|
642 |
"nadd_rinv_def" > "HOLLight.hollight.nadd_rinv_def"
|
|
643 |
"nadd_of_num_def" > "HOLLight.hollight.nadd_of_num_def"
|
|
644 |
"nadd_mul_def" > "HOLLight.hollight.nadd_mul_def"
|
|
645 |
"nadd_le_def" > "HOLLight.hollight.nadd_le_def"
|
|
646 |
"nadd_inv_def" > "HOLLight.hollight.nadd_inv_def"
|
|
647 |
"nadd_eq_def" > "HOLLight.hollight.nadd_eq_def"
|
|
648 |
"nadd_add_def" > "HOLLight.hollight.nadd_add_def"
|
|
649 |
"mtop_istopology" > "HOLLight.hollight.mtop_istopology"
|
|
650 |
"mtop_def" > "HOLLight.hollight.mtop_def"
|
|
651 |
"mr1_def" > "HOLLight.hollight.mr1_def"
|
|
652 |
"monoidal_def" > "HOLLight.hollight.monoidal_def"
|
|
653 |
"mono_def" > "HOLLight.hollight.mono_def"
|
|
654 |
"mod_real_def" > "HOLLight.hollight.mod_real_def"
|
|
655 |
"mod_nat_def" > "HOLLight.hollight.mod_nat_def"
|
|
656 |
"mod_int_def" > "HOLLight.hollight.mod_int_def"
|
|
657 |
"minimal_def" > "HOLLight.hollight.minimal_def"
|
|
658 |
"measure_def" > "HOLLight.hollight.measure_def"
|
|
659 |
"ln_def" > "HOLLight.hollight.ln_def"
|
|
660 |
"list_of_set_def" > "HOLLight.hollight.list_of_set_def"
|
|
661 |
"list_INDUCT" > "HOLLight.hollight.list_INDUCT"
|
|
662 |
"list_CASES" > "HOLLight.hollight.list_CASES"
|
|
663 |
"limpt_def" > "HOLLight.hollight.limpt_def"
|
|
664 |
"lim_def" > "HOLLight.hollight.lim_def"
|
|
665 |
"lambda_def" > "HOLLight.hollight.lambda_def"
|
|
666 |
"iterate_def" > "HOLLight.hollight.iterate_def"
|
|
667 |
"istopology_def" > "HOLLight.hollight.istopology_def"
|
|
668 |
"ismet_def" > "HOLLight.hollight.ismet_def"
|
|
669 |
"is_nadd_def" > "HOLLight.hollight.is_nadd_def"
|
|
670 |
"is_nadd_0" > "HOLLight.hollight.is_nadd_0"
|
|
671 |
"is_int_def" > "HOLLight.hollight.is_int_def"
|
|
672 |
"int_sub_th" > "HOLLight.hollight.int_sub_th"
|
|
673 |
"int_sub_def" > "HOLLight.hollight.int_sub_def"
|
|
674 |
"int_pow_th" > "HOLLight.hollight.int_pow_th"
|
|
675 |
"int_pow_def" > "HOLLight.hollight.int_pow_def"
|
|
676 |
"int_of_num_th" > "HOLLight.hollight.int_of_num_th"
|
|
677 |
"int_of_num_def" > "HOLLight.hollight.int_of_num_def"
|
|
678 |
"int_neg_th" > "HOLLight.hollight.int_neg_th"
|
|
679 |
"int_neg_def" > "HOLLight.hollight.int_neg_def"
|
|
680 |
"int_mul_th" > "HOLLight.hollight.int_mul_th"
|
|
681 |
"int_mul_def" > "HOLLight.hollight.int_mul_def"
|
|
682 |
"int_min_th" > "HOLLight.hollight.int_min_th"
|
|
683 |
"int_min_def" > "HOLLight.hollight.int_min_def"
|
|
684 |
"int_max_th" > "HOLLight.hollight.int_max_th"
|
|
685 |
"int_max_def" > "HOLLight.hollight.int_max_def"
|
|
686 |
"int_lt_def" > "HOLLight.hollight.int_lt_def"
|
|
687 |
"int_le_def" > "HOLLight.hollight.int_le_def"
|
|
688 |
"int_gt_def" > "HOLLight.hollight.int_gt_def"
|
|
689 |
"int_ge_def" > "HOLLight.hollight.int_ge_def"
|
|
690 |
"int_eq" > "HOLLight.hollight.int.dest_int_inject"
|
|
691 |
"int_add_th" > "HOLLight.hollight.int_add_th"
|
|
692 |
"int_add_def" > "HOLLight.hollight.int_add_def"
|
|
693 |
"int_abs_th" > "HOLLight.hollight.int_abs_th"
|
|
694 |
"int_abs_def" > "HOLLight.hollight.int_abs_def"
|
|
695 |
"hreal_of_num_def" > "HOLLight.hollight.hreal_of_num_def"
|
|
696 |
"hreal_mul_def" > "HOLLight.hollight.hreal_mul_def"
|
|
697 |
"hreal_le_def" > "HOLLight.hollight.hreal_le_def"
|
|
698 |
"hreal_inv_def" > "HOLLight.hollight.hreal_inv_def"
|
|
699 |
"hreal_add_def" > "HOLLight.hollight.hreal_add_def"
|
|
700 |
"gauge_def" > "HOLLight.hollight.gauge_def"
|
|
701 |
"fstcart_def" > "HOLLight.hollight.fstcart_def"
|
|
702 |
"finite_index_def" > "HOLLight.hollight.finite_index_def"
|
|
703 |
"fine_def" > "HOLLight.hollight.fine_def"
|
|
704 |
"exp_def" > "HOLLight.hollight.exp_def"
|
|
705 |
"eqeq_def" > "HOLLight.hollight.eqeq_def"
|
|
706 |
"dsize_def" > "HOLLight.hollight.dsize_def"
|
|
707 |
"dotdot_def" > "HOLLight.hollight.dotdot_def"
|
|
708 |
"dorder_def" > "HOLLight.hollight.dorder_def"
|
|
709 |
"division_def" > "HOLLight.hollight.division_def"
|
|
710 |
"dist_def" > "HOLLight.hollight.dist_def"
|
|
711 |
"dimindex_def" > "HOLLight.hollight.dimindex_def"
|
|
712 |
"diffs_def" > "HOLLight.hollight.diffs_def"
|
|
713 |
"diffl_def" > "HOLLight.hollight.diffl_def"
|
|
714 |
"differentiable_def" > "HOLLight.hollight.differentiable_def"
|
|
715 |
"dest_int_rep" > "HOLLight.hollight.dest_int_rep"
|
|
716 |
"defint_def" > "HOLLight.hollight.defint_def"
|
|
717 |
"cth" > "HOLLight.hollight.cth"
|
|
718 |
"cos_def" > "HOLLight.hollight.cos_def"
|
|
719 |
"convergent_def" > "HOLLight.hollight.convergent_def"
|
|
720 |
"contl_def" > "HOLLight.hollight.contl_def"
|
|
721 |
"closed_def" > "HOLLight.hollight.closed_def"
|
|
722 |
"cauchy_def" > "HOLLight.hollight.cauchy_def"
|
|
723 |
"bounded_def" > "HOLLight.hollight.bounded_def"
|
|
724 |
"ball_def" > "HOLLight.hollight.ball_def"
|
|
725 |
"ax__3" > "HOL4Setup.INFINITY_AX"
|
|
726 |
"ax__2" > "Hilbert_Choice.tfl_some"
|
|
727 |
"ax__1" > "Presburger.fm_modd_pinf"
|
|
728 |
"atn_def" > "HOLLight.hollight.atn_def"
|
|
729 |
"asn_def" > "HOLLight.hollight.asn_def"
|
|
730 |
"admissible_def" > "HOLLight.hollight.admissible_def"
|
|
731 |
"acs_def" > "HOLLight.hollight.acs_def"
|
|
732 |
"_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
|
|
733 |
"_10314_def" > "HOLLight.hollight._10314_def"
|
|
734 |
"_10313_def" > "HOLLight.hollight._10313_def"
|
|
735 |
"_10312_def" > "HOLLight.hollight._10312_def"
|
|
736 |
"_10289_def" > "HOLLight.hollight._10289_def"
|
|
737 |
"_10288_def" > "HOLLight.hollight._10288_def"
|
|
738 |
"ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
|
|
739 |
"ZIP_def" > "HOLLight.hollight.ZIP_def"
|
|
740 |
"ZIP" > "HOLLight.hollight.ZIP"
|
|
741 |
"ZCONSTR_def" > "HOLLight.hollight.ZCONSTR_def"
|
|
742 |
"ZCONSTR_ZBOT" > "HOLLight.hollight.ZCONSTR_ZBOT"
|
|
743 |
"ZBOT_def" > "HOLLight.hollight.ZBOT_def"
|
|
744 |
"WLOG_LT" > "HOLLight.hollight.WLOG_LT"
|
|
745 |
"WLOG_LE" > "HOLLight.hollight.WLOG_LE"
|
|
746 |
"WF_num" > "HOLLight.hollight.WF_num"
|
|
747 |
"WF_def" > "HOLLight.hollight.WF_def"
|
|
748 |
"WF_UREC_WF" > "HOLLight.hollight.WF_UREC_WF"
|
|
749 |
"WF_UREC" > "HOLLight.hollight.WF_UREC"
|
|
750 |
"WF_SUBSET" > "HOLLight.hollight.WF_SUBSET"
|
|
751 |
"WF_REFL" > "HOLLight.hollight.WF_REFL"
|
|
752 |
"WF_REC_num" > "HOLLight.hollight.WF_REC_num"
|
|
753 |
"WF_REC_WF" > "HOLLight.hollight.WF_REC_WF"
|
|
754 |
"WF_REC_TAIL_GENERAL" > "HOLLight.hollight.WF_REC_TAIL_GENERAL"
|
|
755 |
"WF_REC_TAIL" > "HOLLight.hollight.WF_REC_TAIL"
|
|
756 |
"WF_REC_INVARIANT" > "HOLLight.hollight.WF_REC_INVARIANT"
|
|
757 |
"WF_REC_CASES" > "HOLLight.hollight.WF_REC_CASES"
|
|
758 |
"WF_REC" > "HOLLight.hollight.WF_REC"
|
|
759 |
"WF_POINTWISE" > "HOLLight.hollight.WF_POINTWISE"
|
|
760 |
"WF_MEASURE_GEN" > "HOLLight.hollight.WF_MEASURE_GEN"
|
|
761 |
"WF_MEASURE" > "HOLLight.hollight.WF_MEASURE"
|
|
762 |
"WF_LEX_DEPENDENT" > "HOLLight.hollight.WF_LEX_DEPENDENT"
|
|
763 |
"WF_LEX" > "HOLLight.hollight.WF_LEX"
|
|
764 |
"WF_IND" > "HOLLight.hollight.WF_IND"
|
|
765 |
"WF_FALSE" > "HOLLight.hollight.WF_FALSE"
|
|
766 |
"WF_EREC" > "HOLLight.hollight.WF_EREC"
|
|
767 |
"WF_EQ" > "HOLLight.hollight.WF_EQ"
|
|
768 |
"WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
|
|
769 |
"UNWIND_THM2" > "HOL.simp_thms_39"
|
|
770 |
"UNWIND_THM1" > "HOL.simp_thms_40"
|
|
771 |
"UNIV_def" > "HOLLight.hollight.UNIV_def"
|
|
772 |
"UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
|
|
773 |
"UNIV_NOT_EMPTY" > "HOLLight.hollight.UNIV_NOT_EMPTY"
|
|
774 |
"UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
|
|
775 |
"UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
|
|
776 |
"UNION_def" > "HOLLight.hollight.UNION_def"
|
|
777 |
"UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
|
|
778 |
"UNION_SUBSET" > "HOLLight.hollight.UNION_SUBSET"
|
|
779 |
"UNION_OVER_INTER" > "HOLLight.hollight.UNION_OVER_INTER"
|
|
780 |
"UNION_IDEMPOT" > "HOLLight.hollight.UNION_IDEMPOT"
|
|
781 |
"UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
|
|
782 |
"UNION_COMM" > "HOLLight.hollight.UNION_COMM"
|
|
783 |
"UNION_ASSOC" > "HOLLight.hollight.UNION_ASSOC"
|
|
784 |
"UNION_ACI" > "HOLLight.hollight.UNION_ACI"
|
|
785 |
"UNIONS_def" > "HOLLight.hollight.UNIONS_def"
|
|
786 |
"UNIONS_INSERT" > "HOLLight.hollight.UNIONS_INSERT"
|
|
787 |
"UNIONS_2" > "HOLLight.hollight.UNIONS_2"
|
|
788 |
"UNIONS_1" > "HOLLight.hollight.UNIONS_1"
|
|
789 |
"UNIONS_0" > "HOLLight.hollight.UNIONS_0"
|
|
790 |
"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
|
|
791 |
"TYDEF_topology" > "HOLLight.hollight.TYDEF_topology"
|
|
792 |
"TYDEF_sum" > "HOLLight.hollight.TYDEF_sum"
|
|
793 |
"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
|
|
794 |
"TYDEF_real" > "HOLLight.hollight.TYDEF_real"
|
|
795 |
"TYDEF_option" > "HOLLight.hollight.TYDEF_option"
|
|
796 |
"TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
|
|
797 |
"TYDEF_metric" > "HOLLight.hollight.TYDEF_metric"
|
|
798 |
"TYDEF_list" > "HOLLight.hollight.TYDEF_list"
|
|
799 |
"TYDEF_int" > "HOLLight.hollight.TYDEF_int"
|
|
800 |
"TYDEF_hreal" > "HOLLight.hollight.TYDEF_hreal"
|
|
801 |
"TYDEF_finite_sum" > "HOLLight.hollight.TYDEF_finite_sum"
|
|
802 |
"TYDEF_finite_image" > "HOLLight.hollight.TYDEF_finite_image"
|
|
803 |
"TYDEF_cart" > "HOLLight.hollight.TYDEF_cart"
|
|
804 |
"TYDEF_3" > "HOLLight.hollight.TYDEF_3"
|
|
805 |
"TYDEF_2" > "HOLLight.hollight.TYDEF_2"
|
|
806 |
"TWO" > "HOLLight.hollight.TWO"
|
|
807 |
"TRIV_OR_FORALL_THM" > "HOLLight.hollight.TRIV_OR_FORALL_THM"
|
|
808 |
"TRIV_FORALL_OR_THM" > "HOLLight.hollight.TRIV_FORALL_OR_THM"
|
|
809 |
"TRIV_FORALL_IMP_THM" > "HOLLight.hollight.TRIV_FORALL_IMP_THM"
|
|
810 |
"TRIV_EXISTS_IMP_THM" > "HOLLight.hollight.TRIV_EXISTS_IMP_THM"
|
|
811 |
"TRIV_EXISTS_AND_THM" > "HOLLight.hollight.TRIV_EXISTS_AND_THM"
|
|
812 |
"TRIV_AND_EXISTS_THM" > "HOLLight.hollight.TRIV_AND_EXISTS_THM"
|
|
813 |
"TREAL_OF_NUM_WELLDEF" > "HOLLight.hollight.TREAL_OF_NUM_WELLDEF"
|
|
814 |
"TREAL_OF_NUM_MUL" > "HOLLight.hollight.TREAL_OF_NUM_MUL"
|
|
815 |
"TREAL_OF_NUM_LE" > "HOLLight.hollight.TREAL_OF_NUM_LE"
|
|
816 |
"TREAL_OF_NUM_EQ" > "HOLLight.hollight.TREAL_OF_NUM_EQ"
|
|
817 |
"TREAL_OF_NUM_ADD" > "HOLLight.hollight.TREAL_OF_NUM_ADD"
|
|
818 |
"TREAL_NEG_WELLDEF" > "HOLLight.hollight.TREAL_NEG_WELLDEF"
|
|
819 |
"TREAL_MUL_WELLDEFR" > "HOLLight.hollight.TREAL_MUL_WELLDEFR"
|
|
820 |
"TREAL_MUL_WELLDEF" > "HOLLight.hollight.TREAL_MUL_WELLDEF"
|
|
821 |
"TREAL_MUL_SYM_EQ" > "HOLLight.hollight.TREAL_MUL_SYM_EQ"
|
|
822 |
"TREAL_MUL_SYM" > "HOLLight.hollight.TREAL_MUL_SYM"
|
|
823 |
"TREAL_MUL_LINV" > "HOLLight.hollight.TREAL_MUL_LINV"
|
|
824 |
"TREAL_MUL_LID" > "HOLLight.hollight.TREAL_MUL_LID"
|
|
825 |
"TREAL_MUL_ASSOC" > "HOLLight.hollight.TREAL_MUL_ASSOC"
|
|
826 |
"TREAL_LE_WELLDEF" > "HOLLight.hollight.TREAL_LE_WELLDEF"
|
|
827 |
"TREAL_LE_TRANS" > "HOLLight.hollight.TREAL_LE_TRANS"
|
|
828 |
"TREAL_LE_TOTAL" > "HOLLight.hollight.TREAL_LE_TOTAL"
|
|
829 |
"TREAL_LE_REFL" > "HOLLight.hollight.TREAL_LE_REFL"
|
|
830 |
"TREAL_LE_MUL" > "HOLLight.hollight.TREAL_LE_MUL"
|
|
831 |
"TREAL_LE_LADD_IMP" > "HOLLight.hollight.TREAL_LE_LADD_IMP"
|
|
832 |
"TREAL_LE_ANTISYM" > "HOLLight.hollight.TREAL_LE_ANTISYM"
|
|
833 |
"TREAL_INV_WELLDEF" > "HOLLight.hollight.TREAL_INV_WELLDEF"
|
|
834 |
"TREAL_INV_0" > "HOLLight.hollight.TREAL_INV_0"
|
|
835 |
"TREAL_EQ_TRANS" > "HOLLight.hollight.TREAL_EQ_TRANS"
|
|
836 |
"TREAL_EQ_SYM" > "HOLLight.hollight.TREAL_EQ_SYM"
|
|
837 |
"TREAL_EQ_REFL" > "HOLLight.hollight.TREAL_EQ_REFL"
|
|
838 |
"TREAL_EQ_IMP_LE" > "HOLLight.hollight.TREAL_EQ_IMP_LE"
|
|
839 |
"TREAL_EQ_AP" > "HOLLight.hollight.TREAL_EQ_AP"
|
|
840 |
"TREAL_ADD_WELLDEFR" > "HOLLight.hollight.TREAL_ADD_WELLDEFR"
|
|
841 |
"TREAL_ADD_WELLDEF" > "HOLLight.hollight.TREAL_ADD_WELLDEF"
|
|
842 |
"TREAL_ADD_SYM_EQ" > "HOLLight.hollight.TREAL_ADD_SYM_EQ"
|
|
843 |
"TREAL_ADD_SYM" > "HOLLight.hollight.TREAL_ADD_SYM"
|
|
844 |
"TREAL_ADD_LINV" > "HOLLight.hollight.TREAL_ADD_LINV"
|
|
845 |
"TREAL_ADD_LID" > "HOLLight.hollight.TREAL_ADD_LID"
|
|
846 |
"TREAL_ADD_LDISTRIB" > "HOLLight.hollight.TREAL_ADD_LDISTRIB"
|
|
847 |
"TREAL_ADD_ASSOC" > "HOLLight.hollight.TREAL_ADD_ASSOC"
|
|
848 |
"TOPOLOGY_UNION" > "HOLLight.hollight.TOPOLOGY_UNION"
|
|
849 |
"TOPOLOGY" > "HOLLight.hollight.TOPOLOGY"
|
|
850 |
"TL_def" > "HOLLight.hollight.TL_def"
|
|
851 |
"TERMDIFF_STRONG" > "HOLLight.hollight.TERMDIFF_STRONG"
|
|
852 |
"TERMDIFF_LEMMA5" > "HOLLight.hollight.TERMDIFF_LEMMA5"
|
|
853 |
"TERMDIFF_LEMMA4" > "HOLLight.hollight.TERMDIFF_LEMMA4"
|
|
854 |
"TERMDIFF_LEMMA3" > "HOLLight.hollight.TERMDIFF_LEMMA3"
|
|
855 |
"TERMDIFF_LEMMA2" > "HOLLight.hollight.TERMDIFF_LEMMA2"
|
|
856 |
"TERMDIFF_LEMMA1" > "HOLLight.hollight.TERMDIFF_LEMMA1"
|
|
857 |
"TERMDIFF_CONVERGES" > "HOLLight.hollight.TERMDIFF_CONVERGES"
|
|
858 |
"TERMDIFF" > "HOLLight.hollight.TERMDIFF"
|
|
859 |
"TAN_TOTAL_POS" > "HOLLight.hollight.TAN_TOTAL_POS"
|
|
860 |
"TAN_TOTAL_LEMMA" > "HOLLight.hollight.TAN_TOTAL_LEMMA"
|
|
861 |
"TAN_TOTAL" > "HOLLight.hollight.TAN_TOTAL"
|
|
862 |
"TAN_SEC" > "HOLLight.hollight.TAN_SEC"
|
|
863 |
"TAN_POS_PI2" > "HOLLight.hollight.TAN_POS_PI2"
|
|
864 |
"TAN_PI4" > "HOLLight.hollight.TAN_PI4"
|
|
865 |
"TAN_PI" > "HOLLight.hollight.TAN_PI"
|
|
866 |
"TAN_PERIODIC_PI" > "HOLLight.hollight.TAN_PERIODIC_PI"
|
|
867 |
"TAN_PERIODIC_NPI" > "HOLLight.hollight.TAN_PERIODIC_NPI"
|
|
868 |
"TAN_PERIODIC" > "HOLLight.hollight.TAN_PERIODIC"
|
|
869 |
"TAN_NPI" > "HOLLight.hollight.TAN_NPI"
|
|
870 |
"TAN_NEG" > "HOLLight.hollight.TAN_NEG"
|
|
871 |
"TAN_DOUBLE" > "HOLLight.hollight.TAN_DOUBLE"
|
|
872 |
"TAN_COT" > "HOLLight.hollight.TAN_COT"
|
|
873 |
"TAN_BOUND_PI2" > "HOLLight.hollight.TAN_BOUND_PI2"
|
|
874 |
"TAN_ATN" > "HOLLight.hollight.TAN_ATN"
|
|
875 |
"TAN_ADD" > "HOLLight.hollight.TAN_ADD"
|
|
876 |
"TAN_ABS_GE_X" > "HOLLight.hollight.TAN_ABS_GE_X"
|
|
877 |
"TAN_0" > "HOLLight.hollight.TAN_0"
|
|
878 |
"TAIL_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.TAIL_IMP_SUPERADMISSIBLE"
|
|
879 |
"SWAP_FORALL_THM" > "HOLLight.hollight.SWAP_FORALL_THM"
|
|
880 |
"SWAP_EXISTS_THM" > "HOLLight.hollight.SWAP_EXISTS_THM"
|
|
881 |
"SURJ_def" > "HOLLight.hollight.SURJ_def"
|
|
882 |
"SURJECTIVE_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_RIGHT_INVERSE"
|
|
883 |
"SURJECTIVE_ON_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_ON_RIGHT_INVERSE"
|
|
884 |
"SURJECTIVE_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
|
|
885 |
"SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
|
|
886 |
"SUPPORT_SUPPORT" > "HOLLight.hollight.SUPPORT_SUPPORT"
|
|
887 |
"SUPPORT_SUBSET" > "HOLLight.hollight.SUPPORT_SUBSET"
|
|
888 |
"SUPPORT_EMPTY" > "HOLLight.hollight.SUPPORT_EMPTY"
|
|
889 |
"SUPPORT_DELTA" > "HOLLight.hollight.SUPPORT_DELTA"
|
|
890 |
"SUPPORT_CLAUSES" > "HOLLight.hollight.SUPPORT_CLAUSES"
|
|
891 |
"SUPERADMISSIBLE_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
|
|
892 |
"SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
|
|
893 |
"SUM_ZERO" > "HOLLight.hollight.SUM_ZERO"
|
|
894 |
"SUM_UNIQ" > "HOLLight.hollight.SUM_UNIQ"
|
|
895 |
"SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
|
|
896 |
"SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
|
|
897 |
"SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
|
|
898 |
"SUM_UNION" > "HOLLight.hollight.SUM_UNION"
|
|
899 |
"SUM_TWO" > "HOLLight.hollight.SUM_TWO"
|
|
900 |
"SUM_TRIV_NUMSEG" > "HOLLight.hollight.SUM_TRIV_NUMSEG"
|
|
901 |
"SUM_SWAP_NUMSEG" > "HOLLight.hollight.SUM_SWAP_NUMSEG"
|
|
902 |
"SUM_SWAP" > "HOLLight.hollight.SUM_SWAP"
|
|
903 |
"SUM_SUPPORT" > "HOLLight.hollight.SUM_SUPPORT"
|
|
904 |
"SUM_SUPERSET" > "HOLLight.hollight.SUM_SUPERSET"
|
|
905 |
"SUM_SUM_RESTRICT" > "HOLLight.hollight.SUM_SUM_RESTRICT"
|
|
906 |
"SUM_SUMMABLE" > "HOLLight.hollight.SUM_SUMMABLE"
|
|
907 |
"SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
|
|
908 |
"SUM_SUBST" > "HOLLight.hollight.SUM_SUBST"
|
|
909 |
"SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
|
|
910 |
"SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
|
|
911 |
"SUM_SUB" > "HOLLight.hollight.SUM_SUB"
|
|
912 |
"SUM_SPLIT" > "HOLLight.hollight.SUM_SPLIT"
|
|
913 |
"SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
|
|
914 |
"SUM_SING" > "HOLLight.hollight.SUM_SING"
|
|
915 |
"SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
|
|
916 |
"SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
|
|
917 |
"SUM_REINDEX" > "HOLLight.hollight.SUM_REINDEX"
|
|
918 |
"SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
|
|
919 |
"SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
|
|
920 |
"SUM_POS_GEN" > "HOLLight.hollight.SUM_POS_GEN"
|
|
921 |
"SUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_POS_EQ_0_NUMSEG"
|
|
922 |
"SUM_POS_EQ_0" > "HOLLight.hollight.SUM_POS_EQ_0"
|
|
923 |
"SUM_POS_BOUND" > "HOLLight.hollight.SUM_POS_BOUND"
|
|
924 |
"SUM_POS" > "HOLLight.hollight.SUM_POS"
|
|
925 |
"SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
|
|
926 |
"SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
|
|
927 |
"SUM_NSUB" > "HOLLight.hollight.SUM_NSUB"
|
|
928 |
"SUM_NEG_NUMSEG" > "HOLLight.hollight.SUM_NEG_NUMSEG"
|
|
929 |
"SUM_NEG" > "HOLLight.hollight.SUM_NEG"
|
|
930 |
"SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
|
|
931 |
"SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
|
|
932 |
"SUM_MORETERMS_EQ" > "HOLLight.hollight.SUM_MORETERMS_EQ"
|
|
933 |
"SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
|
|
934 |
"SUM_LT" > "HOLLight.hollight.SUM_LT"
|
|
935 |
"SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
|
|
936 |
"SUM_LE" > "HOLLight.hollight.SUM_LE"
|
|
937 |
"SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
|
|
938 |
"SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
|
|
939 |
"SUM_HORNER" > "HOLLight.hollight.SUM_HORNER"
|
|
940 |
"SUM_GROUP" > "HOLLight.hollight.SUM_GROUP"
|
|
941 |
"SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
|
|
942 |
"SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
|
|
943 |
"SUM_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_EQ_0_NUMSEG"
|
|
944 |
"SUM_EQ_0" > "HOLLight.hollight.SUM_EQ_0"
|
|
945 |
"SUM_EQ" > "HOLLight.hollight.SUM_EQ"
|
|
946 |
"SUM_DIFFERENCES_EQ" > "HOLLight.hollight.SUM_DIFFERENCES_EQ"
|
|
947 |
"SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
|
|
948 |
"SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
|
|
949 |
"SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
|
|
950 |
"SUM_CONST" > "HOLLight.hollight.SUM_CONST"
|
|
951 |
"SUM_CMUL_NUMSEG" > "HOLLight.hollight.SUM_CMUL_NUMSEG"
|
|
952 |
"SUM_CMUL" > "HOLLight.hollight.SUM_CMUL"
|
|
953 |
"SUM_CLAUSES_RIGHT" > "HOLLight.hollight.SUM_CLAUSES_RIGHT"
|
|
954 |
"SUM_CLAUSES_NUMSEG" > "HOLLight.hollight.SUM_CLAUSES_NUMSEG"
|
|
955 |
"SUM_CLAUSES_LEFT" > "HOLLight.hollight.SUM_CLAUSES_LEFT"
|
|
956 |
"SUM_CLAUSES" > "HOLLight.hollight.SUM_CLAUSES"
|
|
957 |
"SUM_CANCEL" > "HOLLight.hollight.SUM_CANCEL"
|
|
958 |
"SUM_BOUND_LT_GEN" > "HOLLight.hollight.SUM_BOUND_LT_GEN"
|
|
959 |
"SUM_BOUND_LT_ALL" > "HOLLight.hollight.SUM_BOUND_LT_ALL"
|
|
960 |
"SUM_BOUND_LT" > "HOLLight.hollight.SUM_BOUND_LT"
|
|
961 |
"SUM_BOUND_GEN" > "HOLLight.hollight.SUM_BOUND_GEN"
|
|
962 |
"SUM_BOUND" > "HOLLight.hollight.SUM_BOUND"
|
|
963 |
"SUM_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
|
|
964 |
"SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
|
|
965 |
"SUM_ADD" > "HOLLight.hollight.SUM_ADD"
|
|
966 |
"SUM_ABS_NUMSEG" > "HOLLight.hollight.SUM_ABS_NUMSEG"
|
|
967 |
"SUM_ABS_LE" > "HOLLight.hollight.SUM_ABS_LE"
|
|
968 |
"SUM_ABS_BOUND" > "HOLLight.hollight.SUM_ABS_BOUND"
|
|
969 |
"SUM_ABS" > "HOLLight.hollight.SUM_ABS"
|
|
970 |
"SUM_2" > "HOLLight.hollight.SUM_2"
|
|
971 |
"SUM_1" > "HOLLight.hollight.SUM_1"
|
|
972 |
"SUM_0" > "HOLLight.hollight.SUM_0"
|
|
973 |
"SUMMABLE_SUM" > "HOLLight.hollight.SUMMABLE_SUM"
|
|
974 |
"SUC_SUB1" > "HOLLight.hollight.SUC_SUB1"
|
|
975 |
"SUC_INJ" > "Nat.nat.simps_3"
|
|
976 |
"SUB_SUC" > "Nat.diff_Suc_Suc"
|
|
977 |
"SUB_SUB" > "HOLLight.hollight.SUB_SUB"
|
|
978 |
"SUB_REFL" > "Nat.diff_self_eq_0"
|
|
979 |
"SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
|
|
980 |
"SUB_OLD" > "HOLLight.hollight.SUB_OLD"
|
|
981 |
"SUB_EQ_0" > "HOLLight.hollight.SUB_EQ_0"
|
|
982 |
"SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
|
|
983 |
"SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
|
|
984 |
"SUB_ADD_LCANCEL" > "Nat.diff_cancel"
|
|
985 |
"SUB_ADD" > "HOLLight.hollight.SUB_ADD"
|
|
986 |
"SUB_0" > "HOLLight.hollight.SUB_0"
|
|
987 |
"SUBSET_def" > "HOLLight.hollight.SUBSET_def"
|
|
988 |
"SUBSET_UNIV" > "HOLLight.hollight.SUBSET_UNIV"
|
|
989 |
"SUBSET_UNION_ABSORPTION" > "HOLLight.hollight.SUBSET_UNION_ABSORPTION"
|
|
990 |
"SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
|
|
991 |
"SUBSET_TRANS" > "HOLLight.hollight.SUBSET_TRANS"
|
|
992 |
"SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
|
|
993 |
"SUBSET_REFL" > "HOLLight.hollight.SUBSET_REFL"
|
|
994 |
"SUBSET_PSUBSET_TRANS" > "HOLLight.hollight.SUBSET_PSUBSET_TRANS"
|
|
995 |
"SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
|
|
996 |
"SUBSET_INTER_ABSORPTION" > "HOLLight.hollight.SUBSET_INTER_ABSORPTION"
|
|
997 |
"SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
|
|
998 |
"SUBSET_INSERT" > "HOLLight.hollight.SUBSET_INSERT"
|
|
999 |
"SUBSET_IMAGE" > "HOLLight.hollight.SUBSET_IMAGE"
|
|
1000 |
"SUBSET_EMPTY" > "HOLLight.hollight.SUBSET_EMPTY"
|
|
1001 |
"SUBSET_DIFF" > "HOLLight.hollight.SUBSET_DIFF"
|
|
1002 |
"SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
|
|
1003 |
"SUBSET_ANTISYM" > "HOLLight.hollight.SUBSET_ANTISYM"
|
|
1004 |
"SUBSETA_TRANS" > "HOLLight.hollight.SUBSETA_TRANS"
|
|
1005 |
"SUBSETA_REFL" > "HOLLight.hollight.SUBSETA_REFL"
|
|
1006 |
"SUBSETA_ANTISYM" > "HOLLight.hollight.SUBSETA_ANTISYM"
|
|
1007 |
"SUBSEQ_SUC" > "HOLLight.hollight.SUBSEQ_SUC"
|
|
1008 |
"STRADDLE_LEMMA" > "HOLLight.hollight.STRADDLE_LEMMA"
|
|
1009 |
"SQRT_POW_2" > "HOLLight.hollight.SQRT_POW_2"
|
|
1010 |
"SQRT_POW2" > "HOLLight.hollight.SQRT_POW2"
|
|
1011 |
"SQRT_POS_UNIQ" > "HOLLight.hollight.SQRT_POS_UNIQ"
|
|
1012 |
"SQRT_POS_LT" > "HOLLight.hollight.SQRT_POS_LT"
|
|
1013 |
"SQRT_POS_LE" > "HOLLight.hollight.SQRT_POS_LE"
|
|
1014 |
"SQRT_MUL" > "HOLLight.hollight.SQRT_MUL"
|
|
1015 |
"SQRT_MONO_LT_EQ" > "HOLLight.hollight.SQRT_MONO_LT_EQ"
|
|
1016 |
"SQRT_MONO_LT" > "HOLLight.hollight.SQRT_MONO_LT"
|
|
1017 |
"SQRT_MONO_LE_EQ" > "HOLLight.hollight.SQRT_MONO_LE_EQ"
|
|
1018 |
"SQRT_MONO_LE" > "HOLLight.hollight.SQRT_MONO_LE"
|
|
1019 |
"SQRT_INV" > "HOLLight.hollight.SQRT_INV"
|
|
1020 |
"SQRT_INJ" > "HOLLight.hollight.SQRT_INJ"
|
|
1021 |
"SQRT_EVEN_POW2" > "HOLLight.hollight.SQRT_EVEN_POW2"
|
|
1022 |
"SQRT_EQ_0" > "HOLLight.hollight.SQRT_EQ_0"
|
|
1023 |
"SQRT_DIV" > "HOLLight.hollight.SQRT_DIV"
|
|
1024 |
"SQRT_1" > "HOLLight.hollight.SQRT_1"
|
|
1025 |
"SQRT_0" > "HOLLight.hollight.SQRT_0"
|
|
1026 |
"SOME_def" > "HOLLight.hollight.SOME_def"
|
|
1027 |
"SNDCART_PASTECART" > "HOLLight.hollight.SNDCART_PASTECART"
|
|
1028 |
"SND" > "Product_Type.snd_conv"
|
|
1029 |
"SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
|
|
1030 |
"SIN_ZERO_PI" > "HOLLight.hollight.SIN_ZERO_PI"
|
|
1031 |
"SIN_ZERO_LEMMA" > "HOLLight.hollight.SIN_ZERO_LEMMA"
|
|
1032 |
"SIN_ZERO" > "HOLLight.hollight.SIN_ZERO"
|
|
1033 |
"SIN_TOTAL" > "HOLLight.hollight.SIN_TOTAL"
|
|
1034 |
"SIN_POS_PI_LE" > "HOLLight.hollight.SIN_POS_PI_LE"
|
|
1035 |
"SIN_POS_PI2" > "HOLLight.hollight.SIN_POS_PI2"
|
|
1036 |
"SIN_POS_PI" > "HOLLight.hollight.SIN_POS_PI"
|
|
1037 |
"SIN_POS" > "HOLLight.hollight.SIN_POS"
|
|
1038 |
"SIN_PI2" > "HOLLight.hollight.SIN_PI2"
|
|
1039 |
"SIN_PI" > "HOLLight.hollight.SIN_PI"
|
|
1040 |
"SIN_PERIODIC_PI" > "HOLLight.hollight.SIN_PERIODIC_PI"
|
|
1041 |
"SIN_PERIODIC" > "HOLLight.hollight.SIN_PERIODIC"
|
|
1042 |
"SIN_PAIRED" > "HOLLight.hollight.SIN_PAIRED"
|
|
1043 |
"SIN_NPI" > "HOLLight.hollight.SIN_NPI"
|
|
1044 |
"SIN_NEGLEMMA" > "HOLLight.hollight.SIN_NEGLEMMA"
|
|
1045 |
"SIN_NEG" > "HOLLight.hollight.SIN_NEG"
|
|
1046 |
"SIN_FDIFF" > "HOLLight.hollight.SIN_FDIFF"
|
|
1047 |
"SIN_DOUBLE" > "HOLLight.hollight.SIN_DOUBLE"
|
|
1048 |
"SIN_COS_SQRT" > "HOLLight.hollight.SIN_COS_SQRT"
|
|
1049 |
"SIN_COS_NEG" > "HOLLight.hollight.SIN_COS_NEG"
|
|
1050 |
"SIN_COS_ADD" > "HOLLight.hollight.SIN_COS_ADD"
|
|
1051 |
"SIN_COS" > "HOLLight.hollight.SIN_COS"
|
|
1052 |
"SIN_CONVERGES" > "HOLLight.hollight.SIN_CONVERGES"
|
|
1053 |
"SIN_CIRCLE" > "HOLLight.hollight.SIN_CIRCLE"
|
|
1054 |
"SIN_BOUNDS" > "HOLLight.hollight.SIN_BOUNDS"
|
|
1055 |
"SIN_BOUND" > "HOLLight.hollight.SIN_BOUND"
|
|
1056 |
"SIN_ASN" > "HOLLight.hollight.SIN_ASN"
|
|
1057 |
"SIN_ADD" > "HOLLight.hollight.SIN_ADD"
|
|
1058 |
"SIN_ACS_NZ" > "HOLLight.hollight.SIN_ACS_NZ"
|
|
1059 |
"SIN_0" > "HOLLight.hollight.SIN_0"
|
|
1060 |
"SING_def" > "HOLLight.hollight.SING_def"
|
|
1061 |
"SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
|
|
1062 |
"SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
|
|
1063 |
"SET_OF_LIST_OF_SET" > "HOLLight.hollight.SET_OF_LIST_OF_SET"
|
|
1064 |
"SET_OF_LIST_APPEND" > "HOLLight.hollight.SET_OF_LIST_APPEND"
|
|
1065 |
"SET_CASES" > "HOLLight.hollight.SET_CASES"
|
|
1066 |
"SETSPEC_def" > "HOLLight.hollight.SETSPEC_def"
|
|
1067 |
"SETOK_LE_LT" > "HOLLight.hollight.SETOK_LE_LT"
|
|
1068 |
"SER_ZERO" > "HOLLight.hollight.SER_ZERO"
|
|
1069 |
"SER_UNIQ" > "HOLLight.hollight.SER_UNIQ"
|
|
1070 |
"SER_SUB" > "HOLLight.hollight.SER_SUB"
|
|
1071 |
"SER_RATIO" > "HOLLight.hollight.SER_RATIO"
|
|
1072 |
"SER_POS_LT_PAIR" > "HOLLight.hollight.SER_POS_LT_PAIR"
|
|
1073 |
"SER_POS_LT" > "HOLLight.hollight.SER_POS_LT"
|
|
1074 |
"SER_POS_LE" > "HOLLight.hollight.SER_POS_LE"
|
|
1075 |
"SER_PAIR" > "HOLLight.hollight.SER_PAIR"
|
|
1076 |
"SER_OFFSET_REV" > "HOLLight.hollight.SER_OFFSET_REV"
|
|
1077 |
"SER_OFFSET" > "HOLLight.hollight.SER_OFFSET"
|
|
1078 |
"SER_NEG" > "HOLLight.hollight.SER_NEG"
|
|
1079 |
"SER_LE2" > "HOLLight.hollight.SER_LE2"
|
|
1080 |
"SER_LE" > "HOLLight.hollight.SER_LE"
|
|
1081 |
"SER_GROUP" > "HOLLight.hollight.SER_GROUP"
|
|
1082 |
"SER_COMPARA_UNIFORM_WEAK" > "HOLLight.hollight.SER_COMPARA_UNIFORM_WEAK"
|
|
1083 |
"SER_COMPARA_UNIFORM" > "HOLLight.hollight.SER_COMPARA_UNIFORM"
|
|
1084 |
"SER_COMPARA" > "HOLLight.hollight.SER_COMPARA"
|
|
1085 |
"SER_COMPAR" > "HOLLight.hollight.SER_COMPAR"
|
|
1086 |
"SER_CMUL" > "HOLLight.hollight.SER_CMUL"
|
|
1087 |
"SER_CDIV" > "HOLLight.hollight.SER_CDIV"
|
|
1088 |
"SER_CAUCHY" > "HOLLight.hollight.SER_CAUCHY"
|
|
1089 |
"SER_ADD" > "HOLLight.hollight.SER_ADD"
|
|
1090 |
"SER_ACONV" > "HOLLight.hollight.SER_ACONV"
|
|
1091 |
"SER_ABS" > "HOLLight.hollight.SER_ABS"
|
|
1092 |
"SER_0" > "HOLLight.hollight.SER_0"
|
|
1093 |
"SEQ_UNIQ" > "HOLLight.hollight.SEQ_UNIQ"
|
|
1094 |
"SEQ_TRUNCATION" > "HOLLight.hollight.SEQ_TRUNCATION"
|
|
1095 |
"SEQ_TRANSFORM" > "HOLLight.hollight.SEQ_TRANSFORM"
|
|
1096 |
"SEQ_TENDS" > "HOLLight.hollight.SEQ_TENDS"
|
|
1097 |
"SEQ_SUM" > "HOLLight.hollight.SEQ_SUM"
|
|
1098 |
"SEQ_SUC" > "HOLLight.hollight.SEQ_SUC"
|
|
1099 |
"SEQ_SUBLE" > "HOLLight.hollight.SEQ_SUBLE"
|
|
1100 |
"SEQ_SUB" > "HOLLight.hollight.SEQ_SUB"
|
|
1101 |
"SEQ_SBOUNDED" > "HOLLight.hollight.SEQ_SBOUNDED"
|
|
1102 |
"SEQ_POWER_ABS" > "HOLLight.hollight.SEQ_POWER_ABS"
|
|
1103 |
"SEQ_POWER" > "HOLLight.hollight.SEQ_POWER"
|
|
1104 |
"SEQ_NULL" > "HOLLight.hollight.SEQ_NULL"
|
|
1105 |
"SEQ_NPOW" > "HOLLight.hollight.SEQ_NPOW"
|
|
1106 |
"SEQ_NEG_CONV" > "HOLLight.hollight.SEQ_NEG_CONV"
|
|
1107 |
"SEQ_NEG_BOUNDED" > "HOLLight.hollight.SEQ_NEG_BOUNDED"
|
|
1108 |
"SEQ_NEG" > "HOLLight.hollight.SEQ_NEG"
|
|
1109 |
"SEQ_MUL" > "HOLLight.hollight.SEQ_MUL"
|
|
1110 |
"SEQ_MONOSUB" > "HOLLight.hollight.SEQ_MONOSUB"
|
|
1111 |
"SEQ_LIM" > "HOLLight.hollight.SEQ_LIM"
|
|
1112 |
"SEQ_LE_0" > "HOLLight.hollight.SEQ_LE_0"
|
|
1113 |
"SEQ_LE" > "HOLLight.hollight.SEQ_LE"
|
|
1114 |
"SEQ_INV0" > "HOLLight.hollight.SEQ_INV0"
|
|
1115 |
"SEQ_INV" > "HOLLight.hollight.SEQ_INV"
|
|
1116 |
"SEQ_ICONV" > "HOLLight.hollight.SEQ_ICONV"
|
|
1117 |
"SEQ_DIV" > "HOLLight.hollight.SEQ_DIV"
|
|
1118 |
"SEQ_DIRECT" > "HOLLight.hollight.SEQ_DIRECT"
|
|
1119 |
"SEQ_CONT_UNIFORM" > "HOLLight.hollight.SEQ_CONT_UNIFORM"
|
|
1120 |
"SEQ_CONST" > "HOLLight.hollight.SEQ_CONST"
|
|
1121 |
"SEQ_CBOUNDED" > "HOLLight.hollight.SEQ_CBOUNDED"
|
|
1122 |
"SEQ_CAUCHY" > "HOLLight.hollight.SEQ_CAUCHY"
|
|
1123 |
"SEQ_BOUNDED_2" > "HOLLight.hollight.SEQ_BOUNDED_2"
|
|
1124 |
"SEQ_BOUNDED" > "HOLLight.hollight.SEQ_BOUNDED"
|
|
1125 |
"SEQ_BCONV" > "HOLLight.hollight.SEQ_BCONV"
|
|
1126 |
"SEQ_ADD" > "HOLLight.hollight.SEQ_ADD"
|
|
1127 |
"SEQ_ABS_IMP" > "HOLLight.hollight.SEQ_ABS_IMP"
|
|
1128 |
"SEQ_ABS" > "HOLLight.hollight.SEQ_ABS"
|
|
1129 |
"SEQ" > "HOLLight.hollight.SEQ"
|
|
1130 |
"SEMIRING_PTHS" > "HOLLight.hollight.SEMIRING_PTHS"
|
|
1131 |
"SELECT_UNIQUE" > "HOLLight.hollight.SELECT_UNIQUE"
|
|
1132 |
"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
|
|
1133 |
"SELECT_LEMMA" > "Hilbert_Choice.some_sym_eq_trivial"
|
|
1134 |
"ROOT_POW_POS" > "HOLLight.hollight.ROOT_POW_POS"
|
|
1135 |
"ROOT_POS_UNIQ" > "HOLLight.hollight.ROOT_POS_UNIQ"
|
|
1136 |
"ROOT_POS_POSITIVE" > "HOLLight.hollight.ROOT_POS_POSITIVE"
|
|
1137 |
"ROOT_MUL" > "HOLLight.hollight.ROOT_MUL"
|
|
1138 |
"ROOT_MONO_LT_EQ" > "HOLLight.hollight.ROOT_MONO_LT_EQ"
|
|
1139 |
"ROOT_MONO_LT" > "HOLLight.hollight.ROOT_MONO_LT"
|
|
1140 |
"ROOT_MONO_LE_EQ" > "HOLLight.hollight.ROOT_MONO_LE_EQ"
|
|
1141 |
"ROOT_MONO_LE" > "HOLLight.hollight.ROOT_MONO_LE"
|
|
1142 |
"ROOT_LT_LEMMA" > "HOLLight.hollight.ROOT_LT_LEMMA"
|
|
1143 |
"ROOT_LN" > "HOLLight.hollight.ROOT_LN"
|
|
1144 |
"ROOT_INV" > "HOLLight.hollight.ROOT_INV"
|
|
1145 |
"ROOT_INJ" > "HOLLight.hollight.ROOT_INJ"
|
|
1146 |
"ROOT_DIV" > "HOLLight.hollight.ROOT_DIV"
|
|
1147 |
"ROOT_1" > "HOLLight.hollight.ROOT_1"
|
|
1148 |
"ROOT_0" > "HOLLight.hollight.ROOT_0"
|
|
1149 |
"ROLLE" > "HOLLight.hollight.ROLLE"
|
|
1150 |
"RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
|
|
1151 |
"RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
|
|
1152 |
"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
|
|
1153 |
"RIGHT_OR_DISTRIB" > "HOL.conj_disj_distribR"
|
|
1154 |
"RIGHT_IMP_FORALL_THM" > "HOL.all_simps_6"
|
|
1155 |
"RIGHT_IMP_EXISTS_THM" > "HOL.ex_simps_6"
|
|
1156 |
"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
|
|
1157 |
"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
|
|
1158 |
"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
|
|
1159 |
"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
|
|
1160 |
"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
|
|
1161 |
"RIGHT_AND_EXISTS_THM" > "HOL.ex_simps_2"
|
|
1162 |
"RIGHT_ADD_DISTRIB" > "Nat.nat_distrib_1"
|
|
1163 |
"REVERSE_def" > "HOLLight.hollight.REVERSE_def"
|
|
1164 |
"REVERSE_REVERSE" > "HOLLight.hollight.REVERSE_REVERSE"
|
|
1165 |
"REVERSE_APPEND" > "HOLLight.hollight.REVERSE_APPEND"
|
|
1166 |
"REST_def" > "HOLLight.hollight.REST_def"
|
|
1167 |
"REP_ABS_PAIR" > "HOLLightCompat.REP_ABS_PAIR"
|
|
1168 |
"REPLICATE_def" > "HOLLight.hollight.REPLICATE_def"
|
|
1169 |
"REFL_CLAUSE" > "HOL.simp_thms_6"
|
|
1170 |
"RECURSION_CASEWISE_PAIRWISE" > "HOLLight.hollight.RECURSION_CASEWISE_PAIRWISE"
|
|
1171 |
"RECURSION_CASEWISE" > "HOLLight.hollight.RECURSION_CASEWISE"
|
|
1172 |
"REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
|
|
1173 |
"REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
|
|
1174 |
"REAL_SUP_UBOUND_LE" > "HOLLight.hollight.REAL_SUP_UBOUND_LE"
|
|
1175 |
"REAL_SUP_UBOUND" > "HOLLight.hollight.REAL_SUP_UBOUND"
|
|
1176 |
"REAL_SUP_LE" > "HOLLight.hollight.REAL_SUP_LE"
|
|
1177 |
"REAL_SUP_EXISTS" > "HOLLight.hollight.REAL_SUP_EXISTS"
|
|
1178 |
"REAL_SUP" > "HOLLight.hollight.REAL_SUP"
|
|
1179 |
"REAL_SUMSQ" > "HOLLight.hollight.REAL_SUMSQ"
|
|
1180 |
"REAL_SUB_TRIANGLE" > "HOLLight.hollight.REAL_SUB_TRIANGLE"
|
|
1181 |
"REAL_SUB_SUB2" > "HOLLight.hollight.REAL_SUB_SUB2"
|
|
1182 |
"REAL_SUB_SUB" > "HOLLight.hollight.REAL_SUB_SUB"
|
|
1183 |
"REAL_SUB_RZERO" > "HOLLight.hollight.REAL_SUB_RZERO"
|
|
1184 |
"REAL_SUB_RNEG" > "HOLLight.hollight.REAL_SUB_RNEG"
|
|
1185 |
"REAL_SUB_REFL" > "HOLLight.hollight.REAL_SUB_REFL"
|
|
1186 |
"REAL_SUB_RDISTRIB" > "HOLLight.hollight.REAL_SUB_RDISTRIB"
|
|
1187 |
"REAL_SUB_NEG2" > "HOLLight.hollight.REAL_SUB_NEG2"
|
|
1188 |
"REAL_SUB_LZERO" > "HOLLight.hollight.REAL_SUB_LZERO"
|
|
1189 |
"REAL_SUB_LT" > "HOLLight.hollight.REAL_SUB_LT"
|
|
1190 |
"REAL_SUB_LNEG" > "HOLLight.hollight.REAL_SUB_LNEG"
|
|
1191 |
"REAL_SUB_LE" > "HOLLight.hollight.REAL_SUB_LE"
|
|
1192 |
"REAL_SUB_LDISTRIB" > "HOLLight.hollight.REAL_SUB_LDISTRIB"
|
|
1193 |
"REAL_SUB_INV2" > "HOLLight.hollight.REAL_SUB_INV2"
|
|
1194 |
"REAL_SUB_INV" > "HOLLight.hollight.REAL_SUB_INV"
|
|
1195 |
"REAL_SUB_ADD2" > "HOLLight.hollight.REAL_SUB_ADD2"
|
|
1196 |
"REAL_SUB_ADD" > "HOLLight.hollight.REAL_SUB_ADD"
|
|
1197 |
"REAL_SUB_ABS" > "HOLLight.hollight.REAL_SUB_ABS"
|
|
1198 |
"REAL_SUB_0" > "HOLLight.hollight.REAL_SUB_0"
|
|
1199 |
"REAL_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
|
|
1200 |
"REAL_RINV_UNIQ" > "HOLLight.hollight.REAL_RINV_UNIQ"
|
|
1201 |
"REAL_RDISTRIB" > "HOLLight.hollight.REAL_RDISTRIB"
|
|
1202 |
"REAL_POW_SUB" > "HOLLight.hollight.REAL_POW_SUB"
|
|
1203 |
"REAL_POW_POW" > "HOLLight.hollight.REAL_POW_POW"
|
|
1204 |
"REAL_POW_ONE" > "HOLLight.hollight.REAL_POW_ONE"
|
|
1205 |
"REAL_POW_NZ" > "HOLLight.hollight.REAL_POW_NZ"
|
|
1206 |
"REAL_POW_NEG" > "HOLLight.hollight.REAL_POW_NEG"
|
|
1207 |
"REAL_POW_MUL" > "HOLLight.hollight.REAL_POW_MUL"
|
|
1208 |
"REAL_POW_MONO_LT" > "HOLLight.hollight.REAL_POW_MONO_LT"
|
|
1209 |
"REAL_POW_MONO" > "HOLLight.hollight.REAL_POW_MONO"
|
|
1210 |
"REAL_POW_LT2" > "HOLLight.hollight.REAL_POW_LT2"
|
|
1211 |
"REAL_POW_LT" > "HOLLight.hollight.REAL_POW_LT"
|
|
1212 |
"REAL_POW_LE_1" > "HOLLight.hollight.REAL_POW_LE_1"
|
|
1213 |
"REAL_POW_LE2" > "HOLLight.hollight.REAL_POW_LE2"
|
|
1214 |
"REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
|
|
1215 |
"REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
|
|
1216 |
"REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
|
|
1217 |
"REAL_POW_DIV" > "HOLLight.hollight.REAL_POW_DIV"
|
|
1218 |
"REAL_POW_ADD" > "HOLLight.hollight.REAL_POW_ADD"
|
|
1219 |
"REAL_POW_2" > "HOLLight.hollight.REAL_POW_2"
|
|
1220 |
"REAL_POW_1_LE" > "HOLLight.hollight.REAL_POW_1_LE"
|
|
1221 |
"REAL_POW_1" > "HOLLight.hollight.REAL_POW_1"
|
|
1222 |
"REAL_POW2_ABS" > "HOLLight.hollight.REAL_POW2_ABS"
|
|
1223 |
"REAL_POS_NZ" > "HOLLight.hollight.REAL_POS_NZ"
|
|
1224 |
"REAL_POSSQ" > "HOLLight.hollight.REAL_POSSQ"
|
|
1225 |
"REAL_POS" > "HOLLight.hollight.REAL_POS"
|
|
1226 |
"REAL_POLY_NEG_CLAUSES" > "HOLLight.hollight.REAL_POLY_NEG_CLAUSES"
|
|
1227 |
"REAL_POLY_CLAUSES" > "HOLLight.hollight.REAL_POLY_CLAUSES"
|
|
1228 |
"REAL_OF_NUM_SUM_NUMSEG" > "HOLLight.hollight.REAL_OF_NUM_SUM_NUMSEG"
|
|
1229 |
"REAL_OF_NUM_SUM" > "HOLLight.hollight.REAL_OF_NUM_SUM"
|
|
1230 |
"REAL_OF_NUM_SUC" > "HOLLight.hollight.REAL_OF_NUM_SUC"
|
|
1231 |
"REAL_OF_NUM_SUB" > "HOLLight.hollight.REAL_OF_NUM_SUB"
|
|
1232 |
"REAL_OF_NUM_POW" > "HOLLight.hollight.REAL_OF_NUM_POW"
|
|
1233 |
"REAL_OF_NUM_LT" > "HOLLight.hollight.REAL_OF_NUM_LT"
|
|
1234 |
"REAL_OF_NUM_GT" > "HOLLight.hollight.REAL_OF_NUM_GT"
|
|
1235 |
"REAL_OF_NUM_GE" > "HOLLight.hollight.REAL_OF_NUM_GE"
|
|
1236 |
"REAL_NZ_IMP_LT" > "HOLLight.hollight.REAL_NZ_IMP_LT"
|
|
1237 |
"REAL_NOT_LT" > "HOLLight.hollight.REAL_NOT_LT"
|
|
1238 |
"REAL_NOT_LE" > "HOLLight.hollight.real_lt_def"
|
|
1239 |
"REAL_NOT_EQ" > "HOLLight.hollight.REAL_NOT_EQ"
|
|
1240 |
"REAL_NEG_SUB" > "HOLLight.hollight.REAL_NEG_SUB"
|
|
1241 |
"REAL_NEG_RMUL" > "HOLLight.hollight.REAL_NEG_RMUL"
|
|
1242 |
"REAL_NEG_NEG" > "HOLLight.hollight.REAL_NEG_NEG"
|
|
1243 |
"REAL_NEG_MUL2" > "HOLLight.hollight.REAL_NEG_MUL2"
|
|
1244 |
"REAL_NEG_MINUS1" > "HOLLight.hollight.REAL_NEG_MINUS1"
|
|
1245 |
"REAL_NEG_LT0" > "HOLLight.hollight.REAL_NEG_LT0"
|
|
1246 |
"REAL_NEG_LMUL" > "HOLLight.hollight.REAL_NEG_LMUL"
|
|
1247 |
"REAL_NEG_LE0" > "HOLLight.hollight.REAL_NEG_LE0"
|
|
1248 |
"REAL_NEG_INV" > "HOLLight.hollight.REAL_NEG_INV"
|
|
1249 |
"REAL_NEG_GT0" > "HOLLight.hollight.REAL_NEG_GT0"
|
|
1250 |
"REAL_NEG_GE0" > "HOLLight.hollight.REAL_NEG_GE0"
|
|
1251 |
"REAL_NEG_EQ_0" > "HOLLight.hollight.REAL_NEG_EQ_0"
|
|
1252 |
"REAL_NEG_EQ0" > "HOLLight.hollight.REAL_NEG_EQ0"
|
|
1253 |
"REAL_NEG_EQ" > "HOLLight.hollight.REAL_NEG_EQ"
|
|
1254 |
"REAL_NEG_ADD" > "HOLLight.hollight.REAL_NEG_ADD"
|
|
1255 |
"REAL_NEG_0" > "HOLLight.hollight.REAL_NEG_0"
|
|
1256 |
"REAL_NEGNEG" > "HOLLight.hollight.REAL_NEGNEG"
|
|
1257 |
"REAL_MUL_RZERO" > "HOLLight.hollight.REAL_MUL_RZERO"
|
|
1258 |
"REAL_MUL_RNEG" > "HOLLight.hollight.REAL_MUL_RNEG"
|
|
1259 |
"REAL_MUL_RINV_UNIQ" > "HOLLight.hollight.REAL_MUL_RINV_UNIQ"
|
|
1260 |
"REAL_MUL_RINV" > "HOLLight.hollight.REAL_MUL_RINV"
|
|
1261 |
"REAL_MUL_RID" > "HOLLight.hollight.REAL_MUL_RID"
|
|
1262 |
"REAL_MUL_LZERO" > "HOLLight.hollight.REAL_MUL_LZERO"
|
|
1263 |
"REAL_MUL_LNEG" > "HOLLight.hollight.REAL_MUL_LNEG"
|
|
1264 |
"REAL_MUL_LINV_UNIQ" > "HOLLight.hollight.REAL_MUL_LINV_UNIQ"
|
|
1265 |
"REAL_MUL_AC" > "HOLLight.hollight.REAL_MUL_AC"
|
|
1266 |
"REAL_MUL_2" > "HOLLight.hollight.REAL_MUL_2"
|
|
1267 |
"REAL_MUL" > "HOLLight.hollight.REAL_MUL"
|
|
1268 |
"REAL_MIN_SYM" > "HOLLight.hollight.REAL_MIN_SYM"
|
|
1269 |
"REAL_MIN_MIN" > "HOLLight.hollight.REAL_MIN_MIN"
|
|
1270 |
"REAL_MIN_MAX" > "HOLLight.hollight.REAL_MIN_MAX"
|
|
1271 |
"REAL_MIN_LT" > "HOLLight.hollight.REAL_MIN_LT"
|
|
1272 |
"REAL_MIN_LE" > "HOLLight.hollight.REAL_MIN_LE"
|
|
1273 |
"REAL_MIN_ASSOC" > "HOLLight.hollight.REAL_MIN_ASSOC"
|
|
1274 |
"REAL_MIN_ACI" > "HOLLight.hollight.REAL_MIN_ACI"
|
|
1275 |
"REAL_MIDDLE2" > "HOLLight.hollight.REAL_MIDDLE2"
|
|
1276 |
"REAL_MIDDLE1" > "HOLLight.hollight.REAL_MIDDLE1"
|
|
1277 |
"REAL_MEAN" > "HOLLight.hollight.REAL_MEAN"
|
|
1278 |
"REAL_MAX_SYM" > "HOLLight.hollight.REAL_MAX_SYM"
|
|
1279 |
"REAL_MAX_MIN" > "HOLLight.hollight.REAL_MAX_MIN"
|
|
1280 |
"REAL_MAX_MAX" > "HOLLight.hollight.REAL_MAX_MAX"
|
|
1281 |
"REAL_MAX_LT" > "HOLLight.hollight.REAL_MAX_LT"
|
|
1282 |
"REAL_MAX_LE" > "HOLLight.hollight.REAL_MAX_LE"
|
|
1283 |
"REAL_MAX_ASSOC" > "HOLLight.hollight.REAL_MAX_ASSOC"
|
|
1284 |
"REAL_MAX_ACI" > "HOLLight.hollight.REAL_MAX_ACI"
|
|
1285 |
"REAL_LT_TRANS" > "HOLLight.hollight.REAL_LT_TRANS"
|
|
1286 |
"REAL_LT_TOTAL" > "HOLLight.hollight.REAL_LT_TOTAL"
|
|
1287 |
"REAL_LT_SUB_RADD" > "HOLLight.hollight.REAL_LT_SUB_RADD"
|
|
1288 |
"REAL_LT_SUB_LADD" > "HOLLight.hollight.REAL_LT_SUB_LADD"
|
|
1289 |
"REAL_LT_SQUARE" > "HOLLight.hollight.REAL_LT_SQUARE"
|
|
1290 |
"REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
|
|
1291 |
"REAL_LT_RMUL_IMP" > "HOLLight.hollight.REAL_LT_RMUL_IMP"
|
|
1292 |
"REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
|
|
1293 |
"REAL_LT_RMUL_0" > "HOLLight.hollight.REAL_LT_RMUL_0"
|
|
1294 |
"REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
|
|
1295 |
"REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
|
|
1296 |
"REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
|
|
1297 |
"REAL_LT_RDIV_0" > "HOLLight.hollight.REAL_LT_RDIV_0"
|
|
1298 |
"REAL_LT_RDIV" > "HOLLight.hollight.REAL_LT_RDIV"
|
|
1299 |
"REAL_LT_RCANCEL_IMP" > "HOLLight.hollight.REAL_LT_RCANCEL_IMP"
|
|
1300 |
"REAL_LT_RADD" > "HOLLight.hollight.REAL_LT_RADD"
|
|
1301 |
"REAL_LT_POW2" > "HOLLight.hollight.REAL_LT_POW2"
|
|
1302 |
"REAL_LT_NZ" > "HOLLight.hollight.REAL_LT_NZ"
|
|
1303 |
"REAL_LT_NEGTOTAL" > "HOLLight.hollight.REAL_LT_NEGTOTAL"
|
|
1304 |
"REAL_LT_NEG2" > "HOLLight.hollight.REAL_LT_NEG2"
|
|
1305 |
"REAL_LT_NEG" > "HOLLight.hollight.REAL_LT_NEG"
|
|
1306 |
"REAL_LT_MULTIPLE" > "HOLLight.hollight.REAL_LT_MULTIPLE"
|
|
1307 |
"REAL_LT_MUL2_ALT" > "HOLLight.hollight.REAL_LT_MUL2_ALT"
|
|
1308 |
"REAL_LT_MUL2" > "HOLLight.hollight.REAL_LT_MUL2"
|
|
1309 |
"REAL_LT_MUL" > "HOLLight.hollight.REAL_LT_MUL"
|
|
1310 |
"REAL_LT_MIN" > "HOLLight.hollight.REAL_LT_MIN"
|
|
1311 |
"REAL_LT_MAX" > "HOLLight.hollight.REAL_LT_MAX"
|
|
1312 |
"REAL_LT_LNEG" > "HOLLight.hollight.REAL_LT_LNEG"
|
|
1313 |
"REAL_LT_LMUL_IMP" > "HOLLight.hollight.REAL_LT_LMUL_IMP"
|
|
1314 |
"REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
|
|
1315 |
"REAL_LT_LMUL_0" > "HOLLight.hollight.REAL_LT_LMUL_0"
|
|
1316 |
"REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
|
|
1317 |
"REAL_LT_LE" > "HOLLight.hollight.REAL_LT_LE"
|
|
1318 |
"REAL_LT_LDIV_EQ" > "HOLLight.hollight.REAL_LT_LDIV_EQ"
|
|
1319 |
"REAL_LT_LCANCEL_IMP" > "HOLLight.hollight.REAL_LT_LCANCEL_IMP"
|
|
1320 |
"REAL_LT_LADD_IMP" > "HOLLight.hollight.REAL_LT_LADD_IMP"
|
|
1321 |
"REAL_LT_LADD" > "HOLLight.hollight.REAL_LT_LADD"
|
|
1322 |
"REAL_LT_INV_EQ" > "HOLLight.hollight.REAL_LT_INV_EQ"
|
|
1323 |
"REAL_LT_INV2" > "HOLLight.hollight.REAL_LT_INV2"
|
|
1324 |
"REAL_LT_INV" > "HOLLight.hollight.REAL_LT_INV"
|
|
1325 |
"REAL_LT_IMP_NZ" > "HOLLight.hollight.REAL_LT_IMP_NZ"
|
|
1326 |
"REAL_LT_IMP_NE" > "HOLLight.hollight.REAL_LT_IMP_NE"
|
|
1327 |
"REAL_LT_IMP_LE" > "HOLLight.hollight.REAL_LT_IMP_LE"
|
|
1328 |
"REAL_LT_HALF2" > "HOLLight.hollight.REAL_LT_HALF2"
|
|
1329 |
"REAL_LT_HALF1" > "HOLLight.hollight.REAL_LT_HALF1"
|
|
1330 |
"REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
|
|
1331 |
"REAL_LT_FRACTION_0" > "HOLLight.hollight.REAL_LT_FRACTION_0"
|
|
1332 |
"REAL_LT_FRACTION" > "HOLLight.hollight.REAL_LT_FRACTION"
|
|
1333 |
"REAL_LT_DIV2_EQ" > "HOLLight.hollight.REAL_LT_DIV2_EQ"
|
|
1334 |
"REAL_LT_DIV" > "HOLLight.hollight.REAL_LT_DIV"
|
|
1335 |
"REAL_LT_ANTISYM" > "HOLLight.hollight.REAL_LT_ANTISYM"
|
|
1336 |
"REAL_LT_ADD_SUB" > "HOLLight.hollight.REAL_LT_ADD_SUB"
|
|
1337 |
"REAL_LT_ADDR" > "HOLLight.hollight.REAL_LT_ADDR"
|
|
1338 |
"REAL_LT_ADDNEG2" > "HOLLight.hollight.REAL_LT_ADDNEG2"
|
|
1339 |
"REAL_LT_ADDNEG" > "HOLLight.hollight.REAL_LT_ADDNEG"
|
|
1340 |
"REAL_LT_ADDL" > "HOLLight.hollight.REAL_LT_ADDL"
|
|
1341 |
"REAL_LT_ADD2" > "HOLLight.hollight.REAL_LT_ADD2"
|
|
1342 |
"REAL_LT_ADD1" > "HOLLight.hollight.REAL_LT_ADD1"
|
|
1343 |
"REAL_LT_ADD" > "HOLLight.hollight.REAL_LT_ADD"
|
|
1344 |
"REAL_LT_1" > "HOLLight.hollight.REAL_LT_1"
|
|
1345 |
"REAL_LT_01" > "HOLLight.hollight.REAL_LT_01"
|
|
1346 |
"REAL_LTE_TRANS" > "HOLLight.hollight.REAL_LTE_TRANS"
|
|
1347 |
"REAL_LTE_TOTAL" > "HOLLight.hollight.REAL_LTE_TOTAL"
|
|
1348 |
"REAL_LTE_ANTISYM" > "HOLLight.hollight.REAL_LTE_ANTISYM"
|
|
1349 |
"REAL_LTE_ADD2" > "HOLLight.hollight.REAL_LTE_ADD2"
|
|
1350 |
"REAL_LTE_ADD" > "HOLLight.hollight.REAL_LTE_ADD"
|
|
1351 |
"REAL_LT1_POW2" > "HOLLight.hollight.REAL_LT1_POW2"
|
|
1352 |
"REAL_LT" > "HOLLight.hollight.REAL_LT"
|
|
1353 |
"REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
|
|
1354 |
"REAL_LINV_UNIQ" > "HOLLight.hollight.REAL_LINV_UNIQ"
|
|
1355 |
"REAL_LE_TRANS" > "HOLLight.hollight.REAL_LE_TRANS"
|
|
1356 |
"REAL_LE_TOTAL" > "HOLLight.hollight.REAL_LE_TOTAL"
|
|
1357 |
"REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
|
|
1358 |
"REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
|
|
1359 |
"REAL_LE_SQUARE_POW" > "HOLLight.hollight.REAL_LE_SQUARE_POW"
|
|
1360 |
"REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
|
|
1361 |
"REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
|
|
1362 |
"REAL_LE_RSQRT" > "HOLLight.hollight.REAL_LE_RSQRT"
|
|
1363 |
"REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
|
|
1364 |
"REAL_LE_RMUL_IMP" > "HOLLight.hollight.REAL_LE_RMUL_IMP"
|
|
1365 |
"REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
|
|
1366 |
"REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
|
|
1367 |
"REAL_LE_REFL" > "HOLLight.hollight.REAL_LE_REFL"
|
|
1368 |
"REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
|
|
1369 |
"REAL_LE_RDIV" > "HOLLight.hollight.REAL_LE_RDIV"
|
|
1370 |
"REAL_LE_RCANCEL_IMP" > "HOLLight.hollight.REAL_LE_RCANCEL_IMP"
|
|
1371 |
"REAL_LE_RADD" > "HOLLight.hollight.REAL_LE_RADD"
|
|
1372 |
"REAL_LE_POW_2" > "HOLLight.hollight.REAL_LE_POW_2"
|
|
1373 |
"REAL_LE_POW2" > "HOLLight.hollight.REAL_LE_POW2"
|
|
1374 |
"REAL_LE_NEGTOTAL" > "HOLLight.hollight.REAL_LE_NEGTOTAL"
|
|
1375 |
"REAL_LE_NEGR" > "HOLLight.hollight.REAL_LE_NEGR"
|
|
1376 |
"REAL_LE_NEGL" > "HOLLight.hollight.REAL_LE_NEGL"
|
|
1377 |
"REAL_LE_NEG2" > "HOLLight.hollight.REAL_LE_NEG2"
|
|
1378 |
"REAL_LE_NEG" > "HOLLight.hollight.REAL_LE_NEG"
|
|
1379 |
"REAL_LE_MUL2V" > "HOLLight.hollight.REAL_LE_MUL2V"
|
|
1380 |
"REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
|
|
1381 |
"REAL_LE_MUL" > "HOLLight.hollight.REAL_LE_MUL"
|
|
1382 |
"REAL_LE_MIN" > "HOLLight.hollight.REAL_LE_MIN"
|
|
1383 |
"REAL_LE_MAX" > "HOLLight.hollight.REAL_LE_MAX"
|
|
1384 |
"REAL_LE_LT" > "HOLLight.hollight.REAL_LE_LT"
|
|
1385 |
"REAL_LE_LSQRT" > "HOLLight.hollight.REAL_LE_LSQRT"
|
|
1386 |
"REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
|
|
1387 |
"REAL_LE_LMUL_LOCAL" > "HOLLight.hollight.REAL_LE_LMUL_LOCAL"
|
|
1388 |
"REAL_LE_LMUL_IMP" > "HOLLight.hollight.REAL_LE_LMUL_IMP"
|
|
1389 |
"REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
|
|
1390 |
"REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
|
|
1391 |
"REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
|
|
1392 |
"REAL_LE_LDIV" > "HOLLight.hollight.REAL_LE_LDIV"
|
|
1393 |
"REAL_LE_LCANCEL_IMP" > "HOLLight.hollight.REAL_LE_LCANCEL_IMP"
|
|
1394 |
"REAL_LE_LADD" > "HOLLight.hollight.REAL_LE_LADD"
|
|
1395 |
"REAL_LE_INV_EQ" > "HOLLight.hollight.REAL_LE_INV_EQ"
|
|
1396 |
"REAL_LE_INV2" > "HOLLight.hollight.REAL_LE_INV2"
|
|
1397 |
"REAL_LE_INV" > "HOLLight.hollight.REAL_LE_INV"
|
|
1398 |
"REAL_LE_DOUBLE" > "HOLLight.hollight.REAL_LE_DOUBLE"
|
|
1399 |
"REAL_LE_DIV2_EQ" > "HOLLight.hollight.REAL_LE_DIV2_EQ"
|
|
1400 |
"REAL_LE_DIV" > "HOLLight.hollight.REAL_LE_DIV"
|
|
1401 |
"REAL_LE_ANTISYM" > "HOLLight.hollight.REAL_LE_ANTISYM"
|
|
1402 |
"REAL_LE_ADDR" > "HOLLight.hollight.REAL_LE_ADDR"
|
|
1403 |
"REAL_LE_ADDL" > "HOLLight.hollight.REAL_LE_ADDL"
|
|
1404 |
"REAL_LE_ADD2" > "HOLLight.hollight.REAL_LE_ADD2"
|
|
1405 |
"REAL_LE_ADD" > "HOLLight.hollight.REAL_LE_ADD"
|
|
1406 |
"REAL_LE_01" > "HOLLight.hollight.REAL_LE_01"
|
|
1407 |
"REAL_LET_TRANS" > "HOLLight.hollight.REAL_LET_TRANS"
|
|
1408 |
"REAL_LET_TOTAL" > "HOLLight.hollight.REAL_LET_TOTAL"
|
|
1409 |
"REAL_LET_ANTISYM" > "HOLLight.hollight.REAL_LET_ANTISYM"
|
|
1410 |
"REAL_LET_ADD2" > "HOLLight.hollight.REAL_LET_ADD2"
|
|
1411 |
"REAL_LET_ADD" > "HOLLight.hollight.REAL_LET_ADD"
|
|
1412 |
"REAL_LE1_POW2" > "HOLLight.hollight.REAL_LE1_POW2"
|
|
1413 |
"REAL_LE" > "HOLLight.hollight.REAL_LE"
|
|
1414 |
"REAL_INV_POS" > "HOLLight.hollight.REAL_INV_POS"
|
|
1415 |
"REAL_INV_NZ" > "HOLLight.hollight.REAL_INV_NZ"
|
|
1416 |
"REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
|
|
1417 |
"REAL_INV_MUL_WEAK" > "HOLLight.hollight.REAL_INV_MUL_WEAK"
|
|
1418 |
"REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
|
|
1419 |
"REAL_INV_LT1" > "HOLLight.hollight.REAL_INV_LT1"
|
|
1420 |
"REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
|
|
1421 |
"REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
|
|
1422 |
"REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
|
|
1423 |
"REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
|
|
1424 |
"REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
|
|
1425 |
"REAL_INV_1OVER" > "HOLLight.hollight.REAL_INV_1OVER"
|
|
1426 |
"REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
|
|
1427 |
"REAL_INVINV" > "HOLLight.hollight.REAL_INVINV"
|
|
1428 |
"REAL_INV1" > "HOLLight.hollight.REAL_INV1"
|
|
1429 |
"REAL_INJ" > "HOLLight.hollight.REAL_INJ"
|
|
1430 |
"REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
|
|
1431 |
"REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
|
|
1432 |
"REAL_HALF_DOUBLE" > "HOLLight.hollight.REAL_HALF_DOUBLE"
|
|
1433 |
"REAL_FACT_NZ" > "HOLLight.hollight.REAL_FACT_NZ"
|
|
1434 |
"REAL_EXP_TOTAL_LEMMA" > "HOLLight.hollight.REAL_EXP_TOTAL_LEMMA"
|
|
1435 |
"REAL_EXP_TOTAL" > "HOLLight.hollight.REAL_EXP_TOTAL"
|
|
1436 |
"REAL_EXP_SUB" > "HOLLight.hollight.REAL_EXP_SUB"
|
|
1437 |
"REAL_EXP_POS_LT" > "HOLLight.hollight.REAL_EXP_POS_LT"
|
|
1438 |
"REAL_EXP_POS_LE" > "HOLLight.hollight.REAL_EXP_POS_LE"
|
|
1439 |
"REAL_EXP_NZ" > "HOLLight.hollight.REAL_EXP_NZ"
|
|
1440 |
"REAL_EXP_NEG_MUL2" > "HOLLight.hollight.REAL_EXP_NEG_MUL2"
|
|
1441 |
"REAL_EXP_NEG_MUL" > "HOLLight.hollight.REAL_EXP_NEG_MUL"
|
|
1442 |
"REAL_EXP_NEG" > "HOLLight.hollight.REAL_EXP_NEG"
|
|
1443 |
"REAL_EXP_N" > "HOLLight.hollight.REAL_EXP_N"
|
|
1444 |
"REAL_EXP_MONO_LT" > "HOLLight.hollight.REAL_EXP_MONO_LT"
|
|
1445 |
"REAL_EXP_MONO_LE" > "HOLLight.hollight.REAL_EXP_MONO_LE"
|
|
1446 |
"REAL_EXP_MONO_IMP" > "HOLLight.hollight.REAL_EXP_MONO_IMP"
|
|
1447 |
"REAL_EXP_LT_1" > "HOLLight.hollight.REAL_EXP_LT_1"
|
|
1448 |
"REAL_EXP_LN" > "HOLLight.hollight.REAL_EXP_LN"
|
|
1449 |
"REAL_EXP_LE_X" > "HOLLight.hollight.REAL_EXP_LE_X"
|
|
1450 |
"REAL_EXP_INJ" > "HOLLight.hollight.REAL_EXP_INJ"
|
|
1451 |
"REAL_EXP_FDIFF" > "HOLLight.hollight.REAL_EXP_FDIFF"
|
|
1452 |
"REAL_EXP_CONVERGES" > "HOLLight.hollight.REAL_EXP_CONVERGES"
|
|
1453 |
"REAL_EXP_BOUND_LEMMA" > "HOLLight.hollight.REAL_EXP_BOUND_LEMMA"
|
|
1454 |
"REAL_EXP_ADD_MUL" > "HOLLight.hollight.REAL_EXP_ADD_MUL"
|
|
1455 |
"REAL_EXP_ADD" > "HOLLight.hollight.REAL_EXP_ADD"
|
|
1456 |
"REAL_EXP_0" > "HOLLight.hollight.REAL_EXP_0"
|
|
1457 |
"REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
|
|
1458 |
"REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
|
|
1459 |
"REAL_EQ_RMUL_IMP" > "HOLLight.hollight.REAL_EQ_RMUL_IMP"
|
|
1460 |
"REAL_EQ_RMUL" > "HOLLight.hollight.REAL_EQ_RMUL"
|
|
1461 |
"REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
|
|
1462 |
"REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
|
|
1463 |
"REAL_EQ_RADD" > "HOLLight.hollight.REAL_EQ_RADD"
|
|
1464 |
"REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
|
|
1465 |
"REAL_EQ_NEG" > "HOLLight.hollight.REAL_EQ_NEG"
|
|
1466 |
"REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
|
|
1467 |
"REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
|
|
1468 |
"REAL_EQ_LMUL_IMP" > "HOLLight.hollight.REAL_EQ_LMUL_IMP"
|
|
1469 |
"REAL_EQ_LMUL2" > "HOLLight.hollight.REAL_EQ_LMUL2"
|
|
1470 |
"REAL_EQ_LMUL" > "HOLLight.hollight.REAL_EQ_LMUL"
|
|
1471 |
"REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
|
|
1472 |
"REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
|
|
1473 |
"REAL_EQ_LADD" > "HOLLight.hollight.REAL_EQ_LADD"
|
|
1474 |
"REAL_EQ_IMP_LE" > "HOLLight.hollight.REAL_EQ_IMP_LE"
|
|
1475 |
"REAL_EQ_ADD_RCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL_0"
|
|
1476 |
"REAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL"
|
|
1477 |
"REAL_EQ_ADD_LCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL_0"
|
|
1478 |
"REAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL"
|
|
1479 |
"REAL_ENTIRE" > "HOLLight.hollight.REAL_ENTIRE"
|
|
1480 |
"REAL_DOWN2" > "HOLLight.hollight.REAL_DOWN2"
|
|
1481 |
"REAL_DOWN" > "HOLLight.hollight.REAL_DOWN"
|
|
1482 |
"REAL_DOUBLE" > "HOLLight.hollight.REAL_DOUBLE"
|
|
1483 |
"REAL_DIV_SQRT" > "HOLLight.hollight.REAL_DIV_SQRT"
|
|
1484 |
"REAL_DIV_RMUL" > "HOLLight.hollight.REAL_DIV_RMUL"
|
|
1485 |
"REAL_DIV_REFL" > "HOLLight.hollight.REAL_DIV_REFL"
|
|
1486 |
"REAL_DIV_POW2_ALT" > "HOLLight.hollight.REAL_DIV_POW2_ALT"
|
|
1487 |
"REAL_DIV_POW2" > "HOLLight.hollight.REAL_DIV_POW2"
|
|
1488 |
"REAL_DIV_MUL2" > "HOLLight.hollight.REAL_DIV_MUL2"
|
|
1489 |
"REAL_DIV_LZERO" > "HOLLight.hollight.REAL_DIV_LZERO"
|
|
1490 |
"REAL_DIV_LMUL" > "HOLLight.hollight.REAL_DIV_LMUL"
|
|
1491 |
"REAL_DIV_1" > "HOLLight.hollight.REAL_DIV_1"
|
|
1492 |
"REAL_DIFFSQ" > "HOLLight.hollight.REAL_DIFFSQ"
|
|
1493 |
"REAL_COMPLETE_SOMEPOS" > "HOLLight.hollight.REAL_COMPLETE_SOMEPOS"
|
|
1494 |
"REAL_COMPLETE" > "HOLLight.hollight.REAL_COMPLETE"
|
|
1495 |
"REAL_ATN_POWSER_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_SUMMABLE"
|
|
1496 |
"REAL_ATN_POWSER_DIFFS_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_SUMMABLE"
|
|
1497 |
"REAL_ATN_POWSER_DIFFS_SUM" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_SUM"
|
|
1498 |
"REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE"
|
|
1499 |
"REAL_ATN_POWSER_DIFFL" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFL"
|
|
1500 |
"REAL_ATN_POWSER" > "HOLLight.hollight.REAL_ATN_POWSER"
|
|
1501 |
"REAL_ARCH_SIMPLE" > "HOLLight.hollight.REAL_ARCH_SIMPLE"
|
|
1502 |
"REAL_ARCH_LEAST" > "HOLLight.hollight.REAL_ARCH_LEAST"
|
|
1503 |
"REAL_ARCH" > "HOLLight.hollight.REAL_ARCH"
|
|
1504 |
"REAL_ADD_SUB2" > "HOLLight.hollight.REAL_ADD_SUB2"
|
|
1505 |
"REAL_ADD_SUB" > "HOLLight.hollight.REAL_ADD_SUB"
|
|
1506 |
"REAL_ADD_RINV" > "HOLLight.hollight.REAL_ADD_RINV"
|
|
1507 |
"REAL_ADD_RID_UNIQ" > "HOLLight.hollight.REAL_ADD_RID_UNIQ"
|
|
1508 |
"REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
|
|
1509 |
"REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
|
|
1510 |
"REAL_ADD_LID_UNIQ" > "HOLLight.hollight.REAL_ADD_LID_UNIQ"
|
|
1511 |
"REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
|
|
1512 |
"REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
|
|
1513 |
"REAL_ADD" > "HOLLight.hollight.REAL_ADD"
|
|
1514 |
"REAL_ABS_ZERO" > "HOLLight.hollight.REAL_ABS_ZERO"
|
|
1515 |
"REAL_ABS_TRIANGLE_LT" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LT"
|
|
1516 |
"REAL_ABS_TRIANGLE_LE" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LE"
|
|
1517 |
"REAL_ABS_TRIANGLE" > "HOLLight.hollight.REAL_ABS_TRIANGLE"
|
|
1518 |
"REAL_ABS_SUB_ABS" > "HOLLight.hollight.REAL_ABS_SUB_ABS"
|
|
1519 |
"REAL_ABS_SUB" > "HOLLight.hollight.REAL_ABS_SUB"
|
|
1520 |
"REAL_ABS_STILLNZ" > "HOLLight.hollight.REAL_ABS_STILLNZ"
|
|
1521 |
"REAL_ABS_SIGN2" > "HOLLight.hollight.REAL_ABS_SIGN2"
|
|
1522 |
"REAL_ABS_SIGN" > "HOLLight.hollight.REAL_ABS_SIGN"
|
|
1523 |
"REAL_ABS_REFL" > "HOLLight.hollight.REAL_ABS_REFL"
|
|
1524 |
"REAL_ABS_POW" > "HOLLight.hollight.REAL_ABS_POW"
|
|
1525 |
"REAL_ABS_POS" > "HOLLight.hollight.REAL_ABS_POS"
|
|
1526 |
"REAL_ABS_NZ" > "HOLLight.hollight.REAL_ABS_NZ"
|
|
1527 |
"REAL_ABS_NUM" > "HOLLight.hollight.REAL_ABS_NUM"
|
|
1528 |
"REAL_ABS_NEG" > "HOLLight.hollight.REAL_ABS_NEG"
|
|
1529 |
"REAL_ABS_MUL" > "HOLLight.hollight.REAL_ABS_MUL"
|
|
1530 |
"REAL_ABS_LE" > "HOLLight.hollight.REAL_ABS_LE"
|
|
1531 |
"REAL_ABS_INV" > "HOLLight.hollight.REAL_ABS_INV"
|
|
1532 |
"REAL_ABS_DIV" > "HOLLight.hollight.REAL_ABS_DIV"
|
|
1533 |
"REAL_ABS_CIRCLE" > "HOLLight.hollight.REAL_ABS_CIRCLE"
|
|
1534 |
"REAL_ABS_CASES" > "HOLLight.hollight.REAL_ABS_CASES"
|
|
1535 |
"REAL_ABS_BOUNDS" > "HOLLight.hollight.REAL_ABS_BOUNDS"
|
|
1536 |
"REAL_ABS_BOUND" > "HOLLight.hollight.REAL_ABS_BOUND"
|
|
1537 |
"REAL_ABS_BETWEEN2" > "HOLLight.hollight.REAL_ABS_BETWEEN2"
|
|
1538 |
"REAL_ABS_BETWEEN1" > "HOLLight.hollight.REAL_ABS_BETWEEN1"
|
|
1539 |
"REAL_ABS_BETWEEN" > "HOLLight.hollight.REAL_ABS_BETWEEN"
|
|
1540 |
"REAL_ABS_ABS" > "HOLLight.hollight.REAL_ABS_ABS"
|
|
1541 |
"REAL_ABS_1" > "HOLLight.hollight.REAL_ABS_1"
|
|
1542 |
"REAL_ABS_0" > "HOLLight.hollight.REAL_ABS_0"
|
|
1543 |
"REAL" > "HOLLight.hollight.REAL"
|
|
1544 |
"RAT_LEMMA5" > "HOLLight.hollight.RAT_LEMMA5"
|
|
1545 |
"RAT_LEMMA4" > "HOLLight.hollight.RAT_LEMMA4"
|
|
1546 |
"RAT_LEMMA3" > "HOLLight.hollight.RAT_LEMMA3"
|
|
1547 |
"RAT_LEMMA2" > "HOLLight.hollight.RAT_LEMMA2"
|
|
1548 |
"RAT_LEMMA1" > "HOLLight.hollight.RAT_LEMMA1"
|
|
1549 |
"PSUM_SUM_NUMSEG" > "HOLLight.hollight.PSUM_SUM_NUMSEG"
|
|
1550 |
"PSUM_SUM" > "HOLLight.hollight.PSUM_SUM"
|
|
1551 |
"PSUBSET_def" > "HOLLight.hollight.PSUBSET_def"
|
|
1552 |
"PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
|
|
1553 |
"PSUBSET_TRANS" > "HOLLight.hollight.PSUBSET_TRANS"
|
|
1554 |
"PSUBSET_SUBSET_TRANS" > "HOLLight.hollight.PSUBSET_SUBSET_TRANS"
|
|
1555 |
"PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
|
|
1556 |
"PSUBSET_IRREFL" > "HOLLight.hollight.PSUBSET_IRREFL"
|
|
1557 |
"PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
|
|
1558 |
"PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
|
|
1559 |
"POW_ZERO_EQ" > "HOLLight.hollight.POW_ZERO_EQ"
|
|
1560 |
"POW_ZERO" > "HOLLight.hollight.POW_ZERO"
|
|
1561 |
"POW_ROOT_POS" > "HOLLight.hollight.POW_ROOT_POS"
|
|
1562 |
"POW_POS_LT" > "HOLLight.hollight.POW_POS_LT"
|
|
1563 |
"POW_POS" > "HOLLight.hollight.POW_POS"
|
|
1564 |
"POW_PLUS1" > "HOLLight.hollight.POW_PLUS1"
|
|
1565 |
"POW_NZ" > "HOLLight.hollight.POW_NZ"
|
|
1566 |
"POW_MUL" > "HOLLight.hollight.POW_MUL"
|
|
1567 |
"POW_MINUS1" > "HOLLight.hollight.POW_MINUS1"
|
|
1568 |
"POW_M1" > "HOLLight.hollight.POW_M1"
|
|
1569 |
"POW_LT" > "HOLLight.hollight.POW_LT"
|
|
1570 |
"POW_LE" > "HOLLight.hollight.POW_LE"
|
|
1571 |
"POW_INV" > "HOLLight.hollight.POW_INV"
|
|
1572 |
"POW_EQ" > "HOLLight.hollight.POW_EQ"
|
|
1573 |
"POW_ADD" > "HOLLight.hollight.POW_ADD"
|
|
1574 |
"POW_ABS" > "HOLLight.hollight.POW_ABS"
|
|
1575 |
"POW_2_SQRT_ABS" > "HOLLight.hollight.POW_2_SQRT_ABS"
|
|
1576 |
"POW_2_SQRT" > "HOLLight.hollight.POW_2_SQRT"
|
|
1577 |
"POW_2_LT" > "HOLLight.hollight.POW_2_LT"
|
|
1578 |
"POW_2_LE1" > "HOLLight.hollight.POW_2_LE1"
|
|
1579 |
"POW_2" > "HOLLight.hollight.POW_2"
|
|
1580 |
"POW_1" > "HOLLight.hollight.POW_1"
|
|
1581 |
"POW_0" > "HOLLight.hollight.POW_0"
|
|
1582 |
"POWSER_LIMIT_0_STRONG" > "HOLLight.hollight.POWSER_LIMIT_0_STRONG"
|
|
1583 |
"POWSER_LIMIT_0" > "HOLLight.hollight.POWSER_LIMIT_0"
|
|
1584 |
"POWSER_INSIDEA" > "HOLLight.hollight.POWSER_INSIDEA"
|
|
1585 |
"POWSER_INSIDE" > "HOLLight.hollight.POWSER_INSIDE"
|
|
1586 |
"POWSER_EQUAL_0" > "HOLLight.hollight.POWSER_EQUAL_0"
|
|
1587 |
"POWSER_EQUAL" > "HOLLight.hollight.POWSER_EQUAL"
|
|
1588 |
"POWSER_0" > "HOLLight.hollight.POWSER_0"
|
|
1589 |
"POWREV" > "HOLLight.hollight.POWREV"
|
|
1590 |
"POWDIFF_LEMMA" > "HOLLight.hollight.POWDIFF_LEMMA"
|
|
1591 |
"POWDIFF" > "HOLLight.hollight.POWDIFF"
|
|
1592 |
"PI_POS" > "HOLLight.hollight.PI_POS"
|
|
1593 |
"PI2_PI4" > "HOLLight.hollight.PI2_PI4"
|
|
1594 |
"PI2_BOUNDS" > "HOLLight.hollight.PI2_BOUNDS"
|
|
1595 |
"PI2" > "HOLLight.hollight.PI2"
|
|
1596 |
"PASTECART_FST_SND" > "HOLLight.hollight.PASTECART_FST_SND"
|
|
1597 |
"PASTECART_EQ" > "HOLLight.hollight.PASTECART_EQ"
|
|
1598 |
"PASSOC_def" > "HOLLight.hollight.PASSOC_def"
|
|
1599 |
"PAIR_SURJECTIVE" > "Datatype.prod.nchotomy"
|
|
1600 |
"PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
|
|
1601 |
"PAIR_EQ" > "Datatype.prod.simps_1"
|
|
1602 |
"PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
|
|
1603 |
"PAIR" > "HOL4Compat.PAIR"
|
|
1604 |
"OUTR_def" > "HOLLight.hollight.OUTR_def"
|
|
1605 |
"OUTL_def" > "HOLLight.hollight.OUTL_def"
|
|
1606 |
"OR_EXISTS_THM" > "HOL.ex_disj_distrib"
|
|
1607 |
"OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
|
|
1608 |
"OPEN_UNOPEN" > "HOLLight.hollight.OPEN_UNOPEN"
|
|
1609 |
"OPEN_SUBOPEN" > "HOLLight.hollight.OPEN_SUBOPEN"
|
|
1610 |
"OPEN_OWN_NEIGH" > "HOLLight.hollight.OPEN_OWN_NEIGH"
|
|
1611 |
"OPEN_NEIGH" > "HOLLight.hollight.OPEN_NEIGH"
|
|
1612 |
"ONE" > "HOLLight.hollight.ONE"
|
|
1613 |
"ODD_def" > "HOLLight.hollight.ODD_def"
|
|
1614 |
"ODD_MULT" > "HOLLight.hollight.ODD_MULT"
|
|
1615 |
"ODD_MOD" > "HOLLight.hollight.ODD_MOD"
|
|
1616 |
"ODD_EXP" > "HOLLight.hollight.ODD_EXP"
|
|
1617 |
"ODD_EXISTS" > "HOLLight.hollight.ODD_EXISTS"
|
|
1618 |
"ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
|
|
1619 |
"ODD_ADD" > "HOLLight.hollight.ODD_ADD"
|
|
1620 |
"NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
|
|
1621 |
"NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
|
|
1622 |
"NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
|
|
1623 |
"NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
|
|
1624 |
"NUMSND_def" > "HOLLight.hollight.NUMSND_def"
|
|
1625 |
"NUMSEG_SING" > "HOLLight.hollight.NUMSEG_SING"
|
|
1626 |
"NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
|
|
1627 |
"NUMSEG_REC" > "HOLLight.hollight.NUMSEG_REC"
|
|
1628 |
"NUMSEG_OFFSET_IMAGE" > "HOLLight.hollight.NUMSEG_OFFSET_IMAGE"
|
|
1629 |
"NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
|
|
1630 |
"NUMSEG_EMPTY" > "HOLLight.hollight.NUMSEG_EMPTY"
|
|
1631 |
"NUMSEG_COMBINE_R" > "HOLLight.hollight.NUMSEG_COMBINE_R"
|
|
1632 |
"NUMSEG_COMBINE_L" > "HOLLight.hollight.NUMSEG_COMBINE_L"
|
|
1633 |
"NUMSEG_CLAUSES" > "HOLLight.hollight.NUMSEG_CLAUSES"
|
|
1634 |
"NUMSEG_ADD_SPLIT" > "HOLLight.hollight.NUMSEG_ADD_SPLIT"
|
|
1635 |
"NUMRIGHT_def" > "HOLLight.hollight.NUMRIGHT_def"
|
|
1636 |
"NUMPAIR_def" > "HOLLight.hollight.NUMPAIR_def"
|
|
1637 |
"NUMPAIR_INJ_LEMMA" > "HOLLight.hollight.NUMPAIR_INJ_LEMMA"
|
|
1638 |
"NUMPAIR_INJ" > "HOLLight.hollight.NUMPAIR_INJ"
|
|
1639 |
"NUMLEFT_def" > "HOLLight.hollight.NUMLEFT_def"
|
|
1640 |
"NUMFST_def" > "HOLLight.hollight.NUMFST_def"
|
|
1641 |
"NULL_def" > "HOLLight.hollight.NULL_def"
|
|
1642 |
"NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
|
|
1643 |
"NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
|
|
1644 |
"NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
|
|
1645 |
"NSUM_UNION" > "HOLLight.hollight.NSUM_UNION"
|
|
1646 |
"NSUM_TRIV_NUMSEG" > "HOLLight.hollight.NSUM_TRIV_NUMSEG"
|
|
1647 |
"NSUM_SWAP_NUMSEG" > "HOLLight.hollight.NSUM_SWAP_NUMSEG"
|
|
1648 |
"NSUM_SWAP" > "HOLLight.hollight.NSUM_SWAP"
|
|
1649 |
"NSUM_SUPPORT" > "HOLLight.hollight.NSUM_SUPPORT"
|
|
1650 |
"NSUM_SUPERSET" > "HOLLight.hollight.NSUM_SUPERSET"
|
|
1651 |
"NSUM_SUBSET_SIMPLE" > "HOLLight.hollight.NSUM_SUBSET_SIMPLE"
|
|
1652 |
"NSUM_SUBSET" > "HOLLight.hollight.NSUM_SUBSET"
|
|
1653 |
"NSUM_SING_NUMSEG" > "HOLLight.hollight.NSUM_SING_NUMSEG"
|
|
1654 |
"NSUM_SING" > "HOLLight.hollight.NSUM_SING"
|
|
1655 |
"NSUM_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
|
|
1656 |
"NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
|
|
1657 |
"NSUM_POS_LE_NUMSEG" > "HOLLight.hollight.NSUM_POS_LE_NUMSEG"
|
|
1658 |
"NSUM_POS_LE" > "HOLLight.hollight.NSUM_POS_LE"
|
|
1659 |
"NSUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_POS_EQ_0_NUMSEG"
|
|
1660 |
"NSUM_POS_EQ_0" > "HOLLight.hollight.NSUM_POS_EQ_0"
|
|
1661 |
"NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
|
|
1662 |
"NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
|
|
1663 |
"NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
|
|
1664 |
"NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
|
|
1665 |
"NSUM_MULTICOUNT_GEN" > "HOLLight.hollight.NSUM_MULTICOUNT_GEN"
|
|
1666 |
"NSUM_MULTICOUNT" > "HOLLight.hollight.NSUM_MULTICOUNT"
|
|
1667 |
"NSUM_LT_ALL" > "HOLLight.hollight.NSUM_LT_ALL"
|
|
1668 |
"NSUM_LT" > "HOLLight.hollight.NSUM_LT"
|
|
1669 |
"NSUM_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
|
|
1670 |
"NSUM_LE" > "HOLLight.hollight.NSUM_LE"
|
|
1671 |
"NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
|
|
1672 |
"NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
|
|
1673 |
"NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
|
|
1674 |
"NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
|
|
1675 |
"NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
|
|
1676 |
"NSUM_EQ_0" > "HOLLight.hollight.NSUM_EQ_0"
|
|
1677 |
"NSUM_EQ" > "HOLLight.hollight.NSUM_EQ"
|
|
1678 |
"NSUM_DIFF" > "HOLLight.hollight.NSUM_DIFF"
|
|
1679 |
"NSUM_DELTA" > "HOLLight.hollight.NSUM_DELTA"
|
|
1680 |
"NSUM_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
|
|
1681 |
"NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
|
|
1682 |
"NSUM_CMUL_NUMSEG" > "HOLLight.hollight.NSUM_CMUL_NUMSEG"
|
|
1683 |
"NSUM_CMUL" > "HOLLight.hollight.NSUM_CMUL"
|
|
1684 |
"NSUM_CLAUSES_RIGHT" > "HOLLight.hollight.NSUM_CLAUSES_RIGHT"
|
|
1685 |
"NSUM_CLAUSES_NUMSEG" > "HOLLight.hollight.NSUM_CLAUSES_NUMSEG"
|
|
1686 |
"NSUM_CLAUSES_LEFT" > "HOLLight.hollight.NSUM_CLAUSES_LEFT"
|
|
1687 |
"NSUM_CLAUSES" > "HOLLight.hollight.NSUM_CLAUSES"
|
|
1688 |
"NSUM_BOUND_LT_GEN" > "HOLLight.hollight.NSUM_BOUND_LT_GEN"
|
|
1689 |
"NSUM_BOUND_LT_ALL" > "HOLLight.hollight.NSUM_BOUND_LT_ALL"
|
|
1690 |
"NSUM_BOUND_LT" > "HOLLight.hollight.NSUM_BOUND_LT"
|
|
1691 |
"NSUM_BOUND_GEN" > "HOLLight.hollight.NSUM_BOUND_GEN"
|
|
1692 |
"NSUM_BOUND" > "HOLLight.hollight.NSUM_BOUND"
|
|
1693 |
"NSUM_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
|
|
1694 |
"NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
|
|
1695 |
"NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
|
|
1696 |
"NSUM_0" > "HOLLight.hollight.NSUM_0"
|
|
1697 |
"NOT_UNIV_PSUBSET" > "HOLLight.hollight.NOT_UNIV_PSUBSET"
|
|
1698 |
"NOT_SUC" > "Nat.nat.simps_1"
|
|
1699 |
"NOT_PSUBSET_EMPTY" > "HOLLight.hollight.NOT_PSUBSET_EMPTY"
|
|
1700 |
"NOT_ODD" > "HOLLight.hollight.NOT_ODD"
|
|
1701 |
"NOT_LT" > "HOLLight.hollight.NOT_LT"
|
|
1702 |
"NOT_LE" > "HOLLight.hollight.NOT_LE"
|
|
1703 |
"NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
|
|
1704 |
"NOT_INSERT_EMPTY" > "HOLLight.hollight.NOT_INSERT_EMPTY"
|
|
1705 |
"NOT_FORALL_THM" > "Inductive.basic_monos_15"
|
|
1706 |
"NOT_EXISTS_THM" > "Inductive.basic_monos_16"
|
|
1707 |
"NOT_EX" > "HOLLight.hollight.NOT_EX"
|
|
1708 |
"NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
|
|
1709 |
"NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
|
|
1710 |
"NOT_EMPTY_INSERT" > "HOLLight.hollight.NOT_EMPTY_INSERT"
|
|
1711 |
"NOT_CONS_NIL" > "HOLLight.hollight.NOT_CONS_NIL"
|
|
1712 |
"NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
|
|
1713 |
"NOT_ALL" > "HOLLight.hollight.NOT_ALL"
|
|
1714 |
"NONE_def" > "HOLLight.hollight.NONE_def"
|
|
1715 |
"NIL_def" > "HOLLight.hollight.NIL_def"
|
|
1716 |
"NEUTRAL_REAL_MUL" > "HOLLight.hollight.NEUTRAL_REAL_MUL"
|
|
1717 |
"NEUTRAL_REAL_ADD" > "HOLLight.hollight.NEUTRAL_REAL_ADD"
|
|
1718 |
"NEUTRAL_MUL" > "HOLLight.hollight.NEUTRAL_MUL"
|
|
1719 |
"NEUTRAL_ADD" > "HOLLight.hollight.NEUTRAL_ADD"
|
|
1720 |
"NET_SUM" > "HOLLight.hollight.NET_SUM"
|
|
1721 |
"NET_SUB" > "HOLLight.hollight.NET_SUB"
|
|
1722 |
"NET_NULL_MUL" > "HOLLight.hollight.NET_NULL_MUL"
|
|
1723 |
"NET_NULL_CMUL" > "HOLLight.hollight.NET_NULL_CMUL"
|
|
1724 |
"NET_NULL_ADD" > "HOLLight.hollight.NET_NULL_ADD"
|
|
1725 |
"NET_NULL" > "HOLLight.hollight.NET_NULL"
|
|
1726 |
"NET_NEG" > "HOLLight.hollight.NET_NEG"
|
|
1727 |
"NET_MUL" > "HOLLight.hollight.NET_MUL"
|
|
1728 |
"NET_LE" > "HOLLight.hollight.NET_LE"
|
|
1729 |
"NET_INV" > "HOLLight.hollight.NET_INV"
|
|
1730 |
"NET_DIV" > "HOLLight.hollight.NET_DIV"
|
|
1731 |
"NET_CONV_NZ" > "HOLLight.hollight.NET_CONV_NZ"
|
|
1732 |
"NET_CONV_IBOUNDED" > "HOLLight.hollight.NET_CONV_IBOUNDED"
|
|
1733 |
"NET_CONV_BOUNDED" > "HOLLight.hollight.NET_CONV_BOUNDED"
|
|
1734 |
"NET_ADD" > "HOLLight.hollight.NET_ADD"
|
|
1735 |
"NET_ABS" > "HOLLight.hollight.NET_ABS"
|
|
1736 |
"NEST_LEMMA_UNIQ" > "HOLLight.hollight.NEST_LEMMA_UNIQ"
|
|
1737 |
"NEST_LEMMA" > "HOLLight.hollight.NEST_LEMMA"
|
|
1738 |
"NADD_UBOUND" > "HOLLight.hollight.NADD_UBOUND"
|
|
1739 |
"NADD_SUC" > "HOLLight.hollight.NADD_SUC"
|
|
1740 |
"NADD_RDISTRIB" > "HOLLight.hollight.NADD_RDISTRIB"
|
|
1741 |
"NADD_OF_NUM_WELLDEF" > "HOLLight.hollight.NADD_OF_NUM_WELLDEF"
|
|
1742 |
"NADD_OF_NUM_MUL" > "HOLLight.hollight.NADD_OF_NUM_MUL"
|
|
1743 |
"NADD_OF_NUM_LE" > "HOLLight.hollight.NADD_OF_NUM_LE"
|
|
1744 |
"NADD_OF_NUM_EQ" > "HOLLight.hollight.NADD_OF_NUM_EQ"
|
|
1745 |
"NADD_OF_NUM_ADD" > "HOLLight.hollight.NADD_OF_NUM_ADD"
|
|
1746 |
"NADD_OF_NUM" > "HOLLight.hollight.NADD_OF_NUM"
|
|
1747 |
"NADD_NONZERO" > "HOLLight.hollight.NADD_NONZERO"
|
|
1748 |
"NADD_MUL_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_MUL_WELLDEF_LEMMA"
|
|
1749 |
"NADD_MUL_WELLDEF" > "HOLLight.hollight.NADD_MUL_WELLDEF"
|
|
1750 |
"NADD_MUL_SYM" > "HOLLight.hollight.NADD_MUL_SYM"
|
|
1751 |
"NADD_MUL_LINV_LEMMA8" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA8"
|
|
1752 |
"NADD_MUL_LINV_LEMMA7a" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7a"
|
|
1753 |
"NADD_MUL_LINV_LEMMA7" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7"
|
|
1754 |
"NADD_MUL_LINV_LEMMA6" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA6"
|
|
1755 |
"NADD_MUL_LINV_LEMMA5" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA5"
|
|
1756 |
"NADD_MUL_LINV_LEMMA4" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA4"
|
|
1757 |
"NADD_MUL_LINV_LEMMA3" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA3"
|
|
1758 |
"NADD_MUL_LINV_LEMMA2" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA2"
|
|
1759 |
"NADD_MUL_LINV_LEMMA1" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA1"
|
|
1760 |
"NADD_MUL_LINV_LEMMA0" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA0"
|
|
1761 |
"NADD_MUL_LINV" > "HOLLight.hollight.NADD_MUL_LINV"
|
|
1762 |
"NADD_MUL_LID" > "HOLLight.hollight.NADD_MUL_LID"
|
|
1763 |
"NADD_MUL_ASSOC" > "HOLLight.hollight.NADD_MUL_ASSOC"
|
|
1764 |
"NADD_MULTIPLICATIVE" > "HOLLight.hollight.NADD_MULTIPLICATIVE"
|
|
1765 |
"NADD_MUL" > "HOLLight.hollight.NADD_MUL"
|
|
1766 |
"NADD_LE_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_LE_WELLDEF_LEMMA"
|
|
1767 |
"NADD_LE_WELLDEF" > "HOLLight.hollight.NADD_LE_WELLDEF"
|
|
1768 |
"NADD_LE_TRANS" > "HOLLight.hollight.NADD_LE_TRANS"
|
|
1769 |
"NADD_LE_TOTAL_LEMMA" > "HOLLight.hollight.NADD_LE_TOTAL_LEMMA"
|
|
1770 |
"NADD_LE_TOTAL" > "HOLLight.hollight.NADD_LE_TOTAL"
|
|
1771 |
"NADD_LE_RMUL" > "HOLLight.hollight.NADD_LE_RMUL"
|
|
1772 |
"NADD_LE_REFL" > "HOLLight.hollight.NADD_LE_REFL"
|
|
1773 |
"NADD_LE_RADD" > "HOLLight.hollight.NADD_LE_RADD"
|
|
1774 |
"NADD_LE_LMUL" > "HOLLight.hollight.NADD_LE_LMUL"
|
|
1775 |
"NADD_LE_LADD" > "HOLLight.hollight.NADD_LE_LADD"
|
|
1776 |
"NADD_LE_EXISTS" > "HOLLight.hollight.NADD_LE_EXISTS"
|
|
1777 |
"NADD_LE_ANTISYM" > "HOLLight.hollight.NADD_LE_ANTISYM"
|
|
1778 |
"NADD_LE_ADD" > "HOLLight.hollight.NADD_LE_ADD"
|
|
1779 |
"NADD_LE_0" > "HOLLight.hollight.NADD_LE_0"
|
|
1780 |
"NADD_LDISTRIB" > "HOLLight.hollight.NADD_LDISTRIB"
|
|
1781 |
"NADD_LBOUND" > "HOLLight.hollight.NADD_LBOUND"
|
|
1782 |
"NADD_INV_WELLDEF" > "HOLLight.hollight.NADD_INV_WELLDEF"
|
|
1783 |
"NADD_INV_0" > "HOLLight.hollight.NADD_INV_0"
|
|
1784 |
"NADD_INV" > "HOLLight.hollight.NADD_INV"
|
|
1785 |
"NADD_EQ_TRANS" > "HOLLight.hollight.NADD_EQ_TRANS"
|
|
1786 |
"NADD_EQ_SYM" > "HOLLight.hollight.NADD_EQ_SYM"
|
|
1787 |
"NADD_EQ_REFL" > "HOLLight.hollight.NADD_EQ_REFL"
|
|
1788 |
"NADD_EQ_IMP_LE" > "HOLLight.hollight.NADD_EQ_IMP_LE"
|
|
1789 |
"NADD_DIST_LEMMA" > "HOLLight.hollight.NADD_DIST_LEMMA"
|
|
1790 |
"NADD_DIST" > "HOLLight.hollight.NADD_DIST"
|
|
1791 |
"NADD_COMPLETE" > "HOLLight.hollight.NADD_COMPLETE"
|
|
1792 |
"NADD_CAUCHY" > "HOLLight.hollight.NADD_CAUCHY"
|
|
1793 |
"NADD_BOUND" > "HOLLight.hollight.NADD_BOUND"
|
|
1794 |
"NADD_ARCH_ZERO" > "HOLLight.hollight.NADD_ARCH_ZERO"
|
|
1795 |
"NADD_ARCH_MULT" > "HOLLight.hollight.NADD_ARCH_MULT"
|
|
1796 |
"NADD_ARCH_LEMMA" > "HOLLight.hollight.NADD_ARCH_LEMMA"
|
|
1797 |
"NADD_ARCH" > "HOLLight.hollight.NADD_ARCH"
|
|
1798 |
"NADD_ALTMUL" > "HOLLight.hollight.NADD_ALTMUL"
|
|
1799 |
"NADD_ADD_WELLDEF" > "HOLLight.hollight.NADD_ADD_WELLDEF"
|
|
1800 |
"NADD_ADD_SYM" > "HOLLight.hollight.NADD_ADD_SYM"
|
|
1801 |
"NADD_ADD_LID" > "HOLLight.hollight.NADD_ADD_LID"
|
|
1802 |
"NADD_ADD_LCANCEL" > "HOLLight.hollight.NADD_ADD_LCANCEL"
|
|
1803 |
"NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
|
|
1804 |
"NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
|
|
1805 |
"NADD_ADD" > "HOLLight.hollight.NADD_ADD"
|
|
1806 |
"MVT_LEMMA" > "HOLLight.hollight.MVT_LEMMA"
|
|
1807 |
"MVT_ALT" > "HOLLight.hollight.MVT_ALT"
|
|
1808 |
"MVT" > "HOLLight.hollight.MVT"
|
|
1809 |
"MULT_SYM" > "IntDef.zmult_ac_2"
|
|
1810 |
"MULT_SUC" > "Nat.mult_Suc_right"
|
|
1811 |
"MULT_EXP" > "HOLLight.hollight.MULT_EXP"
|
|
1812 |
"MULT_EQ_1" > "HOLLight.hollight.MULT_EQ_1"
|
|
1813 |
"MULT_EQ_0" > "Nat.mult_is_0"
|
|
1814 |
"MULT_DIV_2" > "HOLLight.hollight.MULT_DIV_2"
|
|
1815 |
"MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
|
|
1816 |
"MULT_ASSOC" > "IntDef.zmult_ac_1"
|
|
1817 |
"MULT_AC" > "HOLLight.hollight.MULT_AC"
|
|
1818 |
"MULT_2" > "HOLLight.hollight.MULT_2"
|
|
1819 |
"MULT_0" > "Nat.mult_0_right"
|
|
1820 |
"MTOP_TENDS_UNIQ" > "HOLLight.hollight.MTOP_TENDS_UNIQ"
|
|
1821 |
"MTOP_TENDS" > "HOLLight.hollight.MTOP_TENDS"
|
|
1822 |
"MTOP_OPEN" > "HOLLight.hollight.MTOP_OPEN"
|
|
1823 |
"MTOP_LIMPT" > "HOLLight.hollight.MTOP_LIMPT"
|
|
1824 |
"MR1_SUB_LT" > "HOLLight.hollight.MR1_SUB_LT"
|
|
1825 |
"MR1_SUB_LE" > "HOLLight.hollight.MR1_SUB_LE"
|
|
1826 |
"MR1_SUB" > "HOLLight.hollight.MR1_SUB"
|
|
1827 |
"MR1_LIMPT" > "HOLLight.hollight.MR1_LIMPT"
|
|
1828 |
"MR1_DEF" > "HOLLight.hollight.MR1_DEF"
|
|
1829 |
"MR1_BOUNDED" > "HOLLight.hollight.MR1_BOUNDED"
|
|
1830 |
"MR1_BETWEEN1" > "HOLLight.hollight.MR1_BETWEEN1"
|
|
1831 |
"MR1_ADD_LT" > "HOLLight.hollight.MR1_ADD_LT"
|
|
1832 |
"MR1_ADD_LE" > "HOLLight.hollight.MR1_ADD_LE"
|
|
1833 |
"MR1_ADD" > "HOLLight.hollight.MR1_ADD"
|
|
1834 |
"MONO_SUC" > "HOLLight.hollight.MONO_SUC"
|
|
1835 |
"MONO_FORALL" > "Inductive.basic_monos_6"
|
|
1836 |
"MONO_EXISTS" > "Inductive.basic_monos_5"
|
|
1837 |
"MONO_COND" > "HOLLight.hollight.MONO_COND"
|
|
1838 |
"MONO_ALL2" > "HOLLight.hollight.MONO_ALL2"
|
|
1839 |
"MONO_ALL" > "HOLLight.hollight.MONO_ALL"
|
|
1840 |
"MONOIDAL_REAL_MUL" > "HOLLight.hollight.MONOIDAL_REAL_MUL"
|
|
1841 |
"MONOIDAL_REAL_ADD" > "HOLLight.hollight.MONOIDAL_REAL_ADD"
|
|
1842 |
"MONOIDAL_MUL" > "HOLLight.hollight.MONOIDAL_MUL"
|
|
1843 |
"MONOIDAL_ADD" > "HOLLight.hollight.MONOIDAL_ADD"
|
|
1844 |
"MOD_def" > "HOLLight.hollight.MOD_def"
|
|
1845 |
"MOD_UNIQ" > "HOLLight.hollight.MOD_UNIQ"
|
|
1846 |
"MOD_MULT_RMOD" > "HOLLight.hollight.MOD_MULT_RMOD"
|
|
1847 |
"MOD_MULT_MOD2" > "HOLLight.hollight.MOD_MULT_MOD2"
|
|
1848 |
"MOD_MULT_LMOD" > "HOLLight.hollight.MOD_MULT_LMOD"
|
|
1849 |
"MOD_MULT_ADD" > "HOLLight.hollight.MOD_MULT_ADD"
|
|
1850 |
"MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
|
|
1851 |
"MOD_MULT" > "HOLLight.hollight.MOD_MULT"
|
|
1852 |
"MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
|
|
1853 |
"MOD_MOD" > "HOLLight.hollight.MOD_MOD"
|
|
1854 |
"MOD_LT" > "HOLLight.hollight.MOD_LT"
|
|
1855 |
"MOD_LE" > "HOLLight.hollight.MOD_LE"
|
|
1856 |
"MOD_EXP_MOD" > "HOLLight.hollight.MOD_EXP_MOD"
|
|
1857 |
"MOD_EXISTS" > "HOLLight.hollight.MOD_EXISTS"
|
|
1858 |
"MOD_EQ_0" > "HOLLight.hollight.MOD_EQ_0"
|
|
1859 |
"MOD_EQ" > "HOLLight.hollight.MOD_EQ"
|
|
1860 |
"MOD_ADD_MOD" > "HOLLight.hollight.MOD_ADD_MOD"
|
|
1861 |
"MOD_1" > "HOLLight.hollight.MOD_1"
|
|
1862 |
"MOD_0" > "HOLLight.hollight.MOD_0"
|
|
1863 |
"MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
|
|
1864 |
"MINIMAL" > "HOLLight.hollight.MINIMAL"
|
|
1865 |
"METRIC_ZERO" > "HOLLight.hollight.METRIC_ZERO"
|
|
1866 |
"METRIC_TRIANGLE" > "HOLLight.hollight.METRIC_TRIANGLE"
|
|
1867 |
"METRIC_SYM" > "HOLLight.hollight.METRIC_SYM"
|
|
1868 |
"METRIC_SAME" > "HOLLight.hollight.METRIC_SAME"
|
|
1869 |
"METRIC_POS" > "HOLLight.hollight.METRIC_POS"
|
|
1870 |
"METRIC_NZ" > "HOLLight.hollight.METRIC_NZ"
|
|
1871 |
"METRIC_ISMET" > "HOLLight.hollight.METRIC_ISMET"
|
|
1872 |
"MEM_def" > "HOLLight.hollight.MEM_def"
|
|
1873 |
"MEM_MAP" > "HOLLight.hollight.MEM_MAP"
|
|
1874 |
"MEM_LIST_OF_SET" > "HOLLight.hollight.MEM_LIST_OF_SET"
|
|
1875 |
"MEM_FILTER" > "HOLLight.hollight.MEM_FILTER"
|
|
1876 |
"MEM_EL" > "HOLLight.hollight.MEM_EL"
|
|
1877 |
"MEM_ASSOC" > "HOLLight.hollight.MEM_ASSOC"
|
|
1878 |
"MEM_APPEND" > "HOLLight.hollight.MEM_APPEND"
|
|
1879 |
"MEMBER_NOT_EMPTY" > "HOLLight.hollight.MEMBER_NOT_EMPTY"
|
|
1880 |
"MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
|
|
1881 |
"MCLAURIN_ZERO" > "HOLLight.hollight.MCLAURIN_ZERO"
|
|
1882 |
"MCLAURIN_SIN" > "HOLLight.hollight.MCLAURIN_SIN"
|
|
1883 |
"MCLAURIN_NEG" > "HOLLight.hollight.MCLAURIN_NEG"
|
|
1884 |
"MCLAURIN_LN_POS" > "HOLLight.hollight.MCLAURIN_LN_POS"
|
|
1885 |
"MCLAURIN_LN_NEG" > "HOLLight.hollight.MCLAURIN_LN_NEG"
|
|
1886 |
"MCLAURIN_EXP_LT" > "HOLLight.hollight.MCLAURIN_EXP_LT"
|
|
1887 |
"MCLAURIN_EXP_LEMMA" > "HOLLight.hollight.MCLAURIN_EXP_LEMMA"
|
|
1888 |
"MCLAURIN_EXP_LE" > "HOLLight.hollight.MCLAURIN_EXP_LE"
|
|
1889 |
"MCLAURIN_COS" > "HOLLight.hollight.MCLAURIN_COS"
|
|
1890 |
"MCLAURIN_BI_LE" > "HOLLight.hollight.MCLAURIN_BI_LE"
|
|
1891 |
"MCLAURIN_ATN" > "HOLLight.hollight.MCLAURIN_ATN"
|
|
1892 |
"MCLAURIN_ALL_LT" > "HOLLight.hollight.MCLAURIN_ALL_LT"
|
|
1893 |
"MCLAURIN_ALL_LE" > "HOLLight.hollight.MCLAURIN_ALL_LE"
|
|
1894 |
"MCLAURIN" > "HOLLight.hollight.MCLAURIN"
|
|
1895 |
"MAX_LEMMA" > "HOLLight.hollight.MAX_LEMMA"
|
|
1896 |
"MAP_o" > "HOLLight.hollight.MAP_o"
|
|
1897 |
"MAP_def" > "HOLLight.hollight.MAP_def"
|
|
1898 |
"MAP_SND_ZIP" > "HOLLight.hollight.MAP_SND_ZIP"
|
|
1899 |
"MAP_FST_ZIP" > "HOLLight.hollight.MAP_FST_ZIP"
|
|
1900 |
"MAP_EQ_DEGEN" > "HOLLight.hollight.MAP_EQ_DEGEN"
|
|
1901 |
"MAP_EQ_ALL2" > "HOLLight.hollight.MAP_EQ_ALL2"
|
|
1902 |
"MAP_EQ" > "HOLLight.hollight.MAP_EQ"
|
|
1903 |
"MAP_APPEND" > "HOLLight.hollight.MAP_APPEND"
|
|
1904 |
"MAP2_def" > "HOLLight.hollight.MAP2_def"
|
|
1905 |
"MAP2" > "HOLLight.hollight.MAP2"
|
|
1906 |
"LT_TRANS" > "HOLLight.hollight.LT_TRANS"
|
|
1907 |
"LT_SUC_LE" > "HOLLight.hollight.LT_SUC_LE"
|
|
1908 |
"LT_SUC" > "HOLLight.hollight.LT_SUC"
|
|
1909 |
"LT_REFL" > "HOLLight.hollight.LT_REFL"
|
|
1910 |
"LT_NZ" > "HOLLight.hollight.LT_NZ"
|
|
1911 |
"LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
|
|
1912 |
"LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
|
|
1913 |
"LT_MULT2" > "HOLLight.hollight.LT_MULT2"
|
|
1914 |
"LT_MULT" > "HOLLight.hollight.LT_MULT"
|
|
1915 |
"LT_LMULT" > "HOLLight.hollight.LT_LMULT"
|
|
1916 |
"LT_LE" > "HOLLight.hollight.LT_LE"
|
|
1917 |
"LT_IMP_LE" > "HOLLight.hollight.LT_IMP_LE"
|
|
1918 |
"LT_EXP" > "HOLLight.hollight.LT_EXP"
|
|
1919 |
"LT_EXISTS" > "HOLLight.hollight.LT_EXISTS"
|
|
1920 |
"LT_CASES" > "HOLLight.hollight.LT_CASES"
|
|
1921 |
"LT_ANTISYM" > "HOLLight.hollight.LT_ANTISYM"
|
|
1922 |
"LT_ADD_RCANCEL" > "HOLLight.hollight.LT_ADD_RCANCEL"
|
|
1923 |
"LT_ADD_LCANCEL" > "HOLLight.hollight.LT_ADD_LCANCEL"
|
|
1924 |
"LT_ADDR" > "HOLLight.hollight.LT_ADDR"
|
|
1925 |
"LT_ADD2" > "HOLLight.hollight.LT_ADD2"
|
|
1926 |
"LT_ADD" > "HOLLight.hollight.LT_ADD"
|
|
1927 |
"LT_0" > "HOLLight.hollight.LT_0"
|
|
1928 |
"LTE_TRANS" > "HOLLight.hollight.LTE_TRANS"
|
|
1929 |
"LTE_CASES" > "HOLLight.hollight.LTE_CASES"
|
|
1930 |
"LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
|
|
1931 |
"LTE_ADD2" > "HOLLight.hollight.LTE_ADD2"
|
|
1932 |
"LN_POW" > "HOLLight.hollight.LN_POW"
|
|
1933 |
"LN_POS_LT" > "HOLLight.hollight.LN_POS_LT"
|
|
1934 |
"LN_POS" > "HOLLight.hollight.LN_POS"
|
|
1935 |
"LN_MUL" > "HOLLight.hollight.LN_MUL"
|
|
1936 |
"LN_MONO_LT" > "HOLLight.hollight.LN_MONO_LT"
|
|
1937 |
"LN_MONO_LE" > "HOLLight.hollight.LN_MONO_LE"
|
|
1938 |
"LN_LT_X" > "HOLLight.hollight.LN_LT_X"
|
|
1939 |
"LN_LE" > "HOLLight.hollight.LN_LE"
|
|
1940 |
"LN_INV" > "HOLLight.hollight.LN_INV"
|
|
1941 |
"LN_INJ" > "HOLLight.hollight.LN_INJ"
|
|
1942 |
"LN_EXP" > "HOLLight.hollight.LN_EXP"
|
|
1943 |
"LN_DIV" > "HOLLight.hollight.LN_DIV"
|
|
1944 |
"LN_1" > "HOLLight.hollight.LN_1"
|
|
1945 |
"LIST_OF_SET_PROPERTIES" > "HOLLight.hollight.LIST_OF_SET_PROPERTIES"
|
|
1946 |
"LIM_X" > "HOLLight.hollight.LIM_X"
|
|
1947 |
"LIM_UNIQ" > "HOLLight.hollight.LIM_UNIQ"
|
|
1948 |
"LIM_TRANSFORM" > "HOLLight.hollight.LIM_TRANSFORM"
|
|
1949 |
"LIM_TENDS2" > "HOLLight.hollight.LIM_TENDS2"
|
|
1950 |
"LIM_TENDS" > "HOLLight.hollight.LIM_TENDS"
|
|
1951 |
"LIM_SUM" > "HOLLight.hollight.LIM_SUM"
|
|
1952 |
"LIM_SUB" > "HOLLight.hollight.LIM_SUB"
|
|
1953 |
"LIM_NULL" > "HOLLight.hollight.LIM_NULL"
|
|
1954 |
"LIM_NEG" > "HOLLight.hollight.LIM_NEG"
|
|
1955 |
"LIM_MUL" > "HOLLight.hollight.LIM_MUL"
|
|
1956 |
"LIM_INV" > "HOLLight.hollight.LIM_INV"
|
|
1957 |
"LIM_EQUAL" > "HOLLight.hollight.LIM_EQUAL"
|
|
1958 |
"LIM_DIV" > "HOLLight.hollight.LIM_DIV"
|
|
1959 |
"LIM_CONST" > "HOLLight.hollight.LIM_CONST"
|
|
1960 |
"LIM_ADD" > "HOLLight.hollight.LIM_ADD"
|
|
1961 |
"LIM" > "HOLLight.hollight.LIM"
|
|
1962 |
"LE_TRANS" > "HOLLight.hollight.LE_TRANS"
|
|
1963 |
"LE_SUC_LT" > "HOLLight.hollight.LE_SUC_LT"
|
|
1964 |
"LE_SUC" > "HOLLight.hollight.LE_SUC"
|
|
1965 |
"LE_SQUARE_REFL" > "HOLLight.hollight.LE_SQUARE_REFL"
|
|
1966 |
"LE_REFL" > "HOLLight.hollight.LE_REFL"
|
|
1967 |
"LE_RDIV_EQ" > "HOLLight.hollight.LE_RDIV_EQ"
|
|
1968 |
"LE_MULT_RCANCEL" > "HOLLight.hollight.LE_MULT_RCANCEL"
|
|
1969 |
"LE_MULT_LCANCEL" > "HOLLight.hollight.LE_MULT_LCANCEL"
|
|
1970 |
"LE_MULT2" > "HOLLight.hollight.LE_MULT2"
|
|
1971 |
"LE_LT" > "HOLLight.hollight.LE_LT"
|
|
1972 |
"LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
|
|
1973 |
"LE_LDIV" > "HOLLight.hollight.LE_LDIV"
|
|
1974 |
"LE_EXP" > "HOLLight.hollight.LE_EXP"
|
|
1975 |
"LE_EXISTS" > "HOLLight.hollight.LE_EXISTS"
|
|
1976 |
"LE_CASES" > "HOLLight.hollight.LE_CASES"
|
|
1977 |
"LE_ANTISYM" > "HOLLight.hollight.LE_ANTISYM"
|
|
1978 |
"LE_ADD_RCANCEL" > "HOLLight.hollight.LE_ADD_RCANCEL"
|
|
1979 |
"LE_ADD_LCANCEL" > "HOLLight.hollight.LE_ADD_LCANCEL"
|
|
1980 |
"LE_ADDR" > "HOLLight.hollight.LE_ADDR"
|
|
1981 |
"LE_ADD2" > "HOLLight.hollight.LE_ADD2"
|
|
1982 |
"LE_ADD" > "HOLLight.hollight.LE_ADD"
|
|
1983 |
"LE_0" > "HOLLight.hollight.LE_0"
|
|
1984 |
"LET_TRANS" > "HOLLight.hollight.LET_TRANS"
|
|
1985 |
"LET_END_def" > "HOLLight.hollight.LET_END_def"
|
|
1986 |
"LET_CASES" > "HOLLight.hollight.LET_CASES"
|
|
1987 |
"LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
|
|
1988 |
"LET_ADD2" > "HOLLight.hollight.LET_ADD2"
|
|
1989 |
"LESS_SUC_EQ" > "HOLLight.hollight.LESS_SUC_EQ"
|
|
1990 |
"LESS_1" > "HOLLight.hollight.LESS_1"
|
|
1991 |
"LENGTH_def" > "HOLLight.hollight.LENGTH_def"
|
|
1992 |
"LENGTH_REPLICATE" > "HOLLight.hollight.LENGTH_REPLICATE"
|
|
1993 |
"LENGTH_MAP2" > "HOLLight.hollight.LENGTH_MAP2"
|
|
1994 |
"LENGTH_MAP" > "HOLLight.hollight.LENGTH_MAP"
|
|
1995 |
"LENGTH_LIST_OF_SET" > "HOLLight.hollight.LENGTH_LIST_OF_SET"
|
|
1996 |
"LENGTH_EQ_NIL" > "HOLLight.hollight.LENGTH_EQ_NIL"
|
|
1997 |
"LENGTH_EQ_CONS" > "HOLLight.hollight.LENGTH_EQ_CONS"
|
|
1998 |
"LENGTH_APPEND" > "HOLLight.hollight.LENGTH_APPEND"
|
|
1999 |
"LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
|
|
2000 |
"LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
|
|
2001 |
"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
|
|
2002 |
"LEFT_OR_DISTRIB" > "HOL.conj_disj_distribL"
|
|
2003 |
"LEFT_IMP_FORALL_THM" > "HOL.imp_all"
|
|
2004 |
"LEFT_IMP_EXISTS_THM" > "HOL.imp_ex"
|
|
2005 |
"LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
|
|
2006 |
"LEFT_FORALL_IMP_THM" > "HOL.imp_ex"
|
|
2007 |
"LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
|
|
2008 |
"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
|
|
2009 |
"LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
|
|
2010 |
"LEFT_AND_EXISTS_THM" > "HOL.ex_simps_1"
|
|
2011 |
"LEFT_ADD_DISTRIB" > "Nat.nat_distrib_2"
|
|
2012 |
"LAST_def" > "HOLLight.hollight.LAST_def"
|
|
2013 |
"LAST_CLAUSES" > "HOLLight.hollight.LAST_CLAUSES"
|
|
2014 |
"LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
|
|
2015 |
"LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
|
|
2016 |
"LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
|
|
2017 |
"I_THM" > "Fun.id_apply"
|
|
2018 |
"I_O_ID" > "HOLLight.hollight.I_O_ID"
|
|
2019 |
"IVT_DERIVATIVE_POS" > "HOLLight.hollight.IVT_DERIVATIVE_POS"
|
|
2020 |
"IVT_DERIVATIVE_NEG" > "HOLLight.hollight.IVT_DERIVATIVE_NEG"
|
|
2021 |
"IVT_DERIVATIVE_0" > "HOLLight.hollight.IVT_DERIVATIVE_0"
|
|
2022 |
"IVT2" > "HOLLight.hollight.IVT2"
|
|
2023 |
"IVT" > "HOLLight.hollight.IVT"
|
|
2024 |
"ITSET_def" > "HOLLight.hollight.ITSET_def"
|
|
2025 |
"ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
|
|
2026 |
"ITLIST_def" > "HOLLight.hollight.ITLIST_def"
|
|
2027 |
"ITLIST_EXTRA" > "HOLLight.hollight.ITLIST_EXTRA"
|
|
2028 |
"ITLIST2_def" > "HOLLight.hollight.ITLIST2_def"
|
|
2029 |
"ITLIST2" > "HOLLight.hollight.ITLIST2"
|
|
2030 |
"ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
|
|
2031 |
"ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
|
|
2032 |
"ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
|
|
2033 |
"ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
|
|
2034 |
"ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
|
|
2035 |
"ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
|
|
2036 |
"ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
|
|
2037 |
"ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
|
|
2038 |
"ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
|
|
2039 |
"ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
|
|
2040 |
"ITERATE_CLOSED_GEN" > "HOLLight.hollight.ITERATE_CLOSED_GEN"
|
|
2041 |
"ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
|
|
2042 |
"ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
|
|
2043 |
"ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
|
|
2044 |
"ISO_def" > "HOLLight.hollight.ISO_def"
|
|
2045 |
"ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
|
|
2046 |
"ISO_REFL" > "HOLLight.hollight.ISO_REFL"
|
|
2047 |
"ISO_FUN" > "HOLLight.hollight.ISO_FUN"
|
|
2048 |
"ISMET_R1" > "HOLLight.hollight.ISMET_R1"
|
|
2049 |
"IN_def" > "HOLLight.hollight.IN_def"
|
|
2050 |
"IN_UNIV" > "HOLLight.hollight.IN_UNIV"
|
|
2051 |
"IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
|
|
2052 |
"IN_UNION" > "HOLLight.hollight.IN_UNION"
|
|
2053 |
"IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
|
|
2054 |
"IN_SING" > "HOLLight.hollight.IN_SING"
|
|
2055 |
"IN_SET_OF_LIST" > "HOLLight.hollight.IN_SET_OF_LIST"
|
|
2056 |
"IN_REST" > "HOLLight.hollight.IN_REST"
|
|
2057 |
"IN_NUMSEG" > "HOLLight.hollight.IN_NUMSEG"
|
|
2058 |
"IN_INTERS" > "HOLLight.hollight.IN_INTERS"
|
|
2059 |
"IN_INTER" > "HOLLight.hollight.IN_INTER"
|
|
2060 |
"IN_INSERT" > "HOLLight.hollight.IN_INSERT"
|
|
2061 |
"IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
|
|
2062 |
"IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
|
|
2063 |
"IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
|
|
2064 |
"IN_DIFF" > "HOLLight.hollight.IN_DIFF"
|
|
2065 |
"IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
|
|
2066 |
"IN_DELETE" > "HOLLight.hollight.IN_DELETE"
|
|
2067 |
"INT_POW" > "HOLLight.hollight.INT_POW"
|
|
2068 |
"INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
|
|
2069 |
"INT_LT" > "HOLLight.hollight.INT_LT"
|
|
2070 |
"INT_IMAGE" > "HOLLight.hollight.INT_IMAGE"
|
|
2071 |
"INT_GT_DISCRETE" > "HOLLight.hollight.INT_GT_DISCRETE"
|
|
2072 |
"INT_GT" > "HOLLight.hollight.INT_GT"
|
|
2073 |
"INT_GE" > "HOLLight.hollight.INT_GE"
|
|
2074 |
"INT_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
|
|
2075 |
"INT_ARCH" > "HOLLight.hollight.INT_ARCH"
|
|
2076 |
"INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
|
|
2077 |
"INT_ABS" > "HOLLight.hollight.INT_ABS"
|
|
2078 |
"INTER_def" > "HOLLight.hollight.INTER_def"
|
|
2079 |
"INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
|
|
2080 |
"INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
|
|
2081 |
"INTER_OVER_UNION" > "HOLLight.hollight.INTER_OVER_UNION"
|
|
2082 |
"INTER_IDEMPOT" > "HOLLight.hollight.INTER_IDEMPOT"
|
|
2083 |
"INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
|
|
2084 |
"INTER_COMM" > "HOLLight.hollight.INTER_COMM"
|
|
2085 |
"INTER_ASSOC" > "HOLLight.hollight.INTER_ASSOC"
|
|
2086 |
"INTER_ACI" > "HOLLight.hollight.INTER_ACI"
|
|
2087 |
"INTERVAL_LEMMA_LT" > "HOLLight.hollight.INTERVAL_LEMMA_LT"
|
|
2088 |
"INTERVAL_LEMMA" > "HOLLight.hollight.INTERVAL_LEMMA"
|
|
2089 |
"INTERVAL_ABS" > "HOLLight.hollight.INTERVAL_ABS"
|
|
2090 |
"INTERS_def" > "HOLLight.hollight.INTERS_def"
|
|
2091 |
"INTEGRAL_NULL" > "HOLLight.hollight.INTEGRAL_NULL"
|
|
2092 |
"INSERT_def" > "HOLLight.hollight.INSERT_def"
|
|
2093 |
"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
|
|
2094 |
"INSERT_UNION_EQ" > "HOLLight.hollight.INSERT_UNION_EQ"
|
|
2095 |
"INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
|
|
2096 |
"INSERT_SUBSET" > "HOLLight.hollight.INSERT_SUBSET"
|
|
2097 |
"INSERT_INTER" > "HOLLight.hollight.INSERT_INTER"
|
|
2098 |
"INSERT_INSERT" > "HOLLight.hollight.INSERT_INSERT"
|
|
2099 |
"INSERT_DIFF" > "HOLLight.hollight.INSERT_DIFF"
|
|
2100 |
"INSERT_DELETE" > "HOLLight.hollight.INSERT_DELETE"
|
|
2101 |
"INSERT_COMM" > "HOLLight.hollight.INSERT_COMM"
|
|
2102 |
"INSERT_AC" > "HOLLight.hollight.INSERT_AC"
|
|
2103 |
"INSERT" > "HOLLight.hollight.INSERT"
|
|
2104 |
"INR_def" > "HOLLight.hollight.INR_def"
|
|
2105 |
"INL_def" > "HOLLight.hollight.INL_def"
|
|
2106 |
"INJ_def" > "HOLLight.hollight.INJ_def"
|
|
2107 |
"INJ_INVERSE2" > "HOLLight.hollight.INJ_INVERSE2"
|
|
2108 |
"INJP_def" > "HOLLight.hollight.INJP_def"
|
|
2109 |
"INJP_INJ" > "HOLLight.hollight.INJP_INJ"
|
|
2110 |
"INJN_def" > "HOLLight.hollight.INJN_def"
|
|
2111 |
"INJN_INJ" > "HOLLight.hollight.INJN_INJ"
|
|
2112 |
"INJF_def" > "HOLLight.hollight.INJF_def"
|
|
2113 |
"INJF_INJ" > "HOLLight.hollight.INJF_INJ"
|
|
2114 |
"INJECTIVE_ON_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_ON_LEFT_INVERSE"
|
|
2115 |
"INJECTIVE_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
|
|
2116 |
"INJA_def" > "HOLLight.hollight.INJA_def"
|
|
2117 |
"INJA_INJ" > "HOLLight.hollight.INJA_INJ"
|
|
2118 |
"INFINITE_def" > "HOLLight.hollight.INFINITE_def"
|
|
2119 |
"INFINITE_NONEMPTY" > "HOLLight.hollight.INFINITE_NONEMPTY"
|
|
2120 |
"INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
|
|
2121 |
"INFINITE_DIFF_FINITE" > "HOLLight.hollight.INFINITE_DIFF_FINITE"
|
|
2122 |
"IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
|
|
2123 |
"IMP_CONJ" > "HOL.imp_conjL"
|
|
2124 |
"IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
|
|
2125 |
"IMAGE_o" > "HOLLight.hollight.IMAGE_o"
|
|
2126 |
"IMAGE_def" > "HOLLight.hollight.IMAGE_def"
|
|
2127 |
"IMAGE_UNION" > "HOLLight.hollight.IMAGE_UNION"
|
|
2128 |
"IMAGE_SUBSET" > "HOLLight.hollight.IMAGE_SUBSET"
|
|
2129 |
"IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
|
|
2130 |
"IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
|
|
2131 |
"IMAGE_EQ_EMPTY" > "HOLLight.hollight.IMAGE_EQ_EMPTY"
|
|
2132 |
"IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
|
|
2133 |
"IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
|
|
2134 |
"IMAGE_CONST" > "HOLLight.hollight.IMAGE_CONST"
|
|
2135 |
"IMAGE_CLAUSES" > "HOLLight.hollight.IMAGE_CLAUSES"
|
|
2136 |
"HREAL_MUL_RZERO" > "HOLLight.hollight.HREAL_MUL_RZERO"
|
|
2137 |
"HREAL_MUL_LZERO" > "HOLLight.hollight.HREAL_MUL_LZERO"
|
|
2138 |
"HREAL_LE_MUL_RCANCEL_IMP" > "HOLLight.hollight.HREAL_LE_MUL_RCANCEL_IMP"
|
|
2139 |
"HREAL_LE_EXISTS_DEF" > "HOLLight.hollight.HREAL_LE_EXISTS_DEF"
|
|
2140 |
"HREAL_LE_ADD_RCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_RCANCEL"
|
|
2141 |
"HREAL_LE_ADD_LCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_LCANCEL"
|
|
2142 |
"HREAL_LE_ADD2" > "HOLLight.hollight.HREAL_LE_ADD2"
|
|
2143 |
"HREAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_RCANCEL"
|
|
2144 |
"HREAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_LCANCEL"
|
|
2145 |
"HREAL_ADD_RID" > "HOLLight.hollight.HREAL_ADD_RID"
|
|
2146 |
"HREAL_ADD_RDISTRIB" > "HOLLight.hollight.HREAL_ADD_RDISTRIB"
|
|
2147 |
"HREAL_ADD_AC" > "HOLLight.hollight.HREAL_ADD_AC"
|
|
2148 |
"HD_def" > "HOLLight.hollight.HD_def"
|
|
2149 |
"HAS_SIZE_def" > "HOLLight.hollight.HAS_SIZE_def"
|
|
2150 |
"HAS_SIZE_UNIONS" > "HOLLight.hollight.HAS_SIZE_UNIONS"
|
|
2151 |
"HAS_SIZE_UNION" > "HOLLight.hollight.HAS_SIZE_UNION"
|
|
2152 |
"HAS_SIZE_SUC" > "HOLLight.hollight.HAS_SIZE_SUC"
|
|
2153 |
"HAS_SIZE_PRODUCT_DEPENDENT" > "HOLLight.hollight.HAS_SIZE_PRODUCT_DEPENDENT"
|
|
2154 |
"HAS_SIZE_PRODUCT" > "HOLLight.hollight.HAS_SIZE_PRODUCT"
|
|
2155 |
"HAS_SIZE_POWERSET" > "HOLLight.hollight.HAS_SIZE_POWERSET"
|
|
2156 |
"HAS_SIZE_NUMSEG_LT" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LT"
|
|
2157 |
"HAS_SIZE_NUMSEG_LE" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LE"
|
|
2158 |
"HAS_SIZE_NUMSEG_1" > "HOLLight.hollight.HAS_SIZE_NUMSEG_1"
|
|
2159 |
"HAS_SIZE_NUMSEG" > "HOLLight.hollight.HAS_SIZE_NUMSEG"
|
|
2160 |
"HAS_SIZE_INDEX" > "HOLLight.hollight.HAS_SIZE_INDEX"
|
|
2161 |
"HAS_SIZE_IMAGE_INJ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ"
|
|
2162 |
"HAS_SIZE_FUNSPACE" > "HOLLight.hollight.HAS_SIZE_FUNSPACE"
|
|
2163 |
"HAS_SIZE_FINITE_IMAGE" > "HOLLight.hollight.HAS_SIZE_FINITE_IMAGE"
|
|
2164 |
"HAS_SIZE_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
|
|
2165 |
"HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
|
|
2166 |
"HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
|
|
2167 |
"GSPEC_def" > "HOLLight.hollight.GSPEC_def"
|
|
2168 |
"GP_FINITE" > "HOLLight.hollight.GP_FINITE"
|
|
2169 |
"GP" > "HOLLight.hollight.GP"
|
|
2170 |
"GEQ_def" > "HOLLight.hollight.GEQ_def"
|
|
2171 |
"GAUGE_MIN" > "HOLLight.hollight.GAUGE_MIN"
|
|
2172 |
"GABS_def" > "HOLLight.hollight.GABS_def"
|
|
2173 |
"FUN_EQ_THM" > "Fun.expand_fun_eq"
|
|
2174 |
"FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
|
|
2175 |
"FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
|
|
2176 |
"FTC1" > "HOLLight.hollight.FTC1"
|
|
2177 |
"FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART"
|
|
2178 |
"FST" > "Product_Type.fst_conv"
|
|
2179 |
"FORALL_SIMP" > "HOL.simp_thms_35"
|
|
2180 |
"FORALL_PASTECART" > "HOLLight.hollight.FORALL_PASTECART"
|
|
2181 |
"FORALL_PAIR_THM" > "Product_Type.split_paired_All"
|
|
2182 |
"FORALL_NOT_THM" > "Inductive.basic_monos_16"
|
|
2183 |
"FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
|
|
2184 |
"FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
|
|
2185 |
"FORALL_IN_CLAUSES" > "HOLLight.hollight.FORALL_IN_CLAUSES"
|
|
2186 |
"FORALL_FINITE_INDEX" > "HOLLight.hollight.FORALL_FINITE_INDEX"
|
|
2187 |
"FORALL_BOOL_THM" > "Set.all_bool_eq"
|
|
2188 |
"FORALL_AND_THM" > "HOL.all_conj_distrib"
|
|
2189 |
"FORALL_ALL" > "HOLLight.hollight.FORALL_ALL"
|
|
2190 |
"FNIL_def" > "HOLLight.hollight.FNIL_def"
|
|
2191 |
"FINREC_def" > "HOLLight.hollight.FINREC_def"
|
|
2192 |
"FINREC_UNIQUE_LEMMA" > "HOLLight.hollight.FINREC_UNIQUE_LEMMA"
|
|
2193 |
"FINREC_SUC_LEMMA" > "HOLLight.hollight.FINREC_SUC_LEMMA"
|
|
2194 |
"FINREC_FUN_LEMMA" > "HOLLight.hollight.FINREC_FUN_LEMMA"
|
|
2195 |
"FINREC_FUN" > "HOLLight.hollight.FINREC_FUN"
|
|
2196 |
"FINREC_EXISTS_LEMMA" > "HOLLight.hollight.FINREC_EXISTS_LEMMA"
|
|
2197 |
"FINREC_1_LEMMA" > "HOLLight.hollight.FINREC_1_LEMMA"
|
|
2198 |
"FINITE_def" > "HOLLight.hollight.FINITE_def"
|
|
2199 |
"FINITE_UNION_IMP" > "HOLLight.hollight.FINITE_UNION_IMP"
|
|
2200 |
"FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
|
|
2201 |
"FINITE_UNION" > "HOLLight.hollight.FINITE_UNION"
|
|
2202 |
"FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
|
|
2203 |
"FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
|
|
2204 |
"FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
|
|
2205 |
"FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
|
|
2206 |
"FINITE_SUBSETS" > "HOLLight.hollight.FINITE_SUBSETS"
|
|
2207 |
"FINITE_SUBSET" > "HOLLight.hollight.FINITE_SUBSET"
|
|
2208 |
"FINITE_SET_OF_LIST" > "HOLLight.hollight.FINITE_SET_OF_LIST"
|
|
2209 |
"FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
|
|
2210 |
"FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
|
|
2211 |
"FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
|
|
2212 |
"FINITE_PRODUCT_DEPENDENT" > "HOLLight.hollight.FINITE_PRODUCT_DEPENDENT"
|
|
2213 |
"FINITE_PRODUCT" > "HOLLight.hollight.FINITE_PRODUCT"
|
|
2214 |
"FINITE_POWERSET" > "HOLLight.hollight.FINITE_POWERSET"
|
|
2215 |
"FINITE_NUMSEG_LT" > "HOLLight.hollight.FINITE_NUMSEG_LT"
|
|
2216 |
"FINITE_NUMSEG_LE" > "HOLLight.hollight.FINITE_NUMSEG_LE"
|
|
2217 |
"FINITE_NUMSEG" > "HOLLight.hollight.FINITE_NUMSEG"
|
|
2218 |
"FINITE_INTER" > "HOLLight.hollight.FINITE_INTER"
|
|
2219 |
"FINITE_INSERT" > "HOLLight.hollight.FINITE_INSERT"
|
|
2220 |
"FINITE_INDUCT_STRONG" > "HOLLight.hollight.FINITE_INDUCT_STRONG"
|
|
2221 |
"FINITE_INDEX_WORKS_FINITE" > "HOLLight.hollight.FINITE_INDEX_WORKS_FINITE"
|
|
2222 |
"FINITE_INDEX_WORKS" > "HOLLight.hollight.FINITE_INDEX_WORKS"
|
|
2223 |
"FINITE_INDEX_NUMSEG" > "HOLLight.hollight.FINITE_INDEX_NUMSEG"
|
|
2224 |
"FINITE_INDEX_NUMBERS" > "HOLLight.hollight.FINITE_INDEX_NUMBERS"
|
|
2225 |
"FINITE_INDEX_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
|
|
2226 |
"FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
|
|
2227 |
"FINITE_IMAGE_INJ" > "HOLLight.hollight.FINITE_IMAGE_INJ"
|
|
2228 |
"FINITE_IMAGE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE_IMAGE"
|
|
2229 |
"FINITE_IMAGE_EXPAND" > "HOLLight.hollight.FINITE_IMAGE_EXPAND"
|
|
2230 |
"FINITE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE"
|
|
2231 |
"FINITE_HAS_SIZE_LEMMA" > "HOLLight.hollight.FINITE_HAS_SIZE_LEMMA"
|
|
2232 |
"FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
|
|
2233 |
"FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
|
|
2234 |
"FINITE_DIFF" > "HOLLight.hollight.FINITE_DIFF"
|
|
2235 |
"FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
|
|
2236 |
"FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
|
|
2237 |
"FINE_MIN" > "HOLLight.hollight.FINE_MIN"
|
|
2238 |
"FILTER_def" > "HOLLight.hollight.FILTER_def"
|
|
2239 |
"FILTER_MAP" > "HOLLight.hollight.FILTER_MAP"
|
|
2240 |
"FILTER_APPEND" > "HOLLight.hollight.FILTER_APPEND"
|
|
2241 |
"FCONS_def" > "HOLLight.hollight.FCONS_def"
|
|
2242 |
"FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
|
|
2243 |
"FACT_def" > "HOLLight.hollight.FACT_def"
|
|
2244 |
"FACT_MONO" > "HOLLight.hollight.FACT_MONO"
|
|
2245 |
"FACT_LT" > "HOLLight.hollight.FACT_LT"
|
|
2246 |
"FACT_LE" > "HOLLight.hollight.FACT_LE"
|
|
2247 |
"EX_def" > "HOLLight.hollight.EX_def"
|
|
2248 |
"EX_MEM" > "HOLLight.hollight.EX_MEM"
|
|
2249 |
"EX_MAP" > "HOLLight.hollight.EX_MAP"
|
|
2250 |
"EX_IMP" > "HOLLight.hollight.EX_IMP"
|
|
2251 |
"EXTENSION" > "HOLLight.hollight.EXTENSION"
|
|
2252 |
"EXP_def" > "HOLLight.hollight.EXP_def"
|
|
2253 |
"EXP_ONE" > "HOLLight.hollight.EXP_ONE"
|
|
2254 |
"EXP_MULT" > "HOLLight.hollight.EXP_MULT"
|
|
2255 |
"EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
|
|
2256 |
"EXP_EQ_0" > "HOLLight.hollight.EXP_EQ_0"
|
|
2257 |
"EXP_ADD" > "HOLLight.hollight.EXP_ADD"
|
|
2258 |
"EXP_2" > "HOLLight.hollight.EXP_2"
|
|
2259 |
"EXP_1" > "HOLLight.hollight.EXP_1"
|
|
2260 |
"EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
|
|
2261 |
"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
|
|
2262 |
"EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
|
|
2263 |
"EXISTS_UNIQUE" > "HOL.Ex1_def"
|
|
2264 |
"EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
|
|
2265 |
"EXISTS_SIMP" > "HOL.simp_thms_36"
|
|
2266 |
"EXISTS_REFL" > "HOL.simp_thms_37"
|
|
2267 |
"EXISTS_PASTECART" > "HOLLight.hollight.EXISTS_PASTECART"
|
|
2268 |
"EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
|
|
2269 |
"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
|
|
2270 |
"EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
|
|
2271 |
"EXISTS_NOT_THM" > "Inductive.basic_monos_15"
|
|
2272 |
"EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
|
|
2273 |
"EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
|
|
2274 |
"EXISTS_EX" > "HOLLight.hollight.EXISTS_EX"
|
|
2275 |
"EXISTS_BOOL_THM" > "Set.ex_bool_eq"
|
|
2276 |
"EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
|
|
2277 |
"EVEN_def" > "HOLLight.hollight.EVEN_def"
|
|
2278 |
"EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
|
|
2279 |
"EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
|
|
2280 |
"EVEN_MULT" > "HOLLight.hollight.EVEN_MULT"
|
|
2281 |
"EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
|
|
2282 |
"EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
|
|
2283 |
"EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
|
|
2284 |
"EVEN_EXISTS" > "HOLLight.hollight.EVEN_EXISTS"
|
|
2285 |
"EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
|
|
2286 |
"EVEN_DIV2" > "HOLLight.hollight.EVEN_DIV2"
|
|
2287 |
"EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
|
|
2288 |
"EVEN_ADD" > "HOLLight.hollight.EVEN_ADD"
|
|
2289 |
"EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
|
|
2290 |
"EQ_TRANS" > "Set.basic_trans_rules_31"
|
|
2291 |
"EQ_SYM_EQ" > "HOL.eq_sym_conv"
|
|
2292 |
"EQ_SYM" > "HOL.meta_eq_to_obj_eq"
|
|
2293 |
"EQ_SUC" > "Nat.nat.simps_3"
|
|
2294 |
"EQ_REFL_T" > "HOL.simp_thms_6"
|
|
2295 |
"EQ_REFL" > "Presburger.fm_modd_pinf"
|
|
2296 |
"EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
|
|
2297 |
"EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
|
|
2298 |
"EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
|
|
2299 |
"EQ_EXT" > "HOL.meta_eq_to_obj_eq"
|
|
2300 |
"EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
|
|
2301 |
"EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
|
|
2302 |
"EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
|
|
2303 |
"EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
|
|
2304 |
"EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
|
|
2305 |
"EMPTY_def" > "HOLLight.hollight.EMPTY_def"
|
|
2306 |
"EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
|
|
2307 |
"EMPTY_UNION" > "HOLLight.hollight.EMPTY_UNION"
|
|
2308 |
"EMPTY_SUBSET" > "HOLLight.hollight.EMPTY_SUBSET"
|
|
2309 |
"EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
|
|
2310 |
"EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
|
|
2311 |
"EMPTY_DIFF" > "HOLLight.hollight.EMPTY_DIFF"
|
|
2312 |
"EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
|
|
2313 |
"EL_def" > "HOLLight.hollight.EL_def"
|
|
2314 |
"DORDER_TENDSTO" > "HOLLight.hollight.DORDER_TENDSTO"
|
|
2315 |
"DORDER_NGE" > "HOLLight.hollight.DORDER_NGE"
|
|
2316 |
"DORDER_LEMMA" > "HOLLight.hollight.DORDER_LEMMA"
|
|
2317 |
"DIV_def" > "HOLLight.hollight.DIV_def"
|
|
2318 |
"DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
|
|
2319 |
"DIV_REFL" > "HOLLight.hollight.DIV_REFL"
|
|
2320 |
"DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
|
|
2321 |
"DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
|
|
2322 |
"DIV_MULT" > "HOLLight.hollight.DIV_MULT"
|
|
2323 |
"DIV_MONO_LT" > "HOLLight.hollight.DIV_MONO_LT"
|
|
2324 |
"DIV_MONO2" > "HOLLight.hollight.DIV_MONO2"
|
|
2325 |
"DIV_MONO" > "HOLLight.hollight.DIV_MONO"
|
|
2326 |
"DIV_MOD" > "HOLLight.hollight.DIV_MOD"
|
|
2327 |
"DIV_LT" > "HOLLight.hollight.DIV_LT"
|
|
2328 |
"DIV_LE_EXCLUSION" > "HOLLight.hollight.DIV_LE_EXCLUSION"
|
|
2329 |
"DIV_LE" > "HOLLight.hollight.DIV_LE"
|
|
2330 |
"DIV_EQ_EXCLUSION" > "HOLLight.hollight.DIV_EQ_EXCLUSION"
|
|
2331 |
"DIV_EQ_0" > "HOLLight.hollight.DIV_EQ_0"
|
|
2332 |
"DIV_DIV" > "HOLLight.hollight.DIV_DIV"
|
|
2333 |
"DIV_ADD_MOD" > "HOLLight.hollight.DIV_ADD_MOD"
|
|
2334 |
"DIV_1" > "HOLLight.hollight.DIV_1"
|
|
2335 |
"DIV_0" > "HOLLight.hollight.DIV_0"
|
|
2336 |
"DIVMOD_UNIQ_LEMMA" > "HOLLight.hollight.DIVMOD_UNIQ_LEMMA"
|
|
2337 |
"DIVMOD_UNIQ" > "HOLLight.hollight.DIVMOD_UNIQ"
|
|
2338 |
"DIVMOD_EXIST_0" > "HOLLight.hollight.DIVMOD_EXIST_0"
|
|
2339 |
"DIVMOD_EXIST" > "HOLLight.hollight.DIVMOD_EXIST"
|
|
2340 |
"DIVMOD_ELIM_THM" > "HOLLight.hollight.DIVMOD_ELIM_THM"
|
|
2341 |
"DIVISION_UBOUND_LT" > "HOLLight.hollight.DIVISION_UBOUND_LT"
|
|
2342 |
"DIVISION_UBOUND" > "HOLLight.hollight.DIVISION_UBOUND"
|
|
2343 |
"DIVISION_THM" > "HOLLight.hollight.DIVISION_THM"
|
|
2344 |
"DIVISION_SINGLE" > "HOLLight.hollight.DIVISION_SINGLE"
|
|
2345 |
"DIVISION_RHS" > "HOLLight.hollight.DIVISION_RHS"
|
|
2346 |
"DIVISION_LT_GEN" > "HOLLight.hollight.DIVISION_LT_GEN"
|
|
2347 |
"DIVISION_LT" > "HOLLight.hollight.DIVISION_LT"
|
|
2348 |
"DIVISION_LHS" > "HOLLight.hollight.DIVISION_LHS"
|
|
2349 |
"DIVISION_LE" > "HOLLight.hollight.DIVISION_LE"
|
|
2350 |
"DIVISION_LBOUND_LT" > "HOLLight.hollight.DIVISION_LBOUND_LT"
|
|
2351 |
"DIVISION_LBOUND" > "HOLLight.hollight.DIVISION_LBOUND"
|
|
2352 |
"DIVISION_GT" > "HOLLight.hollight.DIVISION_GT"
|
|
2353 |
"DIVISION_EXISTS" > "HOLLight.hollight.DIVISION_EXISTS"
|
|
2354 |
"DIVISION_EQ" > "HOLLight.hollight.DIVISION_EQ"
|
|
2355 |
"DIVISION_APPEND_LEMMA2" > "HOLLight.hollight.DIVISION_APPEND_LEMMA2"
|
|
2356 |
"DIVISION_APPEND_LEMMA1" > "HOLLight.hollight.DIVISION_APPEND_LEMMA1"
|
|
2357 |
"DIVISION_APPEND" > "HOLLight.hollight.DIVISION_APPEND"
|
|
2358 |
"DIVISION_1" > "HOLLight.hollight.DIVISION_1"
|
|
2359 |
"DIVISION_0" > "HOLLight.hollight.DIVISION_0"
|
|
2360 |
"DIVISION" > "HOLLight.hollight.DIVISION"
|
|
2361 |
"DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
|
|
2362 |
"DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
|
|
2363 |
"DIST_TRIANGLE" > "HOLLight.hollight.DIST_TRIANGLE"
|
|
2364 |
"DIST_SYM" > "HOLLight.hollight.DIST_SYM"
|
|
2365 |
"DIST_RZERO" > "HOLLight.hollight.DIST_RZERO"
|
|
2366 |
"DIST_RMUL" > "HOLLight.hollight.DIST_RMUL"
|
|
2367 |
"DIST_REFL" > "HOLLight.hollight.DIST_REFL"
|
|
2368 |
"DIST_RADD_0" > "HOLLight.hollight.DIST_RADD_0"
|
|
2369 |
"DIST_RADD" > "HOLLight.hollight.DIST_RADD"
|
|
2370 |
"DIST_LZERO" > "HOLLight.hollight.DIST_LZERO"
|
|
2371 |
"DIST_LMUL" > "HOLLight.hollight.DIST_LMUL"
|
|
2372 |
"DIST_LE_CASES" > "HOLLight.hollight.DIST_LE_CASES"
|
|
2373 |
"DIST_LADD_0" > "HOLLight.hollight.DIST_LADD_0"
|
|
2374 |
"DIST_LADD" > "HOLLight.hollight.DIST_LADD"
|
|
2375 |
"DIST_EQ_0" > "HOLLight.hollight.DIST_EQ_0"
|
|
2376 |
"DIST_ELIM_THM" > "HOLLight.hollight.DIST_ELIM_THM"
|
|
2377 |
"DIST_ADDBOUND" > "HOLLight.hollight.DIST_ADDBOUND"
|
|
2378 |
"DIST_ADD2_REV" > "HOLLight.hollight.DIST_ADD2_REV"
|
|
2379 |
"DIST_ADD2" > "HOLLight.hollight.DIST_ADD2"
|
|
2380 |
"DISJ_SYM" > "HOL.disj_comms_1"
|
|
2381 |
"DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
|
|
2382 |
"DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
|
|
2383 |
"DISJOINT_def" > "HOLLight.hollight.DISJOINT_def"
|
|
2384 |
"DISJOINT_UNION" > "HOLLight.hollight.DISJOINT_UNION"
|
|
2385 |
"DISJOINT_SYM" > "HOLLight.hollight.DISJOINT_SYM"
|
|
2386 |
"DISJOINT_NUMSEG" > "HOLLight.hollight.DISJOINT_NUMSEG"
|
|
2387 |
"DISJOINT_INSERT" > "HOLLight.hollight.DISJOINT_INSERT"
|
|
2388 |
"DISJOINT_EMPTY_REFL" > "HOLLight.hollight.DISJOINT_EMPTY_REFL"
|
|
2389 |
"DISJOINT_EMPTY" > "HOLLight.hollight.DISJOINT_EMPTY"
|
|
2390 |
"DISJOINT_DELETE_SYM" > "HOLLight.hollight.DISJOINT_DELETE_SYM"
|
|
2391 |
"DINT_UNIQ" > "HOLLight.hollight.DINT_UNIQ"
|
|
2392 |
"DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
|
|
2393 |
"DIMINDEX_HAS_SIZE_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_HAS_SIZE_FINITE_SUM"
|
|
2394 |
"DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
|
|
2395 |
"DIMINDEX_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_FINITE_SUM"
|
|
2396 |
"DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
|
|
2397 |
"DIFF_def" > "HOLLight.hollight.DIFF_def"
|
|
2398 |
"DIFF_XM1" > "HOLLight.hollight.DIFF_XM1"
|
|
2399 |
"DIFF_X" > "HOLLight.hollight.DIFF_X"
|
|
2400 |
"DIFF_UNIV" > "HOLLight.hollight.DIFF_UNIV"
|
|
2401 |
"DIFF_UNIQ" > "HOLLight.hollight.DIFF_UNIQ"
|
|
2402 |
"DIFF_TAN_COMPOSITE" > "HOLLight.hollight.DIFF_TAN_COMPOSITE"
|
|
2403 |
"DIFF_TAN" > "HOLLight.hollight.DIFF_TAN"
|
|
2404 |
"DIFF_SUM" > "HOLLight.hollight.DIFF_SUM"
|
|
2405 |
"DIFF_SUB" > "HOLLight.hollight.DIFF_SUB"
|
|
2406 |
"DIFF_SIN" > "HOLLight.hollight.DIFF_SIN"
|
|
2407 |
"DIFF_POW" > "HOLLight.hollight.DIFF_POW"
|
|
2408 |
"DIFF_NEG" > "HOLLight.hollight.DIFF_NEG"
|
|
2409 |
"DIFF_MUL" > "HOLLight.hollight.DIFF_MUL"
|
|
2410 |
"DIFF_LN_COMPOSITE" > "HOLLight.hollight.DIFF_LN_COMPOSITE"
|
|
2411 |
"DIFF_LN" > "HOLLight.hollight.DIFF_LN"
|
|
2412 |
"DIFF_LMIN" > "HOLLight.hollight.DIFF_LMIN"
|
|
2413 |
"DIFF_LMAX" > "HOLLight.hollight.DIFF_LMAX"
|
|
2414 |
"DIFF_LINC" > "HOLLight.hollight.DIFF_LINC"
|
|
2415 |
"DIFF_LDEC" > "HOLLight.hollight.DIFF_LDEC"
|
|
2416 |
"DIFF_LCONST" > "HOLLight.hollight.DIFF_LCONST"
|
|
2417 |
"DIFF_ISCONST_END_SIMPLE" > "HOLLight.hollight.DIFF_ISCONST_END_SIMPLE"
|
|
2418 |
"DIFF_ISCONST_END" > "HOLLight.hollight.DIFF_ISCONST_END"
|
|
2419 |
"DIFF_ISCONST_ALL" > "HOLLight.hollight.DIFF_ISCONST_ALL"
|
|
2420 |
"DIFF_ISCONST" > "HOLLight.hollight.DIFF_ISCONST"
|
|
2421 |
"DIFF_INVERSE_LT" > "HOLLight.hollight.DIFF_INVERSE_LT"
|
|
2422 |
"DIFF_INVERSE" > "HOLLight.hollight.DIFF_INVERSE"
|
|
2423 |
"DIFF_INV" > "HOLLight.hollight.DIFF_INV"
|
|
2424 |
"DIFF_INSERT" > "HOLLight.hollight.DIFF_INSERT"
|
|
2425 |
"DIFF_EXP" > "HOLLight.hollight.DIFF_EXP"
|
|
2426 |
"DIFF_EQ_EMPTY" > "HOLLight.hollight.DIFF_EQ_EMPTY"
|
|
2427 |
"DIFF_EMPTY" > "HOLLight.hollight.DIFF_EMPTY"
|
|
2428 |
"DIFF_DIV" > "HOLLight.hollight.DIFF_DIV"
|
|
2429 |
"DIFF_DIFF" > "HOLLight.hollight.DIFF_DIFF"
|
|
2430 |
"DIFF_COS" > "HOLLight.hollight.DIFF_COS"
|
|
2431 |
"DIFF_CONT" > "HOLLight.hollight.DIFF_CONT"
|
|
2432 |
"DIFF_CONST" > "HOLLight.hollight.DIFF_CONST"
|
|
2433 |
"DIFF_COMPOSITE" > "HOLLight.hollight.DIFF_COMPOSITE"
|
|
2434 |
"DIFF_CMUL" > "HOLLight.hollight.DIFF_CMUL"
|
|
2435 |
"DIFF_CHAIN" > "HOLLight.hollight.DIFF_CHAIN"
|
|
2436 |
"DIFF_CARAT" > "HOLLight.hollight.DIFF_CARAT"
|
|
2437 |
"DIFF_ATN_COMPOSITE" > "HOLLight.hollight.DIFF_ATN_COMPOSITE"
|
|
2438 |
"DIFF_ATN" > "HOLLight.hollight.DIFF_ATN"
|
|
2439 |
"DIFF_ASN_COS" > "HOLLight.hollight.DIFF_ASN_COS"
|
|
2440 |
"DIFF_ASN" > "HOLLight.hollight.DIFF_ASN"
|
|
2441 |
"DIFF_ADD" > "HOLLight.hollight.DIFF_ADD"
|
|
2442 |
"DIFF_ACS_SIN" > "HOLLight.hollight.DIFF_ACS_SIN"
|
|
2443 |
"DIFF_ACS" > "HOLLight.hollight.DIFF_ACS"
|
|
2444 |
"DIFFS_NEG" > "HOLLight.hollight.DIFFS_NEG"
|
|
2445 |
"DIFFS_LEMMA2" > "HOLLight.hollight.DIFFS_LEMMA2"
|
|
2446 |
"DIFFS_LEMMA" > "HOLLight.hollight.DIFFS_LEMMA"
|
|
2447 |
"DIFFS_EQUIV" > "HOLLight.hollight.DIFFS_EQUIV"
|
|
2448 |
"DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
|
|
2449 |
"DELETE_def" > "HOLLight.hollight.DELETE_def"
|
|
2450 |
"DELETE_SUBSET" > "HOLLight.hollight.DELETE_SUBSET"
|
|
2451 |
"DELETE_NON_ELEMENT" > "HOLLight.hollight.DELETE_NON_ELEMENT"
|
|
2452 |
"DELETE_INTER" > "HOLLight.hollight.DELETE_INTER"
|
|
2453 |
"DELETE_INSERT" > "HOLLight.hollight.DELETE_INSERT"
|
|
2454 |
"DELETE_DELETE" > "HOLLight.hollight.DELETE_DELETE"
|
|
2455 |
"DELETE_COMM" > "HOLLight.hollight.DELETE_COMM"
|
|
2456 |
"DEF_~" > "HOL.simp_thms_19"
|
|
2457 |
"DEF_two_2" > "HOLLight.hollight.DEF_two_2"
|
|
2458 |
"DEF_two_1" > "HOLLight.hollight.DEF_two_1"
|
|
2459 |
"DEF_treal_of_num" > "HOLLight.hollight.DEF_treal_of_num"
|
|
2460 |
"DEF_treal_neg" > "HOLLight.hollight.DEF_treal_neg"
|
|
2461 |
"DEF_treal_mul" > "HOLLight.hollight.DEF_treal_mul"
|
|
2462 |
"DEF_treal_le" > "HOLLight.hollight.DEF_treal_le"
|
|
2463 |
"DEF_treal_inv" > "HOLLight.hollight.DEF_treal_inv"
|
|
2464 |
"DEF_treal_eq" > "HOLLight.hollight.DEF_treal_eq"
|
|
2465 |
"DEF_treal_add" > "HOLLight.hollight.DEF_treal_add"
|
|
2466 |
"DEF_three_3" > "HOLLight.hollight.DEF_three_3"
|
|
2467 |
"DEF_three_2" > "HOLLight.hollight.DEF_three_2"
|
|
2468 |
"DEF_three_1" > "HOLLight.hollight.DEF_three_1"
|
|
2469 |
"DEF_tendsto" > "HOLLight.hollight.DEF_tendsto"
|
|
2470 |
"DEF_tends_real_real" > "HOLLight.hollight.DEF_tends_real_real"
|
|
2471 |
"DEF_tends_num_real" > "HOLLight.hollight.DEF_tends_num_real"
|
|
2472 |
"DEF_tends" > "HOLLight.hollight.DEF_tends"
|
|
2473 |
"DEF_tdiv" > "HOLLight.hollight.DEF_tdiv"
|
|
2474 |
"DEF_tan" > "HOLLight.hollight.DEF_tan"
|
|
2475 |
"DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
|
|
2476 |
"DEF_support" > "HOLLight.hollight.DEF_support"
|
|
2477 |
"DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
|
|
2478 |
"DEF_sup" > "HOLLight.hollight.DEF_sup"
|
|
2479 |
"DEF_sums" > "HOLLight.hollight.DEF_sums"
|
|
2480 |
"DEF_summable" > "HOLLight.hollight.DEF_summable"
|
|
2481 |
"DEF_suminf" > "HOLLight.hollight.DEF_suminf"
|
|
2482 |
"DEF_sum" > "HOLLight.hollight.DEF_sum"
|
|
2483 |
"DEF_subseq" > "HOLLight.hollight.DEF_subseq"
|
|
2484 |
"DEF_sqrt" > "HOLLight.hollight.DEF_sqrt"
|
|
2485 |
"DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
|
|
2486 |
"DEF_sin" > "HOLLight.hollight.DEF_sin"
|
|
2487 |
"DEF_set_of_list" > "HOLLight.hollight.DEF_set_of_list"
|
|
2488 |
"DEF_rsum" > "HOLLight.hollight.DEF_rsum"
|
|
2489 |
"DEF_root" > "HOLLight.hollight.DEF_root"
|
|
2490 |
"DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
|
|
2491 |
"DEF_real_pow" > "HOLLight.hollight.DEF_real_pow"
|
|
2492 |
"DEF_real_of_num" > "HOLLight.hollight.DEF_real_of_num"
|
|
2493 |
"DEF_real_neg" > "HOLLight.hollight.DEF_real_neg"
|
|
2494 |
"DEF_real_mul" > "HOLLight.hollight.DEF_real_mul"
|
|
2495 |
"DEF_real_min" > "HOLLight.hollight.DEF_real_min"
|
|
2496 |
"DEF_real_max" > "HOLLight.hollight.DEF_real_max"
|
|
2497 |
"DEF_real_lt" > "HOLLight.hollight.DEF_real_lt"
|
|
2498 |
"DEF_real_le" > "HOLLight.hollight.DEF_real_le"
|
|
2499 |
"DEF_real_inv" > "HOLLight.hollight.DEF_real_inv"
|
|
2500 |
"DEF_real_gt" > "HOLLight.hollight.DEF_real_gt"
|
|
2501 |
"DEF_real_ge" > "HOLLight.hollight.DEF_real_ge"
|
|
2502 |
"DEF_real_div" > "HOLLight.hollight.DEF_real_div"
|
|
2503 |
"DEF_real_add" > "HOLLight.hollight.DEF_real_add"
|
|
2504 |
"DEF_real_abs" > "HOLLight.hollight.DEF_real_abs"
|
|
2505 |
"DEF_re_universe" > "HOLLight.hollight.DEF_re_universe"
|
|
2506 |
"DEF_re_union" > "HOLLight.hollight.DEF_re_union"
|
|
2507 |
"DEF_re_subset" > "HOLLight.hollight.DEF_re_subset"
|
|
2508 |
"DEF_re_null" > "HOLLight.hollight.DEF_re_null"
|
|
2509 |
"DEF_re_intersect" > "HOLLight.hollight.DEF_re_intersect"
|
|
2510 |
"DEF_re_compl" > "HOLLight.hollight.DEF_re_compl"
|
|
2511 |
"DEF_re_Union" > "HOLLight.hollight.DEF_re_Union"
|
|
2512 |
"DEF_psum" > "HOLLight.hollight.DEF_psum"
|
|
2513 |
"DEF_pi" > "HOLLight.hollight.DEF_pi"
|
|
2514 |
"DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
|
|
2515 |
"DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
|
|
2516 |
"DEF_o" > "Fun.o_apply"
|
|
2517 |
"DEF_nsum" > "HOLLight.hollight.DEF_nsum"
|
|
2518 |
"DEF_neutral" > "HOLLight.hollight.DEF_neutral"
|
|
2519 |
"DEF_neigh" > "HOLLight.hollight.DEF_neigh"
|
|
2520 |
"DEF_nadd_rinv" > "HOLLight.hollight.DEF_nadd_rinv"
|
|
2521 |
"DEF_nadd_of_num" > "HOLLight.hollight.DEF_nadd_of_num"
|
|
2522 |
"DEF_nadd_mul" > "HOLLight.hollight.DEF_nadd_mul"
|
|
2523 |
"DEF_nadd_le" > "HOLLight.hollight.DEF_nadd_le"
|
|
2524 |
"DEF_nadd_inv" > "HOLLight.hollight.DEF_nadd_inv"
|
|
2525 |
"DEF_nadd_eq" > "HOLLight.hollight.DEF_nadd_eq"
|
|
2526 |
"DEF_nadd_add" > "HOLLight.hollight.DEF_nadd_add"
|
|
2527 |
"DEF_mtop" > "HOLLight.hollight.DEF_mtop"
|
|
2528 |
"DEF_mr1" > "HOLLight.hollight.DEF_mr1"
|
|
2529 |
"DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
|
|
2530 |
"DEF_mono" > "HOLLight.hollight.DEF_mono"
|
|
2531 |
"DEF_mod_real" > "HOLLight.hollight.DEF_mod_real"
|
|
2532 |
"DEF_mod_nat" > "HOLLight.hollight.DEF_mod_nat"
|
|
2533 |
"DEF_mod_int" > "HOLLight.hollight.DEF_mod_int"
|
|
2534 |
"DEF_mk_pair" > "Product_Type.Pair_Rep_def"
|
|
2535 |
"DEF_minimal" > "HOLLight.hollight.DEF_minimal"
|
|
2536 |
"DEF_measure" > "HOLLight.hollight.DEF_measure"
|
|
2537 |
"DEF_ln" > "HOLLight.hollight.DEF_ln"
|
|
2538 |
"DEF_list_of_set" > "HOLLight.hollight.DEF_list_of_set"
|
|
2539 |
"DEF_limpt" > "HOLLight.hollight.DEF_limpt"
|
|
2540 |
"DEF_lim" > "HOLLight.hollight.DEF_lim"
|
|
2541 |
"DEF_lambda" > "HOLLight.hollight.DEF_lambda"
|
|
2542 |
"DEF_iterate" > "HOLLight.hollight.DEF_iterate"
|
|
2543 |
"DEF_istopology" > "HOLLight.hollight.DEF_istopology"
|
|
2544 |
"DEF_ismet" > "HOLLight.hollight.DEF_ismet"
|
|
2545 |
"DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
|
|
2546 |
"DEF_is_int" > "HOLLight.hollight.DEF_is_int"
|
|
2547 |
"DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
|
|
2548 |
"DEF_int_pow" > "HOLLight.hollight.DEF_int_pow"
|
|
2549 |
"DEF_int_of_num" > "HOLLight.hollight.DEF_int_of_num"
|
|
2550 |
"DEF_int_neg" > "HOLLight.hollight.DEF_int_neg"
|
|
2551 |
"DEF_int_mul" > "HOLLight.hollight.DEF_int_mul"
|
|
2552 |
"DEF_int_min" > "HOLLight.hollight.DEF_int_min"
|
|
2553 |
"DEF_int_max" > "HOLLight.hollight.DEF_int_max"
|
|
2554 |
"DEF_int_lt" > "HOLLight.hollight.DEF_int_lt"
|
|
2555 |
"DEF_int_le" > "HOLLight.hollight.DEF_int_le"
|
|
2556 |
"DEF_int_gt" > "HOLLight.hollight.DEF_int_gt"
|
|
2557 |
"DEF_int_ge" > "HOLLight.hollight.DEF_int_ge"
|
|
2558 |
"DEF_int_add" > "HOLLight.hollight.DEF_int_add"
|
|
2559 |
"DEF_int_abs" > "HOLLight.hollight.DEF_int_abs"
|
|
2560 |
"DEF_hreal_of_num" > "HOLLight.hollight.DEF_hreal_of_num"
|
|
2561 |
"DEF_hreal_mul" > "HOLLight.hollight.DEF_hreal_mul"
|
|
2562 |
"DEF_hreal_le" > "HOLLight.hollight.DEF_hreal_le"
|
|
2563 |
"DEF_hreal_inv" > "HOLLight.hollight.DEF_hreal_inv"
|
|
2564 |
"DEF_hreal_add" > "HOLLight.hollight.DEF_hreal_add"
|
|
2565 |
"DEF_gauge" > "HOLLight.hollight.DEF_gauge"
|
|
2566 |
"DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
|
|
2567 |
"DEF_finite_index" > "HOLLight.hollight.DEF_finite_index"
|
|
2568 |
"DEF_fine" > "HOLLight.hollight.DEF_fine"
|
|
2569 |
"DEF_exp" > "HOLLight.hollight.DEF_exp"
|
|
2570 |
"DEF_dsize" > "HOLLight.hollight.DEF_dsize"
|
|
2571 |
"DEF_dorder" > "HOLLight.hollight.DEF_dorder"
|
|
2572 |
"DEF_division" > "HOLLight.hollight.DEF_division"
|
|
2573 |
"DEF_dist" > "HOLLight.hollight.DEF_dist"
|
|
2574 |
"DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
|
|
2575 |
"DEF_diffs" > "HOLLight.hollight.DEF_diffs"
|
|
2576 |
"DEF_diffl" > "HOLLight.hollight.DEF_diffl"
|
|
2577 |
"DEF_differentiable" > "HOLLight.hollight.DEF_differentiable"
|
|
2578 |
"DEF_defint" > "HOLLight.hollight.DEF_defint"
|
|
2579 |
"DEF_cos" > "HOLLight.hollight.DEF_cos"
|
|
2580 |
"DEF_convergent" > "HOLLight.hollight.DEF_convergent"
|
|
2581 |
"DEF_contl" > "HOLLight.hollight.DEF_contl"
|
|
2582 |
"DEF_closed" > "HOLLight.hollight.DEF_closed"
|
|
2583 |
"DEF_cauchy" > "HOLLight.hollight.DEF_cauchy"
|
|
2584 |
"DEF_bounded" > "HOLLight.hollight.DEF_bounded"
|
|
2585 |
"DEF_ball" > "HOLLight.hollight.DEF_ball"
|
|
2586 |
"DEF_atn" > "HOLLight.hollight.DEF_atn"
|
|
2587 |
"DEF_asn" > "HOLLight.hollight.DEF_asn"
|
|
2588 |
"DEF_admissible" > "HOLLight.hollight.DEF_admissible"
|
|
2589 |
"DEF_acs" > "HOLLight.hollight.DEF_acs"
|
|
2590 |
"DEF__star_" > "HOLLightCompat.mult_altdef"
|
|
2591 |
"DEF__slash__backslash_" > "HOLLightCompat.light_and_def"
|
|
2592 |
"DEF__questionmark__exclamationmark_" > "HOL4Compat.EXISTS_UNIQUE_DEF"
|
|
2593 |
"DEF__questionmark_" > "HOL.Ex_def"
|
|
2594 |
"DEF__lessthan__equal_" > "HOLLight.hollight.DEF__lessthan__equal_"
|
|
2595 |
"DEF__lessthan_" > "HOLLight.hollight.DEF__lessthan_"
|
|
2596 |
"DEF__greaterthan__equal_" > "HOLLight.hollight.DEF__greaterthan__equal_"
|
|
2597 |
"DEF__greaterthan_" > "HOLLight.hollight.DEF__greaterthan_"
|
|
2598 |
"DEF__exclamationmark_" > "HOL.All_def"
|
|
2599 |
"DEF__equal__equal__greaterthan_" > "HOLLightCompat.light_imp_def"
|
|
2600 |
"DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
|
|
2601 |
"DEF__dot__dot_" > "HOLLight.hollight.DEF__dot__dot_"
|
|
2602 |
"DEF__backslash__slash_" > "HOL.or_def"
|
|
2603 |
"DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
|
|
2604 |
"DEF__10314" > "HOLLight.hollight.DEF__10314"
|
|
2605 |
"DEF__10313" > "HOLLight.hollight.DEF__10313"
|
|
2606 |
"DEF__10312" > "HOLLight.hollight.DEF__10312"
|
|
2607 |
"DEF__10289" > "HOLLight.hollight.DEF__10289"
|
|
2608 |
"DEF__10288" > "HOLLight.hollight.DEF__10288"
|
|
2609 |
"DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
|
|
2610 |
"DEF_ZIP" > "HOLLight.hollight.DEF_ZIP"
|
|
2611 |
"DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
|
|
2612 |
"DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
|
|
2613 |
"DEF_WF" > "HOLLight.hollight.DEF_WF"
|
|
2614 |
"DEF_UNIV" > "HOLLight.hollight.DEF_UNIV"
|
|
2615 |
"DEF_UNIONS" > "HOLLight.hollight.DEF_UNIONS"
|
|
2616 |
"DEF_UNION" > "HOLLight.hollight.DEF_UNION"
|
|
2617 |
"DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
|
|
2618 |
"DEF_TL" > "HOLLight.hollight.DEF_TL"
|
|
2619 |
"DEF_T" > "HOL.True_def"
|
|
2620 |
"DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
|
|
2621 |
"DEF_SUBSET" > "HOLLight.hollight.DEF_SUBSET"
|
|
2622 |
"DEF_SOME" > "HOLLight.hollight.DEF_SOME"
|
|
2623 |
"DEF_SND" > "HOLLightCompat.snd_altdef"
|
|
2624 |
"DEF_SING" > "HOLLight.hollight.DEF_SING"
|
|
2625 |
"DEF_SETSPEC" > "HOLLight.hollight.DEF_SETSPEC"
|
|
2626 |
"DEF_REVERSE" > "HOLLight.hollight.DEF_REVERSE"
|
|
2627 |
"DEF_REST" > "HOLLight.hollight.DEF_REST"
|
|
2628 |
"DEF_REPLICATE" > "HOLLight.hollight.DEF_REPLICATE"
|
|
2629 |
"DEF_PSUBSET" > "HOLLight.hollight.DEF_PSUBSET"
|
|
2630 |
"DEF_PRE" > "HOLLightCompat.Pred_altdef"
|
|
2631 |
"DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
|
|
2632 |
"DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
|
|
2633 |
"DEF_OUTR" > "HOLLight.hollight.DEF_OUTR"
|
|
2634 |
"DEF_OUTL" > "HOLLight.hollight.DEF_OUTL"
|
|
2635 |
"DEF_ONTO" > "Fun.surj_def"
|
|
2636 |
"DEF_ONE_ONE" > "HOL4Setup.ONE_ONE_DEF"
|
|
2637 |
"DEF_ODD" > "HOLLight.hollight.DEF_ODD"
|
|
2638 |
"DEF_NUMSUM" > "HOLLight.hollight.DEF_NUMSUM"
|
|
2639 |
"DEF_NUMSND" > "HOLLight.hollight.DEF_NUMSND"
|
|
2640 |
"DEF_NUMRIGHT" > "HOLLight.hollight.DEF_NUMRIGHT"
|
|
2641 |
"DEF_NUMPAIR" > "HOLLight.hollight.DEF_NUMPAIR"
|
|
2642 |
"DEF_NUMLEFT" > "HOLLight.hollight.DEF_NUMLEFT"
|
|
2643 |
"DEF_NUMFST" > "HOLLight.hollight.DEF_NUMFST"
|
|
2644 |
"DEF_NUMERAL" > "HOLLightCompat.NUMERAL_rew"
|
|
2645 |
"DEF_NULL" > "HOLLight.hollight.DEF_NULL"
|
|
2646 |
"DEF_NONE" > "HOLLight.hollight.DEF_NONE"
|
|
2647 |
"DEF_NIL" > "HOLLight.hollight.DEF_NIL"
|
|
2648 |
"DEF_MOD" > "HOLLight.hollight.DEF_MOD"
|
|
2649 |
"DEF_MEM" > "HOLLight.hollight.DEF_MEM"
|
|
2650 |
"DEF_MAP2" > "HOLLight.hollight.DEF_MAP2"
|
|
2651 |
"DEF_MAP" > "HOLLight.hollight.DEF_MAP"
|
|
2652 |
"DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
|
|
2653 |
"DEF_LET" > "HOL4Compat.LET_def"
|
|
2654 |
"DEF_LENGTH" > "HOLLight.hollight.DEF_LENGTH"
|
|
2655 |
"DEF_LAST" > "HOLLight.hollight.DEF_LAST"
|
|
2656 |
"DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
|
|
2657 |
"DEF_ITLIST2" > "HOLLight.hollight.DEF_ITLIST2"
|
|
2658 |
"DEF_ITLIST" > "HOLLight.hollight.DEF_ITLIST"
|
|
2659 |
"DEF_ISO" > "HOLLight.hollight.DEF_ISO"
|
|
2660 |
"DEF_INTERS" > "HOLLight.hollight.DEF_INTERS"
|
|
2661 |
"DEF_INTER" > "HOLLight.hollight.DEF_INTER"
|
|
2662 |
"DEF_INSERT" > "HOLLight.hollight.DEF_INSERT"
|
|
2663 |
"DEF_INR" > "HOLLight.hollight.DEF_INR"
|
|
2664 |
"DEF_INL" > "HOLLight.hollight.DEF_INL"
|
|
2665 |
"DEF_INJP" > "HOLLight.hollight.DEF_INJP"
|
|
2666 |
"DEF_INJN" > "HOLLight.hollight.DEF_INJN"
|
|
2667 |
"DEF_INJF" > "HOLLight.hollight.DEF_INJF"
|
|
2668 |
"DEF_INJA" > "HOLLight.hollight.DEF_INJA"
|
|
2669 |
"DEF_INJ" > "HOLLight.hollight.DEF_INJ"
|
|
2670 |
"DEF_INFINITE" > "HOLLight.hollight.DEF_INFINITE"
|
|
2671 |
"DEF_IN" > "HOLLight.hollight.DEF_IN"
|
|
2672 |
"DEF_IMAGE" > "HOLLight.hollight.DEF_IMAGE"
|
|
2673 |
"DEF_I" > "Fun.id_apply"
|
|
2674 |
"DEF_HD" > "HOLLight.hollight.DEF_HD"
|
|
2675 |
"DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
|
|
2676 |
"DEF_GSPEC" > "HOLLight.hollight.DEF_GSPEC"
|
|
2677 |
"DEF_GEQ" > "HOLLight.hollight.DEF_GEQ"
|
|
2678 |
"DEF_GABS" > "HOLLight.hollight.DEF_GABS"
|
|
2679 |
"DEF_FST" > "HOLLightCompat.fst_altdef"
|
|
2680 |
"DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
|
|
2681 |
"DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
|
|
2682 |
"DEF_FINITE" > "HOLLight.hollight.DEF_FINITE"
|
|
2683 |
"DEF_FILTER" > "HOLLight.hollight.DEF_FILTER"
|
|
2684 |
"DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
|
|
2685 |
"DEF_FACT" > "HOLLight.hollight.DEF_FACT"
|
|
2686 |
"DEF_F" > "HOL.False_def"
|
|
2687 |
"DEF_EXP" > "HOLLight.hollight.DEF_EXP"
|
|
2688 |
"DEF_EX" > "HOLLight.hollight.DEF_EX"
|
|
2689 |
"DEF_EVEN" > "HOLLight.hollight.DEF_EVEN"
|
|
2690 |
"DEF_EMPTY" > "HOLLight.hollight.DEF_EMPTY"
|
|
2691 |
"DEF_EL" > "HOLLight.hollight.DEF_EL"
|
|
2692 |
"DEF_DIV" > "HOLLight.hollight.DEF_DIV"
|
|
2693 |
"DEF_DISJOINT" > "HOLLight.hollight.DEF_DISJOINT"
|
|
2694 |
"DEF_DIFF" > "HOLLight.hollight.DEF_DIFF"
|
|
2695 |
"DEF_DELETE" > "HOLLight.hollight.DEF_DELETE"
|
|
2696 |
"DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
|
|
2697 |
"DEF_CURRY" > "HOLLight.hollight.DEF_CURRY"
|
|
2698 |
"DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
|
|
2699 |
"DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
|
|
2700 |
"DEF_CONS" > "HOLLight.hollight.DEF_CONS"
|
|
2701 |
"DEF_COND" > "HOLLight.hollight.DEF_COND"
|
|
2702 |
"DEF_CHOICE" > "HOLLight.hollight.DEF_CHOICE"
|
|
2703 |
"DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
|
|
2704 |
"DEF_CARD_LT" > "HOLLight.hollight.DEF_CARD_LT"
|
|
2705 |
"DEF_CARD_LE" > "HOLLight.hollight.DEF_CARD_LE"
|
|
2706 |
"DEF_CARD_GT" > "HOLLight.hollight.DEF_CARD_GT"
|
|
2707 |
"DEF_CARD_GE" > "HOLLight.hollight.DEF_CARD_GE"
|
|
2708 |
"DEF_CARD_EQ" > "HOLLight.hollight.DEF_CARD_EQ"
|
|
2709 |
"DEF_CARD" > "HOLLight.hollight.DEF_CARD"
|
|
2710 |
"DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
|
|
2711 |
"DEF_BIT1" > "HOLLightCompat.NUMERAL_BIT1_altdef"
|
|
2712 |
"DEF_BIT0" > "HOLLightCompat.NUMERAL_BIT0_def"
|
|
2713 |
"DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
|
|
2714 |
"DEF_ASSOC" > "HOLLight.hollight.DEF_ASSOC"
|
|
2715 |
"DEF_APPEND" > "HOLLight.hollight.DEF_APPEND"
|
|
2716 |
"DEF_ALL2" > "HOLLight.hollight.DEF_ALL2"
|
|
2717 |
"DEF_ALL" > "HOLLight.hollight.DEF_ALL"
|
|
2718 |
"DEF_-" > "HOLLightCompat.sub_altdef"
|
|
2719 |
"DEF_," > "Product_Type.Pair_def"
|
|
2720 |
"DEF_+" > "HOLLightCompat.add_altdef"
|
|
2721 |
"DEF_$" > "HOLLight.hollight.DEF_$"
|
|
2722 |
"DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
|
|
2723 |
"DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
|
|
2724 |
"CURRY_def" > "HOLLight.hollight.CURRY_def"
|
|
2725 |
"COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
|
|
2726 |
"COS_ZERO_LEMMA" > "HOLLight.hollight.COS_ZERO_LEMMA"
|
|
2727 |
"COS_ZERO" > "HOLLight.hollight.COS_ZERO"
|
|
2728 |
"COS_TOTAL" > "HOLLight.hollight.COS_TOTAL"
|
|
2729 |
"COS_SIN_SQRT" > "HOLLight.hollight.COS_SIN_SQRT"
|
|
2730 |
"COS_SIN" > "HOLLight.hollight.COS_SIN"
|
|
2731 |
"COS_POS_PI2" > "HOLLight.hollight.COS_POS_PI2"
|
|
2732 |
"COS_POS_PI" > "HOLLight.hollight.COS_POS_PI"
|
|
2733 |
"COS_PI2" > "HOLLight.hollight.COS_PI2"
|
|
2734 |
"COS_PI" > "HOLLight.hollight.COS_PI"
|
|
2735 |
"COS_PERIODIC_PI" > "HOLLight.hollight.COS_PERIODIC_PI"
|
|
2736 |
"COS_PERIODIC" > "HOLLight.hollight.COS_PERIODIC"
|
|
2737 |
"COS_PAIRED" > "HOLLight.hollight.COS_PAIRED"
|
|
2738 |
"COS_ONE_2PI" > "HOLLight.hollight.COS_ONE_2PI"
|
|
2739 |
"COS_NPI" > "HOLLight.hollight.COS_NPI"
|
|
2740 |
"COS_NEG" > "HOLLight.hollight.COS_NEG"
|
|
2741 |
"COS_ISZERO" > "HOLLight.hollight.COS_ISZERO"
|
|
2742 |
"COS_FDIFF" > "HOLLight.hollight.COS_FDIFF"
|
|
2743 |
"COS_DOUBLE" > "HOLLight.hollight.COS_DOUBLE"
|
|
2744 |
"COS_CONVERGES" > "HOLLight.hollight.COS_CONVERGES"
|
|
2745 |
"COS_BOUNDS" > "HOLLight.hollight.COS_BOUNDS"
|
|
2746 |
"COS_BOUND" > "HOLLight.hollight.COS_BOUND"
|
|
2747 |
"COS_ATN_NZ" > "HOLLight.hollight.COS_ATN_NZ"
|
|
2748 |
"COS_ASN_NZ" > "HOLLight.hollight.COS_ASN_NZ"
|
|
2749 |
"COS_ADD" > "HOLLight.hollight.COS_ADD"
|
|
2750 |
"COS_ACS" > "HOLLight.hollight.COS_ACS"
|
|
2751 |
"COS_ABS" > "HOLLight.hollight.COS_ABS"
|
|
2752 |
"COS_2" > "HOLLight.hollight.COS_2"
|
|
2753 |
"COS_0" > "HOLLight.hollight.COS_0"
|
|
2754 |
"CONT_X" > "HOLLight.hollight.CONT_X"
|
|
2755 |
"CONT_SUB" > "HOLLight.hollight.CONT_SUB"
|
|
2756 |
"CONT_NEG" > "HOLLight.hollight.CONT_NEG"
|
|
2757 |
"CONT_MUL" > "HOLLight.hollight.CONT_MUL"
|
|
2758 |
"CONT_INVERSE" > "HOLLight.hollight.CONT_INVERSE"
|
|
2759 |
"CONT_INV" > "HOLLight.hollight.CONT_INV"
|
|
2760 |
"CONT_INJ_RANGE" > "HOLLight.hollight.CONT_INJ_RANGE"
|
|
2761 |
"CONT_INJ_LEMMA2" > "HOLLight.hollight.CONT_INJ_LEMMA2"
|
|
2762 |
"CONT_INJ_LEMMA" > "HOLLight.hollight.CONT_INJ_LEMMA"
|
|
2763 |
"CONT_HASSUP" > "HOLLight.hollight.CONT_HASSUP"
|
|
2764 |
"CONT_DIV" > "HOLLight.hollight.CONT_DIV"
|
|
2765 |
"CONT_CONST" > "HOLLight.hollight.CONT_CONST"
|
|
2766 |
"CONT_COMPOSE" > "HOLLight.hollight.CONT_COMPOSE"
|
|
2767 |
"CONT_BOUNDED_ABS" > "HOLLight.hollight.CONT_BOUNDED_ABS"
|
|
2768 |
"CONT_BOUNDED" > "HOLLight.hollight.CONT_BOUNDED"
|
|
2769 |
"CONT_ATTAINS_ALL" > "HOLLight.hollight.CONT_ATTAINS_ALL"
|
|
2770 |
"CONT_ATTAINS2" > "HOLLight.hollight.CONT_ATTAINS2"
|
|
2771 |
"CONT_ATTAINS" > "HOLLight.hollight.CONT_ATTAINS"
|
|
2772 |
"CONT_ADD" > "HOLLight.hollight.CONT_ADD"
|
|
2773 |
"CONTL_LIM" > "HOLLight.hollight.CONTL_LIM"
|
|
2774 |
"CONS_def" > "HOLLight.hollight.CONS_def"
|
|
2775 |
"CONS_11" > "HOLLight.hollight.CONS_11"
|
|
2776 |
"CONSTR_def" > "HOLLight.hollight.CONSTR_def"
|
|
2777 |
"CONSTR_REC" > "HOLLight.hollight.CONSTR_REC"
|
|
2778 |
"CONSTR_INJ" > "HOLLight.hollight.CONSTR_INJ"
|
|
2779 |
"CONSTR_IND" > "HOLLight.hollight.CONSTR_IND"
|
|
2780 |
"CONSTR_BOT" > "HOLLight.hollight.CONSTR_BOT"
|
|
2781 |
"CONJ_SYM" > "HOL.conj_comms_1"
|
|
2782 |
"CONJ_ASSOC" > "HOL.conj_assoc"
|
|
2783 |
"CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
|
|
2784 |
"COND_def" > "HOLLight.hollight.COND_def"
|
|
2785 |
"COND_RATOR" > "HOLLight.hollight.COND_RATOR"
|
|
2786 |
"COND_RAND" > "HOLLight.hollight.COND_RAND"
|
|
2787 |
"COND_ID" > "HOLLight.hollight.COND_ID"
|
|
2788 |
"COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
|
|
2789 |
"COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
|
|
2790 |
"COND_ELIM_THM" > "HOLLight.hollight.COND_ELIM_THM"
|
|
2791 |
"COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
|
|
2792 |
"COND_ABS" > "HOLLight.hollight.COND_ABS"
|
|
2793 |
"COMPONENT" > "HOLLight.hollight.COMPONENT"
|
|
2794 |
"COMPL_MEM" > "HOLLight.hollight.COMPL_MEM"
|
|
2795 |
"CLOSED_LIMPT" > "HOLLight.hollight.CLOSED_LIMPT"
|
|
2796 |
"CIRCLE_SINCOS" > "HOLLight.hollight.CIRCLE_SINCOS"
|
|
2797 |
"CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
|
|
2798 |
"CHOICE_def" > "HOLLight.hollight.CHOICE_def"
|
|
2799 |
"CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
|
|
2800 |
"CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
|
|
2801 |
"CASEWISE_WORKS" > "HOLLight.hollight.CASEWISE_WORKS"
|
|
2802 |
"CASEWISE_CASES" > "HOLLight.hollight.CASEWISE_CASES"
|
|
2803 |
"CASEWISE" > "HOLLight.hollight.CASEWISE"
|
|
2804 |
"CART_EQ" > "HOLLight.hollight.CART_EQ"
|
|
2805 |
"CARD_def" > "HOLLight.hollight.CARD_def"
|
|
2806 |
"CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
|
|
2807 |
"CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
|
|
2808 |
"CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
|
|
2809 |
"CARD_UNION" > "HOLLight.hollight.CARD_UNION"
|
|
2810 |
"CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
|
|
2811 |
"CARD_SUBSET_EQ" > "HOLLight.hollight.CARD_SUBSET_EQ"
|
|
2812 |
"CARD_SUBSET" > "HOLLight.hollight.CARD_SUBSET"
|
|
2813 |
"CARD_PSUBSET" > "HOLLight.hollight.CARD_PSUBSET"
|
|
2814 |
"CARD_PRODUCT" > "HOLLight.hollight.CARD_PRODUCT"
|
|
2815 |
"CARD_POWERSET" > "HOLLight.hollight.CARD_POWERSET"
|
|
2816 |
"CARD_NUMSEG_LT" > "HOLLight.hollight.CARD_NUMSEG_LT"
|
|
2817 |
"CARD_NUMSEG_LEMMA" > "HOLLight.hollight.CARD_NUMSEG_LEMMA"
|
|
2818 |
"CARD_NUMSEG_LE" > "HOLLight.hollight.CARD_NUMSEG_LE"
|
|
2819 |
"CARD_NUMSEG_1" > "HOLLight.hollight.CARD_NUMSEG_1"
|
|
2820 |
"CARD_NUMSEG" > "HOLLight.hollight.CARD_NUMSEG"
|
|
2821 |
"CARD_LT_def" > "HOLLight.hollight.CARD_LT_def"
|
|
2822 |
"CARD_LE_def" > "HOLLight.hollight.CARD_LE_def"
|
|
2823 |
"CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
|
|
2824 |
"CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
|
|
2825 |
"CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
|
|
2826 |
"CARD_GT_def" > "HOLLight.hollight.CARD_GT_def"
|
|
2827 |
"CARD_GE_def" > "HOLLight.hollight.CARD_GE_def"
|
|
2828 |
"CARD_GE_TRANS" > "HOLLight.hollight.CARD_GE_TRANS"
|
|
2829 |
"CARD_GE_REFL" > "HOLLight.hollight.CARD_GE_REFL"
|
|
2830 |
"CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
|
|
2831 |
"CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
|
|
2832 |
"CARD_EQ_def" > "HOLLight.hollight.CARD_EQ_def"
|
|
2833 |
"CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
|
|
2834 |
"CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
|
|
2835 |
"CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
|
|
2836 |
"CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
|
|
2837 |
"CARD_CLAUSES" > "HOLLight.hollight.CARD_CLAUSES"
|
|
2838 |
"BOUNDS_NOTZERO" > "HOLLight.hollight.BOUNDS_NOTZERO"
|
|
2839 |
"BOUNDS_LINEAR_0" > "HOLLight.hollight.BOUNDS_LINEAR_0"
|
|
2840 |
"BOUNDS_LINEAR" > "HOLLight.hollight.BOUNDS_LINEAR"
|
|
2841 |
"BOUNDS_IGNORE" > "HOLLight.hollight.BOUNDS_IGNORE"
|
|
2842 |
"BOUNDS_DIVIDED" > "HOLLight.hollight.BOUNDS_DIVIDED"
|
|
2843 |
"BOTTOM_def" > "HOLLight.hollight.BOTTOM_def"
|
|
2844 |
"BOOL_CASES_AX" > "Datatype.bool.nchotomy"
|
|
2845 |
"BOLZANO_LEMMA" > "HOLLight.hollight.BOLZANO_LEMMA"
|
|
2846 |
"BIT1_THM" > "HOLLightCompat.NUMERAL_BIT1_altdef"
|
|
2847 |
"BIT0_THM" > "HOLLightCompat.NUMERAL_BIT0_def"
|
|
2848 |
"BIJ_def" > "HOLLight.hollight.BIJ_def"
|
|
2849 |
"BETA_THM" > "Presburger.fm_modd_pinf"
|
|
2850 |
"BALL_OPEN" > "HOLLight.hollight.BALL_OPEN"
|
|
2851 |
"BALL_NEIGH" > "HOLLight.hollight.BALL_NEIGH"
|
|
2852 |
"ATN_TAN" > "HOLLight.hollight.ATN_TAN"
|
|
2853 |
"ATN_POS_LT" > "HOLLight.hollight.ATN_POS_LT"
|
|
2854 |
"ATN_POS_LE" > "HOLLight.hollight.ATN_POS_LE"
|
|
2855 |
"ATN_NEG" > "HOLLight.hollight.ATN_NEG"
|
|
2856 |
"ATN_MONO_LT_EQ" > "HOLLight.hollight.ATN_MONO_LT_EQ"
|
|
2857 |
"ATN_MONO_LT" > "HOLLight.hollight.ATN_MONO_LT"
|
|
2858 |
"ATN_MONO_LE_EQ" > "HOLLight.hollight.ATN_MONO_LE_EQ"
|
|
2859 |
"ATN_LT_PI4_POS" > "HOLLight.hollight.ATN_LT_PI4_POS"
|
|
2860 |
"ATN_LT_PI4_NEG" > "HOLLight.hollight.ATN_LT_PI4_NEG"
|
|
2861 |
"ATN_LT_PI4" > "HOLLight.hollight.ATN_LT_PI4"
|
|
2862 |
"ATN_LE_PI4" > "HOLLight.hollight.ATN_LE_PI4"
|
|
2863 |
"ATN_INJ" > "HOLLight.hollight.ATN_INJ"
|
|
2864 |
"ATN_BOUNDS" > "HOLLight.hollight.ATN_BOUNDS"
|
|
2865 |
"ATN_1" > "HOLLight.hollight.ATN_1"
|
|
2866 |
"ATN_0" > "HOLLight.hollight.ATN_0"
|
|
2867 |
"ATN" > "HOLLight.hollight.ATN"
|
|
2868 |
"ASSOC_def" > "HOLLight.hollight.ASSOC_def"
|
|
2869 |
"ASN_SIN" > "HOLLight.hollight.ASN_SIN"
|
|
2870 |
"ASN_BOUNDS_LT" > "HOLLight.hollight.ASN_BOUNDS_LT"
|
|
2871 |
"ASN_BOUNDS" > "HOLLight.hollight.ASN_BOUNDS"
|
|
2872 |
"ASN" > "HOLLight.hollight.ASN"
|
|
2873 |
"ARITH_ZERO" > "HOLLight.hollight.ARITH_ZERO"
|
|
2874 |
"ARITH_SUC" > "HOLLight.hollight.ARITH_SUC"
|
|
2875 |
"ARITH_SUB" > "HOLLight.hollight.ARITH_SUB"
|
|
2876 |
"ARITH_PRE" > "HOLLight.hollight.ARITH_PRE"
|
|
2877 |
"ARITH_ODD" > "HOLLight.hollight.ARITH_ODD"
|
|
2878 |
"ARITH_MULT" > "HOLLight.hollight.ARITH_MULT"
|
|
2879 |
"ARITH_LT" > "HOLLight.hollight.ARITH_LT"
|
|
2880 |
"ARITH_LE" > "HOLLight.hollight.ARITH_LE"
|
|
2881 |
"ARITH_EXP" > "HOLLight.hollight.ARITH_EXP"
|
|
2882 |
"ARITH_EVEN" > "HOLLight.hollight.ARITH_EVEN"
|
|
2883 |
"ARITH_EQ" > "HOLLight.hollight.ARITH_EQ"
|
|
2884 |
"ARITH_ADD" > "HOLLight.hollight.ARITH_ADD"
|
|
2885 |
"APPEND_def" > "HOLLight.hollight.APPEND_def"
|
|
2886 |
"APPEND_NIL" > "HOLLight.hollight.APPEND_NIL"
|
|
2887 |
"APPEND_EQ_NIL" > "HOLLight.hollight.APPEND_EQ_NIL"
|
|
2888 |
"APPEND_ASSOC" > "HOLLight.hollight.APPEND_ASSOC"
|
|
2889 |
"AND_FORALL_THM" > "HOL.all_conj_distrib"
|
|
2890 |
"AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
|
|
2891 |
"AND_ALL2" > "HOLLight.hollight.AND_ALL2"
|
|
2892 |
"AND_ALL" > "HOLLight.hollight.AND_ALL"
|
|
2893 |
"ALL_list_def" > "HOLLight.hollight.ALL_list_def"
|
|
2894 |
"ALL_T" > "HOLLight.hollight.ALL_T"
|
|
2895 |
"ALL_MP" > "HOLLight.hollight.ALL_MP"
|
|
2896 |
"ALL_MEM" > "HOLLight.hollight.ALL_MEM"
|
|
2897 |
"ALL_MAP" > "HOLLight.hollight.ALL_MAP"
|
|
2898 |
"ALL_IMP" > "HOLLight.hollight.ALL_IMP"
|
|
2899 |
"ALL_APPEND" > "HOLLight.hollight.ALL_APPEND"
|
|
2900 |
"ALL2_def" > "HOLLight.hollight.ALL2_def"
|
|
2901 |
"ALL2_MAP2" > "HOLLight.hollight.ALL2_MAP2"
|
|
2902 |
"ALL2_MAP" > "HOLLight.hollight.ALL2_MAP"
|
|
2903 |
"ALL2_AND_RIGHT" > "HOLLight.hollight.ALL2_AND_RIGHT"
|
|
2904 |
"ALL2_ALL" > "HOLLight.hollight.ALL2_ALL"
|
|
2905 |
"ALL2" > "HOLLight.hollight.ALL2"
|
|
2906 |
"ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
|
|
2907 |
"ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
|
|
2908 |
"ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
|
|
2909 |
"ADMISSIBLE_CONST" > "HOLLight.hollight.ADMISSIBLE_CONST"
|
|
2910 |
"ADMISSIBLE_COND" > "HOLLight.hollight.ADMISSIBLE_COND"
|
|
2911 |
"ADMISSIBLE_COMB" > "HOLLight.hollight.ADMISSIBLE_COMB"
|
|
2912 |
"ADMISSIBLE_BASE" > "HOLLight.hollight.ADMISSIBLE_BASE"
|
|
2913 |
"ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
|
|
2914 |
"ADD_SUC" > "Nat.add_Suc_right"
|
|
2915 |
"ADD_SUBR2" > "Nat.diff_add_0"
|
|
2916 |
"ADD_SUBR" > "HOLLight.hollight.ADD_SUBR"
|
|
2917 |
"ADD_SUB2" > "Nat.diff_add_inverse"
|
|
2918 |
"ADD_SUB" > "Nat.diff_add_inverse2"
|
|
2919 |
"ADD_EQ_0" > "Nat.add_is_0"
|
|
2920 |
"ADD_CLAUSES" > "HOLLight.hollight.ADD_CLAUSES"
|
|
2921 |
"ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
|
|
2922 |
"ADD_AC" > "HOLLight.hollight.ADD_AC"
|
|
2923 |
"ADD_0" > "Finite_Set.AC_add.f_e.ident"
|
|
2924 |
"ADD1" > "HOLLight.hollight.ADD1"
|
|
2925 |
"ACS_MONO_LT" > "HOLLight.hollight.ACS_MONO_LT"
|
|
2926 |
"ACS_COS" > "HOLLight.hollight.ACS_COS"
|
|
2927 |
"ACS_BOUNDS_LT" > "HOLLight.hollight.ACS_BOUNDS_LT"
|
|
2928 |
"ACS_BOUNDS" > "HOLLight.hollight.ACS_BOUNDS"
|
|
2929 |
"ACS" > "HOLLight.hollight.ACS"
|
|
2930 |
"ABS_ZERO" > "HOLLight.hollight.ABS_ZERO"
|
|
2931 |
"ABS_TRIANGLE" > "HOLLight.hollight.ABS_TRIANGLE"
|
|
2932 |
"ABS_SUM" > "HOLLight.hollight.ABS_SUM"
|
|
2933 |
"ABS_SUB_ABS" > "HOLLight.hollight.ABS_SUB_ABS"
|
|
2934 |
"ABS_SUB" > "HOLLight.hollight.ABS_SUB"
|
|
2935 |
"ABS_STILLNZ" > "HOLLight.hollight.ABS_STILLNZ"
|
|
2936 |
"ABS_SIMP" > "Presburger.fm_modd_pinf"
|
|
2937 |
"ABS_SIGN2" > "HOLLight.hollight.ABS_SIGN2"
|
|
2938 |
"ABS_SIGN" > "HOLLight.hollight.ABS_SIGN"
|
|
2939 |
"ABS_REFL" > "HOLLight.hollight.ABS_REFL"
|
|
2940 |
"ABS_POW2" > "HOLLight.hollight.ABS_POW2"
|
|
2941 |
"ABS_POS" > "HOLLight.hollight.ABS_POS"
|
|
2942 |
"ABS_NZ" > "HOLLight.hollight.ABS_NZ"
|
|
2943 |
"ABS_NEG_LEMMA" > "HOLLight.hollight.ABS_NEG_LEMMA"
|
|
2944 |
"ABS_NEG" > "HOLLight.hollight.ABS_NEG"
|
|
2945 |
"ABS_N" > "HOLLight.hollight.ABS_N"
|
|
2946 |
"ABS_MUL" > "HOLLight.hollight.ABS_MUL"
|
|
2947 |
"ABS_LT_MUL2" > "HOLLight.hollight.ABS_LT_MUL2"
|
|
2948 |
"ABS_LE" > "HOLLight.hollight.ABS_LE"
|
|
2949 |
"ABS_INV" > "HOLLight.hollight.ABS_INV"
|
|
2950 |
"ABS_DIV" > "HOLLight.hollight.ABS_DIV"
|
|
2951 |
"ABS_CIRCLE" > "HOLLight.hollight.ABS_CIRCLE"
|
|
2952 |
"ABS_CASES" > "HOLLight.hollight.ABS_CASES"
|
|
2953 |
"ABS_BOUNDS" > "HOLLight.hollight.ABS_BOUNDS"
|
|
2954 |
"ABS_BOUND" > "HOLLight.hollight.ABS_BOUND"
|
|
2955 |
"ABS_BETWEEN2" > "HOLLight.hollight.ABS_BETWEEN2"
|
|
2956 |
"ABS_BETWEEN1" > "HOLLight.hollight.ABS_BETWEEN1"
|
|
2957 |
"ABS_BETWEEN" > "HOLLight.hollight.ABS_BETWEEN"
|
|
2958 |
"ABS_ABS" > "HOLLight.hollight.ABS_ABS"
|
|
2959 |
"ABS_1" > "HOLLight.hollight.ABS_1"
|
|
2960 |
"ABS_0" > "HOLLight.hollight.ABS_0"
|
|
2961 |
"ABSORPTION" > "HOLLight.hollight.ABSORPTION"
|
|
2962 |
">_def" > "HOLLight.hollight.>_def"
|
|
2963 |
">=_def" > "HOLLight.hollight.>=_def"
|
|
2964 |
"<_def" > "HOLLight.hollight.<_def"
|
|
2965 |
"<=_def" > "HOLLight.hollight.<=_def"
|
|
2966 |
"$_def" > "HOLLight.hollight.$_def"
|
|
2967 |
|
|
2968 |
ignore_thms
|
|
2969 |
"TYDEF_prod"
|
|
2970 |
"TYDEF_num"
|
|
2971 |
"TYDEF_1"
|
|
2972 |
"IND_SUC_0_EXISTS"
|
|
2973 |
"DEF_one"
|
|
2974 |
"DEF__0"
|
|
2975 |
"DEF_SUC"
|
|
2976 |
"DEF_NUM_REP"
|
|
2977 |
"DEF_IND_SUC"
|
|
2978 |
"DEF_IND_0"
|
|
2979 |
|
|
2980 |
end
|