| 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]
b1:11 [binder, in BagPerm]
b1:15 [binder, in BagPerm]
b1:5 [binder, in BagPerm]
b1:9 [binder, in BagPerm]
b2:10 [binder, in BagPerm]
b2:12 [binder, in BagPerm]
b2:16 [binder, in BagPerm]
b2:6 [binder, in BagPerm]
b3: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]
el1:345 [binder, in SearchTree]
el2: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]
e1:102 [binder, in Binom]
e1:242 [binder, in SearchTree]
e1:96 [binder, in Binom]
e1:99 [binder, in Binom]
e2:100 [binder, in Binom]
e2:103 [binder, in Binom]
e2:243 [binder, in SearchTree]
e2: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]H0:33 [binder, in Merge]
H1: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]
k0:101 [binder, in Redblack]
k0:245 [binder, in SearchTree]
k0:95 [binder, in Redblack]
k1:110 [binder, in SearchTree]
k1:129 [binder, in SearchTree]
k1:145 [binder, in SearchTree]
k2:111 [binder, in SearchTree]
k2:130 [binder, in SearchTree]
k2: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]
l1:102 [binder, in Merge]
l1:197 [binder, in SearchTree]
l1:20 [binder, in Merge]
l1:207 [binder, in SearchTree]
l1:211 [binder, in SearchTree]
l1:28 [binder, in BagPerm]
l1:30 [binder, in BagPerm]
l1:30 [binder, in Multiset]
l1:32 [binder, in Multiset]
l1:43 [binder, in Merge]
l1:47 [binder, in Merge]
l1:49 [binder, in Merge]
l1:5 [binder, in Merge]
l1:65 [binder, in Merge]
l1:72 [binder, in Merge]
l1:77 [binder, in Merge]
l1:9 [binder, in Merge]
l1:96 [binder, in Merge]
l1:99 [binder, in Merge]
l2:10 [binder, in Merge]
l2:100 [binder, in Merge]
l2:103 [binder, in Merge]
l2:198 [binder, in SearchTree]
l2:208 [binder, in SearchTree]
l2:21 [binder, in Merge]
l2:212 [binder, in SearchTree]
l2:29 [binder, in BagPerm]
l2:31 [binder, in BagPerm]
l2:31 [binder, in Multiset]
l2:33 [binder, in Multiset]
l2:44 [binder, in Merge]
l2:48 [binder, in Merge]
l2:50 [binder, in Merge]
l2:52 [binder, in Merge]
l2:6 [binder, in Merge]
l2:66 [binder, in Merge]
l2:73 [binder, in Merge]
l2:78 [binder, in Merge]
l2: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]
m1:294 [binder, in SearchTree]
m1:298 [binder, in SearchTree]
m1:302 [binder, in SearchTree]
m1:306 [binder, in SearchTree]
m1:312 [binder, in SearchTree]
m1:317 [binder, in SearchTree]
m2:295 [binder, in SearchTree]
m2:299 [binder, in SearchTree]
m2:303 [binder, in SearchTree]
m2:307 [binder, in SearchTree]
m2:313 [binder, in SearchTree]
m2: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]
r1:59 [binder, in Merge]
r2: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_ex4 [definition, in SearchTree]
Tests.bst_ex3 [definition, in SearchTree]
Tests.bst_ex2 [definition, in SearchTree]
Tests.bst_ex1 [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]
t1:15 [binder, in Redblack]
t2: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]
v0:241 [binder, in SearchTree]
v1:101 [binder, in SearchTree]
v1:108 [binder, in SearchTree]
v1:126 [binder, in SearchTree]
v1:143 [binder, in SearchTree]
v1:23 [binder, in Maps]
v1:30 [binder, in Maps]
v1:309 [binder, in SearchTree]
v1:351 [binder, in ADT]
v1:354 [binder, in ADT]
v1:54 [binder, in Maps]
v1:62 [binder, in Maps]
v2:102 [binder, in SearchTree]
v2:109 [binder, in SearchTree]
v2:127 [binder, in SearchTree]
v2:144 [binder, in SearchTree]
v2:24 [binder, in Maps]
v2:31 [binder, in Maps]
v2:310 [binder, in SearchTree]
v2:352 [binder, in ADT]
v2:355 [binder, in ADT]
v2:55 [binder, in Maps]
v2: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]
x1:18 [binder, in Maps]
x1:32 [binder, in Maps]
x1:49 [binder, in Maps]
x1:57 [binder, in Merge]
x1:64 [binder, in Maps]
x1:95 [binder, in Merge]
x2:19 [binder, in Maps]
x2:33 [binder, in Maps]
x2:50 [binder, in Maps]
x2:58 [binder, in Merge]
x2:65 [binder, in Maps]
x2: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]
b1:11 [in BagPerm]
b1:15 [in BagPerm]
b1:5 [in BagPerm]
b1:9 [in BagPerm]
b2:10 [in BagPerm]
b2:12 [in BagPerm]
b2:16 [in BagPerm]
b2:6 [in BagPerm]
b3: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
el1:345 [in SearchTree]el2: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]
e1:102 [in Binom]
e1:242 [in SearchTree]
e1:96 [in Binom]
e1:99 [in Binom]
e2:100 [in Binom]
e2:103 [in Binom]
e2:243 [in SearchTree]
e2: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
H0:33 [in Merge]H1: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]
k0:101 [in Redblack]
k0:245 [in SearchTree]
k0:95 [in Redblack]
k1:110 [in SearchTree]
k1:129 [in SearchTree]
k1:145 [in SearchTree]
k2:111 [in SearchTree]
k2:130 [in SearchTree]
k2: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]
l1:102 [in Merge]
l1:197 [in SearchTree]
l1:20 [in Merge]
l1:207 [in SearchTree]
l1:211 [in SearchTree]
l1:28 [in BagPerm]
l1:30 [in BagPerm]
l1:30 [in Multiset]
l1:32 [in Multiset]
l1:43 [in Merge]
l1:47 [in Merge]
l1:49 [in Merge]
l1:5 [in Merge]
l1:65 [in Merge]
l1:72 [in Merge]
l1:77 [in Merge]
l1:9 [in Merge]
l1:96 [in Merge]
l1:99 [in Merge]
l2:10 [in Merge]
l2:100 [in Merge]
l2:103 [in Merge]
l2:198 [in SearchTree]
l2:208 [in SearchTree]
l2:21 [in Merge]
l2:212 [in SearchTree]
l2:29 [in BagPerm]
l2:31 [in BagPerm]
l2:31 [in Multiset]
l2:33 [in Multiset]
l2:44 [in Merge]
l2:48 [in Merge]
l2:50 [in Merge]
l2:52 [in Merge]
l2:6 [in Merge]
l2:66 [in Merge]
l2:73 [in Merge]
l2:78 [in Merge]
l2: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]m1:294 [in SearchTree]
m1:298 [in SearchTree]
m1:302 [in SearchTree]
m1:306 [in SearchTree]
m1:312 [in SearchTree]
m1:317 [in SearchTree]
m2:295 [in SearchTree]
m2:299 [in SearchTree]
m2:303 [in SearchTree]
m2:307 [in SearchTree]
m2:313 [in SearchTree]
m2: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]
r1:59 [in Merge]
r2: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]
t1:15 [in Redblack]
t2: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]
v0:241 [in SearchTree]
v1:101 [in SearchTree]
v1:108 [in SearchTree]
v1:126 [in SearchTree]
v1:143 [in SearchTree]
v1:23 [in Maps]
v1:30 [in Maps]
v1:309 [in SearchTree]
v1:351 [in ADT]
v1:354 [in ADT]
v1:54 [in Maps]
v1:62 [in Maps]
v2:102 [in SearchTree]
v2:109 [in SearchTree]
v2:127 [in SearchTree]
v2:144 [in SearchTree]
v2:24 [in Maps]
v2:31 [in Maps]
v2:310 [in SearchTree]
v2:352 [in ADT]
v2:355 [in ADT]
v2:55 [in Maps]
v2: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]
x1:18 [in Maps]
x1:32 [in Maps]
x1:49 [in Maps]
x1:57 [in Merge]
x1:64 [in Maps]
x1:95 [in Merge]
x2:19 [in Maps]
x2:33 [in Maps]
x2:50 [in Maps]
x2:58 [in Merge]
x2:65 [in Maps]
x2: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
ADTB
BagPermBinom
C
ColorD
DecideE
ExtractM
MapsMerge
Multiset
P
PermPreface
Priqueue
R
RedblackS
SearchTreeSelection
Sort
T
TrieLemma 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_ex4 [in SearchTree]
Tests.bst_ex3 [in SearchTree]
Tests.bst_ex2 [in SearchTree]
Tests.bst_ex1 [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