|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"algebra_canon" > "algebra_canon_primdef"
|
|
|
7 |
"alg_twinfree" > "alg_twinfree_primdef"
|
|
|
8 |
"alg_twin" > "alg_twin_primdef"
|
|
|
9 |
"alg_sorted" > "alg_sorted_primdef"
|
|
|
10 |
"alg_prefixfree" > "alg_prefixfree_primdef"
|
|
|
11 |
"alg_order_tupled" > "alg_order_tupled_def"
|
|
|
12 |
"alg_order" > "alg_order_primdef"
|
|
|
13 |
"alg_longest" > "alg_longest_primdef"
|
|
|
14 |
"alg_canon_prefs" > "alg_canon_prefs_primdef"
|
|
|
15 |
"alg_canon_merge" > "alg_canon_merge_primdef"
|
|
|
16 |
"alg_canon_find" > "alg_canon_find_primdef"
|
|
|
17 |
"alg_canon2" > "alg_canon2_primdef"
|
|
|
18 |
"alg_canon1" > "alg_canon1_primdef"
|
|
|
19 |
"alg_canon" > "alg_canon_primdef"
|
|
|
20 |
|
|
|
21 |
const_maps
|
|
|
22 |
"algebra_canon" > "HOL4Prob.prob_canon.algebra_canon"
|
|
|
23 |
"alg_twinfree" > "HOL4Prob.prob_canon.alg_twinfree"
|
|
|
24 |
"alg_twin" > "HOL4Prob.prob_canon.alg_twin"
|
|
|
25 |
"alg_sorted" > "HOL4Prob.prob_canon.alg_sorted"
|
|
|
26 |
"alg_prefixfree" > "HOL4Prob.prob_canon.alg_prefixfree"
|
|
|
27 |
"alg_order_tupled" > "HOL4Prob.prob_canon.alg_order_tupled"
|
|
|
28 |
"alg_order" > "HOL4Prob.prob_canon.alg_order"
|
|
|
29 |
"alg_longest" > "HOL4Prob.prob_canon.alg_longest"
|
|
|
30 |
"alg_canon2" > "HOL4Prob.prob_canon.alg_canon2"
|
|
|
31 |
"alg_canon1" > "HOL4Prob.prob_canon.alg_canon1"
|
|
|
32 |
"alg_canon" > "HOL4Prob.prob_canon.alg_canon"
|
|
|
33 |
|
|
|
34 |
thm_maps
|
|
|
35 |
"algebra_canon_primdef" > "HOL4Prob.prob_canon.algebra_canon_primdef"
|
|
|
36 |
"algebra_canon_def" > "HOL4Prob.prob_canon.algebra_canon_def"
|
|
|
37 |
"alg_twinfree_primitive_def" > "HOL4Prob.prob_canon.alg_twinfree_primitive_def"
|
|
|
38 |
"alg_twinfree_primdef" > "HOL4Prob.prob_canon.alg_twinfree_primdef"
|
|
|
39 |
"alg_twinfree_ind" > "HOL4Prob.prob_canon.alg_twinfree_ind"
|
|
|
40 |
"alg_twinfree_def" > "HOL4Prob.prob_canon.alg_twinfree_def"
|
|
|
41 |
"alg_twin_primdef" > "HOL4Prob.prob_canon.alg_twin_primdef"
|
|
|
42 |
"alg_twin_def" > "HOL4Prob.prob_canon.alg_twin_def"
|
|
|
43 |
"alg_sorted_primitive_def" > "HOL4Prob.prob_canon.alg_sorted_primitive_def"
|
|
|
44 |
"alg_sorted_primdef" > "HOL4Prob.prob_canon.alg_sorted_primdef"
|
|
|
45 |
"alg_sorted_ind" > "HOL4Prob.prob_canon.alg_sorted_ind"
|
|
|
46 |
"alg_sorted_def" > "HOL4Prob.prob_canon.alg_sorted_def"
|
|
|
47 |
"alg_prefixfree_primitive_def" > "HOL4Prob.prob_canon.alg_prefixfree_primitive_def"
|
|
|
48 |
"alg_prefixfree_primdef" > "HOL4Prob.prob_canon.alg_prefixfree_primdef"
|
|
|
49 |
"alg_prefixfree_ind" > "HOL4Prob.prob_canon.alg_prefixfree_ind"
|
|
|
50 |
"alg_prefixfree_def" > "HOL4Prob.prob_canon.alg_prefixfree_def"
|
|
|
51 |
"alg_order_tupled_primitive_def" > "HOL4Prob.prob_canon.alg_order_tupled_primitive_def"
|
|
|
52 |
"alg_order_tupled_def" > "HOL4Prob.prob_canon.alg_order_tupled_def"
|
|
|
53 |
"alg_order_primdef" > "HOL4Prob.prob_canon.alg_order_primdef"
|
|
|
54 |
"alg_order_ind" > "HOL4Prob.prob_canon.alg_order_ind"
|
|
|
55 |
"alg_order_def" > "HOL4Prob.prob_canon.alg_order_def"
|
|
|
56 |
"alg_order_curried_def" > "HOL4Prob.prob_canon.alg_order_curried_def"
|
|
|
57 |
"alg_longest_primdef" > "HOL4Prob.prob_canon.alg_longest_primdef"
|
|
|
58 |
"alg_longest_def" > "HOL4Prob.prob_canon.alg_longest_def"
|
|
|
59 |
"alg_canon_primdef" > "HOL4Prob.prob_canon.alg_canon_primdef"
|
|
|
60 |
"alg_canon_prefs_def" > "HOL4Prob.prob_canon.alg_canon_prefs_def"
|
|
|
61 |
"alg_canon_merge_def" > "HOL4Prob.prob_canon.alg_canon_merge_def"
|
|
|
62 |
"alg_canon_find_def" > "HOL4Prob.prob_canon.alg_canon_find_def"
|
|
|
63 |
"alg_canon_def" > "HOL4Prob.prob_canon.alg_canon_def"
|
|
|
64 |
"alg_canon2_primdef" > "HOL4Prob.prob_canon.alg_canon2_primdef"
|
|
|
65 |
"alg_canon2_def" > "HOL4Prob.prob_canon.alg_canon2_def"
|
|
|
66 |
"alg_canon1_primdef" > "HOL4Prob.prob_canon.alg_canon1_primdef"
|
|
|
67 |
"alg_canon1_def" > "HOL4Prob.prob_canon.alg_canon1_def"
|
|
|
68 |
"MEM_NIL_STEP" > "HOL4Prob.prob_canon.MEM_NIL_STEP"
|
|
|
69 |
"ALG_TWIN_SING" > "HOL4Prob.prob_canon.ALG_TWIN_SING"
|
|
|
70 |
"ALG_TWIN_REDUCE" > "HOL4Prob.prob_canon.ALG_TWIN_REDUCE"
|
|
|
71 |
"ALG_TWIN_NIL" > "HOL4Prob.prob_canon.ALG_TWIN_NIL"
|
|
|
72 |
"ALG_TWIN_CONS" > "HOL4Prob.prob_canon.ALG_TWIN_CONS"
|
|
|
73 |
"ALG_TWINS_PREFIX" > "HOL4Prob.prob_canon.ALG_TWINS_PREFIX"
|
|
|
74 |
"ALG_TWINFREE_TLS" > "HOL4Prob.prob_canon.ALG_TWINFREE_TLS"
|
|
|
75 |
"ALG_TWINFREE_TL" > "HOL4Prob.prob_canon.ALG_TWINFREE_TL"
|
|
|
76 |
"ALG_TWINFREE_STEP2" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP2"
|
|
|
77 |
"ALG_TWINFREE_STEP1" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP1"
|
|
|
78 |
"ALG_TWINFREE_STEP" > "HOL4Prob.prob_canon.ALG_TWINFREE_STEP"
|
|
|
79 |
"ALG_SORTED_TLS" > "HOL4Prob.prob_canon.ALG_SORTED_TLS"
|
|
|
80 |
"ALG_SORTED_TL" > "HOL4Prob.prob_canon.ALG_SORTED_TL"
|
|
|
81 |
"ALG_SORTED_STEP" > "HOL4Prob.prob_canon.ALG_SORTED_STEP"
|
|
|
82 |
"ALG_SORTED_PREFIXFREE_MEM_NIL" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_MEM_NIL"
|
|
|
83 |
"ALG_SORTED_PREFIXFREE_EQUALITY" > "HOL4Prob.prob_canon.ALG_SORTED_PREFIXFREE_EQUALITY"
|
|
|
84 |
"ALG_SORTED_MONO" > "HOL4Prob.prob_canon.ALG_SORTED_MONO"
|
|
|
85 |
"ALG_SORTED_MIN" > "HOL4Prob.prob_canon.ALG_SORTED_MIN"
|
|
|
86 |
"ALG_SORTED_FILTER" > "HOL4Prob.prob_canon.ALG_SORTED_FILTER"
|
|
|
87 |
"ALG_SORTED_DEF_ALT" > "HOL4Prob.prob_canon.ALG_SORTED_DEF_ALT"
|
|
|
88 |
"ALG_SORTED_APPEND" > "HOL4Prob.prob_canon.ALG_SORTED_APPEND"
|
|
|
89 |
"ALG_PREFIXFREE_TLS" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TLS"
|
|
|
90 |
"ALG_PREFIXFREE_TL" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_TL"
|
|
|
91 |
"ALG_PREFIXFREE_STEP" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_STEP"
|
|
|
92 |
"ALG_PREFIXFREE_MONO" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_MONO"
|
|
|
93 |
"ALG_PREFIXFREE_FILTER" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_FILTER"
|
|
|
94 |
"ALG_PREFIXFREE_ELT" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_ELT"
|
|
|
95 |
"ALG_PREFIXFREE_APPEND" > "HOL4Prob.prob_canon.ALG_PREFIXFREE_APPEND"
|
|
|
96 |
"ALG_ORDER_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_TRANS"
|
|
|
97 |
"ALG_ORDER_TOTAL" > "HOL4Prob.prob_canon.ALG_ORDER_TOTAL"
|
|
|
98 |
"ALG_ORDER_SNOC" > "HOL4Prob.prob_canon.ALG_ORDER_SNOC"
|
|
|
99 |
"ALG_ORDER_REFL" > "HOL4Prob.prob_canon.ALG_ORDER_REFL"
|
|
|
100 |
"ALG_ORDER_PREFIX_TRANS" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_TRANS"
|
|
|
101 |
"ALG_ORDER_PREFIX_MONO" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_MONO"
|
|
|
102 |
"ALG_ORDER_PREFIX_ANTI" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX_ANTI"
|
|
|
103 |
"ALG_ORDER_PREFIX" > "HOL4Prob.prob_canon.ALG_ORDER_PREFIX"
|
|
|
104 |
"ALG_ORDER_NIL" > "HOL4Prob.prob_canon.ALG_ORDER_NIL"
|
|
|
105 |
"ALG_ORDER_ANTISYM" > "HOL4Prob.prob_canon.ALG_ORDER_ANTISYM"
|
|
|
106 |
"ALG_LONGEST_TLS" > "HOL4Prob.prob_canon.ALG_LONGEST_TLS"
|
|
|
107 |
"ALG_LONGEST_TL" > "HOL4Prob.prob_canon.ALG_LONGEST_TL"
|
|
|
108 |
"ALG_LONGEST_HD" > "HOL4Prob.prob_canon.ALG_LONGEST_HD"
|
|
|
109 |
"ALG_LONGEST_APPEND" > "HOL4Prob.prob_canon.ALG_LONGEST_APPEND"
|
|
|
110 |
"ALG_CANON_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_SORTED_PREFIXFREE_TWINFREE"
|
|
|
111 |
"ALG_CANON_PREFS_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_SORTED"
|
|
|
112 |
"ALG_CANON_PREFS_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_PREFIXFREE"
|
|
|
113 |
"ALG_CANON_PREFS_HD" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_HD"
|
|
|
114 |
"ALG_CANON_PREFS_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_DELETES"
|
|
|
115 |
"ALG_CANON_PREFS_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_PREFS_CONSTANT"
|
|
|
116 |
"ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE"
|
|
|
117 |
"ALG_CANON_MERGE_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_SHORTENS"
|
|
|
118 |
"ALG_CANON_MERGE_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_PREFIXFREE_PRESERVE"
|
|
|
119 |
"ALG_CANON_MERGE_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_MERGE_CONSTANT"
|
|
|
120 |
"ALG_CANON_IDEMPOT" > "HOL4Prob.prob_canon.ALG_CANON_IDEMPOT"
|
|
|
121 |
"ALG_CANON_FIND_SORTED" > "HOL4Prob.prob_canon.ALG_CANON_FIND_SORTED"
|
|
|
122 |
"ALG_CANON_FIND_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON_FIND_PREFIXFREE"
|
|
|
123 |
"ALG_CANON_FIND_HD" > "HOL4Prob.prob_canon.ALG_CANON_FIND_HD"
|
|
|
124 |
"ALG_CANON_FIND_DELETES" > "HOL4Prob.prob_canon.ALG_CANON_FIND_DELETES"
|
|
|
125 |
"ALG_CANON_FIND_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_FIND_CONSTANT"
|
|
|
126 |
"ALG_CANON_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON_CONSTANT"
|
|
|
127 |
"ALG_CANON_BASIC" > "HOL4Prob.prob_canon.ALG_CANON_BASIC"
|
|
|
128 |
"ALG_CANON2_SORTED_PREFIXFREE_TWINFREE" > "HOL4Prob.prob_canon.ALG_CANON2_SORTED_PREFIXFREE_TWINFREE"
|
|
|
129 |
"ALG_CANON2_SHORTENS" > "HOL4Prob.prob_canon.ALG_CANON2_SHORTENS"
|
|
|
130 |
"ALG_CANON2_PREFIXFREE_PRESERVE" > "HOL4Prob.prob_canon.ALG_CANON2_PREFIXFREE_PRESERVE"
|
|
|
131 |
"ALG_CANON2_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON2_CONSTANT"
|
|
|
132 |
"ALG_CANON1_SORTED" > "HOL4Prob.prob_canon.ALG_CANON1_SORTED"
|
|
|
133 |
"ALG_CANON1_PREFIXFREE" > "HOL4Prob.prob_canon.ALG_CANON1_PREFIXFREE"
|
|
|
134 |
"ALG_CANON1_CONSTANT" > "HOL4Prob.prob_canon.ALG_CANON1_CONSTANT"
|
|
|
135 |
"ALGEBRA_CANON_TLS" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TLS"
|
|
|
136 |
"ALGEBRA_CANON_TL" > "HOL4Prob.prob_canon.ALGEBRA_CANON_TL"
|
|
|
137 |
"ALGEBRA_CANON_STEP2" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP2"
|
|
|
138 |
"ALGEBRA_CANON_STEP1" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP1"
|
|
|
139 |
"ALGEBRA_CANON_STEP" > "HOL4Prob.prob_canon.ALGEBRA_CANON_STEP"
|
|
|
140 |
"ALGEBRA_CANON_NIL_MEM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_NIL_MEM"
|
|
|
141 |
"ALGEBRA_CANON_INDUCTION" > "HOL4Prob.prob_canon.ALGEBRA_CANON_INDUCTION"
|
|
|
142 |
"ALGEBRA_CANON_DEF_ALT" > "HOL4Prob.prob_canon.ALGEBRA_CANON_DEF_ALT"
|
|
|
143 |
"ALGEBRA_CANON_CASES_THM" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES_THM"
|
|
|
144 |
"ALGEBRA_CANON_CASES" > "HOL4Prob.prob_canon.ALGEBRA_CANON_CASES"
|
|
|
145 |
"ALGEBRA_CANON_BASIC" > "HOL4Prob.prob_canon.ALGEBRA_CANON_BASIC"
|
|
|
146 |
|
|
|
147 |
end
|