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]Library Index
A
AutomataB
BasicDefinitionsE
ExternalF
FinTypesLemma 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) |