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 | : | _ | (618 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 | : | _ | (6 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 | _ | (27 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 | _ | (13 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) | |

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 | _ | (211 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) | |

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) | |

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 | _ | (6 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 | _ | (226 entries) |

# Global Index

## A

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

Abs [definition, in VFA.Trie]

abstract [definition, in VFA.Trie]

abstraction_of_bogus_tree [lemma, in VFA.SearchTree]

AbsX [definition, in VFA.SearchTree]

Abs_E [constructor, in VFA.Redblack]

Abs_E [constructor, in VFA.SearchTree]

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]

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]

beq_reflect [lemma, in VFA.Perm]

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]

ble_reflect [lemma, in VFA.Perm]

blt_reflect [lemma, in VFA.Perm]

## C

can_relate [lemma, in VFA.SearchTree]cardinal_map [lemma, in VFA.Color]

check_example_map [lemma, in VFA.SearchTree]

check_too_clever [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.SearchTree]

combine [definition, in VFA.Redblack]

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.Redblack]E [constructor, in VFA.SearchTree]

E [module, in VFA.Color]

elements [definition, in VFA.SearchTree]

elements [definition, in VFA.Redblack]

elements' [definition, in VFA.Redblack]

elements' [definition, in VFA.SearchTree]

elements_property [definition, in VFA.Redblack]

elements_relate [lemma, in VFA.Redblack]

elements_relate [lemma, in VFA.SearchTree]

elements_relate [lemma, in VFA.SearchTree]

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.Multiset]

empty [definition, in VFA.Trie]

empty_is_trie [lemma, in VFA.Trie]

empty_relate [lemma, in VFA.Trie]

empty_tree [definition, in VFA.Redblack]

empty_tree [definition, in VFA.SearchTree]

empty_tree_relate [lemma, in VFA.Redblack]

empty_tree_relate [lemma, in VFA.SearchTree]

empty_tree_SearchTree [lemma, in VFA.Redblack]

empty_tree_SearchTree [lemma, in VFA.SearchTree]

eqlistA_Eeq_eq [lemma, in VFA.Color]

equivlistA_example [definition, in VFA.Color]

example_map [definition, in VFA.Color]

example_map [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.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]

## 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]

## H

how_many_subgoals_remaining [definition, in VFA.Redblack]## 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.SearchTree]

insert [definition, in VFA.Trie]

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_relate [lemma, in VFA.Trie]

insert_relate [lemma, in VFA.Redblack]

insert_relate [lemma, in VFA.SearchTree]

insert_relate' [lemma, in VFA.SearchTree]

insert_SearchTree [lemma, in VFA.SearchTree]

insert_SearchTree [lemma, in VFA.Redblack]

insert_sorted [lemma, in VFA.Sort]

insert_sorted' [lemma, in VFA.Sort]

ins_is_redblack [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_relate [lemma, in VFA.Redblack]

ins_SearchTree [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_blt_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_toblack [lemma, in VFA.Redblack]

is_trie [definition, in VFA.Trie]

## K

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

## L

L [module, in VFA.ADT]Leaf [constructor, in VFA.Trie]

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.Trie]

lookup [definition, in VFA.SearchTree]

lookup [definition, in VFA.Redblack]

lookup_relate [lemma, in VFA.Redblack]

lookup_relate [lemma, in VFA.SearchTree]

lookup_relate [lemma, in VFA.Trie]

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]

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_fiddle [lemma, 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]

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 [definition, in VFA.Color]

Node [constructor, in VFA.Trie]

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]

Red [constructor, in VFA.Redblack]

Redblack [library]

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.Redblack]

SearchTree [inductive, in VFA.SearchTree]

SearchTree [library]

SearchTreeX [definition, in VFA.SearchTree]

SearchTree' [inductive, in VFA.Redblack]

SearchTree' [inductive, in VFA.SearchTree]

SearchTree'_le [lemma, in VFA.Redblack]

SearchTree'_le [lemma, in VFA.SearchTree]

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_smallest [lemma, in VFA.Selection]

select_smallest_aux [lemma, in VFA.Selection]

select_terminates [lemma, in VFA.Color]

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.Selection]

sort_pi [definition, in VFA.Multiset]

sort_pi [definition, in VFA.Sort]

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.Redblack]

ST_E [constructor, in VFA.SearchTree]

ST_intro [constructor, in VFA.SearchTree]

ST_intro [constructor, in VFA.Redblack]

ST_T [constructor, in VFA.SearchTree]

ST_T [constructor, in VFA.Redblack]

subset_nodes [definition, in VFA.Color]

subset_nodes_sub [lemma, in VFA.Color]

## T

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

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]

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.SearchTree]

tree [inductive, in VFA.Redblack]

TREES [section, in VFA.SearchTree]

TREES [section, in VFA.Redblack]

TREES.default [variable, in VFA.SearchTree]

TREES.default [variable, in VFA.Redblack]

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.SearchTree]

TREES.V [variable, in VFA.Redblack]

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

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]

: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]

: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]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.SearchTree]TREES.default [in VFA.Redblack]

TREES.EXAMPLES.v2 [in VFA.SearchTree]

TREES.EXAMPLES.v4 [in VFA.SearchTree]

TREES.EXAMPLES.v5 [in VFA.SearchTree]

TREES.V [in VFA.SearchTree]

TREES.V [in VFA.Redblack]

# Library Index

## A

ADT## B

Binom## C

Color## D

Decide## E

Extract## M

Multiset## P

PermPreface

Priqueue

## R

Redblack## S

SearchTreeSelection

Sort

## T

Trie# Lemma Index

## A

abstraction_of_bogus_tree [in VFA.SearchTree]Abs_helper [in VFA.Redblack]

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]

beq_reflect [in VFA.Perm]

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]

ble_reflect [in VFA.Perm]

blt_reflect [in VFA.Perm]

## C

can_relate [in VFA.SearchTree]cardinal_map [in VFA.Color]

check_example_map [in VFA.SearchTree]

check_too_clever [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.Redblack]elements_relate [in VFA.SearchTree]

elements_relate [in VFA.SearchTree]

elements_relateX [in VFA.SearchTree]

elements_relate_second_attempt [in VFA.SearchTree]

elements_slow_elements [in VFA.SearchTree]

empty_is_trie [in VFA.Trie]

empty_relate [in VFA.Trie]

empty_tree_relate [in VFA.Redblack]

empty_tree_relate [in VFA.SearchTree]

empty_tree_SearchTree [in VFA.Redblack]

empty_tree_SearchTree [in VFA.SearchTree]

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_relate [in VFA.Trie]

insert_relate [in VFA.Redblack]

insert_relate [in VFA.SearchTree]

insert_relate' [in VFA.SearchTree]

insert_SearchTree [in VFA.SearchTree]

insert_SearchTree [in VFA.Redblack]

insert_sorted [in VFA.Sort]

insert_sorted' [in VFA.Sort]

ins_is_redblack [in VFA.Redblack]

ins_not_E [in VFA.Redblack]

ins_not_E [in VFA.Redblack]

ins_not_E [in VFA.Redblack]

ins_relate [in VFA.Redblack]

ins_SearchTree [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_blt_reflect [in VFA.Extract]

in_colors_of_1 [in VFA.Color]

In_decidable [in VFA.SearchTree]

in_perm_delete [in VFA.Multiset]

is_redblack_toblack [in VFA.Redblack]

## L

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_relate [in VFA.Redblack]

lookup_relate [in VFA.SearchTree]

lookup_relate [in VFA.Trie]

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]

lt_proper [in VFA.Color]

lt_strict [in VFA.Color]

## M

makeblack_fiddle [in VFA.Redblack]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.Redblack]

SearchTree'_le [in VFA.SearchTree]

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_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

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

# Constructor Index

## A

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

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.Redblack]E [in VFA.SearchTree]

## 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.Redblack]

ST_E [in VFA.SearchTree]

ST_intro [in VFA.SearchTree]

ST_intro [in VFA.Redblack]

ST_T [in VFA.SearchTree]

ST_T [in VFA.Redblack]

## T

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

# 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]

# Inductive Index

## A

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

## 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.Redblack]

SearchTree [in VFA.SearchTree]

SearchTree' [in VFA.Redblack]

SearchTree' [in VFA.SearchTree]

SearchTree2.Abs [in VFA.Extract]

SearchTree2.tree [in VFA.Extract]

sorted [in VFA.Selection]

sorted [in VFA.Sort]

## T

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

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.SearchTree]TREES [in VFA.Redblack]

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.SearchTree]

combine [in VFA.Redblack]

contents [in VFA.Multiset]

## D

domain_example_map [in VFA.Color]## E

elements [in VFA.SearchTree]elements [in VFA.Redblack]

elements' [in VFA.Redblack]

elements' [in VFA.SearchTree]

elements_property [in VFA.Redblack]

empty [in VFA.Multiset]

empty [in VFA.Trie]

empty_tree [in VFA.Redblack]

empty_tree [in VFA.SearchTree]

equivlistA_example [in VFA.Color]

example_map [in VFA.Color]

example_map [in VFA.SearchTree]

example_tree [in VFA.SearchTree]

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]

## 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]

## H

how_many_subgoals_remaining [in VFA.Redblack]## I

InA_example [in VFA.Color]ins [in VFA.Trie]

ins [in VFA.Redblack]

insert [in VFA.Redblack]

insert [in VFA.SearchTree]

insert [in VFA.Trie]

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.SearchTree]key [in VFA.Redblack]

## 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.Trie]

lookup [in VFA.SearchTree]

lookup [in VFA.Redblack]

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]

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]

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]

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.Selection]

sort_pi [in VFA.Multiset]

sort_pi [in VFA.Sort]

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]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 | : | _ | (618 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 | : | _ | (6 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 | _ | (27 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 | _ | (13 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) | |

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 | _ | (211 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) | |

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) | |

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 | _ | (6 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 | _ | (226 entries) |