Global Index

B

H

J

K

T

U

V

W

X

Y

Z

(471 entries)

Axiom Index

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(2 entries)

Lemma Index

B

H

J

K

T

U

V

W

X

Y

Z

(348 entries)

Constructor Index

A

B

C

D

E

F

G

H

J

K

M

O

Q

R

T

U

V

W

X

Y

Z

_

(27 entries)

Inductive Index

A

B

D

E

F

H

J

K

M

O

P

Q

R

T

U

V

W

X

Y

Z

(15 entries)

Definition Index

B

D

F

H

J

K

Q

T

U

V

W

X

Y

Z

_

(66 entries)

Library Index

A

B

D

E

F

H

I

J

K

O

T

U

V

W

X

Y

Z

_

(13 entries)

Global Index

A

acc_avcolor [lemma, in chordal_graph_coloring]
acc_avcolor_in [lemma, in chordal_graph_coloring]
acc_in_nghbs [lemma, in chordal_graph_coloring]
acc_le_avcolor [lemma, in chordal_graph_coloring]
acc_le_rank_in [lemma, in renaming]
acc_swap [lemma, in chordal_graph_coloring]
add_snd_sort [definition, in lth_in_proof]
all_in_order [lemma, in strict_ord]
app_nodup_eq [lemma, in peo_search]
ax1 [axiom, in graph_construction]

C

check_kcoloring [definition, in chordal_graph_coloring]
chordal_graph [inductive, in chordal_graph_optimality]
chordal_graph_coloring [library]
chordal_graph_coloring_fun [definition, in coloration_renaming]
chordal_graph_optimality [library]
clique_aux [lemma, in peo_search]
clique_construct [lemma, in peo_search]
clique_in [lemma, in peo_search]
clique_in_inv [lemma, in peo_search]
clique_le_graph_coloring [lemma, in chordal_graph_optimality]
clique_le_max_color [lemma, in chordal_graph_optimality]
clique_snd_in [lemma, in peo_search]
clique_sv [lemma, in peo_search]
clique_sv_aux [lemma, in peo_search]
clique_true [lemma, in peo_search]
coloration_renaming [library]
coloring_length [lemma, in coloration_renaming]
coloring_length_aux [lemma, in coloration_renaming]
coloring_optimality [lemma, in coloration_renaming]
coloring_renaming [definition, in coloration_renaming]
coloring_renaming_inv [definition, in coloration_renaming]
coloring_renaming_length [lemma, in coloration_renaming]
correct_get_available_color_aux [lemma, in chordal_graph_coloring]
correct_get_available_color__aux [lemma, in chordal_graph_coloring]
correct_graph_coloring1 [lemma, in chordal_graph_coloring]
correct_graph_coloring2 [lemma, in chordal_graph_coloring]
correct_graph_coloring2_aux1 [lemma, in chordal_graph_coloring]
correct_graph_coloring2_aux2 [lemma, in chordal_graph_coloring]
correct_graph_coloring2__aux1 [lemma, in chordal_graph_coloring]
correct_graph_coloring2__aux2 [lemma, in chordal_graph_coloring]
correct_graph_coloring3 [lemma, in chordal_graph_coloring]
correct_lto_edges1 [lemma, in graph_construction]
correct_lto_edges_aux2 [lemma, in graph_construction]

D

diff_color_clique [lemma, in chordal_graph_optimality]
diff_proj [lemma, in lex_sort]

E

edges_list [axiom, in graph_construction]
edges_nghbs [lemma, in chordal_graph_coloring]
edges_nghbs_aux [lemma, in chordal_graph_coloring]
edges_to_vertices [definition, in graph_construction]
edges_to_vertices_aux [definition, in graph_construction]
elim_dup [definition, in quicksort]
eq_vert [lemma, in renaming]
eq_vert_aux [lemma, in renaming]
eq_vert_aux2_l [lemma, in renaming]
eq_vert_aux2_r [lemma, in renaming]
eq_vert_aux3 [lemma, in renaming]
eq_vert_aux_aux [lemma, in renaming]
ext_acc [lemma, in chordal_graph_coloring]
ex_peo_dec [lemma, in peo_search]
ex_peo_ex_sv [lemma, in peo_search]

F

fst_dup_dup [lemma, in strict_inc_and_dec]

G

get_available_color [definition, in chordal_graph_coloring]
get_available_color_aux [definition, in chordal_graph_coloring]
get_available_color_ext_le [lemma, in chordal_graph_coloring]
get_available_color_get_used_colors [lemma, in chordal_graph_coloring]
get_available_color_get_used_colors_aux [lemma, in chordal_graph_coloring]
get_available_color__aux [definition, in chordal_graph_coloring]
get_avcolor_le_lth [lemma, in chordal_graph_optimality]
get_avcolor_le_lth_aux [lemma, in chordal_graph_optimality]
get_nghbs [definition, in chordal_graph_coloring]
get_nghbs_aux [definition, in chordal_graph_coloring]
get_used_colors2 [definition, in chordal_graph_coloring]
get_used_colors2_aux [definition, in chordal_graph_coloring]
get_used_colors2_ext_out [lemma, in chordal_graph_coloring]
get_used_colors2_lth_le [lemma, in chordal_graph_optimality]
ge_max_color_acc [lemma, in max_color]
graph [inductive, in graph_construction]
graph_coloring [definition, in chordal_graph_coloring]
graph_coloring_aux [definition, in chordal_graph_coloring]
graph_coloring_le_lth [lemma, in chordal_graph_optimality]
graph_coloring_optimality [lemma, in chordal_graph_optimality]
graph_construction [library]

I

inc_dec_perm [lemma, in renaming]
inc_perm_eq [lemma, in renaming]
inject_aux [lemma, in coloration_renaming]
inject_coloring [lemma, in coloration_renaming]
intervalle_dec [definition, in renaming]
intervalle_inc [definition, in renaming]
intervalle_inc_aux [definition, in renaming]
intervalle_lth [lemma, in renaming]
in_acc_graph_coloring [lemma, in chordal_graph_coloring]
in_avcolor_get [lemma, in chordal_graph_coloring]
in_avcolor_get__aux [lemma, in chordal_graph_coloring]
in_coloring [lemma, in coloration_renaming]
in_coloring_renaming [lemma, in coloration_renaming]
in_coloring_renaming_inv [lemma, in coloration_renaming]
in_dup [lemma, in quicksort]
in_dup_aux [lemma, in quicksort]
in_edges_only [lemma, in graph_construction]
in_edges_only_aux [lemma, in graph_construction]
in_elim_dup [lemma, in quicksort]
in_elim_dup_aux [lemma, in quicksort]
in_ex_app [lemma, in peo_search]
in_get_used_colors2 [lemma, in chordal_graph_coloring]
in_get_used_colors2_aux1 [lemma, in chordal_graph_coloring]
in_get_used_colors2_aux2 [lemma, in chordal_graph_coloring]
in_get_used_colors2__aux2 [lemma, in chordal_graph_coloring]
in_interv_le [lemma, in renaming]
in_max_color [lemma, in max_color]
in_max_color_aux [lemma, in max_color]
in_nat_dup [lemma, in nat_quicksort]
in_nat_elim_dup [lemma, in nat_quicksort]
in_nat_nat_dup [lemma, in strict_ord]
in_nat_nat_dup_aux [lemma, in strict_ord]
in_nat_nat_elim_dup [lemma, in strict_ord]
in_nat_nat_elim_dup_aux [lemma, in strict_ord]
in_NoDup_remove [lemma, in peo_search]
in_rank_in [lemma, in coloration_renaming]
in_rank_in_inv [lemma, in coloration_renaming]
in_remove_lth [lemma, in peo_search]
in_rename [lemma, in coloration_renaming]
in_rename_col_inv [lemma, in coloration_renaming]
in_rename_edg_l [lemma, in renaming]
in_rename_edg_le_lth [lemma, in renaming]
in_rename_edg_r [lemma, in renaming]
in_rename_in [lemma, in renaming]
in_rename_inv_rank [lemma, in coloration_renaming]
in_rename_in_aux [lemma, in renaming]
in_rename_in_inv [lemma, in renaming]
in_rename_in_inv_aux [lemma, in renaming]
in_rename_in_inv__aux [lemma, in renaming]
in_rename_vert_le_lth [lemma, in renaming]
in_rename_vert_le_lth_aux [lemma, in renaming]
in_restrict [lemma, in lth_in_proof]
in_restrict_keys [lemma, in lth_in_proof]
in_restrict_keys_aux [lemma, in lth_in_proof]
in_rev_sv [lemma, in renaming]
in_rm [lemma, in peo_search]
in_rm_aux [lemma, in peo_search]
in_rm_couple [lemma, in coloration_renaming]
in_rm_fst [lemma, in coloration_renaming]
in_rm_fst_diff [lemma, in coloration_renaming]
in_snd_is_clique_b_aux [lemma, in peo_search]
in_strict_sort [lemma, in strict_inc_and_dec]
in_sv_nghbs [lemma, in peo_search]
in_sv_nghbs_aux [lemma, in peo_search]
in_sv_nghbs_le [lemma, in peo_search]
in_sv_nghbs_tail [lemma, in peo_search]
in_sv_search_aux [lemma, in peo_search]
in_vertices [lemma, in graph_construction]
in_vertices_aux [lemma, in graph_construction]
in_vert_in_rev_mypeo [lemma, in renaming]
is_clique [inductive, in graph_construction]
is_clique_b [definition, in peo_search]
is_clique_b_aux [definition, in peo_search]
is_clique_b_aux_true [lemma, in peo_search]
is_clique_cons [constructor, in graph_construction]
is_coloring [inductive, in chordal_graph_coloring]
is_coloring_cons [constructor, in chordal_graph_coloring]
is_coloring_graph_coloring [lemma, in chordal_graph_coloring]
is_coloring_renaming [lemma, in coloration_renaming]
is_coloring_renaming_inv [lemma, in coloration_renaming]
is_lex_sorted [definition, in lex_sort]
is_lex_sorted_lex_sort [lemma, in lex_sort]
is_lex_sorted_rmsnd [lemma, in lex_sort]
is_lex_sorted_tail [lemma, in lex_sort]
is_peo [definition, in peo_search]
is_perm_lex_sort [lemma, in lex_sort]
is_sorted [inductive, in quicksort]
is_sorted_add_hd [lemma, in quicksort]
is_sorted_cat [lemma, in quicksort]
is_sorted_cons [constructor, in quicksort]
is_sorted_elim_dup [lemma, in nat_quicksort]
is_sorted_elim_dup_aux [lemma, in nat_quicksort]
is_sorted_head_min [lemma, in quicksort]
is_sorted_in [lemma, in nat_quicksort]
is_sorted_lto_edges [lemma, in graph_construction]
is_sorted_nil [constructor, in quicksort]
is_sorted_quicksort [lemma, in quicksort]
is_sorted_rmsnd [lemma, in quicksort]
is_sorted_rmsnd [lemma, in nat_quicksort]
is_sorted_singleton [constructor, in quicksort]
is_sorted_tail [lemma, in quicksort]
is_strict_dec [inductive, in strict_inc_and_dec]
is_strict_dec_cons [constructor, in strict_inc_and_dec]
is_strict_dec_fst [inductive, in strict_inc_and_dec]
is_strict_dec_fst_cons [constructor, in strict_inc_and_dec]
is_strict_dec_fst_graph_coloring [lemma, in chordal_graph_coloring]
is_strict_dec_fst_graph_coloring_aux [lemma, in chordal_graph_coloring]
is_strict_dec_fst_graph_coloring__aux [lemma, in chordal_graph_coloring]
is_strict_dec_fst_nil [constructor, in strict_inc_and_dec]
is_strict_dec_fst_sing [constructor, in strict_inc_and_dec]
is_strict_dec_nil [constructor, in strict_inc_and_dec]
is_strict_dec_rmsnd [lemma, in strict_inc_and_dec]
is_strict_dec_sing [constructor, in strict_inc_and_dec]
is_strict_dec_tail [lemma, in strict_inc_and_dec]
is_strict_inc [inductive, in strict_inc_and_dec]
is_strict_inc_add_snd [lemma, in lth_in_proof]
is_strict_inc_cons [constructor, in strict_inc_and_dec]
is_strict_inc_nil [constructor, in strict_inc_and_dec]
is_strict_inc_rmsnd [lemma, in strict_inc_and_dec]
is_strict_inc_sing [constructor, in strict_inc_and_dec]
is_strict_inc_snd [inductive, in lth_in_proof]
is_strict_inc_snd_cons [constructor, in lth_in_proof]
is_strict_inc_snd_nil [constructor, in lth_in_proof]
is_strict_inc_snd_sing [constructor, in lth_in_proof]
is_strict_inc_tail [lemma, in strict_inc_and_dec]
is_strict_inc_vertices [lemma, in graph_construction]
is_strict_ord [inductive, in strict_ord]
is_strict_ord_cons [constructor, in strict_ord]
is_strict_ord_lto_edges [lemma, in graph_construction]
is_strict_ord_nil [constructor, in strict_ord]
is_sv [definition, in peo_search]

L

length_no_fst_dup_remove_fst [lemma, in coloration_renaming]
lex_cons_diff [constructor, in lex_sort]
lex_cons_eq [constructor, in lex_sort]
lex_order [inductive, in lex_sort]
lex_order_antisym [lemma, in lex_sort]
lex_order_dec [lemma, in lex_sort]
lex_order_total [lemma, in lex_sort]
lex_order_trans [lemma, in lex_sort]
lex_rm [lemma, in peo_search]
lex_rm_aux [lemma, in peo_search]
lex_sort [definition, in lex_sort]
lex_sort [library]
lex_sort_add_hd [lemma, in lex_sort]
lex_sort_clique_b_aux [lemma, in peo_search]
lex_sort_nat_nat_elim_dup [lemma, in strict_ord]
le_dec [definition, in nat_quicksort]
list_decompose_inv [lemma, in renaming]
lth_in [lemma, in lth_in_proof]
lth_inject [lemma, in lth_in_proof]
lth_in_proof [library]
lth_le [lemma, in lth_in_proof]
lth_le_aux [lemma, in lth_in_proof]
lth_le__aux [lemma, in lth_in_proof]
lth_nat_elim_dup [lemma, in nat_quicksort]
lth_quicksort [lemma, in nat_quicksort]
lth_rename_eq [lemma, in renaming]
lth_rename_vert_eq_aux [lemma, in renaming]
lth_restrict [lemma, in lth_in_proof]
lth_restrict_aux [lemma, in lth_in_proof]
lth_restrict__aux [lemma, in lth_in_proof]
lth_0_nil [lemma, in nat_quicksort]
lto_edges [definition, in graph_construction]

M

max_color [definition, in max_color]
max_color [library]
max_color_aux [definition, in max_color]
max_color_col_rename [lemma, in coloration_renaming]
max_color_col_rename_aux [lemma, in coloration_renaming]
max_color_lth [lemma, in lth_in_proof]
max_color_lth_aux [lemma, in lth_in_proof]
max_color_lth__aux [lemma, in lth_in_proof]
max_color_nil_0 [lemma, in max_color]
max_color_renaming_inv_eq [lemma, in coloration_renaming]
max_color_renaming_inv_eq_aux [lemma, in coloration_renaming]
max_max_color [lemma, in max_color]
max_max_color_aux [lemma, in max_color]
my_chordal_gph [definition, in renaming]
my_chordal_gph_edg [definition, in renaming]
my_chordal_gph_vert [definition, in renaming]
my_chordal_graph [definition, in renaming]
my_graph [definition, in graph_construction]
my_l [definition, in renaming]
my_peo [definition, in renaming]
my_peo_eq [lemma, in renaming]
my_v [definition, in renaming]

N

nat_elim_dup [definition, in nat_quicksort]
nat_nat_elim_dup [definition, in strict_ord]
nat_nat_eq_dec [definition, in lex_sort]
nat_quicksort [definition, in nat_quicksort]
nat_quicksort [library]
new_edg [definition, in renaming]
nghbs_edges [lemma, in chordal_graph_coloring]
nghbs_edges_aux [lemma, in chordal_graph_coloring]
nil [definition, in quicksort]
nil [definition, in peo_search]
nil_restrict [lemma, in lth_in_proof]
nodup_app_in_l [lemma, in peo_search]
nodup_app_in_r [lemma, in peo_search]
NoDup_diff [lemma, in lth_in_proof]
NoDup_elim_dup [lemma, in quicksort]
NoDup_get_nghbs [lemma, in chordal_graph_coloring]
NoDup_get_nghbs_aux [lemma, in chordal_graph_coloring]
nodup_in_app [lemma, in peo_search]
NoDup_lex_sort_diff [lemma, in lex_sort]
NoDup_lto_edges [lemma, in graph_construction]
NoDup_nat_elim_dup [lemma, in nat_quicksort]
NoDup_nat_nat_elim_dup [lemma, in strict_ord]
NoDup_perm [lemma, in nat_quicksort]
NoDup_rank_diff [lemma, in coloration_renaming]
NoDup_remove [lemma, in peo_search]
NoDup_restrict [lemma, in lth_in_proof]
NoDup_rev_mypeo [lemma, in renaming]
NoDup_rm [lemma, in peo_search]
NoDup_rmsnd [lemma, in quicksort]
NoDup_rm_app_l [lemma, in peo_search]
not_in_greaterx_nghbsx [lemma, in chordal_graph_coloring]
not_in_greaterx_nghbsx_aux [lemma, in chordal_graph_coloring]
not_in_rank [lemma, in renaming]
not_in_remove_nat_nat [lemma, in coloration_renaming]
not_in_x_nghbsx [lemma, in chordal_graph_coloring]
not_in_x_nghbsx_aux [lemma, in chordal_graph_coloring]
not_order_order [lemma, in quicksort]
not_sv [lemma, in peo_search]
no_fst_dup [inductive, in strict_inc_and_dec]
no_fst_dup_colors2_aux [lemma, in chordal_graph_coloring]
no_fst_dup_cons [constructor, in strict_inc_and_dec]
no_fst_dup_conservation [lemma, in coloration_renaming]
no_fst_dup_graph_coloring [lemma, in chordal_graph_coloring]
no_fst_dup_graph_coloring_aux [lemma, in chordal_graph_coloring]
no_fst_dup_nil [constructor, in strict_inc_and_dec]
no_fst_dup_remove_fst [lemma, in coloration_renaming]
no_fst_dup_renaming_col_inv [lemma, in coloration_renaming]
no_fst_dup_rm [lemma, in coloration_renaming]
no_fst_dup_strict_dec_fst [lemma, in strict_inc_and_dec]
no_snd_dup [inductive, in lth_in_proof]
no_snd_dup_cons [constructor, in lth_in_proof]
no_snd_dup_nil [constructor, in lth_in_proof]
no_snd_dup_perm_add_snd [lemma, in lth_in_proof]
no_snd_dup_strict_inc_snd [lemma, in lth_in_proof]

O

only_in_interv_le [lemma, in renaming]
only_in_order [lemma, in strict_ord]
only_in_rm_couple [lemma, in coloration_renaming]
only_restrict [lemma, in lth_in_proof]
order [definition, in strict_ord]
order_refl [lemma, in quicksort]

P

partition [definition, in quicksort]
partition_gt [lemma, in quicksort]
partition_le [lemma, in quicksort]
partition_length_l [lemma, in quicksort]
partition_length_r [lemma, in quicksort]
peo [definition, in graph_construction]
peo_clique [lemma, in renaming]
peo_cons [constructor, in graph_construction]
peo_dec [lemma, in peo_search]
peo_lto_edges [lemma, in renaming]
peo_my_peo [lemma, in renaming]
peo_peo_search [lemma, in peo_search]
peo_peo_search_aux [lemma, in peo_search]
peo_perm [lemma, in renaming]
peo_renaming2 [lemma, in renaming]
peo_search [definition, in peo_search]
peo_search [library]
peo_to_peo [lemma, in renaming]
peo_to_peo_aux [lemma, in renaming]
peo_vertices [lemma, in renaming]
Permutation_col [lemma, in coloration_renaming]
permutation_partition [lemma, in quicksort]
permutation_quicksort [lemma, in quicksort]
perm_add_snd [lemma, in lth_in_proof]
positive_in_rename [lemma, in renaming]

Q

quicksort [library]
quicksort_in [lemma, in quicksort]

R

rank [definition, in renaming]
rank_app_eq [lemma, in renaming]
rank_eq [lemma, in renaming]
rank_le [lemma, in renaming]
rank_le_lth [lemma, in renaming]
rank_lth [lemma, in renaming]
rank_next [lemma, in renaming]
rank_next_aux [lemma, in renaming]
rank_S [lemma, in renaming]
remove_fst [definition, in coloration_renaming]
remove_fst_not_in [lemma, in coloration_renaming]
remove_in [lemma, in peo_search]
remove_lth [lemma, in peo_search]
remove_not_in [lemma, in peo_search]
remove_peo [lemma, in peo_search]
rename_edg [definition, in renaming]
rename_fun [definition, in renaming]
rename_fun_aux [definition, in renaming]
rename_fun_fst [lemma, in renaming]
rename_hd [lemma, in renaming]
rename_interv [lemma, in renaming]
rename_inv [lemma, in renaming]
rename_inv_app [lemma, in renaming]
rename_inv_aux [lemma, in renaming]
rename_inv_rev [lemma, in renaming]
rename_inv_rev_aux [lemma, in renaming]
rename_inv__aux [lemma, in renaming]
rename_length [lemma, in coloration_renaming]
rename_length_aux [lemma, in coloration_renaming]
rename_lth_eq [lemma, in renaming]
rename_not_in [lemma, in renaming]
rename_rev_dec [lemma, in renaming]
rename_rev_dec_aux [lemma, in renaming]
rename_rev_dec_ext [lemma, in renaming]
rename_rev_rev_eq [lemma, in renaming]
rename_semi_rev [lemma, in renaming]
rename_semi_rev_aux [lemma, in renaming]
rename_semi_rev_l [lemma, in renaming]
rename_vert [definition, in renaming]
rename_vert_aux [definition, in renaming]
rename_vert_diff [lemma, in renaming]
rename_vert_inv [definition, in renaming]
rename_vert_inv_aux [definition, in renaming]
rename_vert_inv_in [lemma, in renaming]
rename_vert_inv__aux [definition, in renaming]
renaming [library]
renaming_perm [lemma, in renaming]
restriction [definition, in lth_in_proof]
rev_app [lemma, in renaming]
rev_dec_inc [lemma, in strict_inc_and_dec]
rev_dec_inc_aux [lemma, in strict_inc_and_dec]
rev_inc_dec [lemma, in strict_inc_and_dec]
rev_inc_dec_aux [lemma, in strict_inc_and_dec]
rm [definition, in peo_search]
rm_app [lemma, in peo_search]
rm_diff [lemma, in peo_search]
rm_in [lemma, in peo_search]
rm_length_NoDup [lemma, in coloration_renaming]
rm_NoDup [lemma, in peo_search]
rm_nodup_lth [lemma, in peo_search]
rm_only_diff [lemma, in peo_search]
rm_perm [lemma, in peo_search]

S

snd_add_nil [lemma, in lth_in_proof]
snd_is_clique_b_aux_prop [lemma, in peo_search]
snd_perm [lemma, in lth_in_proof]
snd_sort [definition, in lth_in_proof]
snd_sort_nil [lemma, in lth_in_proof]
sort_elim_dup [lemma, in quicksort]
sort_NoDup_strict_inc [lemma, in strict_inc_and_dec]
strict_dec [lemma, in strict_inc_and_dec]
strict_dec_fst_in [lemma, in strict_inc_and_dec]
strict_dec_fst_rmsnd [lemma, in strict_inc_and_dec]
strict_dec_in [lemma, in strict_inc_and_dec]
strict_dec_interv [lemma, in renaming]
strict_dec_nghbs [lemma, in chordal_graph_coloring]
strict_dec_used_colors2 [lemma, in chordal_graph_coloring]
strict_in [lemma, in strict_ord]
strict_inc_add_hd [lemma, in strict_inc_and_dec]
strict_inc_and_dec [library]
strict_inc_app_r [lemma, in renaming]
strict_inc_NoDup [lemma, in strict_inc_and_dec]
strict_inc_rename [lemma, in renaming]
strict_inc_rename_aux [lemma, in renaming]
strict_inc_rename_rev_my_peo [lemma, in renaming]
strict_inc_rename_rev_my_peo_aux [lemma, in renaming]
strict_inc_rev_nghbs__aux [lemma, in chordal_graph_coloring]
strict_inc_sv_nghbs [lemma, in peo_search]
strict_ord [library]
strict_ord_clique_b_aux [lemma, in peo_search]
strict_ord_lex [lemma, in strict_ord]
strict_ord_lex_aux [lemma, in strict_ord]
strict_ord_nat_nat_elim_dup [lemma, in strict_ord]
strict_ord_order [lemma, in strict_ord]
strict_ord_rm [lemma, in peo_search]
strict_sort_in [lemma, in lex_sort]
sv [inductive, in graph_construction]
sv_add_hd [lemma, in peo_search]
sv_clique [lemma, in peo_search]
sv_cons [constructor, in graph_construction]
sv_dec [lemma, in peo_search]
sv_equiv [lemma, in peo_search]
sv_nghbs [definition, in peo_search]
sv_nghbs_add [lemma, in peo_search]
sv_nghbs_aux [definition, in peo_search]
sv_nghbs_swap [lemma, in peo_search]
sv_perm [lemma, in peo_search]
sv_remove [lemma, in peo_search]
sv_rename [lemma, in renaming]
sv_rm [lemma, in peo_search]
sv_search [definition, in peo_search]
sv_search_aux [definition, in peo_search]
sv_simplicial_vertex_aux [lemma, in peo_search]
sv_simplicial_vertex_aux2 [lemma, in peo_search]
sv_sv_search_aux [lemma, in peo_search]

_

_peo [inductive, in graph_construction]
_peo_construction [lemma, in peo_search]
_peo_dec [lemma, in peo_search]

Axiom Index

A

ax1 [in graph_construction]

E

edges_list [in graph_construction]

Lemma Index

A

acc_avcolor [in chordal_graph_coloring]
acc_avcolor_in [in chordal_graph_coloring]
acc_in_nghbs [in chordal_graph_coloring]
acc_le_avcolor [in chordal_graph_coloring]
acc_le_rank_in [in renaming]
acc_swap [in chordal_graph_coloring]
all_in_order [in strict_ord]
app_nodup_eq [in peo_search]

C

clique_aux [in peo_search]
clique_construct [in peo_search]
clique_in [in peo_search]
clique_in_inv [in peo_search]
clique_le_graph_coloring [in chordal_graph_optimality]
clique_le_max_color [in chordal_graph_optimality]
clique_snd_in [in peo_search]
clique_sv [in peo_search]
clique_sv_aux [in peo_search]
clique_true [in peo_search]
coloring_length [in coloration_renaming]
coloring_length_aux [in coloration_renaming]
coloring_optimality [in coloration_renaming]
coloring_renaming_length [in coloration_renaming]
correct_get_available_color_aux [in chordal_graph_coloring]
correct_get_available_color__aux [in chordal_graph_coloring]
correct_graph_coloring1 [in chordal_graph_coloring]
correct_graph_coloring2 [in chordal_graph_coloring]
correct_graph_coloring2_aux1 [in chordal_graph_coloring]
correct_graph_coloring2_aux2 [in chordal_graph_coloring]
correct_graph_coloring2__aux1 [in chordal_graph_coloring]
correct_graph_coloring2__aux2 [in chordal_graph_coloring]
correct_graph_coloring3 [in chordal_graph_coloring]
correct_lto_edges1 [in graph_construction]
correct_lto_edges_aux2 [in graph_construction]

D

diff_color_clique [in chordal_graph_optimality]
diff_proj [in lex_sort]

E

edges_nghbs [in chordal_graph_coloring]
edges_nghbs_aux [in chordal_graph_coloring]
eq_vert [in renaming]
eq_vert_aux [in renaming]
eq_vert_aux2_l [in renaming]
eq_vert_aux2_r [in renaming]
eq_vert_aux3 [in renaming]
eq_vert_aux_aux [in renaming]
ext_acc [in chordal_graph_coloring]
ex_peo_dec [in peo_search]
ex_peo_ex_sv [in peo_search]

F

fst_dup_dup [in strict_inc_and_dec]

G

get_available_color_ext_le [in chordal_graph_coloring]
get_available_color_get_used_colors [in chordal_graph_coloring]
get_available_color_get_used_colors_aux [in chordal_graph_coloring]
get_avcolor_le_lth [in chordal_graph_optimality]
get_avcolor_le_lth_aux [in chordal_graph_optimality]
get_used_colors2_ext_out [in chordal_graph_coloring]
get_used_colors2_lth_le [in chordal_graph_optimality]
ge_max_color_acc [in max_color]
graph_coloring_le_lth [in chordal_graph_optimality]
graph_coloring_optimality [in chordal_graph_optimality]

I

inc_dec_perm [in renaming]
inc_perm_eq [in renaming]
inject_aux [in coloration_renaming]
inject_coloring [in coloration_renaming]
intervalle_lth [in renaming]
in_acc_graph_coloring [in chordal_graph_coloring]
in_avcolor_get [in chordal_graph_coloring]
in_avcolor_get__aux [in chordal_graph_coloring]
in_coloring [in coloration_renaming]
in_coloring_renaming [in coloration_renaming]
in_coloring_renaming_inv [in coloration_renaming]
in_dup [in quicksort]
in_dup_aux [in quicksort]
in_edges_only [in graph_construction]
in_edges_only_aux [in graph_construction]
in_elim_dup [in quicksort]
in_elim_dup_aux [in quicksort]
in_ex_app [in peo_search]
in_get_used_colors2 [in chordal_graph_coloring]
in_get_used_colors2_aux1 [in chordal_graph_coloring]
in_get_used_colors2_aux2 [in chordal_graph_coloring]
in_get_used_colors2__aux2 [in chordal_graph_coloring]
in_interv_le [in renaming]
in_max_color [in max_color]
in_max_color_aux [in max_color]
in_nat_dup [in nat_quicksort]
in_nat_elim_dup [in nat_quicksort]
in_nat_nat_dup [in strict_ord]
in_nat_nat_dup_aux [in strict_ord]
in_nat_nat_elim_dup [in strict_ord]
in_nat_nat_elim_dup_aux [in strict_ord]
in_NoDup_remove [in peo_search]
in_rank_in [in coloration_renaming]
in_rank_in_inv [in coloration_renaming]
in_remove_lth [in peo_search]
in_rename [in coloration_renaming]
in_rename_col_inv [in coloration_renaming]
in_rename_edg_l [in renaming]
in_rename_edg_le_lth [in renaming]
in_rename_edg_r [in renaming]
in_rename_in [in renaming]
in_rename_inv_rank [in coloration_renaming]
in_rename_in_aux [in renaming]
in_rename_in_inv [in renaming]
in_rename_in_inv_aux [in renaming]
in_rename_in_inv__aux [in renaming]
in_rename_vert_le_lth [in renaming]
in_rename_vert_le_lth_aux [in renaming]
in_restrict [in lth_in_proof]
in_restrict_keys [in lth_in_proof]
in_restrict_keys_aux [in lth_in_proof]
in_rev_sv [in renaming]
in_rm [in peo_search]
in_rm_aux [in peo_search]
in_rm_couple [in coloration_renaming]
in_rm_fst [in coloration_renaming]
in_rm_fst_diff [in coloration_renaming]
in_snd_is_clique_b_aux [in peo_search]
in_strict_sort [in strict_inc_and_dec]
in_sv_nghbs [in peo_search]
in_sv_nghbs_aux [in peo_search]
in_sv_nghbs_le [in peo_search]
in_sv_nghbs_tail [in peo_search]
in_sv_search_aux [in peo_search]
in_vertices [in graph_construction]
in_vertices_aux [in graph_construction]
in_vert_in_rev_mypeo [in renaming]
is_clique_b_aux_true [in peo_search]
is_coloring_graph_coloring [in chordal_graph_coloring]
is_coloring_renaming [in coloration_renaming]
is_coloring_renaming_inv [in coloration_renaming]
is_lex_sorted_lex_sort [in lex_sort]
is_lex_sorted_rmsnd [in lex_sort]
is_lex_sorted_tail [in lex_sort]
is_perm_lex_sort [in lex_sort]
is_sorted_add_hd [in quicksort]
is_sorted_cat [in quicksort]
is_sorted_elim_dup [in nat_quicksort]
is_sorted_elim_dup_aux [in nat_quicksort]
is_sorted_head_min [in quicksort]
is_sorted_in [in nat_quicksort]
is_sorted_lto_edges [in graph_construction]
is_sorted_quicksort [in quicksort]
is_sorted_rmsnd [in quicksort]
is_sorted_rmsnd [in nat_quicksort]
is_sorted_tail [in quicksort]
is_strict_dec_fst_graph_coloring [in chordal_graph_coloring]
is_strict_dec_fst_graph_coloring_aux [in chordal_graph_coloring]
is_strict_dec_fst_graph_coloring__aux [in chordal_graph_coloring]
is_strict_dec_rmsnd [in strict_inc_and_dec]
is_strict_dec_tail [in strict_inc_and_dec]
is_strict_inc_add_snd [in lth_in_proof]
is_strict_inc_rmsnd [in strict_inc_and_dec]
is_strict_inc_tail [in strict_inc_and_dec]
is_strict_inc_vertices [in graph_construction]
is_strict_ord_lto_edges [in graph_construction]

L

length_no_fst_dup_remove_fst [in coloration_renaming]
lex_order_antisym [in lex_sort]
lex_order_dec [in lex_sort]
lex_order_total [in lex_sort]
lex_order_trans [in lex_sort]
lex_rm [in peo_search]
lex_rm_aux [in peo_search]
lex_sort_add_hd [in lex_sort]
lex_sort_clique_b_aux [in peo_search]
lex_sort_nat_nat_elim_dup [in strict_ord]
list_decompose_inv [in renaming]
lth_in [in lth_in_proof]
lth_inject [in lth_in_proof]
lth_le [in lth_in_proof]
lth_le_aux [in lth_in_proof]
lth_le__aux [in lth_in_proof]
lth_nat_elim_dup [in nat_quicksort]
lth_quicksort [in nat_quicksort]
lth_rename_eq [in renaming]
lth_rename_vert_eq_aux [in renaming]
lth_restrict [in lth_in_proof]
lth_restrict_aux [in lth_in_proof]
lth_restrict__aux [in lth_in_proof]
lth_0_nil [in nat_quicksort]

M

max_color_col_rename [in coloration_renaming]
max_color_col_rename_aux [in coloration_renaming]
max_color_lth [in lth_in_proof]
max_color_lth_aux [in lth_in_proof]
max_color_lth__aux [in lth_in_proof]
max_color_nil_0 [in max_color]
max_color_renaming_inv_eq [in coloration_renaming]
max_color_renaming_inv_eq_aux [in coloration_renaming]
max_max_color [in max_color]
max_max_color_aux [in max_color]
my_peo_eq [in renaming]

N

nghbs_edges [in chordal_graph_coloring]
nghbs_edges_aux [in chordal_graph_coloring]
nil_restrict [in lth_in_proof]
nodup_app_in_l [in peo_search]
nodup_app_in_r [in peo_search]
NoDup_diff [in lth_in_proof]
NoDup_elim_dup [in quicksort]
NoDup_get_nghbs [in chordal_graph_coloring]
NoDup_get_nghbs_aux [in chordal_graph_coloring]
nodup_in_app [in peo_search]
NoDup_lex_sort_diff [in lex_sort]
NoDup_lto_edges [in graph_construction]
NoDup_nat_elim_dup [in nat_quicksort]
NoDup_nat_nat_elim_dup [in strict_ord]
NoDup_perm [in nat_quicksort]
NoDup_rank_diff [in coloration_renaming]
NoDup_remove [in peo_search]
NoDup_restrict [in lth_in_proof]
NoDup_rev_mypeo [in renaming]
NoDup_rm [in peo_search]
NoDup_rmsnd [in quicksort]
NoDup_rm_app_l [in peo_search]
not_in_greaterx_nghbsx [in chordal_graph_coloring]
not_in_greaterx_nghbsx_aux [in chordal_graph_coloring]
not_in_rank [in renaming]
not_in_remove_nat_nat [in coloration_renaming]
not_in_x_nghbsx [in chordal_graph_coloring]
not_in_x_nghbsx_aux [in chordal_graph_coloring]
not_order_order [in quicksort]
not_sv [in peo_search]
no_fst_dup_colors2_aux [in chordal_graph_coloring]
no_fst_dup_conservation [in coloration_renaming]
no_fst_dup_graph_coloring [in chordal_graph_coloring]
no_fst_dup_graph_coloring_aux [in chordal_graph_coloring]
no_fst_dup_remove_fst [in coloration_renaming]
no_fst_dup_renaming_col_inv [in coloration_renaming]
no_fst_dup_rm [in coloration_renaming]
no_fst_dup_strict_dec_fst [in strict_inc_and_dec]
no_snd_dup_perm_add_snd [in lth_in_proof]
no_snd_dup_strict_inc_snd [in lth_in_proof]

O

only_in_interv_le [in renaming]
only_in_order [in strict_ord]
only_in_rm_couple [in coloration_renaming]
only_restrict [in lth_in_proof]
order_refl [in quicksort]

P

partition_gt [in quicksort]
partition_le [in quicksort]
partition_length_l [in quicksort]
partition_length_r [in quicksort]
peo_clique [in renaming]
peo_dec [in peo_search]
peo_lto_edges [in renaming]
peo_my_peo [in renaming]
peo_peo_search [in peo_search]
peo_peo_search_aux [in peo_search]
peo_perm [in renaming]
peo_renaming2 [in renaming]
peo_to_peo [in renaming]
peo_to_peo_aux [in renaming]
peo_vertices [in renaming]
Permutation_col [in coloration_renaming]
permutation_partition [in quicksort]
permutation_quicksort [in quicksort]
perm_add_snd [in lth_in_proof]
positive_in_rename [in renaming]

Q

quicksort_in [in quicksort]

R

rank_app_eq [in renaming]
rank_eq [in renaming]
rank_le [in renaming]
rank_le_lth [in renaming]
rank_lth [in renaming]
rank_next [in renaming]
rank_next_aux [in renaming]
rank_S [in renaming]
remove_fst_not_in [in coloration_renaming]
remove_in [in peo_search]
remove_lth [in peo_search]
remove_not_in [in peo_search]
remove_peo [in peo_search]
rename_fun_fst [in renaming]
rename_hd [in renaming]
rename_interv [in renaming]
rename_inv [in renaming]
rename_inv_app [in renaming]
rename_inv_aux [in renaming]
rename_inv_rev [in renaming]
rename_inv_rev_aux [in renaming]
rename_inv__aux [in renaming]
rename_length [in coloration_renaming]
rename_length_aux [in coloration_renaming]
rename_lth_eq [in renaming]
rename_not_in [in renaming]
rename_rev_dec [in renaming]
rename_rev_dec_aux [in renaming]
rename_rev_dec_ext [in renaming]
rename_rev_rev_eq [in renaming]
rename_semi_rev [in renaming]
rename_semi_rev_aux [in renaming]
rename_semi_rev_l [in renaming]
rename_vert_diff [in renaming]
rename_vert_inv_in [in renaming]
renaming_perm [in renaming]
rev_app [in renaming]
rev_dec_inc [in strict_inc_and_dec]
rev_dec_inc_aux [in strict_inc_and_dec]
rev_inc_dec [in strict_inc_and_dec]
rev_inc_dec_aux [in strict_inc_and_dec]
rm_app [in peo_search]
rm_diff [in peo_search]
rm_in [in peo_search]
rm_length_NoDup [in coloration_renaming]
rm_NoDup [in peo_search]
rm_nodup_lth [in peo_search]
rm_only_diff [in peo_search]
rm_perm [in peo_search]

S

snd_add_nil [in lth_in_proof]
snd_is_clique_b_aux_prop [in peo_search]
snd_perm [in lth_in_proof]
snd_sort_nil [in lth_in_proof]
sort_elim_dup [in quicksort]
sort_NoDup_strict_inc [in strict_inc_and_dec]
strict_dec [in strict_inc_and_dec]
strict_dec_fst_in [in strict_inc_and_dec]
strict_dec_fst_rmsnd [in strict_inc_and_dec]
strict_dec_in [in strict_inc_and_dec]
strict_dec_interv [in renaming]
strict_dec_nghbs [in chordal_graph_coloring]
strict_dec_used_colors2 [in chordal_graph_coloring]
strict_in [in strict_ord]
strict_inc_add_hd [in strict_inc_and_dec]
strict_inc_app_r [in renaming]
strict_inc_NoDup [in strict_inc_and_dec]
strict_inc_rename [in renaming]
strict_inc_rename_aux [in renaming]
strict_inc_rename_rev_my_peo [in renaming]
strict_inc_rename_rev_my_peo_aux [in renaming]
strict_inc_rev_nghbs__aux [in chordal_graph_coloring]
strict_inc_sv_nghbs [in peo_search]
strict_ord_clique_b_aux [in peo_search]
strict_ord_lex [in strict_ord]
strict_ord_lex_aux [in strict_ord]
strict_ord_nat_nat_elim_dup [in strict_ord]
strict_ord_order [in strict_ord]
strict_ord_rm [in peo_search]
strict_sort_in [in lex_sort]
sv_add_hd [in peo_search]
sv_clique [in peo_search]
sv_dec [in peo_search]
sv_equiv [in peo_search]
sv_nghbs_add [in peo_search]
sv_nghbs_swap [in peo_search]
sv_perm [in peo_search]
sv_remove [in peo_search]
sv_rename [in renaming]
sv_rm [in peo_search]
sv_simplicial_vertex_aux [in peo_search]
sv_simplicial_vertex_aux2 [in peo_search]
sv_sv_search_aux [in peo_search]

_

_peo_construction [in peo_search]
_peo_dec [in peo_search]

Constructor Index

I

is_clique_cons [in graph_construction]
is_coloring_cons [in chordal_graph_coloring]
is_sorted_cons [in quicksort]
is_sorted_nil [in quicksort]
is_sorted_singleton [in quicksort]
is_strict_dec_cons [in strict_inc_and_dec]
is_strict_dec_fst_cons [in strict_inc_and_dec]
is_strict_dec_fst_nil [in strict_inc_and_dec]
is_strict_dec_fst_sing [in strict_inc_and_dec]
is_strict_dec_nil [in strict_inc_and_dec]
is_strict_dec_sing [in strict_inc_and_dec]
is_strict_inc_cons [in strict_inc_and_dec]
is_strict_inc_nil [in strict_inc_and_dec]
is_strict_inc_sing [in strict_inc_and_dec]
is_strict_inc_snd_cons [in lth_in_proof]
is_strict_inc_snd_nil [in lth_in_proof]
is_strict_inc_snd_sing [in lth_in_proof]
is_strict_ord_cons [in strict_ord]
is_strict_ord_nil [in strict_ord]

L

lex_cons_diff [in lex_sort]
lex_cons_eq [in lex_sort]

N

no_fst_dup_cons [in strict_inc_and_dec]
no_fst_dup_nil [in strict_inc_and_dec]
no_snd_dup_cons [in lth_in_proof]
no_snd_dup_nil [in lth_in_proof]

P

peo_cons [in graph_construction]

S

sv_cons [in graph_construction]

Inductive Index

C

chordal_graph [in chordal_graph_optimality]

G

graph [in graph_construction]

I

is_clique [in graph_construction]
is_coloring [in chordal_graph_coloring]
is_sorted [in quicksort]
is_strict_dec [in strict_inc_and_dec]
is_strict_dec_fst [in strict_inc_and_dec]
is_strict_inc [in strict_inc_and_dec]
is_strict_inc_snd [in lth_in_proof]
is_strict_ord [in strict_ord]

L

lex_order [in lex_sort]

N

no_fst_dup [in strict_inc_and_dec]
no_snd_dup [in lth_in_proof]

S

sv [in graph_construction]

_

_peo [in graph_construction]

Definition Index

A

add_snd_sort [in lth_in_proof]

C

check_kcoloring [in chordal_graph_coloring]
chordal_graph_coloring_fun [in coloration_renaming]
coloring_renaming [in coloration_renaming]
coloring_renaming_inv [in coloration_renaming]

E

edges_to_vertices [in graph_construction]
edges_to_vertices_aux [in graph_construction]
elim_dup [in quicksort]

G

get_available_color [in chordal_graph_coloring]
get_available_color_aux [in chordal_graph_coloring]
get_available_color__aux [in chordal_graph_coloring]
get_nghbs [in chordal_graph_coloring]
get_nghbs_aux [in chordal_graph_coloring]
get_used_colors2 [in chordal_graph_coloring]
get_used_colors2_aux [in chordal_graph_coloring]
graph_coloring [in chordal_graph_coloring]
graph_coloring_aux [in chordal_graph_coloring]

I

intervalle_dec [in renaming]
intervalle_inc [in renaming]
intervalle_inc_aux [in renaming]
is_clique_b [in peo_search]
is_clique_b_aux [in peo_search]
is_lex_sorted [in lex_sort]
is_peo [in peo_search]
is_sv [in peo_search]

L

lex_sort [in lex_sort]
le_dec [in nat_quicksort]
lto_edges [in graph_construction]

M

max_color [in max_color]
max_color_aux [in max_color]
my_chordal_gph [in renaming]
my_chordal_gph_edg [in renaming]
my_chordal_gph_vert [in renaming]
my_chordal_graph [in renaming]
my_graph [in graph_construction]
my_l [in renaming]
my_peo [in renaming]
my_v [in renaming]

N

nat_elim_dup [in nat_quicksort]
nat_nat_elim_dup [in strict_ord]
nat_nat_eq_dec [in lex_sort]
nat_quicksort [in nat_quicksort]
new_edg [in renaming]
nil [in quicksort]
nil [in peo_search]

O

order [in strict_ord]

P

partition [in quicksort]
peo [in graph_construction]
peo_search [in peo_search]

R

rank [in renaming]
remove_fst [in coloration_renaming]
rename_edg [in renaming]
rename_fun [in renaming]
rename_fun_aux [in renaming]
rename_vert [in renaming]
rename_vert_aux [in renaming]
rename_vert_inv [in renaming]
rename_vert_inv_aux [in renaming]
rename_vert_inv__aux [in renaming]
restriction [in lth_in_proof]
rm [in peo_search]

S

snd_sort [in lth_in_proof]
sv_nghbs [in peo_search]
sv_nghbs_aux [in peo_search]
sv_search [in peo_search]
sv_search_aux [in peo_search]

Library Index

C

chordal_graph_coloring
chordal_graph_optimality
coloration_renaming

G

graph_construction

L

lex_sort
lth_in_proof

M

N

P

Q

R

S

strict_inc_and_dec
strict_ord

Global Index

B

H

J

K

T

U

V

W

X

Y

Z

(471 entries)

Axiom Index

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(2 entries)

Lemma Index

B

H

J

K

T

U

V

W

X

Y

Z

(348 entries)

Constructor Index

A

B

C

D

E

F

G

H

J

K

M

O

Q

R

T

U

V

W

X

Y

Z

_

(27 entries)

Inductive Index

A

B

D

E

F

H

J

K

M

O

P

Q

R

T

U

V

W

X

Y

Z

(15 entries)

Definition Index

B

D

F

H

J

K

Q

T

U

V

W

X

Y

Z

_

(66 entries)

Library Index

A

B

D

E

F

H

I

J

K

O

T

U

V

W

X

Y

Z

_

(13 entries)

This page has been generated by coqdoc