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 | (2702 entries) |

Notation 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 | (7 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 | (1773 entries) |

Module 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 | (55 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 | (17 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 | (330 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 | (49 entries) |

Axiom 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 | (105 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 | (23 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 | (343 entries) |

# Global Index

## A

Abs [definition, in Trie]Abs [definition, in SearchTree]

Abs [axiom, in Extract]

abstract [definition, in Trie]

Abs_three_ten [definition, in Trie]

Abs_inj [axiom, in Extract]

Abs' [definition, in SearchTree]

acc:217 [binder, in SearchTree]

acc:37 [binder, in Redblack]

acc:74 [binder, in Extract]

add_edge [definition, in Color]

adj [definition, in Color]

adj_ext [lemma, in Color]

adj:67 [binder, in Color]

adj:71 [binder, in Color]

ADT [library]

al:102 [binder, in Priqueue]

al:105 [binder, in Binom]

al:107 [binder, in Selection]

al:108 [binder, in Binom]

al:108 [binder, in Selection]

al:110 [binder, in Binom]

al:12 [binder, in Priqueue]

al:122 [binder, in Binom]

al:135 [binder, in Binom]

al:15 [binder, in Multiset]

al:16 [binder, in Sort]

al:18 [binder, in BagPerm]

al:19 [binder, in Sort]

al:19 [binder, in Multiset]

al:21 [binder, in Priqueue]

al:22 [binder, in BagPerm]

al:22 [binder, in Perm]

al:23 [binder, in Multiset]

al:24 [binder, in Perm]

al:25 [binder, in Color]

al:25 [binder, in Sort]

al:29 [binder, in Selection]

al:32 [binder, in Sort]

al:33 [binder, in Color]

al:33 [binder, in Sort]

al:34 [binder, in BagPerm]

al:36 [binder, in BagPerm]

al:36 [binder, in Multiset]

al:40 [binder, in Perm]

al:40 [binder, in Decide]

al:40 [binder, in Multiset]

al:43 [binder, in Priqueue]

al:43 [binder, in Decide]

al:49 [binder, in Selection]

al:51 [binder, in Perm]

al:52 [binder, in Perm]

al:54 [binder, in Perm]

al:55 [binder, in Extract]

al:57 [binder, in Perm]

al:58 [binder, in Priqueue]

al:59 [binder, in Selection]

al:63 [binder, in Priqueue]

al:63 [binder, in Selection]

al:7 [binder, in Color]

al:71 [binder, in Selection]

al:72 [binder, in Selection]

al:78 [binder, in Priqueue]

al:80 [binder, in Priqueue]

al:85 [binder, in Priqueue]

al:9 [binder, in Priqueue]

al:9 [binder, in Color]

al:94 [binder, in Binom]

apply_empty [lemma, in Maps]

a_vector [definition, in ADT]

A:1 [binder, in Color]

A:1 [binder, in Decide]

A:1 [binder, in Maps]

a:10 [binder, in Multiset]

A:103 [binder, in Trie]

a:104 [binder, in Trie]

a:11 [binder, in Decide]

A:11 [binder, in Merge]

A:117 [binder, in Trie]

A:119 [binder, in Trie]

a:12 [binder, in Multiset]

A:12 [binder, in Maps]

A:122 [binder, in Trie]

A:125 [binder, in Trie]

A:127 [binder, in Trie]

a:13 [binder, in Decide]

a:13 [binder, in Merge]

A:131 [binder, in Trie]

A:133 [binder, in Trie]

A:137 [binder, in Trie]

A:14 [binder, in Sort]

a:14 [binder, in Merge]

A:15 [binder, in Sort]

a:15 [binder, in Decide]

a:172 [binder, in SearchTree]

a:18 [binder, in Perm]

A:2 [binder, in Maps]

A:20 [binder, in Color]

A:21 [binder, in Maps]

A:22 [binder, in Merge]

A:24 [binder, in Color]

a:24 [binder, in Merge]

a:25 [binder, in Merge]

A:26 [binder, in Color]

a:26 [binder, in Sort]

A:29 [binder, in Merge]

a:30 [binder, in Decide]

a:30 [binder, in Selection]

A:303 [binder, in ADT]

A:307 [binder, in ADT]

A:311 [binder, in ADT]

A:315 [binder, in ADT]

A:32 [binder, in Color]

a:32 [binder, in Merge]

A:321 [binder, in ADT]

A:326 [binder, in ADT]

A:330 [binder, in ADT]

A:334 [binder, in ADT]

a:34 [binder, in Merge]

A:35 [binder, in Color]

a:35 [binder, in Sort]

A:35 [binder, in Maps]

A:36 [binder, in Maps]

a:37 [binder, in Perm]

A:37 [binder, in Maps]

A:38 [binder, in Color]

a:38 [binder, in Perm]

a:39 [binder, in Sort]

a:39 [binder, in Perm]

a:4 [binder, in Multiset]

A:4 [binder, in Maps]

A:41 [binder, in Maps]

A:42 [binder, in Color]

A:43 [binder, in Maps]

A:45 [binder, in Trie]

A:45 [binder, in Color]

A:46 [binder, in Trie]

A:48 [binder, in Trie]

a:49 [binder, in Perm]

a:5 [binder, in Decide]

A:52 [binder, in Maps]

A:53 [binder, in Color]

A:55 [binder, in Perm]

A:59 [binder, in Trie]

A:62 [binder, in Trie]

A:63 [binder, in Trie]

A:65 [binder, in Trie]

a:7 [binder, in Decide]

a:7 [binder, in Multiset]

A:72 [binder, in Trie]

A:75 [binder, in Trie]

a:78 [binder, in Trie]

A:84 [binder, in Trie]

a:86 [binder, in Trie]

a:9 [binder, in Decide]

A:9 [binder, in Maps]

A:95 [binder, in Trie]

a:96 [binder, in Trie]

A:98 [binder, in Trie]

a:99 [binder, in Trie]

## B

bag [definition, in BagPerm]BagPerm [library]

bag_eqv_iff_perm [lemma, in BagPerm]

bag_perm [lemma, in BagPerm]

bag_cons_inv [lemma, in BagPerm]

bag_nil_inv [lemma, in BagPerm]

bag_eqv_cons [lemma, in BagPerm]

bag_eqv_trans [lemma, in BagPerm]

bag_eqv_sym [lemma, in BagPerm]

bag_eqv_refl [lemma, in BagPerm]

bag_eqv [definition, in BagPerm]

balance [definition, in Redblack]

balanceP [lemma, in Redblack]

balance_lookup [lemma, in Redblack]

balance_BST [lemma, in Redblack]

balance_BST [lemma, in Redblack]

balance_BST [lemma, in Redblack]

Binom [library]

BinomQueue [module, in Binom]

BinomQueue.Abs [definition, in Binom]

BinomQueue.abs_perm [lemma, in Binom]

BinomQueue.can_relate [lemma, in Binom]

BinomQueue.carry [definition, in Binom]

BinomQueue.carry_elems [lemma, in Binom]

BinomQueue.carry_valid [lemma, in Binom]

BinomQueue.delete_max_Some_relate [lemma, in Binom]

BinomQueue.delete_max_None_relate [lemma, in Binom]

BinomQueue.delete_max_Some_priq [lemma, in Binom]

BinomQueue.delete_max [definition, in Binom]

BinomQueue.delete_max_aux [definition, in Binom]

BinomQueue.empty [definition, in Binom]

BinomQueue.empty_relate [lemma, in Binom]

BinomQueue.empty_priq [lemma, in Binom]

BinomQueue.find_max [definition, in Binom]

BinomQueue.find_max' [definition, in Binom]

BinomQueue.heap_delete_max [definition, in Binom]

BinomQueue.insert [definition, in Binom]

BinomQueue.insert_relate [lemma, in Binom]

BinomQueue.insert_priq [lemma, in Binom]

BinomQueue.join [definition, in Binom]

BinomQueue.join_elems [lemma, in Binom]

BinomQueue.join_valid [lemma, in Binom]

BinomQueue.key [definition, in Binom]

BinomQueue.Leaf [constructor, in Binom]

BinomQueue.manual_grade_for_priqueue_elems [definition, in Binom]

BinomQueue.merge [definition, in Binom]

BinomQueue.merge_relate [lemma, in Binom]

BinomQueue.merge_priq [lemma, in Binom]

BinomQueue.Node [constructor, in Binom]

BinomQueue.pow2heap [definition, in Binom]

BinomQueue.pow2heap' [definition, in Binom]

BinomQueue.priq [definition, in Binom]

BinomQueue.priqueue [definition, in Binom]

BinomQueue.priqueue_elems_ext [lemma, in Binom]

BinomQueue.priqueue_elems [inductive, in Binom]

BinomQueue.priq' [definition, in Binom]

BinomQueue.smash [definition, in Binom]

BinomQueue.smash_elems [lemma, in Binom]

BinomQueue.smash_valid [lemma, in Binom]

BinomQueue.tree [inductive, in Binom]

BinomQueue.tree_can_relate [lemma, in Binom]

BinomQueue.tree_perm [lemma, in Binom]

BinomQueue.tree_elems_ext [lemma, in Binom]

BinomQueue.tree_elems_node [constructor, in Binom]

BinomQueue.tree_elems_leaf [constructor, in Binom]

BinomQueue.tree_elems [inductive, in Binom]

BinomQueue.unzip [definition, in Binom]

Black [constructor, in Redblack]

bl:10 [binder, in Color]

bl:104 [binder, in Selection]

bl:106 [binder, in Binom]

bl:109 [binder, in Selection]

bl:13 [binder, in Priqueue]

bl:23 [binder, in BagPerm]

bl:24 [binder, in Multiset]

bl:34 [binder, in Color]

bl:35 [binder, in BagPerm]

bl:37 [binder, in BagPerm]

bl:37 [binder, in Multiset]

bl:41 [binder, in Decide]

bl:41 [binder, in Multiset]

bl:50 [binder, in Selection]

bl:58 [binder, in Perm]

bl:60 [binder, in Priqueue]

bl:60 [binder, in Selection]

bl:64 [binder, in Selection]

bl:65 [binder, in Priqueue]

bl:67 [binder, in Selection]

bl:8 [binder, in Color]

bl:81 [binder, in Priqueue]

bl:85 [binder, in Binom]

bound [definition, in SearchTree]

bound_relate' [lemma, in SearchTree]

bound_relate [lemma, in SearchTree]

bound_value [lemma, in SearchTree]

bound_default [lemma, in SearchTree]

br:86 [binder, in Binom]

BST [inductive, in Redblack]

BST [inductive, in SearchTree]

BST_T [constructor, in SearchTree]

BST_E [constructor, in SearchTree]

bt:114 [binder, in Binom]

butterfly [definition, in Perm]

bu:115 [binder, in Binom]

b

_{1}:11 [binder, in BagPerm]

b

_{1}:15 [binder, in BagPerm]

b

_{1}:5 [binder, in BagPerm]

b

_{1}:9 [binder, in BagPerm]

b

_{2}:10 [binder, in BagPerm]

b

_{2}:12 [binder, in BagPerm]

b

_{2}:16 [binder, in BagPerm]

b

_{2}:6 [binder, in BagPerm]

b

_{3}:13 [binder, in BagPerm]

b:10 [binder, in Decide]

b:11 [binder, in Multiset]

b:12 [binder, in Decide]

b:13 [binder, in Multiset]

b:14 [binder, in Decide]

b:15 [binder, in Merge]

b:16 [binder, in Decide]

b:171 [binder, in SearchTree]

b:19 [binder, in Perm]

B:2 [binder, in Decide]

b:24 [binder, in BagPerm]

b:26 [binder, in Perm]

b:26 [binder, in Merge]

B:27 [binder, in Color]

b:283 [binder, in ADT]

b:288 [binder, in ADT]

b:33 [binder, in Selection]

b:35 [binder, in Merge]

b:41 [binder, in Perm]

B:46 [binder, in Color]

b:5 [binder, in Multiset]

b:50 [binder, in Perm]

b:6 [binder, in Decide]

b:8 [binder, in BagPerm]

b:8 [binder, in Decide]

b:8 [binder, in Multiset]

b:90 [binder, in Binom]

## C

cardinal_map [lemma, in Color]carry:18 [binder, in Trie]

ce:130 [binder, in Binom]

ci:119 [binder, in Color]

ci:120 [binder, in Color]

cj:121 [binder, in Color]

color [inductive, in Redblack]

color [definition, in Color]

Color [library]

coloring [definition, in Color]

coloring_ok [definition, in Color]

colors_of [definition, in Color]

color_correct [lemma, in Color]

color1 [definition, in Color]

compute_with_StdLib_lt_dec [lemma, in Decide]

compute_with_lt_dec [lemma, in Decide]

cons_of_small_maintains_sort' [lemma, in Selection]

cons_of_small_maintains_sort [lemma, in Selection]

contents [definition, in Multiset]

contents_perm [lemma, in Multiset]

contents_insert_other [lemma, in Multiset]

contents_cons_inv [lemma, in Multiset]

contents_nil_inv [lemma, in Multiset]

cont:24 [binder, in Binom]

count [definition, in BagPerm]

count_insert_other [lemma, in BagPerm]

cts:141 [binder, in Trie]

current:31 [binder, in Binom]

c:105 [binder, in Redblack]

c:114 [binder, in Redblack]

c:126 [binder, in Binom]

c:128 [binder, in Color]

c:137 [binder, in Redblack]

c:14 [binder, in Redblack]

c:14 [binder, in Multiset]

c:18 [binder, in Binom]

c:189 [binder, in Redblack]

c:195 [binder, in Redblack]

c:2 [binder, in Trie]

c:245 [binder, in Redblack]

c:28 [binder, in Trie]

c:31 [binder, in Selection]

c:36 [binder, in Selection]

c:54 [binder, in Trie]

c:58 [binder, in Redblack]

c:71 [binder, in Redblack]

c:76 [binder, in Binom]

c:79 [binder, in Redblack]

c:9 [binder, in Multiset]

c:90 [binder, in Trie]

## D

Decide [library]default:126 [binder, in Trie]

default:132 [binder, in Trie]

default:256 [binder, in ADT]

default:47 [binder, in Trie]

default:61 [binder, in Extract]

default:64 [binder, in Trie]

default:66 [binder, in Trie]

default:76 [binder, in Trie]

default:80 [binder, in Extract]

default:83 [binder, in Extract]

default:88 [binder, in Extract]

disjoint [definition, in SearchTree]

domain_example_map [definition, in Color]

d:117 [binder, in SearchTree]

d:123 [binder, in SearchTree]

d:128 [binder, in SearchTree]

d:133 [binder, in Redblack]

d:136 [binder, in Redblack]

d:139 [binder, in SearchTree]

d:146 [binder, in Redblack]

d:15 [binder, in SearchTree]

d:151 [binder, in Redblack]

d:155 [binder, in SearchTree]

d:157 [binder, in Redblack]

d:160 [binder, in SearchTree]

d:162 [binder, in Redblack]

d:165 [binder, in SearchTree]

d:173 [binder, in Redblack]

d:176 [binder, in Redblack]

d:181 [binder, in Redblack]

d:192 [binder, in SearchTree]

d:230 [binder, in SearchTree]

d:242 [binder, in ADT]

d:244 [binder, in ADT]

d:260 [binder, in ADT]

d:261 [binder, in SearchTree]

d:261 [binder, in ADT]

d:278 [binder, in ADT]

d:285 [binder, in SearchTree]

d:294 [binder, in ADT]

d:299 [binder, in ADT]

d:337 [binder, in SearchTree]

d:34 [binder, in Selection]

d:37 [binder, in Selection]

d:51 [binder, in SearchTree]

d:55 [binder, in SearchTree]

d:60 [binder, in SearchTree]

d:65 [binder, in SearchTree]

d:71 [binder, in SearchTree]

d:74 [binder, in SearchTree]

d:78 [binder, in SearchTree]

d:8 [binder, in Redblack]

d:81 [binder, in SearchTree]

d:90 [binder, in SearchTree]

## E

E [constructor, in Redblack]E [module, in Color]

E [constructor, in SearchTree]

E [constructor, in Extract]

elements [definition, in Redblack]

elements [definition, in SearchTree]

elements [definition, in Extract]

elements_aux [definition, in Redblack]

elements_relate' [lemma, in SearchTree]

elements_relate [lemma, in SearchTree]

elements_empty [lemma, in SearchTree]

elements_nodup_keys [lemma, in SearchTree]

elements_correct_inverse [lemma, in SearchTree]

elements_complete_inverse [lemma, in SearchTree]

elements_correct [lemma, in SearchTree]

elements_preserves_relation [lemma, in SearchTree]

elements_preserves_forall [lemma, in SearchTree]

elements_correct_spec [definition, in SearchTree]

elements_complete [lemma, in SearchTree]

elements_complete_spec [definition, in SearchTree]

elements_complete_broken [lemma, in SearchTree]

elements_complete_broken_spec [definition, in SearchTree]

elements_ex [definition, in SearchTree]

elements_aux [definition, in Extract]

el

_{1}:345 [binder, in SearchTree]

el

_{2}:346 [binder, in SearchTree]

el:133 [binder, in Color]

el:255 [binder, in SearchTree]

el:273 [binder, in SearchTree]

el:277 [binder, in SearchTree]

empty [definition, in Trie]

empty [definition, in Multiset]

empty [definition, in Maps]

empty_relate [lemma, in Trie]

empty_is_trie [lemma, in Trie]

empty_tree_BST [lemma, in Redblack]

empty_tree [definition, in Redblack]

empty_relate' [lemma, in SearchTree]

empty_relate [lemma, in SearchTree]

empty_tree_BST [lemma, in SearchTree]

empty_tree [definition, in SearchTree]

empty_map [definition, in ADT]

empty_tree [definition, in Extract]

eqb_reflect [lemma, in Perm]

eqlistA_Eeq_eq [lemma, in Color]

equivlistA_example [definition, in Color]

eq:119 [binder, in Binom]

ETable [module, in ADT]

ETableAbs [module, in ADT]

ETableAbs.Abs [axiom, in ADT]

ETableAbs.bound [axiom, in ADT]

ETableAbs.bound_relate [axiom, in ADT]

ETableAbs.default [axiom, in ADT]

ETableAbs.elements [axiom, in ADT]

ETableAbs.elements_relate [axiom, in ADT]

ETableAbs.empty [axiom, in ADT]

ETableAbs.empty_relate [axiom, in ADT]

ETableAbs.empty_ok [axiom, in ADT]

ETableAbs.get [axiom, in ADT]

ETableAbs.insert_relate [axiom, in ADT]

ETableAbs.key [definition, in ADT]

ETableAbs.lookup_relate [axiom, in ADT]

ETableAbs.rep_ok [axiom, in ADT]

ETableAbs.set [axiom, in ADT]

ETableAbs.set_ok [axiom, in ADT]

ETableAbs.table [axiom, in ADT]

ETableAbs.V [axiom, in ADT]

ETableSubset [module, in ADT]

ETableSubset.bound [axiom, in ADT]

ETableSubset.bound_set_other [axiom, in ADT]

ETableSubset.bound_set_same [axiom, in ADT]

ETableSubset.bound_empty [axiom, in ADT]

ETableSubset.elements [axiom, in ADT]

ETableSubset.elements_correct [axiom, in ADT]

ETableSubset.elements_complete [axiom, in ADT]

ETable_first_attempt.elements_correct [axiom, in ADT]

ETable_first_attempt.elements_complete [axiom, in ADT]

ETable_first_attempt.elements [axiom, in ADT]

ETable_first_attempt.bound [axiom, in ADT]

ETable_first_attempt [module, in ADT]

ETable.bound [axiom, in ADT]

ETable.bound_set_other [axiom, in ADT]

ETable.bound_set_same [axiom, in ADT]

ETable.bound_empty [axiom, in ADT]

ETable.elements [axiom, in ADT]

ETable.elements_correct [axiom, in ADT]

ETable.elements_complete [axiom, in ADT]

ETable.empty_ok [axiom, in ADT]

ETable.rep_ok [axiom, in ADT]

ETable.set_ok [axiom, in ADT]

et:120 [binder, in Binom]

even_nat [definition, in ADT]

Even2 [lemma, in ADT]

Even2' [definition, in ADT]

examplemap [definition, in Maps]

example_map [definition, in Color]

exposed_trees_ex [definition, in ADT]

Extract [library]

extra_fuel [definition, in Selection]

ex_tree [definition, in SearchTree]

e

_{1}:102 [binder, in Binom]

e

_{1}:242 [binder, in SearchTree]

e

_{1}:96 [binder, in Binom]

e

_{1}:99 [binder, in Binom]

e

_{2}:100 [binder, in Binom]

e

_{2}:103 [binder, in Binom]

e

_{2}:243 [binder, in SearchTree]

e

_{2}:97 [binder, in Binom]

e:131 [binder, in Color]

e:23 [binder, in Color]

e:310 [binder, in ADT]

e:314 [binder, in ADT]

e:328 [binder, in ADT]

e:332 [binder, in ADT]

e:336 [binder, in ADT]

e:44 [binder, in Perm]

## F

FastEnough [module, in Trie]FastEnough.collisions [definition, in Trie]

FastEnough.collisions_pi [definition, in Trie]

FastEnough.loop [definition, in Trie]

fast_elements_correct [lemma, in SearchTree]

fast_elements_eq_elements [lemma, in SearchTree]

fast_elements_tr_helper [lemma, in SearchTree]

fast_elements [definition, in SearchTree]

fast_elements_tr [definition, in SearchTree]

filter_sortE [lemma, in Color]

find [definition, in SearchTree]

first_le_second [definition, in Perm]

fold_right_rev_left [lemma, in Color]

ForallT [definition, in Redblack]

ForallT [definition, in SearchTree]

ForallT_less [lemma, in Redblack]

ForallT_greater [lemma, in Redblack]

ForallT_imp [lemma, in Redblack]

ForallT_insert [lemma, in SearchTree]

Forall_perm [lemma, in Perm]

FunTable [module, in ADT]

FunTableExamples [module, in ADT]

FunTableExamples.ex1 [definition, in ADT]

FunTableExamples.ex2 [definition, in ADT]

FunTableExamples.ex3 [definition, in ADT]

FunTableExamples.StringFunTable [module, in ADT]

FunTable.default [definition, in ADT]

FunTable.empty [definition, in ADT]

FunTable.get [definition, in ADT]

FunTable.get_set_other [lemma, in ADT]

FunTable.get_set_same [lemma, in ADT]

FunTable.get_empty_default [lemma, in ADT]

FunTable.key [definition, in ADT]

FunTable.set [definition, in ADT]

FunTable.table [definition, in ADT]

FunTable.V [definition, in ADT]

f:104 [binder, in Color]

f:11 [binder, in Color]

f:111 [binder, in Color]

f:116 [binder, in Color]

f:127 [binder, in Color]

f:16 [binder, in Color]

f:17 [binder, in BagPerm]

f:17 [binder, in Perm]

f:170 [binder, in SearchTree]

f:18 [binder, in Multiset]

f:24 [binder, in Sort]

f:28 [binder, in Color]

f:28 [binder, in Selection]

f:284 [binder, in ADT]

f:289 [binder, in ADT]

f:46 [binder, in Perm]

f:47 [binder, in Color]

f:56 [binder, in Perm]

## G

G [definition, in Color]geb [definition, in Perm]

geb_reflect [lemma, in Perm]

graph [definition, in Color]

gtb [definition, in Perm]

gtb_reflect [lemma, in Perm]

g:109 [binder, in Color]

g:113 [binder, in Color]

g:115 [binder, in Color]

g:122 [binder, in Color]

g:130 [binder, in Color]

g:132 [binder, in Color]

g:29 [binder, in Color]

g:55 [binder, in Color]

g:56 [binder, in Color]

g:58 [binder, in Color]

g:61 [binder, in Color]

g:63 [binder, in Color]

g:65 [binder, in Color]

g:73 [binder, in Color]

g:75 [binder, in Color]

g:77 [binder, in Color]

g:80 [binder, in Color]

g:83 [binder, in Color]

g:85 [binder, in Color]

g:88 [binder, in Color]

g:90 [binder, in Color]

g:92 [binder, in Color]

## H

height [definition, in Redblack]H

_{0}:33 [binder, in Merge]

H

_{1}:37 [binder, in Merge]

H:31 [binder, in Merge]

## I

InA_map_fst_key [lemma, in Color]InA_example [definition, in Color]

input:1 [binder, in Trie]

input:53 [binder, in Trie]

input:58 [binder, in Trie]

input:6 [binder, in Trie]

input:89 [binder, in Trie]

input:94 [binder, in Trie]

ins [definition, in Trie]

ins [definition, in Redblack]

ins [definition, in Extract]

insert [definition, in Trie]

insert [definition, in Redblack]

insert [definition, in SearchTree]

insert [definition, in Sort]

insert [definition, in Extract]

insertion_sort_correct [lemma, in Sort]

insertion_sort_correct [lemma, in BagPerm]

insertion_sort_correct [lemma, in Multiset]

insert_relate [lemma, in Trie]

insert_is_trie [lemma, in Trie]

insert_RB [lemma, in Redblack]

insert_BST [lemma, in Redblack]

insert_BST [lemma, in Redblack]

insert_relate' [lemma, in SearchTree]

insert_relate [lemma, in SearchTree]

insert_permute_equality_breaks [lemma, in SearchTree]

insert_same_equality_breaks [lemma, in SearchTree]

insert_shadow_equality [lemma, in SearchTree]

insert_BST [lemma, in SearchTree]

insert_sorted' [lemma, in Sort]

insert_perm [lemma, in Sort]

insert_sorted [lemma, in Sort]

insert_bag [lemma, in BagPerm]

insert_contents [lemma, in Multiset]

insP [lemma, in Redblack]

insZ [definition, in Extract]

ins_red [lemma, in Redblack]

ins_RB [lemma, in Redblack]

ins_BST [lemma, in Redblack]

ins_not_E [lemma, in Redblack]

ins_not_E [lemma, in Redblack]

ins_int [definition, in Extract]

int [axiom, in Extract]

Integers [module, in Trie]

Integers.add [definition, in Trie]

Integers.addc [definition, in Trie]

Integers.addc_correct [lemma, in Trie]

Integers.add_correct [lemma, in Trie]

Integers.compare [definition, in Trie]

Integers.compare_correct [lemma, in Trie]

Integers.comparison [inductive, in Trie]

Integers.Eq [constructor, in Trie]

Integers.Gt [constructor, in Trie]

Integers.Lt [constructor, in Trie]

Integers.positive [inductive, in Trie]

Integers.positive2nat [definition, in Trie]

Integers.positive2nat_pos [lemma, in Trie]

Integers.print_in_binary [definition, in Trie]

Integers.succ [definition, in Trie]

Integers.succ_correct [lemma, in Trie]

Integers.ten [definition, in Trie]

Integers.xH [constructor, in Trie]

Integers.xI [constructor, in Trie]

Integers.xO [constructor, in Trie]

Integers.Z [inductive, in Trie]

Integers.Zneg [constructor, in Trie]

Integers.Zpos [constructor, in Trie]

Integers.Z0 [constructor, in Trie]

_ ~ 0 [notation, in Trie]

_ ~ 1 [notation, in Trie]

int_leb_reflect [lemma, in Extract]

int_ltb_reflect [lemma, in Extract]

in_colors_of_1 [lemma, in Color]

in_map_of_list [lemma, in SearchTree]

in_fst [lemma, in SearchTree]

in_4_pi [definition, in Decide]

is_trie [definition, in Trie]

is_BST_ex [definition, in SearchTree]

is_a_sorting_algorithm [definition, in Sort]

is_a_sorting_algorithm' [definition, in BagPerm]

is_a_sorting_algorithm [definition, in Selection]

is_a_sorting_algorithm' [definition, in Multiset]

iv:22 [binder, in Sort]

iv:37 [binder, in Sort]

i':38 [binder, in Sort]

i:1 [binder, in Sort]

i:1 [binder, in Extract]

i:11 [binder, in Perm]

i:112 [binder, in Trie]

i:115 [binder, in Trie]

i:117 [binder, in Color]

i:123 [binder, in Color]

i:125 [binder, in Color]

i:128 [binder, in Trie]

i:13 [binder, in Color]

i:134 [binder, in Trie]

i:14 [binder, in Perm]

i:17 [binder, in Color]

i:17 [binder, in Sort]

i:20 [binder, in Sort]

i:24 [binder, in Selection]

i:25 [binder, in Selection]

i:30 [binder, in Color]

i:32 [binder, in Decide]

i:35 [binder, in Decide]

i:36 [binder, in Sort]

i:38 [binder, in Decide]

i:39 [binder, in Color]

i:42 [binder, in Decide]

i:42 [binder, in Extract]

i:43 [binder, in Color]

i:45 [binder, in Priqueue]

i:49 [binder, in Color]

i:5 [binder, in Color]

i:53 [binder, in Priqueue]

i:57 [binder, in Priqueue]

i:57 [binder, in Color]

i:59 [binder, in Color]

i:61 [binder, in Binom]

i:62 [binder, in Priqueue]

i:62 [binder, in Color]

i:67 [binder, in Trie]

i:7 [binder, in Perm]

i:73 [binder, in Trie]

i:77 [binder, in Trie]

i:8 [binder, in Extract]

i:85 [binder, in Trie]

i:88 [binder, in Trie]

## J

jv:23 [binder, in Sort]j:105 [binder, in Trie]

j:116 [binder, in Trie]

j:118 [binder, in Color]

j:12 [binder, in Perm]

j:124 [binder, in Color]

j:15 [binder, in Perm]

j:18 [binder, in Sort]

j:21 [binder, in Color]

j:21 [binder, in Sort]

j:26 [binder, in Selection]

j:33 [binder, in Decide]

j:36 [binder, in Decide]

j:39 [binder, in Decide]

j:42 [binder, in Binom]

j:44 [binder, in Binom]

j:49 [binder, in Priqueue]

j:5 [binder, in Selection]

j:51 [binder, in Priqueue]

j:55 [binder, in Priqueue]

j:59 [binder, in Priqueue]

j:6 [binder, in Color]

j:60 [binder, in Color]

j:64 [binder, in Priqueue]

j:7 [binder, in Selection]

j:8 [binder, in Perm]

j:97 [binder, in Trie]

## K

key [definition, in Redblack]key [definition, in SearchTree]

key [definition, in Extract]

kvs_insert_elements [lemma, in SearchTree]

kvs_insert_split [lemma, in SearchTree]

kvs_insert [definition, in SearchTree]

kvs:236 [binder, in SearchTree]

k':102 [binder, in Redblack]

k':103 [binder, in Redblack]

k':110 [binder, in Redblack]

k':111 [binder, in Redblack]

k':119 [binder, in SearchTree]

k':119 [binder, in ADT]

k':122 [binder, in SearchTree]

k':131 [binder, in SearchTree]

k':139 [binder, in Redblack]

k':14 [binder, in ADT]

k':140 [binder, in ADT]

k':143 [binder, in Redblack]

k':144 [binder, in Redblack]

k':154 [binder, in Redblack]

k':165 [binder, in Redblack]

k':165 [binder, in ADT]

k':179 [binder, in SearchTree]

k':184 [binder, in Redblack]

k':246 [binder, in SearchTree]

k':248 [binder, in SearchTree]

k':25 [binder, in ADT]

k':31 [binder, in ADT]

k':365 [binder, in ADT]

k':391 [binder, in ADT]

k':399 [binder, in ADT]

k':45 [binder, in ADT]

k':58 [binder, in ADT]

k':63 [binder, in Redblack]

k':64 [binder, in Redblack]

k':67 [binder, in SearchTree]

k':76 [binder, in Redblack]

k':77 [binder, in Redblack]

k':84 [binder, in Redblack]

k':85 [binder, in Redblack]

k':91 [binder, in Extract]

k':92 [binder, in SearchTree]

k':95 [binder, in ADT]

k':96 [binder, in Redblack]

k':97 [binder, in Redblack]

k':97 [binder, in SearchTree]

k

_{0}:101 [binder, in Redblack]

k

_{0}:245 [binder, in SearchTree]

k

_{0}:95 [binder, in Redblack]

k

_{1}:110 [binder, in SearchTree]

k

_{1}:129 [binder, in SearchTree]

k

_{1}:145 [binder, in SearchTree]

k

_{2}:111 [binder, in SearchTree]

k

_{2}:130 [binder, in SearchTree]

k

_{2}:146 [binder, in SearchTree]

k:10 [binder, in Perm]

k:100 [binder, in Trie]

k:100 [binder, in Redblack]

k:103 [binder, in SearchTree]

k:103 [binder, in ADT]

k:105 [binder, in SearchTree]

k:106 [binder, in Trie]

k:107 [binder, in Redblack]

k:108 [binder, in ADT]

k:111 [binder, in ADT]

k:114 [binder, in ADT]

k:115 [binder, in ADT]

k:117 [binder, in Redblack]

k:118 [binder, in SearchTree]

k:118 [binder, in ADT]

k:121 [binder, in SearchTree]

k:122 [binder, in Redblack]

k:122 [binder, in ADT]

k:123 [binder, in Binom]

k:125 [binder, in ADT]

k:126 [binder, in Redblack]

k:129 [binder, in ADT]

k:13 [binder, in Perm]

k:13 [binder, in ADT]

k:131 [binder, in Redblack]

k:132 [binder, in ADT]

k:134 [binder, in Redblack]

k:135 [binder, in SearchTree]

k:135 [binder, in ADT]

k:136 [binder, in ADT]

k:138 [binder, in Trie]

k:138 [binder, in Redblack]

k:139 [binder, in Binom]

k:139 [binder, in ADT]

k:141 [binder, in SearchTree]

k:143 [binder, in ADT]

k:146 [binder, in ADT]

k:148 [binder, in Redblack]

k:153 [binder, in Redblack]

k:153 [binder, in SearchTree]

k:154 [binder, in ADT]

k:157 [binder, in ADT]

k:158 [binder, in SearchTree]

k:159 [binder, in Redblack]

k:16 [binder, in Redblack]

k:16 [binder, in Perm]

k:160 [binder, in ADT]

k:161 [binder, in ADT]

k:163 [binder, in SearchTree]

k:164 [binder, in Redblack]

k:164 [binder, in ADT]

k:168 [binder, in ADT]

k:17 [binder, in Priqueue]

k:171 [binder, in Redblack]

k:171 [binder, in ADT]

k:174 [binder, in Redblack]

k:175 [binder, in ADT]

k:178 [binder, in Redblack]

k:178 [binder, in SearchTree]

k:183 [binder, in Redblack]

k:185 [binder, in SearchTree]

k:189 [binder, in SearchTree]

k:191 [binder, in ADT]

k:192 [binder, in Redblack]

k:194 [binder, in SearchTree]

k:197 [binder, in ADT]

k:198 [binder, in Redblack]

k:20 [binder, in ADT]

k:200 [binder, in ADT]

k:203 [binder, in ADT]

k:208 [binder, in ADT]

k:209 [binder, in Redblack]

k:211 [binder, in ADT]

k:214 [binder, in Redblack]

k:214 [binder, in ADT]

k:218 [binder, in Redblack]

k:22 [binder, in Priqueue]

k:22 [binder, in ADT]

k:220 [binder, in ADT]

k:224 [binder, in Redblack]

k:224 [binder, in ADT]

k:226 [binder, in ADT]

k:228 [binder, in SearchTree]

k:228 [binder, in ADT]

k:233 [binder, in Redblack]

k:234 [binder, in SearchTree]

k:244 [binder, in SearchTree]

k:252 [binder, in SearchTree]

k:26 [binder, in ADT]

k:262 [binder, in SearchTree]

k:265 [binder, in SearchTree]

k:27 [binder, in ADT]

k:274 [binder, in SearchTree]

k:278 [binder, in SearchTree]

k:28 [binder, in Priqueue]

k:282 [binder, in SearchTree]

k:286 [binder, in SearchTree]

k:289 [binder, in SearchTree]

k:296 [binder, in SearchTree]

k:30 [binder, in ADT]

k:300 [binder, in SearchTree]

k:304 [binder, in SearchTree]

k:308 [binder, in SearchTree]

k:314 [binder, in SearchTree]

k:319 [binder, in SearchTree]

k:32 [binder, in Priqueue]

k:328 [binder, in SearchTree]

k:335 [binder, in SearchTree]

k:339 [binder, in SearchTree]

k:34 [binder, in ADT]

k:341 [binder, in SearchTree]

k:358 [binder, in ADT]

k:360 [binder, in ADT]

k:364 [binder, in ADT]

k:369 [binder, in ADT]

k:37 [binder, in ADT]

k:373 [binder, in ADT]

k:378 [binder, in ADT]

k:380 [binder, in ADT]

k:383 [binder, in ADT]

k:386 [binder, in ADT]

k:387 [binder, in ADT]

k:390 [binder, in ADT]

k:394 [binder, in ADT]

k:395 [binder, in ADT]

k:398 [binder, in ADT]

k:40 [binder, in ADT]

k:402 [binder, in ADT]

k:405 [binder, in ADT]

k:41 [binder, in ADT]

k:43 [binder, in Binom]

k:44 [binder, in SearchTree]

k:44 [binder, in ADT]

k:45 [binder, in Binom]

k:47 [binder, in SearchTree]

k:48 [binder, in ADT]

k:5 [binder, in SearchTree]

k:50 [binder, in ADT]

k:52 [binder, in SearchTree]

k:53 [binder, in ADT]

k:54 [binder, in ADT]

k:56 [binder, in SearchTree]

k:57 [binder, in ADT]

k:60 [binder, in Redblack]

k:61 [binder, in SearchTree]

k:63 [binder, in ADT]

k:66 [binder, in SearchTree]

k:67 [binder, in Priqueue]

k:67 [binder, in ADT]

k:69 [binder, in Redblack]

K:69 [binder, in Color]

k:7 [binder, in ADT]

k:70 [binder, in SearchTree]

k:71 [binder, in ADT]

k:73 [binder, in Redblack]

k:74 [binder, in ADT]

k:75 [binder, in SearchTree]

K:76 [binder, in Color]

k:77 [binder, in SearchTree]

k:77 [binder, in ADT]

K:79 [binder, in Color]

k:81 [binder, in Redblack]

k:81 [binder, in Extract]

k:82 [binder, in Priqueue]

K:82 [binder, in Color]

k:82 [binder, in SearchTree]

k:82 [binder, in Binom]

K:84 [binder, in Color]

k:84 [binder, in ADT]

k:85 [binder, in Extract]

k:86 [binder, in Priqueue]

k:86 [binder, in SearchTree]

K:87 [binder, in Color]

k:88 [binder, in ADT]

k:89 [binder, in Priqueue]

K:89 [binder, in Color]

k:9 [binder, in Perm]

k:9 [binder, in ADT]

k:90 [binder, in Redblack]

k:90 [binder, in ADT]

k:90 [binder, in Extract]

K:91 [binder, in Color]

k:91 [binder, in SearchTree]

k:93 [binder, in Priqueue]

k:94 [binder, in Redblack]

k:94 [binder, in ADT]

k:96 [binder, in SearchTree]

k:99 [binder, in ADT]

## L

Leaf [constructor, in Trie]leb [axiom, in Extract]

leb_reflect [lemma, in Perm]

leb_le [axiom, in Extract]

le_all__le_one [lemma, in Selection]

le_all [definition, in Selection]

lia_example_3 [lemma, in Perm]

lia_example2 [lemma, in Perm]

lia_example1 [lemma, in Perm]

lia_example1 [lemma, in Perm]

ListETableAbs [module, in ADT]

ListETableAbs.Abs [definition, in ADT]

ListETableAbs.bound [definition, in ADT]

ListETableAbs.bound_relate [lemma, in ADT]

ListETableAbs.default [definition, in ADT]

ListETableAbs.elements [definition, in ADT]

ListETableAbs.elements_relate [lemma, in ADT]

ListETableAbs.empty [definition, in ADT]

ListETableAbs.empty_relate [lemma, in ADT]

ListETableAbs.empty_ok [lemma, in ADT]

ListETableAbs.get [definition, in ADT]

ListETableAbs.insert_relate [lemma, in ADT]

ListETableAbs.key [definition, in ADT]

ListETableAbs.lookup_relate [lemma, in ADT]

ListETableAbs.rep_ok [definition, in ADT]

ListETableAbs.set [definition, in ADT]

ListETableAbs.set_ok [lemma, in ADT]

ListETableAbs.table [definition, in ADT]

ListETableAbs.V [definition, in ADT]

ListQueue [module, in ADT]

ListQueue.deq [definition, in ADT]

ListQueue.deq_nonempty [lemma, in ADT]

ListQueue.deq_empty [lemma, in ADT]

ListQueue.empty [definition, in ADT]

ListQueue.enq [definition, in ADT]

ListQueue.is_empty_nonempty [lemma, in ADT]

ListQueue.is_empty_empty [lemma, in ADT]

ListQueue.is_empty [definition, in ADT]

ListQueue.peek [definition, in ADT]

ListQueue.peek_nonempty [lemma, in ADT]

ListQueue.peek_empty [lemma, in ADT]

ListQueue.queue [definition, in ADT]

ListQueue.V [definition, in ADT]

ListsTable [module, in ADT]

ListsTable.default [definition, in ADT]

ListsTable.empty [definition, in ADT]

ListsTable.get [definition, in ADT]

ListsTable.get_set_other [lemma, in ADT]

ListsTable.get_set_same [lemma, in ADT]

ListsTable.get_empty_default [lemma, in ADT]

ListsTable.key [definition, in ADT]

ListsTable.set [definition, in ADT]

ListsTable.table [definition, in ADT]

ListsTable.V [definition, in ADT]

List_Priqueue.merge_relate [lemma, in Priqueue]

List_Priqueue.merge_priq [lemma, in Priqueue]

List_Priqueue.delete_max_Some_relate [lemma, in Priqueue]

List_Priqueue.delete_max_None_relate [lemma, in Priqueue]

List_Priqueue.delete_max_Some_priq [lemma, in Priqueue]

List_Priqueue.insert_relate [lemma, in Priqueue]

List_Priqueue.insert_priq [lemma, in Priqueue]

List_Priqueue.empty_relate [lemma, in Priqueue]

List_Priqueue.empty_priq [lemma, in Priqueue]

List_Priqueue.abs_perm [lemma, in Priqueue]

List_Priqueue.can_relate [lemma, in Priqueue]

List_Priqueue.Abs [definition, in Priqueue]

List_Priqueue.Abs_intro [constructor, in Priqueue]

List_Priqueue.Abs' [inductive, in Priqueue]

List_Priqueue.priq [definition, in Priqueue]

List_Priqueue.merge [definition, in Priqueue]

List_Priqueue.delete_max [definition, in Priqueue]

List_Priqueue.insert [definition, in Priqueue]

List_Priqueue.empty [definition, in Priqueue]

List_Priqueue.priqueue [definition, in Priqueue]

List_Priqueue.key [definition, in Priqueue]

List_Priqueue.select_biggest [lemma, in Priqueue]

List_Priqueue.select_biggest_aux [lemma, in Priqueue]

List_Priqueue.select_perm [lemma, in Priqueue]

List_Priqueue.select [definition, in Priqueue]

List_Priqueue [module, in Priqueue]

list_keys [definition, in SearchTree]

list_nat_in [definition, in Decide]

list_nat_eq_dec [definition, in Decide]

list_of_vector [definition, in ADT]

list_ind2 [definition, in Merge]

list_ind2_principle [definition, in Merge]

look [definition, in Trie]

lookup [definition, in Trie]

lookup [definition, in Redblack]

lookup [definition, in SearchTree]

lookup [definition, in Extract]

lookup_relate [lemma, in Trie]

lookup_insert_neq [lemma, in Redblack]

lookup_insert_eq [lemma, in Redblack]

lookup_ins_neq [lemma, in Redblack]

lookup_ins_eq [lemma, in Redblack]

lookup_empty [lemma, in Redblack]

lookup_relate' [lemma, in SearchTree]

lookup_relate [lemma, in SearchTree]

lookup_insert_permute [lemma, in SearchTree]

lookup_insert_same [lemma, in SearchTree]

lookup_insert_shadow [lemma, in SearchTree]

lookup_insert_neq [lemma, in SearchTree]

lookup_insert_eq' [lemma, in SearchTree]

lookup_insert_eq [lemma, in SearchTree]

lookup_empty [lemma, in SearchTree]

lookup_insert_neq [lemma, in Extract]

lookup_insert_eq [lemma, in Extract]

lookup_empty [lemma, in Extract]

look_ins_other [lemma, in Trie]

look_ins_same [lemma, in Trie]

look_leaf [lemma, in Trie]

low_deg [definition, in Color]

lst:203 [binder, in SearchTree]

lst:224 [binder, in SearchTree]

lst:269 [binder, in SearchTree]

lst:56 [binder, in Selection]

ltb [axiom, in Extract]

ltb_reflect [lemma, in Perm]

ltb_lt [axiom, in Extract]

lt_proper [lemma, in Color]

lt_strict [lemma, in Color]

l':50 [binder, in Priqueue]

l':52 [binder, in Priqueue]

l':6 [binder, in Selection]

l':8 [binder, in Selection]

l

_{1}:102 [binder, in Merge]

l

_{1}:197 [binder, in SearchTree]

l

_{1}:20 [binder, in Merge]

l

_{1}:207 [binder, in SearchTree]

l

_{1}:211 [binder, in SearchTree]

l

_{1}:28 [binder, in BagPerm]

l

_{1}:30 [binder, in BagPerm]

l

_{1}:30 [binder, in Multiset]

l

_{1}:32 [binder, in Multiset]

l

_{1}:43 [binder, in Merge]

l

_{1}:47 [binder, in Merge]

l

_{1}:49 [binder, in Merge]

l

_{1}:5 [binder, in Merge]

l

_{1}:65 [binder, in Merge]

l

_{1}:72 [binder, in Merge]

l

_{1}:77 [binder, in Merge]

l

_{1}:9 [binder, in Merge]

l

_{1}:96 [binder, in Merge]

l

_{1}:99 [binder, in Merge]

l

_{2}:10 [binder, in Merge]

l

_{2}:100 [binder, in Merge]

l

_{2}:103 [binder, in Merge]

l

_{2}:198 [binder, in SearchTree]

l

_{2}:208 [binder, in SearchTree]

l

_{2}:21 [binder, in Merge]

l

_{2}:212 [binder, in SearchTree]

l

_{2}:29 [binder, in BagPerm]

l

_{2}:31 [binder, in BagPerm]

l

_{2}:31 [binder, in Multiset]

l

_{2}:33 [binder, in Multiset]

l

_{2}:44 [binder, in Merge]

l

_{2}:48 [binder, in Merge]

l

_{2}:50 [binder, in Merge]

l

_{2}:52 [binder, in Merge]

l

_{2}:6 [binder, in Merge]

l

_{2}:66 [binder, in Merge]

l

_{2}:73 [binder, in Merge]

l

_{2}:78 [binder, in Merge]

l

_{2}:98 [binder, in Merge]

l:101 [binder, in Merge]

l:103 [binder, in Selection]

l:104 [binder, in Merge]

l:106 [binder, in Redblack]

l:113 [binder, in Selection]

l:114 [binder, in Selection]

l:115 [binder, in Redblack]

l:12 [binder, in Color]

l:12 [binder, in Extract]

l:13 [binder, in Sort]

l:14 [binder, in Selection]

l:141 [binder, in Redblack]

l:16 [binder, in Merge]

l:17 [binder, in Merge]

l:18 [binder, in Decide]

l:19 [binder, in Merge]

l:190 [binder, in Redblack]

l:196 [binder, in Redblack]

l:2 [binder, in Sort]

l:2 [binder, in Selection]

l:2 [binder, in Merge]

l:2 [binder, in Extract]

l:20 [binder, in BagPerm]

l:207 [binder, in Redblack]

l:21 [binder, in BagPerm]

l:21 [binder, in Decide]

l:21 [binder, in Selection]

l:21 [binder, in Multiset]

l:212 [binder, in Redblack]

l:22 [binder, in Color]

l:22 [binder, in Multiset]

l:25 [binder, in BagPerm]

l:25 [binder, in Multiset]

l:27 [binder, in Sort]

l:27 [binder, in Selection]

l:27 [binder, in Multiset]

l:27 [binder, in Merge]

l:28 [binder, in Sort]

l:28 [binder, in Merge]

l:29 [binder, in Decide]

l:30 [binder, in Sort]

l:31 [binder, in Sort]

l:31 [binder, in Decide]

l:34 [binder, in SearchTree]

l:34 [binder, in Sort]

l:35 [binder, in Selection]

l:36 [binder, in Merge]

l:38 [binder, in Merge]

l:39 [binder, in Selection]

l:4 [binder, in SearchTree]

l:40 [binder, in Sort]

l:41 [binder, in Sort]

l:42 [binder, in Merge]

l:43 [binder, in Selection]

l:43 [binder, in Extract]

l:46 [binder, in Priqueue]

l:46 [binder, in Merge]

l:46 [binder, in Extract]

l:47 [binder, in Perm]

l:47 [binder, in Selection]

l:48 [binder, in Color]

l:48 [binder, in Selection]

l:5 [binder, in Sort]

l:5 [binder, in Extract]

l:54 [binder, in Priqueue]

l:54 [binder, in Extract]

l:59 [binder, in Redblack]

l:61 [binder, in Merge]

l:62 [binder, in Binom]

l:62 [binder, in Merge]

l:67 [binder, in Merge]

l:68 [binder, in Merge]

l:70 [binder, in Merge]

l:72 [binder, in Redblack]

l:73 [binder, in Selection]

l:74 [binder, in Merge]

l:75 [binder, in Merge]

l:78 [binder, in Selection]

l:79 [binder, in Selection]

l:8 [binder, in Merge]

l:80 [binder, in Redblack]

l:81 [binder, in Selection]

l:85 [binder, in Selection]

l:86 [binder, in Selection]

l:9 [binder, in Selection]

l:9 [binder, in Extract]

## M

M [module, in Color]make_black [definition, in Redblack]

manual_grade_for_successor_of_Z_constant_time [definition, in Trie]

manual_grade_for_redblack_bound [definition, in Redblack]

manual_grade_for_bound_correct [definition, in SearchTree]

manual_grade_for_permutations_vs_multiset [definition, in BagPerm]

manual_grade_for_Permutation_properties [definition, in Perm]

manual_grade_for_ListsETable [definition, in ADT]

manual_grade_for_TreeTableModel [definition, in ADT]

manual_grade_for_permutations_vs_multiset [definition, in Multiset]

Maps [library]

map_of_list_app [lemma, in SearchTree]

map_of_tree_prop [lemma, in SearchTree]

map_of_tree [definition, in SearchTree]

map_bound [definition, in SearchTree]

map_of_list [definition, in SearchTree]

map_find [definition, in ADT]

map_update [definition, in ADT]

maybe_swap_correct [lemma, in Perm]

maybe_swap_perm [lemma, in Perm]

maybe_swap_idempotent [lemma, in Perm]

maybe_swap_idempotent [lemma, in Perm]

maybe_swap_321 [definition, in Perm]

maybe_swap_123 [definition, in Perm]

maybe_swap [definition, in Perm]

Mdomain [definition, in Color]

merge [definition, in Merge]

Merge [library]

mergesort_correct [lemma, in Merge]

mergesort_perm [lemma, in Merge]

mergesort_sorts [lemma, in Merge]

merge_perm [lemma, in Merge]

merge_nil_l [lemma, in Merge]

merge_aux:56 [binder, in Merge]

merge2 [lemma, in Merge]

mindepth [definition, in Redblack]

mk_graph [definition, in Color]

Mremove_cardinal_less [lemma, in Color]

Mremove_elements [lemma, in Color]

multiset [definition, in Multiset]

Multiset [library]

m

_{1}:294 [binder, in SearchTree]

m

_{1}:298 [binder, in SearchTree]

m

_{1}:302 [binder, in SearchTree]

m

_{1}:306 [binder, in SearchTree]

m

_{1}:312 [binder, in SearchTree]

m

_{1}:317 [binder, in SearchTree]

m

_{2}:295 [binder, in SearchTree]

m

_{2}:299 [binder, in SearchTree]

m

_{2}:303 [binder, in SearchTree]

m

_{2}:307 [binder, in SearchTree]

m

_{2}:313 [binder, in SearchTree]

m

_{2}:318 [binder, in SearchTree]

m:100 [binder, in SearchTree]

m:106 [binder, in SearchTree]

m:112 [binder, in SearchTree]

m:124 [binder, in Trie]

m:13 [binder, in Maps]

m:136 [binder, in Trie]

m:177 [binder, in ADT]

m:18 [binder, in Extract]

m:2 [binder, in Color]

m:2 [binder, in Perm]

m:20 [binder, in Maps]

m:22 [binder, in Maps]

m:22 [binder, in Extract]

m:26 [binder, in Extract]

m:263 [binder, in SearchTree]

m:266 [binder, in SearchTree]

m:28 [binder, in Maps]

m:34 [binder, in Maps]

m:38 [binder, in Binom]

m:38 [binder, in Maps]

m:4 [binder, in Perm]

m:44 [binder, in Maps]

m:49 [binder, in Trie]

m:5 [binder, in Maps]

m:51 [binder, in Maps]

m:52 [binder, in Binom]

m:53 [binder, in Maps]

m:6 [binder, in Perm]

m:60 [binder, in Maps]

m:66 [binder, in Maps]

m:68 [binder, in Trie]

m:79 [binder, in Trie]

m:85 [binder, in SearchTree]

m:98 [binder, in SearchTree]

## N

NatFunTableExamples [module, in ADT]nat2pos [definition, in Trie]

nat2pos_injective [lemma, in Trie]

nat2pos2nat [lemma, in Trie]

NearlyRB [inductive, in Redblack]

NearlyRB_b [constructor, in Redblack]

NearlyRB_r [constructor, in Redblack]

NicelyEncapsulatedExample [module, in ADT]

NicelyEncapsulatedExample.ex1 [definition, in ADT]

NicelyEncapsulatedExample.ex2 [definition, in ADT]

NicelyEncapsulatedExample.StringTreeETableEncapsulated [module, in ADT]

Node [constructor, in Trie]

node [definition, in Color]

nodemap [definition, in Color]

nodes [definition, in Color]

nodeset [definition, in Color]

NoDup_append [lemma, in SearchTree]

NotBst [module, in SearchTree]

NotBst.not_bst_lookup_wrong [definition, in SearchTree]

NotBst.t [definition, in SearchTree]

not_in_map_of_list [lemma, in SearchTree]

not_BST_ex [definition, in SearchTree]

not_a_permutation [definition, in Perm]

no_selfloop [definition, in Color]

nth_error_insert [lemma, in Sort]

n':230 [binder, in Redblack]

n':236 [binder, in Redblack]

n:1 [binder, in Perm]

n:102 [binder, in Selection]

n:106 [binder, in Color]

n:106 [binder, in Selection]

n:109 [binder, in Trie]

n:110 [binder, in Trie]

n:110 [binder, in Color]

n:111 [binder, in Binom]

n:112 [binder, in Selection]

n:116 [binder, in Binom]

n:121 [binder, in Trie]

n:127 [binder, in Binom]

n:15 [binder, in Selection]

n:17 [binder, in Extract]

n:194 [binder, in Redblack]

n:200 [binder, in Redblack]

n:200 [binder, in SearchTree]

n:201 [binder, in SearchTree]

n:203 [binder, in Redblack]

n:21 [binder, in Extract]

n:211 [binder, in Redblack]

n:216 [binder, in Redblack]

n:221 [binder, in Redblack]

n:226 [binder, in Redblack]

n:229 [binder, in Redblack]

n:235 [binder, in Redblack]

n:246 [binder, in Redblack]

n:25 [binder, in Extract]

n:27 [binder, in BagPerm]

n:29 [binder, in Multiset]

n:3 [binder, in Color]

n:3 [binder, in Perm]

n:339 [binder, in ADT]

n:46 [binder, in Selection]

n:5 [binder, in Perm]

n:51 [binder, in Binom]

n:52 [binder, in Color]

n:54 [binder, in Color]

n:58 [binder, in Binom]

n:58 [binder, in Selection]

n:66 [binder, in Color]

n:66 [binder, in Binom]

n:69 [binder, in Binom]

n:69 [binder, in Selection]

n:7 [binder, in BagPerm]

n:70 [binder, in Color]

n:70 [binder, in Selection]

n:72 [binder, in Color]

n:77 [binder, in Binom]

n:78 [binder, in Color]

## O

out_of_fuel [definition, in Selection]OverlyEncapsulatedExample [module, in ADT]

OverlyEncapsulatedExample.ex1 [definition, in ADT]

OverlyEncapsulatedExample.StringTreeETableFullyEncapsulated [module, in ADT]

## P

pairs_example [definition, in Selection]palette [definition, in Color]

palette:108 [binder, in Color]

palette:112 [binder, in Color]

palette:114 [binder, in Color]

palette:129 [binder, in Color]

partial_map [definition, in Maps]

pat:173 [binder, in SearchTree]

pat:247 [binder, in SearchTree]

pat:249 [binder, in SearchTree]

pat:285 [binder, in ADT]

pat:290 [binder, in ADT]

pat:341 [binder, in ADT]

Perm [library]

permut_example [definition, in Perm]

perm_bag [lemma, in BagPerm]

perm_contents [lemma, in Multiset]

pe:128 [binder, in Binom]

plus_two [definition, in ADT]

plus_two [definition, in ADT]

pl:100 [binder, in Priqueue]

pl:133 [binder, in Binom]

pl:140 [binder, in Binom]

pl:33 [binder, in Priqueue]

pl:41 [binder, in Priqueue]

pl:94 [binder, in Priqueue]

pos2nat [definition, in Trie]

pos2nat_injective [lemma, in Trie]

pos2nat2pos [lemma, in Trie]

Preface [library]

PRIQUEUE [module, in Priqueue]

Priqueue [library]

PRIQUEUE.Abs [axiom, in Priqueue]

PRIQUEUE.abs_perm [axiom, in Priqueue]

PRIQUEUE.can_relate [axiom, in Priqueue]

PRIQUEUE.delete_max_Some_relate [axiom, in Priqueue]

PRIQUEUE.delete_max_Some_priq [axiom, in Priqueue]

PRIQUEUE.delete_max_None_relate [axiom, in Priqueue]

PRIQUEUE.delete_max [axiom, in Priqueue]

PRIQUEUE.empty [axiom, in Priqueue]

PRIQUEUE.empty_relate [axiom, in Priqueue]

PRIQUEUE.empty_priq [axiom, in Priqueue]

PRIQUEUE.insert [axiom, in Priqueue]

PRIQUEUE.insert_relate [axiom, in Priqueue]

PRIQUEUE.insert_priq [axiom, in Priqueue]

PRIQUEUE.key [definition, in Priqueue]

PRIQUEUE.merge [axiom, in Priqueue]

PRIQUEUE.merge_relate [axiom, in Priqueue]

PRIQUEUE.merge_priq [axiom, in Priqueue]

PRIQUEUE.priq [axiom, in Priqueue]

PRIQUEUE.priqueue [axiom, in Priqueue]

Proper_eq_key_elt [lemma, in Color]

Proper_eq_eq [lemma, in Color]

p':47 [binder, in Binom]

p:104 [binder, in Binom]

p:109 [binder, in Binom]

p:11 [binder, in Priqueue]

p:111 [binder, in Trie]

p:113 [binder, in Trie]

P:113 [binder, in Redblack]

p:12 [binder, in Trie]

P:12 [binder, in Merge]

P:120 [binder, in Redblack]

p:121 [binder, in Binom]

p:124 [binder, in Binom]

p:131 [binder, in Binom]

p:136 [binder, in Binom]

p:137 [binder, in Binom]

p:16 [binder, in Binom]

P:175 [binder, in SearchTree]

p:18 [binder, in Priqueue]

p:20 [binder, in Priqueue]

P:23 [binder, in Merge]

p:24 [binder, in Priqueue]

P:25 [binder, in Perm]

p:26 [binder, in Priqueue]

p:27 [binder, in Trie]

P:27 [binder, in SearchTree]

p:29 [binder, in Trie]

p:30 [binder, in Priqueue]

P:30 [binder, in Merge]

P:304 [binder, in ADT]

P:308 [binder, in ADT]

p:31 [binder, in Trie]

P:312 [binder, in ADT]

P:316 [binder, in ADT]

P:322 [binder, in ADT]

P:326 [binder, in SearchTree]

P:327 [binder, in ADT]

P:331 [binder, in ADT]

P:335 [binder, in ADT]

p:36 [binder, in Priqueue]

p:39 [binder, in Priqueue]

p:39 [binder, in Binom]

p:40 [binder, in Trie]

P:42 [binder, in SearchTree]

p:49 [binder, in Binom]

P:51 [binder, in Redblack]

P:64 [binder, in Color]

p:68 [binder, in Priqueue]

p:69 [binder, in Priqueue]

p:71 [binder, in Priqueue]

p:73 [binder, in Priqueue]

P:74 [binder, in Color]

p:74 [binder, in Binom]

p:76 [binder, in Priqueue]

p:77 [binder, in Priqueue]

p:78 [binder, in Binom]

p:79 [binder, in Priqueue]

p:8 [binder, in Priqueue]

p:80 [binder, in Binom]

p:83 [binder, in Priqueue]

p:84 [binder, in Priqueue]

P:87 [binder, in Redblack]

p:87 [binder, in Priqueue]

p:9 [binder, in Trie]

p:90 [binder, in Priqueue]

p:91 [binder, in Priqueue]

p:93 [binder, in Binom]

p:96 [binder, in Priqueue]

p:98 [binder, in Priqueue]

## Q

qe:129 [binder, in Binom]ql:101 [binder, in Priqueue]

ql:134 [binder, in Binom]

ql:141 [binder, in Binom]

ql:34 [binder, in Priqueue]

ql:42 [binder, in Priqueue]

ql:95 [binder, in Priqueue]

Queue [module, in ADT]

QueueAbs [module, in ADT]

QueueAbs.Abs [axiom, in ADT]

QueueAbs.deq [axiom, in ADT]

QueueAbs.deq_relate [axiom, in ADT]

QueueAbs.empty [axiom, in ADT]

QueueAbs.empty_relate [axiom, in ADT]

QueueAbs.enq [axiom, in ADT]

QueueAbs.enq_relate [axiom, in ADT]

QueueAbs.is_empty [axiom, in ADT]

QueueAbs.peek [axiom, in ADT]

QueueAbs.peek_relate [axiom, in ADT]

QueueAbs.queue [axiom, in ADT]

QueueAbs.V [axiom, in ADT]

Queue.deq [axiom, in ADT]

Queue.deq_nonempty [axiom, in ADT]

Queue.deq_empty [axiom, in ADT]

Queue.empty [axiom, in ADT]

Queue.enq [axiom, in ADT]

Queue.is_empty_nonempty [axiom, in ADT]

Queue.is_empty_empty [axiom, in ADT]

Queue.is_empty [axiom, in ADT]

Queue.peek [axiom, in ADT]

Queue.peek_nonempty [axiom, in ADT]

Queue.peek_empty [axiom, in ADT]

Queue.queue [axiom, in ADT]

Queue.V [axiom, in ADT]

q':48 [binder, in Binom]

q:101 [binder, in Binom]

q:114 [binder, in Trie]

q:117 [binder, in Binom]

q:125 [binder, in Binom]

q:13 [binder, in Binom]

q:132 [binder, in Binom]

q:138 [binder, in Binom]

q:15 [binder, in Binom]

q:17 [binder, in Binom]

q:239 [binder, in ADT]

q:245 [binder, in ADT]

q:249 [binder, in ADT]

q:252 [binder, in ADT]

q:253 [binder, in ADT]

q:255 [binder, in ADT]

q:257 [binder, in ADT]

q:258 [binder, in ADT]

q:262 [binder, in ADT]

q:264 [binder, in ADT]

q:27 [binder, in Priqueue]

q:27 [binder, in Binom]

q:275 [binder, in ADT]

q:279 [binder, in ADT]

q:281 [binder, in ADT]

q:286 [binder, in ADT]

q:292 [binder, in ADT]

q:295 [binder, in ADT]

q:297 [binder, in ADT]

q:30 [binder, in Trie]

q:300 [binder, in ADT]

q:301 [binder, in ADT]

q:31 [binder, in Priqueue]

q:32 [binder, in Trie]

q:32 [binder, in Binom]

q:35 [binder, in Binom]

q:37 [binder, in Priqueue]

q:40 [binder, in Priqueue]

q:46 [binder, in Binom]

q:50 [binder, in Binom]

q:65 [binder, in Binom]

q:7 [binder, in Binom]

q:70 [binder, in Binom]

q:72 [binder, in Priqueue]

q:73 [binder, in Binom]

q:75 [binder, in Binom]

q:79 [binder, in Binom]

q:81 [binder, in Binom]

Q:88 [binder, in Redblack]

q:88 [binder, in Priqueue]

q:92 [binder, in Priqueue]

q:97 [binder, in Priqueue]

q:99 [binder, in Priqueue]

## R

RatherSlow [module, in Trie]RatherSlow.collisions [definition, in Trie]

RatherSlow.collisions_pi [definition, in Trie]

RatherSlow.empty [definition, in Trie]

RatherSlow.loop [definition, in Trie]

RatherSlow.total_mapz [definition, in Trie]

RatherSlow.update [definition, in Trie]

RB [inductive, in Redblack]

RB_blacken_root [lemma, in Redblack]

RB_blacken_parent [lemma, in Redblack]

RB_b [constructor, in Redblack]

RB_r [constructor, in Redblack]

RB_leaf [constructor, in Redblack]

Red [constructor, in Redblack]

Redblack [library]

redblack_balanced [lemma, in Redblack]

reflect_example2 [definition, in Perm]

reflect_example1' [definition, in Perm]

reflect_example1 [definition, in Perm]

remove_node [definition, in Color]

r':13 [binder, in Selection]

r':20 [binder, in Selection]

r':77 [binder, in Selection]

r':84 [binder, in Selection]

r':89 [binder, in Selection]

r

_{1}:59 [binder, in Merge]

r

_{2}:60 [binder, in Merge]

r:109 [binder, in Redblack]

r:116 [binder, in Redblack]

r:142 [binder, in Redblack]

R:182 [binder, in SearchTree]

r:191 [binder, in Redblack]

r:197 [binder, in Redblack]

r:208 [binder, in Redblack]

r:213 [binder, in Redblack]

r:37 [binder, in SearchTree]

r:41 [binder, in Selection]

r:45 [binder, in Perm]

r:45 [binder, in Selection]

r:56 [binder, in Priqueue]

r:62 [binder, in Redblack]

r:7 [binder, in SearchTree]

r:75 [binder, in Redblack]

r:83 [binder, in Redblack]

## S

S [module, in Color]same_mod_10 [definition, in Color]

same_contents_iff_perm [lemma, in Multiset]

ScratchPad [module, in Decide]

ScratchPad.greater23 [lemma, in Decide]

ScratchPad.is_3_less_7 [definition, in Decide]

ScratchPad.left [constructor, in Decide]

ScratchPad.less37 [lemma, in Decide]

ScratchPad.lt_dec_equivalent [lemma, in Decide]

ScratchPad.lt_dec' [definition, in Decide]

ScratchPad.lt_dec [definition, in Decide]

ScratchPad.right [constructor, in Decide]

ScratchPad.sumbool [inductive, in Decide]

ScratchPad.t1 [definition, in Decide]

ScratchPad.t2 [definition, in Decide]

ScratchPad.t4 [definition, in Decide]

ScratchPad.v1a [definition, in Decide]

ScratchPad.v1b [definition, in Decide]

ScratchPad.v2a [definition, in Decide]

ScratchPad.v3 [definition, in Decide]

{ _ } + { _ } (type_scope) [notation, in Decide]

ScratchPad2 [module, in Decide]

ScratchPad2.insert [definition, in Decide]

ScratchPad2.insert_sorted [lemma, in Decide]

ScratchPad2.le_dec [definition, in Decide]

ScratchPad2.lt_dec_axiom_2 [axiom, in Decide]

ScratchPad2.lt_dec_axiom_1 [axiom, in Decide]

ScratchPad2.lt_dec [definition, in Decide]

ScratchPad2.max_with_axiom [definition, in Decide]

ScratchPad2.prove_with_max_axiom [lemma, in Decide]

ScratchPad2.sort [definition, in Decide]

ScratchPad2.sorted [inductive, in Decide]

ScratchPad2.sorted_cons [constructor, in Decide]

ScratchPad2.sorted_1 [constructor, in Decide]

ScratchPad2.sorted_nil [constructor, in Decide]

SearchTree [library]

select [definition, in Selection]

Selection [library]

selection_sort_correct' [lemma, in Selection]

selection_sort_contents [lemma, in Selection]

selection_sort_is_correct [lemma, in Selection]

selection_sort_sorted [lemma, in Selection]

selection_sort_perm [lemma, in Selection]

selection_sort [definition, in Selection]

select_terminates [lemma, in Color]

select_contents [lemma, in Selection]

select_in [lemma, in Selection]

select_smallest [lemma, in Selection]

select_fst_leq [lemma, in Selection]

select_rest_length [lemma, in Selection]

select_perm [lemma, in Selection]

selsort [definition, in Selection]

selsort [definition, in Selection]

selsort_sorted [lemma, in Selection]

selsort_perm [lemma, in Selection]

selsort'_is_correct [lemma, in Selection]

selsort'_sorted [lemma, in Selection]

selsort'_perm [lemma, in Selection]

selsort'_example [definition, in Selection]

SigSandbox [module, in ADT]

SigSandbox.ex [inductive, in ADT]

SigSandbox.exist [constructor, in ADT]

SigSandbox.ex_intro [constructor, in ADT]

SigSandbox.proj1_ex [definition, in ADT]

SigSandbox.proj1_sig [definition, in ADT]

SigSandbox.proj2_sig [definition, in ADT]

SigSandbox.sig [inductive, in ADT]

{ _ : _ | _ } [notation, in ADT]

SimpleStringTable1 [module, in ADT]

SimpleStringTable1.default [definition, in ADT]

SimpleStringTable1.key [definition, in ADT]

SimpleStringTable1.table [definition, in ADT]

SimpleStringTable1.V [definition, in ADT]

SimpleStringTable2 [module, in ADT]

SimpleStringTable2.default [definition, in ADT]

SimpleStringTable2.key [definition, in ADT]

SimpleStringTable2.table [definition, in ADT]

SimpleStringTable2.V [definition, in ADT]

SimpleStringTable3 [module, in ADT]

SimpleStringTable3.default [definition, in ADT]

SimpleStringTable3.key [definition, in ADT]

SimpleStringTable3.table [definition, in ADT]

SimpleStringTable3.V [definition, in ADT]

SimpleTable [module, in ADT]

SimpleTable.default [axiom, in ADT]

SimpleTable.key [axiom, in ADT]

SimpleTable.table [axiom, in ADT]

SimpleTable.V [axiom, in ADT]

SimpleTable2 [module, in ADT]

SimpleTable3 [module, in ADT]

singleton [definition, in Multiset]

Sin_domain [lemma, in Color]

Snot_in_empty [lemma, in Color]

sort [definition, in Sort]

sort [definition, in Extract]

Sort [library]

sorted [inductive, in Sort]

sorted [inductive, in Selection]

sorted [inductive, in Extract]

Sorted_lt_key [lemma, in Color]

sorted_elements [lemma, in SearchTree]

sorted_app [lemma, in SearchTree]

sorted_sorted' [lemma, in Sort]

sorted_cons [constructor, in Sort]

sorted_1 [constructor, in Sort]

sorted_nil [constructor, in Sort]

sorted_iff_sorted [lemma, in Selection]

sorted_cons [constructor, in Selection]

sorted_1 [constructor, in Selection]

sorted_nil [constructor, in Selection]

sorted_merge [lemma, in Merge]

sorted_merge1 [lemma, in Merge]

sorted_cons [constructor, in Extract]

sorted_1 [constructor, in Extract]

sorted_nil [constructor, in Extract]

sorted' [definition, in Sort]

sorted'_sorted [lemma, in Sort]

sorted'' [definition, in Sort]

SortE_equivlistE_eqlistE [lemma, in Color]

sortZ [definition, in Extract]

sort_sorted' [lemma, in Sort]

sort_perm [lemma, in Sort]

sort_sorted [lemma, in Sort]

sort_pi [definition, in Sort]

sort_specifications_equivalent [lemma, in BagPerm]

sort_bag [lemma, in BagPerm]

sort_pi [definition, in Selection]

sort_specifications_equivalent [lemma, in Multiset]

sort_contents [lemma, in Multiset]

sort_pi_same_contents [definition, in Multiset]

sort_int_correct [lemma, in Extract]

sort_int [definition, in Extract]

sort:38 [binder, in BagPerm]

sort:42 [binder, in Multiset]

specialize_SortA_equivlistA_eqlistA [lemma, in Color]

split [definition, in Merge]

split_perm [lemma, in Merge]

split_len [lemma, in Merge]

split_len' [lemma, in Merge]

split_len_first_try [lemma, in Merge]

Sremove_cardinal_less [lemma, in Color]

Sremove_elements [lemma, in Color]

Sremove_elements [lemma, in Color]

StringListETableAbs [module, in ADT]

StringListsTableExamples [module, in ADT]

StringListsTableExamples.ex1 [definition, in ADT]

StringListsTableExamples.ex2 [definition, in ADT]

StringListsTableExamples.ex3 [definition, in ADT]

StringListsTableExamples.StringListsTable [module, in ADT]

StringTreeETableExample [module, in ADT]

StringTreeETableExample.ex1 [definition, in ADT]

StringTreeETableExample.StringTreeETable [module, in ADT]

StringVal [module, in ADT]

StringVal.default [definition, in ADT]

StringVal.V [definition, in ADT]

ST_T [constructor, in Redblack]

ST_E [constructor, in Redblack]

subset_nodes_sub [lemma, in Color]

subset_nodes [definition, in Color]

s:105 [binder, in Color]

s:107 [binder, in Color]

s:126 [binder, in Color]

s:14 [binder, in Color]

s:18 [binder, in Color]

s:2 [binder, in BagPerm]

s:31 [binder, in Color]

s:4 [binder, in Color]

s:40 [binder, in Color]

s:44 [binder, in Color]

s:68 [binder, in Color]

## T

T [constructor, in Redblack]T [constructor, in SearchTree]

T [constructor, in Extract]

Table [module, in ADT]

Table.default [axiom, in ADT]

Table.empty [axiom, in ADT]

Table.get [axiom, in ADT]

Table.get_set_other [axiom, in ADT]

Table.get_set_same [axiom, in ADT]

Table.get_empty_default [axiom, in ADT]

Table.key [definition, in ADT]

Table.set [axiom, in ADT]

Table.table [axiom, in ADT]

Table.V [axiom, in ADT]

table:3 [binder, in Trie]

table:55 [binder, in Trie]

table:91 [binder, in Trie]

Tests [module, in SearchTree]

Tests.bst_ex

_{4}[definition, in SearchTree]

Tests.bst_ex

_{3}[definition, in SearchTree]

Tests.bst_ex

_{2}[definition, in SearchTree]

Tests.bst_ex

_{1}[definition, in SearchTree]

three_ten [definition, in Trie]

three_less_seven_2 [lemma, in Decide]

three_less_seven_1 [lemma, in Decide]

tl:88 [binder, in Binom]

total_map [definition, in Maps]

tree [inductive, in Redblack]

tree [inductive, in SearchTree]

tree [inductive, in Extract]

TreeETable [module, in ADT]

TreeETableEncapsulated [module, in ADT]

TreeETableEncapsulated.bound [definition, in ADT]

TreeETableEncapsulated.bound_set_other [lemma, in ADT]

TreeETableEncapsulated.bound_set_same [lemma, in ADT]

TreeETableEncapsulated.bound_empty [lemma, in ADT]

TreeETableEncapsulated.elements [definition, in ADT]

TreeETableEncapsulated.elements_correct [lemma, in ADT]

TreeETableEncapsulated.elements_complete [lemma, in ADT]

TreeETableEncapsulated.empty_ok [lemma, in ADT]

TreeETableEncapsulated.rep_ok [definition, in ADT]

TreeETableEncapsulated.set_ok [lemma, in ADT]

TreeETableFullyEncapsulated [module, in ADT]

TreeETableFullyEncapsulated.bound [definition, in ADT]

TreeETableFullyEncapsulated.bound_set_other [lemma, in ADT]

TreeETableFullyEncapsulated.bound_set_same [lemma, in ADT]

TreeETableFullyEncapsulated.bound_empty [lemma, in ADT]

TreeETableFullyEncapsulated.elements [definition, in ADT]

TreeETableFullyEncapsulated.elements_correct [lemma, in ADT]

TreeETableFullyEncapsulated.elements_complete [lemma, in ADT]

TreeETableFullyEncapsulated.empty_ok [lemma, in ADT]

TreeETableFullyEncapsulated.rep_ok [definition, in ADT]

TreeETableFullyEncapsulated.set_ok [lemma, in ADT]

TreeETableSubset [module, in ADT]

TreeETableSubset.bound [definition, in ADT]

TreeETableSubset.bound_set_other [lemma, in ADT]

TreeETableSubset.bound_set_same [lemma, in ADT]

TreeETableSubset.bound_empty [lemma, in ADT]

TreeETableSubset.default [definition, in ADT]

TreeETableSubset.elements [definition, in ADT]

TreeETableSubset.elements_correct [lemma, in ADT]

TreeETableSubset.elements_complete [lemma, in ADT]

TreeETableSubset.empty [definition, in ADT]

TreeETableSubset.get [definition, in ADT]

TreeETableSubset.get_set_other [lemma, in ADT]

TreeETableSubset.get_set_same [lemma, in ADT]

TreeETableSubset.get_empty_default [lemma, in ADT]

TreeETableSubset.key [definition, in ADT]

TreeETableSubset.set [definition, in ADT]

TreeETableSubset.table [definition, in ADT]

TreeETableSubset.V [definition, in ADT]

TreeETable_first_attempt.elements_correct [lemma, in ADT]

TreeETable_first_attempt.elements_complete [lemma, in ADT]

TreeETable_first_attempt.elements [definition, in ADT]

TreeETable_first_attempt.bound [definition, in ADT]

TreeETable_first_attempt [module, in ADT]

TreeETable.bound [definition, in ADT]

TreeETable.bound_set_other [lemma, in ADT]

TreeETable.bound_set_same [lemma, in ADT]

TreeETable.bound_empty [lemma, in ADT]

TreeETable.elements [definition, in ADT]

TreeETable.elements_correct [lemma, in ADT]

TreeETable.elements_complete [lemma, in ADT]

TreeETable.empty_ok [lemma, in ADT]

TreeETable.rep_ok [definition, in ADT]

TreeETable.set_ok [lemma, in ADT]

TreeTable [module, in ADT]

TreeTable.default [definition, in ADT]

TreeTable.empty [definition, in ADT]

TreeTable.get [definition, in ADT]

TreeTable.get_set_other [lemma, in ADT]

TreeTable.get_set_same [lemma, in ADT]

TreeTable.get_empty_default [lemma, in ADT]

TreeTable.key [definition, in ADT]

TreeTable.set [definition, in ADT]

TreeTable.table [definition, in ADT]

TreeTable.V [definition, in ADT]

trie [inductive, in Trie]

Trie [library]

trie_table [definition, in Trie]

truncated_subtraction [lemma, in Perm]

tr:89 [binder, in Binom]

two [definition, in ADT]

two [definition, in ADT]

TwoListQueueAbs [module, in ADT]

TwoListQueueAbs.Abs [definition, in ADT]

TwoListQueueAbs.deq [definition, in ADT]

TwoListQueueAbs.deq_relate [lemma, in ADT]

TwoListQueueAbs.empty [definition, in ADT]

TwoListQueueAbs.empty_relate [lemma, in ADT]

TwoListQueueAbs.enq [definition, in ADT]

TwoListQueueAbs.enq_relate [lemma, in ADT]

TwoListQueueAbs.is_empty [definition, in ADT]

TwoListQueueAbs.peek [definition, in ADT]

TwoListQueueAbs.peek_relate [lemma, in ADT]

TwoListQueueAbs.queue [definition, in ADT]

TwoListQueueAbs.V [definition, in ADT]

two' [definition, in ADT]

t_update_permute [lemma, in Maps]

t_update_same [lemma, in Maps]

t_update_shadow [lemma, in Maps]

t_update_neq [lemma, in Maps]

t_update_eq [lemma, in Maps]

t_apply_empty [lemma, in Maps]

t_update [definition, in Maps]

t_empty [definition, in Maps]

t

_{1}:15 [binder, in Redblack]

t

_{2}:18 [binder, in Redblack]

t:10 [binder, in Redblack]

t:101 [binder, in ADT]

t:102 [binder, in Trie]

t:105 [binder, in ADT]

t:107 [binder, in Binom]

t:107 [binder, in ADT]

t:108 [binder, in Trie]

t:109 [binder, in ADT]

t:11 [binder, in SearchTree]

t:11 [binder, in ADT]

t:110 [binder, in ADT]

t:112 [binder, in Binom]

t:113 [binder, in ADT]

t:114 [binder, in SearchTree]

t:117 [binder, in ADT]

t:118 [binder, in Trie]

t:118 [binder, in Binom]

t:120 [binder, in Trie]

t:121 [binder, in Redblack]

t:121 [binder, in ADT]

t:123 [binder, in Trie]

t:124 [binder, in SearchTree]

t:124 [binder, in ADT]

t:125 [binder, in Redblack]

t:127 [binder, in ADT]

t:128 [binder, in ADT]

t:129 [binder, in Redblack]

t:130 [binder, in Trie]

t:130 [binder, in ADT]

t:131 [binder, in ADT]

t:132 [binder, in SearchTree]

t:134 [binder, in SearchTree]

t:134 [binder, in ADT]

t:135 [binder, in Trie]

t:138 [binder, in ADT]

t:140 [binder, in Trie]

t:140 [binder, in SearchTree]

t:142 [binder, in ADT]

t:145 [binder, in ADT]

t:147 [binder, in Redblack]

t:147 [binder, in SearchTree]

t:148 [binder, in ADT]

t:149 [binder, in SearchTree]

t:152 [binder, in Redblack]

t:153 [binder, in ADT]

t:155 [binder, in ADT]

t:156 [binder, in SearchTree]

t:156 [binder, in ADT]

t:158 [binder, in Redblack]

t:159 [binder, in ADT]

t:16 [binder, in ADT]

t:161 [binder, in SearchTree]

t:163 [binder, in Redblack]

t:163 [binder, in ADT]

t:166 [binder, in SearchTree]

t:167 [binder, in ADT]

t:169 [binder, in Redblack]

t:17 [binder, in SearchTree]

t:170 [binder, in ADT]

t:173 [binder, in ADT]

t:176 [binder, in SearchTree]

t:177 [binder, in Redblack]

t:181 [binder, in SearchTree]

t:182 [binder, in Redblack]

t:187 [binder, in SearchTree]

t:190 [binder, in SearchTree]

t:193 [binder, in ADT]

t:195 [binder, in SearchTree]

t:196 [binder, in ADT]

t:199 [binder, in ADT]

t:202 [binder, in Redblack]

t:202 [binder, in ADT]

t:205 [binder, in SearchTree]

t:206 [binder, in ADT]

t:209 [binder, in ADT]

t:21 [binder, in ADT]

t:213 [binder, in ADT]

t:214 [binder, in SearchTree]

t:215 [binder, in ADT]

t:216 [binder, in SearchTree]

t:217 [binder, in ADT]

t:218 [binder, in ADT]

t:219 [binder, in ADT]

t:220 [binder, in Redblack]

t:221 [binder, in SearchTree]

t:222 [binder, in ADT]

t:223 [binder, in Redblack]

t:223 [binder, in SearchTree]

t:223 [binder, in ADT]

t:225 [binder, in ADT]

t:226 [binder, in SearchTree]

t:227 [binder, in ADT]

t:228 [binder, in Redblack]

t:23 [binder, in SearchTree]

t:23 [binder, in Binom]

t:230 [binder, in ADT]

t:231 [binder, in SearchTree]

t:232 [binder, in Redblack]

t:238 [binder, in Redblack]

t:24 [binder, in ADT]

t:241 [binder, in Redblack]

t:244 [binder, in Redblack]

t:25 [binder, in Redblack]

t:251 [binder, in SearchTree]

t:259 [binder, in SearchTree]

t:28 [binder, in SearchTree]

t:28 [binder, in Binom]

t:281 [binder, in SearchTree]

t:284 [binder, in SearchTree]

t:288 [binder, in SearchTree]

t:29 [binder, in Redblack]

t:29 [binder, in ADT]

t:292 [binder, in SearchTree]

t:3 [binder, in Binom]

t:322 [binder, in SearchTree]

t:327 [binder, in SearchTree]

t:33 [binder, in ADT]

t:331 [binder, in SearchTree]

t:334 [binder, in SearchTree]

t:338 [binder, in SearchTree]

t:34 [binder, in Redblack]

t:343 [binder, in SearchTree]

t:348 [binder, in SearchTree]

t:35 [binder, in ADT]

t:36 [binder, in Redblack]

t:362 [binder, in ADT]

t:367 [binder, in ADT]

t:371 [binder, in ADT]

t:375 [binder, in ADT]

t:377 [binder, in ADT]

t:379 [binder, in ADT]

t:382 [binder, in ADT]

t:384 [binder, in ADT]

t:385 [binder, in ADT]

t:389 [binder, in ADT]

t:39 [binder, in ADT]

t:393 [binder, in ADT]

t:397 [binder, in ADT]

t:401 [binder, in ADT]

t:404 [binder, in ADT]

t:407 [binder, in ADT]

t:41 [binder, in Redblack]

t:43 [binder, in SearchTree]

t:43 [binder, in Perm]

t:43 [binder, in ADT]

t:45 [binder, in Redblack]

t:47 [binder, in ADT]

t:49 [binder, in Redblack]

t:49 [binder, in SearchTree]

t:49 [binder, in ADT]

t:52 [binder, in Redblack]

t:52 [binder, in ADT]

t:53 [binder, in Binom]

t:54 [binder, in SearchTree]

t:56 [binder, in ADT]

t:59 [binder, in SearchTree]

t:59 [binder, in Binom]

t:60 [binder, in ADT]

t:63 [binder, in Extract]

t:64 [binder, in SearchTree]

t:65 [binder, in ADT]

t:67 [binder, in Redblack]

t:67 [binder, in Binom]

t:69 [binder, in ADT]

t:69 [binder, in Extract]

t:71 [binder, in Binom]

t:72 [binder, in SearchTree]

t:72 [binder, in ADT]

t:73 [binder, in ADT]

t:73 [binder, in Extract]

t:74 [binder, in Trie]

t:76 [binder, in ADT]

t:78 [binder, in Extract]

t:79 [binder, in ADT]

t:8 [binder, in Binom]

t:80 [binder, in SearchTree]

t:84 [binder, in Extract]

t:86 [binder, in ADT]

t:87 [binder, in Trie]

t:89 [binder, in Redblack]

t:89 [binder, in SearchTree]

t:89 [binder, in Extract]

t:92 [binder, in ADT]

t:93 [binder, in Redblack]

t:95 [binder, in Binom]

t:97 [binder, in ADT]

t:98 [binder, in Binom]

t:99 [binder, in Redblack]

## U

uncurry [definition, in SearchTree]undirected [definition, in Color]

union [definition, in SearchTree]

union [definition, in Multiset]

union_update_left [lemma, in SearchTree]

union_update_right [lemma, in SearchTree]

union_both [lemma, in SearchTree]

union_right [lemma, in SearchTree]

union_left [lemma, in SearchTree]

union_swap [lemma, in Multiset]

union_comm [lemma, in Multiset]

union_assoc [lemma, in Multiset]

Unnamed_thm [definition, in Trie]

Unnamed_thm0 [definition, in Color]

Unnamed_thm [definition, in Color]

Unnamed_thm [definition, in Decide]

update [definition, in Maps]

update_permute [lemma, in Maps]

update_same [lemma, in Maps]

update_shadow [lemma, in Maps]

update_neq [lemma, in Maps]

update_eq [lemma, in Maps]

update_example4 [definition, in Maps]

update_example3 [definition, in Maps]

update_example2 [definition, in Maps]

update_example1 [definition, in Maps]

u:113 [binder, in Binom]

u:30 [binder, in Binom]

u:4 [binder, in Binom]

u:42 [binder, in Perm]

u:68 [binder, in Binom]

## V

ValType [module, in ADT]ValType.default [axiom, in ADT]

ValType.V [axiom, in ADT]

value [definition, in Multiset]

vector [definition, in ADT]

vector_app_correct [lemma, in ADT]

vector_app [definition, in ADT]

vector_cons_correct [lemma, in ADT]

vector_cons [definition, in ADT]

VerySlow [module, in Trie]

VerySlow.collisions [definition, in Trie]

VerySlow.collisions_pi [definition, in Trie]

VerySlow.loop [definition, in Trie]

vk:17 [binder, in Redblack]

vx:24 [binder, in Redblack]

vx:33 [binder, in Redblack]

vx:44 [binder, in Redblack]

vx:48 [binder, in Redblack]

v':116 [binder, in SearchTree]

v':137 [binder, in SearchTree]

v

_{0}:241 [binder, in SearchTree]

v

_{1}:101 [binder, in SearchTree]

v

_{1}:108 [binder, in SearchTree]

v

_{1}:126 [binder, in SearchTree]

v

_{1}:143 [binder, in SearchTree]

v

_{1}:23 [binder, in Maps]

v

_{1}:30 [binder, in Maps]

v

_{1}:309 [binder, in SearchTree]

v

_{1}:351 [binder, in ADT]

v

_{1}:354 [binder, in ADT]

v

_{1}:54 [binder, in Maps]

v

_{1}:62 [binder, in Maps]

v

_{2}:102 [binder, in SearchTree]

v

_{2}:109 [binder, in SearchTree]

v

_{2}:127 [binder, in SearchTree]

v

_{2}:144 [binder, in SearchTree]

v

_{2}:24 [binder, in Maps]

v

_{2}:31 [binder, in Maps]

v

_{2}:310 [binder, in SearchTree]

v

_{2}:352 [binder, in ADT]

v

_{2}:355 [binder, in ADT]

v

_{2}:55 [binder, in Maps]

v

_{2}:63 [binder, in Maps]

V:1 [binder, in SearchTree]

v:1 [binder, in BagPerm]

v:10 [binder, in ADT]

v:100 [binder, in ADT]

v:101 [binder, in Trie]

V:104 [binder, in Redblack]

V:104 [binder, in SearchTree]

v:104 [binder, in ADT]

v:107 [binder, in Trie]

V:107 [binder, in SearchTree]

v:108 [binder, in Redblack]

v:11 [binder, in Maps]

V:112 [binder, in Redblack]

v:112 [binder, in ADT]

V:113 [binder, in SearchTree]

v:115 [binder, in SearchTree]

v:116 [binder, in ADT]

v:118 [binder, in Redblack]

V:119 [binder, in Redblack]

V:120 [binder, in SearchTree]

v:120 [binder, in ADT]

v:123 [binder, in Redblack]

v:123 [binder, in ADT]

V:124 [binder, in Redblack]

V:125 [binder, in SearchTree]

v:126 [binder, in ADT]

v:127 [binder, in Redblack]

V:128 [binder, in Redblack]

V:13 [binder, in Redblack]

v:130 [binder, in Redblack]

V:132 [binder, in Redblack]

V:133 [binder, in SearchTree]

v:133 [binder, in ADT]

V:135 [binder, in Redblack]

v:136 [binder, in SearchTree]

v:137 [binder, in ADT]

V:138 [binder, in SearchTree]

v:139 [binder, in Trie]

V:14 [binder, in SearchTree]

v:140 [binder, in Redblack]

v:141 [binder, in ADT]

V:142 [binder, in SearchTree]

v:144 [binder, in ADT]

V:145 [binder, in Redblack]

v:147 [binder, in ADT]

V:148 [binder, in SearchTree]

v:149 [binder, in Redblack]

v:15 [binder, in ADT]

v:15 [binder, in Maps]

V:150 [binder, in Redblack]

V:152 [binder, in SearchTree]

v:154 [binder, in SearchTree]

v:155 [binder, in Redblack]

V:156 [binder, in Redblack]

V:157 [binder, in SearchTree]

v:158 [binder, in ADT]

v:159 [binder, in SearchTree]

v:160 [binder, in Redblack]

V:161 [binder, in Redblack]

V:162 [binder, in SearchTree]

v:162 [binder, in ADT]

v:164 [binder, in SearchTree]

v:166 [binder, in Redblack]

v:166 [binder, in ADT]

V:167 [binder, in Redblack]

V:168 [binder, in Redblack]

v:169 [binder, in ADT]

v:17 [binder, in Maps]

v:170 [binder, in Redblack]

V:172 [binder, in Redblack]

v:172 [binder, in ADT]

V:174 [binder, in SearchTree]

V:174 [binder, in ADT]

V:175 [binder, in Redblack]

v:176 [binder, in ADT]

V:177 [binder, in SearchTree]

V:178 [binder, in ADT]

v:179 [binder, in Redblack]

V:179 [binder, in ADT]

V:180 [binder, in Redblack]

v:180 [binder, in SearchTree]

V:184 [binder, in SearchTree]

v:185 [binder, in Redblack]

V:186 [binder, in Redblack]

v:186 [binder, in SearchTree]

V:188 [binder, in SearchTree]

v:191 [binder, in SearchTree]

v:192 [binder, in ADT]

v:193 [binder, in Redblack]

V:193 [binder, in SearchTree]

v:196 [binder, in SearchTree]

v:199 [binder, in Redblack]

v:2 [binder, in Multiset]

V:20 [binder, in SearchTree]

V:201 [binder, in Redblack]

V:202 [binder, in SearchTree]

V:204 [binder, in Redblack]

V:204 [binder, in SearchTree]

v:204 [binder, in ADT]

v:210 [binder, in Redblack]

v:212 [binder, in ADT]

V:213 [binder, in SearchTree]

v:215 [binder, in Redblack]

V:215 [binder, in SearchTree]

V:217 [binder, in Redblack]

v:219 [binder, in Redblack]

V:22 [binder, in Redblack]

v:22 [binder, in SearchTree]

V:220 [binder, in SearchTree]

v:221 [binder, in ADT]

V:222 [binder, in Redblack]

V:222 [binder, in SearchTree]

v:225 [binder, in Redblack]

V:225 [binder, in SearchTree]

V:227 [binder, in Redblack]

V:227 [binder, in SearchTree]

v:229 [binder, in SearchTree]

v:229 [binder, in ADT]

v:23 [binder, in ADT]

V:231 [binder, in Redblack]

V:232 [binder, in SearchTree]

V:233 [binder, in SearchTree]

v:234 [binder, in Redblack]

v:235 [binder, in SearchTree]

V:237 [binder, in Redblack]

V:239 [binder, in SearchTree]

V:240 [binder, in Redblack]

v:240 [binder, in SearchTree]

v:240 [binder, in ADT]

V:243 [binder, in Redblack]

v:246 [binder, in ADT]

V:250 [binder, in SearchTree]

v:250 [binder, in ADT]

v:253 [binder, in SearchTree]

V:254 [binder, in SearchTree]

v:254 [binder, in ADT]

V:258 [binder, in SearchTree]

v:259 [binder, in ADT]

V:26 [binder, in SearchTree]

V:260 [binder, in SearchTree]

v:263 [binder, in ADT]

V:264 [binder, in SearchTree]

v:265 [binder, in ADT]

V:272 [binder, in SearchTree]

v:275 [binder, in SearchTree]

V:276 [binder, in SearchTree]

v:276 [binder, in ADT]

V:279 [binder, in SearchTree]

V:28 [binder, in Redblack]

v:28 [binder, in ADT]

V:280 [binder, in SearchTree]

V:283 [binder, in SearchTree]

V:287 [binder, in SearchTree]

v:290 [binder, in SearchTree]

V:291 [binder, in SearchTree]

v:291 [binder, in ADT]

v:298 [binder, in ADT]

V:3 [binder, in Redblack]

v:3 [binder, in Maps]

V:31 [binder, in Redblack]

V:31 [binder, in SearchTree]

v:315 [binder, in SearchTree]

v:32 [binder, in ADT]

v:320 [binder, in SearchTree]

V:321 [binder, in SearchTree]

V:325 [binder, in SearchTree]

v:329 [binder, in SearchTree]

V:330 [binder, in SearchTree]

V:332 [binder, in SearchTree]

V:333 [binder, in SearchTree]

V:336 [binder, in SearchTree]

V:340 [binder, in SearchTree]

v:342 [binder, in SearchTree]

V:344 [binder, in SearchTree]

v:344 [binder, in ADT]

v:346 [binder, in ADT]

V:347 [binder, in SearchTree]

v:349 [binder, in ADT]

V:35 [binder, in Redblack]

v:36 [binder, in SearchTree]

v:361 [binder, in ADT]

v:366 [binder, in ADT]

v:370 [binder, in ADT]

v:374 [binder, in ADT]

v:38 [binder, in ADT]

v:381 [binder, in ADT]

v:388 [binder, in ADT]

v:392 [binder, in ADT]

v:396 [binder, in ADT]

V:40 [binder, in Redblack]

V:40 [binder, in SearchTree]

v:40 [binder, in Maps]

v:400 [binder, in ADT]

v:403 [binder, in ADT]

v:406 [binder, in ADT]

V:41 [binder, in SearchTree]

V:42 [binder, in Redblack]

v:42 [binder, in ADT]

v:45 [binder, in SearchTree]

V:46 [binder, in Redblack]

V:46 [binder, in SearchTree]

v:46 [binder, in ADT]

v:46 [binder, in Maps]

v:48 [binder, in SearchTree]

v:48 [binder, in Maps]

V:50 [binder, in Redblack]

V:50 [binder, in SearchTree]

v:51 [binder, in Trie]

v:51 [binder, in ADT]

V:53 [binder, in SearchTree]

V:55 [binder, in Redblack]

v:55 [binder, in ADT]

V:56 [binder, in Extract]

v:57 [binder, in SearchTree]

V:58 [binder, in SearchTree]

v:58 [binder, in Maps]

v:59 [binder, in ADT]

V:59 [binder, in Extract]

V:6 [binder, in Redblack]

v:6 [binder, in SearchTree]

V:60 [binder, in Extract]

v:61 [binder, in Redblack]

v:62 [binder, in SearchTree]

V:63 [binder, in SearchTree]

v:64 [binder, in ADT]

V:65 [binder, in Redblack]

V:66 [binder, in Redblack]

V:66 [binder, in Extract]

v:68 [binder, in Redblack]

v:68 [binder, in SearchTree]

v:68 [binder, in ADT]

v:68 [binder, in Extract]

V:69 [binder, in SearchTree]

V:7 [binder, in Redblack]

v:7 [binder, in Maps]

V:70 [binder, in Redblack]

V:72 [binder, in Extract]

V:73 [binder, in SearchTree]

v:74 [binder, in Redblack]

v:75 [binder, in ADT]

V:76 [binder, in SearchTree]

V:77 [binder, in Extract]

V:78 [binder, in Redblack]

v:78 [binder, in ADT]

V:79 [binder, in SearchTree]

V:79 [binder, in Extract]

V:8 [binder, in SearchTree]

v:82 [binder, in Redblack]

V:82 [binder, in Extract]

v:83 [binder, in SearchTree]

V:84 [binder, in SearchTree]

v:85 [binder, in ADT]

V:86 [binder, in Redblack]

v:86 [binder, in Extract]

v:87 [binder, in SearchTree]

v:87 [binder, in Binom]

V:87 [binder, in Extract]

V:88 [binder, in SearchTree]

V:9 [binder, in SearchTree]

v:91 [binder, in Redblack]

v:91 [binder, in ADT]

V:92 [binder, in Redblack]

v:92 [binder, in Extract]

v:93 [binder, in SearchTree]

V:94 [binder, in SearchTree]

v:95 [binder, in SearchTree]

v:96 [binder, in ADT]

V:98 [binder, in Redblack]

V:99 [binder, in SearchTree]

## W

WF [module, in Color]WP [module, in Color]

## X

xs:340 [binder, in ADT]xs:54 [binder, in Selection]

x':52 [binder, in Trie]

x':8 [binder, in Maps]

x

_{1}:18 [binder, in Maps]

x

_{1}:32 [binder, in Maps]

x

_{1}:49 [binder, in Maps]

x

_{1}:57 [binder, in Merge]

x

_{1}:64 [binder, in Maps]

x

_{1}:95 [binder, in Merge]

x

_{2}:19 [binder, in Maps]

x

_{2}:33 [binder, in Maps]

x

_{2}:50 [binder, in Maps]

x

_{2}:58 [binder, in Merge]

x

_{2}:65 [binder, in Maps]

x

_{2}:97 [binder, in Merge]

x:1 [binder, in Selection]

x:1 [binder, in Multiset]

X:1 [binder, in Merge]

x:10 [binder, in SearchTree]

x:10 [binder, in Sort]

x:10 [binder, in Maps]

x:11 [binder, in Sort]

x:110 [binder, in Selection]

x:12 [binder, in Binom]

x:129 [binder, in Trie]

x:14 [binder, in BagPerm]

x:14 [binder, in Binom]

x:14 [binder, in Maps]

x:15 [binder, in Trie]

x:15 [binder, in Color]

x:16 [binder, in SearchTree]

X:16 [binder, in Maps]

X:167 [binder, in SearchTree]

x:17 [binder, in Decide]

X:18 [binder, in Merge]

x:19 [binder, in Trie]

x:19 [binder, in Color]

x:19 [binder, in BagPerm]

x:199 [binder, in SearchTree]

x:20 [binder, in Perm]

x:20 [binder, in Multiset]

X:206 [binder, in SearchTree]

x:209 [binder, in SearchTree]

x:21 [binder, in SearchTree]

X:210 [binder, in SearchTree]

x:23 [binder, in Redblack]

x:25 [binder, in Trie]

x:25 [binder, in Maps]

x:26 [binder, in BagPerm]

x:26 [binder, in Decide]

x:26 [binder, in Multiset]

X:26 [binder, in Maps]

X:267 [binder, in SearchTree]

x:27 [binder, in Perm]

x:27 [binder, in Decide]

x:27 [binder, in Maps]

x:270 [binder, in SearchTree]

x:28 [binder, in Multiset]

x:28 [binder, in Extract]

x:29 [binder, in Sort]

x:29 [binder, in Perm]

X:29 [binder, in Maps]

X:293 [binder, in SearchTree]

X:297 [binder, in SearchTree]

x:3 [binder, in Multiset]

x:30 [binder, in Extract]

X:301 [binder, in SearchTree]

x:302 [binder, in ADT]

X:305 [binder, in SearchTree]

x:305 [binder, in ADT]

x:306 [binder, in ADT]

x:309 [binder, in ADT]

x:31 [binder, in Perm]

X:311 [binder, in SearchTree]

x:313 [binder, in ADT]

X:316 [binder, in SearchTree]

x:319 [binder, in ADT]

x:32 [binder, in Redblack]

x:32 [binder, in BagPerm]

x:32 [binder, in Selection]

x:32 [binder, in Extract]

x:320 [binder, in ADT]

x:325 [binder, in ADT]

x:33 [binder, in Perm]

X:338 [binder, in ADT]

x:34 [binder, in Multiset]

x:34 [binder, in Extract]

X:342 [binder, in ADT]

x:343 [binder, in ADT]

X:345 [binder, in ADT]

X:347 [binder, in ADT]

x:348 [binder, in ADT]

x:35 [binder, in Trie]

x:35 [binder, in SearchTree]

x:35 [binder, in Perm]

X:350 [binder, in ADT]

X:353 [binder, in ADT]

x:36 [binder, in Color]

x:36 [binder, in Extract]

x:38 [binder, in Selection]

x:38 [binder, in Multiset]

x:38 [binder, in Extract]

x:39 [binder, in Multiset]

x:39 [binder, in Maps]

x:40 [binder, in Extract]

x:41 [binder, in Trie]

x:41 [binder, in Color]

X:41 [binder, in Merge]

x:42 [binder, in Selection]

x:42 [binder, in Maps]

x:43 [binder, in Redblack]

X:45 [binder, in Merge]

x:45 [binder, in Maps]

x:47 [binder, in Redblack]

X:47 [binder, in Maps]

x:50 [binder, in Trie]

x:50 [binder, in Color]

x:51 [binder, in Selection]

x:51 [binder, in Extract]

x:52 [binder, in Extract]

x:53 [binder, in Selection]

x:56 [binder, in Maps]

X:57 [binder, in Maps]

x:59 [binder, in Maps]

x:6 [binder, in Multiset]

x:6 [binder, in Maps]

x:61 [binder, in Priqueue]

x:61 [binder, in Selection]

X:61 [binder, in Maps]

x:62 [binder, in Extract]

x:65 [binder, in Selection]

x:66 [binder, in Priqueue]

x:67 [binder, in Extract]

X:7 [binder, in Merge]

x:72 [binder, in Binom]

x:9 [binder, in Redblack]

x:94 [binder, in Merge]

## Y

y:105 [binder, in Selection]y:111 [binder, in Selection]

y:12 [binder, in Sort]

y:12 [binder, in Selection]

Y:168 [binder, in SearchTree]

y:183 [binder, in SearchTree]

y:19 [binder, in Selection]

y:20 [binder, in Trie]

y:21 [binder, in Perm]

y:26 [binder, in Trie]

Y:268 [binder, in SearchTree]

y:271 [binder, in SearchTree]

y:28 [binder, in Perm]

y:28 [binder, in Decide]

y:29 [binder, in Extract]

y:30 [binder, in Perm]

y:31 [binder, in Extract]

y:32 [binder, in Perm]

y:33 [binder, in BagPerm]

y:33 [binder, in Extract]

y:34 [binder, in Perm]

y:35 [binder, in Multiset]

y:35 [binder, in Extract]

y:36 [binder, in Trie]

y:36 [binder, in Perm]

y:37 [binder, in Color]

y:37 [binder, in Extract]

y:38 [binder, in SearchTree]

y:39 [binder, in SearchTree]

y:39 [binder, in Extract]

y:40 [binder, in Selection]

y:41 [binder, in Extract]

y:42 [binder, in Trie]

y:44 [binder, in Selection]

y:48 [binder, in Perm]

y:51 [binder, in Color]

y:52 [binder, in Selection]

y:53 [binder, in Extract]

y:55 [binder, in Selection]

y:57 [binder, in Selection]

y:62 [binder, in Selection]

y:66 [binder, in Selection]

y:68 [binder, in Selection]

y:76 [binder, in Selection]

y:83 [binder, in Selection]

y:88 [binder, in Selection]

## Z

Z_geb_reflect [lemma, in Extract]Z_gtb_reflect [lemma, in Extract]

Z_leb_reflect [lemma, in Extract]

Z_ltb_reflect [lemma, in Extract]

Z_eqb_reflect [lemma, in Extract]

Z:169 [binder, in SearchTree]

## other

_ >? _ (nat_scope) [notation, in Perm]_ >=? _ (nat_scope) [notation, in Perm]

_ <=* _ [notation, in Selection]

# Notation Index

## I

_ ~ 0 [in Trie]_ ~ 1 [in Trie]

## S

{ _ } + { _ } (type_scope) [in Decide]{ _ : _ | _ } [in ADT]

## other

_ >? _ (nat_scope) [in Perm]_ >=? _ (nat_scope) [in Perm]

_ <=* _ [in Selection]

# Binder Index

## A

acc:217 [in SearchTree]acc:37 [in Redblack]

acc:74 [in Extract]

adj:67 [in Color]

adj:71 [in Color]

al:102 [in Priqueue]

al:105 [in Binom]

al:107 [in Selection]

al:108 [in Binom]

al:108 [in Selection]

al:110 [in Binom]

al:12 [in Priqueue]

al:122 [in Binom]

al:135 [in Binom]

al:15 [in Multiset]

al:16 [in Sort]

al:18 [in BagPerm]

al:19 [in Sort]

al:19 [in Multiset]

al:21 [in Priqueue]

al:22 [in BagPerm]

al:22 [in Perm]

al:23 [in Multiset]

al:24 [in Perm]

al:25 [in Color]

al:25 [in Sort]

al:29 [in Selection]

al:32 [in Sort]

al:33 [in Color]

al:33 [in Sort]

al:34 [in BagPerm]

al:36 [in BagPerm]

al:36 [in Multiset]

al:40 [in Perm]

al:40 [in Decide]

al:40 [in Multiset]

al:43 [in Priqueue]

al:43 [in Decide]

al:49 [in Selection]

al:51 [in Perm]

al:52 [in Perm]

al:54 [in Perm]

al:55 [in Extract]

al:57 [in Perm]

al:58 [in Priqueue]

al:59 [in Selection]

al:63 [in Priqueue]

al:63 [in Selection]

al:7 [in Color]

al:71 [in Selection]

al:72 [in Selection]

al:78 [in Priqueue]

al:80 [in Priqueue]

al:85 [in Priqueue]

al:9 [in Priqueue]

al:9 [in Color]

al:94 [in Binom]

A:1 [in Color]

A:1 [in Decide]

A:1 [in Maps]

a:10 [in Multiset]

A:103 [in Trie]

a:104 [in Trie]

a:11 [in Decide]

A:11 [in Merge]

A:117 [in Trie]

A:119 [in Trie]

a:12 [in Multiset]

A:12 [in Maps]

A:122 [in Trie]

A:125 [in Trie]

A:127 [in Trie]

a:13 [in Decide]

a:13 [in Merge]

A:131 [in Trie]

A:133 [in Trie]

A:137 [in Trie]

A:14 [in Sort]

a:14 [in Merge]

A:15 [in Sort]

a:15 [in Decide]

a:172 [in SearchTree]

a:18 [in Perm]

A:2 [in Maps]

A:20 [in Color]

A:21 [in Maps]

A:22 [in Merge]

A:24 [in Color]

a:24 [in Merge]

a:25 [in Merge]

A:26 [in Color]

a:26 [in Sort]

A:29 [in Merge]

a:30 [in Decide]

a:30 [in Selection]

A:303 [in ADT]

A:307 [in ADT]

A:311 [in ADT]

A:315 [in ADT]

A:32 [in Color]

a:32 [in Merge]

A:321 [in ADT]

A:326 [in ADT]

A:330 [in ADT]

A:334 [in ADT]

a:34 [in Merge]

A:35 [in Color]

a:35 [in Sort]

A:35 [in Maps]

A:36 [in Maps]

a:37 [in Perm]

A:37 [in Maps]

A:38 [in Color]

a:38 [in Perm]

a:39 [in Sort]

a:39 [in Perm]

a:4 [in Multiset]

A:4 [in Maps]

A:41 [in Maps]

A:42 [in Color]

A:43 [in Maps]

A:45 [in Trie]

A:45 [in Color]

A:46 [in Trie]

A:48 [in Trie]

a:49 [in Perm]

a:5 [in Decide]

A:52 [in Maps]

A:53 [in Color]

A:55 [in Perm]

A:59 [in Trie]

A:62 [in Trie]

A:63 [in Trie]

A:65 [in Trie]

a:7 [in Decide]

a:7 [in Multiset]

A:72 [in Trie]

A:75 [in Trie]

a:78 [in Trie]

A:84 [in Trie]

a:86 [in Trie]

a:9 [in Decide]

A:9 [in Maps]

A:95 [in Trie]

a:96 [in Trie]

A:98 [in Trie]

a:99 [in Trie]

## B

bl:10 [in Color]bl:104 [in Selection]

bl:106 [in Binom]

bl:109 [in Selection]

bl:13 [in Priqueue]

bl:23 [in BagPerm]

bl:24 [in Multiset]

bl:34 [in Color]

bl:35 [in BagPerm]

bl:37 [in BagPerm]

bl:37 [in Multiset]

bl:41 [in Decide]

bl:41 [in Multiset]

bl:50 [in Selection]

bl:58 [in Perm]

bl:60 [in Priqueue]

bl:60 [in Selection]

bl:64 [in Selection]

bl:65 [in Priqueue]

bl:67 [in Selection]

bl:8 [in Color]

bl:81 [in Priqueue]

bl:85 [in Binom]

br:86 [in Binom]

bt:114 [in Binom]

bu:115 [in Binom]

b

_{1}:11 [in BagPerm]

b

_{1}:15 [in BagPerm]

b

_{1}:5 [in BagPerm]

b

_{1}:9 [in BagPerm]

b

_{2}:10 [in BagPerm]

b

_{2}:12 [in BagPerm]

b

_{2}:16 [in BagPerm]

b

_{2}:6 [in BagPerm]

b

_{3}:13 [in BagPerm]

b:10 [in Decide]

b:11 [in Multiset]

b:12 [in Decide]

b:13 [in Multiset]

b:14 [in Decide]

b:15 [in Merge]

b:16 [in Decide]

b:171 [in SearchTree]

b:19 [in Perm]

B:2 [in Decide]

b:24 [in BagPerm]

b:26 [in Perm]

b:26 [in Merge]

B:27 [in Color]

b:283 [in ADT]

b:288 [in ADT]

b:33 [in Selection]

b:35 [in Merge]

b:41 [in Perm]

B:46 [in Color]

b:5 [in Multiset]

b:50 [in Perm]

b:6 [in Decide]

b:8 [in BagPerm]

b:8 [in Decide]

b:8 [in Multiset]

b:90 [in Binom]

## C

carry:18 [in Trie]ce:130 [in Binom]

ci:119 [in Color]

ci:120 [in Color]

cj:121 [in Color]

cont:24 [in Binom]

cts:141 [in Trie]

current:31 [in Binom]

c:105 [in Redblack]

c:114 [in Redblack]

c:126 [in Binom]

c:128 [in Color]

c:137 [in Redblack]

c:14 [in Redblack]

c:14 [in Multiset]

c:18 [in Binom]

c:189 [in Redblack]

c:195 [in Redblack]

c:2 [in Trie]

c:245 [in Redblack]

c:28 [in Trie]

c:31 [in Selection]

c:36 [in Selection]

c:54 [in Trie]

c:58 [in Redblack]

c:71 [in Redblack]

c:76 [in Binom]

c:79 [in Redblack]

c:9 [in Multiset]

c:90 [in Trie]

## D

default:126 [in Trie]default:132 [in Trie]

default:256 [in ADT]

default:47 [in Trie]

default:61 [in Extract]

default:64 [in Trie]

default:66 [in Trie]

default:76 [in Trie]

default:80 [in Extract]

default:83 [in Extract]

default:88 [in Extract]

d:117 [in SearchTree]

d:123 [in SearchTree]

d:128 [in SearchTree]

d:133 [in Redblack]

d:136 [in Redblack]

d:139 [in SearchTree]

d:146 [in Redblack]

d:15 [in SearchTree]

d:151 [in Redblack]

d:155 [in SearchTree]

d:157 [in Redblack]

d:160 [in SearchTree]

d:162 [in Redblack]

d:165 [in SearchTree]

d:173 [in Redblack]

d:176 [in Redblack]

d:181 [in Redblack]

d:192 [in SearchTree]

d:230 [in SearchTree]

d:242 [in ADT]

d:244 [in ADT]

d:260 [in ADT]

d:261 [in SearchTree]

d:261 [in ADT]

d:278 [in ADT]

d:285 [in SearchTree]

d:294 [in ADT]

d:299 [in ADT]

d:337 [in SearchTree]

d:34 [in Selection]

d:37 [in Selection]

d:51 [in SearchTree]

d:55 [in SearchTree]

d:60 [in SearchTree]

d:65 [in SearchTree]

d:71 [in SearchTree]

d:74 [in SearchTree]

d:78 [in SearchTree]

d:8 [in Redblack]

d:81 [in SearchTree]

d:90 [in SearchTree]

## E

el_{1}:345 [in SearchTree]

el

_{2}:346 [in SearchTree]

el:133 [in Color]

el:255 [in SearchTree]

el:273 [in SearchTree]

el:277 [in SearchTree]

eq:119 [in Binom]

et:120 [in Binom]

e

_{1}:102 [in Binom]

e

_{1}:242 [in SearchTree]

e

_{1}:96 [in Binom]

e

_{1}:99 [in Binom]

e

_{2}:100 [in Binom]

e

_{2}:103 [in Binom]

e

_{2}:243 [in SearchTree]

e

_{2}:97 [in Binom]

e:131 [in Color]

e:23 [in Color]

e:310 [in ADT]

e:314 [in ADT]

e:328 [in ADT]

e:332 [in ADT]

e:336 [in ADT]

e:44 [in Perm]

## F

f:104 [in Color]f:11 [in Color]

f:111 [in Color]

f:116 [in Color]

f:127 [in Color]

f:16 [in Color]

f:17 [in BagPerm]

f:17 [in Perm]

f:170 [in SearchTree]

f:18 [in Multiset]

f:24 [in Sort]

f:28 [in Color]

f:28 [in Selection]

f:284 [in ADT]

f:289 [in ADT]

f:46 [in Perm]

f:47 [in Color]

f:56 [in Perm]

## G

g:109 [in Color]g:113 [in Color]

g:115 [in Color]

g:122 [in Color]

g:130 [in Color]

g:132 [in Color]

g:29 [in Color]

g:55 [in Color]

g:56 [in Color]

g:58 [in Color]

g:61 [in Color]

g:63 [in Color]

g:65 [in Color]

g:73 [in Color]

g:75 [in Color]

g:77 [in Color]

g:80 [in Color]

g:83 [in Color]

g:85 [in Color]

g:88 [in Color]

g:90 [in Color]

g:92 [in Color]

## H

H_{0}:33 [in Merge]

H

_{1}:37 [in Merge]

H:31 [in Merge]

## I

input:1 [in Trie]input:53 [in Trie]

input:58 [in Trie]

input:6 [in Trie]

input:89 [in Trie]

input:94 [in Trie]

iv:22 [in Sort]

iv:37 [in Sort]

i':38 [in Sort]

i:1 [in Sort]

i:1 [in Extract]

i:11 [in Perm]

i:112 [in Trie]

i:115 [in Trie]

i:117 [in Color]

i:123 [in Color]

i:125 [in Color]

i:128 [in Trie]

i:13 [in Color]

i:134 [in Trie]

i:14 [in Perm]

i:17 [in Color]

i:17 [in Sort]

i:20 [in Sort]

i:24 [in Selection]

i:25 [in Selection]

i:30 [in Color]

i:32 [in Decide]

i:35 [in Decide]

i:36 [in Sort]

i:38 [in Decide]

i:39 [in Color]

i:42 [in Decide]

i:42 [in Extract]

i:43 [in Color]

i:45 [in Priqueue]

i:49 [in Color]

i:5 [in Color]

i:53 [in Priqueue]

i:57 [in Priqueue]

i:57 [in Color]

i:59 [in Color]

i:61 [in Binom]

i:62 [in Priqueue]

i:62 [in Color]

i:67 [in Trie]

i:7 [in Perm]

i:73 [in Trie]

i:77 [in Trie]

i:8 [in Extract]

i:85 [in Trie]

i:88 [in Trie]

## J

jv:23 [in Sort]j:105 [in Trie]

j:116 [in Trie]

j:118 [in Color]

j:12 [in Perm]

j:124 [in Color]

j:15 [in Perm]

j:18 [in Sort]

j:21 [in Color]

j:21 [in Sort]

j:26 [in Selection]

j:33 [in Decide]

j:36 [in Decide]

j:39 [in Decide]

j:42 [in Binom]

j:44 [in Binom]

j:49 [in Priqueue]

j:5 [in Selection]

j:51 [in Priqueue]

j:55 [in Priqueue]

j:59 [in Priqueue]

j:6 [in Color]

j:60 [in Color]

j:64 [in Priqueue]

j:7 [in Selection]

j:8 [in Perm]

j:97 [in Trie]

## K

kvs:236 [in SearchTree]k':102 [in Redblack]

k':103 [in Redblack]

k':110 [in Redblack]

k':111 [in Redblack]

k':119 [in SearchTree]

k':119 [in ADT]

k':122 [in SearchTree]

k':131 [in SearchTree]

k':139 [in Redblack]

k':14 [in ADT]

k':140 [in ADT]

k':143 [in Redblack]

k':144 [in Redblack]

k':154 [in Redblack]

k':165 [in Redblack]

k':165 [in ADT]

k':179 [in SearchTree]

k':184 [in Redblack]

k':246 [in SearchTree]

k':248 [in SearchTree]

k':25 [in ADT]

k':31 [in ADT]

k':365 [in ADT]

k':391 [in ADT]

k':399 [in ADT]

k':45 [in ADT]

k':58 [in ADT]

k':63 [in Redblack]

k':64 [in Redblack]

k':67 [in SearchTree]

k':76 [in Redblack]

k':77 [in Redblack]

k':84 [in Redblack]

k':85 [in Redblack]

k':91 [in Extract]

k':92 [in SearchTree]

k':95 [in ADT]

k':96 [in Redblack]

k':97 [in Redblack]

k':97 [in SearchTree]

k

_{0}:101 [in Redblack]

k

_{0}:245 [in SearchTree]

k

_{0}:95 [in Redblack]

k

_{1}:110 [in SearchTree]

k

_{1}:129 [in SearchTree]

k

_{1}:145 [in SearchTree]

k

_{2}:111 [in SearchTree]

k

_{2}:130 [in SearchTree]

k

_{2}:146 [in SearchTree]

k:10 [in Perm]

k:100 [in Trie]

k:100 [in Redblack]

k:103 [in SearchTree]

k:103 [in ADT]

k:105 [in SearchTree]

k:106 [in Trie]

k:107 [in Redblack]

k:108 [in ADT]

k:111 [in ADT]

k:114 [in ADT]

k:115 [in ADT]

k:117 [in Redblack]

k:118 [in SearchTree]

k:118 [in ADT]

k:121 [in SearchTree]

k:122 [in Redblack]

k:122 [in ADT]

k:123 [in Binom]

k:125 [in ADT]

k:126 [in Redblack]

k:129 [in ADT]

k:13 [in Perm]

k:13 [in ADT]

k:131 [in Redblack]

k:132 [in ADT]

k:134 [in Redblack]

k:135 [in SearchTree]

k:135 [in ADT]

k:136 [in ADT]

k:138 [in Trie]

k:138 [in Redblack]

k:139 [in Binom]

k:139 [in ADT]

k:141 [in SearchTree]

k:143 [in ADT]

k:146 [in ADT]

k:148 [in Redblack]

k:153 [in Redblack]

k:153 [in SearchTree]

k:154 [in ADT]

k:157 [in ADT]

k:158 [in SearchTree]

k:159 [in Redblack]

k:16 [in Redblack]

k:16 [in Perm]

k:160 [in ADT]

k:161 [in ADT]

k:163 [in SearchTree]

k:164 [in Redblack]

k:164 [in ADT]

k:168 [in ADT]

k:17 [in Priqueue]

k:171 [in Redblack]

k:171 [in ADT]

k:174 [in Redblack]

k:175 [in ADT]

k:178 [in Redblack]

k:178 [in SearchTree]

k:183 [in Redblack]

k:185 [in SearchTree]

k:189 [in SearchTree]

k:191 [in ADT]

k:192 [in Redblack]

k:194 [in SearchTree]

k:197 [in ADT]

k:198 [in Redblack]

k:20 [in ADT]

k:200 [in ADT]

k:203 [in ADT]

k:208 [in ADT]

k:209 [in Redblack]

k:211 [in ADT]

k:214 [in Redblack]

k:214 [in ADT]

k:218 [in Redblack]

k:22 [in Priqueue]

k:22 [in ADT]

k:220 [in ADT]

k:224 [in Redblack]

k:224 [in ADT]

k:226 [in ADT]

k:228 [in SearchTree]

k:228 [in ADT]

k:233 [in Redblack]

k:234 [in SearchTree]

k:244 [in SearchTree]

k:252 [in SearchTree]

k:26 [in ADT]

k:262 [in SearchTree]

k:265 [in SearchTree]

k:27 [in ADT]

k:274 [in SearchTree]

k:278 [in SearchTree]

k:28 [in Priqueue]

k:282 [in SearchTree]

k:286 [in SearchTree]

k:289 [in SearchTree]

k:296 [in SearchTree]

k:30 [in ADT]

k:300 [in SearchTree]

k:304 [in SearchTree]

k:308 [in SearchTree]

k:314 [in SearchTree]

k:319 [in SearchTree]

k:32 [in Priqueue]

k:328 [in SearchTree]

k:335 [in SearchTree]

k:339 [in SearchTree]

k:34 [in ADT]

k:341 [in SearchTree]

k:358 [in ADT]

k:360 [in ADT]

k:364 [in ADT]

k:369 [in ADT]

k:37 [in ADT]

k:373 [in ADT]

k:378 [in ADT]

k:380 [in ADT]

k:383 [in ADT]

k:386 [in ADT]

k:387 [in ADT]

k:390 [in ADT]

k:394 [in ADT]

k:395 [in ADT]

k:398 [in ADT]

k:40 [in ADT]

k:402 [in ADT]

k:405 [in ADT]

k:41 [in ADT]

k:43 [in Binom]

k:44 [in SearchTree]

k:44 [in ADT]

k:45 [in Binom]

k:47 [in SearchTree]

k:48 [in ADT]

k:5 [in SearchTree]

k:50 [in ADT]

k:52 [in SearchTree]

k:53 [in ADT]

k:54 [in ADT]

k:56 [in SearchTree]

k:57 [in ADT]

k:60 [in Redblack]

k:61 [in SearchTree]

k:63 [in ADT]

k:66 [in SearchTree]

k:67 [in Priqueue]

k:67 [in ADT]

k:69 [in Redblack]

K:69 [in Color]

k:7 [in ADT]

k:70 [in SearchTree]

k:71 [in ADT]

k:73 [in Redblack]

k:74 [in ADT]

k:75 [in SearchTree]

K:76 [in Color]

k:77 [in SearchTree]

k:77 [in ADT]

K:79 [in Color]

k:81 [in Redblack]

k:81 [in Extract]

k:82 [in Priqueue]

K:82 [in Color]

k:82 [in SearchTree]

k:82 [in Binom]

K:84 [in Color]

k:84 [in ADT]

k:85 [in Extract]

k:86 [in Priqueue]

k:86 [in SearchTree]

K:87 [in Color]

k:88 [in ADT]

k:89 [in Priqueue]

K:89 [in Color]

k:9 [in Perm]

k:9 [in ADT]

k:90 [in Redblack]

k:90 [in ADT]

k:90 [in Extract]

K:91 [in Color]

k:91 [in SearchTree]

k:93 [in Priqueue]

k:94 [in Redblack]

k:94 [in ADT]

k:96 [in SearchTree]

k:99 [in ADT]

## L

lst:203 [in SearchTree]lst:224 [in SearchTree]

lst:269 [in SearchTree]

lst:56 [in Selection]

l':50 [in Priqueue]

l':52 [in Priqueue]

l':6 [in Selection]

l':8 [in Selection]

l

_{1}:102 [in Merge]

l

_{1}:197 [in SearchTree]

l

_{1}:20 [in Merge]

l

_{1}:207 [in SearchTree]

l

_{1}:211 [in SearchTree]

l

_{1}:28 [in BagPerm]

l

_{1}:30 [in BagPerm]

l

_{1}:30 [in Multiset]

l

_{1}:32 [in Multiset]

l

_{1}:43 [in Merge]

l

_{1}:47 [in Merge]

l

_{1}:49 [in Merge]

l

_{1}:5 [in Merge]

l

_{1}:65 [in Merge]

l

_{1}:72 [in Merge]

l

_{1}:77 [in Merge]

l

_{1}:9 [in Merge]

l

_{1}:96 [in Merge]

l

_{1}:99 [in Merge]

l

_{2}:10 [in Merge]

l

_{2}:100 [in Merge]

l

_{2}:103 [in Merge]

l

_{2}:198 [in SearchTree]

l

_{2}:208 [in SearchTree]

l

_{2}:21 [in Merge]

l

_{2}:212 [in SearchTree]

l

_{2}:29 [in BagPerm]

l

_{2}:31 [in BagPerm]

l

_{2}:31 [in Multiset]

l

_{2}:33 [in Multiset]

l

_{2}:44 [in Merge]

l

_{2}:48 [in Merge]

l

_{2}:50 [in Merge]

l

_{2}:52 [in Merge]

l

_{2}:6 [in Merge]

l

_{2}:66 [in Merge]

l

_{2}:73 [in Merge]

l

_{2}:78 [in Merge]

l

_{2}:98 [in Merge]

l:101 [in Merge]

l:103 [in Selection]

l:104 [in Merge]

l:106 [in Redblack]

l:113 [in Selection]

l:114 [in Selection]

l:115 [in Redblack]

l:12 [in Color]

l:12 [in Extract]

l:13 [in Sort]

l:14 [in Selection]

l:141 [in Redblack]

l:16 [in Merge]

l:17 [in Merge]

l:18 [in Decide]

l:19 [in Merge]

l:190 [in Redblack]

l:196 [in Redblack]

l:2 [in Sort]

l:2 [in Selection]

l:2 [in Merge]

l:2 [in Extract]

l:20 [in BagPerm]

l:207 [in Redblack]

l:21 [in BagPerm]

l:21 [in Decide]

l:21 [in Selection]

l:21 [in Multiset]

l:212 [in Redblack]

l:22 [in Color]

l:22 [in Multiset]

l:25 [in BagPerm]

l:25 [in Multiset]

l:27 [in Sort]

l:27 [in Selection]

l:27 [in Multiset]

l:27 [in Merge]

l:28 [in Sort]

l:28 [in Merge]

l:29 [in Decide]

l:30 [in Sort]

l:31 [in Sort]

l:31 [in Decide]

l:34 [in SearchTree]

l:34 [in Sort]

l:35 [in Selection]

l:36 [in Merge]

l:38 [in Merge]

l:39 [in Selection]

l:4 [in SearchTree]

l:40 [in Sort]

l:41 [in Sort]

l:42 [in Merge]

l:43 [in Selection]

l:43 [in Extract]

l:46 [in Priqueue]

l:46 [in Merge]

l:46 [in Extract]

l:47 [in Perm]

l:47 [in Selection]

l:48 [in Color]

l:48 [in Selection]

l:5 [in Sort]

l:5 [in Extract]

l:54 [in Priqueue]

l:54 [in Extract]

l:59 [in Redblack]

l:61 [in Merge]

l:62 [in Binom]

l:62 [in Merge]

l:67 [in Merge]

l:68 [in Merge]

l:70 [in Merge]

l:72 [in Redblack]

l:73 [in Selection]

l:74 [in Merge]

l:75 [in Merge]

l:78 [in Selection]

l:79 [in Selection]

l:8 [in Merge]

l:80 [in Redblack]

l:81 [in Selection]

l:85 [in Selection]

l:86 [in Selection]

l:9 [in Selection]

l:9 [in Extract]

## M

merge_aux:56 [in Merge]m

_{1}:294 [in SearchTree]

m

_{1}:298 [in SearchTree]

m

_{1}:302 [in SearchTree]

m

_{1}:306 [in SearchTree]

m

_{1}:312 [in SearchTree]

m

_{1}:317 [in SearchTree]

m

_{2}:295 [in SearchTree]

m

_{2}:299 [in SearchTree]

m

_{2}:303 [in SearchTree]

m

_{2}:307 [in SearchTree]

m

_{2}:313 [in SearchTree]

m

_{2}:318 [in SearchTree]

m:100 [in SearchTree]

m:106 [in SearchTree]

m:112 [in SearchTree]

m:124 [in Trie]

m:13 [in Maps]

m:136 [in Trie]

m:177 [in ADT]

m:18 [in Extract]

m:2 [in Color]

m:2 [in Perm]

m:20 [in Maps]

m:22 [in Maps]

m:22 [in Extract]

m:26 [in Extract]

m:263 [in SearchTree]

m:266 [in SearchTree]

m:28 [in Maps]

m:34 [in Maps]

m:38 [in Binom]

m:38 [in Maps]

m:4 [in Perm]

m:44 [in Maps]

m:49 [in Trie]

m:5 [in Maps]

m:51 [in Maps]

m:52 [in Binom]

m:53 [in Maps]

m:6 [in Perm]

m:60 [in Maps]

m:66 [in Maps]

m:68 [in Trie]

m:79 [in Trie]

m:85 [in SearchTree]

m:98 [in SearchTree]

## N

n':230 [in Redblack]n':236 [in Redblack]

n:1 [in Perm]

n:102 [in Selection]

n:106 [in Color]

n:106 [in Selection]

n:109 [in Trie]

n:110 [in Trie]

n:110 [in Color]

n:111 [in Binom]

n:112 [in Selection]

n:116 [in Binom]

n:121 [in Trie]

n:127 [in Binom]

n:15 [in Selection]

n:17 [in Extract]

n:194 [in Redblack]

n:200 [in Redblack]

n:200 [in SearchTree]

n:201 [in SearchTree]

n:203 [in Redblack]

n:21 [in Extract]

n:211 [in Redblack]

n:216 [in Redblack]

n:221 [in Redblack]

n:226 [in Redblack]

n:229 [in Redblack]

n:235 [in Redblack]

n:246 [in Redblack]

n:25 [in Extract]

n:27 [in BagPerm]

n:29 [in Multiset]

n:3 [in Color]

n:3 [in Perm]

n:339 [in ADT]

n:46 [in Selection]

n:5 [in Perm]

n:51 [in Binom]

n:52 [in Color]

n:54 [in Color]

n:58 [in Binom]

n:58 [in Selection]

n:66 [in Color]

n:66 [in Binom]

n:69 [in Binom]

n:69 [in Selection]

n:7 [in BagPerm]

n:70 [in Color]

n:70 [in Selection]

n:72 [in Color]

n:77 [in Binom]

n:78 [in Color]

## P

palette:108 [in Color]palette:112 [in Color]

palette:114 [in Color]

palette:129 [in Color]

pat:173 [in SearchTree]

pat:247 [in SearchTree]

pat:249 [in SearchTree]

pat:285 [in ADT]

pat:290 [in ADT]

pat:341 [in ADT]

pe:128 [in Binom]

pl:100 [in Priqueue]

pl:133 [in Binom]

pl:140 [in Binom]

pl:33 [in Priqueue]

pl:41 [in Priqueue]

pl:94 [in Priqueue]

p':47 [in Binom]

p:104 [in Binom]

p:109 [in Binom]

p:11 [in Priqueue]

p:111 [in Trie]

p:113 [in Trie]

P:113 [in Redblack]

p:12 [in Trie]

P:12 [in Merge]

P:120 [in Redblack]

p:121 [in Binom]

p:124 [in Binom]

p:131 [in Binom]

p:136 [in Binom]

p:137 [in Binom]

p:16 [in Binom]

P:175 [in SearchTree]

p:18 [in Priqueue]

p:20 [in Priqueue]

P:23 [in Merge]

p:24 [in Priqueue]

P:25 [in Perm]

p:26 [in Priqueue]

p:27 [in Trie]

P:27 [in SearchTree]

p:29 [in Trie]

p:30 [in Priqueue]

P:30 [in Merge]

P:304 [in ADT]

P:308 [in ADT]

p:31 [in Trie]

P:312 [in ADT]

P:316 [in ADT]

P:322 [in ADT]

P:326 [in SearchTree]

P:327 [in ADT]

P:331 [in ADT]

P:335 [in ADT]

p:36 [in Priqueue]

p:39 [in Priqueue]

p:39 [in Binom]

p:40 [in Trie]

P:42 [in SearchTree]

p:49 [in Binom]

P:51 [in Redblack]

P:64 [in Color]

p:68 [in Priqueue]

p:69 [in Priqueue]

p:71 [in Priqueue]

p:73 [in Priqueue]

P:74 [in Color]

p:74 [in Binom]

p:76 [in Priqueue]

p:77 [in Priqueue]

p:78 [in Binom]

p:79 [in Priqueue]

p:8 [in Priqueue]

p:80 [in Binom]

p:83 [in Priqueue]

p:84 [in Priqueue]

P:87 [in Redblack]

p:87 [in Priqueue]

p:9 [in Trie]

p:90 [in Priqueue]

p:91 [in Priqueue]

p:93 [in Binom]

p:96 [in Priqueue]

p:98 [in Priqueue]

## Q

qe:129 [in Binom]ql:101 [in Priqueue]

ql:134 [in Binom]

ql:141 [in Binom]

ql:34 [in Priqueue]

ql:42 [in Priqueue]

ql:95 [in Priqueue]

q':48 [in Binom]

q:101 [in Binom]

q:114 [in Trie]

q:117 [in Binom]

q:125 [in Binom]

q:13 [in Binom]

q:132 [in Binom]

q:138 [in Binom]

q:15 [in Binom]

q:17 [in Binom]

q:239 [in ADT]

q:245 [in ADT]

q:249 [in ADT]

q:252 [in ADT]

q:253 [in ADT]

q:255 [in ADT]

q:257 [in ADT]

q:258 [in ADT]

q:262 [in ADT]

q:264 [in ADT]

q:27 [in Priqueue]

q:27 [in Binom]

q:275 [in ADT]

q:279 [in ADT]

q:281 [in ADT]

q:286 [in ADT]

q:292 [in ADT]

q:295 [in ADT]

q:297 [in ADT]

q:30 [in Trie]

q:300 [in ADT]

q:301 [in ADT]

q:31 [in Priqueue]

q:32 [in Trie]

q:32 [in Binom]

q:35 [in Binom]

q:37 [in Priqueue]

q:40 [in Priqueue]

q:46 [in Binom]

q:50 [in Binom]

q:65 [in Binom]

q:7 [in Binom]

q:70 [in Binom]

q:72 [in Priqueue]

q:73 [in Binom]

q:75 [in Binom]

q:79 [in Binom]

q:81 [in Binom]

Q:88 [in Redblack]

q:88 [in Priqueue]

q:92 [in Priqueue]

q:97 [in Priqueue]

q:99 [in Priqueue]

## R

r':13 [in Selection]r':20 [in Selection]

r':77 [in Selection]

r':84 [in Selection]

r':89 [in Selection]

r

_{1}:59 [in Merge]

r

_{2}:60 [in Merge]

r:109 [in Redblack]

r:116 [in Redblack]

r:142 [in Redblack]

R:182 [in SearchTree]

r:191 [in Redblack]

r:197 [in Redblack]

r:208 [in Redblack]

r:213 [in Redblack]

r:37 [in SearchTree]

r:41 [in Selection]

r:45 [in Perm]

r:45 [in Selection]

r:56 [in Priqueue]

r:62 [in Redblack]

r:7 [in SearchTree]

r:75 [in Redblack]

r:83 [in Redblack]

## S

sort:38 [in BagPerm]sort:42 [in Multiset]

s:105 [in Color]

s:107 [in Color]

s:126 [in Color]

s:14 [in Color]

s:18 [in Color]

s:2 [in BagPerm]

s:31 [in Color]

s:4 [in Color]

s:40 [in Color]

s:44 [in Color]

s:68 [in Color]

## T

table:3 [in Trie]table:55 [in Trie]

table:91 [in Trie]

tl:88 [in Binom]

tr:89 [in Binom]

t

_{1}:15 [in Redblack]

t

_{2}:18 [in Redblack]

t:10 [in Redblack]

t:101 [in ADT]

t:102 [in Trie]

t:105 [in ADT]

t:107 [in Binom]

t:107 [in ADT]

t:108 [in Trie]

t:109 [in ADT]

t:11 [in SearchTree]

t:11 [in ADT]

t:110 [in ADT]

t:112 [in Binom]

t:113 [in ADT]

t:114 [in SearchTree]

t:117 [in ADT]

t:118 [in Trie]

t:118 [in Binom]

t:120 [in Trie]

t:121 [in Redblack]

t:121 [in ADT]

t:123 [in Trie]

t:124 [in SearchTree]

t:124 [in ADT]

t:125 [in Redblack]

t:127 [in ADT]

t:128 [in ADT]

t:129 [in Redblack]

t:130 [in Trie]

t:130 [in ADT]

t:131 [in ADT]

t:132 [in SearchTree]

t:134 [in SearchTree]

t:134 [in ADT]

t:135 [in Trie]

t:138 [in ADT]

t:140 [in Trie]

t:140 [in SearchTree]

t:142 [in ADT]

t:145 [in ADT]

t:147 [in Redblack]

t:147 [in SearchTree]

t:148 [in ADT]

t:149 [in SearchTree]

t:152 [in Redblack]

t:153 [in ADT]

t:155 [in ADT]

t:156 [in SearchTree]

t:156 [in ADT]

t:158 [in Redblack]

t:159 [in ADT]

t:16 [in ADT]

t:161 [in SearchTree]

t:163 [in Redblack]

t:163 [in ADT]

t:166 [in SearchTree]

t:167 [in ADT]

t:169 [in Redblack]

t:17 [in SearchTree]

t:170 [in ADT]

t:173 [in ADT]

t:176 [in SearchTree]

t:177 [in Redblack]

t:181 [in SearchTree]

t:182 [in Redblack]

t:187 [in SearchTree]

t:190 [in SearchTree]

t:193 [in ADT]

t:195 [in SearchTree]

t:196 [in ADT]

t:199 [in ADT]

t:202 [in Redblack]

t:202 [in ADT]

t:205 [in SearchTree]

t:206 [in ADT]

t:209 [in ADT]

t:21 [in ADT]

t:213 [in ADT]

t:214 [in SearchTree]

t:215 [in ADT]

t:216 [in SearchTree]

t:217 [in ADT]

t:218 [in ADT]

t:219 [in ADT]

t:220 [in Redblack]

t:221 [in SearchTree]

t:222 [in ADT]

t:223 [in Redblack]

t:223 [in SearchTree]

t:223 [in ADT]

t:225 [in ADT]

t:226 [in SearchTree]

t:227 [in ADT]

t:228 [in Redblack]

t:23 [in SearchTree]

t:23 [in Binom]

t:230 [in ADT]

t:231 [in SearchTree]

t:232 [in Redblack]

t:238 [in Redblack]

t:24 [in ADT]

t:241 [in Redblack]

t:244 [in Redblack]

t:25 [in Redblack]

t:251 [in SearchTree]

t:259 [in SearchTree]

t:28 [in SearchTree]

t:28 [in Binom]

t:281 [in SearchTree]

t:284 [in SearchTree]

t:288 [in SearchTree]

t:29 [in Redblack]

t:29 [in ADT]

t:292 [in SearchTree]

t:3 [in Binom]

t:322 [in SearchTree]

t:327 [in SearchTree]

t:33 [in ADT]

t:331 [in SearchTree]

t:334 [in SearchTree]

t:338 [in SearchTree]

t:34 [in Redblack]

t:343 [in SearchTree]

t:348 [in SearchTree]

t:35 [in ADT]

t:36 [in Redblack]

t:362 [in ADT]

t:367 [in ADT]

t:371 [in ADT]

t:375 [in ADT]

t:377 [in ADT]

t:379 [in ADT]

t:382 [in ADT]

t:384 [in ADT]

t:385 [in ADT]

t:389 [in ADT]

t:39 [in ADT]

t:393 [in ADT]

t:397 [in ADT]

t:401 [in ADT]

t:404 [in ADT]

t:407 [in ADT]

t:41 [in Redblack]

t:43 [in SearchTree]

t:43 [in Perm]

t:43 [in ADT]

t:45 [in Redblack]

t:47 [in ADT]

t:49 [in Redblack]

t:49 [in SearchTree]

t:49 [in ADT]

t:52 [in Redblack]

t:52 [in ADT]

t:53 [in Binom]

t:54 [in SearchTree]

t:56 [in ADT]

t:59 [in SearchTree]

t:59 [in Binom]

t:60 [in ADT]

t:63 [in Extract]

t:64 [in SearchTree]

t:65 [in ADT]

t:67 [in Redblack]

t:67 [in Binom]

t:69 [in ADT]

t:69 [in Extract]

t:71 [in Binom]

t:72 [in SearchTree]

t:72 [in ADT]

t:73 [in ADT]

t:73 [in Extract]

t:74 [in Trie]

t:76 [in ADT]

t:78 [in Extract]

t:79 [in ADT]

t:8 [in Binom]

t:80 [in SearchTree]

t:84 [in Extract]

t:86 [in ADT]

t:87 [in Trie]

t:89 [in Redblack]

t:89 [in SearchTree]

t:89 [in Extract]

t:92 [in ADT]

t:93 [in Redblack]

t:95 [in Binom]

t:97 [in ADT]

t:98 [in Binom]

t:99 [in Redblack]

## U

u:113 [in Binom]u:30 [in Binom]

u:4 [in Binom]

u:42 [in Perm]

u:68 [in Binom]

## V

vk:17 [in Redblack]vx:24 [in Redblack]

vx:33 [in Redblack]

vx:44 [in Redblack]

vx:48 [in Redblack]

v':116 [in SearchTree]

v':137 [in SearchTree]

v

_{0}:241 [in SearchTree]

v

_{1}:101 [in SearchTree]

v

_{1}:108 [in SearchTree]

v

_{1}:126 [in SearchTree]

v

_{1}:143 [in SearchTree]

v

_{1}:23 [in Maps]

v

_{1}:30 [in Maps]

v

_{1}:309 [in SearchTree]

v

_{1}:351 [in ADT]

v

_{1}:354 [in ADT]

v

_{1}:54 [in Maps]

v

_{1}:62 [in Maps]

v

_{2}:102 [in SearchTree]

v

_{2}:109 [in SearchTree]

v

_{2}:127 [in SearchTree]

v

_{2}:144 [in SearchTree]

v

_{2}:24 [in Maps]

v

_{2}:31 [in Maps]

v

_{2}:310 [in SearchTree]

v

_{2}:352 [in ADT]

v

_{2}:355 [in ADT]

v

_{2}:55 [in Maps]

v

_{2}:63 [in Maps]

V:1 [in SearchTree]

v:1 [in BagPerm]

v:10 [in ADT]

v:100 [in ADT]

v:101 [in Trie]

V:104 [in Redblack]

V:104 [in SearchTree]

v:104 [in ADT]

v:107 [in Trie]

V:107 [in SearchTree]

v:108 [in Redblack]

v:11 [in Maps]

V:112 [in Redblack]

v:112 [in ADT]

V:113 [in SearchTree]

v:115 [in SearchTree]

v:116 [in ADT]

v:118 [in Redblack]

V:119 [in Redblack]

V:120 [in SearchTree]

v:120 [in ADT]

v:123 [in Redblack]

v:123 [in ADT]

V:124 [in Redblack]

V:125 [in SearchTree]

v:126 [in ADT]

v:127 [in Redblack]

V:128 [in Redblack]

V:13 [in Redblack]

v:130 [in Redblack]

V:132 [in Redblack]

V:133 [in SearchTree]

v:133 [in ADT]

V:135 [in Redblack]

v:136 [in SearchTree]

v:137 [in ADT]

V:138 [in SearchTree]

v:139 [in Trie]

V:14 [in SearchTree]

v:140 [in Redblack]

v:141 [in ADT]

V:142 [in SearchTree]

v:144 [in ADT]

V:145 [in Redblack]

v:147 [in ADT]

V:148 [in SearchTree]

v:149 [in Redblack]

v:15 [in ADT]

v:15 [in Maps]

V:150 [in Redblack]

V:152 [in SearchTree]

v:154 [in SearchTree]

v:155 [in Redblack]

V:156 [in Redblack]

V:157 [in SearchTree]

v:158 [in ADT]

v:159 [in SearchTree]

v:160 [in Redblack]

V:161 [in Redblack]

V:162 [in SearchTree]

v:162 [in ADT]

v:164 [in SearchTree]

v:166 [in Redblack]

v:166 [in ADT]

V:167 [in Redblack]

V:168 [in Redblack]

v:169 [in ADT]

v:17 [in Maps]

v:170 [in Redblack]

V:172 [in Redblack]

v:172 [in ADT]

V:174 [in SearchTree]

V:174 [in ADT]

V:175 [in Redblack]

v:176 [in ADT]

V:177 [in SearchTree]

V:178 [in ADT]

v:179 [in Redblack]

V:179 [in ADT]

V:180 [in Redblack]

v:180 [in SearchTree]

V:184 [in SearchTree]

v:185 [in Redblack]

V:186 [in Redblack]

v:186 [in SearchTree]

V:188 [in SearchTree]

v:191 [in SearchTree]

v:192 [in ADT]

v:193 [in Redblack]

V:193 [in SearchTree]

v:196 [in SearchTree]

v:199 [in Redblack]

v:2 [in Multiset]

V:20 [in SearchTree]

V:201 [in Redblack]

V:202 [in SearchTree]

V:204 [in Redblack]

V:204 [in SearchTree]

v:204 [in ADT]

v:210 [in Redblack]

v:212 [in ADT]

V:213 [in SearchTree]

v:215 [in Redblack]

V:215 [in SearchTree]

V:217 [in Redblack]

v:219 [in Redblack]

V:22 [in Redblack]

v:22 [in SearchTree]

V:220 [in SearchTree]

v:221 [in ADT]

V:222 [in Redblack]

V:222 [in SearchTree]

v:225 [in Redblack]

V:225 [in SearchTree]

V:227 [in Redblack]

V:227 [in SearchTree]

v:229 [in SearchTree]

v:229 [in ADT]

v:23 [in ADT]

V:231 [in Redblack]

V:232 [in SearchTree]

V:233 [in SearchTree]

v:234 [in Redblack]

v:235 [in SearchTree]

V:237 [in Redblack]

V:239 [in SearchTree]

V:240 [in Redblack]

v:240 [in SearchTree]

v:240 [in ADT]

V:243 [in Redblack]

v:246 [in ADT]

V:250 [in SearchTree]

v:250 [in ADT]

v:253 [in SearchTree]

V:254 [in SearchTree]

v:254 [in ADT]

V:258 [in SearchTree]

v:259 [in ADT]

V:26 [in SearchTree]

V:260 [in SearchTree]

v:263 [in ADT]

V:264 [in SearchTree]

v:265 [in ADT]

V:272 [in SearchTree]

v:275 [in SearchTree]

V:276 [in SearchTree]

v:276 [in ADT]

V:279 [in SearchTree]

V:28 [in Redblack]

v:28 [in ADT]

V:280 [in SearchTree]

V:283 [in SearchTree]

V:287 [in SearchTree]

v:290 [in SearchTree]

V:291 [in SearchTree]

v:291 [in ADT]

v:298 [in ADT]

V:3 [in Redblack]

v:3 [in Maps]

V:31 [in Redblack]

V:31 [in SearchTree]

v:315 [in SearchTree]

v:32 [in ADT]

v:320 [in SearchTree]

V:321 [in SearchTree]

V:325 [in SearchTree]

v:329 [in SearchTree]

V:330 [in SearchTree]

V:332 [in SearchTree]

V:333 [in SearchTree]

V:336 [in SearchTree]

V:340 [in SearchTree]

v:342 [in SearchTree]

V:344 [in SearchTree]

v:344 [in ADT]

v:346 [in ADT]

V:347 [in SearchTree]

v:349 [in ADT]

V:35 [in Redblack]

v:36 [in SearchTree]

v:361 [in ADT]

v:366 [in ADT]

v:370 [in ADT]

v:374 [in ADT]

v:38 [in ADT]

v:381 [in ADT]

v:388 [in ADT]

v:392 [in ADT]

v:396 [in ADT]

V:40 [in Redblack]

V:40 [in SearchTree]

v:40 [in Maps]

v:400 [in ADT]

v:403 [in ADT]

v:406 [in ADT]

V:41 [in SearchTree]

V:42 [in Redblack]

v:42 [in ADT]

v:45 [in SearchTree]

V:46 [in Redblack]

V:46 [in SearchTree]

v:46 [in ADT]

v:46 [in Maps]

v:48 [in SearchTree]

v:48 [in Maps]

V:50 [in Redblack]

V:50 [in SearchTree]

v:51 [in Trie]

v:51 [in ADT]

V:53 [in SearchTree]

V:55 [in Redblack]

v:55 [in ADT]

V:56 [in Extract]

v:57 [in SearchTree]

V:58 [in SearchTree]

v:58 [in Maps]

v:59 [in ADT]

V:59 [in Extract]

V:6 [in Redblack]

v:6 [in SearchTree]

V:60 [in Extract]

v:61 [in Redblack]

v:62 [in SearchTree]

V:63 [in SearchTree]

v:64 [in ADT]

V:65 [in Redblack]

V:66 [in Redblack]

V:66 [in Extract]

v:68 [in Redblack]

v:68 [in SearchTree]

v:68 [in ADT]

v:68 [in Extract]

V:69 [in SearchTree]

V:7 [in Redblack]

v:7 [in Maps]

V:70 [in Redblack]

V:72 [in Extract]

V:73 [in SearchTree]

v:74 [in Redblack]

v:75 [in ADT]

V:76 [in SearchTree]

V:77 [in Extract]

V:78 [in Redblack]

v:78 [in ADT]

V:79 [in SearchTree]

V:79 [in Extract]

V:8 [in SearchTree]

v:82 [in Redblack]

V:82 [in Extract]

v:83 [in SearchTree]

V:84 [in SearchTree]

v:85 [in ADT]

V:86 [in Redblack]

v:86 [in Extract]

v:87 [in SearchTree]

v:87 [in Binom]

V:87 [in Extract]

V:88 [in SearchTree]

V:9 [in SearchTree]

v:91 [in Redblack]

v:91 [in ADT]

V:92 [in Redblack]

v:92 [in Extract]

v:93 [in SearchTree]

V:94 [in SearchTree]

v:95 [in SearchTree]

v:96 [in ADT]

V:98 [in Redblack]

V:99 [in SearchTree]

## X

xs:340 [in ADT]xs:54 [in Selection]

x':52 [in Trie]

x':8 [in Maps]

x

_{1}:18 [in Maps]

x

_{1}:32 [in Maps]

x

_{1}:49 [in Maps]

x

_{1}:57 [in Merge]

x

_{1}:64 [in Maps]

x

_{1}:95 [in Merge]

x

_{2}:19 [in Maps]

x

_{2}:33 [in Maps]

x

_{2}:50 [in Maps]

x

_{2}:58 [in Merge]

x

_{2}:65 [in Maps]

x

_{2}:97 [in Merge]

x:1 [in Selection]

x:1 [in Multiset]

X:1 [in Merge]

x:10 [in SearchTree]

x:10 [in Sort]

x:10 [in Maps]

x:11 [in Sort]

x:110 [in Selection]

x:12 [in Binom]

x:129 [in Trie]

x:14 [in BagPerm]

x:14 [in Binom]

x:14 [in Maps]

x:15 [in Trie]

x:15 [in Color]

x:16 [in SearchTree]

X:16 [in Maps]

X:167 [in SearchTree]

x:17 [in Decide]

X:18 [in Merge]

x:19 [in Trie]

x:19 [in Color]

x:19 [in BagPerm]

x:199 [in SearchTree]

x:20 [in Perm]

x:20 [in Multiset]

X:206 [in SearchTree]

x:209 [in SearchTree]

x:21 [in SearchTree]

X:210 [in SearchTree]

x:23 [in Redblack]

x:25 [in Trie]

x:25 [in Maps]

x:26 [in BagPerm]

x:26 [in Decide]

x:26 [in Multiset]

X:26 [in Maps]

X:267 [in SearchTree]

x:27 [in Perm]

x:27 [in Decide]

x:27 [in Maps]

x:270 [in SearchTree]

x:28 [in Multiset]

x:28 [in Extract]

x:29 [in Sort]

x:29 [in Perm]

X:29 [in Maps]

X:293 [in SearchTree]

X:297 [in SearchTree]

x:3 [in Multiset]

x:30 [in Extract]

X:301 [in SearchTree]

x:302 [in ADT]

X:305 [in SearchTree]

x:305 [in ADT]

x:306 [in ADT]

x:309 [in ADT]

x:31 [in Perm]

X:311 [in SearchTree]

x:313 [in ADT]

X:316 [in SearchTree]

x:319 [in ADT]

x:32 [in Redblack]

x:32 [in BagPerm]

x:32 [in Selection]

x:32 [in Extract]

x:320 [in ADT]

x:325 [in ADT]

x:33 [in Perm]

X:338 [in ADT]

x:34 [in Multiset]

x:34 [in Extract]

X:342 [in ADT]

x:343 [in ADT]

X:345 [in ADT]

X:347 [in ADT]

x:348 [in ADT]

x:35 [in Trie]

x:35 [in SearchTree]

x:35 [in Perm]

X:350 [in ADT]

X:353 [in ADT]

x:36 [in Color]

x:36 [in Extract]

x:38 [in Selection]

x:38 [in Multiset]

x:38 [in Extract]

x:39 [in Multiset]

x:39 [in Maps]

x:40 [in Extract]

x:41 [in Trie]

x:41 [in Color]

X:41 [in Merge]

x:42 [in Selection]

x:42 [in Maps]

x:43 [in Redblack]

X:45 [in Merge]

x:45 [in Maps]

x:47 [in Redblack]

X:47 [in Maps]

x:50 [in Trie]

x:50 [in Color]

x:51 [in Selection]

x:51 [in Extract]

x:52 [in Extract]

x:53 [in Selection]

x:56 [in Maps]

X:57 [in Maps]

x:59 [in Maps]

x:6 [in Multiset]

x:6 [in Maps]

x:61 [in Priqueue]

x:61 [in Selection]

X:61 [in Maps]

x:62 [in Extract]

x:65 [in Selection]

x:66 [in Priqueue]

x:67 [in Extract]

X:7 [in Merge]

x:72 [in Binom]

x:9 [in Redblack]

x:94 [in Merge]

## Y

y:105 [in Selection]y:111 [in Selection]

y:12 [in Sort]

y:12 [in Selection]

Y:168 [in SearchTree]

y:183 [in SearchTree]

y:19 [in Selection]

y:20 [in Trie]

y:21 [in Perm]

y:26 [in Trie]

Y:268 [in SearchTree]

y:271 [in SearchTree]

y:28 [in Perm]

y:28 [in Decide]

y:29 [in Extract]

y:30 [in Perm]

y:31 [in Extract]

y:32 [in Perm]

y:33 [in BagPerm]

y:33 [in Extract]

y:34 [in Perm]

y:35 [in Multiset]

y:35 [in Extract]

y:36 [in Trie]

y:36 [in Perm]

y:37 [in Color]

y:37 [in Extract]

y:38 [in SearchTree]

y:39 [in SearchTree]

y:39 [in Extract]

y:40 [in Selection]

y:41 [in Extract]

y:42 [in Trie]

y:44 [in Selection]

y:48 [in Perm]

y:51 [in Color]

y:52 [in Selection]

y:53 [in Extract]

y:55 [in Selection]

y:57 [in Selection]

y:62 [in Selection]

y:66 [in Selection]

y:68 [in Selection]

y:76 [in Selection]

y:83 [in Selection]

y:88 [in Selection]

## Z

Z:169 [in SearchTree]# Module Index

## B

BinomQueue [in Binom]## E

E [in Color]ETable [in ADT]

ETableAbs [in ADT]

ETableSubset [in ADT]

ETable_first_attempt [in ADT]

## F

FastEnough [in Trie]FunTable [in ADT]

FunTableExamples [in ADT]

FunTableExamples.StringFunTable [in ADT]

## I

Integers [in Trie]## L

ListETableAbs [in ADT]ListQueue [in ADT]

ListsTable [in ADT]

List_Priqueue [in Priqueue]

## M

M [in Color]## N

NatFunTableExamples [in ADT]NicelyEncapsulatedExample [in ADT]

NicelyEncapsulatedExample.StringTreeETableEncapsulated [in ADT]

NotBst [in SearchTree]

## O

OverlyEncapsulatedExample [in ADT]OverlyEncapsulatedExample.StringTreeETableFullyEncapsulated [in ADT]

## P

PRIQUEUE [in Priqueue]## Q

Queue [in ADT]QueueAbs [in ADT]

## R

RatherSlow [in Trie]## S

S [in Color]ScratchPad [in Decide]

ScratchPad2 [in Decide]

SigSandbox [in ADT]

SimpleStringTable1 [in ADT]

SimpleStringTable2 [in ADT]

SimpleStringTable3 [in ADT]

SimpleTable [in ADT]

SimpleTable2 [in ADT]

SimpleTable3 [in ADT]

StringListETableAbs [in ADT]

StringListsTableExamples [in ADT]

StringListsTableExamples.StringListsTable [in ADT]

StringTreeETableExample [in ADT]

StringTreeETableExample.StringTreeETable [in ADT]

StringVal [in ADT]

## T

Table [in ADT]Tests [in SearchTree]

TreeETable [in ADT]

TreeETableEncapsulated [in ADT]

TreeETableFullyEncapsulated [in ADT]

TreeETableSubset [in ADT]

TreeETable_first_attempt [in ADT]

TreeTable [in ADT]

TwoListQueueAbs [in ADT]

## V

ValType [in ADT]VerySlow [in Trie]

## W

WF [in Color]WP [in Color]

# Library Index

## A

ADT## B

BagPermBinom

## C

Color## D

Decide## E

Extract## M

MapsMerge

Multiset

## P

PermPreface

Priqueue

## R

Redblack## S

SearchTreeSelection

Sort

## T

Trie# Lemma Index

## A

adj_ext [in Color]apply_empty [in Maps]

## B

bag_eqv_iff_perm [in BagPerm]bag_perm [in BagPerm]

bag_cons_inv [in BagPerm]

bag_nil_inv [in BagPerm]

bag_eqv_cons [in BagPerm]

bag_eqv_trans [in BagPerm]

bag_eqv_sym [in BagPerm]

bag_eqv_refl [in BagPerm]

balanceP [in Redblack]

balance_lookup [in Redblack]

balance_BST [in Redblack]

balance_BST [in Redblack]

balance_BST [in Redblack]

BinomQueue.abs_perm [in Binom]

BinomQueue.can_relate [in Binom]

BinomQueue.carry_elems [in Binom]

BinomQueue.carry_valid [in Binom]

BinomQueue.delete_max_Some_relate [in Binom]

BinomQueue.delete_max_None_relate [in Binom]

BinomQueue.delete_max_Some_priq [in Binom]

BinomQueue.empty_relate [in Binom]

BinomQueue.empty_priq [in Binom]

BinomQueue.insert_relate [in Binom]

BinomQueue.insert_priq [in Binom]

BinomQueue.join_elems [in Binom]

BinomQueue.join_valid [in Binom]

BinomQueue.merge_relate [in Binom]

BinomQueue.merge_priq [in Binom]

BinomQueue.priqueue_elems_ext [in Binom]

BinomQueue.smash_elems [in Binom]

BinomQueue.smash_valid [in Binom]

BinomQueue.tree_can_relate [in Binom]

BinomQueue.tree_perm [in Binom]

BinomQueue.tree_elems_ext [in Binom]

bound_relate' [in SearchTree]

bound_relate [in SearchTree]

bound_value [in SearchTree]

bound_default [in SearchTree]

## C

cardinal_map [in Color]color_correct [in Color]

compute_with_StdLib_lt_dec [in Decide]

compute_with_lt_dec [in Decide]

cons_of_small_maintains_sort' [in Selection]

cons_of_small_maintains_sort [in Selection]

contents_perm [in Multiset]

contents_insert_other [in Multiset]

contents_cons_inv [in Multiset]

contents_nil_inv [in Multiset]

count_insert_other [in BagPerm]

## E

elements_relate' [in SearchTree]elements_relate [in SearchTree]

elements_empty [in SearchTree]

elements_nodup_keys [in SearchTree]

elements_correct_inverse [in SearchTree]

elements_complete_inverse [in SearchTree]

elements_correct [in SearchTree]

elements_preserves_relation [in SearchTree]

elements_preserves_forall [in SearchTree]

elements_complete [in SearchTree]

elements_complete_broken [in SearchTree]

empty_relate [in Trie]

empty_is_trie [in Trie]

empty_tree_BST [in Redblack]

empty_relate' [in SearchTree]

empty_relate [in SearchTree]

empty_tree_BST [in SearchTree]

eqb_reflect [in Perm]

eqlistA_Eeq_eq [in Color]

Even2 [in ADT]

## F

fast_elements_correct [in SearchTree]fast_elements_eq_elements [in SearchTree]

fast_elements_tr_helper [in SearchTree]

filter_sortE [in Color]

fold_right_rev_left [in Color]

ForallT_less [in Redblack]

ForallT_greater [in Redblack]

ForallT_imp [in Redblack]

ForallT_insert [in SearchTree]

Forall_perm [in Perm]

FunTable.get_set_other [in ADT]

FunTable.get_set_same [in ADT]

FunTable.get_empty_default [in ADT]

## G

geb_reflect [in Perm]gtb_reflect [in Perm]

## I

InA_map_fst_key [in Color]insertion_sort_correct [in Sort]

insertion_sort_correct [in BagPerm]

insertion_sort_correct [in Multiset]

insert_relate [in Trie]

insert_is_trie [in Trie]

insert_RB [in Redblack]

insert_BST [in Redblack]

insert_BST [in Redblack]

insert_relate' [in SearchTree]

insert_relate [in SearchTree]

insert_permute_equality_breaks [in SearchTree]

insert_same_equality_breaks [in SearchTree]

insert_shadow_equality [in SearchTree]

insert_BST [in SearchTree]

insert_sorted' [in Sort]

insert_perm [in Sort]

insert_sorted [in Sort]

insert_bag [in BagPerm]

insert_contents [in Multiset]

insP [in Redblack]

ins_red [in Redblack]

ins_RB [in Redblack]

ins_BST [in Redblack]

ins_not_E [in Redblack]

ins_not_E [in Redblack]

Integers.addc_correct [in Trie]

Integers.add_correct [in Trie]

Integers.compare_correct [in Trie]

Integers.positive2nat_pos [in Trie]

Integers.succ_correct [in Trie]

int_leb_reflect [in Extract]

int_ltb_reflect [in Extract]

in_colors_of_1 [in Color]

in_map_of_list [in SearchTree]

in_fst [in SearchTree]

## K

kvs_insert_elements [in SearchTree]kvs_insert_split [in SearchTree]

## L

leb_reflect [in Perm]le_all__le_one [in Selection]

lia_example_3 [in Perm]

lia_example2 [in Perm]

lia_example1 [in Perm]

lia_example1 [in Perm]

ListETableAbs.bound_relate [in ADT]

ListETableAbs.elements_relate [in ADT]

ListETableAbs.empty_relate [in ADT]

ListETableAbs.empty_ok [in ADT]

ListETableAbs.insert_relate [in ADT]

ListETableAbs.lookup_relate [in ADT]

ListETableAbs.set_ok [in ADT]

ListQueue.deq_nonempty [in ADT]

ListQueue.deq_empty [in ADT]

ListQueue.is_empty_nonempty [in ADT]

ListQueue.is_empty_empty [in ADT]

ListQueue.peek_nonempty [in ADT]

ListQueue.peek_empty [in ADT]

ListsTable.get_set_other [in ADT]

ListsTable.get_set_same [in ADT]

ListsTable.get_empty_default [in ADT]

List_Priqueue.merge_relate [in Priqueue]

List_Priqueue.merge_priq [in Priqueue]

List_Priqueue.delete_max_Some_relate [in Priqueue]

List_Priqueue.delete_max_None_relate [in Priqueue]

List_Priqueue.delete_max_Some_priq [in Priqueue]

List_Priqueue.insert_relate [in Priqueue]

List_Priqueue.insert_priq [in Priqueue]

List_Priqueue.empty_relate [in Priqueue]

List_Priqueue.empty_priq [in Priqueue]

List_Priqueue.abs_perm [in Priqueue]

List_Priqueue.can_relate [in Priqueue]

List_Priqueue.select_biggest [in Priqueue]

List_Priqueue.select_biggest_aux [in Priqueue]

List_Priqueue.select_perm [in Priqueue]

lookup_relate [in Trie]

lookup_insert_neq [in Redblack]

lookup_insert_eq [in Redblack]

lookup_ins_neq [in Redblack]

lookup_ins_eq [in Redblack]

lookup_empty [in Redblack]

lookup_relate' [in SearchTree]

lookup_relate [in SearchTree]

lookup_insert_permute [in SearchTree]

lookup_insert_same [in SearchTree]

lookup_insert_shadow [in SearchTree]

lookup_insert_neq [in SearchTree]

lookup_insert_eq' [in SearchTree]

lookup_insert_eq [in SearchTree]

lookup_empty [in SearchTree]

lookup_insert_neq [in Extract]

lookup_insert_eq [in Extract]

lookup_empty [in Extract]

look_ins_other [in Trie]

look_ins_same [in Trie]

look_leaf [in Trie]

ltb_reflect [in Perm]

lt_proper [in Color]

lt_strict [in Color]

## M

map_of_list_app [in SearchTree]map_of_tree_prop [in SearchTree]

maybe_swap_correct [in Perm]

maybe_swap_perm [in Perm]

maybe_swap_idempotent [in Perm]

maybe_swap_idempotent [in Perm]

mergesort_correct [in Merge]

mergesort_perm [in Merge]

mergesort_sorts [in Merge]

merge_perm [in Merge]

merge_nil_l [in Merge]

merge2 [in Merge]

Mremove_cardinal_less [in Color]

Mremove_elements [in Color]

## N

nat2pos_injective [in Trie]nat2pos2nat [in Trie]

NoDup_append [in SearchTree]

not_in_map_of_list [in SearchTree]

nth_error_insert [in Sort]

## P

perm_bag [in BagPerm]perm_contents [in Multiset]

pos2nat_injective [in Trie]

pos2nat2pos [in Trie]

Proper_eq_key_elt [in Color]

Proper_eq_eq [in Color]

## R

RB_blacken_root [in Redblack]RB_blacken_parent [in Redblack]

redblack_balanced [in Redblack]

## S

same_contents_iff_perm [in Multiset]ScratchPad.greater23 [in Decide]

ScratchPad.less37 [in Decide]

ScratchPad.lt_dec_equivalent [in Decide]

ScratchPad2.insert_sorted [in Decide]

ScratchPad2.prove_with_max_axiom [in Decide]

selection_sort_correct' [in Selection]

selection_sort_contents [in Selection]

selection_sort_is_correct [in Selection]

selection_sort_sorted [in Selection]

selection_sort_perm [in Selection]

select_terminates [in Color]

select_contents [in Selection]

select_in [in Selection]

select_smallest [in Selection]

select_fst_leq [in Selection]

select_rest_length [in Selection]

select_perm [in Selection]

selsort_sorted [in Selection]

selsort_perm [in Selection]

selsort'_is_correct [in Selection]

selsort'_sorted [in Selection]

selsort'_perm [in Selection]

Sin_domain [in Color]

Snot_in_empty [in Color]

Sorted_lt_key [in Color]

sorted_elements [in SearchTree]

sorted_app [in SearchTree]

sorted_sorted' [in Sort]

sorted_iff_sorted [in Selection]

sorted_merge [in Merge]

sorted_merge1 [in Merge]

sorted'_sorted [in Sort]

SortE_equivlistE_eqlistE [in Color]

sort_sorted' [in Sort]

sort_perm [in Sort]

sort_sorted [in Sort]

sort_specifications_equivalent [in BagPerm]

sort_bag [in BagPerm]

sort_specifications_equivalent [in Multiset]

sort_contents [in Multiset]

sort_int_correct [in Extract]

specialize_SortA_equivlistA_eqlistA [in Color]

split_perm [in Merge]

split_len [in Merge]

split_len' [in Merge]

split_len_first_try [in Merge]

Sremove_cardinal_less [in Color]

Sremove_elements [in Color]

Sremove_elements [in Color]

subset_nodes_sub [in Color]

## T

three_less_seven_2 [in Decide]three_less_seven_1 [in Decide]

TreeETableEncapsulated.bound_set_other [in ADT]

TreeETableEncapsulated.bound_set_same [in ADT]

TreeETableEncapsulated.bound_empty [in ADT]

TreeETableEncapsulated.elements_correct [in ADT]

TreeETableEncapsulated.elements_complete [in ADT]

TreeETableEncapsulated.empty_ok [in ADT]

TreeETableEncapsulated.set_ok [in ADT]

TreeETableFullyEncapsulated.bound_set_other [in ADT]

TreeETableFullyEncapsulated.bound_set_same [in ADT]

TreeETableFullyEncapsulated.bound_empty [in ADT]

TreeETableFullyEncapsulated.elements_correct [in ADT]

TreeETableFullyEncapsulated.elements_complete [in ADT]

TreeETableFullyEncapsulated.empty_ok [in ADT]

TreeETableFullyEncapsulated.set_ok [in ADT]

TreeETableSubset.bound_set_other [in ADT]

TreeETableSubset.bound_set_same [in ADT]

TreeETableSubset.bound_empty [in ADT]

TreeETableSubset.elements_correct [in ADT]

TreeETableSubset.elements_complete [in ADT]

TreeETableSubset.get_set_other [in ADT]

TreeETableSubset.get_set_same [in ADT]

TreeETableSubset.get_empty_default [in ADT]

TreeETable_first_attempt.elements_correct [in ADT]

TreeETable_first_attempt.elements_complete [in ADT]

TreeETable.bound_set_other [in ADT]

TreeETable.bound_set_same [in ADT]

TreeETable.bound_empty [in ADT]

TreeETable.elements_correct [in ADT]

TreeETable.elements_complete [in ADT]

TreeETable.empty_ok [in ADT]

TreeETable.set_ok [in ADT]

TreeTable.get_set_other [in ADT]

TreeTable.get_set_same [in ADT]

TreeTable.get_empty_default [in ADT]

truncated_subtraction [in Perm]

TwoListQueueAbs.deq_relate [in ADT]

TwoListQueueAbs.empty_relate [in ADT]

TwoListQueueAbs.enq_relate [in ADT]

TwoListQueueAbs.peek_relate [in ADT]

t_update_permute [in Maps]

t_update_same [in Maps]

t_update_shadow [in Maps]

t_update_neq [in Maps]

t_update_eq [in Maps]

t_apply_empty [in Maps]

## U

union_update_left [in SearchTree]union_update_right [in SearchTree]

union_both [in SearchTree]

union_right [in SearchTree]

union_left [in SearchTree]

union_swap [in Multiset]

union_comm [in Multiset]

union_assoc [in Multiset]

update_permute [in Maps]

update_same [in Maps]

update_shadow [in Maps]

update_neq [in Maps]

update_eq [in Maps]

## V

vector_app_correct [in ADT]vector_cons_correct [in ADT]

## Z

Z_geb_reflect [in Extract]Z_gtb_reflect [in Extract]

Z_leb_reflect [in Extract]

Z_ltb_reflect [in Extract]

Z_eqb_reflect [in Extract]

# Constructor Index

## B

BinomQueue.Leaf [in Binom]BinomQueue.Node [in Binom]

BinomQueue.tree_elems_node [in Binom]

BinomQueue.tree_elems_leaf [in Binom]

Black [in Redblack]

BST_T [in SearchTree]

BST_E [in SearchTree]

## E

E [in Redblack]E [in SearchTree]

E [in Extract]

## I

Integers.Eq [in Trie]Integers.Gt [in Trie]

Integers.Lt [in Trie]

Integers.xH [in Trie]

Integers.xI [in Trie]

Integers.xO [in Trie]

Integers.Zneg [in Trie]

Integers.Zpos [in Trie]

Integers.Z0 [in Trie]

## L

Leaf [in Trie]List_Priqueue.Abs_intro [in Priqueue]

## N

NearlyRB_b [in Redblack]NearlyRB_r [in Redblack]

Node [in Trie]

## R

RB_b [in Redblack]RB_r [in Redblack]

RB_leaf [in Redblack]

Red [in Redblack]

## S

ScratchPad.left [in Decide]ScratchPad.right [in Decide]

ScratchPad2.sorted_cons [in Decide]

ScratchPad2.sorted_1 [in Decide]

ScratchPad2.sorted_nil [in Decide]

SigSandbox.exist [in ADT]

SigSandbox.ex_intro [in ADT]

sorted_cons [in Sort]

sorted_1 [in Sort]

sorted_nil [in Sort]

sorted_cons [in Selection]

sorted_1 [in Selection]

sorted_nil [in Selection]

sorted_cons [in Extract]

sorted_1 [in Extract]

sorted_nil [in Extract]

ST_T [in Redblack]

ST_E [in Redblack]

## T

T [in Redblack]T [in SearchTree]

T [in Extract]

# Axiom Index

## A

Abs [in Extract]Abs_inj [in Extract]

## E

ETableAbs.Abs [in ADT]ETableAbs.bound [in ADT]

ETableAbs.bound_relate [in ADT]

ETableAbs.default [in ADT]

ETableAbs.elements [in ADT]

ETableAbs.elements_relate [in ADT]

ETableAbs.empty [in ADT]

ETableAbs.empty_relate [in ADT]

ETableAbs.empty_ok [in ADT]

ETableAbs.get [in ADT]

ETableAbs.insert_relate [in ADT]

ETableAbs.lookup_relate [in ADT]

ETableAbs.rep_ok [in ADT]

ETableAbs.set [in ADT]

ETableAbs.set_ok [in ADT]

ETableAbs.table [in ADT]

ETableAbs.V [in ADT]

ETableSubset.bound [in ADT]

ETableSubset.bound_set_other [in ADT]

ETableSubset.bound_set_same [in ADT]

ETableSubset.bound_empty [in ADT]

ETableSubset.elements [in ADT]

ETableSubset.elements_correct [in ADT]

ETableSubset.elements_complete [in ADT]

ETable_first_attempt.elements_correct [in ADT]

ETable_first_attempt.elements_complete [in ADT]

ETable_first_attempt.elements [in ADT]

ETable_first_attempt.bound [in ADT]

ETable.bound [in ADT]

ETable.bound_set_other [in ADT]

ETable.bound_set_same [in ADT]

ETable.bound_empty [in ADT]

ETable.elements [in ADT]

ETable.elements_correct [in ADT]

ETable.elements_complete [in ADT]

ETable.empty_ok [in ADT]

ETable.rep_ok [in ADT]

ETable.set_ok [in ADT]

## I

int [in Extract]## L

leb [in Extract]leb_le [in Extract]

ltb [in Extract]

ltb_lt [in Extract]

## P

PRIQUEUE.Abs [in Priqueue]PRIQUEUE.abs_perm [in Priqueue]

PRIQUEUE.can_relate [in Priqueue]

PRIQUEUE.delete_max_Some_relate [in Priqueue]

PRIQUEUE.delete_max_Some_priq [in Priqueue]

PRIQUEUE.delete_max_None_relate [in Priqueue]

PRIQUEUE.delete_max [in Priqueue]

PRIQUEUE.empty [in Priqueue]

PRIQUEUE.empty_relate [in Priqueue]

PRIQUEUE.empty_priq [in Priqueue]

PRIQUEUE.insert [in Priqueue]

PRIQUEUE.insert_relate [in Priqueue]

PRIQUEUE.insert_priq [in Priqueue]

PRIQUEUE.merge [in Priqueue]

PRIQUEUE.merge_relate [in Priqueue]

PRIQUEUE.merge_priq [in Priqueue]

PRIQUEUE.priq [in Priqueue]

PRIQUEUE.priqueue [in Priqueue]

## Q

QueueAbs.Abs [in ADT]QueueAbs.deq [in ADT]

QueueAbs.deq_relate [in ADT]

QueueAbs.empty [in ADT]

QueueAbs.empty_relate [in ADT]

QueueAbs.enq [in ADT]

QueueAbs.enq_relate [in ADT]

QueueAbs.is_empty [in ADT]

QueueAbs.peek [in ADT]

QueueAbs.peek_relate [in ADT]

QueueAbs.queue [in ADT]

QueueAbs.V [in ADT]

Queue.deq [in ADT]

Queue.deq_nonempty [in ADT]

Queue.deq_empty [in ADT]

Queue.empty [in ADT]

Queue.enq [in ADT]

Queue.is_empty_nonempty [in ADT]

Queue.is_empty_empty [in ADT]

Queue.is_empty [in ADT]

Queue.peek [in ADT]

Queue.peek_nonempty [in ADT]

Queue.peek_empty [in ADT]

Queue.queue [in ADT]

Queue.V [in ADT]

## S

ScratchPad2.lt_dec_axiom_2 [in Decide]ScratchPad2.lt_dec_axiom_1 [in Decide]

SimpleTable.default [in ADT]

SimpleTable.key [in ADT]

SimpleTable.table [in ADT]

SimpleTable.V [in ADT]

## T

Table.default [in ADT]Table.empty [in ADT]

Table.get [in ADT]

Table.get_set_other [in ADT]

Table.get_set_same [in ADT]

Table.get_empty_default [in ADT]

Table.set [in ADT]

Table.table [in ADT]

Table.V [in ADT]

## V

ValType.default [in ADT]ValType.V [in ADT]

# Inductive Index

## B

BinomQueue.priqueue_elems [in Binom]BinomQueue.tree [in Binom]

BinomQueue.tree_elems [in Binom]

BST [in Redblack]

BST [in SearchTree]

## C

color [in Redblack]## I

Integers.comparison [in Trie]Integers.positive [in Trie]

Integers.Z [in Trie]

## L

List_Priqueue.Abs' [in Priqueue]## N

NearlyRB [in Redblack]## R

RB [in Redblack]## S

ScratchPad.sumbool [in Decide]ScratchPad2.sorted [in Decide]

SigSandbox.ex [in ADT]

SigSandbox.sig [in ADT]

sorted [in Sort]

sorted [in Selection]

sorted [in Extract]

## T

tree [in Redblack]tree [in SearchTree]

tree [in Extract]

trie [in Trie]

# Definition Index

## A

Abs [in Trie]Abs [in SearchTree]

abstract [in Trie]

Abs_three_ten [in Trie]

Abs' [in SearchTree]

add_edge [in Color]

adj [in Color]

a_vector [in ADT]

## B

bag [in BagPerm]bag_eqv [in BagPerm]

balance [in Redblack]

BinomQueue.Abs [in Binom]

BinomQueue.carry [in Binom]

BinomQueue.delete_max [in Binom]

BinomQueue.delete_max_aux [in Binom]

BinomQueue.empty [in Binom]

BinomQueue.find_max [in Binom]

BinomQueue.find_max' [in Binom]

BinomQueue.heap_delete_max [in Binom]

BinomQueue.insert [in Binom]

BinomQueue.join [in Binom]

BinomQueue.key [in Binom]

BinomQueue.manual_grade_for_priqueue_elems [in Binom]

BinomQueue.merge [in Binom]

BinomQueue.pow2heap [in Binom]

BinomQueue.pow2heap' [in Binom]

BinomQueue.priq [in Binom]

BinomQueue.priqueue [in Binom]

BinomQueue.priq' [in Binom]

BinomQueue.smash [in Binom]

BinomQueue.unzip [in Binom]

bound [in SearchTree]

butterfly [in Perm]

## C

color [in Color]coloring [in Color]

coloring_ok [in Color]

colors_of [in Color]

color1 [in Color]

contents [in Multiset]

count [in BagPerm]

## D

disjoint [in SearchTree]domain_example_map [in Color]

## E

elements [in Redblack]elements [in SearchTree]

elements [in Extract]

elements_aux [in Redblack]

elements_correct_spec [in SearchTree]

elements_complete_spec [in SearchTree]

elements_complete_broken_spec [in SearchTree]

elements_ex [in SearchTree]

elements_aux [in Extract]

empty [in Trie]

empty [in Multiset]

empty [in Maps]

empty_tree [in Redblack]

empty_tree [in SearchTree]

empty_map [in ADT]

empty_tree [in Extract]

equivlistA_example [in Color]

ETableAbs.key [in ADT]

even_nat [in ADT]

Even2' [in ADT]

examplemap [in Maps]

example_map [in Color]

exposed_trees_ex [in ADT]

extra_fuel [in Selection]

ex_tree [in SearchTree]

## F

FastEnough.collisions [in Trie]FastEnough.collisions_pi [in Trie]

FastEnough.loop [in Trie]

fast_elements [in SearchTree]

fast_elements_tr [in SearchTree]

find [in SearchTree]

first_le_second [in Perm]

ForallT [in Redblack]

ForallT [in SearchTree]

FunTableExamples.ex1 [in ADT]

FunTableExamples.ex2 [in ADT]

FunTableExamples.ex3 [in ADT]

FunTable.default [in ADT]

FunTable.empty [in ADT]

FunTable.get [in ADT]

FunTable.key [in ADT]

FunTable.set [in ADT]

FunTable.table [in ADT]

FunTable.V [in ADT]

## G

G [in Color]geb [in Perm]

graph [in Color]

gtb [in Perm]

## H

height [in Redblack]## I

InA_example [in Color]ins [in Trie]

ins [in Redblack]

ins [in Extract]

insert [in Trie]

insert [in Redblack]

insert [in SearchTree]

insert [in Sort]

insert [in Extract]

insZ [in Extract]

ins_int [in Extract]

Integers.add [in Trie]

Integers.addc [in Trie]

Integers.compare [in Trie]

Integers.positive2nat [in Trie]

Integers.print_in_binary [in Trie]

Integers.succ [in Trie]

Integers.ten [in Trie]

in_4_pi [in Decide]

is_trie [in Trie]

is_BST_ex [in SearchTree]

is_a_sorting_algorithm [in Sort]

is_a_sorting_algorithm' [in BagPerm]

is_a_sorting_algorithm [in Selection]

is_a_sorting_algorithm' [in Multiset]

## K

key [in Redblack]key [in SearchTree]

key [in Extract]

kvs_insert [in SearchTree]

## L

le_all [in Selection]ListETableAbs.Abs [in ADT]

ListETableAbs.bound [in ADT]

ListETableAbs.default [in ADT]

ListETableAbs.elements [in ADT]

ListETableAbs.empty [in ADT]

ListETableAbs.get [in ADT]

ListETableAbs.key [in ADT]

ListETableAbs.rep_ok [in ADT]

ListETableAbs.set [in ADT]

ListETableAbs.table [in ADT]

ListETableAbs.V [in ADT]

ListQueue.deq [in ADT]

ListQueue.empty [in ADT]

ListQueue.enq [in ADT]

ListQueue.is_empty [in ADT]

ListQueue.peek [in ADT]

ListQueue.queue [in ADT]

ListQueue.V [in ADT]

ListsTable.default [in ADT]

ListsTable.empty [in ADT]

ListsTable.get [in ADT]

ListsTable.key [in ADT]

ListsTable.set [in ADT]

ListsTable.table [in ADT]

ListsTable.V [in ADT]

List_Priqueue.Abs [in Priqueue]

List_Priqueue.priq [in Priqueue]

List_Priqueue.merge [in Priqueue]

List_Priqueue.delete_max [in Priqueue]

List_Priqueue.insert [in Priqueue]

List_Priqueue.empty [in Priqueue]

List_Priqueue.priqueue [in Priqueue]

List_Priqueue.key [in Priqueue]

List_Priqueue.select [in Priqueue]

list_keys [in SearchTree]

list_nat_in [in Decide]

list_nat_eq_dec [in Decide]

list_of_vector [in ADT]

list_ind2 [in Merge]

list_ind2_principle [in Merge]

look [in Trie]

lookup [in Trie]

lookup [in Redblack]

lookup [in SearchTree]

lookup [in Extract]

low_deg [in Color]

## M

make_black [in Redblack]manual_grade_for_successor_of_Z_constant_time [in Trie]

manual_grade_for_redblack_bound [in Redblack]

manual_grade_for_bound_correct [in SearchTree]

manual_grade_for_permutations_vs_multiset [in BagPerm]

manual_grade_for_Permutation_properties [in Perm]

manual_grade_for_ListsETable [in ADT]

manual_grade_for_TreeTableModel [in ADT]

manual_grade_for_permutations_vs_multiset [in Multiset]

map_of_tree [in SearchTree]

map_bound [in SearchTree]

map_of_list [in SearchTree]

map_find [in ADT]

map_update [in ADT]

maybe_swap_321 [in Perm]

maybe_swap_123 [in Perm]

maybe_swap [in Perm]

Mdomain [in Color]

merge [in Merge]

mindepth [in Redblack]

mk_graph [in Color]

multiset [in Multiset]

## N

nat2pos [in Trie]NicelyEncapsulatedExample.ex1 [in ADT]

NicelyEncapsulatedExample.ex2 [in ADT]

node [in Color]

nodemap [in Color]

nodes [in Color]

nodeset [in Color]

NotBst.not_bst_lookup_wrong [in SearchTree]

NotBst.t [in SearchTree]

not_BST_ex [in SearchTree]

not_a_permutation [in Perm]

no_selfloop [in Color]

## O

out_of_fuel [in Selection]OverlyEncapsulatedExample.ex1 [in ADT]

## P

pairs_example [in Selection]palette [in Color]

partial_map [in Maps]

permut_example [in Perm]

plus_two [in ADT]

plus_two [in ADT]

pos2nat [in Trie]

PRIQUEUE.key [in Priqueue]

## R

RatherSlow.collisions [in Trie]RatherSlow.collisions_pi [in Trie]

RatherSlow.empty [in Trie]

RatherSlow.loop [in Trie]

RatherSlow.total_mapz [in Trie]

RatherSlow.update [in Trie]

reflect_example2 [in Perm]

reflect_example1' [in Perm]

reflect_example1 [in Perm]

remove_node [in Color]

## S

same_mod_10 [in Color]ScratchPad.is_3_less_7 [in Decide]

ScratchPad.lt_dec' [in Decide]

ScratchPad.lt_dec [in Decide]

ScratchPad.t1 [in Decide]

ScratchPad.t2 [in Decide]

ScratchPad.t4 [in Decide]

ScratchPad.v1a [in Decide]

ScratchPad.v1b [in Decide]

ScratchPad.v2a [in Decide]

ScratchPad.v3 [in Decide]

ScratchPad2.insert [in Decide]

ScratchPad2.le_dec [in Decide]

ScratchPad2.lt_dec [in Decide]

ScratchPad2.max_with_axiom [in Decide]

ScratchPad2.sort [in Decide]

select [in Selection]

selection_sort [in Selection]

selsort [in Selection]

selsort [in Selection]

selsort'_example [in Selection]

SigSandbox.proj1_ex [in ADT]

SigSandbox.proj1_sig [in ADT]

SigSandbox.proj2_sig [in ADT]

SimpleStringTable1.default [in ADT]

SimpleStringTable1.key [in ADT]

SimpleStringTable1.table [in ADT]

SimpleStringTable1.V [in ADT]

SimpleStringTable2.default [in ADT]

SimpleStringTable2.key [in ADT]

SimpleStringTable2.table [in ADT]

SimpleStringTable2.V [in ADT]

SimpleStringTable3.default [in ADT]

SimpleStringTable3.key [in ADT]

SimpleStringTable3.table [in ADT]

SimpleStringTable3.V [in ADT]

singleton [in Multiset]

sort [in Sort]

sort [in Extract]

sorted' [in Sort]

sorted'' [in Sort]

sortZ [in Extract]

sort_pi [in Sort]

sort_pi [in Selection]

sort_pi_same_contents [in Multiset]

sort_int [in Extract]

split [in Merge]

StringListsTableExamples.ex1 [in ADT]

StringListsTableExamples.ex2 [in ADT]

StringListsTableExamples.ex3 [in ADT]

StringTreeETableExample.ex1 [in ADT]

StringVal.default [in ADT]

StringVal.V [in ADT]

subset_nodes [in Color]

## T

Table.key [in ADT]Tests.bst_ex

_{4}[in SearchTree]

Tests.bst_ex

_{3}[in SearchTree]

Tests.bst_ex

_{2}[in SearchTree]

Tests.bst_ex

_{1}[in SearchTree]

three_ten [in Trie]

total_map [in Maps]

TreeETableEncapsulated.bound [in ADT]

TreeETableEncapsulated.elements [in ADT]

TreeETableEncapsulated.rep_ok [in ADT]

TreeETableFullyEncapsulated.bound [in ADT]

TreeETableFullyEncapsulated.elements [in ADT]

TreeETableFullyEncapsulated.rep_ok [in ADT]

TreeETableSubset.bound [in ADT]

TreeETableSubset.default [in ADT]

TreeETableSubset.elements [in ADT]

TreeETableSubset.empty [in ADT]

TreeETableSubset.get [in ADT]

TreeETableSubset.key [in ADT]

TreeETableSubset.set [in ADT]

TreeETableSubset.table [in ADT]

TreeETableSubset.V [in ADT]

TreeETable_first_attempt.elements [in ADT]

TreeETable_first_attempt.bound [in ADT]

TreeETable.bound [in ADT]

TreeETable.elements [in ADT]

TreeETable.rep_ok [in ADT]

TreeTable.default [in ADT]

TreeTable.empty [in ADT]

TreeTable.get [in ADT]

TreeTable.key [in ADT]

TreeTable.set [in ADT]

TreeTable.table [in ADT]

TreeTable.V [in ADT]

trie_table [in Trie]

two [in ADT]

two [in ADT]

TwoListQueueAbs.Abs [in ADT]

TwoListQueueAbs.deq [in ADT]

TwoListQueueAbs.empty [in ADT]

TwoListQueueAbs.enq [in ADT]

TwoListQueueAbs.is_empty [in ADT]

TwoListQueueAbs.peek [in ADT]

TwoListQueueAbs.queue [in ADT]

TwoListQueueAbs.V [in ADT]

two' [in ADT]

t_update [in Maps]

t_empty [in Maps]

## U

uncurry [in SearchTree]undirected [in Color]

union [in SearchTree]

union [in Multiset]

Unnamed_thm [in Trie]

Unnamed_thm0 [in Color]

Unnamed_thm [in Color]

Unnamed_thm [in Decide]

update [in Maps]

update_example4 [in Maps]

update_example3 [in Maps]

update_example2 [in Maps]

update_example1 [in Maps]

## V

value [in Multiset]vector [in ADT]

vector_app [in ADT]

vector_cons [in ADT]

VerySlow.collisions [in Trie]

VerySlow.collisions_pi [in Trie]

VerySlow.loop [in Trie]

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 | (2702 entries) |

Notation 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 | (7 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 | (1773 entries) |

Module 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 | (55 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 | (17 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 | (330 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 | (49 entries) |

Axiom 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 | (105 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 | (23 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 | (343 entries) |

This page has been generated by coqdoc