Volume 3: Verified Functional Algorithms

• Table of Contents
• Index
• Roadmap

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

:

_

(652 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

:

_

(5 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

_

(28 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(16 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

_

(14 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

_

(37 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

_

(225 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

_

(52 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

_

(26 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(8 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

_

(241 entries)

---

Global Index

A

Abs [definition, in VFA.Trie]
Abs [inductive, in VFA.SearchTree]
Abs [inductive, in VFA.Redblack]
abstract [definition, in VFA.Trie]
abstraction_of_bogus_tree [lemma, in VFA.SearchTree]
AbsX [definition, in VFA.SearchTree]
Abs_E [constructor, in VFA.SearchTree]
Abs_E [constructor, in VFA.Redblack]
Abs_helper [lemma, in VFA.Redblack]
Abs_T [constructor, in VFA.SearchTree]
Abs_T [constructor, in VFA.Redblack]
Abs_three_ten [definition, in VFA.Trie]
Abs_T_aux [lemma, in VFA.SearchTree]
add_edge [definition, in VFA.Color]
adj [definition, in VFA.Color]
adj_ext [lemma, in VFA.Color]
ADT [library]
ADT_SUMMARY [section, in VFA.ADT]
ADT_SUMMARY.default [variable, in VFA.ADT]
ADT_SUMMARY.V [variable, in VFA.ADT]

B

balance [definition, in VFA.Redblack]
balance_relate [lemma, in VFA.Redblack]
balance_SearchTree [lemma, in VFA.Redblack]
balance_SearchTree [lemma, in VFA.Redblack]
balance_SearchTree [lemma, in VFA.Redblack]
Binom [library]
BinomQueue [module, in VFA.Binom]
BinomQueue.Abs [definition, in VFA.Binom]
BinomQueue.abs_perm [lemma, in VFA.Binom]
BinomQueue.can_relate [lemma, in VFA.Binom]
BinomQueue.carry [definition, in VFA.Binom]
BinomQueue.carry_elems [lemma, in VFA.Binom]
BinomQueue.carry_valid [lemma, in VFA.Binom]
BinomQueue.delete_max [definition, in VFA.Binom]
BinomQueue.delete_max_aux [definition, in VFA.Binom]
BinomQueue.delete_max_None_relate [lemma, in VFA.Binom]
BinomQueue.delete_max_Some_priq [lemma, in VFA.Binom]
BinomQueue.delete_max_Some_relate [lemma, in VFA.Binom]
BinomQueue.empty [definition, in VFA.Binom]
BinomQueue.empty_priq [lemma, in VFA.Binom]
BinomQueue.empty_relate [lemma, in VFA.Binom]
BinomQueue.find_max [definition, in VFA.Binom]
BinomQueue.find_max' [definition, in VFA.Binom]
BinomQueue.heap_delete_max [definition, in VFA.Binom]
BinomQueue.insert [definition, in VFA.Binom]
BinomQueue.insert_priq [lemma, in VFA.Binom]
BinomQueue.insert_relate [lemma, in VFA.Binom]
BinomQueue.join [definition, in VFA.Binom]
BinomQueue.join_elems [lemma, in VFA.Binom]
BinomQueue.join_valid [lemma, in VFA.Binom]
BinomQueue.key [definition, in VFA.Binom]
BinomQueue.Leaf [constructor, in VFA.Binom]
BinomQueue.manual_grade_for_priqueue_elems [definition, in VFA.Binom]
BinomQueue.merge [definition, in VFA.Binom]
BinomQueue.merge_priq [lemma, in VFA.Binom]
BinomQueue.merge_relate [lemma, in VFA.Binom]
BinomQueue.Node [constructor, in VFA.Binom]
BinomQueue.pow2heap [definition, in VFA.Binom]
BinomQueue.pow2heap' [definition, in VFA.Binom]
BinomQueue.priq [definition, in VFA.Binom]
BinomQueue.priqueue [definition, in VFA.Binom]
BinomQueue.priqueue_elems [inductive, in VFA.Binom]
BinomQueue.priqueue_elems_ext [lemma, in VFA.Binom]
BinomQueue.priq' [definition, in VFA.Binom]
BinomQueue.smash [definition, in VFA.Binom]
BinomQueue.smash_elems [lemma, in VFA.Binom]
BinomQueue.smash_valid [lemma, in VFA.Binom]
BinomQueue.tree [inductive, in VFA.Binom]
BinomQueue.tree_can_relate [lemma, in VFA.Binom]
BinomQueue.tree_elems [inductive, in VFA.Binom]
BinomQueue.tree_elems_ext [lemma, in VFA.Binom]
BinomQueue.tree_elems_leaf [constructor, in VFA.Binom]
BinomQueue.tree_elems_node [constructor, in VFA.Binom]
BinomQueue.tree_perm [lemma, in VFA.Binom]
BinomQueue.unzip [definition, in VFA.Binom]
Black [constructor, in VFA.Redblack]

C

can_relate [lemma, in VFA.SearchTree]
cardinal_map [lemma, in VFA.Color]
check_example_map [lemma, in VFA.SearchTree]
color [inductive, in VFA.Redblack]
color [definition, in VFA.Color]
Color [library]
coloring [definition, in VFA.Color]
coloring_ok [definition, in VFA.Color]
colors_of [definition, in VFA.Color]
color1 [definition, in VFA.Color]
color_correct [lemma, in VFA.Color]
combine [definition, in VFA.Redblack]
combine [definition, in VFA.SearchTree]
compute_with_lt_dec [lemma, in VFA.Decide]
compute_with_StdLib_lt_dec [lemma, in VFA.Decide]
cons_relate [lemma, in VFA.ADT]
contents [definition, in VFA.Multiset]
contents_in [lemma, in VFA.Multiset]
contents_perm [lemma, in VFA.Multiset]
contents_perm_aux [lemma, in VFA.Multiset]
create_relate [lemma, in VFA.ADT]

D

Decide [library]
delete_contents [lemma, in VFA.Multiset]
domain_example_map [definition, in VFA.Color]

E

E [constructor, in VFA.SearchTree]
E [module, in VFA.Color]
E [constructor, in VFA.Redblack]
elements [definition, in VFA.Redblack]
elements [definition, in VFA.SearchTree]
elements' [definition, in VFA.Redblack]
elements' [definition, in VFA.SearchTree]
elements_property [definition, in VFA.Redblack]
elements_relate [lemma, in VFA.SearchTree]
elements_relate [lemma, in VFA.SearchTree]
elements_relate [lemma, in VFA.Redblack]
elements_relateX [lemma, in VFA.SearchTree]
elements_relate_second_attempt [lemma, in VFA.SearchTree]
elements_slow_elements [lemma, in VFA.SearchTree]
empty [definition, in VFA.Trie]
empty [definition, in VFA.Multiset]
empty_equiv [lemma, in VFA.SearchTree]
empty_is_trie [lemma, in VFA.Trie]
empty_rb [lemma, in VFA.Redblack]
empty_relate [lemma, in VFA.Trie]
empty_SearchTree [lemma, in VFA.Redblack]
empty_tree [definition, in VFA.SearchTree]
empty_tree [definition, in VFA.Redblack]
empty_tree_relate [lemma, in VFA.SearchTree]
empty_tree_relate [lemma, in VFA.Redblack]
empty_tree_SearchTree [lemma, in VFA.SearchTree]
eqb_reflect [lemma, in VFA.Perm]
eqlistA_Eeq_eq [lemma, in VFA.Color]
equivlistA_example [definition, in VFA.Color]
even_nat [definition, in VFA.ADT]
even_zero [definition, in VFA.ADT]
example_map [definition, in VFA.Color]
example_map [definition, in VFA.SearchTree]
example_map_default [definition, in VFA.SearchTree]
example_map_2 [definition, in VFA.SearchTree]
example_map_4 [definition, in VFA.SearchTree]
example_map_5 [definition, in VFA.SearchTree]
example_SearchTree_bad [lemma, in VFA.SearchTree]
example_SearchTree_good [lemma, in VFA.SearchTree]
example_tree [definition, in VFA.SearchTree]
expand_range_SearchTree' [lemma, in VFA.Redblack]
Experiments [module, in VFA.Extract]
Experiments.consecutive [definition, in VFA.Extract]
Experiments.E [definition, in VFA.Extract]
Experiments.empty_tree [definition, in VFA.Extract]
Experiments.insert [definition, in VFA.Extract]
Experiments.lookup [definition, in VFA.Extract]
Experiments.T [definition, in VFA.Extract]
Exploration1 [module, in VFA.Perm]
Exploration1.bogus_subtraction [lemma, in VFA.Perm]
Exploration1.butterfly [definition, in VFA.Perm]
Exploration1.first_le_second [definition, in VFA.Perm]
Exploration1.manual_grade_for_Permutation_properties [definition, in VFA.Perm]
Exploration1.maybe_swap [definition, in VFA.Perm]
Exploration1.maybe_swap_correct [lemma, in VFA.Perm]
Exploration1.maybe_swap_idempotent [lemma, in VFA.Perm]
Exploration1.maybe_swap_idempotent [lemma, in VFA.Perm]
Exploration1.maybe_swap_idempotent' [lemma, in VFA.Perm]
Exploration1.maybe_swap_perm [lemma, in VFA.Perm]
Exploration1.maybe_swap_123 [definition, in VFA.Perm]
Exploration1.maybe_swap_321 [definition, in VFA.Perm]
Exploration1.not_a_permutation [definition, in VFA.Perm]
Exploration1.omega_example1 [lemma, in VFA.Perm]
Exploration1.omega_example1 [lemma, in VFA.Perm]
Exploration1.omega_example2 [lemma, in VFA.Perm]
Exploration1.permut_example [definition, in VFA.Perm]
Extract [library]
ex_t [definition, in VFA.ADT]

F

FastEnough [module, in VFA.Trie]
FastEnough.collisions [definition, in VFA.Trie]
FastEnough.collisions_pi [definition, in VFA.Trie]
FastEnough.loop [definition, in VFA.Trie]
fib [definition, in VFA.ADT]
fibish [definition, in VFA.ADT]
fibish_correct [lemma, in VFA.ADT]
fibonacci [definition, in VFA.ADT]
filter_sortE [lemma, in VFA.Color]
fold_right_rev_left [lemma, in VFA.Color]
forall_nodes [definition, in VFA.SearchTree]
Forall_nth [lemma, in VFA.Sort]
Forall_perm [lemma, in VFA.Perm]

G

G [definition, in VFA.Color]
graph [definition, in VFA.Color]

I

InA_example [definition, in VFA.Color]
InA_map_fst_key [lemma, in VFA.Color]
ins [definition, in VFA.Trie]
ins [definition, in VFA.Redblack]
insert [definition, in VFA.Redblack]
insert [definition, in VFA.Trie]
insert [definition, in VFA.SearchTree]
insert [definition, in VFA.Sort]
insertion_sort_correct [lemma, in VFA.Sort]
insertion_sort_correct [lemma, in VFA.Multiset]
insert_contents [lemma, in VFA.Multiset]
insert_is_redblack [lemma, in VFA.Redblack]
insert_is_trie [lemma, in VFA.Trie]
insert_perm [lemma, in VFA.Sort]
insert_rb [lemma, in VFA.Redblack]
insert_relate [lemma, in VFA.SearchTree]
insert_relate [lemma, in VFA.Trie]
insert_relate [lemma, in VFA.Redblack]
insert_relate' [lemma, in VFA.SearchTree]
insert_SearchTree [lemma, in VFA.Redblack]
insert_SearchTree [lemma, in VFA.SearchTree]
insert_sorted [lemma, in VFA.Sort]
insert_sorted' [lemma, in VFA.Sort]
ins_black [lemma, in VFA.Redblack]
ins_E_SearchTree [lemma, in VFA.Redblack]
ins_is_redblack [lemma, in VFA.Redblack]
ins_left [lemma, in VFA.Redblack]
ins_makeBlack_SearchTree [lemma, in VFA.Redblack]
ins_not_E [lemma, in VFA.Redblack]
ins_not_E [lemma, in VFA.Redblack]
ins_not_E [lemma, in VFA.Redblack]
ins_red [lemma, in VFA.Redblack]
ins_relate [lemma, in VFA.Redblack]
ins_right [lemma, in VFA.Redblack]
ins_SearchTree [lemma, in VFA.Redblack]
ins_T_SearchTree [lemma, in VFA.Redblack]
ins_T_SearchTree_aux [lemma, in VFA.Redblack]
int [axiom, in VFA.Extract]
Integers [module, in VFA.Trie]
Integers.add [definition, in VFA.Trie]
Integers.addc [definition, in VFA.Trie]
Integers.addc_correct [lemma, in VFA.Trie]
Integers.add_correct [lemma, in VFA.Trie]
Integers.compare [definition, in VFA.Trie]
Integers.compare_correct [lemma, in VFA.Trie]
Integers.comparison [inductive, in VFA.Trie]
Integers.Eq [constructor, in VFA.Trie]
Integers.Gt [constructor, in VFA.Trie]
Integers.Lt [constructor, in VFA.Trie]
Integers.positive [inductive, in VFA.Trie]
Integers.positive2nat [definition, in VFA.Trie]
Integers.positive2nat_pos [lemma, in VFA.Trie]
Integers.print_in_binary [definition, in VFA.Trie]
Integers.succ [definition, in VFA.Trie]
Integers.succ_correct [lemma, in VFA.Trie]
Integers.ten [definition, in VFA.Trie]
Integers.xH [constructor, in VFA.Trie]
Integers.xI [constructor, in VFA.Trie]
Integers.xO [constructor, in VFA.Trie]
Integers.Z [inductive, in VFA.Trie]
Integers.Zneg [constructor, in VFA.Trie]
Integers.Zpos [constructor, in VFA.Trie]
Integers.Z0 [constructor, in VFA.Trie]
Integers.::x_'~'_'0' [notation, in VFA.Trie]
Integers.::x_'~'_'1' [notation, in VFA.Trie]
IntMaps [module, in VFA.Extract]
IntMaps.total_map [definition, in VFA.Extract]
IntMaps.t_empty [definition, in VFA.Extract]
IntMaps.t_update [definition, in VFA.Extract]
IntMaps.t_update_eq [lemma, in VFA.Extract]
IntMaps.t_update_neq [lemma, in VFA.Extract]
IntMaps.t_update_shadow [lemma, in VFA.Extract]
int2Z [axiom, in VFA.Extract]
int_ltb_reflect [lemma, in VFA.Extract]
in_colors_of_1 [lemma, in VFA.Color]
In_decidable [lemma, in VFA.SearchTree]
in_perm_delete [lemma, in VFA.Multiset]
in_4_pi [definition, in VFA.Decide]
IsRB_b [constructor, in VFA.Redblack]
IsRB_leaf [constructor, in VFA.Redblack]
IsRB_r [constructor, in VFA.Redblack]
is_a_sorting_algorithm [definition, in VFA.Sort]
is_a_sorting_algorithm [definition, in VFA.Selection]
is_a_sorting_algorithm' [definition, in VFA.Multiset]
is_redblack [inductive, in VFA.Redblack]
is_redblack_makeblack [lemma, in VFA.Redblack]
is_redblack_toblack [lemma, in VFA.Redblack]
is_trie [definition, in VFA.Trie]

K

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

L

L [module, in VFA.ADT]
Leaf [constructor, in VFA.Trie]
leb_reflect [lemma, in VFA.Perm]
LISTISH [module, in VFA.ADT]
LISTISH.cons [axiom, in VFA.ADT]
LISTISH.create [axiom, in VFA.ADT]
LISTISH.list [axiom, in VFA.ADT]
LISTISH.nth [axiom, in VFA.ADT]
list2map [definition, in VFA.SearchTree]
list2map_app_left [lemma, in VFA.SearchTree]
list2map_app_right [lemma, in VFA.SearchTree]
list2map_not_in_default [lemma, in VFA.SearchTree]
list_delete [definition, in VFA.Multiset]
list_nat_eq_dec [definition, in VFA.Decide]
list_nat_in [definition, in VFA.Decide]
List_Priqueue [module, in VFA.Priqueue]
List_Priqueue.Abs [definition, in VFA.Priqueue]
List_Priqueue.Abs' [inductive, in VFA.Priqueue]
List_Priqueue.Abs_intro [constructor, in VFA.Priqueue]
List_Priqueue.abs_perm [lemma, in VFA.Priqueue]
List_Priqueue.can_relate [lemma, in VFA.Priqueue]
List_Priqueue.delete_max [definition, in VFA.Priqueue]
List_Priqueue.delete_max_None_relate [lemma, in VFA.Priqueue]
List_Priqueue.delete_max_Some_priq [lemma, in VFA.Priqueue]
List_Priqueue.delete_max_Some_relate [lemma, in VFA.Priqueue]
List_Priqueue.empty [definition, in VFA.Priqueue]
List_Priqueue.empty_priq [lemma, in VFA.Priqueue]
List_Priqueue.empty_relate [lemma, in VFA.Priqueue]
List_Priqueue.insert [definition, in VFA.Priqueue]
List_Priqueue.insert_priq [lemma, in VFA.Priqueue]
List_Priqueue.insert_relate [lemma, in VFA.Priqueue]
List_Priqueue.key [definition, in VFA.Priqueue]
List_Priqueue.merge [definition, in VFA.Priqueue]
List_Priqueue.merge_priq [lemma, in VFA.Priqueue]
List_Priqueue.merge_relate [lemma, in VFA.Priqueue]
List_Priqueue.priq [definition, in VFA.Priqueue]
List_Priqueue.priqueue [definition, in VFA.Priqueue]
List_Priqueue.select [definition, in VFA.Priqueue]
List_Priqueue.select_biggest [lemma, in VFA.Priqueue]
List_Priqueue.select_biggest_aux [lemma, in VFA.Priqueue]
List_Priqueue.select_perm [lemma, in VFA.Priqueue]
look [definition, in VFA.Trie]
lookup [definition, in VFA.Redblack]
lookup [definition, in VFA.SearchTree]
lookup [definition, in VFA.Trie]
lookup_equiv [lemma, in VFA.SearchTree]
lookup_relate [lemma, in VFA.SearchTree]
lookup_relate [lemma, in VFA.Trie]
lookup_relate [lemma, in VFA.Redblack]
lookup_relateX [lemma, in VFA.SearchTree]
lookup_relate' [lemma, in VFA.SearchTree]
look_ins_other [lemma, in VFA.Trie]
look_ins_same [lemma, in VFA.Trie]
look_leaf [lemma, in VFA.Trie]
low_deg [definition, in VFA.Color]
ltb [axiom, in VFA.Extract]
ltb_lt [axiom, in VFA.Extract]
ltb_reflect [lemma, in VFA.Perm]
lt_proper [lemma, in VFA.Color]
lt_strict [lemma, in VFA.Color]
L.cons [definition, in VFA.ADT]
L.create [definition, in VFA.ADT]
L.list [definition, in VFA.ADT]
L.nth [definition, in VFA.ADT]
L_Abs [inductive, in VFA.ADT]

M

M [module, in VFA.Color]
makeBlack [definition, in VFA.Redblack]
makeBlack_relate [lemma, in VFA.Redblack]
manual_grade_for_elements_relate_informal [definition, in VFA.SearchTree]
manual_grade_for_permutations_vs_multiset [definition, in VFA.Multiset]
manual_grade_for_successor_of_Z_constant_time [definition, in VFA.Trie]
MapsTable [module, in VFA.ADT]
MapsTable.default [definition, in VFA.ADT]
MapsTable.empty [definition, in VFA.ADT]
MapsTable.gempty [lemma, in VFA.ADT]
MapsTable.get [definition, in VFA.ADT]
MapsTable.gso [lemma, in VFA.ADT]
MapsTable.gss [lemma, in VFA.ADT]
MapsTable.key [definition, in VFA.ADT]
MapsTable.set [definition, in VFA.ADT]
MapsTable.table [definition, in VFA.ADT]
MapsTable.V [definition, in VFA.ADT]
maps_equiv_ex [definition, in VFA.Redblack]
Mdomain [definition, in VFA.Color]
mk_graph [definition, in VFA.Color]
Mremove_cardinal_less [lemma, in VFA.Color]
Mremove_elements [lemma, in VFA.Color]
multiset [definition, in VFA.Multiset]
Multiset [library]
multiset_delete [definition, in VFA.Multiset]

N

naive_lookup_relateX [lemma, in VFA.SearchTree]
nat2pos [definition, in VFA.Trie]
nat2pos2nat [lemma, in VFA.Trie]
nat2pos_injective [lemma, in VFA.Trie]
nearly_redblack [inductive, in VFA.Redblack]
Node [constructor, in VFA.Trie]
node [definition, in VFA.Color]
nodemap [definition, in VFA.Color]
nodes [definition, in VFA.Color]
nodeset [definition, in VFA.Color]
not_elements_relate [lemma, in VFA.SearchTree]
not_naive_lookup_relateX [lemma, in VFA.SearchTree]
no_selfloop [definition, in VFA.Color]
nrRB_b [constructor, in VFA.Redblack]
nrRB_r [constructor, in VFA.Redblack]
nth_firstn [lemma, in VFA.ADT]
nth_relate [lemma, in VFA.ADT]

O

out_of_gas [definition, in VFA.Selection]
O_Abs [definition, in VFA.ADT]

P

palette [definition, in VFA.Color]
Perm [library]
perm_contents [lemma, in VFA.Multiset]
pos2nat [definition, in VFA.Trie]
pos2nat2pos [lemma, in VFA.Trie]
pos2nat_injective [lemma, in VFA.Trie]
Preface [library]
PRIQUEUE [module, in VFA.Priqueue]
Priqueue [library]
PRIQUEUE.Abs [axiom, in VFA.Priqueue]
PRIQUEUE.abs_perm [axiom, in VFA.Priqueue]
PRIQUEUE.can_relate [axiom, in VFA.Priqueue]
PRIQUEUE.delete_max [axiom, in VFA.Priqueue]
PRIQUEUE.delete_max_None_relate [axiom, in VFA.Priqueue]
PRIQUEUE.delete_max_Some_priq [axiom, in VFA.Priqueue]
PRIQUEUE.delete_max_Some_relate [axiom, in VFA.Priqueue]
PRIQUEUE.empty [axiom, in VFA.Priqueue]
PRIQUEUE.empty_priq [axiom, in VFA.Priqueue]
PRIQUEUE.empty_relate [axiom, in VFA.Priqueue]
PRIQUEUE.insert [axiom, in VFA.Priqueue]
PRIQUEUE.insert_priq [axiom, in VFA.Priqueue]
PRIQUEUE.insert_relate [axiom, in VFA.Priqueue]
PRIQUEUE.key [definition, in VFA.Priqueue]
PRIQUEUE.merge [axiom, in VFA.Priqueue]
PRIQUEUE.merge_priq [axiom, in VFA.Priqueue]
PRIQUEUE.merge_relate [axiom, in VFA.Priqueue]
PRIQUEUE.priq [axiom, in VFA.Priqueue]
PRIQUEUE.priqueue [axiom, in VFA.Priqueue]
Proper_eq_eq [lemma, in VFA.Color]
Proper_eq_key_elt [lemma, in VFA.Color]

R

RatherSlow [module, in VFA.Trie]
RatherSlow.collisions [definition, in VFA.Trie]
RatherSlow.collisions_pi [definition, in VFA.Trie]
RatherSlow.empty [definition, in VFA.Trie]
RatherSlow.loop [definition, in VFA.Trie]
RatherSlow.total_mapz [definition, in VFA.Trie]
RatherSlow.update [definition, in VFA.Trie]
rb [definition, in VFA.Redblack]
Red [constructor, in VFA.Redblack]
Redblack [library]
reflect_example1 [definition, in VFA.Perm]
reflect_example1' [definition, in VFA.Perm]
reflect_example2 [definition, in VFA.Perm]
remove_node [definition, in VFA.Color]
repeat [definition, in VFA.ADT]
repeat_step_relate [lemma, in VFA.ADT]

S

S [module, in VFA.Color]
same_contents_iff_perm [lemma, in VFA.Multiset]
same_mod_10 [definition, in VFA.Color]
ScratchPad [module, in VFA.Decide]
ScratchPad.greater23 [lemma, in VFA.Decide]
ScratchPad.is_3_less_7 [definition, in VFA.Decide]
ScratchPad.left [constructor, in VFA.Decide]
ScratchPad.less37 [lemma, in VFA.Decide]
ScratchPad.lt_dec [definition, in VFA.Decide]
ScratchPad.lt_dec' [definition, in VFA.Decide]
ScratchPad.lt_dec_equivalent [lemma, in VFA.Decide]
ScratchPad.right [constructor, in VFA.Decide]
ScratchPad.sumbool [inductive, in VFA.Decide]
ScratchPad.t1 [definition, in VFA.Decide]
ScratchPad.t2 [definition, in VFA.Decide]
ScratchPad.t4 [definition, in VFA.Decide]
ScratchPad.v1a [definition, in VFA.Decide]
ScratchPad.v1b [definition, in VFA.Decide]
ScratchPad.v2a [definition, in VFA.Decide]
ScratchPad.v3 [definition, in VFA.Decide]
ScratchPad.:type_scope:'{'_x_'}'_'+'_'{'_x_'}' [notation, in VFA.Decide]
ScratchPad2 [module, in VFA.Decide]
ScratchPad2.insert [definition, in VFA.Decide]
ScratchPad2.insert_sorted [lemma, in VFA.Decide]
ScratchPad2.le_dec [definition, in VFA.Decide]
ScratchPad2.lt_dec [definition, in VFA.Decide]
ScratchPad2.lt_dec_axiom_1 [axiom, in VFA.Decide]
ScratchPad2.lt_dec_axiom_2 [axiom, in VFA.Decide]
ScratchPad2.max_with_axiom [definition, in VFA.Decide]
ScratchPad2.prove_with_max_axiom [lemma, in VFA.Decide]
ScratchPad2.sort [definition, in VFA.Decide]
ScratchPad2.sorted [inductive, in VFA.Decide]
ScratchPad2.sorted_cons [constructor, in VFA.Decide]
ScratchPad2.sorted_nil [constructor, in VFA.Decide]
ScratchPad2.sorted_1 [constructor, in VFA.Decide]
SearchTree [inductive, in VFA.SearchTree]
SearchTree [inductive, in VFA.Redblack]
SearchTree [library]
SearchTreeX [definition, in VFA.SearchTree]
SearchTree' [inductive, in VFA.SearchTree]
SearchTree' [inductive, in VFA.Redblack]
SearchTree'_le [lemma, in VFA.SearchTree]
SearchTree'_le [lemma, in VFA.Redblack]
SearchTree2 [module, in VFA.Extract]
SearchTree2.Abs [inductive, in VFA.Extract]
SearchTree2.Abs_E [constructor, in VFA.Extract]
SearchTree2.Abs_T [constructor, in VFA.Extract]
SearchTree2.combine [definition, in VFA.Extract]
SearchTree2.E [constructor, in VFA.Extract]
SearchTree2.elements [definition, in VFA.Extract]
SearchTree2.elements' [definition, in VFA.Extract]
SearchTree2.empty_tree [definition, in VFA.Extract]
SearchTree2.empty_tree_relate [lemma, in VFA.Extract]
SearchTree2.insert [definition, in VFA.Extract]
SearchTree2.insert_relate [lemma, in VFA.Extract]
SearchTree2.key [definition, in VFA.Extract]
SearchTree2.lookup [definition, in VFA.Extract]
SearchTree2.lookup_relate [lemma, in VFA.Extract]
SearchTree2.T [constructor, in VFA.Extract]
SearchTree2.tree [inductive, in VFA.Extract]
SearchTree2.TREES [section, in VFA.Extract]
SearchTree2.TREES.default [variable, in VFA.Extract]
SearchTree2.TREES.V [variable, in VFA.Extract]
SearchTree2.unrealistically_strong_can_relate [lemma, in VFA.Extract]
SectionExample1 [module, in VFA.SearchTree]
SectionExample1.empty [definition, in VFA.SearchTree]
SectionExample1.lookup [definition, in VFA.SearchTree]
SectionExample1.lookup_empty [lemma, in VFA.SearchTree]
SectionExample1.mymap [definition, in VFA.SearchTree]
SectionExample2 [module, in VFA.SearchTree]
SectionExample2.empty [definition, in VFA.SearchTree]
SectionExample2.lookup [definition, in VFA.SearchTree]
SectionExample2.lookup_empty [lemma, in VFA.SearchTree]
SectionExample2.MAPS [section, in VFA.SearchTree]
SectionExample2.MAPS.default [variable, in VFA.SearchTree]
SectionExample2.MAPS.V [variable, in VFA.SearchTree]
SectionExample2.mymap [definition, in VFA.SearchTree]
select [definition, in VFA.Selection]
Selection [library]
selection_sort [definition, in VFA.Selection]
selection_sort_correct [definition, in VFA.Selection]
selection_sort_is_correct [lemma, in VFA.Selection]
selection_sort_perm [lemma, in VFA.Selection]
selection_sort_sorted [lemma, in VFA.Selection]
selection_sort_sorted_aux [lemma, in VFA.Selection]
select_perm [lemma, in VFA.Selection]
select_perm' [lemma, in VFA.Selection]
select_smallest [lemma, in VFA.Selection]
select_smallest_aux [lemma, in VFA.Selection]
select_terminates [lemma, in VFA.Color]
selsort [definition, in VFA.Selection]
selsort [definition, in VFA.Selection]
selsort'_perm [lemma, in VFA.Selection]
selsort_perm [lemma, in VFA.Selection]
singleton [definition, in VFA.Multiset]
Sin_domain [lemma, in VFA.Color]
sixlist [definition, in VFA.ADT]
slow_elements [definition, in VFA.SearchTree]
slow_elements_range [lemma, in VFA.SearchTree]
Snot_in_empty [lemma, in VFA.Color]
sort [definition, in VFA.Sort]
Sort [library]
sorted [inductive, in VFA.Selection]
sorted [inductive, in VFA.Sort]
sorted' [definition, in VFA.Sort]
sorted'_sorted [lemma, in VFA.Sort]
sorted_cons [constructor, in VFA.Selection]
sorted_cons [constructor, in VFA.Sort]
Sorted_lt_key [lemma, in VFA.Color]
sorted_nil [constructor, in VFA.Sort]
sorted_nil [constructor, in VFA.Selection]
sorted_sorted' [lemma, in VFA.Sort]
sorted_1 [constructor, in VFA.Sort]
sorted_1 [constructor, in VFA.Selection]
SortE_equivlistE_eqlistE [lemma, in VFA.Color]
Sort1 [module, in VFA.Extract]
Sort1.insert [definition, in VFA.Extract]
Sort1.sort [definition, in VFA.Extract]
sort_contents [lemma, in VFA.Multiset]
sort_perm [lemma, in VFA.Sort]
sort_pi [definition, in VFA.Multiset]
sort_pi [definition, in VFA.Sort]
sort_pi [definition, in VFA.Selection]
sort_pi_same_contents [definition, in VFA.Multiset]
sort_sorted [lemma, in VFA.Sort]
sort_sorted' [lemma, in VFA.Sort]
sort_specifications_equivalent [lemma, in VFA.Multiset]
specialize_SortA_equivlistA_eqlistA [lemma, in VFA.Color]
Sremove_cardinal_less [lemma, in VFA.Color]
Sremove_elements [lemma, in VFA.Color]
Sremove_elements [lemma, in VFA.Color]
step [definition, in VFA.ADT]
stepish [definition, in VFA.ADT]
step_relate [lemma, in VFA.ADT]
ST_E [constructor, in VFA.SearchTree]
ST_E [constructor, in VFA.Redblack]
ST_intro [constructor, in VFA.Redblack]
ST_intro [constructor, in VFA.SearchTree]
ST_T [constructor, in VFA.Redblack]
ST_T [constructor, in VFA.SearchTree]
subset_nodes [definition, in VFA.Color]
subset_nodes_sub [lemma, in VFA.Color]

T

T [constructor, in VFA.Redblack]
T [constructor, in VFA.SearchTree]
TABLE [module, in VFA.ADT]
TABLE.default [axiom, in VFA.ADT]
TABLE.empty [axiom, in VFA.ADT]
TABLE.gempty [axiom, in VFA.ADT]
TABLE.get [axiom, in VFA.ADT]
TABLE.gso [axiom, in VFA.ADT]
TABLE.gss [axiom, in VFA.ADT]
TABLE.key [definition, in VFA.ADT]
TABLE.set [axiom, in VFA.ADT]
TABLE.table [axiom, in VFA.ADT]
TABLE.V [axiom, in VFA.ADT]
TABLE_STRING [module, in VFA.ADT]
test_maps_table [definition, in VFA.ADT]
test_maps_table [definition, in VFA.ADT]
the_proof [definition, in VFA.ADT]
the_witness [definition, in VFA.ADT]
three_less_seven_1 [lemma, in VFA.Decide]
three_less_seven_2 [lemma, in VFA.Decide]
three_ten [definition, in VFA.Trie]
too_much_gas [definition, in VFA.Selection]
tree [inductive, in VFA.Redblack]
tree [inductive, in VFA.SearchTree]
TREES [section, in VFA.Redblack]
TREES [section, in VFA.SearchTree]
TREES.ContentsExample [section, in VFA.Redblack]
TREES.default [variable, in VFA.Redblack]
TREES.default [variable, in VFA.SearchTree]
TREES.ExampleMap [section, in VFA.SearchTree]
TREES.ExampleMap.v2 [variable, in VFA.SearchTree]
TREES.ExampleMap.v4 [variable, in VFA.SearchTree]
TREES.ExampleMap.v5 [variable, in VFA.SearchTree]
TREES.EXAMPLES [section, in VFA.SearchTree]
TREES.EXAMPLES.v2 [variable, in VFA.SearchTree]
TREES.EXAMPLES.v4 [variable, in VFA.SearchTree]
TREES.EXAMPLES.v5 [variable, in VFA.SearchTree]
TREES.V [variable, in VFA.Redblack]
TREES.V [variable, in VFA.SearchTree]
TreeTable [module, in VFA.ADT]
TreeTable.default [definition, in VFA.ADT]
TreeTable.empty [definition, in VFA.ADT]
TreeTable.gempty [lemma, in VFA.ADT]
TreeTable.get [definition, in VFA.ADT]
TreeTable.gso [lemma, in VFA.ADT]
TreeTable.gss [lemma, in VFA.ADT]
TreeTable.key [definition, in VFA.ADT]
TreeTable.set [definition, in VFA.ADT]
TreeTable.table [definition, in VFA.ADT]
TreeTable.V [definition, in VFA.ADT]
TreeTable2 [module, in VFA.ADT]
TreeTable2.default [definition, in VFA.ADT]
TreeTable2.empty [definition, in VFA.ADT]
TreeTable2.gempty [lemma, in VFA.ADT]
TreeTable2.get [definition, in VFA.ADT]
TreeTable2.gso [lemma, in VFA.ADT]
TreeTable2.gss [lemma, in VFA.ADT]
TreeTable2.key [definition, in VFA.ADT]
TreeTable2.set [definition, in VFA.ADT]
TreeTable2.table [definition, in VFA.ADT]
TreeTable2.V [definition, in VFA.ADT]
trie [inductive, in VFA.Trie]
Trie [library]
trie_table [definition, in VFA.Trie]
T_neq_E [lemma, in VFA.Redblack]

U

undirected [definition, in VFA.Color]
union [definition, in VFA.Multiset]
union_assoc [lemma, in VFA.Multiset]
union_comm [lemma, in VFA.Multiset]
unrealistically_strong_can_relate [lemma, in VFA.SearchTree]

V

value [definition, in VFA.Multiset]
VerySlow [module, in VFA.Trie]
VerySlow.collisions [definition, in VFA.Trie]
VerySlow.collisions_pi [definition, in VFA.Trie]
VerySlow.loop [definition, in VFA.Trie]

W

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

Z

zero_even [lemma, in VFA.ADT]
Z_eqb_reflect [lemma, in VFA.Extract]
Z_ltb_reflect [lemma, in VFA.Extract]

:

:nat_scope:x_'>=?'_x [notation, in VFA.Perm]
:nat_scope:x_'>?'_x [notation, in VFA.Perm]

---

Notation Index

I

Integers.::x_'~'_'0' [in VFA.Trie]
Integers.::x_'~'_'1' [in VFA.Trie]

S

ScratchPad.:type_scope:'{'_x_'}'_'+'_'{'_x_'}' [in VFA.Decide]

:

:nat_scope:x_'>=?'_x [in VFA.Perm]
:nat_scope:x_'>?'_x [in VFA.Perm]

---

Module Index

B

BinomQueue [in VFA.Binom]

E

E [in VFA.Color]
Experiments [in VFA.Extract]
Exploration1 [in VFA.Perm]

F

FastEnough [in VFA.Trie]

I

Integers [in VFA.Trie]
IntMaps [in VFA.Extract]

L

L [in VFA.ADT]
LISTISH [in VFA.ADT]
List_Priqueue [in VFA.Priqueue]

M

M [in VFA.Color]
MapsTable [in VFA.ADT]

P

PRIQUEUE [in VFA.Priqueue]

R

RatherSlow [in VFA.Trie]

S

S [in VFA.Color]
ScratchPad [in VFA.Decide]
ScratchPad2 [in VFA.Decide]
SearchTree2 [in VFA.Extract]
SectionExample1 [in VFA.SearchTree]
SectionExample2 [in VFA.SearchTree]
Sort1 [in VFA.Extract]

T

TABLE [in VFA.ADT]
TABLE_STRING [in VFA.ADT]
TreeTable [in VFA.ADT]
TreeTable2 [in VFA.ADT]

V

VerySlow [in VFA.Trie]

W

WF [in VFA.Color]
WP [in VFA.Color]

---

Variable Index

A

ADT_SUMMARY.default [in VFA.ADT]
ADT_SUMMARY.V [in VFA.ADT]

S

SearchTree2.TREES.default [in VFA.Extract]
SearchTree2.TREES.V [in VFA.Extract]
SectionExample2.MAPS.default [in VFA.SearchTree]
SectionExample2.MAPS.V [in VFA.SearchTree]

T

TREES.default [in VFA.Redblack]
TREES.default [in VFA.SearchTree]
TREES.ExampleMap.v2 [in VFA.SearchTree]
TREES.ExampleMap.v4 [in VFA.SearchTree]
TREES.ExampleMap.v5 [in VFA.SearchTree]
TREES.EXAMPLES.v2 [in VFA.SearchTree]
TREES.EXAMPLES.v4 [in VFA.SearchTree]
TREES.EXAMPLES.v5 [in VFA.SearchTree]
TREES.V [in VFA.Redblack]
TREES.V [in VFA.SearchTree]

---

Library Index

A

ADT

B

Binom

C

Color

D

Decide

E

Extract

M

Multiset

P

Perm
Preface
Priqueue

R

Redblack

S

SearchTree
Selection
Sort

T

Trie

---

Axiom Index

I

int [in VFA.Extract]
int2Z [in VFA.Extract]

L

LISTISH.cons [in VFA.ADT]
LISTISH.create [in VFA.ADT]
LISTISH.list [in VFA.ADT]
LISTISH.nth [in VFA.ADT]
ltb [in VFA.Extract]
ltb_lt [in VFA.Extract]

P

PRIQUEUE.Abs [in VFA.Priqueue]
PRIQUEUE.abs_perm [in VFA.Priqueue]
PRIQUEUE.can_relate [in VFA.Priqueue]
PRIQUEUE.delete_max [in VFA.Priqueue]
PRIQUEUE.delete_max_None_relate [in VFA.Priqueue]
PRIQUEUE.delete_max_Some_priq [in VFA.Priqueue]
PRIQUEUE.delete_max_Some_relate [in VFA.Priqueue]
PRIQUEUE.empty [in VFA.Priqueue]
PRIQUEUE.empty_priq [in VFA.Priqueue]
PRIQUEUE.empty_relate [in VFA.Priqueue]
PRIQUEUE.insert [in VFA.Priqueue]
PRIQUEUE.insert_priq [in VFA.Priqueue]
PRIQUEUE.insert_relate [in VFA.Priqueue]
PRIQUEUE.merge [in VFA.Priqueue]
PRIQUEUE.merge_priq [in VFA.Priqueue]
PRIQUEUE.merge_relate [in VFA.Priqueue]
PRIQUEUE.priq [in VFA.Priqueue]
PRIQUEUE.priqueue [in VFA.Priqueue]

S

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

T

TABLE.default [in VFA.ADT]
TABLE.empty [in VFA.ADT]
TABLE.gempty [in VFA.ADT]
TABLE.get [in VFA.ADT]
TABLE.gso [in VFA.ADT]
TABLE.gss [in VFA.ADT]
TABLE.set [in VFA.ADT]
TABLE.table [in VFA.ADT]
TABLE.V [in VFA.ADT]

---

Lemma Index

A

abstraction_of_bogus_tree [in VFA.SearchTree]
Abs_helper [in VFA.Redblack]
Abs_T_aux [in VFA.SearchTree]
adj_ext [in VFA.Color]

B

balance_relate [in VFA.Redblack]
balance_SearchTree [in VFA.Redblack]
balance_SearchTree [in VFA.Redblack]
balance_SearchTree [in VFA.Redblack]
BinomQueue.abs_perm [in VFA.Binom]
BinomQueue.can_relate [in VFA.Binom]
BinomQueue.carry_elems [in VFA.Binom]
BinomQueue.carry_valid [in VFA.Binom]
BinomQueue.delete_max_None_relate [in VFA.Binom]
BinomQueue.delete_max_Some_priq [in VFA.Binom]
BinomQueue.delete_max_Some_relate [in VFA.Binom]
BinomQueue.empty_priq [in VFA.Binom]
BinomQueue.empty_relate [in VFA.Binom]
BinomQueue.insert_priq [in VFA.Binom]
BinomQueue.insert_relate [in VFA.Binom]
BinomQueue.join_elems [in VFA.Binom]
BinomQueue.join_valid [in VFA.Binom]
BinomQueue.merge_priq [in VFA.Binom]
BinomQueue.merge_relate [in VFA.Binom]
BinomQueue.priqueue_elems_ext [in VFA.Binom]
BinomQueue.smash_elems [in VFA.Binom]
BinomQueue.smash_valid [in VFA.Binom]
BinomQueue.tree_can_relate [in VFA.Binom]
BinomQueue.tree_elems_ext [in VFA.Binom]
BinomQueue.tree_perm [in VFA.Binom]

C

can_relate [in VFA.SearchTree]
cardinal_map [in VFA.Color]
check_example_map [in VFA.SearchTree]
color_correct [in VFA.Color]
compute_with_lt_dec [in VFA.Decide]
compute_with_StdLib_lt_dec [in VFA.Decide]
cons_relate [in VFA.ADT]
contents_in [in VFA.Multiset]
contents_perm [in VFA.Multiset]
contents_perm_aux [in VFA.Multiset]
create_relate [in VFA.ADT]

D

delete_contents [in VFA.Multiset]

E

elements_relate [in VFA.SearchTree]
elements_relate [in VFA.SearchTree]
elements_relate [in VFA.Redblack]
elements_relateX [in VFA.SearchTree]
elements_relate_second_attempt [in VFA.SearchTree]
elements_slow_elements [in VFA.SearchTree]
empty_equiv [in VFA.SearchTree]
empty_is_trie [in VFA.Trie]
empty_rb [in VFA.Redblack]
empty_relate [in VFA.Trie]
empty_SearchTree [in VFA.Redblack]
empty_tree_relate [in VFA.SearchTree]
empty_tree_relate [in VFA.Redblack]
empty_tree_SearchTree [in VFA.SearchTree]
eqb_reflect [in VFA.Perm]
eqlistA_Eeq_eq [in VFA.Color]
example_SearchTree_bad [in VFA.SearchTree]
example_SearchTree_good [in VFA.SearchTree]
expand_range_SearchTree' [in VFA.Redblack]
Exploration1.bogus_subtraction [in VFA.Perm]
Exploration1.maybe_swap_correct [in VFA.Perm]
Exploration1.maybe_swap_idempotent [in VFA.Perm]
Exploration1.maybe_swap_idempotent [in VFA.Perm]
Exploration1.maybe_swap_idempotent' [in VFA.Perm]
Exploration1.maybe_swap_perm [in VFA.Perm]
Exploration1.omega_example1 [in VFA.Perm]
Exploration1.omega_example1 [in VFA.Perm]
Exploration1.omega_example2 [in VFA.Perm]

F

fibish_correct [in VFA.ADT]
filter_sortE [in VFA.Color]
fold_right_rev_left [in VFA.Color]
Forall_nth [in VFA.Sort]
Forall_perm [in VFA.Perm]

I

InA_map_fst_key [in VFA.Color]
insertion_sort_correct [in VFA.Sort]
insertion_sort_correct [in VFA.Multiset]
insert_contents [in VFA.Multiset]
insert_is_redblack [in VFA.Redblack]
insert_is_trie [in VFA.Trie]
insert_perm [in VFA.Sort]
insert_rb [in VFA.Redblack]
insert_relate [in VFA.SearchTree]
insert_relate [in VFA.Trie]
insert_relate [in VFA.Redblack]
insert_relate' [in VFA.SearchTree]
insert_SearchTree [in VFA.Redblack]
insert_SearchTree [in VFA.SearchTree]
insert_sorted [in VFA.Sort]
insert_sorted' [in VFA.Sort]
ins_black [in VFA.Redblack]
ins_E_SearchTree [in VFA.Redblack]
ins_is_redblack [in VFA.Redblack]
ins_left [in VFA.Redblack]
ins_makeBlack_SearchTree [in VFA.Redblack]
ins_not_E [in VFA.Redblack]
ins_not_E [in VFA.Redblack]
ins_not_E [in VFA.Redblack]
ins_red [in VFA.Redblack]
ins_relate [in VFA.Redblack]
ins_right [in VFA.Redblack]
ins_SearchTree [in VFA.Redblack]
ins_T_SearchTree [in VFA.Redblack]
ins_T_SearchTree_aux [in VFA.Redblack]
Integers.addc_correct [in VFA.Trie]
Integers.add_correct [in VFA.Trie]
Integers.compare_correct [in VFA.Trie]
Integers.positive2nat_pos [in VFA.Trie]
Integers.succ_correct [in VFA.Trie]
IntMaps.t_update_eq [in VFA.Extract]
IntMaps.t_update_neq [in VFA.Extract]
IntMaps.t_update_shadow [in VFA.Extract]
int_ltb_reflect [in VFA.Extract]
in_colors_of_1 [in VFA.Color]
In_decidable [in VFA.SearchTree]
in_perm_delete [in VFA.Multiset]
is_redblack_makeblack [in VFA.Redblack]
is_redblack_toblack [in VFA.Redblack]

L

leb_reflect [in VFA.Perm]
list2map_app_left [in VFA.SearchTree]
list2map_app_right [in VFA.SearchTree]
list2map_not_in_default [in VFA.SearchTree]
List_Priqueue.abs_perm [in VFA.Priqueue]
List_Priqueue.can_relate [in VFA.Priqueue]
List_Priqueue.delete_max_None_relate [in VFA.Priqueue]
List_Priqueue.delete_max_Some_priq [in VFA.Priqueue]
List_Priqueue.delete_max_Some_relate [in VFA.Priqueue]
List_Priqueue.empty_priq [in VFA.Priqueue]
List_Priqueue.empty_relate [in VFA.Priqueue]
List_Priqueue.insert_priq [in VFA.Priqueue]
List_Priqueue.insert_relate [in VFA.Priqueue]
List_Priqueue.merge_priq [in VFA.Priqueue]
List_Priqueue.merge_relate [in VFA.Priqueue]
List_Priqueue.select_biggest [in VFA.Priqueue]
List_Priqueue.select_biggest_aux [in VFA.Priqueue]
List_Priqueue.select_perm [in VFA.Priqueue]
lookup_equiv [in VFA.SearchTree]
lookup_relate [in VFA.SearchTree]
lookup_relate [in VFA.Trie]
lookup_relate [in VFA.Redblack]
lookup_relateX [in VFA.SearchTree]
lookup_relate' [in VFA.SearchTree]
look_ins_other [in VFA.Trie]
look_ins_same [in VFA.Trie]
look_leaf [in VFA.Trie]
ltb_reflect [in VFA.Perm]
lt_proper [in VFA.Color]
lt_strict [in VFA.Color]

M

makeBlack_relate [in VFA.Redblack]
MapsTable.gempty [in VFA.ADT]
MapsTable.gso [in VFA.ADT]
MapsTable.gss [in VFA.ADT]
Mremove_cardinal_less [in VFA.Color]
Mremove_elements [in VFA.Color]

N

naive_lookup_relateX [in VFA.SearchTree]
nat2pos2nat [in VFA.Trie]
nat2pos_injective [in VFA.Trie]
not_elements_relate [in VFA.SearchTree]
not_naive_lookup_relateX [in VFA.SearchTree]
nth_firstn [in VFA.ADT]
nth_relate [in VFA.ADT]

P

perm_contents [in VFA.Multiset]
pos2nat2pos [in VFA.Trie]
pos2nat_injective [in VFA.Trie]
Proper_eq_eq [in VFA.Color]
Proper_eq_key_elt [in VFA.Color]

R

repeat_step_relate [in VFA.ADT]

S

same_contents_iff_perm [in VFA.Multiset]
ScratchPad.greater23 [in VFA.Decide]
ScratchPad.less37 [in VFA.Decide]
ScratchPad.lt_dec_equivalent [in VFA.Decide]
ScratchPad2.insert_sorted [in VFA.Decide]
ScratchPad2.prove_with_max_axiom [in VFA.Decide]
SearchTree'_le [in VFA.SearchTree]
SearchTree'_le [in VFA.Redblack]
SearchTree2.empty_tree_relate [in VFA.Extract]
SearchTree2.insert_relate [in VFA.Extract]
SearchTree2.lookup_relate [in VFA.Extract]
SearchTree2.unrealistically_strong_can_relate [in VFA.Extract]
SectionExample1.lookup_empty [in VFA.SearchTree]
SectionExample2.lookup_empty [in VFA.SearchTree]
selection_sort_is_correct [in VFA.Selection]
selection_sort_perm [in VFA.Selection]
selection_sort_sorted [in VFA.Selection]
selection_sort_sorted_aux [in VFA.Selection]
select_perm [in VFA.Selection]
select_perm' [in VFA.Selection]
select_smallest [in VFA.Selection]
select_smallest_aux [in VFA.Selection]
select_terminates [in VFA.Color]
selsort'_perm [in VFA.Selection]
selsort_perm [in VFA.Selection]
Sin_domain [in VFA.Color]
slow_elements_range [in VFA.SearchTree]
Snot_in_empty [in VFA.Color]
sorted'_sorted [in VFA.Sort]
Sorted_lt_key [in VFA.Color]
sorted_sorted' [in VFA.Sort]
SortE_equivlistE_eqlistE [in VFA.Color]
sort_contents [in VFA.Multiset]
sort_perm [in VFA.Sort]
sort_sorted [in VFA.Sort]
sort_sorted' [in VFA.Sort]
sort_specifications_equivalent [in VFA.Multiset]
specialize_SortA_equivlistA_eqlistA [in VFA.Color]
Sremove_cardinal_less [in VFA.Color]
Sremove_elements [in VFA.Color]
Sremove_elements [in VFA.Color]
step_relate [in VFA.ADT]
subset_nodes_sub [in VFA.Color]

T

three_less_seven_1 [in VFA.Decide]
three_less_seven_2 [in VFA.Decide]
TreeTable.gempty [in VFA.ADT]
TreeTable.gso [in VFA.ADT]
TreeTable.gss [in VFA.ADT]
TreeTable2.gempty [in VFA.ADT]
TreeTable2.gso [in VFA.ADT]
TreeTable2.gss [in VFA.ADT]
T_neq_E [in VFA.Redblack]

U

union_assoc [in VFA.Multiset]
union_comm [in VFA.Multiset]
unrealistically_strong_can_relate [in VFA.SearchTree]

Z

zero_even [in VFA.ADT]
Z_eqb_reflect [in VFA.Extract]
Z_ltb_reflect [in VFA.Extract]

---

Constructor Index

A

Abs_E [in VFA.SearchTree]
Abs_E [in VFA.Redblack]
Abs_T [in VFA.SearchTree]
Abs_T [in VFA.Redblack]

B

BinomQueue.Leaf [in VFA.Binom]
BinomQueue.Node [in VFA.Binom]
BinomQueue.tree_elems_leaf [in VFA.Binom]
BinomQueue.tree_elems_node [in VFA.Binom]
Black [in VFA.Redblack]

E

E [in VFA.SearchTree]
E [in VFA.Redblack]

I

Integers.Eq [in VFA.Trie]
Integers.Gt [in VFA.Trie]
Integers.Lt [in VFA.Trie]
Integers.xH [in VFA.Trie]
Integers.xI [in VFA.Trie]
Integers.xO [in VFA.Trie]
Integers.Zneg [in VFA.Trie]
Integers.Zpos [in VFA.Trie]
Integers.Z0 [in VFA.Trie]
IsRB_b [in VFA.Redblack]
IsRB_leaf [in VFA.Redblack]
IsRB_r [in VFA.Redblack]

L

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

N

Node [in VFA.Trie]
nrRB_b [in VFA.Redblack]
nrRB_r [in VFA.Redblack]

R

Red [in VFA.Redblack]

S

ScratchPad.left [in VFA.Decide]
ScratchPad.right [in VFA.Decide]
ScratchPad2.sorted_cons [in VFA.Decide]
ScratchPad2.sorted_nil [in VFA.Decide]
ScratchPad2.sorted_1 [in VFA.Decide]
SearchTree2.Abs_E [in VFA.Extract]
SearchTree2.Abs_T [in VFA.Extract]
SearchTree2.E [in VFA.Extract]
SearchTree2.T [in VFA.Extract]
sorted_cons [in VFA.Selection]
sorted_cons [in VFA.Sort]
sorted_nil [in VFA.Sort]
sorted_nil [in VFA.Selection]
sorted_1 [in VFA.Sort]
sorted_1 [in VFA.Selection]
ST_E [in VFA.SearchTree]
ST_E [in VFA.Redblack]
ST_intro [in VFA.Redblack]
ST_intro [in VFA.SearchTree]
ST_T [in VFA.Redblack]
ST_T [in VFA.SearchTree]

T

T [in VFA.Redblack]
T [in VFA.SearchTree]

---

Inductive Index

A

Abs [in VFA.SearchTree]
Abs [in VFA.Redblack]

B

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

C

color [in VFA.Redblack]

I

Integers.comparison [in VFA.Trie]
Integers.positive [in VFA.Trie]
Integers.Z [in VFA.Trie]
is_redblack [in VFA.Redblack]

L

List_Priqueue.Abs' [in VFA.Priqueue]
L_Abs [in VFA.ADT]

N

nearly_redblack [in VFA.Redblack]

S

ScratchPad.sumbool [in VFA.Decide]
ScratchPad2.sorted [in VFA.Decide]
SearchTree [in VFA.SearchTree]
SearchTree [in VFA.Redblack]
SearchTree' [in VFA.SearchTree]
SearchTree' [in VFA.Redblack]
SearchTree2.Abs [in VFA.Extract]
SearchTree2.tree [in VFA.Extract]
sorted [in VFA.Selection]
sorted [in VFA.Sort]

T

tree [in VFA.Redblack]
tree [in VFA.SearchTree]
trie [in VFA.Trie]

---

Section Index

A

ADT_SUMMARY [in VFA.ADT]

S

SearchTree2.TREES [in VFA.Extract]
SectionExample2.MAPS [in VFA.SearchTree]

T

TREES [in VFA.Redblack]
TREES [in VFA.SearchTree]
TREES.ContentsExample [in VFA.Redblack]
TREES.ExampleMap [in VFA.SearchTree]
TREES.EXAMPLES [in VFA.SearchTree]

---

Definition Index

A

Abs [in VFA.Trie]
abstract [in VFA.Trie]
AbsX [in VFA.SearchTree]
Abs_three_ten [in VFA.Trie]
add_edge [in VFA.Color]
adj [in VFA.Color]

B

balance [in VFA.Redblack]
BinomQueue.Abs [in VFA.Binom]
BinomQueue.carry [in VFA.Binom]
BinomQueue.delete_max [in VFA.Binom]
BinomQueue.delete_max_aux [in VFA.Binom]
BinomQueue.empty [in VFA.Binom]
BinomQueue.find_max [in VFA.Binom]
BinomQueue.find_max' [in VFA.Binom]
BinomQueue.heap_delete_max [in VFA.Binom]
BinomQueue.insert [in VFA.Binom]
BinomQueue.join [in VFA.Binom]
BinomQueue.key [in VFA.Binom]
BinomQueue.manual_grade_for_priqueue_elems [in VFA.Binom]
BinomQueue.merge [in VFA.Binom]
BinomQueue.pow2heap [in VFA.Binom]
BinomQueue.pow2heap' [in VFA.Binom]
BinomQueue.priq [in VFA.Binom]
BinomQueue.priqueue [in VFA.Binom]
BinomQueue.priq' [in VFA.Binom]
BinomQueue.smash [in VFA.Binom]
BinomQueue.unzip [in VFA.Binom]

C

color [in VFA.Color]
coloring [in VFA.Color]
coloring_ok [in VFA.Color]
colors_of [in VFA.Color]
color1 [in VFA.Color]
combine [in VFA.Redblack]
combine [in VFA.SearchTree]
contents [in VFA.Multiset]

D

domain_example_map [in VFA.Color]

E

elements [in VFA.Redblack]
elements [in VFA.SearchTree]
elements' [in VFA.Redblack]
elements' [in VFA.SearchTree]
elements_property [in VFA.Redblack]
empty [in VFA.Trie]
empty [in VFA.Multiset]
empty_tree [in VFA.SearchTree]
empty_tree [in VFA.Redblack]
equivlistA_example [in VFA.Color]
even_nat [in VFA.ADT]
even_zero [in VFA.ADT]
example_map [in VFA.Color]
example_map [in VFA.SearchTree]
example_map_default [in VFA.SearchTree]
example_map_2 [in VFA.SearchTree]
example_map_4 [in VFA.SearchTree]
example_map_5 [in VFA.SearchTree]
example_tree [in VFA.SearchTree]
Experiments.consecutive [in VFA.Extract]
Experiments.E [in VFA.Extract]
Experiments.empty_tree [in VFA.Extract]
Experiments.insert [in VFA.Extract]
Experiments.lookup [in VFA.Extract]
Experiments.T [in VFA.Extract]
Exploration1.butterfly [in VFA.Perm]
Exploration1.first_le_second [in VFA.Perm]
Exploration1.manual_grade_for_Permutation_properties [in VFA.Perm]
Exploration1.maybe_swap [in VFA.Perm]
Exploration1.maybe_swap_123 [in VFA.Perm]
Exploration1.maybe_swap_321 [in VFA.Perm]
Exploration1.not_a_permutation [in VFA.Perm]
Exploration1.permut_example [in VFA.Perm]
ex_t [in VFA.ADT]

F

FastEnough.collisions [in VFA.Trie]
FastEnough.collisions_pi [in VFA.Trie]
FastEnough.loop [in VFA.Trie]
fib [in VFA.ADT]
fibish [in VFA.ADT]
fibonacci [in VFA.ADT]
forall_nodes [in VFA.SearchTree]

G

G [in VFA.Color]
graph [in VFA.Color]

I

InA_example [in VFA.Color]
ins [in VFA.Trie]
ins [in VFA.Redblack]
insert [in VFA.Redblack]
insert [in VFA.Trie]
insert [in VFA.SearchTree]
insert [in VFA.Sort]
Integers.add [in VFA.Trie]
Integers.addc [in VFA.Trie]
Integers.compare [in VFA.Trie]
Integers.positive2nat [in VFA.Trie]
Integers.print_in_binary [in VFA.Trie]
Integers.succ [in VFA.Trie]
Integers.ten [in VFA.Trie]
IntMaps.total_map [in VFA.Extract]
IntMaps.t_empty [in VFA.Extract]
IntMaps.t_update [in VFA.Extract]
in_4_pi [in VFA.Decide]
is_a_sorting_algorithm [in VFA.Sort]
is_a_sorting_algorithm [in VFA.Selection]
is_a_sorting_algorithm' [in VFA.Multiset]
is_trie [in VFA.Trie]

K

key [in VFA.Redblack]
key [in VFA.SearchTree]

L

list2map [in VFA.SearchTree]
list_delete [in VFA.Multiset]
list_nat_eq_dec [in VFA.Decide]
list_nat_in [in VFA.Decide]
List_Priqueue.Abs [in VFA.Priqueue]
List_Priqueue.delete_max [in VFA.Priqueue]
List_Priqueue.empty [in VFA.Priqueue]
List_Priqueue.insert [in VFA.Priqueue]
List_Priqueue.key [in VFA.Priqueue]
List_Priqueue.merge [in VFA.Priqueue]
List_Priqueue.priq [in VFA.Priqueue]
List_Priqueue.priqueue [in VFA.Priqueue]
List_Priqueue.select [in VFA.Priqueue]
look [in VFA.Trie]
lookup [in VFA.Redblack]
lookup [in VFA.SearchTree]
lookup [in VFA.Trie]
low_deg [in VFA.Color]
L.cons [in VFA.ADT]
L.create [in VFA.ADT]
L.list [in VFA.ADT]
L.nth [in VFA.ADT]

M

makeBlack [in VFA.Redblack]
manual_grade_for_elements_relate_informal [in VFA.SearchTree]
manual_grade_for_permutations_vs_multiset [in VFA.Multiset]
manual_grade_for_successor_of_Z_constant_time [in VFA.Trie]
MapsTable.default [in VFA.ADT]
MapsTable.empty [in VFA.ADT]
MapsTable.get [in VFA.ADT]
MapsTable.key [in VFA.ADT]
MapsTable.set [in VFA.ADT]
MapsTable.table [in VFA.ADT]
MapsTable.V [in VFA.ADT]
maps_equiv_ex [in VFA.Redblack]
Mdomain [in VFA.Color]
mk_graph [in VFA.Color]
multiset [in VFA.Multiset]
multiset_delete [in VFA.Multiset]

N

nat2pos [in VFA.Trie]
node [in VFA.Color]
nodemap [in VFA.Color]
nodes [in VFA.Color]
nodeset [in VFA.Color]
no_selfloop [in VFA.Color]

O

out_of_gas [in VFA.Selection]
O_Abs [in VFA.ADT]

P

palette [in VFA.Color]
pos2nat [in VFA.Trie]
PRIQUEUE.key [in VFA.Priqueue]

R

RatherSlow.collisions [in VFA.Trie]
RatherSlow.collisions_pi [in VFA.Trie]
RatherSlow.empty [in VFA.Trie]
RatherSlow.loop [in VFA.Trie]
RatherSlow.total_mapz [in VFA.Trie]
RatherSlow.update [in VFA.Trie]
rb [in VFA.Redblack]
reflect_example1 [in VFA.Perm]
reflect_example1' [in VFA.Perm]
reflect_example2 [in VFA.Perm]
remove_node [in VFA.Color]
repeat [in VFA.ADT]

S

same_mod_10 [in VFA.Color]
ScratchPad.is_3_less_7 [in VFA.Decide]
ScratchPad.lt_dec [in VFA.Decide]
ScratchPad.lt_dec' [in VFA.Decide]
ScratchPad.t1 [in VFA.Decide]
ScratchPad.t2 [in VFA.Decide]
ScratchPad.t4 [in VFA.Decide]
ScratchPad.v1a [in VFA.Decide]
ScratchPad.v1b [in VFA.Decide]
ScratchPad.v2a [in VFA.Decide]
ScratchPad.v3 [in VFA.Decide]
ScratchPad2.insert [in VFA.Decide]
ScratchPad2.le_dec [in VFA.Decide]
ScratchPad2.lt_dec [in VFA.Decide]
ScratchPad2.max_with_axiom [in VFA.Decide]
ScratchPad2.sort [in VFA.Decide]
SearchTreeX [in VFA.SearchTree]
SearchTree2.combine [in VFA.Extract]
SearchTree2.elements [in VFA.Extract]
SearchTree2.elements' [in VFA.Extract]
SearchTree2.empty_tree [in VFA.Extract]
SearchTree2.insert [in VFA.Extract]
SearchTree2.key [in VFA.Extract]
SearchTree2.lookup [in VFA.Extract]
SectionExample1.empty [in VFA.SearchTree]
SectionExample1.lookup [in VFA.SearchTree]
SectionExample1.mymap [in VFA.SearchTree]
SectionExample2.empty [in VFA.SearchTree]
SectionExample2.lookup [in VFA.SearchTree]
SectionExample2.mymap [in VFA.SearchTree]
select [in VFA.Selection]
selection_sort [in VFA.Selection]
selection_sort_correct [in VFA.Selection]
selsort [in VFA.Selection]
selsort [in VFA.Selection]
singleton [in VFA.Multiset]
sixlist [in VFA.ADT]
slow_elements [in VFA.SearchTree]
sort [in VFA.Sort]
sorted' [in VFA.Sort]
Sort1.insert [in VFA.Extract]
Sort1.sort [in VFA.Extract]
sort_pi [in VFA.Multiset]
sort_pi [in VFA.Sort]
sort_pi [in VFA.Selection]
sort_pi_same_contents [in VFA.Multiset]
step [in VFA.ADT]
stepish [in VFA.ADT]
subset_nodes [in VFA.Color]

T

TABLE.key [in VFA.ADT]
test_maps_table [in VFA.ADT]
test_maps_table [in VFA.ADT]
the_proof [in VFA.ADT]
the_witness [in VFA.ADT]
three_ten [in VFA.Trie]
too_much_gas [in VFA.Selection]
TreeTable.default [in VFA.ADT]
TreeTable.empty [in VFA.ADT]
TreeTable.get [in VFA.ADT]
TreeTable.key [in VFA.ADT]
TreeTable.set [in VFA.ADT]
TreeTable.table [in VFA.ADT]
TreeTable.V [in VFA.ADT]
TreeTable2.default [in VFA.ADT]
TreeTable2.empty [in VFA.ADT]
TreeTable2.get [in VFA.ADT]
TreeTable2.key [in VFA.ADT]
TreeTable2.set [in VFA.ADT]
TreeTable2.table [in VFA.ADT]
TreeTable2.V [in VFA.ADT]
trie_table [in VFA.Trie]

U

undirected [in VFA.Color]
union [in VFA.Multiset]

V

value [in VFA.Multiset]
VerySlow.collisions [in VFA.Trie]
VerySlow.collisions_pi [in VFA.Trie]
VerySlow.loop [in VFA.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

:

_

(652 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

:

_

(5 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

_

(28 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(16 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

_

(14 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

_

(37 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

_

(225 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

_

(52 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

_

(26 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(8 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

_

(241 entries)