Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1953 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1461 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (70 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (23 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (259 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (37 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (13 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (62 entries)

Global Index

A

add_frequency_list_not_in [lemma, in Huffman.Frequency]
add_frequency_list_in [lemma, in Huffman.Frequency]
add_frequency_list_1 [lemma, in Huffman.Frequency]
add_frequency_list_unique_key [lemma, in Huffman.Frequency]
add_frequency_list_in_inv [lemma, in Huffman.Frequency]
add_frequency_list_perm [lemma, in Huffman.Frequency]
add_frequency_list [definition, in Huffman.Frequency]
all_permutations_permutation [lemma, in Huffman.AuxLib]
all_permutations_aux_permutation [lemma, in Huffman.AuxLib]
all_permutations [definition, in Huffman.AuxLib]
all_permutations_aux [definition, in Huffman.AuxLib]
all_cover_cover [lemma, in Huffman.Cover]
all_cover_aux_cover [lemma, in Huffman.Cover]
all_cover [definition, in Huffman.Cover]
all_cover_aux [definition, in Huffman.Cover]
all_pbleaves_pbbuild [lemma, in Huffman.PBTree]
all_pbleaves_compute_pb [lemma, in Huffman.PBTree]
all_pbleaves_pbleaf [lemma, in Huffman.PBTree]
all_pbleaves_pbadd [lemma, in Huffman.PBTree]
all_pbleaves_NoDup [lemma, in Huffman.PBTree]
all_pbleaves_unique [lemma, in Huffman.PBTree]
all_pbleaves_inpb [lemma, in Huffman.PBTree]
all_pbleaves_in [lemma, in Huffman.PBTree]
all_pbleaves [definition, in Huffman.PBTree]
all_leaves_NoDup [lemma, in Huffman.BTree]
all_leaves_unique [lemma, in Huffman.BTree]
all_leaves_inb [lemma, in Huffman.BTree]
all_leaves_in [lemma, in Huffman.BTree]
all_leaves [definition, in Huffman.BTree]
app_inv_app2 [lemma, in Huffman.AuxLib]
app_inv_app [lemma, in Huffman.AuxLib]
AuxLib [library]
a1:113 [binder, in Huffman.PBTree]
a1:116 [binder, in Huffman.PBTree]
a1:137 [binder, in Huffman.HeightPred]
a1:144 [binder, in Huffman.HeightPred]
a1:151 [binder, in Huffman.HeightPred]
a1:155 [binder, in Huffman.PBTree]
a1:158 [binder, in Huffman.HeightPred]
a1:163 [binder, in Huffman.PBTree]
a1:165 [binder, in Huffman.PBTree]
a1:170 [binder, in Huffman.PBTree]
a1:174 [binder, in Huffman.PBTree]
a1:178 [binder, in Huffman.PBTree]
a1:181 [binder, in Huffman.PBTree]
a1:195 [binder, in Huffman.PBTree]
a1:199 [binder, in Huffman.PBTree]
a1:201 [binder, in Huffman.PBTree]
a1:204 [binder, in Huffman.PBTree]
a1:23 [binder, in Huffman.Frequency]
a1:241 [binder, in Huffman.PBTree]
a1:246 [binder, in Huffman.PBTree]
a1:47 [binder, in Huffman.Code]
a1:52 [binder, in Huffman.Code]
a1:84 [binder, in Huffman.PBTree]
a1:86 [binder, in Huffman.BTree]
a2:114 [binder, in Huffman.PBTree]
a2:166 [binder, in Huffman.PBTree]
a2:171 [binder, in Huffman.PBTree]
a2:175 [binder, in Huffman.PBTree]
a2:196 [binder, in Huffman.PBTree]
a2:200 [binder, in Huffman.PBTree]
a2:24 [binder, in Huffman.Frequency]
a2:48 [binder, in Huffman.Code]
a2:53 [binder, in Huffman.Code]
a2:85 [binder, in Huffman.PBTree]
a2:87 [binder, in Huffman.BTree]
a3:167 [binder, in Huffman.PBTree]
a3:172 [binder, in Huffman.PBTree]
a3:176 [binder, in Huffman.PBTree]
a4:168 [binder, in Huffman.PBTree]
a:1 [binder, in Huffman.AuxLib]
a:10 [binder, in Huffman.ISort]
a:10 [binder, in Huffman.Ordered]
a:10 [binder, in Huffman.PBTree]
a:10 [binder, in Huffman.WeightTree]
a:100 [binder, in Huffman.HeightPred]
a:102 [binder, in Huffman.Code]
a:105 [binder, in Huffman.Code]
a:106 [binder, in Huffman.PBTree]
a:109 [binder, in Huffman.Prod2List]
a:11 [binder, in Huffman.AuxLib]
a:11 [binder, in Huffman.UniqueKey]
a:11 [binder, in Huffman.Prod2List]
a:11 [binder, in Huffman.PBTree2BTree]
a:11 [binder, in Huffman.Weight]
a:115 [binder, in Huffman.Code]
a:119 [binder, in Huffman.HeightPred]
a:12 [binder, in Huffman.WeightTree]
a:121 [binder, in Huffman.AuxLib]
a:13 [binder, in Huffman.Restrict]
a:13 [binder, in Huffman.Ordered]
a:13 [binder, in Huffman.Frequency]
a:134 [binder, in Huffman.Code]
a:135 [binder, in Huffman.Code]
a:136 [binder, in Huffman.Code]
a:14 [binder, in Huffman.AuxLib]
a:14 [binder, in Huffman.Prod2List]
a:14 [binder, in Huffman.PBTree2BTree]
A:140 [binder, in Huffman.AuxLib]
a:142 [binder, in Huffman.Code]
a:143 [binder, in Huffman.AuxLib]
a:146 [binder, in Huffman.AuxLib]
a:15 [binder, in Huffman.ISort]
a:15 [binder, in Huffman.UniqueKey]
a:15 [binder, in Huffman.Code]
a:15 [binder, in Huffman.PBTree2BTree]
a:154 [binder, in Huffman.AuxLib]
a:157 [binder, in Huffman.AuxLib]
a:158 [binder, in Huffman.PBTree]
a:16 [binder, in Huffman.Ordered]
a:162 [binder, in Huffman.PBTree]
a:164 [binder, in Huffman.HeightPred]
a:165 [binder, in Huffman.HeightPred]
a:167 [binder, in Huffman.HeightPred]
a:17 [binder, in Huffman.AuxLib]
a:17 [binder, in Huffman.ISort]
a:17 [binder, in Huffman.Prod2List]
a:17 [binder, in Huffman.PBTree2BTree]
a:170 [binder, in Huffman.HeightPred]
a:172 [binder, in Huffman.HeightPred]
a:175 [binder, in Huffman.HeightPred]
a:177 [binder, in Huffman.HeightPred]
a:178 [binder, in Huffman.AuxLib]
a:18 [binder, in Huffman.Ordered]
a:18 [binder, in Huffman.Code]
a:18 [binder, in Huffman.Weight]
a:180 [binder, in Huffman.HeightPred]
a:182 [binder, in Huffman.AuxLib]
a:182 [binder, in Huffman.HeightPred]
a:186 [binder, in Huffman.HeightPred]
a:189 [binder, in Huffman.PBTree]
a:189 [binder, in Huffman.HeightPred]
a:19 [binder, in Huffman.AuxLib]
a:191 [binder, in Huffman.PBTree]
a:192 [binder, in Huffman.HeightPred]
a:194 [binder, in Huffman.HeightPred]
a:196 [binder, in Huffman.HeightPred]
a:198 [binder, in Huffman.HeightPred]
a:2 [binder, in Huffman.Code]
a:2 [binder, in Huffman.PBTree2BTree]
a:2 [binder, in Huffman.BTree]
a:2 [binder, in Huffman.Weight]
a:2 [binder, in Huffman.Frequency]
a:20 [binder, in Huffman.Prod2List]
a:20 [binder, in Huffman.Weight]
a:200 [binder, in Huffman.HeightPred]
a:208 [binder, in Huffman.PBTree]
a:21 [binder, in Huffman.AuxLib]
a:21 [binder, in Huffman.Ordered]
a:21 [binder, in Huffman.Code]
a:211 [binder, in Huffman.PBTree]
a:213 [binder, in Huffman.PBTree]
a:216 [binder, in Huffman.PBTree]
a:219 [binder, in Huffman.PBTree]
a:22 [binder, in Huffman.Weight]
a:221 [binder, in Huffman.PBTree]
a:224 [binder, in Huffman.PBTree]
a:227 [binder, in Huffman.PBTree]
a:229 [binder, in Huffman.PBTree]
a:23 [binder, in Huffman.UniqueKey]
a:23 [binder, in Huffman.Prod2List]
A:23 [binder, in Huffman.WeightTree]
a:232 [binder, in Huffman.PBTree]
a:234 [binder, in Huffman.PBTree]
a:24 [binder, in Huffman.Ordered]
a:250 [binder, in Huffman.PBTree]
a:26 [binder, in Huffman.PBTree]
a:26 [binder, in Huffman.Prod2List]
a:27 [binder, in Huffman.Code]
a:27 [binder, in Huffman.Frequency]
a:28 [binder, in Huffman.Ordered]
a:28 [binder, in Huffman.PBTree]
A:28 [binder, in Huffman.UniqueKey]
a:28 [binder, in Huffman.Code]
a:28 [binder, in Huffman.Weight]
a:29 [binder, in Huffman.BTree]
a:29 [binder, in Huffman.Frequency]
a:3 [binder, in Huffman.Restrict]
a:3 [binder, in Huffman.Ordered]
a:3 [binder, in Huffman.PBTree]
a:3 [binder, in Huffman.HeightPred]
a:3 [binder, in Huffman.Huffman]
a:30 [binder, in Huffman.Cover]
a:30 [binder, in Huffman.Code]
a:31 [binder, in Huffman.Cover]
a:31 [binder, in Huffman.BTree]
A:32 [binder, in Huffman.Ordered]
a:32 [binder, in Huffman.Prod2List]
a:33 [binder, in Huffman.Frequency]
a:34 [binder, in Huffman.UniqueKey]
a:36 [binder, in Huffman.Frequency]
a:37 [binder, in Huffman.BTree]
a:39 [binder, in Huffman.PBTree]
a:39 [binder, in Huffman.BTree]
a:4 [binder, in Huffman.ISort]
a:41 [binder, in Huffman.Huffman]
a:42 [binder, in Huffman.AuxLib]
a:42 [binder, in Huffman.Huffman]
a:42 [binder, in Huffman.Frequency]
a:44 [binder, in Huffman.BTree]
a:44 [binder, in Huffman.Huffman]
a:46 [binder, in Huffman.PBTree]
a:49 [binder, in Huffman.PBTree]
A:49 [binder, in Huffman.Weight]
a:49 [binder, in Huffman.Frequency]
a:5 [binder, in Huffman.UniqueKey]
a:5 [binder, in Huffman.Prod2List]
a:5 [binder, in Huffman.Frequency]
a:50 [binder, in Huffman.AuxLib]
a:51 [binder, in Huffman.BTree]
a:51 [binder, in Huffman.Frequency]
a:52 [binder, in Huffman.BTree]
a:52 [binder, in Huffman.Frequency]
a:56 [binder, in Huffman.Frequency]
a:57 [binder, in Huffman.AuxLib]
a:57 [binder, in Huffman.Weight]
a:58 [binder, in Huffman.Code]
a:59 [binder, in Huffman.Frequency]
a:6 [binder, in Huffman.PBTree2BTree]
a:60 [binder, in Huffman.Prod2List]
a:61 [binder, in Huffman.AuxLib]
a:61 [binder, in Huffman.Code]
a:61 [binder, in Huffman.BTree]
a:62 [binder, in Huffman.PBTree]
a:62 [binder, in Huffman.HeightPred]
a:63 [binder, in Huffman.BTree]
a:63 [binder, in Huffman.Frequency]
a:64 [binder, in Huffman.PBTree]
a:65 [binder, in Huffman.Code]
a:66 [binder, in Huffman.Frequency]
a:67 [binder, in Huffman.HeightPred]
a:67 [binder, in Huffman.Frequency]
a:7 [binder, in Huffman.ISort]
a:7 [binder, in Huffman.Code]
a:70 [binder, in Huffman.AuxLib]
a:70 [binder, in Huffman.Code]
a:71 [binder, in Huffman.AuxLib]
a:71 [binder, in Huffman.Cover]
a:74 [binder, in Huffman.Code]
a:76 [binder, in Huffman.AuxLib]
a:76 [binder, in Huffman.Code]
a:79 [binder, in Huffman.Code]
a:80 [binder, in Huffman.AuxLib]
a:81 [binder, in Huffman.HeightPred]
a:82 [binder, in Huffman.Code]
a:84 [binder, in Huffman.AuxLib]
a:84 [binder, in Huffman.BTree]
a:85 [binder, in Huffman.HeightPred]
a:86 [binder, in Huffman.Code]
a:87 [binder, in Huffman.AuxLib]
a:88 [binder, in Huffman.Prod2List]
a:9 [binder, in Huffman.AuxLib]
a:9 [binder, in Huffman.Ordered]
a:9 [binder, in Huffman.PBTree]
a:9 [binder, in Huffman.UniqueKey]
a:9 [binder, in Huffman.PBTree2BTree]
a:9 [binder, in Huffman.Weight]
a:9 [binder, in Huffman.Frequency]
a:92 [binder, in Huffman.Code]
a:97 [binder, in Huffman.Prod2List]
a:97 [binder, in Huffman.Code]
a:97 [binder, in Huffman.Huffman]
a:99 [binder, in Huffman.Huffman]


B

btree [inductive, in Huffman.BTree]
BTree [library]
btree_unique_prefix [lemma, in Huffman.BTree]
btree_unique_prefix2 [lemma, in Huffman.BTree]
btree_unique_prefix1 [lemma, in Huffman.BTree]
btree_dec [definition, in Huffman.BTree]
build [inductive, in Huffman.Build]
Build [section, in Huffman.Build]
Build [library]
buildf [definition, in Huffman.Build]
build_fun [definition, in Huffman.Build]
build_correct [lemma, in Huffman.Build]
build_permutation [lemma, in Huffman.Build]
build_same_weight_tree [lemma, in Huffman.Build]
build_comp [lemma, in Huffman.Build]
build_cover [lemma, in Huffman.Build]
build_step [constructor, in Huffman.Build]
build_one [constructor, in Huffman.Build]
Build.A [variable, in Huffman.Build]
Build.f [variable, in Huffman.Build]
b1:11 [binder, in Huffman.WeightTree]
b1:112 [binder, in Huffman.Prod2List]
b1:12 [binder, in Huffman.UniqueKey]
b1:13 [binder, in Huffman.WeightTree]
b1:138 [binder, in Huffman.HeightPred]
b1:144 [binder, in Huffman.AuxLib]
b1:145 [binder, in Huffman.HeightPred]
b1:152 [binder, in Huffman.HeightPred]
b1:159 [binder, in Huffman.HeightPred]
b1:242 [binder, in Huffman.PBTree]
b1:247 [binder, in Huffman.PBTree]
b1:25 [binder, in Huffman.Frequency]
b1:27 [binder, in Huffman.Build]
b1:30 [binder, in Huffman.Build]
b1:99 [binder, in Huffman.Prod2List]
b2:13 [binder, in Huffman.UniqueKey]
b2:145 [binder, in Huffman.AuxLib]
b:10 [binder, in Huffman.PBTree2BTree]
b:10 [binder, in Huffman.Weight]
b:100 [binder, in Huffman.PBTree]
b:101 [binder, in Huffman.HeightPred]
b:103 [binder, in Huffman.PBTree]
b:105 [binder, in Huffman.Prod2List]
b:106 [binder, in Huffman.Prod2List]
b:11 [binder, in Huffman.Ordered]
b:110 [binder, in Huffman.Prod2List]
b:119 [binder, in Huffman.Prod2List]
b:12 [binder, in Huffman.AuxLib]
b:12 [binder, in Huffman.Prod2List]
b:12 [binder, in Huffman.PBTree2BTree]
b:12 [binder, in Huffman.Weight]
b:120 [binder, in Huffman.Prod2List]
b:120 [binder, in Huffman.HeightPred]
B:13 [binder, in Huffman.Weight]
b:134 [binder, in Huffman.HeightPred]
b:14 [binder, in Huffman.Ordered]
B:141 [binder, in Huffman.AuxLib]
b:141 [binder, in Huffman.HeightPred]
b:148 [binder, in Huffman.HeightPred]
b:15 [binder, in Huffman.Prod2List]
b:155 [binder, in Huffman.HeightPred]
b:166 [binder, in Huffman.HeightPred]
b:168 [binder, in Huffman.HeightPred]
b:169 [binder, in Huffman.HeightPred]
b:171 [binder, in Huffman.HeightPred]
b:173 [binder, in Huffman.HeightPred]
b:174 [binder, in Huffman.HeightPred]
b:176 [binder, in Huffman.HeightPred]
b:178 [binder, in Huffman.HeightPred]
b:179 [binder, in Huffman.AuxLib]
b:179 [binder, in Huffman.HeightPred]
b:18 [binder, in Huffman.AuxLib]
b:18 [binder, in Huffman.Prod2List]
b:181 [binder, in Huffman.HeightPred]
b:183 [binder, in Huffman.AuxLib]
b:183 [binder, in Huffman.HeightPred]
b:184 [binder, in Huffman.HeightPred]
b:185 [binder, in Huffman.HeightPred]
b:187 [binder, in Huffman.HeightPred]
b:188 [binder, in Huffman.HeightPred]
b:19 [binder, in Huffman.Ordered]
b:19 [binder, in Huffman.Weight]
b:190 [binder, in Huffman.HeightPred]
b:191 [binder, in Huffman.HeightPred]
b:193 [binder, in Huffman.HeightPred]
b:195 [binder, in Huffman.HeightPred]
b:197 [binder, in Huffman.HeightPred]
b:199 [binder, in Huffman.HeightPred]
b:2 [binder, in Huffman.AuxLib]
b:20 [binder, in Huffman.AuxLib]
b:201 [binder, in Huffman.HeightPred]
b:21 [binder, in Huffman.Prod2List]
b:21 [binder, in Huffman.Weight]
b:22 [binder, in Huffman.Ordered]
b:22 [binder, in Huffman.BTree]
b:238 [binder, in Huffman.PBTree]
b:24 [binder, in Huffman.UniqueKey]
b:24 [binder, in Huffman.Prod2List]
b:243 [binder, in Huffman.PBTree]
b:25 [binder, in Huffman.Ordered]
b:27 [binder, in Huffman.PBTree]
b:27 [binder, in Huffman.Prod2List]
b:29 [binder, in Huffman.Ordered]
b:29 [binder, in Huffman.PBTree]
B:29 [binder, in Huffman.UniqueKey]
b:29 [binder, in Huffman.Weight]
b:3 [binder, in Huffman.Code]
b:3 [binder, in Huffman.PBTree2BTree]
b:3 [binder, in Huffman.BTree]
b:3 [binder, in Huffman.Weight]
b:3 [binder, in Huffman.Frequency]
b:30 [binder, in Huffman.BTree]
b:30 [binder, in Huffman.Weight]
b:31 [binder, in Huffman.Code]
b:31 [binder, in Huffman.Weight]
b:32 [binder, in Huffman.Weight]
B:33 [binder, in Huffman.Ordered]
b:33 [binder, in Huffman.Prod2List]
b:35 [binder, in Huffman.UniqueKey]
b:35 [binder, in Huffman.Weight]
b:36 [binder, in Huffman.Code]
b:36 [binder, in Huffman.Weight]
b:37 [binder, in Huffman.Weight]
b:37 [binder, in Huffman.Frequency]
b:38 [binder, in Huffman.Weight]
b:39 [binder, in Huffman.Weight]
b:4 [binder, in Huffman.Restrict]
b:4 [binder, in Huffman.Ordered]
b:4 [binder, in Huffman.PBTree]
b:4 [binder, in Huffman.HeightPred]
b:4 [binder, in Huffman.Huffman]
b:40 [binder, in Huffman.Weight]
b:42 [binder, in Huffman.Code]
b:5 [binder, in Huffman.ISort]
B:5 [binder, in Huffman.Weight]
B:50 [binder, in Huffman.Weight]
b:58 [binder, in Huffman.AuxLib]
b:6 [binder, in Huffman.UniqueKey]
b:6 [binder, in Huffman.Prod2List]
b:61 [binder, in Huffman.Prod2List]
b:62 [binder, in Huffman.Code]
b:67 [binder, in Huffman.AuxLib]
b:68 [binder, in Huffman.AuxLib]
b:71 [binder, in Huffman.Code]
b:72 [binder, in Huffman.Cover]
b:77 [binder, in Huffman.AuxLib]
b:8 [binder, in Huffman.ISort]
b:8 [binder, in Huffman.UniqueKey]
b:81 [binder, in Huffman.AuxLib]
b:88 [binder, in Huffman.Code]
b:89 [binder, in Huffman.Prod2List]
b:92 [binder, in Huffman.PBTree]
b:93 [binder, in Huffman.Code]
b:94 [binder, in Huffman.PBTree]
b:96 [binder, in Huffman.PBTree]
b:98 [binder, in Huffman.PBTree]
b:98 [binder, in Huffman.Prod2List]


C

ca:16 [binder, in Huffman.Code]
ca:31 [binder, in Huffman.Frequency]
cc:54 [binder, in Huffman.Huffman]
cc:59 [binder, in Huffman.Huffman]
code [definition, in Huffman.Code]
Code [section, in Huffman.Code]
Code [library]
code_dec [definition, in Huffman.Code]
Code.A [variable, in Huffman.Code]
Code.A_eq_dec [variable, in Huffman.Code]
compute_pbcode_not_null [lemma, in Huffman.PBTree]
compute_pbcode [definition, in Huffman.PBTree]
compute_code [definition, in Huffman.BTree]
correct_encoding [lemma, in Huffman.Code]
cover [inductive, in Huffman.Cover]
Cover [section, in Huffman.Cover]
Cover [library]
CoverMin [section, in Huffman.CoverMin]
CoverMin [library]
CoverMin.A [variable, in Huffman.CoverMin]
CoverMin.f [variable, in Huffman.CoverMin]
cover_all_leaves [lemma, in Huffman.Cover]
cover_dec [definition, in Huffman.Cover]
cover_all_cover [lemma, in Huffman.Cover]
cover_all_cover_aux [lemma, in Huffman.Cover]
cover_number_of_nodes [lemma, in Huffman.Cover]
cover_app [lemma, in Huffman.Cover]
cover_inv_app [lemma, in Huffman.Cover]
cover_inv_app_aux [lemma, in Huffman.Cover]
cover_one_inv [lemma, in Huffman.Cover]
cover_inv_leaf [lemma, in Huffman.Cover]
cover_inv_leaf_aux [lemma, in Huffman.Cover]
cover_in_inb [lemma, in Huffman.Cover]
cover_in_inb_inb [lemma, in Huffman.Cover]
cover_not_nil [lemma, in Huffman.Cover]
cover_cons_l [lemma, in Huffman.Cover]
cover_permutation [lemma, in Huffman.Cover]
cover_node [constructor, in Huffman.Cover]
cover_one [constructor, in Huffman.Cover]
cover_min_ex [lemma, in Huffman.CoverMin]
cover_min_permutation [lemma, in Huffman.CoverMin]
cover_min_one [lemma, in Huffman.CoverMin]
cover_min [definition, in Huffman.CoverMin]
cover_ordered_cover [lemma, in Huffman.OrderedCover]
Cover.A [variable, in Huffman.Cover]
Cover.empty [variable, in Huffman.Cover]
c1:113 [binder, in Huffman.Prod2List]
c1:115 [binder, in Huffman.Huffman]
c1:120 [binder, in Huffman.Code]
c1:257 [binder, in Huffman.PBTree]
c1:28 [binder, in Huffman.Build]
c1:31 [binder, in Huffman.Build]
c1:44 [binder, in Huffman.Weight]
c1:63 [binder, in Huffman.Code]
c1:83 [binder, in Huffman.Code]
c2:121 [binder, in Huffman.Code]
c2:258 [binder, in Huffman.PBTree]
c2:45 [binder, in Huffman.Weight]
c2:64 [binder, in Huffman.Code]
c2:84 [binder, in Huffman.Code]
c3:66 [binder, in Huffman.Huffman]
c:10 [binder, in Huffman.Restrict]
c:101 [binder, in Huffman.PBTree]
c:101 [binder, in Huffman.Code]
c:104 [binder, in Huffman.PBTree]
c:104 [binder, in Huffman.Code]
c:107 [binder, in Huffman.Code]
c:108 [binder, in Huffman.Code]
c:11 [binder, in Huffman.Code]
c:111 [binder, in Huffman.Prod2List]
c:114 [binder, in Huffman.Code]
c:114 [binder, in Huffman.Huffman]
c:119 [binder, in Huffman.Huffman]
c:12 [binder, in Huffman.Code]
c:124 [binder, in Huffman.Code]
c:125 [binder, in Huffman.Code]
C:13 [binder, in Huffman.AuxLib]
c:130 [binder, in Huffman.Code]
c:133 [binder, in Huffman.AuxLib]
c:137 [binder, in Huffman.Code]
c:139 [binder, in Huffman.AuxLib]
c:139 [binder, in Huffman.Code]
c:14 [binder, in Huffman.Restrict]
c:14 [binder, in Huffman.Code]
c:143 [binder, in Huffman.Code]
c:146 [binder, in Huffman.Code]
c:16 [binder, in Huffman.Restrict]
c:16 [binder, in Huffman.Weight]
c:17 [binder, in Huffman.Restrict]
c:17 [binder, in Huffman.Code]
c:18 [binder, in Huffman.Restrict]
c:19 [binder, in Huffman.Restrict]
c:20 [binder, in Huffman.Restrict]
c:20 [binder, in Huffman.Code]
c:212 [binder, in Huffman.PBTree]
c:214 [binder, in Huffman.PBTree]
c:220 [binder, in Huffman.PBTree]
c:222 [binder, in Huffman.PBTree]
c:228 [binder, in Huffman.PBTree]
c:230 [binder, in Huffman.PBTree]
c:233 [binder, in Huffman.PBTree]
c:248 [binder, in Huffman.PBTree]
c:249 [binder, in Huffman.PBTree]
c:25 [binder, in Huffman.Restrict]
c:25 [binder, in Huffman.UniqueKey]
c:25 [binder, in Huffman.Code]
c:251 [binder, in Huffman.PBTree]
c:253 [binder, in Huffman.PBTree]
c:255 [binder, in Huffman.PBTree]
c:26 [binder, in Huffman.Code]
c:27 [binder, in Huffman.Weight]
C:30 [binder, in Huffman.UniqueKey]
c:34 [binder, in Huffman.Prod2List]
c:42 [binder, in Huffman.Weight]
c:45 [binder, in Huffman.Huffman]
c:47 [binder, in Huffman.Weight]
c:5 [binder, in Huffman.Ordered]
c:51 [binder, in Huffman.Code]
c:53 [binder, in Huffman.Weight]
c:56 [binder, in Huffman.Code]
c:57 [binder, in Huffman.Code]
c:58 [binder, in Huffman.Weight]
c:6 [binder, in Huffman.Code]
c:60 [binder, in Huffman.Code]
c:61 [binder, in Huffman.Weight]
c:62 [binder, in Huffman.Prod2List]
c:63 [binder, in Huffman.Weight]
c:69 [binder, in Huffman.Code]
c:7 [binder, in Huffman.Weight]
c:73 [binder, in Huffman.AuxLib]
c:73 [binder, in Huffman.Code]
c:8 [binder, in Huffman.Restrict]
c:8 [binder, in Huffman.Huffman]
c:90 [binder, in Huffman.Prod2List]


D

decode [definition, in Huffman.Code]
decode_correct [lemma, in Huffman.Code]
decode_aux_correct [lemma, in Huffman.Code]
decode_aux [definition, in Huffman.Code]
distinct_pbleaves_pbadd_prop2 [lemma, in Huffman.PBTree]
distinct_pbleaves_pbadd_prop1 [lemma, in Huffman.PBTree]
distinct_pbleaves_pbright [lemma, in Huffman.PBTree]
distinct_pbleaves_pbleft [lemma, in Huffman.PBTree]
distinct_pbleaves_pbleaf [lemma, in Huffman.PBTree]
distinct_pbleaves_pr [lemma, in Huffman.PBTree]
distinct_pbleaves_pl [lemma, in Huffman.PBTree]
distinct_pbleaves_r [lemma, in Huffman.PBTree]
distinct_pbleaves_l [lemma, in Huffman.PBTree]
distinct_pbleaves_Leaf [lemma, in Huffman.PBTree]
distinct_pbleaves [definition, in Huffman.PBTree]
distinct_leaves_dec [definition, in Huffman.BTree]
distinct_leaves_r [lemma, in Huffman.BTree]
distinct_leaves_l [lemma, in Huffman.BTree]
distinct_leaves_leaf [lemma, in Huffman.BTree]
distinct_leaves [definition, in Huffman.BTree]
D:31 [binder, in Huffman.UniqueKey]
d:35 [binder, in Huffman.Prod2List]
d:63 [binder, in Huffman.Prod2List]


E

encode [definition, in Huffman.Code]
encode_permutation_val [lemma, in Huffman.Code]
encode_permutation [lemma, in Huffman.Code]
encode_cons_inv [lemma, in Huffman.Code]
encode_app [lemma, in Huffman.Code]
exist_first_max [lemma, in Huffman.AuxLib]
Extraction [library]


F

FindMin [section, in Huffman.AuxLib]
FindMin.A [variable, in Huffman.AuxLib]
FindMin.f [variable, in Huffman.AuxLib]
find_max_correct [lemma, in Huffman.AuxLib]
find_max [definition, in Huffman.AuxLib]
find_min_correct [lemma, in Huffman.AuxLib]
find_min [definition, in Huffman.AuxLib]
find_val_correct2 [lemma, in Huffman.Code]
find_val_correct1 [lemma, in Huffman.Code]
find_val [definition, in Huffman.Code]
find_code_permutation [lemma, in Huffman.Code]
find_code_app [lemma, in Huffman.Code]
find_code_correct2 [lemma, in Huffman.Code]
find_code_correct1 [lemma, in Huffman.Code]
find_code [definition, in Huffman.Code]
First [section, in Huffman.AuxLib]
FirstMax [section, in Huffman.AuxLib]
firstn_le_length_eq [lemma, in Huffman.AuxLib]
firstn_le_app2 [lemma, in Huffman.AuxLib]
firstn_le_app1 [lemma, in Huffman.AuxLib]
First.A [variable, in Huffman.AuxLib]
Fold [section, in Huffman.AuxLib]
fold_left_permutation [lemma, in Huffman.AuxLib]
fold_left_init [lemma, in Huffman.AuxLib]
fold_left_map [lemma, in Huffman.AuxLib]
fold_left_eta [lemma, in Huffman.AuxLib]
fold_pbadd_prop_node [lemma, in Huffman.PBTree]
fold_pbadd_prop_right [lemma, in Huffman.PBTree]
fold_pbadd_prop_left [lemma, in Huffman.PBTree]
fold_plus_permutation [lemma, in Huffman.Weight]
fold_plus_split [lemma, in Huffman.Weight]
Fold.A [variable, in Huffman.AuxLib]
Fold.B [variable, in Huffman.AuxLib]
Fold.f [variable, in Huffman.AuxLib]
Fold.g [variable, in Huffman.AuxLib]
Fold.h [variable, in Huffman.AuxLib]
Frequency [section, in Huffman.Frequency]
Frequency [library]
frequency_list_restric_code_map [lemma, in Huffman.Restrict]
frequency_not_null [lemma, in Huffman.Code]
frequency_length [lemma, in Huffman.Weight]
frequency_number_of_occurrences [lemma, in Huffman.Frequency]
frequency_list_unique [lemma, in Huffman.Frequency]
frequency_list_perm [lemma, in Huffman.Frequency]
frequency_list_in [lemma, in Huffman.Frequency]
frequency_list [definition, in Huffman.Frequency]
Frequency.A [variable, in Huffman.Frequency]
Frequency.A_eq_dec [variable, in Huffman.Frequency]
f1:10 [binder, in Huffman.AuxLib]
f:142 [binder, in Huffman.AuxLib]
f:17 [binder, in Huffman.Weight]
f:24 [binder, in Huffman.WeightTree]
f:33 [binder, in Huffman.UniqueKey]
f:75 [binder, in Huffman.AuxLib]
f:79 [binder, in Huffman.AuxLib]
f:8 [binder, in Huffman.Weight]


G

g:35 [binder, in Huffman.Ordered]


H

head:126 [binder, in Huffman.Code]
head:133 [binder, in Huffman.Code]
HeightPred [section, in Huffman.HeightPred]
HeightPred [library]
HeightPred.A [variable, in Huffman.HeightPred]
HeightPred.A_eq_dec [variable, in Huffman.HeightPred]
HeightPred.f [variable, in Huffman.HeightPred]
height_pred_compute_code [lemma, in Huffman.HeightPred]
height_pred_shrink [lemma, in Huffman.HeightPred]
height_pred_shrink_aux [lemma, in Huffman.HeightPred]
height_pred_disj_larger2 [lemma, in Huffman.HeightPred]
height_pred_disj_larger2_aux [lemma, in Huffman.HeightPred]
height_pred_disj_larger [lemma, in Huffman.HeightPred]
height_pred_disj_larger_aux [lemma, in Huffman.HeightPred]
height_pred_larger_ex [lemma, in Huffman.HeightPred]
height_pred_larger_strict [lemma, in Huffman.HeightPred]
height_pred_larger [lemma, in Huffman.HeightPred]
height_pred_weight [lemma, in Huffman.HeightPred]
height_pred_length [lemma, in Huffman.HeightPred]
height_pred_not_nil2 [lemma, in Huffman.HeightPred]
height_pred_not_nil1 [lemma, in Huffman.HeightPred]
height_pred_ordered_cover [lemma, in Huffman.HeightPred]
height_pred_node [constructor, in Huffman.HeightPred]
height_pred_nil [constructor, in Huffman.HeightPred]
height_pred [inductive, in Huffman.HeightPred]
height_pred_subst_pred [lemma, in Huffman.SubstPred]
huffman [definition, in Huffman.Huffman]
Huffman [section, in Huffman.Huffman]
Huffman [library]
huffman_aux [definition, in Huffman.Huffman]
huffman_aux_rec:50 [binder, in Huffman.Huffman]
huffman_aux_F [definition, in Huffman.Huffman]
huffman_aux_type [definition, in Huffman.Huffman]
huffman_build_minimum [lemma, in Huffman.Huffman]
Huffman.A [variable, in Huffman.Huffman]
Huffman.A_eq_dec [variable, in Huffman.Huffman]
Huffman.empty [variable, in Huffman.Huffman]
Huffman.frequency_more_than_one [variable, in Huffman.Huffman]
Huffman.m [variable, in Huffman.Huffman]


I

id_list [definition, in Huffman.Frequency]
inb [inductive, in Huffman.BTree]
inb_compute_ex [lemma, in Huffman.BTree]
inb_dec [definition, in Huffman.BTree]
inb_antisym [lemma, in Huffman.BTree]
inb_ex [lemma, in Huffman.BTree]
inb_trans [lemma, in Huffman.BTree]
inCompute_inb [lemma, in Huffman.BTree]
inleaf [constructor, in Huffman.BTree]
innodeL [constructor, in Huffman.BTree]
innodeR [constructor, in Huffman.BTree]
inpb [inductive, in Huffman.PBTree]
inpbleaf_pbadd_inv [lemma, in Huffman.PBTree]
inpbleaf_eq [lemma, in Huffman.PBTree]
inpb_pbbuild_inv [lemma, in Huffman.PBTree]
inpb_pbadd_ex [lemma, in Huffman.PBTree]
inpb_pbadd [lemma, in Huffman.PBTree]
inpb_compute_ex [lemma, in Huffman.PBTree]
inpb_ex [lemma, in Huffman.PBTree]
inpb_trans [lemma, in Huffman.PBTree]
inpb_dec [definition, in Huffman.PBTree]
inpb_node_r [constructor, in Huffman.PBTree]
inpb_node_l [constructor, in Huffman.PBTree]
inpb_right [constructor, in Huffman.PBTree]
inpb_left [constructor, in Huffman.PBTree]
inpb_leaf [constructor, in Huffman.PBTree]
insert [definition, in Huffman.ISort]
insert_permutation [lemma, in Huffman.ISort]
insert_ordered [lemma, in Huffman.ISort]
in_flat_map_ex [lemma, in Huffman.AuxLib]
in_flat_map_in [lemma, in Huffman.AuxLib]
in_map_fst_inv [lemma, in Huffman.AuxLib]
in_map_inv [lemma, in Huffman.AuxLib]
in_ex_app [lemma, in Huffman.AuxLib]
in_pbleaf_node [lemma, in Huffman.PBTree]
in_pbcompute_inpb [lemma, in Huffman.PBTree]
in_find_map [lemma, in Huffman.Code]
in_alphabet_dec [definition, in Huffman.Code]
in_alphabet_inv [lemma, in Huffman.Code]
in_alphabet_cons [lemma, in Huffman.Code]
in_alphabet_nil [lemma, in Huffman.Code]
in_alphabet_incl [lemma, in Huffman.Code]
in_alphabet [definition, in Huffman.Code]
in_alphabet_compute_code [lemma, in Huffman.BTree]
in_frequency_map_inv [lemma, in Huffman.Frequency]
in_frequency_map [lemma, in Huffman.Frequency]
isort [definition, in Huffman.ISort]
ISort [library]
ISortExample [section, in Huffman.ISort]
ISortExample.A [variable, in Huffman.ISort]
ISortExample.order [variable, in Huffman.ISort]
ISortExample.order_fun_false [variable, in Huffman.ISort]
ISortExample.order_fun_true [variable, in Huffman.ISort]
ISortExample.order_fun [variable, in Huffman.ISort]
isort_permutation [lemma, in Huffman.ISort]
isort_ordered [lemma, in Huffman.ISort]
is_prefix_refl [lemma, in Huffman.Code]
is_prefix [inductive, in Huffman.Code]


K

k:16 [binder, in Huffman.AuxLib]


L

lb1:49 [binder, in Huffman.Code]
lb1:54 [binder, in Huffman.Code]
lb1:86 [binder, in Huffman.PBTree]
lb1:88 [binder, in Huffman.BTree]
lb2:50 [binder, in Huffman.Code]
lb2:55 [binder, in Huffman.Code]
lb2:87 [binder, in Huffman.PBTree]
lb2:89 [binder, in Huffman.BTree]
leaf [constructor, in Huffman.BTree]
length_compute_lt_O [lemma, in Huffman.BTree]
length_encode_nId [lemma, in Huffman.Weight]
le_minus [lemma, in Huffman.AuxLib]
le_sum_correct2 [lemma, in Huffman.WeightTree]
le_sum_correct1 [lemma, in Huffman.WeightTree]
le_sum [definition, in Huffman.WeightTree]
lin:56 [binder, in Huffman.Huffman]
lin:61 [binder, in Huffman.Huffman]
List [section, in Huffman.AuxLib]
list_length_induction [definition, in Huffman.AuxLib]
list_length_ind [lemma, in Huffman.AuxLib]
List.A [variable, in Huffman.AuxLib]
List.B [variable, in Huffman.AuxLib]
List.C [variable, in Huffman.AuxLib]
List.f [variable, in Huffman.AuxLib]
ln1:11 [binder, in Huffman.HeightPred]
ln1:121 [binder, in Huffman.HeightPred]
ln1:60 [binder, in Huffman.HeightPred]
ln1:68 [binder, in Huffman.HeightPred]
ln1:79 [binder, in Huffman.HeightPred]
ln1:86 [binder, in Huffman.HeightPred]
ln1:98 [binder, in Huffman.HeightPred]
ln2:12 [binder, in Huffman.HeightPred]
ln2:122 [binder, in Huffman.HeightPred]
ln2:61 [binder, in Huffman.HeightPred]
ln2:69 [binder, in Huffman.HeightPred]
ln2:80 [binder, in Huffman.HeightPred]
ln2:87 [binder, in Huffman.HeightPred]
ln2:99 [binder, in Huffman.HeightPred]
ln3:65 [binder, in Huffman.HeightPred]
ln3:74 [binder, in Huffman.HeightPred]
ln:18 [binder, in Huffman.HeightPred]
ln:22 [binder, in Huffman.HeightPred]
ln:26 [binder, in Huffman.HeightPred]
ln:30 [binder, in Huffman.HeightPred]
ln:34 [binder, in Huffman.HeightPred]
ln:35 [binder, in Huffman.SubstPred]
ln:40 [binder, in Huffman.HeightPred]
ln:43 [binder, in Huffman.HeightPred]
ln:48 [binder, in Huffman.HeightPred]
ln:52 [binder, in Huffman.HeightPred]
ln:57 [binder, in Huffman.HeightPred]
ln:76 [binder, in Huffman.HeightPred]
ln:93 [binder, in Huffman.HeightPred]
l1:100 [binder, in Huffman.Prod2List]
l1:101 [binder, in Huffman.AuxLib]
l1:107 [binder, in Huffman.AuxLib]
l1:11 [binder, in Huffman.Build]
l1:11 [binder, in Huffman.OneStep]
l1:110 [binder, in Huffman.AuxLib]
l1:112 [binder, in Huffman.Code]
l1:113 [binder, in Huffman.AuxLib]
l1:114 [binder, in Huffman.Prod2List]
l1:115 [binder, in Huffman.AuxLib]
l1:115 [binder, in Huffman.PBTree]
l1:116 [binder, in Huffman.Code]
l1:117 [binder, in Huffman.PBTree]
l1:118 [binder, in Huffman.AuxLib]
l1:12 [binder, in Huffman.Cover]
l1:12 [binder, in Huffman.SubstPred]
l1:122 [binder, in Huffman.AuxLib]
l1:126 [binder, in Huffman.HeightPred]
l1:13 [binder, in Huffman.OrderedCover]
l1:14 [binder, in Huffman.OneStep]
l1:14 [binder, in Huffman.Weight]
l1:147 [binder, in Huffman.AuxLib]
l1:15 [binder, in Huffman.HeightPred]
l1:155 [binder, in Huffman.AuxLib]
l1:157 [binder, in Huffman.PBTree]
l1:158 [binder, in Huffman.AuxLib]
l1:159 [binder, in Huffman.PBTree]
l1:16 [binder, in Huffman.Cover]
l1:16 [binder, in Huffman.UniqueKey]
l1:16 [binder, in Huffman.OrderedCover]
l1:164 [binder, in Huffman.PBTree]
l1:169 [binder, in Huffman.AuxLib]
l1:171 [binder, in Huffman.AuxLib]
l1:174 [binder, in Huffman.AuxLib]
l1:176 [binder, in Huffman.AuxLib]
l1:179 [binder, in Huffman.PBTree]
l1:18 [binder, in Huffman.Build]
l1:180 [binder, in Huffman.AuxLib]
l1:182 [binder, in Huffman.PBTree]
l1:184 [binder, in Huffman.AuxLib]
l1:19 [binder, in Huffman.UniqueKey]
l1:194 [binder, in Huffman.PBTree]
l1:20 [binder, in Huffman.SubstPred]
l1:202 [binder, in Huffman.PBTree]
l1:205 [binder, in Huffman.PBTree]
l1:21 [binder, in Huffman.UniqueKey]
l1:21 [binder, in Huffman.WeightTree]
l1:23 [binder, in Huffman.Weight]
l1:235 [binder, in Huffman.PBTree]
l1:24 [binder, in Huffman.SubstPred]
l1:25 [binder, in Huffman.WeightTree]
l1:26 [binder, in Huffman.Ordered]
l1:28 [binder, in Huffman.AuxLib]
l1:28 [binder, in Huffman.SubstPred]
l1:3 [binder, in Huffman.Prod2List]
l1:3 [binder, in Huffman.OneStep]
l1:3 [binder, in Huffman.SameSumLeaves]
l1:30 [binder, in Huffman.Ordered]
l1:31 [binder, in Huffman.SubstPred]
l1:33 [binder, in Huffman.Code]
l1:36 [binder, in Huffman.AuxLib]
l1:36 [binder, in Huffman.Prod2List]
l1:37 [binder, in Huffman.SubstPred]
l1:39 [binder, in Huffman.Cover]
l1:43 [binder, in Huffman.Code]
l1:44 [binder, in Huffman.AuxLib]
l1:44 [binder, in Huffman.Cover]
l1:46 [binder, in Huffman.AuxLib]
l1:48 [binder, in Huffman.Cover]
l1:48 [binder, in Huffman.Huffman]
l1:53 [binder, in Huffman.AuxLib]
l1:58 [binder, in Huffman.Cover]
l1:6 [binder, in Huffman.Cover]
l1:6 [binder, in Huffman.SubstPred]
l1:61 [binder, in Huffman.Frequency]
l1:62 [binder, in Huffman.AuxLib]
l1:64 [binder, in Huffman.Prod2List]
l1:64 [binder, in Huffman.Frequency]
l1:7 [binder, in Huffman.Prod2List]
l1:7 [binder, in Huffman.Build]
l1:7 [binder, in Huffman.SameSumLeaves]
l1:8 [binder, in Huffman.CoverMin]
l1:8 [binder, in Huffman.OneStep]
l1:8 [binder, in Huffman.OrderedCover]
l1:80 [binder, in Huffman.Code]
l1:82 [binder, in Huffman.AuxLib]
l1:85 [binder, in Huffman.AuxLib]
l1:88 [binder, in Huffman.AuxLib]
l1:90 [binder, in Huffman.AuxLib]
l1:91 [binder, in Huffman.Prod2List]
l1:96 [binder, in Huffman.AuxLib]
l1:96 [binder, in Huffman.HeightPred]
l2:101 [binder, in Huffman.Prod2List]
l2:102 [binder, in Huffman.AuxLib]
l2:108 [binder, in Huffman.AuxLib]
l2:111 [binder, in Huffman.AuxLib]
l2:113 [binder, in Huffman.Code]
l2:115 [binder, in Huffman.Prod2List]
l2:116 [binder, in Huffman.AuxLib]
l2:118 [binder, in Huffman.PBTree]
l2:119 [binder, in Huffman.AuxLib]
l2:12 [binder, in Huffman.Build]
l2:12 [binder, in Huffman.OneStep]
l2:123 [binder, in Huffman.AuxLib]
l2:127 [binder, in Huffman.HeightPred]
l2:13 [binder, in Huffman.Cover]
l2:13 [binder, in Huffman.SubstPred]
l2:148 [binder, in Huffman.AuxLib]
l2:15 [binder, in Huffman.OneStep]
l2:15 [binder, in Huffman.Weight]
l2:15 [binder, in Huffman.OrderedCover]
l2:156 [binder, in Huffman.AuxLib]
l2:159 [binder, in Huffman.AuxLib]
l2:16 [binder, in Huffman.HeightPred]
l2:160 [binder, in Huffman.PBTree]
l2:17 [binder, in Huffman.UniqueKey]
l2:17 [binder, in Huffman.OrderedCover]
l2:170 [binder, in Huffman.AuxLib]
l2:172 [binder, in Huffman.AuxLib]
l2:175 [binder, in Huffman.AuxLib]
l2:177 [binder, in Huffman.AuxLib]
l2:181 [binder, in Huffman.AuxLib]
l2:185 [binder, in Huffman.AuxLib]
l2:19 [binder, in Huffman.Build]
l2:20 [binder, in Huffman.UniqueKey]
l2:21 [binder, in Huffman.SubstPred]
l2:22 [binder, in Huffman.UniqueKey]
l2:22 [binder, in Huffman.WeightTree]
l2:236 [binder, in Huffman.PBTree]
l2:25 [binder, in Huffman.SubstPred]
l2:26 [binder, in Huffman.WeightTree]
l2:27 [binder, in Huffman.Ordered]
l2:29 [binder, in Huffman.AuxLib]
l2:29 [binder, in Huffman.SubstPred]
l2:31 [binder, in Huffman.Ordered]
l2:32 [binder, in Huffman.SubstPred]
l2:33 [binder, in Huffman.Weight]
l2:34 [binder, in Huffman.Code]
l2:34 [binder, in Huffman.Weight]
l2:37 [binder, in Huffman.AuxLib]
l2:37 [binder, in Huffman.Prod2List]
l2:38 [binder, in Huffman.SubstPred]
l2:4 [binder, in Huffman.Prod2List]
l2:4 [binder, in Huffman.OneStep]
l2:4 [binder, in Huffman.SameSumLeaves]
l2:40 [binder, in Huffman.Cover]
l2:44 [binder, in Huffman.Code]
l2:45 [binder, in Huffman.AuxLib]
l2:45 [binder, in Huffman.Cover]
l2:47 [binder, in Huffman.AuxLib]
l2:49 [binder, in Huffman.Cover]
l2:49 [binder, in Huffman.Huffman]
l2:54 [binder, in Huffman.AuxLib]
l2:62 [binder, in Huffman.Frequency]
l2:63 [binder, in Huffman.AuxLib]
l2:65 [binder, in Huffman.Prod2List]
l2:65 [binder, in Huffman.Frequency]
l2:7 [binder, in Huffman.Cover]
l2:7 [binder, in Huffman.SubstPred]
l2:8 [binder, in Huffman.Prod2List]
l2:8 [binder, in Huffman.Build]
l2:8 [binder, in Huffman.SameSumLeaves]
l2:81 [binder, in Huffman.Code]
l2:83 [binder, in Huffman.AuxLib]
l2:86 [binder, in Huffman.AuxLib]
l2:89 [binder, in Huffman.AuxLib]
l2:9 [binder, in Huffman.CoverMin]
l2:9 [binder, in Huffman.OneStep]
l2:9 [binder, in Huffman.OrderedCover]
l2:91 [binder, in Huffman.AuxLib]
l2:92 [binder, in Huffman.Prod2List]
l2:97 [binder, in Huffman.HeightPred]
l2:98 [binder, in Huffman.AuxLib]
l3:10 [binder, in Huffman.OneStep]
l3:10 [binder, in Huffman.OrderedCover]
l3:102 [binder, in Huffman.Prod2List]
l3:103 [binder, in Huffman.AuxLib]
l3:116 [binder, in Huffman.Prod2List]
l3:13 [binder, in Huffman.OneStep]
l3:14 [binder, in Huffman.SubstPred]
l3:16 [binder, in Huffman.OneStep]
l3:161 [binder, in Huffman.PBTree]
l3:20 [binder, in Huffman.OrderedCover]
l3:24 [binder, in Huffman.OrderedCover]
l3:38 [binder, in Huffman.Prod2List]
l3:48 [binder, in Huffman.AuxLib]
l3:5 [binder, in Huffman.OneStep]
l3:5 [binder, in Huffman.SameSumLeaves]
l3:55 [binder, in Huffman.AuxLib]
l3:64 [binder, in Huffman.AuxLib]
l3:66 [binder, in Huffman.Prod2List]
l3:9 [binder, in Huffman.Prod2List]
l3:93 [binder, in Huffman.Prod2List]
l4:10 [binder, in Huffman.Prod2List]
l4:103 [binder, in Huffman.Prod2List]
l4:104 [binder, in Huffman.AuxLib]
l4:117 [binder, in Huffman.Prod2List]
l4:15 [binder, in Huffman.SubstPred]
l4:17 [binder, in Huffman.OneStep]
l4:22 [binder, in Huffman.OrderedCover]
l4:26 [binder, in Huffman.OrderedCover]
l4:29 [binder, in Huffman.Build]
l4:32 [binder, in Huffman.Build]
l4:39 [binder, in Huffman.Prod2List]
l4:49 [binder, in Huffman.AuxLib]
l4:56 [binder, in Huffman.AuxLib]
l4:6 [binder, in Huffman.SameSumLeaves]
l4:65 [binder, in Huffman.AuxLib]
l4:67 [binder, in Huffman.Prod2List]
l4:94 [binder, in Huffman.Prod2List]
l5:104 [binder, in Huffman.Prod2List]
l5:118 [binder, in Huffman.Prod2List]
l5:16 [binder, in Huffman.SubstPred]
l5:40 [binder, in Huffman.Prod2List]
l5:51 [binder, in Huffman.AuxLib]
l5:52 [binder, in Huffman.AuxLib]
l5:59 [binder, in Huffman.AuxLib]
l5:60 [binder, in Huffman.AuxLib]
l5:66 [binder, in Huffman.AuxLib]
l5:68 [binder, in Huffman.Prod2List]
l5:95 [binder, in Huffman.Prod2List]
l6:107 [binder, in Huffman.Prod2List]
l6:121 [binder, in Huffman.Prod2List]
l6:17 [binder, in Huffman.SubstPred]
l6:41 [binder, in Huffman.Prod2List]
l6:69 [binder, in Huffman.Prod2List]
l6:96 [binder, in Huffman.Prod2List]
l7:108 [binder, in Huffman.Prod2List]
l7:122 [binder, in Huffman.Prod2List]
l:10 [binder, in Huffman.CoverMin]
l:10 [binder, in Huffman.UniqueKey]
l:10 [binder, in Huffman.Frequency]
l:102 [binder, in Huffman.PBTree]
l:103 [binder, in Huffman.Code]
l:105 [binder, in Huffman.PBTree]
l:106 [binder, in Huffman.Code]
l:108 [binder, in Huffman.PBTree]
l:11 [binder, in Huffman.ISort]
l:11 [binder, in Huffman.OrderedCover]
l:113 [binder, in Huffman.Huffman]
l:117 [binder, in Huffman.Code]
l:12 [binder, in Huffman.Ordered]
l:120 [binder, in Huffman.AuxLib]
l:128 [binder, in Huffman.AuxLib]
l:132 [binder, in Huffman.AuxLib]
l:134 [binder, in Huffman.AuxLib]
l:135 [binder, in Huffman.HeightPred]
l:138 [binder, in Huffman.AuxLib]
l:14 [binder, in Huffman.ISort]
l:14 [binder, in Huffman.UniqueKey]
l:14 [binder, in Huffman.Frequency]
l:142 [binder, in Huffman.HeightPred]
l:149 [binder, in Huffman.HeightPred]
l:15 [binder, in Huffman.AuxLib]
l:15 [binder, in Huffman.Ordered]
l:15 [binder, in Huffman.Build]
l:150 [binder, in Huffman.AuxLib]
l:156 [binder, in Huffman.PBTree]
l:156 [binder, in Huffman.HeightPred]
L:16 [binder, in Huffman.ISort]
l:162 [binder, in Huffman.AuxLib]
l:167 [binder, in Huffman.AuxLib]
l:169 [binder, in Huffman.PBTree]
l:17 [binder, in Huffman.Cover]
l:17 [binder, in Huffman.Ordered]
l:173 [binder, in Huffman.PBTree]
l:177 [binder, in Huffman.PBTree]
l:18 [binder, in Huffman.ISort]
l:18 [binder, in Huffman.UniqueKey]
l:19 [binder, in Huffman.Cover]
l:19 [binder, in Huffman.Code]
l:197 [binder, in Huffman.PBTree]
l:198 [binder, in Huffman.PBTree]
l:20 [binder, in Huffman.Ordered]
l:20 [binder, in Huffman.HeightPred]
l:20 [binder, in Huffman.WeightTree]
l:206 [binder, in Huffman.PBTree]
l:207 [binder, in Huffman.PBTree]
l:21 [binder, in Huffman.Cover]
l:21 [binder, in Huffman.ISort]
l:21 [binder, in Huffman.Build]
l:215 [binder, in Huffman.PBTree]
l:22 [binder, in Huffman.AuxLib]
l:22 [binder, in Huffman.ISort]
l:22 [binder, in Huffman.Code]
l:223 [binder, in Huffman.PBTree]
l:23 [binder, in Huffman.Ordered]
l:23 [binder, in Huffman.Build]
l:23 [binder, in Huffman.Code]
l:231 [binder, in Huffman.PBTree]
l:239 [binder, in Huffman.PBTree]
l:24 [binder, in Huffman.HeightPred]
l:24 [binder, in Huffman.Weight]
l:244 [binder, in Huffman.PBTree]
l:25 [binder, in Huffman.Cover]
l:25 [binder, in Huffman.Build]
l:252 [binder, in Huffman.PBTree]
l:26 [binder, in Huffman.UniqueKey]
l:26 [binder, in Huffman.Frequency]
l:27 [binder, in Huffman.UniqueKey]
l:28 [binder, in Huffman.HeightPred]
l:28 [binder, in Huffman.Frequency]
l:29 [binder, in Huffman.Cover]
l:29 [binder, in Huffman.Code]
l:3 [binder, in Huffman.CoverMin]
l:30 [binder, in Huffman.AuxLib]
l:30 [binder, in Huffman.Frequency]
l:32 [binder, in Huffman.Cover]
l:32 [binder, in Huffman.UniqueKey]
l:32 [binder, in Huffman.HeightPred]
l:32 [binder, in Huffman.Code]
l:33 [binder, in Huffman.Build]
l:35 [binder, in Huffman.Code]
l:36 [binder, in Huffman.Ordered]
l:36 [binder, in Huffman.HeightPred]
l:38 [binder, in Huffman.Cover]
l:38 [binder, in Huffman.Huffman]
l:39 [binder, in Huffman.AuxLib]
l:39 [binder, in Huffman.HeightPred]
l:39 [binder, in Huffman.Frequency]
l:41 [binder, in Huffman.Code]
l:43 [binder, in Huffman.AuxLib]
l:43 [binder, in Huffman.Cover]
l:45 [binder, in Huffman.HeightPred]
l:45 [binder, in Huffman.Code]
l:45 [binder, in Huffman.Frequency]
l:46 [binder, in Huffman.Code]
l:47 [binder, in Huffman.Frequency]
l:48 [binder, in Huffman.Frequency]
l:5 [binder, in Huffman.OrderedCover]
l:50 [binder, in Huffman.HeightPred]
l:50 [binder, in Huffman.Frequency]
l:51 [binder, in Huffman.Cover]
l:51 [binder, in Huffman.Weight]
l:53 [binder, in Huffman.Frequency]
l:54 [binder, in Huffman.Cover]
l:54 [binder, in Huffman.HeightPred]
l:57 [binder, in Huffman.Frequency]
l:59 [binder, in Huffman.HeightPred]
l:59 [binder, in Huffman.Code]
l:6 [binder, in Huffman.Weight]
l:60 [binder, in Huffman.Cover]
l:62 [binder, in Huffman.Cover]
l:62 [binder, in Huffman.BTree]
l:63 [binder, in Huffman.PBTree]
l:64 [binder, in Huffman.Cover]
l:65 [binder, in Huffman.BTree]
l:66 [binder, in Huffman.PBTree]
l:66 [binder, in Huffman.Code]
l:67 [binder, in Huffman.Cover]
l:69 [binder, in Huffman.AuxLib]
l:69 [binder, in Huffman.Cover]
l:7 [binder, in Huffman.UniqueKey]
l:71 [binder, in Huffman.HeightPred]
l:72 [binder, in Huffman.AuxLib]
l:72 [binder, in Huffman.Code]
l:73 [binder, in Huffman.Cover]
l:74 [binder, in Huffman.AuxLib]
l:75 [binder, in Huffman.Code]
l:77 [binder, in Huffman.Code]
l:78 [binder, in Huffman.AuxLib]
l:78 [binder, in Huffman.HeightPred]
l:8 [binder, in Huffman.AuxLib]
l:8 [binder, in Huffman.Code]
l:87 [binder, in Huffman.Code]
l:89 [binder, in Huffman.HeightPred]
l:9 [binder, in Huffman.Build]
l:93 [binder, in Huffman.PBTree]
l:94 [binder, in Huffman.Code]
l:95 [binder, in Huffman.PBTree]
l:95 [binder, in Huffman.HeightPred]
l:97 [binder, in Huffman.PBTree]
l:98 [binder, in Huffman.Code]
l:99 [binder, in Huffman.PBTree]


M

map2 [definition, in Huffman.AuxLib]
map2 [section, in Huffman.AuxLib]
map2_app [lemma, in Huffman.AuxLib]
map2.A [variable, in Huffman.AuxLib]
map2.B [variable, in Huffman.AuxLib]
map2.C [variable, in Huffman.AuxLib]
map2.f [variable, in Huffman.AuxLib]
m1:118 [binder, in Huffman.Code]
m1:122 [binder, in Huffman.Code]
m1:131 [binder, in Huffman.Code]
m1:140 [binder, in Huffman.Code]
m1:15 [binder, in Huffman.Restrict]
m1:60 [binder, in Huffman.Weight]
m1:60 [binder, in Huffman.Frequency]
m1:9 [binder, in Huffman.Code]
m2:10 [binder, in Huffman.Code]
m2:123 [binder, in Huffman.Code]
m2:132 [binder, in Huffman.Code]
m2:141 [binder, in Huffman.Code]
m:109 [binder, in Huffman.Code]
m:119 [binder, in Huffman.Code]
m:127 [binder, in Huffman.Code]
m:13 [binder, in Huffman.Code]
m:138 [binder, in Huffman.Code]
m:144 [binder, in Huffman.Code]
m:145 [binder, in Huffman.Code]
m:162 [binder, in Huffman.HeightPred]
m:24 [binder, in Huffman.Code]
m:26 [binder, in Huffman.Weight]
m:32 [binder, in Huffman.Frequency]
m:35 [binder, in Huffman.Frequency]
m:41 [binder, in Huffman.Weight]
m:43 [binder, in Huffman.Weight]
m:44 [binder, in Huffman.Frequency]
m:46 [binder, in Huffman.Weight]
m:5 [binder, in Huffman.Code]
m:52 [binder, in Huffman.Weight]
m:56 [binder, in Huffman.Weight]
m:58 [binder, in Huffman.Frequency]
m:59 [binder, in Huffman.Weight]
m:62 [binder, in Huffman.Weight]
m:68 [binder, in Huffman.Frequency]
m:7 [binder, in Huffman.Restrict]
m:82 [binder, in Huffman.BTree]


N

nnil:52 [binder, in Huffman.Huffman]
nnil:57 [binder, in Huffman.Huffman]
node [constructor, in Huffman.BTree]
NoDup_app_inv_r [lemma, in Huffman.AuxLib]
NoDup_app_inv_l [lemma, in Huffman.AuxLib]
NoDup_app_inv [lemma, in Huffman.AuxLib]
NoDup_app [lemma, in Huffman.AuxLib]
NoDup_pbadd_prop2 [lemma, in Huffman.PBTree]
NoDup_unique_key [lemma, in Huffman.UniqueKey]
NoDup_unique_key [lemma, in Huffman.Weight]
NoDup_ordered_cover [lemma, in Huffman.OrderedCover]
not_null_find_val [lemma, in Huffman.Code]
not_in_find_map [lemma, in Huffman.Code]
not_in_find_code [lemma, in Huffman.Code]
not_null_map [lemma, in Huffman.Code]
not_null_app [lemma, in Huffman.Code]
not_null_cons [lemma, in Huffman.Code]
not_null_inv [lemma, in Huffman.Code]
not_null [definition, in Huffman.Code]
not_null_m [lemma, in Huffman.Huffman]
number_of_nodes_inb_le [lemma, in Huffman.BTree]
number_of_nodes [definition, in Huffman.BTree]
number_of_occurrences_permutation [lemma, in Huffman.Frequency]
number_of_occurrences_app [lemma, in Huffman.Frequency]
number_of_occurrences_permutation_ex [lemma, in Huffman.Frequency]
number_of_occurrences_O [lemma, in Huffman.Frequency]
number_of_occurrences [definition, in Huffman.Frequency]
n1:104 [binder, in Huffman.HeightPred]
n1:105 [binder, in Huffman.HeightPred]
n1:124 [binder, in Huffman.AuxLib]
n1:125 [binder, in Huffman.AuxLib]
n1:128 [binder, in Huffman.HeightPred]
n1:129 [binder, in Huffman.HeightPred]
n1:42 [binder, in Huffman.HeightPred]
n1:47 [binder, in Huffman.HeightPred]
n1:55 [binder, in Huffman.HeightPred]
n1:63 [binder, in Huffman.HeightPred]
n1:64 [binder, in Huffman.HeightPred]
n1:72 [binder, in Huffman.HeightPred]
n1:73 [binder, in Huffman.HeightPred]
n1:82 [binder, in Huffman.HeightPred]
n1:83 [binder, in Huffman.HeightPred]
n1:90 [binder, in Huffman.HeightPred]
n1:91 [binder, in Huffman.HeightPred]
n2:131 [binder, in Huffman.AuxLib]
n2:137 [binder, in Huffman.AuxLib]
n:10 [binder, in Huffman.HeightPred]
n:106 [binder, in Huffman.AuxLib]
n:109 [binder, in Huffman.AuxLib]
n:112 [binder, in Huffman.AuxLib]
n:114 [binder, in Huffman.AuxLib]
n:117 [binder, in Huffman.AuxLib]
n:118 [binder, in Huffman.HeightPred]
n:130 [binder, in Huffman.HeightPred]
n:163 [binder, in Huffman.AuxLib]
n:168 [binder, in Huffman.AuxLib]
n:17 [binder, in Huffman.HeightPred]
n:173 [binder, in Huffman.AuxLib]
n:21 [binder, in Huffman.HeightPred]
n:25 [binder, in Huffman.HeightPred]
n:25 [binder, in Huffman.Weight]
n:29 [binder, in Huffman.HeightPred]
n:33 [binder, in Huffman.HeightPred]
n:34 [binder, in Huffman.Frequency]
n:34 [binder, in Huffman.SubstPred]
n:37 [binder, in Huffman.HeightPred]
n:38 [binder, in Huffman.Frequency]
n:41 [binder, in Huffman.HeightPred]
n:43 [binder, in Huffman.Frequency]
n:46 [binder, in Huffman.HeightPred]
n:51 [binder, in Huffman.HeightPred]
n:55 [binder, in Huffman.Cover]
n:56 [binder, in Huffman.HeightPred]
n:6 [binder, in Huffman.Frequency]
n:61 [binder, in Huffman.Cover]
n:66 [binder, in Huffman.Cover]
n:66 [binder, in Huffman.HeightPred]
n:75 [binder, in Huffman.HeightPred]
n:8 [binder, in Huffman.HeightPred]
n:84 [binder, in Huffman.HeightPred]
n:92 [binder, in Huffman.HeightPred]


O

obuildf [definition, in Huffman.Build]
OneStep [section, in Huffman.OneStep]
OneStep [library]
OneStep.A [variable, in Huffman.OneStep]
OneStep.f [variable, in Huffman.OneStep]
one_cover_ex [lemma, in Huffman.Cover]
one_step_comp [lemma, in Huffman.OneStep]
one_step_same_sum_leaves [lemma, in Huffman.OneStep]
one_step_weight_tree_list [lemma, in Huffman.OneStep]
one_step [definition, in Huffman.OneStep]
ordered [inductive, in Huffman.Ordered]
ordered [section, in Huffman.Ordered]
Ordered [library]
OrderedCover [section, in Huffman.OrderedCover]
OrderedCover [library]
OrderedCover.A [variable, in Huffman.OrderedCover]
ordered_map_inv [lemma, in Huffman.Ordered]
ordered_perm_antisym_eq [lemma, in Huffman.Ordered]
ordered_trans_app [lemma, in Huffman.Ordered]
ordered_trans [lemma, in Huffman.Ordered]
ordered_skip [lemma, in Huffman.Ordered]
ordered_inv [lemma, in Huffman.Ordered]
ordered_inv_order [lemma, in Huffman.Ordered]
ordered_cons [constructor, in Huffman.Ordered]
ordered_one [constructor, in Huffman.Ordered]
ordered_nil [constructor, in Huffman.Ordered]
ordered_cover_height_pred [lemma, in Huffman.HeightPred]
ordered_sum_leaves_eq [lemma, in Huffman.WeightTree]
ordered_cover_cover [lemma, in Huffman.OrderedCover]
ordered_cover_node [constructor, in Huffman.OrderedCover]
ordered_cover_one [constructor, in Huffman.OrderedCover]
ordered_cover [inductive, in Huffman.OrderedCover]
ordered_cover_subst_pred [lemma, in Huffman.SubstPred]
ordered.A [variable, in Huffman.Ordered]
ordered.order [variable, in Huffman.Ordered]
ordered.order_trans [variable, in Huffman.Ordered]
order:34 [binder, in Huffman.Ordered]
ord:53 [binder, in Huffman.Huffman]
ord:58 [binder, in Huffman.Huffman]


P

pbadd [definition, in Huffman.PBTree]
pbadd_prop2 [lemma, in Huffman.PBTree]
pbadd_prop1 [lemma, in Huffman.PBTree]
pbbuild [definition, in Huffman.PBTree]
pbbuild_pbnode [lemma, in Huffman.PBTree]
pbbuild_true_pbright [lemma, in Huffman.PBTree]
pbbuild_compute_peq [lemma, in Huffman.PBTree]
pbbuild_distinct_pbleaves [lemma, in Huffman.PBTree]
pbbuild_compute_perm [lemma, in Huffman.PBTree]
pbfree [inductive, in Huffman.PBTree]
pbfree_pbbuild_prop1 [lemma, in Huffman.PBTree]
pbfree_pbadd_prop2 [lemma, in Huffman.PBTree]
pbfree_pbadd_prop1 [lemma, in Huffman.PBTree]
pbfree_node2 [constructor, in Huffman.PBTree]
pbfree_node1 [constructor, in Huffman.PBTree]
pbfree_right2 [constructor, in Huffman.PBTree]
pbfree_right1 [constructor, in Huffman.PBTree]
pbfree_left2 [constructor, in Huffman.PBTree]
pbfree_left1 [constructor, in Huffman.PBTree]
pbleaf [constructor, in Huffman.PBTree]
pbleaf_or_not [lemma, in Huffman.PBTree]
pbleft [constructor, in Huffman.PBTree]
pbnode [constructor, in Huffman.PBTree]
pbright [constructor, in Huffman.PBTree]
pbtree [inductive, in Huffman.PBTree]
PBTree [section, in Huffman.PBTree]
PBTree [library]
pbtree_dec [definition, in Huffman.PBTree]
PBTree.A [variable, in Huffman.PBTree]
PBTree.A_eq_dec [variable, in Huffman.PBTree]
PBTree.empty [variable, in Huffman.PBTree]
PBTREE2BTREE [section, in Huffman.PBTree2BTree]
PBTree2BTree [library]
PBTREE2BTREE.A [variable, in Huffman.PBTree2BTree]
PBTREE2BTREE.A_eq_dec [variable, in Huffman.PBTree2BTree]
PBTREE2BTREE.empty [variable, in Huffman.PBTree2BTree]
pb_unique_prefix [lemma, in Huffman.PBTree]
pb_unique_key [lemma, in Huffman.PBTree]
pb_unique_prefix1 [lemma, in Huffman.PBTree]
Permutation [section, in Huffman.AuxLib]
Permutation_transposition [lemma, in Huffman.AuxLib]
Permutation_dec [definition, in Huffman.AuxLib]
permutation_all_permutations [lemma, in Huffman.AuxLib]
permutation_all_permutations_aux [lemma, in Huffman.AuxLib]
Permutation.A [variable, in Huffman.AuxLib]
prefixCons [constructor, in Huffman.Code]
prefixNull [constructor, in Huffman.Code]
prod2list [definition, in Huffman.Prod2List]
Prod2List [section, in Huffman.Prod2List]
Prod2List [library]
prod2list_reorder2 [lemma, in Huffman.Prod2List]
prod2list_reorder [lemma, in Huffman.Prod2List]
prod2list_eq [lemma, in Huffman.Prod2List]
prod2list_le_r [lemma, in Huffman.Prod2List]
prod2list_le_l [lemma, in Huffman.Prod2List]
prod2list_app [lemma, in Huffman.Prod2List]
Prod2List.A [variable, in Huffman.Prod2List]
Prod2List.f [variable, in Huffman.Prod2List]
p:15 [binder, in Huffman.Frequency]
p:153 [binder, in Huffman.AuxLib]
p:16 [binder, in Huffman.Frequency]
p:160 [binder, in Huffman.AuxLib]
p:161 [binder, in Huffman.AuxLib]
p:166 [binder, in Huffman.AuxLib]
p:17 [binder, in Huffman.Frequency]
p:18 [binder, in Huffman.Frequency]
p:19 [binder, in Huffman.Frequency]
p:20 [binder, in Huffman.Frequency]
p:21 [binder, in Huffman.Frequency]
p:22 [binder, in Huffman.Frequency]
P:27 [binder, in Huffman.AuxLib]
p:32 [binder, in Huffman.BTree]
P:35 [binder, in Huffman.AuxLib]
p:46 [binder, in Huffman.Frequency]
p:60 [binder, in Huffman.PBTree]
p:64 [binder, in Huffman.BTree]
p:65 [binder, in Huffman.PBTree]
p:78 [binder, in Huffman.Code]
p:8 [binder, in Huffman.PBTree]
p:85 [binder, in Huffman.Code]
p:91 [binder, in Huffman.Code]


R

rec:38 [binder, in Huffman.AuxLib]
Restrict [section, in Huffman.Restrict]
Restrict [library]
restrict_code_pbbuild [lemma, in Huffman.Restrict]
restrict_not_null [lemma, in Huffman.Restrict]
restrict_unique_prefix [lemma, in Huffman.Restrict]
restrict_code_encode [lemma, in Huffman.Restrict]
restrict_code_encode_incl [lemma, in Huffman.Restrict]
restrict_code_in [lemma, in Huffman.Restrict]
restrict_code_unique_key [lemma, in Huffman.Restrict]
restrict_code [definition, in Huffman.Restrict]
restrict_code_encode_length [lemma, in Huffman.Weight]
restrict_code_encode_length_inc [lemma, in Huffman.Weight]
restrict_code_in [lemma, in Huffman.Weight]
restrict_code_unique_key [lemma, in Huffman.Weight]
restrict_code [definition, in Huffman.Weight]
Restrict.A [variable, in Huffman.Restrict]
Restrict.A_eq_dec [variable, in Huffman.Restrict]
Restrict.empty [variable, in Huffman.Restrict]
Restrict.m [variable, in Huffman.Restrict]


S

SameSumLeaves [section, in Huffman.SameSumLeaves]
SameSumLeaves [library]
SameSumLeaves.A [variable, in Huffman.SameSumLeaves]
SameSumLeaves.f [variable, in Huffman.SameSumLeaves]
same_length_ex [lemma, in Huffman.AuxLib]
same_sum_leaves_length [lemma, in Huffman.SameSumLeaves]
same_sum_leaves [definition, in Huffman.SameSumLeaves]
skipn_le_app2 [lemma, in Huffman.AuxLib]
skipn_le_app1 [lemma, in Huffman.AuxLib]
sl:55 [binder, in Huffman.Huffman]
sl:60 [binder, in Huffman.Huffman]
split_one_in_ex [lemma, in Huffman.AuxLib]
split_one_permutation [lemma, in Huffman.AuxLib]
split_one [definition, in Huffman.AuxLib]
SubstPred [section, in Huffman.SubstPred]
SubstPred [library]
SubstPred.A [variable, in Huffman.SubstPred]
subst_pred_length [lemma, in Huffman.SubstPred]
subst_pred_ordered_cover_r [lemma, in Huffman.SubstPred]
subst_pred_ordered_cover_l [lemma, in Huffman.SubstPred]
subst_pred_node [constructor, in Huffman.SubstPred]
subst_pred_id [constructor, in Huffman.SubstPred]
subst_pred [inductive, in Huffman.SubstPred]
sum_order [definition, in Huffman.WeightTree]
sum_leaves [definition, in Huffman.WeightTree]


T

to_btree_smaller [lemma, in Huffman.PBTree2BTree]
to_btree_distinct_pbleaves [lemma, in Huffman.PBTree2BTree]
to_btree_distinct_leaves [lemma, in Huffman.PBTree2BTree]
to_btree_all_leaves [lemma, in Huffman.PBTree2BTree]
to_btree_inpb [lemma, in Huffman.PBTree2BTree]
to_btree_inb [lemma, in Huffman.PBTree2BTree]
to_btree [definition, in Huffman.PBTree2BTree]
Tree [section, in Huffman.BTree]
Tree.A [variable, in Huffman.BTree]
Tree.A_eq_dec [variable, in Huffman.BTree]
Tree.empty [variable, in Huffman.BTree]
t0:36 [binder, in Huffman.PBTree]
t0:41 [binder, in Huffman.BTree]
t1:102 [binder, in Huffman.HeightPred]
t1:12 [binder, in Huffman.BTree]
t1:124 [binder, in Huffman.HeightPred]
t1:13 [binder, in Huffman.HeightPred]
t1:13 [binder, in Huffman.Build]
t1:14 [binder, in Huffman.Cover]
t1:15 [binder, in Huffman.PBTree]
t1:15 [binder, in Huffman.BTree]
t1:16 [binder, in Huffman.Build]
t1:17 [binder, in Huffman.BTree]
t1:18 [binder, in Huffman.PBTree]
t1:18 [binder, in Huffman.WeightTree]
t1:18 [binder, in Huffman.SubstPred]
t1:180 [binder, in Huffman.PBTree]
t1:183 [binder, in Huffman.PBTree]
t1:21 [binder, in Huffman.PBTree]
t1:22 [binder, in Huffman.Cover]
t1:22 [binder, in Huffman.SubstPred]
t1:24 [binder, in Huffman.PBTree]
t1:25 [binder, in Huffman.BTree]
t1:26 [binder, in Huffman.Cover]
t1:26 [binder, in Huffman.SubstPred]
t1:27 [binder, in Huffman.BTree]
t1:30 [binder, in Huffman.PBTree]
t1:30 [binder, in Huffman.SubstPred]
t1:33 [binder, in Huffman.Cover]
t1:36 [binder, in Huffman.Cover]
t1:36 [binder, in Huffman.SubstPred]
t1:37 [binder, in Huffman.PBTree]
t1:4 [binder, in Huffman.CoverMin]
t1:4 [binder, in Huffman.SubstPred]
t1:40 [binder, in Huffman.PBTree]
t1:41 [binder, in Huffman.Cover]
t1:42 [binder, in Huffman.PBTree]
t1:42 [binder, in Huffman.BTree]
t1:44 [binder, in Huffman.PBTree]
t1:45 [binder, in Huffman.PBTree]
t1:45 [binder, in Huffman.BTree]
t1:46 [binder, in Huffman.Cover]
t1:47 [binder, in Huffman.BTree]
t1:6 [binder, in Huffman.OneStep]
t1:6 [binder, in Huffman.OrderedCover]
t1:8 [binder, in Huffman.Cover]
t1:8 [binder, in Huffman.SubstPred]
t2:103 [binder, in Huffman.HeightPred]
t2:125 [binder, in Huffman.HeightPred]
t2:13 [binder, in Huffman.BTree]
t2:14 [binder, in Huffman.HeightPred]
t2:14 [binder, in Huffman.Build]
t2:15 [binder, in Huffman.Cover]
t2:16 [binder, in Huffman.PBTree]
t2:16 [binder, in Huffman.BTree]
t2:17 [binder, in Huffman.Build]
t2:18 [binder, in Huffman.BTree]
t2:19 [binder, in Huffman.PBTree]
t2:19 [binder, in Huffman.WeightTree]
t2:19 [binder, in Huffman.SubstPred]
t2:22 [binder, in Huffman.PBTree]
t2:23 [binder, in Huffman.Cover]
t2:23 [binder, in Huffman.SubstPred]
t2:25 [binder, in Huffman.PBTree]
t2:26 [binder, in Huffman.BTree]
t2:27 [binder, in Huffman.Cover]
t2:27 [binder, in Huffman.SubstPred]
t2:28 [binder, in Huffman.BTree]
t2:31 [binder, in Huffman.PBTree]
t2:33 [binder, in Huffman.SubstPred]
t2:34 [binder, in Huffman.Cover]
t2:37 [binder, in Huffman.Cover]
t2:38 [binder, in Huffman.PBTree]
t2:39 [binder, in Huffman.SubstPred]
t2:41 [binder, in Huffman.PBTree]
t2:42 [binder, in Huffman.Cover]
t2:43 [binder, in Huffman.PBTree]
t2:43 [binder, in Huffman.BTree]
t2:46 [binder, in Huffman.BTree]
t2:47 [binder, in Huffman.Cover]
t2:48 [binder, in Huffman.BTree]
t2:5 [binder, in Huffman.CoverMin]
t2:5 [binder, in Huffman.SubstPred]
t2:7 [binder, in Huffman.OneStep]
t2:7 [binder, in Huffman.OrderedCover]
t2:9 [binder, in Huffman.Cover]
t2:9 [binder, in Huffman.SubstPred]
t3:10 [binder, in Huffman.Cover]
t3:10 [binder, in Huffman.SubstPred]
t3:19 [binder, in Huffman.BTree]
t3:24 [binder, in Huffman.Cover]
t3:32 [binder, in Huffman.PBTree]
t4:11 [binder, in Huffman.SubstPred]
t:10 [binder, in Huffman.Build]
t:10 [binder, in Huffman.BTree]
t:107 [binder, in Huffman.PBTree]
t:11 [binder, in Huffman.Cover]
t:11 [binder, in Huffman.CoverMin]
t:11 [binder, in Huffman.BTree]
t:12 [binder, in Huffman.OrderedCover]
t:123 [binder, in Huffman.HeightPred]
t:13 [binder, in Huffman.PBTree]
t:13 [binder, in Huffman.PBTree2BTree]
t:131 [binder, in Huffman.HeightPred]
t:14 [binder, in Huffman.PBTree]
t:14 [binder, in Huffman.WeightTree]
t:14 [binder, in Huffman.BTree]
t:14 [binder, in Huffman.OrderedCover]
t:16 [binder, in Huffman.PBTree2BTree]
t:163 [binder, in Huffman.HeightPred]
t:17 [binder, in Huffman.PBTree]
t:18 [binder, in Huffman.Cover]
t:18 [binder, in Huffman.OrderedCover]
t:184 [binder, in Huffman.PBTree]
t:185 [binder, in Huffman.PBTree]
t:188 [binder, in Huffman.PBTree]
t:19 [binder, in Huffman.HeightPred]
t:190 [binder, in Huffman.PBTree]
t:192 [binder, in Huffman.PBTree]
t:193 [binder, in Huffman.PBTree]
t:20 [binder, in Huffman.Cover]
t:20 [binder, in Huffman.PBTree]
t:20 [binder, in Huffman.Build]
t:20 [binder, in Huffman.BTree]
t:203 [binder, in Huffman.PBTree]
t:22 [binder, in Huffman.Build]
t:23 [binder, in Huffman.PBTree]
t:23 [binder, in Huffman.HeightPred]
t:237 [binder, in Huffman.PBTree]
t:24 [binder, in Huffman.Build]
t:254 [binder, in Huffman.PBTree]
t:26 [binder, in Huffman.Build]
t:27 [binder, in Huffman.HeightPred]
t:28 [binder, in Huffman.Cover]
t:3 [binder, in Huffman.WeightTree]
t:31 [binder, in Huffman.HeightPred]
t:33 [binder, in Huffman.PBTree]
t:33 [binder, in Huffman.BTree]
t:34 [binder, in Huffman.Build]
t:35 [binder, in Huffman.Cover]
t:35 [binder, in Huffman.PBTree]
t:35 [binder, in Huffman.HeightPred]
t:36 [binder, in Huffman.BTree]
t:38 [binder, in Huffman.HeightPred]
t:38 [binder, in Huffman.BTree]
t:4 [binder, in Huffman.OrderedCover]
t:40 [binder, in Huffman.BTree]
t:44 [binder, in Huffman.HeightPred]
t:47 [binder, in Huffman.PBTree]
t:48 [binder, in Huffman.PBTree]
t:49 [binder, in Huffman.HeightPred]
t:49 [binder, in Huffman.BTree]
t:5 [binder, in Huffman.Cover]
t:5 [binder, in Huffman.Build]
t:50 [binder, in Huffman.Cover]
t:50 [binder, in Huffman.BTree]
t:53 [binder, in Huffman.HeightPred]
t:58 [binder, in Huffman.HeightPred]
t:59 [binder, in Huffman.BTree]
t:6 [binder, in Huffman.CoverMin]
t:6 [binder, in Huffman.Build]
t:60 [binder, in Huffman.BTree]
t:61 [binder, in Huffman.PBTree]
t:63 [binder, in Huffman.Cover]
t:65 [binder, in Huffman.Cover]
t:68 [binder, in Huffman.Cover]
t:7 [binder, in Huffman.CoverMin]
t:70 [binder, in Huffman.Cover]
t:70 [binder, in Huffman.HeightPred]
t:74 [binder, in Huffman.Cover]
t:75 [binder, in Huffman.Cover]
t:77 [binder, in Huffman.HeightPred]
t:83 [binder, in Huffman.PBTree]
t:83 [binder, in Huffman.BTree]
t:85 [binder, in Huffman.BTree]
t:88 [binder, in Huffman.PBTree]
t:88 [binder, in Huffman.HeightPred]
t:89 [binder, in Huffman.PBTree]
t:9 [binder, in Huffman.HeightPred]
t:9 [binder, in Huffman.Huffman]
t:90 [binder, in Huffman.BTree]
t:91 [binder, in Huffman.BTree]
t:94 [binder, in Huffman.HeightPred]


U

UniqueKey [section, in Huffman.UniqueKey]
UniqueKey [library]
UniqueKey.A [variable, in Huffman.UniqueKey]
UniqueKey.B [variable, in Huffman.UniqueKey]
unique_key_map [lemma, in Huffman.UniqueKey]
unique_key_NoDup [lemma, in Huffman.UniqueKey]
unique_key_app [lemma, in Huffman.UniqueKey]
unique_key_perm [lemma, in Huffman.UniqueKey]
unique_key_in_inv [lemma, in Huffman.UniqueKey]
unique_key_in [lemma, in Huffman.UniqueKey]
unique_key_inv [lemma, in Huffman.UniqueKey]
unique_key_cons [constructor, in Huffman.UniqueKey]
unique_key_nil [constructor, in Huffman.UniqueKey]
unique_key [inductive, in Huffman.UniqueKey]
unique_prefix_permutation [lemma, in Huffman.Code]
unique_prefix_not_null [lemma, in Huffman.Code]
unique_prefix_inv [lemma, in Huffman.Code]
unique_prefix2 [lemma, in Huffman.Code]
unique_prefix1 [lemma, in Huffman.Code]
unique_prefix_nil [lemma, in Huffman.Code]
unique_prefix [definition, in Huffman.Code]


V

v:119 [binder, in Huffman.PBTree]
v:121 [binder, in Huffman.PBTree]
v:123 [binder, in Huffman.PBTree]
v:125 [binder, in Huffman.PBTree]
v:127 [binder, in Huffman.PBTree]
v:129 [binder, in Huffman.PBTree]
v:131 [binder, in Huffman.PBTree]
v:133 [binder, in Huffman.PBTree]
v:135 [binder, in Huffman.PBTree]
v:136 [binder, in Huffman.HeightPred]
v:137 [binder, in Huffman.PBTree]
v:139 [binder, in Huffman.PBTree]
v:141 [binder, in Huffman.PBTree]
v:143 [binder, in Huffman.PBTree]
v:143 [binder, in Huffman.HeightPred]
v:145 [binder, in Huffman.PBTree]
v:147 [binder, in Huffman.PBTree]
v:149 [binder, in Huffman.PBTree]
v:150 [binder, in Huffman.HeightPred]
v:151 [binder, in Huffman.PBTree]
v:153 [binder, in Huffman.PBTree]
v:157 [binder, in Huffman.HeightPred]
v:209 [binder, in Huffman.PBTree]
v:217 [binder, in Huffman.PBTree]
v:225 [binder, in Huffman.PBTree]
v:240 [binder, in Huffman.PBTree]
v:245 [binder, in Huffman.PBTree]
v:37 [binder, in Huffman.Code]
v:52 [binder, in Huffman.PBTree]
v:54 [binder, in Huffman.PBTree]
v:55 [binder, in Huffman.BTree]
v:56 [binder, in Huffman.PBTree]
v:57 [binder, in Huffman.BTree]
v:58 [binder, in Huffman.PBTree]
v:66 [binder, in Huffman.BTree]
v:67 [binder, in Huffman.PBTree]
v:68 [binder, in Huffman.BTree]
v:69 [binder, in Huffman.PBTree]
v:70 [binder, in Huffman.BTree]
v:71 [binder, in Huffman.PBTree]
v:72 [binder, in Huffman.BTree]
v:73 [binder, in Huffman.PBTree]
v:74 [binder, in Huffman.BTree]
v:75 [binder, in Huffman.PBTree]
v:76 [binder, in Huffman.BTree]
v:77 [binder, in Huffman.PBTree]
v:78 [binder, in Huffman.BTree]
v:79 [binder, in Huffman.PBTree]
v:80 [binder, in Huffman.BTree]
v:81 [binder, in Huffman.PBTree]
v:89 [binder, in Huffman.Code]
v:95 [binder, in Huffman.Code]


W

weight [definition, in Huffman.Weight]
Weight [section, in Huffman.Weight]
Weight [library]
WeightTree [section, in Huffman.WeightTree]
WeightTree [library]
WeightTree.A [variable, in Huffman.WeightTree]
WeightTree.f [variable, in Huffman.WeightTree]
weight_tree_compute [lemma, in Huffman.HeightPred]
weight_tree_list_permutation [lemma, in Huffman.WeightTree]
weight_tree_list_node [lemma, in Huffman.WeightTree]
weight_tree_list [definition, in Huffman.WeightTree]
weight_tree [definition, in Huffman.WeightTree]
weight_permutation [lemma, in Huffman.Weight]
Weight.A [variable, in Huffman.Weight]
Weight.A_eq_dec [variable, in Huffman.Weight]


X

x:10 [binder, in Huffman.Huffman]
x:100 [binder, in Huffman.Huffman]
x:101 [binder, in Huffman.Huffman]
x:102 [binder, in Huffman.Huffman]
x:103 [binder, in Huffman.Huffman]
x:104 [binder, in Huffman.Huffman]
x:105 [binder, in Huffman.Huffman]
x:106 [binder, in Huffman.HeightPred]
x:106 [binder, in Huffman.Huffman]
x:107 [binder, in Huffman.Huffman]
x:108 [binder, in Huffman.HeightPred]
x:108 [binder, in Huffman.Huffman]
x:109 [binder, in Huffman.Huffman]
x:11 [binder, in Huffman.Restrict]
x:11 [binder, in Huffman.Huffman]
x:110 [binder, in Huffman.HeightPred]
x:110 [binder, in Huffman.Huffman]
x:111 [binder, in Huffman.Huffman]
x:112 [binder, in Huffman.HeightPred]
x:112 [binder, in Huffman.Huffman]
x:114 [binder, in Huffman.HeightPred]
x:116 [binder, in Huffman.HeightPred]
x:116 [binder, in Huffman.Huffman]
x:117 [binder, in Huffman.Huffman]
x:12 [binder, in Huffman.Restrict]
x:12 [binder, in Huffman.Huffman]
x:120 [binder, in Huffman.Huffman]
x:121 [binder, in Huffman.Huffman]
x:123 [binder, in Huffman.Prod2List]
x:123 [binder, in Huffman.Huffman]
x:124 [binder, in Huffman.Prod2List]
x:124 [binder, in Huffman.Huffman]
x:125 [binder, in Huffman.Prod2List]
x:126 [binder, in Huffman.Prod2List]
x:126 [binder, in Huffman.Huffman]
x:127 [binder, in Huffman.Prod2List]
x:127 [binder, in Huffman.Huffman]
x:128 [binder, in Huffman.Prod2List]
x:128 [binder, in Huffman.Huffman]
x:129 [binder, in Huffman.Huffman]
x:13 [binder, in Huffman.Prod2List]
x:13 [binder, in Huffman.Huffman]
x:130 [binder, in Huffman.Huffman]
x:131 [binder, in Huffman.Huffman]
x:132 [binder, in Huffman.HeightPred]
x:132 [binder, in Huffman.Huffman]
x:133 [binder, in Huffman.HeightPred]
x:133 [binder, in Huffman.Huffman]
x:134 [binder, in Huffman.Huffman]
x:135 [binder, in Huffman.Huffman]
x:136 [binder, in Huffman.Huffman]
x:137 [binder, in Huffman.Huffman]
x:138 [binder, in Huffman.Huffman]
x:139 [binder, in Huffman.HeightPred]
x:139 [binder, in Huffman.Huffman]
x:14 [binder, in Huffman.Huffman]
x:140 [binder, in Huffman.HeightPred]
x:140 [binder, in Huffman.Huffman]
x:141 [binder, in Huffman.Huffman]
x:146 [binder, in Huffman.HeightPred]
x:147 [binder, in Huffman.HeightPred]
x:15 [binder, in Huffman.Huffman]
x:153 [binder, in Huffman.HeightPred]
x:154 [binder, in Huffman.HeightPred]
x:16 [binder, in Huffman.Prod2List]
x:16 [binder, in Huffman.Huffman]
x:160 [binder, in Huffman.HeightPred]
x:161 [binder, in Huffman.HeightPred]
x:17 [binder, in Huffman.WeightTree]
x:17 [binder, in Huffman.Huffman]
x:18 [binder, in Huffman.Huffman]
x:19 [binder, in Huffman.Prod2List]
x:19 [binder, in Huffman.OrderedCover]
x:19 [binder, in Huffman.Huffman]
x:20 [binder, in Huffman.Huffman]
x:21 [binder, in Huffman.Restrict]
x:21 [binder, in Huffman.BTree]
x:21 [binder, in Huffman.OrderedCover]
x:21 [binder, in Huffman.Huffman]
x:22 [binder, in Huffman.Restrict]
x:22 [binder, in Huffman.Prod2List]
x:22 [binder, in Huffman.Huffman]
x:23 [binder, in Huffman.Restrict]
x:23 [binder, in Huffman.OrderedCover]
x:23 [binder, in Huffman.Huffman]
x:24 [binder, in Huffman.Restrict]
x:24 [binder, in Huffman.Huffman]
x:25 [binder, in Huffman.Prod2List]
x:25 [binder, in Huffman.OrderedCover]
x:25 [binder, in Huffman.Huffman]
x:256 [binder, in Huffman.PBTree]
x:259 [binder, in Huffman.PBTree]
x:26 [binder, in Huffman.Huffman]
x:260 [binder, in Huffman.PBTree]
x:27 [binder, in Huffman.OrderedCover]
x:27 [binder, in Huffman.Huffman]
x:28 [binder, in Huffman.Prod2List]
x:28 [binder, in Huffman.Huffman]
x:29 [binder, in Huffman.Prod2List]
x:29 [binder, in Huffman.Huffman]
x:30 [binder, in Huffman.Prod2List]
x:30 [binder, in Huffman.Huffman]
x:31 [binder, in Huffman.AuxLib]
x:31 [binder, in Huffman.Prod2List]
x:31 [binder, in Huffman.Huffman]
x:32 [binder, in Huffman.Huffman]
x:33 [binder, in Huffman.AuxLib]
x:33 [binder, in Huffman.Huffman]
x:34 [binder, in Huffman.PBTree]
x:34 [binder, in Huffman.Huffman]
x:35 [binder, in Huffman.Huffman]
x:36 [binder, in Huffman.Huffman]
x:37 [binder, in Huffman.Ordered]
x:37 [binder, in Huffman.Huffman]
x:39 [binder, in Huffman.Huffman]
x:40 [binder, in Huffman.AuxLib]
x:42 [binder, in Huffman.Prod2List]
x:43 [binder, in Huffman.Huffman]
x:45 [binder, in Huffman.Prod2List]
x:46 [binder, in Huffman.Huffman]
x:47 [binder, in Huffman.Huffman]
x:48 [binder, in Huffman.Prod2List]
x:48 [binder, in Huffman.Weight]
x:51 [binder, in Huffman.Prod2List]
x:52 [binder, in Huffman.Cover]
x:54 [binder, in Huffman.Prod2List]
x:54 [binder, in Huffman.Weight]
x:55 [binder, in Huffman.Weight]
x:57 [binder, in Huffman.Prod2List]
x:6 [binder, in Huffman.WeightTree]
x:62 [binder, in Huffman.Huffman]
x:63 [binder, in Huffman.Huffman]
x:64 [binder, in Huffman.Huffman]
x:67 [binder, in Huffman.Huffman]
x:68 [binder, in Huffman.Huffman]
x:69 [binder, in Huffman.Huffman]
x:70 [binder, in Huffman.Prod2List]
x:70 [binder, in Huffman.Huffman]
x:71 [binder, in Huffman.Huffman]
x:72 [binder, in Huffman.Huffman]
x:73 [binder, in Huffman.Prod2List]
x:73 [binder, in Huffman.Huffman]
x:74 [binder, in Huffman.Huffman]
x:75 [binder, in Huffman.Huffman]
x:76 [binder, in Huffman.Cover]
x:76 [binder, in Huffman.Prod2List]
x:76 [binder, in Huffman.Huffman]
x:77 [binder, in Huffman.Huffman]
x:78 [binder, in Huffman.Huffman]
x:79 [binder, in Huffman.Prod2List]
x:79 [binder, in Huffman.Huffman]
x:8 [binder, in Huffman.WeightTree]
x:80 [binder, in Huffman.Huffman]
x:81 [binder, in Huffman.Huffman]
x:82 [binder, in Huffman.Prod2List]
x:82 [binder, in Huffman.Huffman]
x:83 [binder, in Huffman.Huffman]
x:84 [binder, in Huffman.Huffman]
x:85 [binder, in Huffman.Prod2List]
x:85 [binder, in Huffman.Huffman]
x:86 [binder, in Huffman.Huffman]
x:87 [binder, in Huffman.Huffman]
x:88 [binder, in Huffman.Huffman]
x:89 [binder, in Huffman.Huffman]
x:9 [binder, in Huffman.Restrict]
x:90 [binder, in Huffman.Huffman]
x:91 [binder, in Huffman.Huffman]
x:92 [binder, in Huffman.Huffman]
x:93 [binder, in Huffman.Huffman]
x:94 [binder, in Huffman.Huffman]
x:95 [binder, in Huffman.Huffman]
x:96 [binder, in Huffman.Huffman]
x:98 [binder, in Huffman.Huffman]


Y

y:107 [binder, in Huffman.HeightPred]
y:109 [binder, in Huffman.HeightPred]
y:111 [binder, in Huffman.HeightPred]
y:113 [binder, in Huffman.HeightPred]
y:115 [binder, in Huffman.HeightPred]
y:117 [binder, in Huffman.HeightPred]
y:118 [binder, in Huffman.Huffman]
y:122 [binder, in Huffman.Huffman]
y:125 [binder, in Huffman.Huffman]
y:32 [binder, in Huffman.AuxLib]
y:34 [binder, in Huffman.AuxLib]
y:38 [binder, in Huffman.Ordered]
y:40 [binder, in Huffman.Huffman]
y:41 [binder, in Huffman.AuxLib]
y:43 [binder, in Huffman.Prod2List]
y:46 [binder, in Huffman.Prod2List]
y:49 [binder, in Huffman.Prod2List]
y:52 [binder, in Huffman.Prod2List]
y:53 [binder, in Huffman.Cover]
y:55 [binder, in Huffman.Prod2List]
y:58 [binder, in Huffman.Prod2List]
y:65 [binder, in Huffman.Huffman]
y:7 [binder, in Huffman.WeightTree]
y:71 [binder, in Huffman.Prod2List]
y:74 [binder, in Huffman.Prod2List]
y:77 [binder, in Huffman.Prod2List]
y:80 [binder, in Huffman.Prod2List]
y:83 [binder, in Huffman.Prod2List]
y:86 [binder, in Huffman.Prod2List]
y:9 [binder, in Huffman.WeightTree]


Z

z:44 [binder, in Huffman.Prod2List]
z:47 [binder, in Huffman.Prod2List]
z:50 [binder, in Huffman.Prod2List]
z:53 [binder, in Huffman.Prod2List]
z:56 [binder, in Huffman.Prod2List]
z:59 [binder, in Huffman.Prod2List]
z:72 [binder, in Huffman.Prod2List]
z:75 [binder, in Huffman.Prod2List]
z:78 [binder, in Huffman.Prod2List]
z:81 [binder, in Huffman.Prod2List]
z:84 [binder, in Huffman.Prod2List]
z:87 [binder, in Huffman.Prod2List]


Binder Index

A

a1:113 [in Huffman.PBTree]
a1:116 [in Huffman.PBTree]
a1:137 [in Huffman.HeightPred]
a1:144 [in Huffman.HeightPred]
a1:151 [in Huffman.HeightPred]
a1:155 [in Huffman.PBTree]
a1:158 [in Huffman.HeightPred]
a1:163 [in Huffman.PBTree]
a1:165 [in Huffman.PBTree]
a1:170 [in Huffman.PBTree]
a1:174 [in Huffman.PBTree]
a1:178 [in Huffman.PBTree]
a1:181 [in Huffman.PBTree]
a1:195 [in Huffman.PBTree]
a1:199 [in Huffman.PBTree]
a1:201 [in Huffman.PBTree]
a1:204 [in Huffman.PBTree]
a1:23 [in Huffman.Frequency]
a1:241 [in Huffman.PBTree]
a1:246 [in Huffman.PBTree]
a1:47 [in Huffman.Code]
a1:52 [in Huffman.Code]
a1:84 [in Huffman.PBTree]
a1:86 [in Huffman.BTree]
a2:114 [in Huffman.PBTree]
a2:166 [in Huffman.PBTree]
a2:171 [in Huffman.PBTree]
a2:175 [in Huffman.PBTree]
a2:196 [in Huffman.PBTree]
a2:200 [in Huffman.PBTree]
a2:24 [in Huffman.Frequency]
a2:48 [in Huffman.Code]
a2:53 [in Huffman.Code]
a2:85 [in Huffman.PBTree]
a2:87 [in Huffman.BTree]
a3:167 [in Huffman.PBTree]
a3:172 [in Huffman.PBTree]
a3:176 [in Huffman.PBTree]
a4:168 [in Huffman.PBTree]
a:1 [in Huffman.AuxLib]
a:10 [in Huffman.ISort]
a:10 [in Huffman.Ordered]
a:10 [in Huffman.PBTree]
a:10 [in Huffman.WeightTree]
a:100 [in Huffman.HeightPred]
a:102 [in Huffman.Code]
a:105 [in Huffman.Code]
a:106 [in Huffman.PBTree]
a:109 [in Huffman.Prod2List]
a:11 [in Huffman.AuxLib]
a:11 [in Huffman.UniqueKey]
a:11 [in Huffman.Prod2List]
a:11 [in Huffman.PBTree2BTree]
a:11 [in Huffman.Weight]
a:115 [in Huffman.Code]
a:119 [in Huffman.HeightPred]
a:12 [in Huffman.WeightTree]
a:121 [in Huffman.AuxLib]
a:13 [in Huffman.Restrict]
a:13 [in Huffman.Ordered]
a:13 [in Huffman.Frequency]
a:134 [in Huffman.Code]
a:135 [in Huffman.Code]
a:136 [in Huffman.Code]
a:14 [in Huffman.AuxLib]
a:14 [in Huffman.Prod2List]
a:14 [in Huffman.PBTree2BTree]
A:140 [in Huffman.AuxLib]
a:142 [in Huffman.Code]
a:143 [in Huffman.AuxLib]
a:146 [in Huffman.AuxLib]
a:15 [in Huffman.ISort]
a:15 [in Huffman.UniqueKey]
a:15 [in Huffman.Code]
a:15 [in Huffman.PBTree2BTree]
a:154 [in Huffman.AuxLib]
a:157 [in Huffman.AuxLib]
a:158 [in Huffman.PBTree]
a:16 [in Huffman.Ordered]
a:162 [in Huffman.PBTree]
a:164 [in Huffman.HeightPred]
a:165 [in Huffman.HeightPred]
a:167 [in Huffman.HeightPred]
a:17 [in Huffman.AuxLib]
a:17 [in Huffman.ISort]
a:17 [in Huffman.Prod2List]
a:17 [in Huffman.PBTree2BTree]
a:170 [in Huffman.HeightPred]
a:172 [in Huffman.HeightPred]
a:175 [in Huffman.HeightPred]
a:177 [in Huffman.HeightPred]
a:178 [in Huffman.AuxLib]
a:18 [in Huffman.Ordered]
a:18 [in Huffman.Code]
a:18 [in Huffman.Weight]
a:180 [in Huffman.HeightPred]
a:182 [in Huffman.AuxLib]
a:182 [in Huffman.HeightPred]
a:186 [in Huffman.HeightPred]
a:189 [in Huffman.PBTree]
a:189 [in Huffman.HeightPred]
a:19 [in Huffman.AuxLib]
a:191 [in Huffman.PBTree]
a:192 [in Huffman.HeightPred]
a:194 [in Huffman.HeightPred]
a:196 [in Huffman.HeightPred]
a:198 [in Huffman.HeightPred]
a:2 [in Huffman.Code]
a:2 [in Huffman.PBTree2BTree]
a:2 [in Huffman.BTree]
a:2 [in Huffman.Weight]
a:2 [in Huffman.Frequency]
a:20 [in Huffman.Prod2List]
a:20 [in Huffman.Weight]
a:200 [in Huffman.HeightPred]
a:208 [in Huffman.PBTree]
a:21 [in Huffman.AuxLib]
a:21 [in Huffman.Ordered]
a:21 [in Huffman.Code]
a:211 [in Huffman.PBTree]
a:213 [in Huffman.PBTree]
a:216 [in Huffman.PBTree]
a:219 [in Huffman.PBTree]
a:22 [in Huffman.Weight]
a:221 [in Huffman.PBTree]
a:224 [in Huffman.PBTree]
a:227 [in Huffman.PBTree]
a:229 [in Huffman.PBTree]
a:23 [in Huffman.UniqueKey]
a:23 [in Huffman.Prod2List]
A:23 [in Huffman.WeightTree]
a:232 [in Huffman.PBTree]
a:234 [in Huffman.PBTree]
a:24 [in Huffman.Ordered]
a:250 [in Huffman.PBTree]
a:26 [in Huffman.PBTree]
a:26 [in Huffman.Prod2List]
a:27 [in Huffman.Code]
a:27 [in Huffman.Frequency]
a:28 [in Huffman.Ordered]
a:28 [in Huffman.PBTree]
A:28 [in Huffman.UniqueKey]
a:28 [in Huffman.Code]
a:28 [in Huffman.Weight]
a:29 [in Huffman.BTree]
a:29 [in Huffman.Frequency]
a:3 [in Huffman.Restrict]
a:3 [in Huffman.Ordered]
a:3 [in Huffman.PBTree]
a:3 [in Huffman.HeightPred]
a:3 [in Huffman.Huffman]
a:30 [in Huffman.Cover]
a:30 [in Huffman.Code]
a:31 [in Huffman.Cover]
a:31 [in Huffman.BTree]
A:32 [in Huffman.Ordered]
a:32 [in Huffman.Prod2List]
a:33 [in Huffman.Frequency]
a:34 [in Huffman.UniqueKey]
a:36 [in Huffman.Frequency]
a:37 [in Huffman.BTree]
a:39 [in Huffman.PBTree]
a:39 [in Huffman.BTree]
a:4 [in Huffman.ISort]
a:41 [in Huffman.Huffman]
a:42 [in Huffman.AuxLib]
a:42 [in Huffman.Huffman]
a:42 [in Huffman.Frequency]
a:44 [in Huffman.BTree]
a:44 [in Huffman.Huffman]
a:46 [in Huffman.PBTree]
a:49 [in Huffman.PBTree]
A:49 [in Huffman.Weight]
a:49 [in Huffman.Frequency]
a:5 [in Huffman.UniqueKey]
a:5 [in Huffman.Prod2List]
a:5 [in Huffman.Frequency]
a:50 [in Huffman.AuxLib]
a:51 [in Huffman.BTree]
a:51 [in Huffman.Frequency]
a:52 [in Huffman.BTree]
a:52 [in Huffman.Frequency]
a:56 [in Huffman.Frequency]
a:57 [in Huffman.AuxLib]
a:57 [in Huffman.Weight]
a:58 [in Huffman.Code]
a:59 [in Huffman.Frequency]
a:6 [in Huffman.PBTree2BTree]
a:60 [in Huffman.Prod2List]
a:61 [in Huffman.AuxLib]
a:61 [in Huffman.Code]
a:61 [in Huffman.BTree]
a:62 [in Huffman.PBTree]
a:62 [in Huffman.HeightPred]
a:63 [in Huffman.BTree]
a:63 [in Huffman.Frequency]
a:64 [in Huffman.PBTree]
a:65 [in Huffman.Code]
a:66 [in Huffman.Frequency]
a:67 [in Huffman.HeightPred]
a:67 [in Huffman.Frequency]
a:7 [in Huffman.ISort]
a:7 [in Huffman.Code]
a:70 [in Huffman.AuxLib]
a:70 [in Huffman.Code]
a:71 [in Huffman.AuxLib]
a:71 [in Huffman.Cover]
a:74 [in Huffman.Code]
a:76 [in Huffman.AuxLib]
a:76 [in Huffman.Code]
a:79 [in Huffman.Code]
a:80 [in Huffman.AuxLib]
a:81 [in Huffman.HeightPred]
a:82 [in Huffman.Code]
a:84 [in Huffman.AuxLib]
a:84 [in Huffman.BTree]
a:85 [in Huffman.HeightPred]
a:86 [in Huffman.Code]
a:87 [in Huffman.AuxLib]
a:88 [in Huffman.Prod2List]
a:9 [in Huffman.AuxLib]
a:9 [in Huffman.Ordered]
a:9 [in Huffman.PBTree]
a:9 [in Huffman.UniqueKey]
a:9 [in Huffman.PBTree2BTree]
a:9 [in Huffman.Weight]
a:9 [in Huffman.Frequency]
a:92 [in Huffman.Code]
a:97 [in Huffman.Prod2List]
a:97 [in Huffman.Code]
a:97 [in Huffman.Huffman]
a:99 [in Huffman.Huffman]


B

b1:11 [in Huffman.WeightTree]
b1:112 [in Huffman.Prod2List]
b1:12 [in Huffman.UniqueKey]
b1:13 [in Huffman.WeightTree]
b1:138 [in Huffman.HeightPred]
b1:144 [in Huffman.AuxLib]
b1:145 [in Huffman.HeightPred]
b1:152 [in Huffman.HeightPred]
b1:159 [in Huffman.HeightPred]
b1:242 [in Huffman.PBTree]
b1:247 [in Huffman.PBTree]
b1:25 [in Huffman.Frequency]
b1:27 [in Huffman.Build]
b1:30 [in Huffman.Build]
b1:99 [in Huffman.Prod2List]
b2:13 [in Huffman.UniqueKey]
b2:145 [in Huffman.AuxLib]
b:10 [in Huffman.PBTree2BTree]
b:10 [in Huffman.Weight]
b:100 [in Huffman.PBTree]
b:101 [in Huffman.HeightPred]
b:103 [in Huffman.PBTree]
b:105 [in Huffman.Prod2List]
b:106 [in Huffman.Prod2List]
b:11 [in Huffman.Ordered]
b:110 [in Huffman.Prod2List]
b:119 [in Huffman.Prod2List]
b:12 [in Huffman.AuxLib]
b:12 [in Huffman.Prod2List]
b:12 [in Huffman.PBTree2BTree]
b:12 [in Huffman.Weight]
b:120 [in Huffman.Prod2List]
b:120 [in Huffman.HeightPred]
B:13 [in Huffman.Weight]
b:134 [in Huffman.HeightPred]
b:14 [in Huffman.Ordered]
B:141 [in Huffman.AuxLib]
b:141 [in Huffman.HeightPred]
b:148 [in Huffman.HeightPred]
b:15 [in Huffman.Prod2List]
b:155 [in Huffman.HeightPred]
b:166 [in Huffman.HeightPred]
b:168 [in Huffman.HeightPred]
b:169 [in Huffman.HeightPred]
b:171 [in Huffman.HeightPred]
b:173 [in Huffman.HeightPred]
b:174 [in Huffman.HeightPred]
b:176 [in Huffman.HeightPred]
b:178 [in Huffman.HeightPred]
b:179 [in Huffman.AuxLib]
b:179 [in Huffman.HeightPred]
b:18 [in Huffman.AuxLib]
b:18 [in Huffman.Prod2List]
b:181 [in Huffman.HeightPred]
b:183 [in Huffman.AuxLib]
b:183 [in Huffman.HeightPred]
b:184 [in Huffman.HeightPred]
b:185 [in Huffman.HeightPred]
b:187 [in Huffman.HeightPred]
b:188 [in Huffman.HeightPred]
b:19 [in Huffman.Ordered]
b:19 [in Huffman.Weight]
b:190 [in Huffman.HeightPred]
b:191 [in Huffman.HeightPred]
b:193 [in Huffman.HeightPred]
b:195 [in Huffman.HeightPred]
b:197 [in Huffman.HeightPred]
b:199 [in Huffman.HeightPred]
b:2 [in Huffman.AuxLib]
b:20 [in Huffman.AuxLib]
b:201 [in Huffman.HeightPred]
b:21 [in Huffman.Prod2List]
b:21 [in Huffman.Weight]
b:22 [in Huffman.Ordered]
b:22 [in Huffman.BTree]
b:238 [in Huffman.PBTree]
b:24 [in Huffman.UniqueKey]
b:24 [in Huffman.Prod2List]
b:243 [in Huffman.PBTree]
b:25 [in Huffman.Ordered]
b:27 [in Huffman.PBTree]
b:27 [in Huffman.Prod2List]
b:29 [in Huffman.Ordered]
b:29 [in Huffman.PBTree]
B:29 [in Huffman.UniqueKey]
b:29 [in Huffman.Weight]
b:3 [in Huffman.Code]
b:3 [in Huffman.PBTree2BTree]
b:3 [in Huffman.BTree]
b:3 [in Huffman.Weight]
b:3 [in Huffman.Frequency]
b:30 [in Huffman.BTree]
b:30 [in Huffman.Weight]
b:31 [in Huffman.Code]
b:31 [in Huffman.Weight]
b:32 [in Huffman.Weight]
B:33 [in Huffman.Ordered]
b:33 [in Huffman.Prod2List]
b:35 [in Huffman.UniqueKey]
b:35 [in Huffman.Weight]
b:36 [in Huffman.Code]
b:36 [in Huffman.Weight]
b:37 [in Huffman.Weight]
b:37 [in Huffman.Frequency]
b:38 [in Huffman.Weight]
b:39 [in Huffman.Weight]
b:4 [in Huffman.Restrict]
b:4 [in Huffman.Ordered]
b:4 [in Huffman.PBTree]
b:4 [in Huffman.HeightPred]
b:4 [in Huffman.Huffman]
b:40 [in Huffman.Weight]
b:42 [in Huffman.Code]
b:5 [in Huffman.ISort]
B:5 [in Huffman.Weight]
B:50 [in Huffman.Weight]
b:58 [in Huffman.AuxLib]
b:6 [in Huffman.UniqueKey]
b:6 [in Huffman.Prod2List]
b:61 [in Huffman.Prod2List]
b:62 [in Huffman.Code]
b:67 [in Huffman.AuxLib]
b:68 [in Huffman.AuxLib]
b:71 [in Huffman.Code]
b:72 [in Huffman.Cover]
b:77 [in Huffman.AuxLib]
b:8 [in Huffman.ISort]
b:8 [in Huffman.UniqueKey]
b:81 [in Huffman.AuxLib]
b:88 [in Huffman.Code]
b:89 [in Huffman.Prod2List]
b:92 [in Huffman.PBTree]
b:93 [in Huffman.Code]
b:94 [in Huffman.PBTree]
b:96 [in Huffman.PBTree]
b:98 [in Huffman.PBTree]
b:98 [in Huffman.Prod2List]


C

ca:16 [in Huffman.Code]
ca:31 [in Huffman.Frequency]
cc:54 [in Huffman.Huffman]
cc:59 [in Huffman.Huffman]
c1:113 [in Huffman.Prod2List]
c1:115 [in Huffman.Huffman]
c1:120 [in Huffman.Code]
c1:257 [in Huffman.PBTree]
c1:28 [in Huffman.Build]
c1:31 [in Huffman.Build]
c1:44 [in Huffman.Weight]
c1:63 [in Huffman.Code]
c1:83 [in Huffman.Code]
c2:121 [in Huffman.Code]
c2:258 [in Huffman.PBTree]
c2:45 [in Huffman.Weight]
c2:64 [in Huffman.Code]
c2:84 [in Huffman.Code]
c3:66 [in Huffman.Huffman]
c:10 [in Huffman.Restrict]
c:101 [in Huffman.PBTree]
c:101 [in Huffman.Code]
c:104 [in Huffman.PBTree]
c:104 [in Huffman.Code]
c:107 [in Huffman.Code]
c:108 [in Huffman.Code]
c:11 [in Huffman.Code]
c:111 [in Huffman.Prod2List]
c:114 [in Huffman.Code]
c:114 [in Huffman.Huffman]
c:119 [in Huffman.Huffman]
c:12 [in Huffman.Code]
c:124 [in Huffman.Code]
c:125 [in Huffman.Code]
C:13 [in Huffman.AuxLib]
c:130 [in Huffman.Code]
c:133 [in Huffman.AuxLib]
c:137 [in Huffman.Code]
c:139 [in Huffman.AuxLib]
c:139 [in Huffman.Code]
c:14 [in Huffman.Restrict]
c:14 [in Huffman.Code]
c:143 [in Huffman.Code]
c:146 [in Huffman.Code]
c:16 [in Huffman.Restrict]
c:16 [in Huffman.Weight]
c:17 [in Huffman.Restrict]
c:17 [in Huffman.Code]
c:18 [in Huffman.Restrict]
c:19 [in Huffman.Restrict]
c:20 [in Huffman.Restrict]
c:20 [in Huffman.Code]
c:212 [in Huffman.PBTree]
c:214 [in Huffman.PBTree]
c:220 [in Huffman.PBTree]
c:222 [in Huffman.PBTree]
c:228 [in Huffman.PBTree]
c:230 [in Huffman.PBTree]
c:233 [in Huffman.PBTree]
c:248 [in Huffman.PBTree]
c:249 [in Huffman.PBTree]
c:25 [in Huffman.Restrict]
c:25 [in Huffman.UniqueKey]
c:25 [in Huffman.Code]
c:251 [in Huffman.PBTree]
c:253 [in Huffman.PBTree]
c:255 [in Huffman.PBTree]
c:26 [in Huffman.Code]
c:27 [in Huffman.Weight]
C:30 [in Huffman.UniqueKey]
c:34 [in Huffman.Prod2List]
c:42 [in Huffman.Weight]
c:45 [in Huffman.Huffman]
c:47 [in Huffman.Weight]
c:5 [in Huffman.Ordered]
c:51 [in Huffman.Code]
c:53 [in Huffman.Weight]
c:56 [in Huffman.Code]
c:57 [in Huffman.Code]
c:58 [in Huffman.Weight]
c:6 [in Huffman.Code]
c:60 [in Huffman.Code]
c:61 [in Huffman.Weight]
c:62 [in Huffman.Prod2List]
c:63 [in Huffman.Weight]
c:69 [in Huffman.Code]
c:7 [in Huffman.Weight]
c:73 [in Huffman.AuxLib]
c:73 [in Huffman.Code]
c:8 [in Huffman.Restrict]
c:8 [in Huffman.Huffman]
c:90 [in Huffman.Prod2List]


D

D:31 [in Huffman.UniqueKey]
d:35 [in Huffman.Prod2List]
d:63 [in Huffman.Prod2List]


F

f1:10 [in Huffman.AuxLib]
f:142 [in Huffman.AuxLib]
f:17 [in Huffman.Weight]
f:24 [in Huffman.WeightTree]
f:33 [in Huffman.UniqueKey]
f:75 [in Huffman.AuxLib]
f:79 [in Huffman.AuxLib]
f:8 [in Huffman.Weight]


G

g:35 [in Huffman.Ordered]


H

head:126 [in Huffman.Code]
head:133 [in Huffman.Code]
huffman_aux_rec:50 [in Huffman.Huffman]


K

k:16 [in Huffman.AuxLib]


L

lb1:49 [in Huffman.Code]
lb1:54 [in Huffman.Code]
lb1:86 [in Huffman.PBTree]
lb1:88 [in Huffman.BTree]
lb2:50 [in Huffman.Code]
lb2:55 [in Huffman.Code]
lb2:87 [in Huffman.PBTree]
lb2:89 [in Huffman.BTree]
lin:56 [in Huffman.Huffman]
lin:61 [in Huffman.Huffman]
ln1:11 [in Huffman.HeightPred]
ln1:121 [in Huffman.HeightPred]
ln1:60 [in Huffman.HeightPred]
ln1:68 [in Huffman.HeightPred]
ln1:79 [in Huffman.HeightPred]
ln1:86 [in Huffman.HeightPred]
ln1:98 [in Huffman.HeightPred]
ln2:12 [in Huffman.HeightPred]
ln2:122 [in Huffman.HeightPred]
ln2:61 [in Huffman.HeightPred]
ln2:69 [in Huffman.HeightPred]
ln2:80 [in Huffman.HeightPred]
ln2:87 [in Huffman.HeightPred]
ln2:99 [in Huffman.HeightPred]
ln3:65 [in Huffman.HeightPred]
ln3:74 [in Huffman.HeightPred]
ln:18 [in Huffman.HeightPred]
ln:22 [in Huffman.HeightPred]
ln:26 [in Huffman.HeightPred]
ln:30 [in Huffman.HeightPred]
ln:34 [in Huffman.HeightPred]
ln:35 [in Huffman.SubstPred]
ln:40 [in Huffman.HeightPred]
ln:43 [in Huffman.HeightPred]
ln:48 [in Huffman.HeightPred]
ln:52 [in Huffman.HeightPred]
ln:57 [in Huffman.HeightPred]
ln:76 [in Huffman.HeightPred]
ln:93 [in Huffman.HeightPred]
l1:100 [in Huffman.Prod2List]
l1:101 [in Huffman.AuxLib]
l1:107 [in Huffman.AuxLib]
l1:11 [in Huffman.Build]
l1:11 [in Huffman.OneStep]
l1:110 [in Huffman.AuxLib]
l1:112 [in Huffman.Code]
l1:113 [in Huffman.AuxLib]
l1:114 [in Huffman.Prod2List]
l1:115 [in Huffman.AuxLib]
l1:115 [in Huffman.PBTree]
l1:116 [in Huffman.Code]
l1:117 [in Huffman.PBTree]
l1:118 [in Huffman.AuxLib]
l1:12 [in Huffman.Cover]
l1:12 [in Huffman.SubstPred]
l1:122 [in Huffman.AuxLib]
l1:126 [in Huffman.HeightPred]
l1:13 [in Huffman.OrderedCover]
l1:14 [in Huffman.OneStep]
l1:14 [in Huffman.Weight]
l1:147 [in Huffman.AuxLib]
l1:15 [in Huffman.HeightPred]
l1:155 [in Huffman.AuxLib]
l1:157 [in Huffman.PBTree]
l1:158 [in Huffman.AuxLib]
l1:159 [in Huffman.PBTree]
l1:16 [in Huffman.Cover]
l1:16 [in Huffman.UniqueKey]
l1:16 [in Huffman.OrderedCover]
l1:164 [in Huffman.PBTree]
l1:169 [in Huffman.AuxLib]
l1:171 [in Huffman.AuxLib]
l1:174 [in Huffman.AuxLib]
l1:176 [in Huffman.AuxLib]
l1:179 [in Huffman.PBTree]
l1:18 [in Huffman.Build]
l1:180 [in Huffman.AuxLib]
l1:182 [in Huffman.PBTree]
l1:184 [in Huffman.AuxLib]
l1:19 [in Huffman.UniqueKey]
l1:194 [in Huffman.PBTree]
l1:20 [in Huffman.SubstPred]
l1:202 [in Huffman.PBTree]
l1:205 [in Huffman.PBTree]
l1:21 [in Huffman.UniqueKey]
l1:21 [in Huffman.WeightTree]
l1:23 [in Huffman.Weight]
l1:235 [in Huffman.PBTree]
l1:24 [in Huffman.SubstPred]
l1:25 [in Huffman.WeightTree]
l1:26 [in Huffman.Ordered]
l1:28 [in Huffman.AuxLib]
l1:28 [in Huffman.SubstPred]
l1:3 [in Huffman.Prod2List]
l1:3 [in Huffman.OneStep]
l1:3 [in Huffman.SameSumLeaves]
l1:30 [in Huffman.Ordered]
l1:31 [in Huffman.SubstPred]
l1:33 [in Huffman.Code]
l1:36 [in Huffman.AuxLib]
l1:36 [in Huffman.Prod2List]
l1:37 [in Huffman.SubstPred]
l1:39 [in Huffman.Cover]
l1:43 [in Huffman.Code]
l1:44 [in Huffman.AuxLib]
l1:44 [in Huffman.Cover]
l1:46 [in Huffman.AuxLib]
l1:48 [in Huffman.Cover]
l1:48 [in Huffman.Huffman]
l1:53 [in Huffman.AuxLib]
l1:58 [in Huffman.Cover]
l1:6 [in Huffman.Cover]
l1:6 [in Huffman.SubstPred]
l1:61 [in Huffman.Frequency]
l1:62 [in Huffman.AuxLib]
l1:64 [in Huffman.Prod2List]
l1:64 [in Huffman.Frequency]
l1:7 [in Huffman.Prod2List]
l1:7 [in Huffman.Build]
l1:7 [in Huffman.SameSumLeaves]
l1:8 [in Huffman.CoverMin]
l1:8 [in Huffman.OneStep]
l1:8 [in Huffman.OrderedCover]
l1:80 [in Huffman.Code]
l1:82 [in Huffman.AuxLib]
l1:85 [in Huffman.AuxLib]
l1:88 [in Huffman.AuxLib]
l1:90 [in Huffman.AuxLib]
l1:91 [in Huffman.Prod2List]
l1:96 [in Huffman.AuxLib]
l1:96 [in Huffman.HeightPred]
l2:101 [in Huffman.Prod2List]
l2:102 [in Huffman.AuxLib]
l2:108 [in Huffman.AuxLib]
l2:111 [in Huffman.AuxLib]
l2:113 [in Huffman.Code]
l2:115 [in Huffman.Prod2List]
l2:116 [in Huffman.AuxLib]
l2:118 [in Huffman.PBTree]
l2:119 [in Huffman.AuxLib]
l2:12 [in Huffman.Build]
l2:12 [in Huffman.OneStep]
l2:123 [in Huffman.AuxLib]
l2:127 [in Huffman.HeightPred]
l2:13 [in Huffman.Cover]
l2:13 [in Huffman.SubstPred]
l2:148 [in Huffman.AuxLib]
l2:15 [in Huffman.OneStep]
l2:15 [in Huffman.Weight]
l2:15 [in Huffman.OrderedCover]
l2:156 [in Huffman.AuxLib]
l2:159 [in Huffman.AuxLib]
l2:16 [in Huffman.HeightPred]
l2:160 [in Huffman.PBTree]
l2:17 [in Huffman.UniqueKey]
l2:17 [in Huffman.OrderedCover]
l2:170 [in Huffman.AuxLib]
l2:172 [in Huffman.AuxLib]
l2:175 [in Huffman.AuxLib]
l2:177 [in Huffman.AuxLib]
l2:181 [in Huffman.AuxLib]
l2:185 [in Huffman.AuxLib]
l2:19 [in Huffman.Build]
l2:20 [in Huffman.UniqueKey]
l2:21 [in Huffman.SubstPred]
l2:22 [in Huffman.UniqueKey]
l2:22 [in Huffman.WeightTree]
l2:236 [in Huffman.PBTree]
l2:25 [in Huffman.SubstPred]
l2:26 [in Huffman.WeightTree]
l2:27 [in Huffman.Ordered]
l2:29 [in Huffman.AuxLib]
l2:29 [in Huffman.SubstPred]
l2:31 [in Huffman.Ordered]
l2:32 [in Huffman.SubstPred]
l2:33 [in Huffman.Weight]
l2:34 [in Huffman.Code]
l2:34 [in Huffman.Weight]
l2:37 [in Huffman.AuxLib]
l2:37 [in Huffman.Prod2List]
l2:38 [in Huffman.SubstPred]
l2:4 [in Huffman.Prod2List]
l2:4 [in Huffman.OneStep]
l2:4 [in Huffman.SameSumLeaves]
l2:40 [in Huffman.Cover]
l2:44 [in Huffman.Code]
l2:45 [in Huffman.AuxLib]
l2:45 [in Huffman.Cover]
l2:47 [in Huffman.AuxLib]
l2:49 [in Huffman.Cover]
l2:49 [in Huffman.Huffman]
l2:54 [in Huffman.AuxLib]
l2:62 [in Huffman.Frequency]
l2:63 [in Huffman.AuxLib]
l2:65 [in Huffman.Prod2List]
l2:65 [in Huffman.Frequency]
l2:7 [in Huffman.Cover]
l2:7 [in Huffman.SubstPred]
l2:8 [in Huffman.Prod2List]
l2:8 [in Huffman.Build]
l2:8 [in Huffman.SameSumLeaves]
l2:81 [in Huffman.Code]
l2:83 [in Huffman.AuxLib]
l2:86 [in Huffman.AuxLib]
l2:89 [in Huffman.AuxLib]
l2:9 [in Huffman.CoverMin]
l2:9 [in Huffman.OneStep]
l2:9 [in Huffman.OrderedCover]
l2:91 [in Huffman.AuxLib]
l2:92 [in Huffman.Prod2List]
l2:97 [in Huffman.HeightPred]
l2:98 [in Huffman.AuxLib]
l3:10 [in Huffman.OneStep]
l3:10 [in Huffman.OrderedCover]
l3:102 [in Huffman.Prod2List]
l3:103 [in Huffman.AuxLib]
l3:116 [in Huffman.Prod2List]
l3:13 [in Huffman.OneStep]
l3:14 [in Huffman.SubstPred]
l3:16 [in Huffman.OneStep]
l3:161 [in Huffman.PBTree]
l3:20 [in Huffman.OrderedCover]
l3:24 [in Huffman.OrderedCover]
l3:38 [in Huffman.Prod2List]
l3:48 [in Huffman.AuxLib]
l3:5 [in Huffman.OneStep]
l3:5 [in Huffman.SameSumLeaves]
l3:55 [in Huffman.AuxLib]
l3:64 [in Huffman.AuxLib]
l3:66 [in Huffman.Prod2List]
l3:9 [in Huffman.Prod2List]
l3:93 [in Huffman.Prod2List]
l4:10 [in Huffman.Prod2List]
l4:103 [in Huffman.Prod2List]
l4:104 [in Huffman.AuxLib]
l4:117 [in Huffman.Prod2List]
l4:15 [in Huffman.SubstPred]
l4:17 [in Huffman.OneStep]
l4:22 [in Huffman.OrderedCover]
l4:26 [in Huffman.OrderedCover]
l4:29 [in Huffman.Build]
l4:32 [in Huffman.Build]
l4:39 [in Huffman.Prod2List]
l4:49 [in Huffman.AuxLib]
l4:56 [in Huffman.AuxLib]
l4:6 [in Huffman.SameSumLeaves]
l4:65 [in Huffman.AuxLib]
l4:67 [in Huffman.Prod2List]
l4:94 [in Huffman.Prod2List]
l5:104 [in Huffman.Prod2List]
l5:118 [in Huffman.Prod2List]
l5:16 [in Huffman.SubstPred]
l5:40 [in Huffman.Prod2List]
l5:51 [in Huffman.AuxLib]
l5:52 [in Huffman.AuxLib]
l5:59 [in Huffman.AuxLib]
l5:60 [in Huffman.AuxLib]
l5:66 [in Huffman.AuxLib]
l5:68 [in Huffman.Prod2List]
l5:95 [in Huffman.Prod2List]
l6:107 [in Huffman.Prod2List]
l6:121 [in Huffman.Prod2List]
l6:17 [in Huffman.SubstPred]
l6:41 [in Huffman.Prod2List]
l6:69 [in Huffman.Prod2List]
l6:96 [in Huffman.Prod2List]
l7:108 [in Huffman.Prod2List]
l7:122 [in Huffman.Prod2List]
l:10 [in Huffman.CoverMin]
l:10 [in Huffman.UniqueKey]
l:10 [in Huffman.Frequency]
l:102 [in Huffman.PBTree]
l:103 [in Huffman.Code]
l:105 [in Huffman.PBTree]
l:106 [in Huffman.Code]
l:108 [in Huffman.PBTree]
l:11 [in Huffman.ISort]
l:11 [in Huffman.OrderedCover]
l:113 [in Huffman.Huffman]
l:117 [in Huffman.Code]
l:12 [in Huffman.Ordered]
l:120 [in Huffman.AuxLib]
l:128 [in Huffman.AuxLib]
l:132 [in Huffman.AuxLib]
l:134 [in Huffman.AuxLib]
l:135 [in Huffman.HeightPred]
l:138 [in Huffman.AuxLib]
l:14 [in Huffman.ISort]
l:14 [in Huffman.UniqueKey]
l:14 [in Huffman.Frequency]
l:142 [in Huffman.HeightPred]
l:149 [in Huffman.HeightPred]
l:15 [in Huffman.AuxLib]
l:15 [in Huffman.Ordered]
l:15 [in Huffman.Build]
l:150 [in Huffman.AuxLib]
l:156 [in Huffman.PBTree]
l:156 [in Huffman.HeightPred]
L:16 [in Huffman.ISort]
l:162 [in Huffman.AuxLib]
l:167 [in Huffman.AuxLib]
l:169 [in Huffman.PBTree]
l:17 [in Huffman.Cover]
l:17 [in Huffman.Ordered]
l:173 [in Huffman.PBTree]
l:177 [in Huffman.PBTree]
l:18 [in Huffman.ISort]
l:18 [in Huffman.UniqueKey]
l:19 [in Huffman.Cover]
l:19 [in Huffman.Code]
l:197 [in Huffman.PBTree]
l:198 [in Huffman.PBTree]
l:20 [in Huffman.Ordered]
l:20 [in Huffman.HeightPred]
l:20 [in Huffman.WeightTree]
l:206 [in Huffman.PBTree]
l:207 [in Huffman.PBTree]
l:21 [in Huffman.Cover]
l:21 [in Huffman.ISort]
l:21 [in Huffman.Build]
l:215 [in Huffman.PBTree]
l:22 [in Huffman.AuxLib]
l:22 [in Huffman.ISort]
l:22 [in Huffman.Code]
l:223 [in Huffman.PBTree]
l:23 [in Huffman.Ordered]
l:23 [in Huffman.Build]
l:23 [in Huffman.Code]
l:231 [in Huffman.PBTree]
l:239 [in Huffman.PBTree]
l:24 [in Huffman.HeightPred]
l:24 [in Huffman.Weight]
l:244 [in Huffman.PBTree]
l:25 [in Huffman.Cover]
l:25 [in Huffman.Build]
l:252 [in Huffman.PBTree]
l:26 [in Huffman.UniqueKey]
l:26 [in Huffman.Frequency]
l:27 [in Huffman.UniqueKey]
l:28 [in Huffman.HeightPred]
l:28 [in Huffman.Frequency]
l:29 [in Huffman.Cover]
l:29 [in Huffman.Code]
l:3 [in Huffman.CoverMin]
l:30 [in Huffman.AuxLib]
l:30 [in Huffman.Frequency]
l:32 [in Huffman.Cover]
l:32 [in Huffman.UniqueKey]
l:32 [in Huffman.HeightPred]
l:32 [in Huffman.Code]
l:33 [in Huffman.Build]
l:35 [in Huffman.Code]
l:36 [in Huffman.Ordered]
l:36 [in Huffman.HeightPred]
l:38 [in Huffman.Cover]
l:38 [in Huffman.Huffman]
l:39 [in Huffman.AuxLib]
l:39 [in Huffman.HeightPred]
l:39 [in Huffman.Frequency]
l:41 [in Huffman.Code]
l:43 [in Huffman.AuxLib]
l:43 [in Huffman.Cover]
l:45 [in Huffman.HeightPred]
l:45 [in Huffman.Code]
l:45 [in Huffman.Frequency]
l:46 [in Huffman.Code]
l:47 [in Huffman.Frequency]
l:48 [in Huffman.Frequency]
l:5 [in Huffman.OrderedCover]
l:50 [in Huffman.HeightPred]
l:50 [in Huffman.Frequency]
l:51 [in Huffman.Cover]
l:51 [in Huffman.Weight]
l:53 [in Huffman.Frequency]
l:54 [in Huffman.Cover]
l:54 [in Huffman.HeightPred]
l:57 [in Huffman.Frequency]
l:59 [in Huffman.HeightPred]
l:59 [in Huffman.Code]
l:6 [in Huffman.Weight]
l:60 [in Huffman.Cover]
l:62 [in Huffman.Cover]
l:62 [in Huffman.BTree]
l:63 [in Huffman.PBTree]
l:64 [in Huffman.Cover]
l:65 [in Huffman.BTree]
l:66 [in Huffman.PBTree]
l:66 [in Huffman.Code]
l:67 [in Huffman.Cover]
l:69 [in Huffman.AuxLib]
l:69 [in Huffman.Cover]
l:7 [in Huffman.UniqueKey]
l:71 [in Huffman.HeightPred]
l:72 [in Huffman.AuxLib]
l:72 [in Huffman.Code]
l:73 [in Huffman.Cover]
l:74 [in Huffman.AuxLib]
l:75 [in Huffman.Code]
l:77 [in Huffman.Code]
l:78 [in Huffman.AuxLib]
l:78 [in Huffman.HeightPred]
l:8 [in Huffman.AuxLib]
l:8 [in Huffman.Code]
l:87 [in Huffman.Code]
l:89 [in Huffman.HeightPred]
l:9 [in Huffman.Build]
l:93 [in Huffman.PBTree]
l:94 [in Huffman.Code]
l:95 [in Huffman.PBTree]
l:95 [in Huffman.HeightPred]
l:97 [in Huffman.PBTree]
l:98 [in Huffman.Code]
l:99 [in Huffman.PBTree]


M

m1:118 [in Huffman.Code]
m1:122 [in Huffman.Code]
m1:131 [in Huffman.Code]
m1:140 [in Huffman.Code]
m1:15 [in Huffman.Restrict]
m1:60 [in Huffman.Weight]
m1:60 [in Huffman.Frequency]
m1:9 [in Huffman.Code]
m2:10 [in Huffman.Code]
m2:123 [in Huffman.Code]
m2:132 [in Huffman.Code]
m2:141 [in Huffman.Code]
m:109 [in Huffman.Code]
m:119 [in Huffman.Code]
m:127 [in Huffman.Code]
m:13 [in Huffman.Code]
m:138 [in Huffman.Code]
m:144 [in Huffman.Code]
m:145 [in Huffman.Code]
m:162 [in Huffman.HeightPred]
m:24 [in Huffman.Code]
m:26 [in Huffman.Weight]
m:32 [in Huffman.Frequency]
m:35 [in Huffman.Frequency]
m:41 [in Huffman.Weight]
m:43 [in Huffman.Weight]
m:44 [in Huffman.Frequency]
m:46 [in Huffman.Weight]
m:5 [in Huffman.Code]
m:52 [in Huffman.Weight]
m:56 [in Huffman.Weight]
m:58 [in Huffman.Frequency]
m:59 [in Huffman.Weight]
m:62 [in Huffman.Weight]
m:68 [in Huffman.Frequency]
m:7 [in Huffman.Restrict]
m:82 [in Huffman.BTree]


N

nnil:52 [in Huffman.Huffman]
nnil:57 [in Huffman.Huffman]
n1:104 [in Huffman.HeightPred]
n1:105 [in Huffman.HeightPred]
n1:124 [in Huffman.AuxLib]
n1:125 [in Huffman.AuxLib]
n1:128 [in Huffman.HeightPred]
n1:129 [in Huffman.HeightPred]
n1:42 [in Huffman.HeightPred]
n1:47 [in Huffman.HeightPred]
n1:55 [in Huffman.HeightPred]
n1:63 [in Huffman.HeightPred]
n1:64 [in Huffman.HeightPred]
n1:72 [in Huffman.HeightPred]
n1:73 [in Huffman.HeightPred]
n1:82 [in Huffman.HeightPred]
n1:83 [in Huffman.HeightPred]
n1:90 [in Huffman.HeightPred]
n1:91 [in Huffman.HeightPred]
n2:131 [in Huffman.AuxLib]
n2:137 [in Huffman.AuxLib]
n:10 [in Huffman.HeightPred]
n:106 [in Huffman.AuxLib]
n:109 [in Huffman.AuxLib]
n:112 [in Huffman.AuxLib]
n:114 [in Huffman.AuxLib]
n:117 [in Huffman.AuxLib]
n:118 [in Huffman.HeightPred]
n:130 [in Huffman.HeightPred]
n:163 [in Huffman.AuxLib]
n:168 [in Huffman.AuxLib]
n:17 [in Huffman.HeightPred]
n:173 [in Huffman.AuxLib]
n:21 [in Huffman.HeightPred]
n:25 [in Huffman.HeightPred]
n:25 [in Huffman.Weight]
n:29 [in Huffman.HeightPred]
n:33 [in Huffman.HeightPred]
n:34 [in Huffman.Frequency]
n:34 [in Huffman.SubstPred]
n:37 [in Huffman.HeightPred]
n:38 [in Huffman.Frequency]
n:41 [in Huffman.HeightPred]
n:43 [in Huffman.Frequency]
n:46 [in Huffman.HeightPred]
n:51 [in Huffman.HeightPred]
n:55 [in Huffman.Cover]
n:56 [in Huffman.HeightPred]
n:6 [in Huffman.Frequency]
n:61 [in Huffman.Cover]
n:66 [in Huffman.Cover]
n:66 [in Huffman.HeightPred]
n:75 [in Huffman.HeightPred]
n:8 [in Huffman.HeightPred]
n:84 [in Huffman.HeightPred]
n:92 [in Huffman.HeightPred]


O

order:34 [in Huffman.Ordered]
ord:53 [in Huffman.Huffman]
ord:58 [in Huffman.Huffman]


P

p:15 [in Huffman.Frequency]
p:153 [in Huffman.AuxLib]
p:16 [in Huffman.Frequency]
p:160 [in Huffman.AuxLib]
p:161 [in Huffman.AuxLib]
p:166 [in Huffman.AuxLib]
p:17 [in Huffman.Frequency]
p:18 [in Huffman.Frequency]
p:19 [in Huffman.Frequency]
p:20 [in Huffman.Frequency]
p:21 [in Huffman.Frequency]
p:22 [in Huffman.Frequency]
P:27 [in Huffman.AuxLib]
p:32 [in Huffman.BTree]
P:35 [in Huffman.AuxLib]
p:46 [in Huffman.Frequency]
p:60 [in Huffman.PBTree]
p:64 [in Huffman.BTree]
p:65 [in Huffman.PBTree]
p:78 [in Huffman.Code]
p:8 [in Huffman.PBTree]
p:85 [in Huffman.Code]
p:91 [in Huffman.Code]


R

rec:38 [in Huffman.AuxLib]


S

sl:55 [in Huffman.Huffman]
sl:60 [in Huffman.Huffman]


T

t0:36 [in Huffman.PBTree]
t0:41 [in Huffman.BTree]
t1:102 [in Huffman.HeightPred]
t1:12 [in Huffman.BTree]
t1:124 [in Huffman.HeightPred]
t1:13 [in Huffman.HeightPred]
t1:13 [in Huffman.Build]
t1:14 [in Huffman.Cover]
t1:15 [in Huffman.PBTree]
t1:15 [in Huffman.BTree]
t1:16 [in Huffman.Build]
t1:17 [in Huffman.BTree]
t1:18 [in Huffman.PBTree]
t1:18 [in Huffman.WeightTree]
t1:18 [in Huffman.SubstPred]
t1:180 [in Huffman.PBTree]
t1:183 [in Huffman.PBTree]
t1:21 [in Huffman.PBTree]
t1:22 [in Huffman.Cover]
t1:22 [in Huffman.SubstPred]
t1:24 [in Huffman.PBTree]
t1:25 [in Huffman.BTree]
t1:26 [in Huffman.Cover]
t1:26 [in Huffman.SubstPred]
t1:27 [in Huffman.BTree]
t1:30 [in Huffman.PBTree]
t1:30 [in Huffman.SubstPred]
t1:33 [in Huffman.Cover]
t1:36 [in Huffman.Cover]
t1:36 [in Huffman.SubstPred]
t1:37 [in Huffman.PBTree]
t1:4 [in Huffman.CoverMin]
t1:4 [in Huffman.SubstPred]
t1:40 [in Huffman.PBTree]
t1:41 [in Huffman.Cover]
t1:42 [in Huffman.PBTree]
t1:42 [in Huffman.BTree]
t1:44 [in Huffman.PBTree]
t1:45 [in Huffman.PBTree]
t1:45 [in Huffman.BTree]
t1:46 [in Huffman.Cover]
t1:47 [in Huffman.BTree]
t1:6 [in Huffman.OneStep]
t1:6 [in Huffman.OrderedCover]
t1:8 [in Huffman.Cover]
t1:8 [in Huffman.SubstPred]
t2:103 [in Huffman.HeightPred]
t2:125 [in Huffman.HeightPred]
t2:13 [in Huffman.BTree]
t2:14 [in Huffman.HeightPred]
t2:14 [in Huffman.Build]
t2:15 [in Huffman.Cover]
t2:16 [in Huffman.PBTree]
t2:16 [in Huffman.BTree]
t2:17 [in Huffman.Build]
t2:18 [in Huffman.BTree]
t2:19 [in Huffman.PBTree]
t2:19 [in Huffman.WeightTree]
t2:19 [in Huffman.SubstPred]
t2:22 [in Huffman.PBTree]
t2:23 [in Huffman.Cover]
t2:23 [in Huffman.SubstPred]
t2:25 [in Huffman.PBTree]
t2:26 [in Huffman.BTree]
t2:27 [in Huffman.Cover]
t2:27 [in Huffman.SubstPred]
t2:28 [in Huffman.BTree]
t2:31 [in Huffman.PBTree]
t2:33 [in Huffman.SubstPred]
t2:34 [in Huffman.Cover]
t2:37 [in Huffman.Cover]
t2:38 [in Huffman.PBTree]
t2:39 [in Huffman.SubstPred]
t2:41 [in Huffman.PBTree]
t2:42 [in Huffman.Cover]
t2:43 [in Huffman.PBTree]
t2:43 [in Huffman.BTree]
t2:46 [in Huffman.BTree]
t2:47 [in Huffman.Cover]
t2:48 [in Huffman.BTree]
t2:5 [in Huffman.CoverMin]
t2:5 [in Huffman.SubstPred]
t2:7 [in Huffman.OneStep]
t2:7 [in Huffman.OrderedCover]
t2:9 [in Huffman.Cover]
t2:9 [in Huffman.SubstPred]
t3:10 [in Huffman.Cover]
t3:10 [in Huffman.SubstPred]
t3:19 [in Huffman.BTree]
t3:24 [in Huffman.Cover]
t3:32 [in Huffman.PBTree]
t4:11 [in Huffman.SubstPred]
t:10 [in Huffman.Build]
t:10 [in Huffman.BTree]
t:107 [in Huffman.PBTree]
t:11 [in Huffman.Cover]
t:11 [in Huffman.CoverMin]
t:11 [in Huffman.BTree]
t:12 [in Huffman.OrderedCover]
t:123 [in Huffman.HeightPred]
t:13 [in Huffman.PBTree]
t:13 [in Huffman.PBTree2BTree]
t:131 [in Huffman.HeightPred]
t:14 [in Huffman.PBTree]
t:14 [in Huffman.WeightTree]
t:14 [in Huffman.BTree]
t:14 [in Huffman.OrderedCover]
t:16 [in Huffman.PBTree2BTree]
t:163 [in Huffman.HeightPred]
t:17 [in Huffman.PBTree]
t:18 [in Huffman.Cover]
t:18 [in Huffman.OrderedCover]
t:184 [in Huffman.PBTree]
t:185 [in Huffman.PBTree]
t:188 [in Huffman.PBTree]
t:19 [in Huffman.HeightPred]
t:190 [in Huffman.PBTree]
t:192 [in Huffman.PBTree]
t:193 [in Huffman.PBTree]
t:20 [in Huffman.Cover]
t:20 [in Huffman.PBTree]
t:20 [in Huffman.Build]
t:20 [in Huffman.BTree]
t:203 [in Huffman.PBTree]
t:22 [in Huffman.Build]
t:23 [in Huffman.PBTree]
t:23 [in Huffman.HeightPred]
t:237 [in Huffman.PBTree]
t:24 [in Huffman.Build]
t:254 [in Huffman.PBTree]
t:26 [in Huffman.Build]
t:27 [in Huffman.HeightPred]
t:28 [in Huffman.Cover]
t:3 [in Huffman.WeightTree]
t:31 [in Huffman.HeightPred]
t:33 [in Huffman.PBTree]
t:33 [in Huffman.BTree]
t:34 [in Huffman.Build]
t:35 [in Huffman.Cover]
t:35 [in Huffman.PBTree]
t:35 [in Huffman.HeightPred]
t:36 [in Huffman.BTree]
t:38 [in Huffman.HeightPred]
t:38 [in Huffman.BTree]
t:4 [in Huffman.OrderedCover]
t:40 [in Huffman.BTree]
t:44 [in Huffman.HeightPred]
t:47 [in Huffman.PBTree]
t:48 [in Huffman.PBTree]
t:49 [in Huffman.HeightPred]
t:49 [in Huffman.BTree]
t:5 [in Huffman.Cover]
t:5 [in Huffman.Build]
t:50 [in Huffman.Cover]
t:50 [in Huffman.BTree]
t:53 [in Huffman.HeightPred]
t:58 [in Huffman.HeightPred]
t:59 [in Huffman.BTree]
t:6 [in Huffman.CoverMin]
t:6 [in Huffman.Build]
t:60 [in Huffman.BTree]
t:61 [in Huffman.PBTree]
t:63 [in Huffman.Cover]
t:65 [in Huffman.Cover]
t:68 [in Huffman.Cover]
t:7 [in Huffman.CoverMin]
t:70 [in Huffman.Cover]
t:70 [in Huffman.HeightPred]
t:74 [in Huffman.Cover]
t:75 [in Huffman.Cover]
t:77 [in Huffman.HeightPred]
t:83 [in Huffman.PBTree]
t:83 [in Huffman.BTree]
t:85 [in Huffman.BTree]
t:88 [in Huffman.PBTree]
t:88 [in Huffman.HeightPred]
t:89 [in Huffman.PBTree]
t:9 [in Huffman.HeightPred]
t:9 [in Huffman.Huffman]
t:90 [in Huffman.BTree]
t:91 [in Huffman.BTree]
t:94 [in Huffman.HeightPred]


V

v:119 [in Huffman.PBTree]
v:121 [in Huffman.PBTree]
v:123 [in Huffman.PBTree]
v:125 [in Huffman.PBTree]
v:127 [in Huffman.PBTree]
v:129 [in Huffman.PBTree]
v:131 [in Huffman.PBTree]
v:133 [in Huffman.PBTree]
v:135 [in Huffman.PBTree]
v:136 [in Huffman.HeightPred]
v:137 [in Huffman.PBTree]
v:139 [in Huffman.PBTree]
v:141 [in Huffman.PBTree]
v:143 [in Huffman.PBTree]
v:143 [in Huffman.HeightPred]
v:145 [in Huffman.PBTree]
v:147 [in Huffman.PBTree]
v:149 [in Huffman.PBTree]
v:150 [in Huffman.HeightPred]
v:151 [in Huffman.PBTree]
v:153 [in Huffman.PBTree]
v:157 [in Huffman.HeightPred]
v:209 [in Huffman.PBTree]
v:217 [in Huffman.PBTree]
v:225 [in Huffman.PBTree]
v:240 [in Huffman.PBTree]
v:245 [in Huffman.PBTree]
v:37 [in Huffman.Code]
v:52 [in Huffman.PBTree]
v:54 [in Huffman.PBTree]
v:55 [in Huffman.BTree]
v:56 [in Huffman.PBTree]
v:57 [in Huffman.BTree]
v:58 [in Huffman.PBTree]
v:66 [in Huffman.BTree]
v:67 [in Huffman.PBTree]
v:68 [in Huffman.BTree]
v:69 [in Huffman.PBTree]
v:70 [in Huffman.BTree]
v:71 [in Huffman.PBTree]
v:72 [in Huffman.BTree]
v:73 [in Huffman.PBTree]
v:74 [in Huffman.BTree]
v:75 [in Huffman.PBTree]
v:76 [in Huffman.BTree]
v:77 [in Huffman.PBTree]
v:78 [in Huffman.BTree]
v:79 [in Huffman.PBTree]
v:80 [in Huffman.BTree]
v:81 [in Huffman.PBTree]
v:89 [in Huffman.Code]
v:95 [in Huffman.Code]


X

x:10 [in Huffman.Huffman]
x:100 [in Huffman.Huffman]
x:101 [in Huffman.Huffman]
x:102 [in Huffman.Huffman]
x:103 [in Huffman.Huffman]
x:104 [in Huffman.Huffman]
x:105 [in Huffman.Huffman]
x:106 [in Huffman.HeightPred]
x:106 [in Huffman.Huffman]
x:107 [in Huffman.Huffman]
x:108 [in Huffman.HeightPred]
x:108 [in Huffman.Huffman]
x:109 [in Huffman.Huffman]
x:11 [in Huffman.Restrict]
x:11 [in Huffman.Huffman]
x:110 [in Huffman.HeightPred]
x:110 [in Huffman.Huffman]
x:111 [in Huffman.Huffman]
x:112 [in Huffman.HeightPred]
x:112 [in Huffman.Huffman]
x:114 [in Huffman.HeightPred]
x:116 [in Huffman.HeightPred]
x:116 [in Huffman.Huffman]
x:117 [in Huffman.Huffman]
x:12 [in Huffman.Restrict]
x:12 [in Huffman.Huffman]
x:120 [in Huffman.Huffman]
x:121 [in Huffman.Huffman]
x:123 [in Huffman.Prod2List]
x:123 [in Huffman.Huffman]
x:124 [in Huffman.Prod2List]
x:124 [in Huffman.Huffman]
x:125 [in Huffman.Prod2List]
x:126 [in Huffman.Prod2List]
x:126 [in Huffman.Huffman]
x:127 [in Huffman.Prod2List]
x:127 [in Huffman.Huffman]
x:128 [in Huffman.Prod2List]
x:128 [in Huffman.Huffman]
x:129 [in Huffman.Huffman]
x:13 [in Huffman.Prod2List]
x:13 [in Huffman.Huffman]
x:130 [in Huffman.Huffman]
x:131 [in Huffman.Huffman]
x:132 [in Huffman.HeightPred]
x:132 [in Huffman.Huffman]
x:133 [in Huffman.HeightPred]
x:133 [in Huffman.Huffman]
x:134 [in Huffman.Huffman]
x:135 [in Huffman.Huffman]
x:136 [in Huffman.Huffman]
x:137 [in Huffman.Huffman]
x:138 [in Huffman.Huffman]
x:139 [in Huffman.HeightPred]
x:139 [in Huffman.Huffman]
x:14 [in Huffman.Huffman]
x:140 [in Huffman.HeightPred]
x:140 [in Huffman.Huffman]
x:141 [in Huffman.Huffman]
x:146 [in Huffman.HeightPred]
x:147 [in Huffman.HeightPred]
x:15 [in Huffman.Huffman]
x:153 [in Huffman.HeightPred]
x:154 [in Huffman.HeightPred]
x:16 [in Huffman.Prod2List]
x:16 [in Huffman.Huffman]
x:160 [in Huffman.HeightPred]
x:161 [in Huffman.HeightPred]
x:17 [in Huffman.WeightTree]
x:17 [in Huffman.Huffman]
x:18 [in Huffman.Huffman]
x:19 [in Huffman.Prod2List]
x:19 [in Huffman.OrderedCover]
x:19 [in Huffman.Huffman]
x:20 [in Huffman.Huffman]
x:21 [in Huffman.Restrict]
x:21 [in Huffman.BTree]
x:21 [in Huffman.OrderedCover]
x:21 [in Huffman.Huffman]
x:22 [in Huffman.Restrict]
x:22 [in Huffman.Prod2List]
x:22 [in Huffman.Huffman]
x:23 [in Huffman.Restrict]
x:23 [in Huffman.OrderedCover]
x:23 [in Huffman.Huffman]
x:24 [in Huffman.Restrict]
x:24 [in Huffman.Huffman]
x:25 [in Huffman.Prod2List]
x:25 [in Huffman.OrderedCover]
x:25 [in Huffman.Huffman]
x:256 [in Huffman.PBTree]
x:259 [in Huffman.PBTree]
x:26 [in Huffman.Huffman]
x:260 [in Huffman.PBTree]
x:27 [in Huffman.OrderedCover]
x:27 [in Huffman.Huffman]
x:28 [in Huffman.Prod2List]
x:28 [in Huffman.Huffman]
x:29 [in Huffman.Prod2List]
x:29 [in Huffman.Huffman]
x:30 [in Huffman.Prod2List]
x:30 [in Huffman.Huffman]
x:31 [in Huffman.AuxLib]
x:31 [in Huffman.Prod2List]
x:31 [in Huffman.Huffman]
x:32 [in Huffman.Huffman]
x:33 [in Huffman.AuxLib]
x:33 [in Huffman.Huffman]
x:34 [in Huffman.PBTree]
x:34 [in Huffman.Huffman]
x:35 [in Huffman.Huffman]
x:36 [in Huffman.Huffman]
x:37 [in Huffman.Ordered]
x:37 [in Huffman.Huffman]
x:39 [in Huffman.Huffman]
x:40 [in Huffman.AuxLib]
x:42 [in Huffman.Prod2List]
x:43 [in Huffman.Huffman]
x:45 [in Huffman.Prod2List]
x:46 [in Huffman.Huffman]
x:47 [in Huffman.Huffman]
x:48 [in Huffman.Prod2List]
x:48 [in Huffman.Weight]
x:51 [in Huffman.Prod2List]
x:52 [in Huffman.Cover]
x:54 [in Huffman.Prod2List]
x:54 [in Huffman.Weight]
x:55 [in Huffman.Weight]
x:57 [in Huffman.Prod2List]
x:6 [in Huffman.WeightTree]
x:62 [in Huffman.Huffman]
x:63 [in Huffman.Huffman]
x:64 [in Huffman.Huffman]
x:67 [in Huffman.Huffman]
x:68 [in Huffman.Huffman]
x:69 [in Huffman.Huffman]
x:70 [in Huffman.Prod2List]
x:70 [in Huffman.Huffman]
x:71 [in Huffman.Huffman]
x:72 [in Huffman.Huffman]
x:73 [in Huffman.Prod2List]
x:73 [in Huffman.Huffman]
x:74 [in Huffman.Huffman]
x:75 [in Huffman.Huffman]
x:76 [in Huffman.Cover]
x:76 [in Huffman.Prod2List]
x:76 [in Huffman.Huffman]
x:77 [in Huffman.Huffman]
x:78 [in Huffman.Huffman]
x:79 [in Huffman.Prod2List]
x:79 [in Huffman.Huffman]
x:8 [in Huffman.WeightTree]
x:80 [in Huffman.Huffman]
x:81 [in Huffman.Huffman]
x:82 [in Huffman.Prod2List]
x:82 [in Huffman.Huffman]
x:83 [in Huffman.Huffman]
x:84 [in Huffman.Huffman]
x:85 [in Huffman.Prod2List]
x:85 [in Huffman.Huffman]
x:86 [in Huffman.Huffman]
x:87 [in Huffman.Huffman]
x:88 [in Huffman.Huffman]
x:89 [in Huffman.Huffman]
x:9 [in Huffman.Restrict]
x:90 [in Huffman.Huffman]
x:91 [in Huffman.Huffman]
x:92 [in Huffman.Huffman]
x:93 [in Huffman.Huffman]
x:94 [in Huffman.Huffman]
x:95 [in Huffman.Huffman]
x:96 [in Huffman.Huffman]
x:98 [in Huffman.Huffman]


Y

y:107 [in Huffman.HeightPred]
y:109 [in Huffman.HeightPred]
y:111 [in Huffman.HeightPred]
y:113 [in Huffman.HeightPred]
y:115 [in Huffman.HeightPred]
y:117 [in Huffman.HeightPred]
y:118 [in Huffman.Huffman]
y:122 [in Huffman.Huffman]
y:125 [in Huffman.Huffman]
y:32 [in Huffman.AuxLib]
y:34 [in Huffman.AuxLib]
y:38 [in Huffman.Ordered]
y:40 [in Huffman.Huffman]
y:41 [in Huffman.AuxLib]
y:43 [in Huffman.Prod2List]
y:46 [in Huffman.Prod2List]
y:49 [in Huffman.Prod2List]
y:52 [in Huffman.Prod2List]
y:53 [in Huffman.Cover]
y:55 [in Huffman.Prod2List]
y:58 [in Huffman.Prod2List]
y:65 [in Huffman.Huffman]
y:7 [in Huffman.WeightTree]
y:71 [in Huffman.Prod2List]
y:74 [in Huffman.Prod2List]
y:77 [in Huffman.Prod2List]
y:80 [in Huffman.Prod2List]
y:83 [in Huffman.Prod2List]
y:86 [in Huffman.Prod2List]
y:9 [in Huffman.WeightTree]


Z

z:44 [in Huffman.Prod2List]
z:47 [in Huffman.Prod2List]
z:50 [in Huffman.Prod2List]
z:53 [in Huffman.Prod2List]
z:56 [in Huffman.Prod2List]
z:59 [in Huffman.Prod2List]
z:72 [in Huffman.Prod2List]
z:75 [in Huffman.Prod2List]
z:78 [in Huffman.Prod2List]
z:81 [in Huffman.Prod2List]
z:84 [in Huffman.Prod2List]
z:87 [in Huffman.Prod2List]


Variable Index

B

Build.A [in Huffman.Build]
Build.f [in Huffman.Build]


C

Code.A [in Huffman.Code]
Code.A_eq_dec [in Huffman.Code]
CoverMin.A [in Huffman.CoverMin]
CoverMin.f [in Huffman.CoverMin]
Cover.A [in Huffman.Cover]
Cover.empty [in Huffman.Cover]


F

FindMin.A [in Huffman.AuxLib]
FindMin.f [in Huffman.AuxLib]
First.A [in Huffman.AuxLib]
Fold.A [in Huffman.AuxLib]
Fold.B [in Huffman.AuxLib]
Fold.f [in Huffman.AuxLib]
Fold.g [in Huffman.AuxLib]
Fold.h [in Huffman.AuxLib]
Frequency.A [in Huffman.Frequency]
Frequency.A_eq_dec [in Huffman.Frequency]


H

HeightPred.A [in Huffman.HeightPred]
HeightPred.A_eq_dec [in Huffman.HeightPred]
HeightPred.f [in Huffman.HeightPred]
Huffman.A [in Huffman.Huffman]
Huffman.A_eq_dec [in Huffman.Huffman]
Huffman.empty [in Huffman.Huffman]
Huffman.frequency_more_than_one [in Huffman.Huffman]
Huffman.m [in Huffman.Huffman]


I

ISortExample.A [in Huffman.ISort]
ISortExample.order [in Huffman.ISort]
ISortExample.order_fun_false [in Huffman.ISort]
ISortExample.order_fun_true [in Huffman.ISort]
ISortExample.order_fun [in Huffman.ISort]


L

List.A [in Huffman.AuxLib]
List.B [in Huffman.AuxLib]
List.C [in Huffman.AuxLib]
List.f [in Huffman.AuxLib]


M

map2.A [in Huffman.AuxLib]
map2.B [in Huffman.AuxLib]
map2.C [in Huffman.AuxLib]
map2.f [in Huffman.AuxLib]


O

OneStep.A [in Huffman.OneStep]
OneStep.f [in Huffman.OneStep]
OrderedCover.A [in Huffman.OrderedCover]
ordered.A [in Huffman.Ordered]
ordered.order [in Huffman.Ordered]
ordered.order_trans [in Huffman.Ordered]


P

PBTree.A [in Huffman.PBTree]
PBTree.A_eq_dec [in Huffman.PBTree]
PBTree.empty [in Huffman.PBTree]
PBTREE2BTREE.A [in Huffman.PBTree2BTree]
PBTREE2BTREE.A_eq_dec [in Huffman.PBTree2BTree]
PBTREE2BTREE.empty [in Huffman.PBTree2BTree]
Permutation.A [in Huffman.AuxLib]
Prod2List.A [in Huffman.Prod2List]
Prod2List.f [in Huffman.Prod2List]


R

Restrict.A [in Huffman.Restrict]
Restrict.A_eq_dec [in Huffman.Restrict]
Restrict.empty [in Huffman.Restrict]
Restrict.m [in Huffman.Restrict]


S

SameSumLeaves.A [in Huffman.SameSumLeaves]
SameSumLeaves.f [in Huffman.SameSumLeaves]
SubstPred.A [in Huffman.SubstPred]


T

Tree.A [in Huffman.BTree]
Tree.A_eq_dec [in Huffman.BTree]
Tree.empty [in Huffman.BTree]


U

UniqueKey.A [in Huffman.UniqueKey]
UniqueKey.B [in Huffman.UniqueKey]


W

WeightTree.A [in Huffman.WeightTree]
WeightTree.f [in Huffman.WeightTree]
Weight.A [in Huffman.Weight]
Weight.A_eq_dec [in Huffman.Weight]


Library Index

A

AuxLib


B

BTree
Build


C

Code
Cover
CoverMin


E

Extraction


F

Frequency


H

HeightPred
Huffman


I

ISort


O

OneStep
Ordered
OrderedCover


P

PBTree
PBTree2BTree
Prod2List


R

Restrict


S

SameSumLeaves
SubstPred


U

UniqueKey


W

Weight
WeightTree


Lemma Index

A

add_frequency_list_not_in [in Huffman.Frequency]
add_frequency_list_in [in Huffman.Frequency]
add_frequency_list_1 [in Huffman.Frequency]
add_frequency_list_unique_key [in Huffman.Frequency]
add_frequency_list_in_inv [in Huffman.Frequency]
add_frequency_list_perm [in Huffman.Frequency]
all_permutations_permutation [in Huffman.AuxLib]
all_permutations_aux_permutation [in Huffman.AuxLib]
all_cover_cover [in Huffman.Cover]
all_cover_aux_cover [in Huffman.Cover]
all_pbleaves_pbbuild [in Huffman.PBTree]
all_pbleaves_compute_pb [in Huffman.PBTree]
all_pbleaves_pbleaf [in Huffman.PBTree]
all_pbleaves_pbadd [in Huffman.PBTree]
all_pbleaves_NoDup [in Huffman.PBTree]
all_pbleaves_unique [in Huffman.PBTree]
all_pbleaves_inpb [in Huffman.PBTree]
all_pbleaves_in [in Huffman.PBTree]
all_leaves_NoDup [in Huffman.BTree]
all_leaves_unique [in Huffman.BTree]
all_leaves_inb [in Huffman.BTree]
all_leaves_in [in Huffman.BTree]
app_inv_app2 [in Huffman.AuxLib]
app_inv_app [in Huffman.AuxLib]


B

btree_unique_prefix [in Huffman.BTree]
btree_unique_prefix2 [in Huffman.BTree]
btree_unique_prefix1 [in Huffman.BTree]
build_correct [in Huffman.Build]
build_permutation [in Huffman.Build]
build_same_weight_tree [in Huffman.Build]
build_comp [in Huffman.Build]
build_cover [in Huffman.Build]


C

compute_pbcode_not_null [in Huffman.PBTree]
correct_encoding [in Huffman.Code]
cover_all_leaves [in Huffman.Cover]
cover_all_cover [in Huffman.Cover]
cover_all_cover_aux [in Huffman.Cover]
cover_number_of_nodes [in Huffman.Cover]
cover_app [in Huffman.Cover]
cover_inv_app [in Huffman.Cover]
cover_inv_app_aux [in Huffman.Cover]
cover_one_inv [in Huffman.Cover]
cover_inv_leaf [in Huffman.Cover]
cover_inv_leaf_aux [in Huffman.Cover]
cover_in_inb [in Huffman.Cover]
cover_in_inb_inb [in Huffman.Cover]
cover_not_nil [in Huffman.Cover]
cover_cons_l [in Huffman.Cover]
cover_permutation [in Huffman.Cover]
cover_min_ex [in Huffman.CoverMin]
cover_min_permutation [in Huffman.CoverMin]
cover_min_one [in Huffman.CoverMin]
cover_ordered_cover [in Huffman.OrderedCover]


D

decode_correct [in Huffman.Code]
decode_aux_correct [in Huffman.Code]
distinct_pbleaves_pbadd_prop2 [in Huffman.PBTree]
distinct_pbleaves_pbadd_prop1 [in Huffman.PBTree]
distinct_pbleaves_pbright [in Huffman.PBTree]
distinct_pbleaves_pbleft [in Huffman.PBTree]
distinct_pbleaves_pbleaf [in Huffman.PBTree]
distinct_pbleaves_pr [in Huffman.PBTree]
distinct_pbleaves_pl [in Huffman.PBTree]
distinct_pbleaves_r [in Huffman.PBTree]
distinct_pbleaves_l [in Huffman.PBTree]
distinct_pbleaves_Leaf [in Huffman.PBTree]
distinct_leaves_r [in Huffman.BTree]
distinct_leaves_l [in Huffman.BTree]
distinct_leaves_leaf [in Huffman.BTree]


E

encode_permutation_val [in Huffman.Code]
encode_permutation [in Huffman.Code]
encode_cons_inv [in Huffman.Code]
encode_app [in Huffman.Code]
exist_first_max [in Huffman.AuxLib]


F

find_max_correct [in Huffman.AuxLib]
find_min_correct [in Huffman.AuxLib]
find_val_correct2 [in Huffman.Code]
find_val_correct1 [in Huffman.Code]
find_code_permutation [in Huffman.Code]
find_code_app [in Huffman.Code]
find_code_correct2 [in Huffman.Code]
find_code_correct1 [in Huffman.Code]
firstn_le_length_eq [in Huffman.AuxLib]
firstn_le_app2 [in Huffman.AuxLib]
firstn_le_app1 [in Huffman.AuxLib]
fold_left_permutation [in Huffman.AuxLib]
fold_left_init [in Huffman.AuxLib]
fold_left_map [in Huffman.AuxLib]
fold_left_eta [in Huffman.AuxLib]
fold_pbadd_prop_node [in Huffman.PBTree]
fold_pbadd_prop_right [in Huffman.PBTree]
fold_pbadd_prop_left [in Huffman.PBTree]
fold_plus_permutation [in Huffman.Weight]
fold_plus_split [in Huffman.Weight]
frequency_list_restric_code_map [in Huffman.Restrict]
frequency_not_null [in Huffman.Code]
frequency_length [in Huffman.Weight]
frequency_number_of_occurrences [in Huffman.Frequency]
frequency_list_unique [in Huffman.Frequency]
frequency_list_perm [in Huffman.Frequency]
frequency_list_in [in Huffman.Frequency]


H

height_pred_compute_code [in Huffman.HeightPred]
height_pred_shrink [in Huffman.HeightPred]
height_pred_shrink_aux [in Huffman.HeightPred]
height_pred_disj_larger2 [in Huffman.HeightPred]
height_pred_disj_larger2_aux [in Huffman.HeightPred]
height_pred_disj_larger [in Huffman.HeightPred]
height_pred_disj_larger_aux [in Huffman.HeightPred]
height_pred_larger_ex [in Huffman.HeightPred]
height_pred_larger_strict [in Huffman.HeightPred]
height_pred_larger [in Huffman.HeightPred]
height_pred_weight [in Huffman.HeightPred]
height_pred_length [in Huffman.HeightPred]
height_pred_not_nil2 [in Huffman.HeightPred]
height_pred_not_nil1 [in Huffman.HeightPred]
height_pred_ordered_cover [in Huffman.HeightPred]
height_pred_subst_pred [in Huffman.SubstPred]
huffman_build_minimum [in Huffman.Huffman]


I

inb_compute_ex [in Huffman.BTree]
inb_antisym [in Huffman.BTree]
inb_ex [in Huffman.BTree]
inb_trans [in Huffman.BTree]
inCompute_inb [in Huffman.BTree]
inpbleaf_pbadd_inv [in Huffman.PBTree]
inpbleaf_eq [in Huffman.PBTree]
inpb_pbbuild_inv [in Huffman.PBTree]
inpb_pbadd_ex [in Huffman.PBTree]
inpb_pbadd [in Huffman.PBTree]
inpb_compute_ex [in Huffman.PBTree]
inpb_ex [in Huffman.PBTree]
inpb_trans [in Huffman.PBTree]
insert_permutation [in Huffman.ISort]
insert_ordered [in Huffman.ISort]
in_flat_map_ex [in Huffman.AuxLib]
in_flat_map_in [in Huffman.AuxLib]
in_map_fst_inv [in Huffman.AuxLib]
in_map_inv [in Huffman.AuxLib]
in_ex_app [in Huffman.AuxLib]
in_pbleaf_node [in Huffman.PBTree]
in_pbcompute_inpb [in Huffman.PBTree]
in_find_map [in Huffman.Code]
in_alphabet_inv [in Huffman.Code]
in_alphabet_cons [in Huffman.Code]
in_alphabet_nil [in Huffman.Code]
in_alphabet_incl [in Huffman.Code]
in_alphabet_compute_code [in Huffman.BTree]
in_frequency_map_inv [in Huffman.Frequency]
in_frequency_map [in Huffman.Frequency]
isort_permutation [in Huffman.ISort]
isort_ordered [in Huffman.ISort]
is_prefix_refl [in Huffman.Code]


L

length_compute_lt_O [in Huffman.BTree]
length_encode_nId [in Huffman.Weight]
le_minus [in Huffman.AuxLib]
le_sum_correct2 [in Huffman.WeightTree]
le_sum_correct1 [in Huffman.WeightTree]
list_length_ind [in Huffman.AuxLib]


M

map2_app [in Huffman.AuxLib]


N

NoDup_app_inv_r [in Huffman.AuxLib]
NoDup_app_inv_l [in Huffman.AuxLib]
NoDup_app_inv [in Huffman.AuxLib]
NoDup_app [in Huffman.AuxLib]
NoDup_pbadd_prop2 [in Huffman.PBTree]
NoDup_unique_key [in Huffman.UniqueKey]
NoDup_unique_key [in Huffman.Weight]
NoDup_ordered_cover [in Huffman.OrderedCover]
not_null_find_val [in Huffman.Code]
not_in_find_map [in Huffman.Code]
not_in_find_code [in Huffman.Code]
not_null_map [in Huffman.Code]
not_null_app [in Huffman.Code]
not_null_cons [in Huffman.Code]
not_null_inv [in Huffman.Code]
not_null_m [in Huffman.Huffman]
number_of_nodes_inb_le [in Huffman.BTree]
number_of_occurrences_permutation [in Huffman.Frequency]
number_of_occurrences_app [in Huffman.Frequency]
number_of_occurrences_permutation_ex [in Huffman.Frequency]
number_of_occurrences_O [in Huffman.Frequency]


O

one_cover_ex [in Huffman.Cover]
one_step_comp [in Huffman.OneStep]
one_step_same_sum_leaves [in Huffman.OneStep]
one_step_weight_tree_list [in Huffman.OneStep]
ordered_map_inv [in Huffman.Ordered]
ordered_perm_antisym_eq [in Huffman.Ordered]
ordered_trans_app [in Huffman.Ordered]
ordered_trans [in Huffman.Ordered]
ordered_skip [in Huffman.Ordered]
ordered_inv [in Huffman.Ordered]
ordered_inv_order [in Huffman.Ordered]
ordered_cover_height_pred [in Huffman.HeightPred]
ordered_sum_leaves_eq [in Huffman.WeightTree]
ordered_cover_cover [in Huffman.OrderedCover]
ordered_cover_subst_pred [in Huffman.SubstPred]


P

pbadd_prop2 [in Huffman.PBTree]
pbadd_prop1 [in Huffman.PBTree]
pbbuild_pbnode [in Huffman.PBTree]
pbbuild_true_pbright [in Huffman.PBTree]
pbbuild_compute_peq [in Huffman.PBTree]
pbbuild_distinct_pbleaves [in Huffman.PBTree]
pbbuild_compute_perm [in Huffman.PBTree]
pbfree_pbbuild_prop1 [in Huffman.PBTree]
pbfree_pbadd_prop2 [in Huffman.PBTree]
pbfree_pbadd_prop1 [in Huffman.PBTree]
pbleaf_or_not [in Huffman.PBTree]
pb_unique_prefix [in Huffman.PBTree]
pb_unique_key [in Huffman.PBTree]
pb_unique_prefix1 [in Huffman.PBTree]
Permutation_transposition [in Huffman.AuxLib]
permutation_all_permutations [in Huffman.AuxLib]
permutation_all_permutations_aux [in Huffman.AuxLib]
prod2list_reorder2 [in Huffman.Prod2List]
prod2list_reorder [in Huffman.Prod2List]
prod2list_eq [in Huffman.Prod2List]
prod2list_le_r [in Huffman.Prod2List]
prod2list_le_l [in Huffman.Prod2List]
prod2list_app [in Huffman.Prod2List]


R

restrict_code_pbbuild [in Huffman.Restrict]
restrict_not_null [in Huffman.Restrict]
restrict_unique_prefix [in Huffman.Restrict]
restrict_code_encode [in Huffman.Restrict]
restrict_code_encode_incl [in Huffman.Restrict]
restrict_code_in [in Huffman.Restrict]
restrict_code_unique_key [in Huffman.Restrict]
restrict_code_encode_length [in Huffman.Weight]
restrict_code_encode_length_inc [in Huffman.Weight]
restrict_code_in [in Huffman.Weight]
restrict_code_unique_key [in Huffman.Weight]


S

same_length_ex [in Huffman.AuxLib]
same_sum_leaves_length [in Huffman.SameSumLeaves]
skipn_le_app2 [in Huffman.AuxLib]
skipn_le_app1 [in Huffman.AuxLib]
split_one_in_ex [in Huffman.AuxLib]
split_one_permutation [in Huffman.AuxLib]
subst_pred_length [in Huffman.SubstPred]
subst_pred_ordered_cover_r [in Huffman.SubstPred]
subst_pred_ordered_cover_l [in Huffman.SubstPred]


T

to_btree_smaller [in Huffman.PBTree2BTree]
to_btree_distinct_pbleaves [in Huffman.PBTree2BTree]
to_btree_distinct_leaves [in Huffman.PBTree2BTree]
to_btree_all_leaves [in Huffman.PBTree2BTree]
to_btree_inpb [in Huffman.PBTree2BTree]
to_btree_inb [in Huffman.PBTree2BTree]


U

unique_key_map [in Huffman.UniqueKey]
unique_key_NoDup [in Huffman.UniqueKey]
unique_key_app [in Huffman.UniqueKey]
unique_key_perm [in Huffman.UniqueKey]
unique_key_in_inv [in Huffman.UniqueKey]
unique_key_in [in Huffman.UniqueKey]
unique_key_inv [in Huffman.UniqueKey]
unique_prefix_permutation [in Huffman.Code]
unique_prefix_not_null [in Huffman.Code]
unique_prefix_inv [in Huffman.Code]
unique_prefix2 [in Huffman.Code]
unique_prefix1 [in Huffman.Code]
unique_prefix_nil [in Huffman.Code]


W

weight_tree_compute [in Huffman.HeightPred]
weight_tree_list_permutation [in Huffman.WeightTree]
weight_tree_list_node [in Huffman.WeightTree]
weight_permutation [in Huffman.Weight]


Constructor Index

B

build_step [in Huffman.Build]
build_one [in Huffman.Build]


C

cover_node [in Huffman.Cover]
cover_one [in Huffman.Cover]


H

height_pred_node [in Huffman.HeightPred]
height_pred_nil [in Huffman.HeightPred]


I

inleaf [in Huffman.BTree]
innodeL [in Huffman.BTree]
innodeR [in Huffman.BTree]
inpb_node_r [in Huffman.PBTree]
inpb_node_l [in Huffman.PBTree]
inpb_right [in Huffman.PBTree]
inpb_left [in Huffman.PBTree]
inpb_leaf [in Huffman.PBTree]


L

leaf [in Huffman.BTree]


N

node [in Huffman.BTree]


O

ordered_cons [in Huffman.Ordered]
ordered_one [in Huffman.Ordered]
ordered_nil [in Huffman.Ordered]
ordered_cover_node [in Huffman.OrderedCover]
ordered_cover_one [in Huffman.OrderedCover]


P

pbfree_node2 [in Huffman.PBTree]
pbfree_node1 [in Huffman.PBTree]
pbfree_right2 [in Huffman.PBTree]
pbfree_right1 [in Huffman.PBTree]
pbfree_left2 [in Huffman.PBTree]
pbfree_left1 [in Huffman.PBTree]
pbleaf [in Huffman.PBTree]
pbleft [in Huffman.PBTree]
pbnode [in Huffman.PBTree]
pbright [in Huffman.PBTree]
prefixCons [in Huffman.Code]
prefixNull [in Huffman.Code]


S

subst_pred_node [in Huffman.SubstPred]
subst_pred_id [in Huffman.SubstPred]


U

unique_key_cons [in Huffman.UniqueKey]
unique_key_nil [in Huffman.UniqueKey]


Inductive Index

B

btree [in Huffman.BTree]
build [in Huffman.Build]


C

cover [in Huffman.Cover]


H

height_pred [in Huffman.HeightPred]


I

inb [in Huffman.BTree]
inpb [in Huffman.PBTree]
is_prefix [in Huffman.Code]


O

ordered [in Huffman.Ordered]
ordered_cover [in Huffman.OrderedCover]


P

pbfree [in Huffman.PBTree]
pbtree [in Huffman.PBTree]


S

subst_pred [in Huffman.SubstPred]


U

unique_key [in Huffman.UniqueKey]


Section Index

B

Build [in Huffman.Build]


C

Code [in Huffman.Code]
Cover [in Huffman.Cover]
CoverMin [in Huffman.CoverMin]


F

FindMin [in Huffman.AuxLib]
First [in Huffman.AuxLib]
FirstMax [in Huffman.AuxLib]
Fold [in Huffman.AuxLib]
Frequency [in Huffman.Frequency]


H

HeightPred [in Huffman.HeightPred]
Huffman [in Huffman.Huffman]


I

ISortExample [in Huffman.ISort]


L

List [in Huffman.AuxLib]


M

map2 [in Huffman.AuxLib]


O

OneStep [in Huffman.OneStep]
ordered [in Huffman.Ordered]
OrderedCover [in Huffman.OrderedCover]


P

PBTree [in Huffman.PBTree]
PBTREE2BTREE [in Huffman.PBTree2BTree]
Permutation [in Huffman.AuxLib]
Prod2List [in Huffman.Prod2List]


R

Restrict [in Huffman.Restrict]


S

SameSumLeaves [in Huffman.SameSumLeaves]
SubstPred [in Huffman.SubstPred]


T

Tree [in Huffman.BTree]


U

UniqueKey [in Huffman.UniqueKey]


W

Weight [in Huffman.Weight]
WeightTree [in Huffman.WeightTree]


Definition Index

A

add_frequency_list [in Huffman.Frequency]
all_permutations [in Huffman.AuxLib]
all_permutations_aux [in Huffman.AuxLib]
all_cover [in Huffman.Cover]
all_cover_aux [in Huffman.Cover]
all_pbleaves [in Huffman.PBTree]
all_leaves [in Huffman.BTree]


B

btree_dec [in Huffman.BTree]
buildf [in Huffman.Build]
build_fun [in Huffman.Build]


C

code [in Huffman.Code]
code_dec [in Huffman.Code]
compute_pbcode [in Huffman.PBTree]
compute_code [in Huffman.BTree]
cover_dec [in Huffman.Cover]
cover_min [in Huffman.CoverMin]


D

decode [in Huffman.Code]
decode_aux [in Huffman.Code]
distinct_pbleaves [in Huffman.PBTree]
distinct_leaves_dec [in Huffman.BTree]
distinct_leaves [in Huffman.BTree]


E

encode [in Huffman.Code]


F

find_max [in Huffman.AuxLib]
find_min [in Huffman.AuxLib]
find_val [in Huffman.Code]
find_code [in Huffman.Code]
frequency_list [in Huffman.Frequency]


H

huffman [in Huffman.Huffman]
huffman_aux [in Huffman.Huffman]
huffman_aux_F [in Huffman.Huffman]
huffman_aux_type [in Huffman.Huffman]


I

id_list [in Huffman.Frequency]
inb_dec [in Huffman.BTree]
inpb_dec [in Huffman.PBTree]
insert [in Huffman.ISort]
in_alphabet_dec [in Huffman.Code]
in_alphabet [in Huffman.Code]
isort [in Huffman.ISort]


L

le_sum [in Huffman.WeightTree]
list_length_induction [in Huffman.AuxLib]


M

map2 [in Huffman.AuxLib]


N

not_null [in Huffman.Code]
number_of_nodes [in Huffman.BTree]
number_of_occurrences [in Huffman.Frequency]


O

obuildf [in Huffman.Build]
one_step [in Huffman.OneStep]


P

pbadd [in Huffman.PBTree]
pbbuild [in Huffman.PBTree]
pbtree_dec [in Huffman.PBTree]
Permutation_dec [in Huffman.AuxLib]
prod2list [in Huffman.Prod2List]


R

restrict_code [in Huffman.Restrict]
restrict_code [in Huffman.Weight]


S

same_sum_leaves [in Huffman.SameSumLeaves]
split_one [in Huffman.AuxLib]
sum_order [in Huffman.WeightTree]
sum_leaves [in Huffman.WeightTree]


T

to_btree [in Huffman.PBTree2BTree]


U

unique_prefix [in Huffman.Code]


W

weight [in Huffman.Weight]
weight_tree_list [in Huffman.WeightTree]
weight_tree [in Huffman.WeightTree]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1953 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1461 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (70 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (23 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (259 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (37 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (13 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (62 entries)