Global Index

H

J

K

Q

U

W

X

_

(565 entries)

Lemma Index

H

J

K

Q

U

W

X

Y

_

other

(403 entries)

Section Index

A

C

D

E

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

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

Constructor Index

A

B

C

D

F

G

H

I

J

K

L

P

Q

R

S

T

U

V

W

X

_

other

(8 entries)

Inductive Index

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

H

J

K

Q

U

W

X

Y

_

other

(98 entries)

Variable Index

A

C

D

E

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

(27 entries)

Library Index

A

C

D

F

G

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

Z

_

other

(11 entries)

Global Index

A

add_to_all_NoDup [lemma, in Optimization]
add_to_all_In [lemma, in Optimization]
add_to_all_standard [lemma, in Optimization]
add_to_all [definition, in Optimization]
all_in_dec [lemma, in Basics]
all_lt_remove [lemma, in Permutations]
all_lt_dec [lemma, in Permutations]
all_lt_In [lemma, in Permutations]
all_lt_char [lemma, in Permutations]
all_lt [definition, in Permutations]
all_co_bin_seqs_lemma [lemma, in BinarySequences]
all_co_bin_seqs [definition, in BinarySequences]
all_bin_seqs_lemma [lemma, in BinarySequences]
all_bin_seqs [definition, in BinarySequences]
all_sorted_dec [lemma, in BinarySequences]
all_ones_dec [lemma, in BinarySequences]
all_ones_zeros [lemma, in BinarySequences]
all_ones_sorted [lemma, in BinarySequences]
all_ones_char [lemma, in BinarySequences]
all_ones [definition, in BinarySequences]
all_st_comps_NoDup [lemma, in SortingNetworks]
all_st_comps_standard [lemma, in SortingNetworks]
all_st_comps_lemma [lemma, in SortingNetworks]
all_st_comps [definition, in SortingNetworks]
Answer [inductive, in Prune]
apply [definition, in SortingNetworks]
apply_perm_inverse [lemma, in Permutations]
apply_perm_equiv [lemma, in Permutations]
apply_perm_get [lemma, in Permutations]
apply_perm_get_lemma [lemma, in Permutations]
apply_perm [definition, in Permutations]
apply_perm_transp_red [lemma, in Standardization]
apply_perm_to_net_inv [lemma, in Standardization]
apply_perm_to_net [definition, in Standardization]
apply_perm_to_comp [definition, in Standardization]
apply_inv [lemma, in SortingNetworks]
apply_zeros_folded [lemma, in SortingNetworks]
apply_zeros [lemma, in SortingNetworks]
apply_id [lemma, in SortingNetworks]
apply_transp_gt [lemma, in SortingNetworks]
apply_transp_le [lemma, in SortingNetworks]

B

Basics [library]
Basic_Properties.HP [variable, in Permutations]
Basic_Properties.P [variable, in Permutations]
Basic_Properties.n [variable, in Permutations]
Basic_Properties [section, in Permutations]
BinarySequences [library]
BinaryTree [inductive, in BinaryTrees]
BinaryTrees [library]
bin_seq_eq_dec [lemma, in BinarySequences]
bin_seq_alt_induction [lemma, in BinarySequences]
bin_seq_alt_char_all [lemma, in BinarySequences]
bin_seq_last_get [lemma, in BinarySequences]
bin_seq_alt_char_1 [lemma, in BinarySequences]
bin_seq_alt_char_0 [lemma, in BinarySequences]
bin_seq_alt_char [lemma, in BinarySequences]
bin_seq_drop [definition, in BinarySequences]
bin_seq_last [definition, in BinarySequences]
bin_seq_1_inv [lemma, in BinarySequences]
bin_seq_0_inv [lemma, in BinarySequences]
bin_seq_inversion_S [lemma, in BinarySequences]
bin_seq_inversion_0 [lemma, in BinarySequences]
bin_seq_induction [lemma, in BinarySequences]
bin_seq_get_str [lemma, in BinarySequences]
bin_seq_get [lemma, in BinarySequences]
bin_seq [inductive, in BinarySequences]
bin_seq_compare [definition, in Subsumption]
BS_compare_sym_Gt [lemma, in Subsumption]
BS_compare_trans [lemma, in Subsumption]
BS_compare_eq [lemma, in Subsumption]
BTree [definition, in Prune]
BT_map_in [lemma, in BinaryTrees]
BT_map [definition, in BinaryTrees]
BT_in_add_all [lemma, in BinaryTrees]
BT_add_all_in [lemma, in BinaryTrees]
BT_add_all_mon [lemma, in BinaryTrees]
BT_add_all [definition, in BinaryTrees]
BT_size_split [lemma, in BinaryTrees]
BT_size [definition, in BinaryTrees]
BT_all_in_dec [lemma, in BinaryTrees]
BT_in_dec [lemma, in BinaryTrees]
BT_split_compare [lemma, in BinaryTrees]
BT_split_in [lemma, in BinaryTrees]
BT_split_in_l [lemma, in BinaryTrees]
BT_split_wf [lemma, in BinaryTrees]
BT_split_in_r [lemma, in BinaryTrees]
BT_split [definition, in BinaryTrees]
BT_add_mon [lemma, in BinaryTrees]
BT_wf_add [lemma, in BinaryTrees]
BT_in_add [lemma, in BinaryTrees]
BT_add_in [lemma, in BinaryTrees]
BT_add [definition, in BinaryTrees]
BT_wf [definition, in BinaryTrees]
BT_In [definition, in BinaryTrees]
BZ [lemma, in Subsumption]

C

change [definition, in Basics]
change_nth_neq [lemma, in Basics]
change_nth_k [lemma, in Basics]
change_In [lemma, in Basics]
change_len [lemma, in Basics]
channels [definition, in SortingNetworks]
channels_standardization [lemma, in Standardization]
channels_cons [lemma, in SortingNetworks]
channels_app [lemma, in SortingNetworks]
CN_eq_dec [lemma, in SortingNetworks]
cod [definition, in Permutations]
comparator [definition, in SortingNetworks]
comparator_network [definition, in SortingNetworks]
complete_size [lemma, in Optimization]
compose [definition, in Permutations]
compose_val [lemma, in Permutations]
comp_standard [definition, in SortingNetworks]
comp_channels [definition, in SortingNetworks]
comp_eq_dec [lemma, in SortingNetworks]
count_NoDup [lemma, in Basics]
count_occ_zero [lemma, in Basics]
count_remove [lemma, in Basics]
count_length [lemma, in Basics]
count_zeros_eq [lemma, in BinarySequences]
count_zeros_remove [lemma, in BinarySequences]
count_zeros [definition, in BinarySequences]
co_one_get [lemma, in BinarySequences]
co_zero_get [lemma, in BinarySequences]
co_one_le [lemma, in BinarySequences]
co_one_sort_out [lemma, in BinarySequences]
co_one_sort_in [lemma, in BinarySequences]
co_one_last [lemma, in BinarySequences]
co_zero_last [lemma, in BinarySequences]
co_one [definition, in BinarySequences]
co_zero [definition, in BinarySequences]

D

direct_subsumption [definition, in Subsumption]
dom [definition, in Permutations]
drop [definition, in BinarySequences]
drop_1 [lemma, in BinarySequences]
drop_0 [lemma, in BinarySequences]
drop_lemma [lemma, in BinarySequences]
drop_get [lemma, in BinarySequences]
dummy_standard [lemma, in Prune]
dummy_length [lemma, in Prune]
dummy_net [definition, in Prune]

E

empty [constructor, in BinarySequences]
empty_complete [lemma, in Optimization]
equivalent_perm_trans [lemma, in Permutations]
equivalent_perm_sym [lemma, in Permutations]
equivalent_perm_refl [lemma, in Permutations]
equivalent_perm [definition, in Permutations]
eq_BS_compare [lemma, in Subsumption]
eq_OCN_compare [lemma, in Optimization]
exists_SN_dec_str [lemma, in Prune]
exists_SN_dec [lemma, in SortingNetworks]
Extraction [library]
ext_map [lemma, in Basics]

F

filtered_NoDup [lemma, in Optimization]
filtered_in_src [lemma, in Optimization]
filtered_in_str [lemma, in Optimization]
filtered_in [lemma, in Optimization]
filter_non_redundant [definition, in Optimization]
FindAndRemove [section, in Basics]
FindAndRemove.A [variable, in Basics]
FindAndRemove.A_dec [variable, in Basics]
find_and_remove_smaller [lemma, in Basics]
find_and_remove_le [lemma, in Basics]
find_and_remove_3c [lemma, in Basics]
find_and_remove_not_in [lemma, in Basics]
find_and_remove_3b [lemma, in Basics]
find_and_remove_3a [lemma, in Basics]
find_and_remove_2a [lemma, in Basics]
find_and_remove_2 [lemma, in Basics]
find_and_remove_2_true [lemma, in Basics]
find_and_remove_1a [lemma, in Basics]
find_and_remove_1 [lemma, in Basics]
find_and_remove_1_true [lemma, in Basics]
find_and_remove_true_true [lemma, in Basics]
find_and_remove [definition, in Basics]
full_apply_permute [lemma, in Standardization]
full_apply_permutation [lemma, in Standardization]
full_apply_app [lemma, in SortingNetworks]
full_apply_zeros [lemma, in SortingNetworks]
full_apply [definition, in SortingNetworks]

G

Generate [definition, in Optimization]
Generate_complete [lemma, in Optimization]
Generate_NoDup [lemma, in Optimization]
Generate_in [lemma, in Optimization]
Generate_extend [lemma, in Optimization]
Generate_standard [lemma, in Optimization]
Generate_OK [lemma, in Optimization]
Generate_channels [lemma, in Optimization]
Generate_length [lemma, in Optimization]
Generate_it_standard [lemma, in Prune]
Generate_it_length [lemma, in Prune]
Generate_has_all [lemma, in Prune]
Generate_it [definition, in Prune]
Generate_and_Prune [definition, in Prune]
get [definition, in BinarySequences]
get_perm_set [lemma, in Permutations]
get_perm_set_lemma [lemma, in Permutations]
get_set_2 [lemma, in BinarySequences]
get_set_1 [lemma, in BinarySequences]
get_lt_neq [lemma, in BinarySequences]
get_is_lt_1 [lemma, in BinarySequences]
get_is_lt_0 [lemma, in BinarySequences]
get_lt [lemma, in BinarySequences]
get_le [lemma, in BinarySequences]
get_in_dec [lemma, in BinarySequences]
get_in [lemma, in BinarySequences]
GP_yes [lemma, in Prune]
GP_yes_str [lemma, in Prune]
GP_has_SN [lemma, in Prune]
GP_no [lemma, in Prune]
GP_complete [lemma, in Prune]
GP_no_SN [lemma, in Prune]
GP_non_red [lemma, in Prune]
GP_channels [lemma, in Prune]
GP_channels_1 [lemma, in Prune]
GP_channels_0 [lemma, in Prune]
GP_yes_le [lemma, in Prune]
GP_no_OK_2 [lemma, in Prune]
GP_no_OK_1 [lemma, in Prune]
GP_yes_weak [lemma, in Prune]
GP_yes_OK [lemma, in Prune]
GP_yes_no_OK [lemma, in Prune]
GP_SC [lemma, in Prune]
GP_it_2 [lemma, in Prune]
GP_it_1 [lemma, in Prune]
GP_it_0 [lemma, in Prune]
GP_start_2 [lemma, in Prune]
GP_start_1 [lemma, in Prune]
GP_start_0 [lemma, in Prune]
gt_neq [lemma, in Basics]

I

id_perm_apply [lemma, in Permutations]
id_perm_get [lemma, in Permutations]
id_perm_val [lemma, in Permutations]
id_perm [lemma, in Permutations]
id_permutation [definition, in Permutations]
inverse_perm_bin_seq [lemma, in Permutations]
inverse_perm_val_3 [lemma, in Permutations]
inverse_perm_val_2 [lemma, in Permutations]
inverse_perm_val_1 [lemma, in Permutations]
inverse_inverse_perm [lemma, in Permutations]
inverse_perm_In [lemma, in Permutations]
inverse_perm_perm [lemma, in Permutations]
inverse_perm_cod [lemma, in Permutations]
inverse_perm_dom [lemma, in Permutations]
inverse_perm [definition, in Permutations]
In_split [lemma, in Basics]
in_remove [lemma, in Basics]
In_suff [lemma, in Basics]
In_char [lemma, in Basics]
in_BTree_list [lemma, in BinaryTrees]
in_list_BTree [lemma, in BinaryTrees]
in_Generate [lemma, in Optimization]
is_nil_dec [lemma, in Basics]

L

last_redundant_dec [lemma, in Redundancy]
last_redundant [definition, in Redundancy]
length_nth_ok [lemma, in Basics]
list_eq [lemma, in Basics]
list_length_induction [lemma, in Basics]
list_to_BTree_wf [lemma, in BinaryTrees]
list_to_BTree [definition, in BinaryTrees]
lt_neq [lemma, in Basics]

M

make [definition, in SortingNetworks]
make_permutation_cod [lemma, in Prune]
make_permutation_dom [lemma, in Prune]
make_permutation [definition, in Prune]
make_permutation_rec [definition, in Prune]
map_in [lemma, in Basics]
map_ext_str [lemma, in Redundancy]
maybe [constructor, in Prune]
minimal_SN [lemma, in Prune]
minus_S [lemma, in Basics]

N

nat_compare_trans [lemma, in Basics]
nat_compare_sym_gt [lemma, in Basics]
nat_compare_sym_lt [lemma, in Basics]
nat_compare_eq_rev [lemma, in Basics]
nat_to_comp_inv [lemma, in Optimization]
nat_to_comp_ok [lemma, in Optimization]
nat_to_comp [definition, in Optimization]
nat_to_comp_inj [lemma, in Prune]
Nil [definition, in Prune]
nil_length [lemma, in Basics]
nil_not_SN [lemma, in Prune]
no [constructor, in Prune]
node [constructor, in BinaryTrees]
NoDup_app [lemma, in Basics]
NoDup_lemma [lemma, in Basics]
NoDup_count_occ [lemma, in Basics]
NoDup_count_length_lt [lemma, in Basics]
NoDup_count_length_le [lemma, in Basics]
NoDup_count [lemma, in Basics]
NoDup_char_3 [lemma, in Basics]
NoDup_char_2 [lemma, in Basics]
NoDup_char_1 [lemma, in Basics]
NoDup_append [lemma, in Basics]
NoDup_remove [lemma, in Basics]
NoDup_dec [lemma, in Basics]
NoDup_val [lemma, in Permutations]
NoDup_val_lemma [lemma, in Permutations]
NoDup_count_zeros [lemma, in BinarySequences]
NoDup_count_zeros_set [lemma, in BinarySequences]
NoDup_all_lt_lt [lemma, in SortingNetworks]
NoDup_all_lt_prop [lemma, in SortingNetworks]
NoDup_all_lt_count [lemma, in SortingNetworks]
nought [constructor, in BinaryTrees]
nth_In_Prop [lemma, in Basics]
nth_ok_length [lemma, in Basics]

O

OCN [definition, in Optimization]
OCN_compare_trans [lemma, in Optimization]
OCN_compare_sym_Gt [lemma, in Optimization]
OCN_compare_sym_Lt [lemma, in Optimization]
OCN_compare_eq [lemma, in Optimization]
OCN_compare [definition, in Optimization]
OCN_standard [lemma, in Optimization]
OCN_ok [definition, in Optimization]
OCN_to_CN [definition, in Optimization]
OCN_standard_ok [lemma, in Prune]
OCN_to_CN_inj [lemma, in Prune]
OCN_to_CN_inv [lemma, in Prune]
OCN_eq_dec [definition, in Prune]
OGenerate [definition, in Optimization]
OGenerate_complete [lemma, in Optimization]
one [constructor, in BinarySequences]
ones [definition, in BinarySequences]
ones_le [lemma, in BinarySequences]
Optimization [library]
opt_outputs [definition, in Subsumption]
Oracle [definition, in Prune]
oracle_test_in [lemma, in Prune]
oracle_test_in_lemma [lemma, in Prune]
oracle_test [definition, in Prune]
oracle_filter_wf [lemma, in Prune]
oracle_filter_in [lemma, in Prune]
oracle_subs [lemma, in Prune]
oracle_perm [lemma, in Prune]
oracle_ok [definition, in Prune]
outputs [definition, in SortingNetworks]
outputs_app [lemma, in SortingNetworks]
outputs_redundant [lemma, in Redundancy]

P

Parberry [lemma, in Subsumption]
permut [definition, in Permutations]
permutation [definition, in Permutations]
Permutations [library]
Permutation_NoDup [lemma, in Basics]
permutation_eq [lemma, in Permutations]
permutation_In_cod_dom [lemma, in Permutations]
permutation_In_dom_cod [lemma, in Permutations]
permutation_Permutation [lemma, in Permutations]
permutation_NoDup_cod [lemma, in Permutations]
permutation_NoDup_dom [lemma, in Permutations]
permutation_in_cod [lemma, in Permutations]
permutation_in_dom [lemma, in Permutations]
permutation_all_lt_cod [lemma, in Permutations]
permutation_all_lt_dom [lemma, in Permutations]
permutation_Prop_cod [lemma, in Permutations]
permutation_channels [lemma, in Standardization]
permutation_length [lemma, in Standardization]
permute [definition, in Standardization]
permute_char [lemma, in Standardization]
permute_app [lemma, in Standardization]
permute_channels [lemma, in Standardization]
permute_length [lemma, in Standardization]
plus_minus_S_S [lemma, in Basics]
pre_permutation_lemma [lemma, in Prune]
pre_permutation_In [lemma, in Prune]
pre_permutation_dec [lemma, in Prune]
pre_permutation [definition, in Prune]
Pre_permutations.l [variable, in Prune]
Pre_permutations.n [variable, in Prune]
Pre_permutations [section, in Prune]
Prune [definition, in Prune]
Prune [section, in Prune]
Prune [library]
Prune_SN [lemma, in Prune]
Prune_complete [lemma, in Prune]
Prune_NoDup [lemma, in Prune]
Prune_standard [lemma, in Prune]
Prune_in [lemma, in Prune]
Prune_nil [lemma, in Prune]

R

Redundancy [library]
redundant [definition, in Redundancy]
redundant_dec [lemma, in Redundancy]
redundant_red_wrt [lemma, in Redundancy]
redundant_outputs [lemma, in Redundancy]
red_wrt_dec [lemma, in Redundancy]
red_wrt_redundant [lemma, in Redundancy]
red_wrt [definition, in Redundancy]
Remove [section, in Basics]
RemoveAll [section, in Basics]
RemoveAll.A [variable, in Basics]
RemoveAll.A_dec [variable, in Basics]
remove_all_not_in [lemma, in Basics]
remove_all_NoDup [lemma, in Basics]
remove_all_nil [lemma, in Basics]
remove_all_in [lemma, in Basics]
remove_all_length_lt [lemma, in Basics]
remove_all_length_le [lemma, in Basics]
remove_all [definition, in Basics]
remove_fst_length_In [lemma, in Basics]
remove_fst_not_In [lemma, in Basics]
remove_fst_NoDup [lemma, in Basics]
remove_fst [definition, in Basics]
remove_count_length [lemma, in Basics]
remove_length_In [lemma, in Basics]
remove_length [lemma, in Basics]
remove_In_neq [lemma, in Basics]
remove_out [lemma, in Basics]
remove_not_in [lemma, in Basics]
remove_app [lemma, in Basics]
remove_red [definition, in Redundancy]
Remove.A [variable, in Basics]
Remove.A_dec [variable, in Basics]
rem_red_app [lemma, in Redundancy]
rem_red_SN [lemma, in Redundancy]
rem_red_outputs [lemma, in Redundancy]
rem_red_apply [lemma, in Redundancy]
rem_red_fixpoint [lemma, in Redundancy]
rem_red_not_redundant [lemma, in Redundancy]
rem_red_length [lemma, in Redundancy]
rem_red_standard [lemma, in Redundancy]
rem_red_channels [lemma, in Redundancy]
rem_red [definition, in Redundancy]
run_3rd [lemma, in Prune]
run_lemma [lemma, in Prune]
run_oracle [definition, in Prune]

S

set [definition, in BinarySequences]
set_set_del [lemma, in BinarySequences]
set_set_comm [lemma, in BinarySequences]
set_get_strong [lemma, in BinarySequences]
set_get [lemma, in BinarySequences]
sign [definition, in Basics]
sign_lt [lemma, in Basics]
sign_mon [lemma, in Basics]
sign_get [lemma, in BinarySequences]
size_complete [definition, in Optimization]
SN_size_dec [lemma, in Prune]
SN_1 [lemma, in Prune]
SN_0 [lemma, in Prune]
SN_dec [lemma, in SortingNetworks]
SN_extend [lemma, in SortingNetworks]
SN_sort [lemma, in SortingNetworks]
SN_idemp [lemma, in SortingNetworks]
SN_compute [lemma, in SortingNetworks]
SN_char [lemma, in SortingNetworks]
SN_redundant [lemma, in Redundancy]
SN2 [definition, in SortingNetworks]
SN2_SN [lemma, in SortingNetworks]
SN3 [definition, in SortingNetworks]
SN3_SN [lemma, in SortingNetworks]
SN4 [definition, in SortingNetworks]
SN4_SN [lemma, in SortingNetworks]
SN5 [definition, in SortingNetworks]
SN9 [definition, in SortingNetworks]
sort [definition, in BinarySequences]
sorted [definition, in BinarySequences]
sorted_idemp [lemma, in BinarySequences]
sorted_sort [lemma, in BinarySequences]
sorted_dec [lemma, in BinarySequences]
sorted_lem [lemma, in BinarySequences]
sorted_char [lemma, in BinarySequences]
SortingNetworks [library]
sorting_char [lemma, in BinarySequences]
sorting_char_lemma [lemma, in BinarySequences]
sorting_network [definition, in SortingNetworks]
sort_zeros [lemma, in BinarySequences]
split [definition, in Basics]
Split [section, in Basics]
split_length_2 [lemma, in Basics]
split_length_1 [lemma, in Basics]
split_char_out [lemma, in Basics]
split_char_in [lemma, in Basics]
Split.A [variable, in Basics]
Split.A_dec [variable, in Basics]
standard [definition, in SortingNetworks]
standardization [lemma, in Standardization]
Standardization [library]
standardization_sort [lemma, in Standardization]
standardization_sort_lemma [lemma, in Standardization]
standardization_char [lemma, in Standardization]
standardization_length [lemma, in Standardization]
standardization_channels [lemma, in Standardization]
standardize_app [lemma, in Standardization]
standardize_idemp [lemma, in Standardization]
standardize_gt [lemma, in Standardization]
standardize_gt_lemma [lemma, in Standardization]
standardize_le [lemma, in Standardization]
standardize_le_lemma [lemma, in Standardization]
standard_network_idemp [lemma, in SortingNetworks]
standard_app [lemma, in SortingNetworks]
standard_channels [lemma, in SortingNetworks]
subsumption [definition, in Subsumption]
Subsumption [library]
subsumption_dec [lemma, in Subsumption]
subsumption_opt_dec [lemma, in Subsumption]
subsumption_to_opt [lemma, in Subsumption]
subsumption_opt_to [lemma, in Subsumption]
subsumption_opt [definition, in Subsumption]
subsumption_dec_1 [lemma, in Subsumption]

T

till_n'_NoDup [lemma, in Optimization]
till_n'_char [lemma, in Optimization]
till_n'_length [lemma, in Optimization]
till_n'_lt [lemma, in Optimization]
till_n'_lemma [lemma, in Optimization]
till_n' [definition, in Optimization]
till_n_NoDup [lemma, in SortingNetworks]
till_n_char [lemma, in SortingNetworks]
till_n_length [lemma, in SortingNetworks]
till_n_lt [lemma, in SortingNetworks]
till_n_lemma [lemma, in SortingNetworks]
till_n [definition, in SortingNetworks]
transposition [definition, in Permutations]
Transpositions [section, in Permutations]
Transpositions.Hij [variable, in Permutations]
Transpositions.i [variable, in Permutations]
Transpositions.j [variable, in Permutations]
Transpositions.T [variable, in Permutations]
transp_sym_apply [lemma, in Permutations]
transp_sym [lemma, in Permutations]
transp_inverse_equiv [lemma, in Permutations]
transp_idemp [lemma, in Permutations]
transp_get_neq [lemma, in Permutations]
transp_get_j [lemma, in Permutations]
transp_get_i [lemma, in Permutations]
transp_val_neq [lemma, in Permutations]
transp_val_j [lemma, in Permutations]
transp_val_i [lemma, in Permutations]
transp_perm [lemma, in Permutations]
Trees [section, in BinaryTrees]
Trees.BT_Wf [variable, in BinaryTrees]
Trees.BT_Add [variable, in BinaryTrees]
Trees.eq_T_compare [variable, in BinaryTrees]
Trees.Map [section, in BinaryTrees]
Trees.Map.f [variable, in BinaryTrees]
Trees.T [variable, in BinaryTrees]
Trees.T_dec [variable, in BinaryTrees]
Trees.T_compare_sym_Gt [variable, in BinaryTrees]
Trees.T_compare_trans [variable, in BinaryTrees]
Trees.T_compare_eq [variable, in BinaryTrees]
Trees.T_compare [variable, in BinaryTrees]

V

val [definition, in Permutations]
val_neq [lemma, in Permutations]
val_eq [lemma, in Permutations]
val_in_snd [lemma, in Permutations]
val_not_in [lemma, in Permutations]
val_lt [lemma, in Permutations]
val_lt_lemma [lemma, in Permutations]

Y

yes [constructor, in Prune]

Z

zero [constructor, in BinarySequences]
zeros [definition, in BinarySequences]
zeros_apply_perm [lemma, in Permutations]
zeros_apply_perm_count [lemma, in Permutations]
zeros_co_one [lemma, in BinarySequences]
zeros_all_ones [lemma, in BinarySequences]
zeros_gt [lemma, in BinarySequences]
zeros_set_plus [lemma, in BinarySequences]
zeros_set_minus [lemma, in BinarySequences]
zeros_set_eq_1 [lemma, in BinarySequences]
zeros_set_eq_0 [lemma, in BinarySequences]
zeros_le [lemma, in BinarySequences]
zero_count [lemma, in Basics]
zero_seq_zeros [lemma, in BinarySequences]
zero_seq [definition, in BinarySequences]

other

_ [<] _ [notation, in SortingNetworks]
[00] [notation, in BinarySequences]
[0] _ [notation, in BinarySequences]
[1] _ [notation, in BinarySequences]
[] [notation, in BinarySequences]

Lemma Index

A

add_to_all_NoDup [in Optimization]
add_to_all_In [in Optimization]
add_to_all_standard [in Optimization]
all_in_dec [in Basics]
all_lt_remove [in Permutations]
all_lt_dec [in Permutations]
all_lt_In [in Permutations]
all_lt_char [in Permutations]
all_co_bin_seqs_lemma [in BinarySequences]
all_bin_seqs_lemma [in BinarySequences]
all_sorted_dec [in BinarySequences]
all_ones_dec [in BinarySequences]
all_ones_zeros [in BinarySequences]
all_ones_sorted [in BinarySequences]
all_ones_char [in BinarySequences]
all_st_comps_NoDup [in SortingNetworks]
all_st_comps_standard [in SortingNetworks]
all_st_comps_lemma [in SortingNetworks]
apply_perm_inverse [in Permutations]
apply_perm_equiv [in Permutations]
apply_perm_get [in Permutations]
apply_perm_get_lemma [in Permutations]
apply_perm_transp_red [in Standardization]
apply_perm_to_net_inv [in Standardization]
apply_inv [in SortingNetworks]
apply_zeros_folded [in SortingNetworks]
apply_zeros [in SortingNetworks]
apply_id [in SortingNetworks]
apply_transp_gt [in SortingNetworks]
apply_transp_le [in SortingNetworks]

B

bin_seq_eq_dec [in BinarySequences]
bin_seq_alt_induction [in BinarySequences]
bin_seq_alt_char_all [in BinarySequences]
bin_seq_last_get [in BinarySequences]
bin_seq_alt_char_1 [in BinarySequences]
bin_seq_alt_char_0 [in BinarySequences]
bin_seq_alt_char [in BinarySequences]
bin_seq_1_inv [in BinarySequences]
bin_seq_0_inv [in BinarySequences]
bin_seq_inversion_S [in BinarySequences]
bin_seq_inversion_0 [in BinarySequences]
bin_seq_induction [in BinarySequences]
bin_seq_get_str [in BinarySequences]
bin_seq_get [in BinarySequences]
BS_compare_sym_Gt [in Subsumption]
BS_compare_trans [in Subsumption]
BS_compare_eq [in Subsumption]
BT_map_in [in BinaryTrees]
BT_in_add_all [in BinaryTrees]
BT_add_all_in [in BinaryTrees]
BT_add_all_mon [in BinaryTrees]
BT_size_split [in BinaryTrees]
BT_all_in_dec [in BinaryTrees]
BT_in_dec [in BinaryTrees]
BT_split_compare [in BinaryTrees]
BT_split_in [in BinaryTrees]
BT_split_in_l [in BinaryTrees]
BT_split_wf [in BinaryTrees]
BT_split_in_r [in BinaryTrees]
BT_add_mon [in BinaryTrees]
BT_wf_add [in BinaryTrees]
BT_in_add [in BinaryTrees]
BT_add_in [in BinaryTrees]
BZ [in Subsumption]

C

change_nth_neq [in Basics]
change_nth_k [in Basics]
change_In [in Basics]
change_len [in Basics]
channels_standardization [in Standardization]
channels_cons [in SortingNetworks]
channels_app [in SortingNetworks]
CN_eq_dec [in SortingNetworks]
complete_size [in Optimization]
compose_val [in Permutations]
comp_eq_dec [in SortingNetworks]
count_NoDup [in Basics]
count_occ_zero [in Basics]
count_remove [in Basics]
count_length [in Basics]
count_zeros_eq [in BinarySequences]
count_zeros_remove [in BinarySequences]
co_one_get [in BinarySequences]
co_zero_get [in BinarySequences]
co_one_le [in BinarySequences]
co_one_sort_out [in BinarySequences]
co_one_sort_in [in BinarySequences]
co_one_last [in BinarySequences]
co_zero_last [in BinarySequences]

D

drop_1 [in BinarySequences]
drop_0 [in BinarySequences]
drop_lemma [in BinarySequences]
drop_get [in BinarySequences]
dummy_standard [in Prune]
dummy_length [in Prune]

E

empty_complete [in Optimization]
equivalent_perm_trans [in Permutations]
equivalent_perm_sym [in Permutations]
equivalent_perm_refl [in Permutations]
eq_BS_compare [in Subsumption]
eq_OCN_compare [in Optimization]
exists_SN_dec_str [in Prune]
exists_SN_dec [in SortingNetworks]
ext_map [in Basics]

F

filtered_NoDup [in Optimization]
filtered_in_src [in Optimization]
filtered_in_str [in Optimization]
filtered_in [in Optimization]
find_and_remove_smaller [in Basics]
find_and_remove_le [in Basics]
find_and_remove_3c [in Basics]
find_and_remove_not_in [in Basics]
find_and_remove_3b [in Basics]
find_and_remove_3a [in Basics]
find_and_remove_2a [in Basics]
find_and_remove_2 [in Basics]
find_and_remove_2_true [in Basics]
find_and_remove_1a [in Basics]
find_and_remove_1 [in Basics]
find_and_remove_1_true [in Basics]
find_and_remove_true_true [in Basics]
full_apply_permute [in Standardization]
full_apply_permutation [in Standardization]
full_apply_app [in SortingNetworks]
full_apply_zeros [in SortingNetworks]

G

Generate_complete [in Optimization]
Generate_NoDup [in Optimization]
Generate_in [in Optimization]
Generate_extend [in Optimization]
Generate_standard [in Optimization]
Generate_OK [in Optimization]
Generate_channels [in Optimization]
Generate_length [in Optimization]
Generate_it_standard [in Prune]
Generate_it_length [in Prune]
Generate_has_all [in Prune]
get_perm_set [in Permutations]
get_perm_set_lemma [in Permutations]
get_set_2 [in BinarySequences]
get_set_1 [in BinarySequences]
get_lt_neq [in BinarySequences]
get_is_lt_1 [in BinarySequences]
get_is_lt_0 [in BinarySequences]
get_lt [in BinarySequences]
get_le [in BinarySequences]
get_in_dec [in BinarySequences]
get_in [in BinarySequences]
GP_yes [in Prune]
GP_yes_str [in Prune]
GP_has_SN [in Prune]
GP_no [in Prune]
GP_complete [in Prune]
GP_no_SN [in Prune]
GP_non_red [in Prune]
GP_channels [in Prune]
GP_channels_1 [in Prune]
GP_channels_0 [in Prune]
GP_yes_le [in Prune]
GP_no_OK_2 [in Prune]
GP_no_OK_1 [in Prune]
GP_yes_weak [in Prune]
GP_yes_OK [in Prune]
GP_yes_no_OK [in Prune]
GP_SC [in Prune]
GP_it_2 [in Prune]
GP_it_1 [in Prune]
GP_it_0 [in Prune]
GP_start_2 [in Prune]
GP_start_1 [in Prune]
GP_start_0 [in Prune]
gt_neq [in Basics]

I

id_perm_apply [in Permutations]
id_perm_get [in Permutations]
id_perm_val [in Permutations]
id_perm [in Permutations]
inverse_perm_bin_seq [in Permutations]
inverse_perm_val_3 [in Permutations]
inverse_perm_val_2 [in Permutations]
inverse_perm_val_1 [in Permutations]
inverse_inverse_perm [in Permutations]
inverse_perm_In [in Permutations]
inverse_perm_perm [in Permutations]
inverse_perm_cod [in Permutations]
inverse_perm_dom [in Permutations]
In_split [in Basics]
in_remove [in Basics]
In_suff [in Basics]
In_char [in Basics]
in_BTree_list [in BinaryTrees]
in_list_BTree [in BinaryTrees]
in_Generate [in Optimization]
is_nil_dec [in Basics]

L

last_redundant_dec [in Redundancy]
length_nth_ok [in Basics]
list_eq [in Basics]
list_length_induction [in Basics]
list_to_BTree_wf [in BinaryTrees]
lt_neq [in Basics]

M

make_permutation_cod [in Prune]
make_permutation_dom [in Prune]
map_in [in Basics]
map_ext_str [in Redundancy]
minimal_SN [in Prune]
minus_S [in Basics]

N

nat_compare_trans [in Basics]
nat_compare_sym_gt [in Basics]
nat_compare_sym_lt [in Basics]
nat_compare_eq_rev [in Basics]
nat_to_comp_inv [in Optimization]
nat_to_comp_ok [in Optimization]
nat_to_comp_inj [in Prune]
nil_length [in Basics]
nil_not_SN [in Prune]
NoDup_app [in Basics]
NoDup_lemma [in Basics]
NoDup_count_occ [in Basics]
NoDup_count_length_lt [in Basics]
NoDup_count_length_le [in Basics]
NoDup_count [in Basics]
NoDup_char_3 [in Basics]
NoDup_char_2 [in Basics]
NoDup_char_1 [in Basics]
NoDup_append [in Basics]
NoDup_remove [in Basics]
NoDup_dec [in Basics]
NoDup_val [in Permutations]
NoDup_val_lemma [in Permutations]
NoDup_count_zeros [in BinarySequences]
NoDup_count_zeros_set [in BinarySequences]
NoDup_all_lt_lt [in SortingNetworks]
NoDup_all_lt_prop [in SortingNetworks]
NoDup_all_lt_count [in SortingNetworks]
nth_In_Prop [in Basics]
nth_ok_length [in Basics]

O

OCN_compare_trans [in Optimization]
OCN_compare_sym_Gt [in Optimization]
OCN_compare_sym_Lt [in Optimization]
OCN_compare_eq [in Optimization]
OCN_standard [in Optimization]
OCN_standard_ok [in Prune]
OCN_to_CN_inj [in Prune]
OCN_to_CN_inv [in Prune]
OGenerate_complete [in Optimization]
ones_le [in BinarySequences]
oracle_test_in [in Prune]
oracle_test_in_lemma [in Prune]
oracle_filter_wf [in Prune]
oracle_filter_in [in Prune]
oracle_subs [in Prune]
oracle_perm [in Prune]
outputs_app [in SortingNetworks]
outputs_redundant [in Redundancy]

P

Parberry [in Subsumption]
Permutation_NoDup [in Basics]
permutation_eq [in Permutations]
permutation_In_cod_dom [in Permutations]
permutation_In_dom_cod [in Permutations]
permutation_Permutation [in Permutations]
permutation_NoDup_cod [in Permutations]
permutation_NoDup_dom [in Permutations]
permutation_in_cod [in Permutations]
permutation_in_dom [in Permutations]
permutation_all_lt_cod [in Permutations]
permutation_all_lt_dom [in Permutations]
permutation_Prop_cod [in Permutations]
permutation_channels [in Standardization]
permutation_length [in Standardization]
permute_char [in Standardization]
permute_app [in Standardization]
permute_channels [in Standardization]
permute_length [in Standardization]
plus_minus_S_S [in Basics]
pre_permutation_lemma [in Prune]
pre_permutation_In [in Prune]
pre_permutation_dec [in Prune]
Prune_SN [in Prune]
Prune_complete [in Prune]
Prune_NoDup [in Prune]
Prune_standard [in Prune]
Prune_in [in Prune]
Prune_nil [in Prune]

R

redundant_dec [in Redundancy]
redundant_red_wrt [in Redundancy]
redundant_outputs [in Redundancy]
red_wrt_dec [in Redundancy]
red_wrt_redundant [in Redundancy]
remove_all_not_in [in Basics]
remove_all_NoDup [in Basics]
remove_all_nil [in Basics]
remove_all_in [in Basics]
remove_all_length_lt [in Basics]
remove_all_length_le [in Basics]
remove_fst_length_In [in Basics]
remove_fst_not_In [in Basics]
remove_fst_NoDup [in Basics]
remove_count_length [in Basics]
remove_length_In [in Basics]
remove_length [in Basics]
remove_In_neq [in Basics]
remove_out [in Basics]
remove_not_in [in Basics]
remove_app [in Basics]
rem_red_app [in Redundancy]
rem_red_SN [in Redundancy]
rem_red_outputs [in Redundancy]
rem_red_apply [in Redundancy]
rem_red_fixpoint [in Redundancy]
rem_red_not_redundant [in Redundancy]
rem_red_length [in Redundancy]
rem_red_standard [in Redundancy]
rem_red_channels [in Redundancy]
run_3rd [in Prune]
run_lemma [in Prune]

S

set_set_del [in BinarySequences]
set_set_comm [in BinarySequences]
set_get_strong [in BinarySequences]
set_get [in BinarySequences]
sign_lt [in Basics]
sign_mon [in Basics]
sign_get [in BinarySequences]
SN_size_dec [in Prune]
SN_1 [in Prune]
SN_0 [in Prune]
SN_dec [in SortingNetworks]
SN_extend [in SortingNetworks]
SN_sort [in SortingNetworks]
SN_idemp [in SortingNetworks]
SN_compute [in SortingNetworks]
SN_char [in SortingNetworks]
SN_redundant [in Redundancy]
SN2_SN [in SortingNetworks]
SN3_SN [in SortingNetworks]
SN4_SN [in SortingNetworks]
sorted_idemp [in BinarySequences]
sorted_sort [in BinarySequences]
sorted_dec [in BinarySequences]
sorted_lem [in BinarySequences]
sorted_char [in BinarySequences]
sorting_char [in BinarySequences]
sorting_char_lemma [in BinarySequences]
sort_zeros [in BinarySequences]
split_length_2 [in Basics]
split_length_1 [in Basics]
split_char_out [in Basics]
split_char_in [in Basics]
standardization [in Standardization]
standardization_sort [in Standardization]
standardization_sort_lemma [in Standardization]
standardization_char [in Standardization]
standardization_length [in Standardization]
standardization_channels [in Standardization]
standardize_app [in Standardization]
standardize_idemp [in Standardization]
standardize_gt [in Standardization]
standardize_gt_lemma [in Standardization]
standardize_le [in Standardization]
standardize_le_lemma [in Standardization]
standard_network_idemp [in SortingNetworks]
standard_app [in SortingNetworks]
standard_channels [in SortingNetworks]
subsumption_dec [in Subsumption]
subsumption_opt_dec [in Subsumption]
subsumption_to_opt [in Subsumption]
subsumption_opt_to [in Subsumption]
subsumption_dec_1 [in Subsumption]

T

till_n'_NoDup [in Optimization]
till_n'_char [in Optimization]
till_n'_length [in Optimization]
till_n'_lt [in Optimization]
till_n'_lemma [in Optimization]
till_n_NoDup [in SortingNetworks]
till_n_char [in SortingNetworks]
till_n_length [in SortingNetworks]
till_n_lt [in SortingNetworks]
till_n_lemma [in SortingNetworks]
transp_sym_apply [in Permutations]
transp_sym [in Permutations]
transp_inverse_equiv [in Permutations]
transp_idemp [in Permutations]
transp_get_neq [in Permutations]
transp_get_j [in Permutations]
transp_get_i [in Permutations]
transp_val_neq [in Permutations]
transp_val_j [in Permutations]
transp_val_i [in Permutations]
transp_perm [in Permutations]

V

val_neq [in Permutations]
val_eq [in Permutations]
val_in_snd [in Permutations]
val_not_in [in Permutations]
val_lt [in Permutations]
val_lt_lemma [in Permutations]

Z

zeros_apply_perm [in Permutations]
zeros_apply_perm_count [in Permutations]
zeros_co_one [in BinarySequences]
zeros_all_ones [in BinarySequences]
zeros_gt [in BinarySequences]
zeros_set_plus [in BinarySequences]
zeros_set_minus [in BinarySequences]
zeros_set_eq_1 [in BinarySequences]
zeros_set_eq_0 [in BinarySequences]
zeros_le [in BinarySequences]
zero_count [in Basics]
zero_seq_zeros [in BinarySequences]

Section Index

B

Basic_Properties [in Permutations]

F

FindAndRemove [in Basics]

P

Pre_permutations [in Prune]
Prune [in Prune]

R

Remove [in Basics]
RemoveAll [in Basics]

S

Split [in Basics]

T

Transpositions [in Permutations]
Trees [in BinaryTrees]
Trees.Map [in BinaryTrees]

Notation Index

other

_ [<] _ [in SortingNetworks]
[00] [in BinarySequences]
[0] _ [in BinarySequences]
[1] _ [in BinarySequences]
[] [in BinarySequences]

Constructor Index

E

empty [in BinarySequences]

M

maybe [in Prune]

N

no [in Prune]
node [in BinaryTrees]
nought [in BinaryTrees]

O

one [in BinarySequences]

Y

yes [in Prune]

Z

zero [in BinarySequences]

Inductive Index

A

Answer [in Prune]

B

BinaryTree [in BinaryTrees]
bin_seq [in BinarySequences]

Definition Index

A

add_to_all [in Optimization]
all_lt [in Permutations]
all_co_bin_seqs [in BinarySequences]
all_bin_seqs [in BinarySequences]
all_ones [in BinarySequences]
all_st_comps [in SortingNetworks]
apply [in SortingNetworks]
apply_perm [in Permutations]
apply_perm_to_net [in Standardization]
apply_perm_to_comp [in Standardization]

B

bin_seq_drop [in BinarySequences]
bin_seq_last [in BinarySequences]
bin_seq_compare [in Subsumption]
BTree [in Prune]
BT_map [in BinaryTrees]
BT_add_all [in BinaryTrees]
BT_size [in BinaryTrees]
BT_split [in BinaryTrees]
BT_add [in BinaryTrees]
BT_wf [in BinaryTrees]
BT_In [in BinaryTrees]

C

change [in Basics]
channels [in SortingNetworks]
cod [in Permutations]
comparator [in SortingNetworks]
comparator_network [in SortingNetworks]
compose [in Permutations]
comp_standard [in SortingNetworks]
comp_channels [in SortingNetworks]
count_zeros [in BinarySequences]
co_one [in BinarySequences]
co_zero [in BinarySequences]

D

direct_subsumption [in Subsumption]
dom [in Permutations]
drop [in BinarySequences]
dummy_net [in Prune]

E

equivalent_perm [in Permutations]

F

filter_non_redundant [in Optimization]
find_and_remove [in Basics]
full_apply [in SortingNetworks]

G

Generate [in Optimization]
Generate_it [in Prune]
Generate_and_Prune [in Prune]
get [in BinarySequences]

I

id_permutation [in Permutations]
inverse_perm [in Permutations]

L

last_redundant [in Redundancy]
list_to_BTree [in BinaryTrees]

M

make [in SortingNetworks]
make_permutation [in Prune]
make_permutation_rec [in Prune]

N

nat_to_comp [in Optimization]
Nil [in Prune]

O

OCN [in Optimization]
OCN_compare [in Optimization]
OCN_ok [in Optimization]
OCN_to_CN [in Optimization]
OCN_eq_dec [in Prune]
OGenerate [in Optimization]
ones [in BinarySequences]
opt_outputs [in Subsumption]
Oracle [in Prune]
oracle_test [in Prune]
oracle_ok [in Prune]
outputs [in SortingNetworks]

P

permut [in Permutations]
permutation [in Permutations]
permute [in Standardization]
pre_permutation [in Prune]
Prune [in Prune]

R

redundant [in Redundancy]
red_wrt [in Redundancy]
remove_all [in Basics]
remove_fst [in Basics]
remove_red [in Redundancy]
rem_red [in Redundancy]
run_oracle [in Prune]

S

set [in BinarySequences]
sign [in Basics]
size_complete [in Optimization]
SN2 [in SortingNetworks]
SN3 [in SortingNetworks]
SN4 [in SortingNetworks]
SN5 [in SortingNetworks]
SN9 [in SortingNetworks]
sort [in BinarySequences]
sorted [in BinarySequences]
sorting_network [in SortingNetworks]
split [in Basics]
standard [in SortingNetworks]
subsumption [in Subsumption]
subsumption_opt [in Subsumption]

T

till_n' [in Optimization]
till_n [in SortingNetworks]
transposition [in Permutations]

V

val [in Permutations]

Z

zeros [in BinarySequences]
zero_seq [in BinarySequences]

Variable Index

B

Basic_Properties.HP [in Permutations]
Basic_Properties.P [in Permutations]
Basic_Properties.n [in Permutations]

F

FindAndRemove.A [in Basics]
FindAndRemove.A_dec [in Basics]

P

Pre_permutations.l [in Prune]
Pre_permutations.n [in Prune]

R

RemoveAll.A [in Basics]
RemoveAll.A_dec [in Basics]
Remove.A [in Basics]
Remove.A_dec [in Basics]

S

Split.A [in Basics]
Split.A_dec [in Basics]

T

Transpositions.Hij [in Permutations]
Transpositions.i [in Permutations]
Transpositions.j [in Permutations]
Transpositions.T [in Permutations]
Trees.BT_Wf [in BinaryTrees]
Trees.BT_Add [in BinaryTrees]
Trees.eq_T_compare [in BinaryTrees]
Trees.Map.f [in BinaryTrees]
Trees.T [in BinaryTrees]
Trees.T_dec [in BinaryTrees]
Trees.T_compare_sym_Gt [in BinaryTrees]
Trees.T_compare_trans [in BinaryTrees]
Trees.T_compare_eq [in BinaryTrees]
Trees.T_compare [in BinaryTrees]

Library Index

B

Basics
BinarySequences
BinaryTrees

E

O

P

Permutations
Prune

R

S

SortingNetworks
Standardization
Subsumption

Global Index

H

J

K

Q

U

W

X

_

(565 entries)

Lemma Index

H

J

K

Q

U

W

X

Y

_

other

(403 entries)

Section Index

A

C

D

E

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

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

Constructor Index

A

B

C

D

F

G

H

I

J

K

L

P

Q

R

S

T

U

V

W

X

_

other

(8 entries)

Inductive Index

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

H

J

K

Q

U

W

X

Y

_

other

(98 entries)

Variable Index

A

C

D

E

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

(27 entries)

Library Index

A

C

D

F

G

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

Z

_

other

(11 entries)

This page has been generated by coqdoc