|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"indep_set" > "indep_set_primdef"
|
|
|
7 |
"indep" > "indep_primdef"
|
|
|
8 |
"alg_cover_set" > "alg_cover_set_primdef"
|
|
|
9 |
"alg_cover" > "alg_cover_primdef"
|
|
|
10 |
|
|
|
11 |
const_maps
|
|
|
12 |
"indep_set" > "HOL4Prob.prob_indep.indep_set"
|
|
|
13 |
"indep" > "HOL4Prob.prob_indep.indep"
|
|
|
14 |
"alg_cover_set" > "HOL4Prob.prob_indep.alg_cover_set"
|
|
|
15 |
"alg_cover" > "HOL4Prob.prob_indep.alg_cover"
|
|
|
16 |
|
|
|
17 |
thm_maps
|
|
|
18 |
"indep_set_primdef" > "HOL4Prob.prob_indep.indep_set_primdef"
|
|
|
19 |
"indep_set_def" > "HOL4Prob.prob_indep.indep_set_def"
|
|
|
20 |
"indep_primdef" > "HOL4Prob.prob_indep.indep_primdef"
|
|
|
21 |
"indep_def" > "HOL4Prob.prob_indep.indep_def"
|
|
|
22 |
"alg_cover_set_primdef" > "HOL4Prob.prob_indep.alg_cover_set_primdef"
|
|
|
23 |
"alg_cover_set_def" > "HOL4Prob.prob_indep.alg_cover_set_def"
|
|
|
24 |
"alg_cover_primdef" > "HOL4Prob.prob_indep.alg_cover_primdef"
|
|
|
25 |
"alg_cover_def" > "HOL4Prob.prob_indep.alg_cover_def"
|
|
|
26 |
"PROB_INDEP_BOUND" > "HOL4Prob.prob_indep.PROB_INDEP_BOUND"
|
|
|
27 |
"MAP_CONS_TL_FILTER" > "HOL4Prob.prob_indep.MAP_CONS_TL_FILTER"
|
|
|
28 |
"INDEP_UNIT" > "HOL4Prob.prob_indep.INDEP_UNIT"
|
|
|
29 |
"INDEP_SET_SYM" > "HOL4Prob.prob_indep.INDEP_SET_SYM"
|
|
|
30 |
"INDEP_SET_LIST" > "HOL4Prob.prob_indep.INDEP_SET_LIST"
|
|
|
31 |
"INDEP_SET_DISJOINT_DECOMP" > "HOL4Prob.prob_indep.INDEP_SET_DISJOINT_DECOMP"
|
|
|
32 |
"INDEP_SET_BASIC" > "HOL4Prob.prob_indep.INDEP_SET_BASIC"
|
|
|
33 |
"INDEP_SDEST" > "HOL4Prob.prob_indep.INDEP_SDEST"
|
|
|
34 |
"INDEP_PROB" > "HOL4Prob.prob_indep.INDEP_PROB"
|
|
|
35 |
"INDEP_MEASURABLE2" > "HOL4Prob.prob_indep.INDEP_MEASURABLE2"
|
|
|
36 |
"INDEP_MEASURABLE1" > "HOL4Prob.prob_indep.INDEP_MEASURABLE1"
|
|
|
37 |
"INDEP_INDEP_SET_LEMMA" > "HOL4Prob.prob_indep.INDEP_INDEP_SET_LEMMA"
|
|
|
38 |
"INDEP_INDEP_SET" > "HOL4Prob.prob_indep.INDEP_INDEP_SET"
|
|
|
39 |
"INDEP_BIND_SDEST" > "HOL4Prob.prob_indep.INDEP_BIND_SDEST"
|
|
|
40 |
"INDEP_BIND" > "HOL4Prob.prob_indep.INDEP_BIND"
|
|
|
41 |
"BIND_STEP" > "HOL4Prob.prob_indep.BIND_STEP"
|
|
|
42 |
"ALG_COVER_WELL_DEFINED" > "HOL4Prob.prob_indep.ALG_COVER_WELL_DEFINED"
|
|
|
43 |
"ALG_COVER_UNIV" > "HOL4Prob.prob_indep.ALG_COVER_UNIV"
|
|
|
44 |
"ALG_COVER_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_UNIQUE"
|
|
|
45 |
"ALG_COVER_TAIL_STEP" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_STEP"
|
|
|
46 |
"ALG_COVER_TAIL_PROB" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_PROB"
|
|
|
47 |
"ALG_COVER_TAIL_MEASURABLE" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_MEASURABLE"
|
|
|
48 |
"ALG_COVER_STEP" > "HOL4Prob.prob_indep.ALG_COVER_STEP"
|
|
|
49 |
"ALG_COVER_SET_INDUCTION" > "HOL4Prob.prob_indep.ALG_COVER_SET_INDUCTION"
|
|
|
50 |
"ALG_COVER_SET_CASES_THM" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES_THM"
|
|
|
51 |
"ALG_COVER_SET_CASES" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES"
|
|
|
52 |
"ALG_COVER_SET_BASIC" > "HOL4Prob.prob_indep.ALG_COVER_SET_BASIC"
|
|
|
53 |
"ALG_COVER_HEAD" > "HOL4Prob.prob_indep.ALG_COVER_HEAD"
|
|
|
54 |
"ALG_COVER_EXISTS_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_EXISTS_UNIQUE"
|
|
|
55 |
|
|
|
56 |
end
|