# Bachelor thesis Jan Menz

 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (610 entries) Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (16 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 _ other (27 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (315 entries) Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries) Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (18 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 _ other (18 entries) Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68 entries) Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (122 entries) Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7 entries)

# Global Index

## A

accept [definition, in BA.Automata]
accept_dec [instance, in BA.Automata]
acc_dec [instance, in BA.Automata]
admissible [definition, in BA.FinTypes]
allSub [lemma, in BA.FinTypes]
and_dec [instance, in BA.External]
appendNil [lemma, in BA.BasicDefinitions]
applyVect [definition, in BA.FinTypes]
apply_vectorise_inverse [lemma, in BA.FinTypes]
app_equi_proper [instance, in BA.External]
app_incl_proper [instance, in BA.External]
Automata [library]

## B

BasicDefinitions [library]
bijective [definition, in BA.BasicDefinitions]
boolOption_enum_ok [lemma, in BA.FinTypes]
bool_eq_dec [instance, in BA.External]
bool_enum_ok [lemma, in BA.FinTypes]

## C

card [definition, in BA.External]
CardIn [lemma, in BA.FinTypes]
Cardinality [section, in BA.External]
Cardinality [definition, in BA.FinTypes]
Cardinality_card_eq [lemma, in BA.FinTypes]
Cardinality.X [variable, in BA.External]
card_equi_proper [instance, in BA.External]
card_or [lemma, in BA.External]
card_lt [lemma, in BA.External]
card_equi [lemma, in BA.External]
card_ex [lemma, in BA.External]
card_0 [lemma, in BA.External]
card_cons_rem [lemma, in BA.External]
card_eq [lemma, in BA.External]
card_le [lemma, in BA.External]
card_not_in_rem [lemma, in BA.External]
card_in_rem [lemma, in BA.External]
card_length_leq [lemma, in BA.BasicDefinitions]
card_upper_bound [lemma, in BA.FinTypes]
Card_positiv [lemma, in BA.FinTypes]
Card_X_eq [definition, in BA.FinTypes]
class [projection, in BA.FinTypes]
Closure [lemma, in BA.FinTypes]
Closure_FCIter [lemma, in BA.FinTypes]
complement [definition, in BA.Automata]
complement_correct [lemma, in BA.Automata]
conact_delta_dec [instance, in BA.Automata]
concat [definition, in BA.Automata]
concat_map_length [lemma, in BA.FinTypes]
concat_correct [lemma, in BA.Automata]
concat_delta_Q_star_correct4 [lemma, in BA.Automata]
concat_delta_Q_star_correct3 [lemma, in BA.Automata]
concat_delta_Q_star_correct2 [lemma, in BA.Automata]
concat_delta_Q_star_correct1 [lemma, in BA.Automata]
concat_delta_Q [definition, in BA.Automata]
concat_delta [definition, in BA.Automata]
concat_acc_decPred [definition, in BA.Automata]
concat_acc_pred [definition, in BA.Automata]
cons [definition, in BA.Automata]
consAppend [lemma, in BA.BasicDefinitions]
cons_equi_proper [instance, in BA.External]
cons_incl_proper [instance, in BA.External]
cons_incll [lemma, in BA.BasicDefinitions]
cons_correct [lemma, in BA.Automata]
count [definition, in BA.BasicDefinitions]
countApp [lemma, in BA.BasicDefinitions]
countIn [lemma, in BA.BasicDefinitions]
countMap [lemma, in BA.BasicDefinitions]
countMapExistT [lemma, in BA.FinTypes]
countMapExistT_Zero [lemma, in BA.FinTypes]
countMapZero [lemma, in BA.BasicDefinitions]
countNumberApp [lemma, in BA.FinTypes]
countSplit [lemma, in BA.BasicDefinitions]
counttFL [lemma, in BA.FinTypes]
countZero [lemma, in BA.BasicDefinitions]
count_in_equiv [lemma, in BA.BasicDefinitions]

## D

dec [definition, in BA.External]
decide_rel [projection, in BA.External]
decide_pred [projection, in BA.External]
decide_eq [projection, in BA.External]
decision [definition, in BA.External]
decPred [record, in BA.External]
DecPred [constructor, in BA.External]
decp_dec [instance, in BA.External]
DecRef [lemma, in BA.BasicDefinitions]
decRel [record, in BA.External]
DecRel [constructor, in BA.External]
decRel_dec [instance, in BA.External]
dec_prop_iff [lemma, in BA.External]
dec_DM_all [lemma, in BA.External]
dec_DM_impl [lemma, in BA.External]
dec_DM_and' [lemma, in BA.External]
dec_DM_and [lemma, in BA.External]
dec_DN [lemma, in BA.External]
dec_trans [lemma, in BA.External]
deltaCons [definition, in BA.Automata]
delta_Q_star_trans [lemma, in BA.Automata]
delta_Q_star_dec [instance, in BA.Automata]
delta_Q_star [definition, in BA.Automata]
delta_Q [projection, in BA.Automata]
delta_star_reach [lemma, in BA.Automata]
delta_star [definition, in BA.Automata]
delta_S [projection, in BA.Automata]
dfa [record, in BA.Automata]
DFA [constructor, in BA.Automata]
DFA [section, in BA.Automata]
DFA.Operations [section, in BA.Automata]
DFA.Operations.A [variable, in BA.Automata]
DFA.Operations.A' [variable, in BA.Automata]
DFA.Operations.Product_automaton.op_dec [variable, in BA.Automata]
DFA.Operations.Product_automaton.op [variable, in BA.Automata]
DFA.Operations.Product_automaton [section, in BA.Automata]
DFA.Reachability [section, in BA.Automata]
DFA.Reachability.A [variable, in BA.Automata]
DFA.Sig [variable, in BA.Automata]
diff [definition, in BA.Automata]
diff_correct [lemma, in BA.Automata]
disjoint [definition, in BA.External]
disjoint_app [lemma, in BA.External]
disjoint_cons [lemma, in BA.External]
disjoint_nil' [lemma, in BA.External]
disjoint_nil [lemma, in BA.External]
disjoint_incl [lemma, in BA.External]
disjoint_symm [lemma, in BA.External]
disjoint_forall [lemma, in BA.External]
disjoint_in_map_map_cons [lemma, in BA.FinTypes]
disjoint_in [lemma, in BA.FinTypes]
disjoint_map_cons [lemma, in BA.FinTypes]
disjoint_concat [lemma, in BA.FinTypes]
DM_not_exists [lemma, in BA.External]
DM_or [lemma, in BA.External]
DM_exists [lemma, in BA.FinTypes]
DM_notAll [lemma, in BA.FinTypes]
Dupfree [section, in BA.External]
dupfree [inductive, in BA.External]
dupfreeC [constructor, in BA.External]
dupfreeCount [lemma, in BA.BasicDefinitions]
DupFreeDis [section, in BA.External]
DupFreeDis.X [variable, in BA.External]
dupfreeN [constructor, in BA.External]
dupfree_in_power [lemma, in BA.External]
dupfree_power [lemma, in BA.External]
dupfree_undup [lemma, in BA.External]
dupfree_card [lemma, in BA.External]
dupfree_dec [lemma, in BA.External]
dupfree_filter [lemma, in BA.External]
dupfree_map [lemma, in BA.External]
dupfree_app [lemma, in BA.External]
dupfree_cons [lemma, in BA.External]
dupfree_FCIter [lemma, in BA.FinTypes]
dupfree_iterstep [lemma, in BA.FinTypes]
dupfree_FCStep [lemma, in BA.FinTypes]
dupfree_concat_map_cons [lemma, in BA.FinTypes]
dupfree_concat [lemma, in BA.FinTypes]
dupfree_length [lemma, in BA.FinTypes]
dupfree_elements [lemma, in BA.FinTypes]
dupfree_countOne [lemma, in BA.FinTypes]
Dupfree.X [variable, in BA.External]

## E

elem [definition, in BA.FinTypes]
elementIn [lemma, in BA.FinTypes]
empty [definition, in BA.Automata]
Empty_set_eq_dec [instance, in BA.BasicDefinitions]
Empty_set_enum_ok [lemma, in BA.FinTypes]
empty_reach [lemma, in BA.Automata]
empty_dec [instance, in BA.Automata]
enum [projection, in BA.FinTypes]
enum_ok_fromList [lemma, in BA.FinTypes]
enum_ok [projection, in BA.FinTypes]
Epsilon_autom_correct [lemma, in BA.Automata]
Epsilon_autom [definition, in BA.Automata]
EqBool [definition, in BA.BasicDefinitions]
EqEmpty_set [definition, in BA.BasicDefinitions]
EqFalse [definition, in BA.BasicDefinitions]
EqList [definition, in BA.BasicDefinitions]
EqNat [definition, in BA.BasicDefinitions]
EqOption [definition, in BA.BasicDefinitions]
EqProd [definition, in BA.BasicDefinitions]
EqSigT [definition, in BA.BasicDefinitions]
EqSubType [definition, in BA.BasicDefinitions]
EqSum [definition, in BA.BasicDefinitions]
EqTrue [definition, in BA.BasicDefinitions]
eqtype [projection, in BA.External]
eqType [record, in BA.External]
EqType [constructor, in BA.External]
Equi [section, in BA.External]
equi [definition, in BA.External]
Equivalence_property_exists' [lemma, in BA.FinTypes]
Equivalence_property_exists [lemma, in BA.FinTypes]
Equivalence_property_all [lemma, in BA.FinTypes]
equiv_eq_dec [instance, in BA.Automata]
equi_rotate [lemma, in BA.External]
equi_shift [lemma, in BA.External]
equi_swap [lemma, in BA.External]
equi_dup [lemma, in BA.External]
equi_push [lemma, in BA.External]
equi_Equivalence [instance, in BA.External]
Equi.X [variable, in BA.External]
EqUnit [definition, in BA.BasicDefinitions]
EqVect [definition, in BA.FinTypes]
eq_dec_sigT [instance, in BA.BasicDefinitions]
eq_funTrans [lemma, in BA.BasicDefinitions]
eq_iff [lemma, in BA.FinTypes]
exactW [definition, in BA.Automata]
exactW_correct [lemma, in BA.Automata]
Example1 [definition, in BA.FinTypes]
Example1 [definition, in BA.FinTypes]
Example2 [definition, in BA.FinTypes]
Example2 [definition, in BA.FinTypes]
exists_not_accept_dec [instance, in BA.Automata]
exists_accept_dec [instance, in BA.Automata]
expl [definition, in BA.FinTypes]
extensionalPower [definition, in BA.FinTypes]
External [library]
extPow_length [lemma, in BA.FinTypes]

## F

F [projection, in BA.Automata]
False_dec [instance, in BA.External]
False_eq_dec [instance, in BA.BasicDefinitions]
False_enum_ok [lemma, in BA.FinTypes]
FCIter [definition, in BA.FinTypes]
FCIter_ind [lemma, in BA.FinTypes]
FCIter_fp [lemma, in BA.FinTypes]
FCStep [definition, in BA.FinTypes]
FCStep_admissible [lemma, in BA.FinTypes]
filter [definition, in BA.External]
FilterLemmas [section, in BA.External]
FilterLemmas_pq.q [variable, in BA.External]
FilterLemmas_pq.p [variable, in BA.External]
FilterLemmas_pq.X [variable, in BA.External]
FilterLemmas_pq [section, in BA.External]
FilterLemmas.p [variable, in BA.External]
FilterLemmas.X [variable, in BA.External]
filter_comm [lemma, in BA.External]
filter_and [lemma, in BA.External]
filter_pq_eq [lemma, in BA.External]
filter_pq_mono [lemma, in BA.External]
filter_fst' [lemma, in BA.External]
filter_fst [lemma, in BA.External]
filter_app [lemma, in BA.External]
filter_id [lemma, in BA.External]
filter_mono [lemma, in BA.External]
filter_incl [lemma, in BA.External]
fInduction [lemma, in BA.FinTypes]
FiniteClosureIteration [section, in BA.FinTypes]
FiniteClosureIteration.step [variable, in BA.FinTypes]
FiniteClosureIteration.step_dec [variable, in BA.FinTypes]
FiniteClosureIteration.X [variable, in BA.FinTypes]
finType [record, in BA.FinTypes]
FinType [constructor, in BA.FinTypes]
finTypeC [record, in BA.FinTypes]
FinTypeC [constructor, in BA.FinTypes]
FinTypeClass2 [instance, in BA.FinTypes]
finTypeC_sub [instance, in BA.FinTypes]
finTypeC_sigT [instance, in BA.FinTypes]
finTypeC_vector [instance, in BA.FinTypes]
finTypeC_sum [instance, in BA.FinTypes]
finTypeC_Option [instance, in BA.FinTypes]
finTypeC_Prod [instance, in BA.FinTypes]
finTypeC_False [instance, in BA.FinTypes]
finTypeC_True [instance, in BA.FinTypes]
finTypeC_empty [instance, in BA.FinTypes]
finTypeC_unit [instance, in BA.FinTypes]
finTypeC_bool [instance, in BA.FinTypes]
finTypeOption_enum [lemma, in BA.FinTypes]
finTypeOption_correct [lemma, in BA.FinTypes]
finTypeProd_enum [lemma, in BA.FinTypes]
FinTypes [library]
finTypeSum_enum [lemma, in BA.FinTypes]
finTypeSum_correct [lemma, in BA.FinTypes]
finType_fromList_correct [lemma, in BA.FinTypes]
finType_fromList [definition, in BA.FinTypes]
finType_sub_enum [lemma, in BA.FinTypes]
finType_sub_correct [lemma, in BA.FinTypes]
finType_sub [definition, in BA.FinTypes]
finType_sigT_enum [lemma, in BA.FinTypes]
finType_sigT_correct [lemma, in BA.FinTypes]
finType_sigT [definition, in BA.FinTypes]
finType_vector_enum [lemma, in BA.FinTypes]
finType_vector_correct [lemma, in BA.FinTypes]
finType_vector [definition, in BA.FinTypes]
finType_sum [definition, in BA.FinTypes]
finType_BoolUnit [definition, in BA.FinTypes]
finType_Prod_correct [lemma, in BA.FinTypes]
finType_Option [definition, in BA.FinTypes]
finType_Prod [definition, in BA.FinTypes]
finType_False [definition, in BA.FinTypes]
finType_True [definition, in BA.FinTypes]
finType_Empty_set [definition, in BA.FinTypes]
finType_bool [definition, in BA.FinTypes]
finType_unit [definition, in BA.FinTypes]
finType_cc [definition, in BA.FinTypes]
finType_exists_dec [instance, in BA.FinTypes]
finType_forall_dec [instance, in BA.FinTypes]
Fixedpoints [section, in BA.FinTypes]
Fixedpoints.f [variable, in BA.FinTypes]
Fixedpoints.X [variable, in BA.FinTypes]
fp [definition, in BA.FinTypes]
fp_admissible [lemma, in BA.FinTypes]
fp_card_admissible [lemma, in BA.FinTypes]
fp_iter_trans [lemma, in BA.FinTypes]
fp_trans [lemma, in BA.FinTypes]
fromListC [instance, in BA.FinTypes]

## G

getAt [definition, in BA.FinTypes]
getAt_correct [lemma, in BA.FinTypes]
getImage [definition, in BA.FinTypes]
getImage_correct [lemma, in BA.FinTypes]
getImage_length [lemma, in BA.FinTypes]
getImage_in [lemma, in BA.FinTypes]
getPosition [definition, in BA.FinTypes]

## H

Hedberg [lemma, in BA.BasicDefinitions]
HelpApply [lemma, in BA.FinTypes]

## I

iff_dec [instance, in BA.External]
image [definition, in BA.FinTypes]
images [definition, in BA.FinTypes]
imagesDupfree [lemma, in BA.FinTypes]
imagesInnerLength [lemma, in BA.FinTypes]
imagesNonempty [lemma, in BA.FinTypes]
images_length [lemma, in BA.FinTypes]
impl_dec [instance, in BA.External]
inclp [definition, in BA.External]
Inclusion [section, in BA.External]
Inclusion.X [variable, in BA.External]
incl_equi_proper [instance, in BA.External]
incl_preorder [instance, in BA.External]
incl_app_left [lemma, in BA.External]
incl_lrcons [lemma, in BA.External]
incl_rcons [lemma, in BA.External]
incl_sing [lemma, in BA.External]
incl_lcons [lemma, in BA.External]
incl_shift [lemma, in BA.External]
incl_nil_eq [lemma, in BA.External]
incl_map [lemma, in BA.External]
incl_nil [lemma, in BA.External]
inConcatCons [lemma, in BA.FinTypes]
InCount [lemma, in BA.BasicDefinitions]
index [definition, in BA.FinTypes]
inImages [lemma, in BA.FinTypes]
injective [definition, in BA.BasicDefinitions]
injectiveApply [lemma, in BA.BasicDefinitions]
injective_dupfree [lemma, in BA.FinTypes]
inr_fix [lemma, in BA.Automata]
inr_fix_epsilon [lemma, in BA.Automata]
intersect [definition, in BA.Automata]
intersect_correct [lemma, in BA.Automata]
in_rem_iff [lemma, in BA.External]
in_filter_iff [lemma, in BA.External]
in_equi_proper [instance, in BA.External]
in_incl_proper [instance, in BA.External]
in_cons_neq [lemma, in BA.External]
in_sing [lemma, in BA.External]
in_undup [lemma, in BA.FinTypes]
in_lang [abbreviation, in BA.Automata]
in_lang [abbreviation, in BA.Automata]

## K

kleene_star_correct [lemma, in BA.Automata]
kleene_star_correct2 [lemma, in BA.Automata]
kleene_delta_ok8 [lemma, in BA.Automata]
kleene_delta_ok7 [lemma, in BA.Automata]
kleene_delta_ok6 [lemma, in BA.Automata]
kleene_star_correct1 [lemma, in BA.Automata]
kleene_delta_ok_5 [lemma, in BA.Automata]
kleene_delta_ok_4 [lemma, in BA.Automata]
kleene_delta_ok_3 [lemma, in BA.Automata]
kleene_delta_ok2 [lemma, in BA.Automata]
kleene_delta_ok1 [lemma, in BA.Automata]
kleene_star [definition, in BA.Automata]
kleene_delta_dec [instance, in BA.Automata]
kleene_delta [definition, in BA.Automata]
kleene_acc_decPred [definition, in BA.Automata]
kleene_acc_dec [instance, in BA.Automata]
kleene_acc_pred [definition, in BA.Automata]

## L

lang_sub_dec [instance, in BA.Automata]
lang_equiv [definition, in BA.Automata]
lang_incl_iff [lemma, in BA.Automata]
lang_incl [definition, in BA.Automata]
least_fp_containing [definition, in BA.FinTypes]
lengthEq [lemma, in BA.BasicDefinitions]
list_cc [lemma, in BA.External]
list_exists_not_incl [lemma, in BA.External]
list_exists_DM [lemma, in BA.External]
list_exists_dec [instance, in BA.External]
list_forall_dec [instance, in BA.External]
list_sigma_forall [lemma, in BA.External]
list_cycle [lemma, in BA.External]
list_in_dec [instance, in BA.External]
list_eq_dec [instance, in BA.External]
loop [lemma, in BA.BasicDefinitions]

## M

mC [definition, in BA.FinTypes]
Membership [section, in BA.External]
Membership.X [variable, in BA.External]
mmC [definition, in BA.FinTypes]

## N

nat_le_dec [instance, in BA.External]
nat_eq_dec [instance, in BA.External]
negOr [lemma, in BA.BasicDefinitions]
neg_F [definition, in BA.Automata]
nfa [record, in BA.Automata]
NFA [constructor, in BA.Automata]
nil_kleene [lemma, in BA.Automata]
NoneElement [lemma, in BA.FinTypes]
notInMapCons [lemma, in BA.FinTypes]
notInZero [lemma, in BA.BasicDefinitions]
not_in_cons [lemma, in BA.External]
not_dec [instance, in BA.External]
NullMul [lemma, in BA.BasicDefinitions]
n_accept [definition, in BA.Automata]

## O

onestate [definition, in BA.Automata]
onestate_correct [lemma, in BA.Automata]
option_eq_dec [instance, in BA.BasicDefinitions]
Option_Card [lemma, in BA.FinTypes]
option_enum_ok [lemma, in BA.FinTypes]
or_dec [instance, in BA.External]

## P

pick [lemma, in BA.FinTypes]
pickx [definition, in BA.FinTypes]
pidgeonHole_bij [lemma, in BA.FinTypes]
pidgeonHole_surj [lemma, in BA.FinTypes]
pidgeonHole_inj [lemma, in BA.FinTypes]
power [definition, in BA.External]
PowerRep [section, in BA.External]
PowerRep.X [variable, in BA.External]
power_extensional [lemma, in BA.External]
power_nil [lemma, in BA.External]
power_incl [lemma, in BA.External]
predCons [definition, in BA.Automata]
predCons_dec [instance, in BA.Automata]
predicate [projection, in BA.External]
preservation_FCIter [lemma, in BA.FinTypes]
preservation_iter [lemma, in BA.FinTypes]
preservation_step [lemma, in BA.FinTypes]
prod [definition, in BA.Automata]
ProdCount [lemma, in BA.FinTypes]
prodLists [definition, in BA.BasicDefinitions]
prod_nil [lemma, in BA.BasicDefinitions]
prod_eq_dec [instance, in BA.BasicDefinitions]
Prod_Card [lemma, in BA.FinTypes]
prod_enum_ok [lemma, in BA.FinTypes]
prod_correct [lemma, in BA.Automata]
prod_delta_star [lemma, in BA.Automata]
prod_F [definition, in BA.Automata]
prod_pred_dec [instance, in BA.Automata]
prod_pred [definition, in BA.Automata]
prod_delta [definition, in BA.Automata]
proj1_sig_fun [lemma, in BA.BasicDefinitions]
proveOne [lemma, in BA.FinTypes]
pure [definition, in BA.BasicDefinitions]
pure_eq [lemma, in BA.BasicDefinitions]
pure_impure [lemma, in BA.BasicDefinitions]
pure_equiv [lemma, in BA.BasicDefinitions]
purify [lemma, in BA.BasicDefinitions]

## Q

Q [projection, in BA.Automata]
Q_acc [projection, in BA.Automata]
q0 [projection, in BA.Automata]

## R

reach [definition, in BA.Automata]
reachable [inductive, in BA.Automata]
reachable_with_something_dec [instance, in BA.Automata]
reachable_dec [instance, in BA.Automata]
reachable_transitive [lemma, in BA.Automata]
reachable_with_reachable [lemma, in BA.Automata]
reachable_with [definition, in BA.Automata]
reach_reachable_with [lemma, in BA.Automata]
reach_correct [lemma, in BA.Automata]
reach_correct2 [lemma, in BA.Automata]
reach_correct2' [lemma, in BA.Automata]
reach_correct1 [lemma, in BA.Automata]
reach_least_fp [lemma, in BA.Automata]
refl [constructor, in BA.Automata]
relation [projection, in BA.External]
rem [definition, in BA.External]
Removal [section, in BA.External]
Removal.X [variable, in BA.External]
rem_inclr [lemma, in BA.External]
rem_reorder [lemma, in BA.External]
rem_id [lemma, in BA.External]
rem_fst' [lemma, in BA.External]
rem_fst [lemma, in BA.External]
rem_comm [lemma, in BA.External]
rem_equi [lemma, in BA.External]
rem_app' [lemma, in BA.External]
rem_app [lemma, in BA.External]
rem_neq [lemma, in BA.External]
rem_in [lemma, in BA.External]
rem_cons' [lemma, in BA.External]
rem_cons [lemma, in BA.External]
rem_mono [lemma, in BA.External]
rem_incl [lemma, in BA.External]
rem_not_in [lemma, in BA.External]
rep [definition, in BA.External]
rep_dupfree [lemma, in BA.External]
rep_idempotent [lemma, in BA.External]
rep_injective [lemma, in BA.External]
rep_eq [lemma, in BA.External]
rep_eq' [lemma, in BA.External]
rep_mono [lemma, in BA.External]
rep_equi [lemma, in BA.External]
rep_in [lemma, in BA.External]
rep_incl [lemma, in BA.External]
rep_power [lemma, in BA.External]
rightResult [lemma, in BA.FinTypes]

## S

s [projection, in BA.Automata]
S [projection, in BA.Automata]
sigT_proj2_fun [lemma, in BA.BasicDefinitions]
sigT_proj1_fun [lemma, in BA.BasicDefinitions]
sigT_enum_ok [lemma, in BA.FinTypes]
Sig_dec [instance, in BA.Automata]
Sig_reach [lemma, in BA.Automata]
size_induction [lemma, in BA.External]
SomeElement [lemma, in BA.FinTypes]
step [constructor, in BA.Automata]
step_consistent_least_fp [lemma, in BA.FinTypes]
step_trans_fp_incl [lemma, in BA.FinTypes]
step_iter_consistent [lemma, in BA.FinTypes]
step_consistent [definition, in BA.FinTypes]
step_reach_consistent [lemma, in BA.Automata]
step_reach [definition, in BA.Automata]
Streicher_K [lemma, in BA.BasicDefinitions]
subtype [definition, in BA.BasicDefinitions]
subType_eq_dec [instance, in BA.BasicDefinitions]
subtype_extensionality [lemma, in BA.BasicDefinitions]
subType_enum_ok [lemma, in BA.FinTypes]
success2 [definition, in BA.FinTypes]
success3 [definition, in BA.FinTypes]
SumCard [lemma, in BA.FinTypes]
sum_eq_dec [instance, in BA.BasicDefinitions]
sum_enum_ok [lemma, in BA.FinTypes]
surjective [definition, in BA.BasicDefinitions]
surjectiveApply [lemma, in BA.BasicDefinitions]
surj_sub [lemma, in BA.FinTypes]

## T

Test [section, in BA.FinTypes]
Test.X [variable, in BA.FinTypes]
Test.Y [variable, in BA.FinTypes]
# _ [notation, in BA.FinTypes]
toBool [definition, in BA.BasicDefinitions]
toDFA [definition, in BA.Automata]
toDFA_correct [lemma, in BA.Automata]
toDFA_delta_star_correct2 [lemma, in BA.Automata]
toDFA_delta_star_correct1 [lemma, in BA.Automata]
toDFA_delta_correct [lemma, in BA.Automata]
toDFA_delta [definition, in BA.Automata]
toDFA_F [definition, in BA.Automata]
toeqType [definition, in BA.BasicDefinitions]
toeqTypeCorrect [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_sub [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_sigT [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_list [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_true [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_false [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_empty [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_prod [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_option [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_nat [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_bool [lemma, in BA.BasicDefinitions]
toeqTypeCorrect_unit [lemma, in BA.BasicDefinitions]
toeqType_idempotent [lemma, in BA.BasicDefinitions]
toeqType_sum [lemma, in BA.BasicDefinitions]
tofinType [definition, in BA.FinTypes]
tofinType_sub_correct [lemma, in BA.FinTypes]
tofinType_sigT_correct [lemma, in BA.FinTypes]
tofinType_vector_correct [lemma, in BA.FinTypes]
tofinType_idempotent [lemma, in BA.FinTypes]
tofinType_works [lemma, in BA.FinTypes]
toNFA [definition, in BA.Automata]
toNFA_correct [lemma, in BA.Automata]
toNFA_delta_star_correct [lemma, in BA.Automata]
toOptionList [definition, in BA.BasicDefinitions]
toProp [definition, in BA.Automata]
toProp_dec [instance, in BA.Automata]
toSigTList [definition, in BA.FinTypes]
toSigTList_count [lemma, in BA.FinTypes]
toSubList [definition, in BA.FinTypes]
toSubList_count [lemma, in BA.FinTypes]
toSumList1 [definition, in BA.BasicDefinitions]
toSumList1_missing [lemma, in BA.BasicDefinitions]
toSumList1_count [lemma, in BA.BasicDefinitions]
toSumList2 [definition, in BA.BasicDefinitions]
toSumList2_missing [lemma, in BA.BasicDefinitions]
toSumList2_count [lemma, in BA.BasicDefinitions]
True_dec [instance, in BA.External]
True_eq_dec [instance, in BA.BasicDefinitions]
True_enum_ok [lemma, in BA.FinTypes]
type [projection, in BA.FinTypes]

## U

U [definition, in BA.Automata]
undup [definition, in BA.External]
Undup [section, in BA.External]
undup_idempotent [lemma, in BA.External]
undup_id [lemma, in BA.External]
undup_equi [lemma, in BA.External]
undup_incl [lemma, in BA.External]
undup_id_equi [lemma, in BA.External]
Undup.X [variable, in BA.External]
unit_eq_dec [instance, in BA.BasicDefinitions]
unit_enum_ok [lemma, in BA.FinTypes]
U_correct [lemma, in BA.Automata]

## V

vector [definition, in BA.FinTypes]
vectorise [definition, in BA.FinTypes]
vectorise_apply_inverse [lemma, in BA.FinTypes]
vectorise_apply_inverse' [lemma, in BA.FinTypes]
Vector_Card [lemma, in BA.FinTypes]
vector_extensionality [lemma, in BA.FinTypes]
vector_enum_ok [lemma, in BA.FinTypes]
vector_eq_dec [instance, in BA.FinTypes]

## W

word [definition, in BA.Automata]

## other

_ ** _ (EqTypeScope) [notation, in BA.BasicDefinitions]
Sigma _ .. _ , _ (type_scope) [notation, in BA.External]
_ === _ [notation, in BA.External]
_ <<= _ [notation, in BA.External]
_ el _ [notation, in BA.External]
_ ** _ [notation, in BA.BasicDefinitions]
_ ^ _ [notation, in BA.FinTypes]
_ --> _ [notation, in BA.FinTypes]
_ (+) _ [notation, in BA.FinTypes]
_ (x) _ [notation, in BA.FinTypes]
eq_dec _ [notation, in BA.External]
# _ [notation, in BA.FinTypes]
? _ [notation, in BA.FinTypes]
?? _ [notation, in BA.BasicDefinitions]
| _ | [notation, in BA.External]

# Notation Index

## T

# _ [in BA.FinTypes]

## other

_ ** _ (EqTypeScope) [in BA.BasicDefinitions]
Sigma _ .. _ , _ (type_scope) [in BA.External]
_ === _ [in BA.External]
_ <<= _ [in BA.External]
_ el _ [in BA.External]
_ ** _ [in BA.BasicDefinitions]
_ ^ _ [in BA.FinTypes]
_ --> _ [in BA.FinTypes]
_ (+) _ [in BA.FinTypes]
_ (x) _ [in BA.FinTypes]
eq_dec _ [in BA.External]
# _ [in BA.FinTypes]
? _ [in BA.FinTypes]
?? _ [in BA.BasicDefinitions]
| _ | [in BA.External]

# Variable Index

## C

Cardinality.X [in BA.External]

## D

DFA.Operations.A [in BA.Automata]
DFA.Operations.A' [in BA.Automata]
DFA.Operations.Product_automaton.op_dec [in BA.Automata]
DFA.Operations.Product_automaton.op [in BA.Automata]
DFA.Reachability.A [in BA.Automata]
DFA.Sig [in BA.Automata]
DupFreeDis.X [in BA.External]
Dupfree.X [in BA.External]

## E

Equi.X [in BA.External]

## F

FilterLemmas_pq.q [in BA.External]
FilterLemmas_pq.p [in BA.External]
FilterLemmas_pq.X [in BA.External]
FilterLemmas.p [in BA.External]
FilterLemmas.X [in BA.External]
FiniteClosureIteration.step [in BA.FinTypes]
FiniteClosureIteration.step_dec [in BA.FinTypes]
FiniteClosureIteration.X [in BA.FinTypes]
Fixedpoints.f [in BA.FinTypes]
Fixedpoints.X [in BA.FinTypes]

## I

Inclusion.X [in BA.External]

## M

Membership.X [in BA.External]

## P

PowerRep.X [in BA.External]

## R

Removal.X [in BA.External]

## T

Test.X [in BA.FinTypes]
Test.Y [in BA.FinTypes]

## U

Undup.X [in BA.External]

Automata

BasicDefinitions

External

FinTypes

# Lemma Index

## A

allSub [in BA.FinTypes]
appendNil [in BA.BasicDefinitions]
apply_vectorise_inverse [in BA.FinTypes]

## B

boolOption_enum_ok [in BA.FinTypes]
bool_enum_ok [in BA.FinTypes]

## C

CardIn [in BA.FinTypes]
Cardinality_card_eq [in BA.FinTypes]
card_or [in BA.External]
card_lt [in BA.External]
card_equi [in BA.External]
card_ex [in BA.External]
card_0 [in BA.External]
card_cons_rem [in BA.External]
card_eq [in BA.External]
card_le [in BA.External]
card_not_in_rem [in BA.External]
card_in_rem [in BA.External]
card_length_leq [in BA.BasicDefinitions]
card_upper_bound [in BA.FinTypes]
Card_positiv [in BA.FinTypes]
Closure [in BA.FinTypes]
Closure_FCIter [in BA.FinTypes]
complement_correct [in BA.Automata]
concat_map_length [in BA.FinTypes]
concat_correct [in BA.Automata]
concat_delta_Q_star_correct4 [in BA.Automata]
concat_delta_Q_star_correct3 [in BA.Automata]
concat_delta_Q_star_correct2 [in BA.Automata]
concat_delta_Q_star_correct1 [in BA.Automata]
consAppend [in BA.BasicDefinitions]
cons_incll [in BA.BasicDefinitions]
cons_correct [in BA.Automata]
countApp [in BA.BasicDefinitions]
countIn [in BA.BasicDefinitions]
countMap [in BA.BasicDefinitions]
countMapExistT [in BA.FinTypes]
countMapExistT_Zero [in BA.FinTypes]
countMapZero [in BA.BasicDefinitions]
countNumberApp [in BA.FinTypes]
countSplit [in BA.BasicDefinitions]
counttFL [in BA.FinTypes]
countZero [in BA.BasicDefinitions]
count_in_equiv [in BA.BasicDefinitions]

## D

DecRef [in BA.BasicDefinitions]
dec_prop_iff [in BA.External]
dec_DM_all [in BA.External]
dec_DM_impl [in BA.External]
dec_DM_and' [in BA.External]
dec_DM_and [in BA.External]
dec_DN [in BA.External]
dec_trans [in BA.External]
delta_Q_star_trans [in BA.Automata]
delta_star_reach [in BA.Automata]
diff_correct [in BA.Automata]
disjoint_app [in BA.External]
disjoint_cons [in BA.External]
disjoint_nil' [in BA.External]
disjoint_nil [in BA.External]
disjoint_incl [in BA.External]
disjoint_symm [in BA.External]
disjoint_forall [in BA.External]
disjoint_in_map_map_cons [in BA.FinTypes]
disjoint_in [in BA.FinTypes]
disjoint_map_cons [in BA.FinTypes]
disjoint_concat [in BA.FinTypes]
DM_not_exists [in BA.External]
DM_or [in BA.External]
DM_exists [in BA.FinTypes]
DM_notAll [in BA.FinTypes]
dupfreeCount [in BA.BasicDefinitions]
dupfree_in_power [in BA.External]
dupfree_power [in BA.External]
dupfree_undup [in BA.External]
dupfree_card [in BA.External]
dupfree_dec [in BA.External]
dupfree_filter [in BA.External]
dupfree_map [in BA.External]
dupfree_app [in BA.External]
dupfree_cons [in BA.External]
dupfree_FCIter [in BA.FinTypes]
dupfree_iterstep [in BA.FinTypes]
dupfree_FCStep [in BA.FinTypes]
dupfree_concat_map_cons [in BA.FinTypes]
dupfree_concat [in BA.FinTypes]
dupfree_length [in BA.FinTypes]
dupfree_elements [in BA.FinTypes]
dupfree_countOne [in BA.FinTypes]

## E

elementIn [in BA.FinTypes]
Empty_set_enum_ok [in BA.FinTypes]
empty_reach [in BA.Automata]
enum_ok_fromList [in BA.FinTypes]
Epsilon_autom_correct [in BA.Automata]
Equivalence_property_exists' [in BA.FinTypes]
Equivalence_property_exists [in BA.FinTypes]
Equivalence_property_all [in BA.FinTypes]
equi_rotate [in BA.External]
equi_shift [in BA.External]
equi_swap [in BA.External]
equi_dup [in BA.External]
equi_push [in BA.External]
eq_funTrans [in BA.BasicDefinitions]
eq_iff [in BA.FinTypes]
exactW_correct [in BA.Automata]
extPow_length [in BA.FinTypes]

## F

False_enum_ok [in BA.FinTypes]
FCIter_ind [in BA.FinTypes]
FCIter_fp [in BA.FinTypes]
FCStep_admissible [in BA.FinTypes]
filter_comm [in BA.External]
filter_and [in BA.External]
filter_pq_eq [in BA.External]
filter_pq_mono [in BA.External]
filter_fst' [in BA.External]
filter_fst [in BA.External]
filter_app [in BA.External]
filter_id [in BA.External]
filter_mono [in BA.External]
filter_incl [in BA.External]
fInduction [in BA.FinTypes]
finTypeOption_enum [in BA.FinTypes]
finTypeOption_correct [in BA.FinTypes]
finTypeProd_enum [in BA.FinTypes]
finTypeSum_enum [in BA.FinTypes]
finTypeSum_correct [in BA.FinTypes]
finType_fromList_correct [in BA.FinTypes]
finType_sub_enum [in BA.FinTypes]
finType_sub_correct [in BA.FinTypes]
finType_sigT_enum [in BA.FinTypes]
finType_sigT_correct [in BA.FinTypes]
finType_vector_enum [in BA.FinTypes]
finType_vector_correct [in BA.FinTypes]
finType_Prod_correct [in BA.FinTypes]
fp_admissible [in BA.FinTypes]
fp_card_admissible [in BA.FinTypes]
fp_iter_trans [in BA.FinTypes]
fp_trans [in BA.FinTypes]

## G

getAt_correct [in BA.FinTypes]
getImage_correct [in BA.FinTypes]
getImage_length [in BA.FinTypes]
getImage_in [in BA.FinTypes]

## H

Hedberg [in BA.BasicDefinitions]
HelpApply [in BA.FinTypes]

## I

imagesDupfree [in BA.FinTypes]
imagesInnerLength [in BA.FinTypes]
imagesNonempty [in BA.FinTypes]
images_length [in BA.FinTypes]
incl_app_left [in BA.External]
incl_lrcons [in BA.External]
incl_rcons [in BA.External]
incl_sing [in BA.External]
incl_lcons [in BA.External]
incl_shift [in BA.External]
incl_nil_eq [in BA.External]
incl_map [in BA.External]
incl_nil [in BA.External]
inConcatCons [in BA.FinTypes]
InCount [in BA.BasicDefinitions]
inImages [in BA.FinTypes]
injectiveApply [in BA.BasicDefinitions]
injective_dupfree [in BA.FinTypes]
inr_fix [in BA.Automata]
inr_fix_epsilon [in BA.Automata]
intersect_correct [in BA.Automata]
in_rem_iff [in BA.External]
in_filter_iff [in BA.External]
in_cons_neq [in BA.External]
in_sing [in BA.External]
in_undup [in BA.FinTypes]

## K

kleene_star_correct [in BA.Automata]
kleene_star_correct2 [in BA.Automata]
kleene_delta_ok8 [in BA.Automata]
kleene_delta_ok7 [in BA.Automata]
kleene_delta_ok6 [in BA.Automata]
kleene_star_correct1 [in BA.Automata]
kleene_delta_ok_5 [in BA.Automata]
kleene_delta_ok_4 [in BA.Automata]
kleene_delta_ok_3 [in BA.Automata]
kleene_delta_ok2 [in BA.Automata]
kleene_delta_ok1 [in BA.Automata]

## L

lang_incl_iff [in BA.Automata]
lengthEq [in BA.BasicDefinitions]
list_cc [in BA.External]
list_exists_not_incl [in BA.External]
list_exists_DM [in BA.External]
list_sigma_forall [in BA.External]
list_cycle [in BA.External]
loop [in BA.BasicDefinitions]

## N

negOr [in BA.BasicDefinitions]
nil_kleene [in BA.Automata]
NoneElement [in BA.FinTypes]
notInMapCons [in BA.FinTypes]
notInZero [in BA.BasicDefinitions]
not_in_cons [in BA.External]
NullMul [in BA.BasicDefinitions]

## O

onestate_correct [in BA.Automata]
Option_Card [in BA.FinTypes]
option_enum_ok [in BA.FinTypes]

## P

pick [in BA.FinTypes]
pidgeonHole_bij [in BA.FinTypes]
pidgeonHole_surj [in BA.FinTypes]
pidgeonHole_inj [in BA.FinTypes]
power_extensional [in BA.External]
power_nil [in BA.External]
power_incl [in BA.External]
preservation_FCIter [in BA.FinTypes]
preservation_iter [in BA.FinTypes]
preservation_step [in BA.FinTypes]
ProdCount [in BA.FinTypes]
prod_nil [in BA.BasicDefinitions]
Prod_Card [in BA.FinTypes]
prod_enum_ok [in BA.FinTypes]
prod_correct [in BA.Automata]
prod_delta_star [in BA.Automata]
proj1_sig_fun [in BA.BasicDefinitions]
proveOne [in BA.FinTypes]
pure_eq [in BA.BasicDefinitions]
pure_impure [in BA.BasicDefinitions]
pure_equiv [in BA.BasicDefinitions]
purify [in BA.BasicDefinitions]

## R

reachable_transitive [in BA.Automata]
reachable_with_reachable [in BA.Automata]
reach_reachable_with [in BA.Automata]
reach_correct [in BA.Automata]
reach_correct2 [in BA.Automata]
reach_correct2' [in BA.Automata]
reach_correct1 [in BA.Automata]
reach_least_fp [in BA.Automata]
rem_inclr [in BA.External]
rem_reorder [in BA.External]
rem_id [in BA.External]
rem_fst' [in BA.External]
rem_fst [in BA.External]
rem_comm [in BA.External]
rem_equi [in BA.External]
rem_app' [in BA.External]
rem_app [in BA.External]
rem_neq [in BA.External]
rem_in [in BA.External]
rem_cons' [in BA.External]
rem_cons [in BA.External]
rem_mono [in BA.External]
rem_incl [in BA.External]
rem_not_in [in BA.External]
rep_dupfree [in BA.External]
rep_idempotent [in BA.External]
rep_injective [in BA.External]
rep_eq [in BA.External]
rep_eq' [in BA.External]
rep_mono [in BA.External]
rep_equi [in BA.External]
rep_in [in BA.External]
rep_incl [in BA.External]
rep_power [in BA.External]
rightResult [in BA.FinTypes]

## S

sigT_proj2_fun [in BA.BasicDefinitions]
sigT_proj1_fun [in BA.BasicDefinitions]
sigT_enum_ok [in BA.FinTypes]
Sig_reach [in BA.Automata]
size_induction [in BA.External]
SomeElement [in BA.FinTypes]
step_consistent_least_fp [in BA.FinTypes]
step_trans_fp_incl [in BA.FinTypes]
step_iter_consistent [in BA.FinTypes]
step_reach_consistent [in BA.Automata]
Streicher_K [in BA.BasicDefinitions]
subtype_extensionality [in BA.BasicDefinitions]
subType_enum_ok [in BA.FinTypes]
SumCard [in BA.FinTypes]
sum_enum_ok [in BA.FinTypes]
surjectiveApply [in BA.BasicDefinitions]
surj_sub [in BA.FinTypes]

## T

toDFA_correct [in BA.Automata]
toDFA_delta_star_correct2 [in BA.Automata]
toDFA_delta_star_correct1 [in BA.Automata]
toDFA_delta_correct [in BA.Automata]
toeqTypeCorrect [in BA.BasicDefinitions]
toeqTypeCorrect_sub [in BA.BasicDefinitions]
toeqTypeCorrect_sigT [in BA.BasicDefinitions]
toeqTypeCorrect_list [in BA.BasicDefinitions]
toeqTypeCorrect_true [in BA.BasicDefinitions]
toeqTypeCorrect_false [in BA.BasicDefinitions]
toeqTypeCorrect_empty [in BA.BasicDefinitions]
toeqTypeCorrect_prod [in BA.BasicDefinitions]
toeqTypeCorrect_option [in BA.BasicDefinitions]
toeqTypeCorrect_nat [in BA.BasicDefinitions]
toeqTypeCorrect_bool [in BA.BasicDefinitions]
toeqTypeCorrect_unit [in BA.BasicDefinitions]
toeqType_idempotent [in BA.BasicDefinitions]
toeqType_sum [in BA.BasicDefinitions]
tofinType_sub_correct [in BA.FinTypes]
tofinType_sigT_correct [in BA.FinTypes]
tofinType_vector_correct [in BA.FinTypes]
tofinType_idempotent [in BA.FinTypes]
tofinType_works [in BA.FinTypes]
toNFA_correct [in BA.Automata]
toNFA_delta_star_correct [in BA.Automata]
toSigTList_count [in BA.FinTypes]
toSubList_count [in BA.FinTypes]
toSumList1_missing [in BA.BasicDefinitions]
toSumList1_count [in BA.BasicDefinitions]
toSumList2_missing [in BA.BasicDefinitions]
toSumList2_count [in BA.BasicDefinitions]
True_enum_ok [in BA.FinTypes]

## U

undup_idempotent [in BA.External]
undup_id [in BA.External]
undup_equi [in BA.External]
undup_incl [in BA.External]
undup_id_equi [in BA.External]
unit_enum_ok [in BA.FinTypes]
U_correct [in BA.Automata]

## V

vectorise_apply_inverse [in BA.FinTypes]
vectorise_apply_inverse' [in BA.FinTypes]
Vector_Card [in BA.FinTypes]
vector_extensionality [in BA.FinTypes]
vector_enum_ok [in BA.FinTypes]

# Constructor Index

## D

DecPred [in BA.External]
DecRel [in BA.External]
DFA [in BA.Automata]
dupfreeC [in BA.External]
dupfreeN [in BA.External]

## E

EqType [in BA.External]

## F

FinType [in BA.FinTypes]
FinTypeC [in BA.FinTypes]

## N

NFA [in BA.Automata]

## R

refl [in BA.Automata]

## S

step [in BA.Automata]

# Inductive Index

## D

dupfree [in BA.External]

## R

reachable [in BA.Automata]

# Projection Index

## C

class [in BA.FinTypes]

## D

decide_rel [in BA.External]
decide_pred [in BA.External]
decide_eq [in BA.External]
delta_Q [in BA.Automata]
delta_S [in BA.Automata]

## E

enum [in BA.FinTypes]
enum_ok [in BA.FinTypes]
eqtype [in BA.External]

## F

F [in BA.Automata]

## P

predicate [in BA.External]

## Q

Q [in BA.Automata]
Q_acc [in BA.Automata]
q0 [in BA.Automata]

## R

relation [in BA.External]

## S

s [in BA.Automata]
S [in BA.Automata]

## T

type [in BA.FinTypes]

# Section Index

## C

Cardinality [in BA.External]

## D

DFA [in BA.Automata]
DFA.Operations [in BA.Automata]
DFA.Operations.Product_automaton [in BA.Automata]
DFA.Reachability [in BA.Automata]
Dupfree [in BA.External]
DupFreeDis [in BA.External]

## E

Equi [in BA.External]

## F

FilterLemmas [in BA.External]
FilterLemmas_pq [in BA.External]
FiniteClosureIteration [in BA.FinTypes]
Fixedpoints [in BA.FinTypes]

## I

Inclusion [in BA.External]

## M

Membership [in BA.External]

## P

PowerRep [in BA.External]

## R

Removal [in BA.External]

## T

Test [in BA.FinTypes]

## U

Undup [in BA.External]

# Instance Index

## A

accept_dec [in BA.Automata]
acc_dec [in BA.Automata]
and_dec [in BA.External]
app_equi_proper [in BA.External]
app_incl_proper [in BA.External]

## B

bool_eq_dec [in BA.External]

## C

card_equi_proper [in BA.External]
conact_delta_dec [in BA.Automata]
cons_equi_proper [in BA.External]
cons_incl_proper [in BA.External]

## D

decp_dec [in BA.External]
decRel_dec [in BA.External]
delta_Q_star_dec [in BA.Automata]

## E

Empty_set_eq_dec [in BA.BasicDefinitions]
empty_dec [in BA.Automata]
equiv_eq_dec [in BA.Automata]
equi_Equivalence [in BA.External]
eq_dec_sigT [in BA.BasicDefinitions]
exists_not_accept_dec [in BA.Automata]
exists_accept_dec [in BA.Automata]

## F

False_dec [in BA.External]
False_eq_dec [in BA.BasicDefinitions]
FinTypeClass2 [in BA.FinTypes]
finTypeC_sub [in BA.FinTypes]
finTypeC_sigT [in BA.FinTypes]
finTypeC_vector [in BA.FinTypes]
finTypeC_sum [in BA.FinTypes]
finTypeC_Option [in BA.FinTypes]
finTypeC_Prod [in BA.FinTypes]
finTypeC_False [in BA.FinTypes]
finTypeC_True [in BA.FinTypes]
finTypeC_empty [in BA.FinTypes]
finTypeC_unit [in BA.FinTypes]
finTypeC_bool [in BA.FinTypes]
finType_exists_dec [in BA.FinTypes]
finType_forall_dec [in BA.FinTypes]
fromListC [in BA.FinTypes]

## I

iff_dec [in BA.External]
impl_dec [in BA.External]
incl_equi_proper [in BA.External]
incl_preorder [in BA.External]
in_equi_proper [in BA.External]
in_incl_proper [in BA.External]

## K

kleene_delta_dec [in BA.Automata]
kleene_acc_dec [in BA.Automata]

## L

lang_sub_dec [in BA.Automata]
list_exists_dec [in BA.External]
list_forall_dec [in BA.External]
list_in_dec [in BA.External]
list_eq_dec [in BA.External]

## N

nat_le_dec [in BA.External]
nat_eq_dec [in BA.External]
not_dec [in BA.External]

## O

option_eq_dec [in BA.BasicDefinitions]
or_dec [in BA.External]

## P

predCons_dec [in BA.Automata]
prod_eq_dec [in BA.BasicDefinitions]
prod_pred_dec [in BA.Automata]

## R

reachable_with_something_dec [in BA.Automata]
reachable_dec [in BA.Automata]

## S

Sig_dec [in BA.Automata]
subType_eq_dec [in BA.BasicDefinitions]
sum_eq_dec [in BA.BasicDefinitions]

## T

toProp_dec [in BA.Automata]
True_dec [in BA.External]
True_eq_dec [in BA.BasicDefinitions]

## U

unit_eq_dec [in BA.BasicDefinitions]

## V

vector_eq_dec [in BA.FinTypes]

# Abbreviation Index

## I

in_lang [in BA.Automata]
in_lang [in BA.Automata]

# Definition Index

## A

accept [in BA.Automata]
admissible [in BA.FinTypes]
applyVect [in BA.FinTypes]

## B

bijective [in BA.BasicDefinitions]

## C

card [in BA.External]
Cardinality [in BA.FinTypes]
Card_X_eq [in BA.FinTypes]
complement [in BA.Automata]
concat [in BA.Automata]
concat_delta_Q [in BA.Automata]
concat_delta [in BA.Automata]
concat_acc_decPred [in BA.Automata]
concat_acc_pred [in BA.Automata]
cons [in BA.Automata]
count [in BA.BasicDefinitions]

## D

dec [in BA.External]
decision [in BA.External]
deltaCons [in BA.Automata]
delta_Q_star [in BA.Automata]
delta_star [in BA.Automata]
diff [in BA.Automata]
disjoint [in BA.External]

## E

elem [in BA.FinTypes]
empty [in BA.Automata]
Epsilon_autom [in BA.Automata]
EqBool [in BA.BasicDefinitions]
EqEmpty_set [in BA.BasicDefinitions]
EqFalse [in BA.BasicDefinitions]
EqList [in BA.BasicDefinitions]
EqNat [in BA.BasicDefinitions]
EqOption [in BA.BasicDefinitions]
EqProd [in BA.BasicDefinitions]
EqSigT [in BA.BasicDefinitions]
EqSubType [in BA.BasicDefinitions]
EqSum [in BA.BasicDefinitions]
EqTrue [in BA.BasicDefinitions]
equi [in BA.External]
EqUnit [in BA.BasicDefinitions]
EqVect [in BA.FinTypes]
exactW [in BA.Automata]
Example1 [in BA.FinTypes]
Example1 [in BA.FinTypes]
Example2 [in BA.FinTypes]
Example2 [in BA.FinTypes]
expl [in BA.FinTypes]
extensionalPower [in BA.FinTypes]

## F

FCIter [in BA.FinTypes]
FCStep [in BA.FinTypes]
filter [in BA.External]
finType_fromList [in BA.FinTypes]
finType_sub [in BA.FinTypes]
finType_sigT [in BA.FinTypes]
finType_vector [in BA.FinTypes]
finType_sum [in BA.FinTypes]
finType_BoolUnit [in BA.FinTypes]
finType_Option [in BA.FinTypes]
finType_Prod [in BA.FinTypes]
finType_False [in BA.FinTypes]
finType_True [in BA.FinTypes]
finType_Empty_set [in BA.FinTypes]
finType_bool [in BA.FinTypes]
finType_unit [in BA.FinTypes]
finType_cc [in BA.FinTypes]
fp [in BA.FinTypes]

## G

getAt [in BA.FinTypes]
getImage [in BA.FinTypes]
getPosition [in BA.FinTypes]

## I

image [in BA.FinTypes]
images [in BA.FinTypes]
inclp [in BA.External]
index [in BA.FinTypes]
injective [in BA.BasicDefinitions]
intersect [in BA.Automata]

## K

kleene_star [in BA.Automata]
kleene_delta [in BA.Automata]
kleene_acc_decPred [in BA.Automata]
kleene_acc_pred [in BA.Automata]

## L

lang_equiv [in BA.Automata]
lang_incl [in BA.Automata]
least_fp_containing [in BA.FinTypes]

## M

mC [in BA.FinTypes]
mmC [in BA.FinTypes]

## N

neg_F [in BA.Automata]
n_accept [in BA.Automata]

## O

onestate [in BA.Automata]

## P

pickx [in BA.FinTypes]
power [in BA.External]
predCons [in BA.Automata]
prod [in BA.Automata]
prodLists [in BA.BasicDefinitions]
prod_F [in BA.Automata]
prod_pred [in BA.Automata]
prod_delta [in BA.Automata]
pure [in BA.BasicDefinitions]

## R

reach [in BA.Automata]
reachable_with [in BA.Automata]
rem [in BA.External]
rep [in BA.External]

## S

step_consistent [in BA.FinTypes]
step_reach [in BA.Automata]
subtype [in BA.BasicDefinitions]
success2 [in BA.FinTypes]
success3 [in BA.FinTypes]
surjective [in BA.BasicDefinitions]

## T

toBool [in BA.BasicDefinitions]
toDFA [in BA.Automata]
toDFA_delta [in BA.Automata]
toDFA_F [in BA.Automata]
toeqType [in BA.BasicDefinitions]
tofinType [in BA.FinTypes]
toNFA [in BA.Automata]
toOptionList [in BA.BasicDefinitions]
toProp [in BA.Automata]
toSigTList [in BA.FinTypes]
toSubList [in BA.FinTypes]
toSumList1 [in BA.BasicDefinitions]
toSumList2 [in BA.BasicDefinitions]

## U

U [in BA.Automata]
undup [in BA.External]

## V

vector [in BA.FinTypes]
vectorise [in BA.FinTypes]

## W

word [in BA.Automata]

# Record Index

## D

decPred [in BA.External]
decRel [in BA.External]
dfa [in BA.Automata]

## E

eqType [in BA.External]

## F

finType [in BA.FinTypes]
finTypeC [in BA.FinTypes]

## N

nfa [in BA.Automata]

 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (610 entries) Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (16 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 _ other (27 entries) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (315 entries) Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries) Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries) Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (18 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 _ other (18 entries) Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68 entries) Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (122 entries) Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7 entries)
Generated by coqdoc and Tebbi's js postprocessing