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

(1373 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

(47 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

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

(99 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

(15 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

(663 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

(20 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 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

(5 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

(27 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

(61 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

(111 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

(311 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

(9 entries)

---

Global Index

A

accept [definition, in BA.Automata]
accepting [definition, in OAut.Buechi]
accepting_run_for_W' [lemma, in OAut.Complement]
accept_dec [instance, in BA.Automata]
accessible [definition, in OAut.DecLanguageEmpty]
acc_dec [instance, in BA.Automata]
adjacent_paths_agree [lemma, in OAut.NFAs]
admissible [definition, in BA.FinTypes]
AllAutomaton [section, in OAut.fin_languages]
allSub [lemma, in BA.FinTypes]
all_Le_K_length_all_le_k [lemma, in OAut.Utils]
all_Le_K [definition, in OAut.Utils]
all_le_k [definition, in OAut.Utils]
all_aut_accepts_everything [lemma, in OAut.fin_languages]
all_aut [definition, in OAut.fin_languages]
all_transition_dec [lemma, in OAut.fin_languages]
all_state_initial_dec [lemma, in OAut.fin_languages]
all_state_final_dec [lemma, in OAut.fin_languages]
all_transition [definition, in OAut.fin_languages]
all_state_initial [definition, in OAut.fin_languages]
all_state_final [definition, in OAut.fin_languages]
all_state [definition, in OAut.fin_languages]
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]
autC [definition, in OAut.Complement]
autC_disjoint [lemma, in OAut.Complement]
autI [definition, in OAut.Buechi]
autI_incl_aut2 [lemma, in OAut.Buechi]
autI_incl_aut1 [lemma, in OAut.Buechi]
Automata [library]
autU [definition, in OAut.Buechi]
autU_accepted_by_aut2 [lemma, in OAut.Buechi]
autU_accepted_by_aut1 [lemma, in OAut.Buechi]
aut_accepted_by_trim [lemma, in OAut.DecLanguageEmpty]
aut_is_w_omega [lemma, in OAut.NFAConstructions]
aut_accepts_w_omega [lemma, in OAut.NFAConstructions]
aut_accepts_norm_aut [lemma, in OAut.NFAConstructions]
aut1_inter_aut2_incl_autI [lemma, in OAut.Buechi]
aut1_incl_autU [lemma, in OAut.Buechi]
aut2_incl_autU [lemma, in OAut.Buechi]

B

BasicDefinitions [library]
BasicDefs [library]
begin_in [definition, in OAut.SeqOperations]
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]
BoundedPath [definition, in OAut.NFAs]
BoundedString [definition, in OAut.NFAs]
bounded_unchanged [lemma, in OAut.Utils]
bounded_exist [lemma, in OAut.Utils]
bounded_type_exist [lemma, in OAut.Utils]
bounded_path_to_path [lemma, in OAut.NFAs]
bounded_string_is_valid_path [lemma, in OAut.NFAs]
bounded_run_is_valid_path [lemma, in OAut.NFAs]
bound_path_unchanged [lemma, in OAut.Complement]
Buechi [library]
BuechiAut [definition, in OAut.Buechi]
BuechiExample [module, in OAut.Buechi]
BuechiExample.ab_omega_incl_aut [lemma, in OAut.Buechi]
BuechiExample.ab_omega [definition, in OAut.Buechi]
BuechiExample.alphabet [definition, in OAut.Buechi]
BuechiExample.aut [definition, in OAut.Buechi]
BuechiExample.aut_incl_ab_omega [lemma, in OAut.Buechi]
BuechiExample.dec_final_state [lemma, in OAut.Buechi]
BuechiExample.dec_initial_state [lemma, in OAut.Buechi]
BuechiExample.dec_transition [lemma, in OAut.Buechi]
BuechiExample.final_state [definition, in OAut.Buechi]
BuechiExample.initial_state [definition, in OAut.Buechi]
BuechiExample.state [definition, in OAut.Buechi]
BuechiExample.transition [definition, in OAut.Buechi]
a [notation, in OAut.Buechi]
b [notation, in OAut.Buechi]
S1 [notation, in OAut.Buechi]
S2 [notation, in OAut.Buechi]
BuechiLanguage [section, in OAut.Buechi]
BuechiLanguage.A [variable, in OAut.Buechi]

C

can_find_duplicate [lemma, in OAut.Utils]
can_find_next_position [lemma, in OAut.SeqOperations]
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_finType_Le_K [lemma, in OAut.Utils]
card_finTypeC_Le_K [lemma, in OAut.Utils]
card_length_leq [lemma, in BA.BasicDefinitions]
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_upper_bound [lemma, in BA.FinTypes]
Card_positiv [lemma, in BA.FinTypes]
Card_X_eq [definition, in BA.FinTypes]
cc_nat [lemma, in OAut.Utils]
class [projection, in BA.FinTypes]
classifier [definition, in OAut.Complement]
closed_intersection [lemma, in OAut.Buechi]
Closed_Intersection.aut2 [variable, in OAut.Buechi]
Closed_Intersection.aut1 [variable, in OAut.Buechi]
Closed_Intersection [section, in OAut.Buechi]
closed_union [lemma, in OAut.Buechi]
Closed_Union.aut2 [variable, in OAut.Buechi]
Closed_Union.aut1 [variable, in OAut.Buechi]
Closed_Union [section, in OAut.Buechi]
Closure [lemma, in BA.FinTypes]
ClosureProperties [section, in OAut.fin_languages]
Closure_FCIter [lemma, in BA.FinTypes]
combine_final_transforms_right [lemma, in OAut.Complement]
combine_final_transforms_left [lemma, in OAut.Complement]
combine_transforms [lemma, in OAut.Complement]
common_merge_index [lemma, in OAut.Complement]
compatibility [lemma, in OAut.Complement]
compatibilityComplement [lemma, in OAut.Complement]
compatibility2 [lemma, in OAut.Complement]
complement [definition, in BA.Automata]
complement [definition, in OAut.Complement]
Complement [library]
ComplementCorollaries [section, in OAut.Complement]
complement_correct [lemma, in BA.Automata]
complement_correct2 [lemma, in OAut.Complement]
complement_correct [lemma, in OAut.Complement]
complement_complete [lemma, in OAut.Complement]
complement_auts [definition, in OAut.Complement]
complete_induction [lemma, in OAut.BasicDefs]
compose_s_monotone [lemma, in OAut.StrictlyMonotoneSeqs]
compute_run_final_transforms [lemma, in OAut.Complement]
compute_run_transforms [lemma, in OAut.Complement]
compute_run [lemma, in OAut.NFAConstructions]
conact_delta_dec [instance, in BA.Automata]
concat [definition, in BA.Automata]
ConcatInfPrependNFA [section, in OAut.NFAConstructions]
ConcatInfPrependNFA.runs [variable, in OAut.NFAConstructions]
ConcatInfPrependNFA.strings [variable, in OAut.NFAConstructions]
concat_paths [lemma, in OAut.NFAs]
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]
concat_inf_index_equal [lemma, in OAut.SeqOperations]
concat_inf_correct [lemma, in OAut.SeqOperations]
concat_inf_index_to_begin [lemma, in OAut.SeqOperations]
concat_inf_index_injective [lemma, in OAut.SeqOperations]
concat_inf_index_le [lemma, in OAut.SeqOperations]
concat_inf_index_step_correct [lemma, in OAut.SeqOperations]
concat_inf_index_in_bounds [lemma, in OAut.SeqOperations]
concat_inf_index_correct [lemma, in OAut.SeqOperations]
concat_inf_index_begin [lemma, in OAut.SeqOperations]
concat_inf_index_in_string [lemma, in OAut.SeqOperations]
concat_inf [definition, in OAut.SeqOperations]
concat_inf_indices [definition, in OAut.SeqOperations]
concat_extract [lemma, in OAut.Seqs]
concat_strings [definition, in OAut.Seqs]
concat_inf_final_step [lemma, in OAut.NFAConstructions]
concat_inf_is_final_not_constructive [lemma, in OAut.NFAConstructions]
concat_inf_is_valid [lemma, in OAut.NFAConstructions]
concat_map_length [lemma, in BA.FinTypes]
congruence [definition, in OAut.Complement]
connected [definition, in OAut.NFAs]
cons [definition, in BA.Automata]
consAppend [lemma, in BA.BasicDefinitions]
cons_incll [lemma, in BA.BasicDefinitions]
cons_correct [lemma, in BA.Automata]
cons_equi_proper [instance, in BA.External]
cons_incl_proper [instance, in BA.External]
ConvertFinTypeToSeq [section, in OAut.Utils]
convertFromNFA [lemma, in OAut.fin_languages]
convertoToNFA [lemma, in OAut.fin_languages]
ConvertToNFA [section, in OAut.fin_languages]
ConvertToNFA.aut [variable, in OAut.fin_languages]
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]
create_Le_K [lemma, in OAut.Utils]
cut [definition, in OAut.Seqs]
cut_rest_correct [lemma, in OAut.Seqs]
cut_front_correct [lemma, in OAut.Seqs]
cyclic [definition, in OAut.NFAs]
cyclic_path_connects [lemma, in OAut.NFAs]
cyclic_path_connects_on_path [lemma, in OAut.NFAs]
cyclic_path [definition, in OAut.NFAs]

D

dec [definition, in BA.External]
DecConnected [section, in OAut.NFAs]
decFinEquivRel_RamseyImpliesFinEquivClasses [lemma, in OAut.Buechi]
decFinEquivRel_FiniteTypeSeqImpliesFinEquivClasses [lemma, in OAut.Buechi]
decide_rel [projection, in BA.External]
decide_pred [projection, in BA.External]
decide_eq [projection, in BA.External]
decision [definition, in BA.External]
decision_false [lemma, in OAut.BasicDefs]
decision_true [lemma, in OAut.BasicDefs]
DecLanguageEmpty [library]
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_pure_le_k_public [instance, in OAut.Utils]
dec_pure_le_k [instance, in OAut.Utils]
dec_le_k [instance, in OAut.Utils]
dec_saccepting [instance, in OAut.NFAs]
dec_sfinal [instance, in OAut.NFAs]
dec_sinitial [instance, in OAut.NFAs]
dec_svalid [instance, in OAut.NFAs]
dec_connected_public [instance, in OAut.NFAs]
dec_valid_path_public [instance, in OAut.NFAs]
dec_connected [lemma, in OAut.NFAs]
dec_bounded_path [lemma, in OAut.NFAs]
dec_valid_path [instance, in OAut.NFAs]
dec_language_empty [lemma, in OAut.DecLanguageEmpty]
dec_language_empty_informative [lemma, in OAut.DecLanguageEmpty]
dec_trim_states_empty [instance, in OAut.DecLanguageEmpty]
dec_trim_final [lemma, in OAut.DecLanguageEmpty]
dec_trim_initial [lemma, in OAut.DecLanguageEmpty]
dec_trim_transition [lemma, in OAut.DecLanguageEmpty]
dec_state_trim [lemma, in OAut.DecLanguageEmpty]
dec_final_coaccessible [instance, in OAut.DecLanguageEmpty]
dec_final_cyclic [instance, in OAut.DecLanguageEmpty]
dec_finite_accessible [instance, in OAut.DecLanguageEmpty]
dec_union_final [lemma, in OAut.Buechi]
dec_union_initial [lemma, in OAut.Buechi]
dec_union_transition [lemma, in OAut.Buechi]
dec_no_transition [instance, in OAut.Buechi]
dec_no_state [instance, in OAut.Buechi]
dec_language_eq [lemma, in OAut.Complement]
dec_language_inclusion [lemma, in OAut.Complement]
dec_language_universal [lemma, in OAut.Complement]
dec_VW_part_of_complement [instance, in OAut.Complement]
dec_merge_at_next [instance, in OAut.Complement]
dec_merge_at [instance, in OAut.Complement]
dec_pure_W_final [instance, in OAut.Complement]
dec_tilde_eq_class [instance, in OAut.Complement]
dec_transforms_final [instance, in OAut.Complement]
dec_transforms [instance, in OAut.Complement]
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]
dec_strict_bounded_nat_forall [instance, in OAut.Seqs]
dec_bounded_nat_forall [instance, in OAut.Seqs]
dec_vw_state_initial [instance, in OAut.NFAConstructions]
dec_vw_state_final [instance, in OAut.NFAConstructions]
dec_vw_transition [instance, in OAut.NFAConstructions]
dec_Womega_state_initial [instance, in OAut.NFAConstructions]
dec_Womega_state_final [instance, in OAut.NFAConstructions]
dec_Womega_transition [instance, in OAut.NFAConstructions]
dec_norm_transition [instance, in OAut.NFAConstructions]
dec_norm_final_state [instance, in OAut.NFAConstructions]
dec_norm_initial_state [instance, in OAut.NFAConstructions]
dec_visits_final [instance, in OAut.NFAConstructions]
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]
detlaQstar_convert_inverse [lemma, in OAut.fin_languages]
detlaQstar_convert [lemma, in OAut.fin_languages]
detlaQstar_decrease_step [lemma, in OAut.fin_languages]
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]
drop [definition, in OAut.Seqs]
drop_string_end [definition, in OAut.Seqs]
drop_string_begin [definition, in OAut.Seqs]
drop_preserves_finite [lemma, in OAut.Seqs]
drop_correct [lemma, in OAut.Seqs]
dummy [lemma, in OAut.Utils]
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]
dup_free_all_Le_K [lemma, in OAut.Utils]
dup_free_all_le_k [lemma, in OAut.Utils]

E

econcat [definition, in OAut.Complement]
elem [definition, in BA.FinTypes]
elementIn [lemma, in BA.FinTypes]
empty [definition, in BA.Automata]
EmptyAut [section, in OAut.Buechi]
Empty_set_eq_dec [instance, in BA.BasicDefinitions]
empty_reach [lemma, in BA.Automata]
empty_dec [instance, in BA.Automata]
empty_aut_correct [lemma, in OAut.Buechi]
empty_aut [definition, in OAut.Buechi]
empty_state [definition, in OAut.Buechi]
Empty_set_enum_ok [lemma, in BA.FinTypes]
empty_language [definition, in OAut.BasicDefs]
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]
EqLe_K [definition, in OAut.Utils]
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]
equalSELangImpliesEqualSLang [lemma, in OAut.Complement]
Equi [section, in BA.External]
equi [definition, in BA.External]
EquivalenceClassIndex [definition, in OAut.Complement]
equivalence_class_closed [lemma, in OAut.Complement]
Equivalence_property_exists' [lemma, in BA.FinTypes]
Equivalence_property_exists [lemma, in BA.FinTypes]
Equivalence_property_all [lemma, in BA.FinTypes]
equivalent_drop [lemma, in OAut.Complement]
equivalent_if_same_equivalence_class [lemma, in OAut.Complement]
equivalent_in_equivalence_class [lemma, in OAut.Complement]
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]
EqWaitFinal [definition, in OAut.Buechi]
eq_dec_sigT [instance, in BA.BasicDefinitions]
eq_funTrans [lemma, in BA.BasicDefinitions]
eq_classes_extensional [lemma, in OAut.Complement]
eq_iff [lemma, in BA.FinTypes]
EString [definition, in OAut.Complement]
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]
extensional_o_iter2_implies_iter1 [lemma, in OAut.SeqOperations]
External [library]
extPow_length [lemma, in BA.FinTypes]
extract [definition, in OAut.Seqs]
extract_from_drop [lemma, in OAut.Seqs]
extract_correct [lemma, in OAut.Seqs]

F

F [projection, in BA.Automata]
False_eq_dec [instance, in BA.BasicDefinitions]
False_dec [instance, in BA.External]
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]
Final [constructor, in OAut.Buechi]
final [definition, in OAut.Buechi]
FinalCycle [section, in OAut.DecLanguageEmpty]
finalW_does_not_appear_in_valid_run [lemma, in OAut.NFAConstructions]
final_dec_public [instance, in OAut.NFAs]
final_state_dec [projection, in OAut.NFAs]
final_state [projection, in OAut.NFAs]
final_coaccessible_iff_final_cycle [lemma, in OAut.DecLanguageEmpty]
final_valid_run_has_cycle [lemma, in OAut.DecLanguageEmpty]
final_cyclic_to_connected [lemma, in OAut.DecLanguageEmpty]
final_cyclic [definition, in OAut.DecLanguageEmpty]
final_cycle [definition, in OAut.DecLanguageEmpty]
final_coaccessible [definition, in OAut.DecLanguageEmpty]
final_state_intersection_is_final_state_aut2 [lemma, in OAut.Buechi]
final_extensional [lemma, in OAut.Buechi]
final_prepend [lemma, in OAut.Buechi]
final_drop [lemma, in OAut.Buechi]
final_r' [lemma, in OAut.Complement]
final_transforms_extensional [lemma, in OAut.Complement]
final_transform_implies_transform [lemma, in OAut.Complement]
final_concat_inf_infinite_final_strings [lemma, in OAut.NFAConstructions]
FindNextPosition [section, in OAut.SeqOperations]
FindNextPosition.decP [variable, in OAut.SeqOperations]
FindNextPosition.P [variable, in OAut.SeqOperations]
FindNextPosition.w [variable, in OAut.SeqOperations]
fInduction [lemma, in BA.FinTypes]
find_final_aut1_correct [lemma, in OAut.Buechi]
find_final_aut1_less [lemma, in OAut.Buechi]
find_final_aut1 [definition, in OAut.Buechi]
find_next_position_correct [lemma, in OAut.SeqOperations]
find_next_position [definition, in OAut.SeqOperations]
finEquivClassesImpliesFiniteTypeSeq [lemma, in OAut.Buechi]
FiniteClosureIteration [section, in BA.FinTypes]
FiniteClosureIteration.step [variable, in BA.FinTypes]
FiniteClosureIteration.step_dec [variable, in BA.FinTypes]
FiniteClosureIteration.X [variable, in BA.FinTypes]
FiniteEquivClasses [definition, in OAut.Buechi]
finiteIndex [definition, in OAut.Buechi]
finiteIndexImpliesFiniteIndexNeg [lemma, in OAut.Buechi]
finiteIndexNeg [definition, in OAut.Buechi]
finiteIndexNegAndXMImpliesFiniteIndex [lemma, in OAut.Buechi]
FiniteTypeSeq [definition, in OAut.Buechi]
finite_type_predicate_seq [lemma, in OAut.Buechi]
finite_equiv_classes [axiom, in OAut.Buechi]
finite_type_seq [axiom, in OAut.Buechi]
finite_prefix_preserves_infinite [lemma, in OAut.Seqs]
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_Le_K [instance, in OAut.Utils]
finTypeC_WaitFinal [instance, in OAut.Buechi]
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]
finTypeEqEquiv [lemma, in OAut.Buechi]
finTypeEqFiniteIndex [lemma, in OAut.Buechi]
finTypeEqRelXM [lemma, in OAut.Buechi]
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_Le_K [definition, in OAut.Utils]
finType_WaitFinal [definition, in OAut.Buechi]
finType_cc_sigma [lemma, in OAut.Complement]
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]
fin_languages [library]
first [definition, in OAut.Utils]
First [section, in OAut.Utils]
FirstKFinType [section, in OAut.Utils]
FirstKFinType.DeclareFinType [section, in OAut.Utils]
FirstKFinType.DeclareFinType.k [variable, in OAut.Utils]
first_norm_is_initial [lemma, in OAut.NFAConstructions]
First.p [variable, in OAut.Utils]
First.p_dec [variable, in OAut.Utils]
Fixedpoints [section, in BA.FinTypes]
Fixedpoints.f [variable, in BA.FinTypes]
Fixedpoints.X [variable, in BA.FinTypes]
fix_first_zero_s_monotone [lemma, in OAut.StrictlyMonotoneSeqs]
fix_first_zero [definition, in OAut.StrictlyMonotoneSeqs]
found_pos [constructor, in OAut.SeqOperations]
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]
ge_to_le [lemma, in OAut.SeqOperations]

H

Hedberg [lemma, in BA.BasicDefinitions]
HelpApply [lemma, in BA.FinTypes]
HistoryFilter [section, in OAut.SeqOperations]
HistoryFilter.baseP [variable, in OAut.SeqOperations]
HistoryFilter.decP [variable, in OAut.SeqOperations]
HistoryFilter.extP [variable, in OAut.SeqOperations]
HistoryFilter.P [variable, in OAut.SeqOperations]
HistoryFilter.stepP [variable, in OAut.SeqOperations]
HistoryFilter.w [variable, in OAut.SeqOperations]
history_filter_correct [lemma, in OAut.SeqOperations]
history_filter_proof_only_append [lemma, in OAut.SeqOperations]
history_filter_proof_only_append_step [lemma, in OAut.SeqOperations]
history_filter_zero [lemma, in OAut.SeqOperations]
history_filter_s_monotone [lemma, in OAut.SeqOperations]
history_filter [definition, in OAut.SeqOperations]
history_filter_proof [definition, in OAut.SeqOperations]
history_filter_step [lemma, in OAut.SeqOperations]
history_filter_base [lemma, in OAut.SeqOperations]

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]
infinite [definition, in OAut.Seqs]
Infinite [section, in OAut.Seqs]
InfiniteConcat [section, in OAut.SeqOperations]
InfiniteFilter [section, in OAut.SeqOperations]
InfiniteFilter.decP [variable, in OAut.SeqOperations]
InfiniteFilter.infP [variable, in OAut.SeqOperations]
InfiniteFilter.P [variable, in OAut.SeqOperations]
InfiniteFilter.w [variable, in OAut.SeqOperations]
infinite_final_is_accepting_for_finite_automaton [lemma, in OAut.Buechi]
infinite_equiv_indices_merging [lemma, in OAut.Complement]
infinite_equiv_indices_equiv_begin [lemma, in OAut.Complement]
infinite_equiv_indices [lemma, in OAut.Complement]
infinite_final_strings_R [lemma, in OAut.Complement]
infinite_filter_zero [lemma, in OAut.SeqOperations]
infinite_filter_all [lemma, in OAut.SeqOperations]
infinite_filter_correct [lemma, in OAut.SeqOperations]
infinite_filter_s_monotone [lemma, in OAut.SeqOperations]
infinite_filter [definition, in OAut.SeqOperations]
inImages [lemma, in BA.FinTypes]
initial [definition, in OAut.Buechi]
initialW_always_final [lemma, in OAut.NFAConstructions]
initialW_partitions_in_W [lemma, in OAut.NFAConstructions]
initial_dec_public [instance, in OAut.NFAs]
initial_state_dec [projection, in OAut.NFAs]
initial_state [projection, in OAut.NFAs]
initial_r' [lemma, in OAut.Complement]
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 [definition, in OAut.Buechi]
intersectionRunStaysWait1UntilNextFinalAut1 [lemma, in OAut.Buechi]
intersectionRunStaysWait2UntilNextFinalAut2 [lemma, in OAut.Buechi]
intersectionRunSwitchtesFromWait1ToWait2 [lemma, in OAut.Buechi]
intersectionRunSwitchtesFromWait2ToFinal [lemma, in OAut.Buechi]
intersection_run_is_valid [lemma, in OAut.Buechi]
intersection_run_does_not_change_states [lemma, in OAut.Buechi]
intersection_run [definition, in OAut.Buechi]
intersection_final_dec [lemma, in OAut.Buechi]
intersection_initial_dec [lemma, in OAut.Buechi]
intersection_transition_dec [lemma, in OAut.Buechi]
intersection_final [definition, in OAut.Buechi]
intersection_initial [definition, in OAut.Buechi]
intersection_transition [definition, in OAut.Buechi]
intersection_state [definition, in OAut.Buechi]
intersect_correct [lemma, in BA.Automata]
intersect_correct [lemma, in OAut.Buechi]
in_all_Le_K_ifLess [lemma, in OAut.Utils]
in_all_Le_K_if2 [lemma, in OAut.Utils]
in_all_Le_K_if [lemma, in OAut.Utils]
in_all_le_k_iff [lemma, in OAut.Utils]
in_lang [abbreviation, in BA.Automata]
in_lang [abbreviation, 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]

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

language [definition, in OAut.Buechi]
Language [definition, in OAut.BasicDefs]
LanguageLemmata [section, in OAut.BasicDefs]
LanguageLemmata.L [variable, in OAut.BasicDefs]
LanguageLemmata.L_2 [variable, in OAut.BasicDefs]
LanguageLemmata.L_1 [variable, in OAut.BasicDefs]
LanguageLemmata.X [variable, in OAut.BasicDefs]
Languages [section, in OAut.BasicDefs]
Languages.X [variable, in OAut.BasicDefs]
language_intersection_comm [lemma, in OAut.BasicDefs]
language_union_comm [lemma, in OAut.BasicDefs]
language_eq_symmetric [lemma, in OAut.BasicDefs]
language_eq_iff [lemma, in OAut.BasicDefs]
language_universal_iff [lemma, in OAut.BasicDefs]
language_empty_iff [lemma, in OAut.BasicDefs]
language_difference [definition, in OAut.BasicDefs]
language_complement [definition, in OAut.BasicDefs]
language_intersection [definition, in OAut.BasicDefs]
language_union [definition, in OAut.BasicDefs]
language_eq [definition, in OAut.BasicDefs]
language_inclusion [definition, in OAut.BasicDefs]
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]
lang_prepend [definition, in OAut.SeqOperations]
lang_o_iter2 [definition, in OAut.SeqOperations]
lang_o_iter [definition, in OAut.SeqOperations]
lastindex [projection, in OAut.Seqs]
last_norm_is_final [lemma, in OAut.NFAConstructions]
least_fp_containing [definition, in BA.FinTypes]
lengthEq [lemma, in BA.BasicDefinitions]
leq_to_distance [lemma, in OAut.Buechi]
leq_0 [lemma, in OAut.Complement]
Le_K_enum_ok [lemma, in OAut.Utils]
LE_K_eq_dec [instance, in OAut.Utils]
Le_K [definition, in OAut.Utils]
le_k [definition, in OAut.Utils]
list_eq [lemma, in OAut.Utils]
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

M [definition, in OAut.NFAs]
m [definition, in OAut.NFAs]
many_aut_union [lemma, in OAut.Buechi]
many_aut_intersection [lemma, in OAut.fin_languages]
max_of_nat_string_correct [lemma, in OAut.Utils]
max_of_nat_string [definition, in OAut.Utils]
max_le_right [lemma, in OAut.BasicDefs]
max_le_left [lemma, in OAut.BasicDefs]
mC [definition, in BA.FinTypes]
Membership [section, in BA.External]
Membership.X [variable, in BA.External]
merge_at_next_append [lemma, in OAut.Complement]
merge_at_next_extensional [lemma, in OAut.Complement]
merge_at_next [definition, in OAut.Complement]
minimize_path_correct [lemma, in OAut.NFAs]
minimize_path [definition, in OAut.NFAs]
mknfa [constructor, in OAut.NFAs]
mkstring [constructor, in OAut.Seqs]
mmC [definition, in BA.FinTypes]
MyhillNerode [definition, in OAut.Complement]

N

nat_pair_le_not_equal [lemma, in OAut.SeqOperations]
nat_pair_le [definition, in OAut.SeqOperations]
nat_le_dec [instance, in BA.External]
nat_eq_dec [instance, in BA.External]
NecessaryAssumptions [section, in OAut.Buechi]
negOr [lemma, in BA.BasicDefinitions]
neg_F [definition, in BA.Automata]
NFA [record, in OAut.NFAs]
nfa [record, in BA.Automata]
NFA [constructor, in BA.Automata]
NFAConstructions [library]
NFAs [library]
NFAStringLanguage [section, in OAut.NFAs]
nil_kleene [lemma, in BA.Automata]
NoneElement [lemma, in BA.FinTypes]
non_empty_cycle_is_valid [lemma, in OAut.NFAs]
NormalizeNFA [section, in OAut.NFAConstructions]
NormalizeNFA.aut [variable, in OAut.NFAConstructions]
Final [notation, in OAut.NFAConstructions]
Initial [notation, in OAut.NFAConstructions]
normalize_aut [lemma, in OAut.NFAConstructions]
norm_aut_accepts_aut [lemma, in OAut.NFAConstructions]
norm_aut [definition, in OAut.NFAConstructions]
norm_transition [definition, in OAut.NFAConstructions]
norm_final_state [definition, in OAut.NFAConstructions]
norm_initial_state [definition, in OAut.NFAConstructions]
norm_state [definition, in OAut.NFAConstructions]
notInMapCons [lemma, in BA.FinTypes]
notInZero [lemma, in BA.BasicDefinitions]
not_part_of_complement_implies_aut [lemma, in OAut.Complement]
not_tilde_w_extend [lemma, in OAut.Complement]
not_in_cons [lemma, in BA.External]
not_dec [instance, in BA.External]
no_transition [definition, in OAut.Buechi]
no_state [definition, in OAut.Buechi]
NullMul [lemma, in BA.BasicDefinitions]
n_accept [definition, in BA.Automata]

O

OmegaIteration [section, in OAut.SeqOperations]
OmegaIteration.l [variable, in OAut.SeqOperations]
omega_iteration_infinite [lemma, in OAut.SeqOperations]
omega_iteration [definition, in OAut.SeqOperations]
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]
orig_state [definition, in OAut.DecLanguageEmpty]
or_dec [instance, in BA.External]
other_norm_is_aut_state [lemma, in OAut.NFAConstructions]
o_iter_implies_o_iter2 [lemma, in OAut.SeqOperations]

P

partition_run_on_concat_inf [lemma, in OAut.NFAConstructions]
partition_run_on_prepend_string [lemma, in OAut.NFAConstructions]
part_of_complement_implies_complement [lemma, in OAut.Complement]
path [definition, in OAut.NFAs]
path_length_bounded [lemma, in OAut.NFAs]
path_extensional [lemma, in OAut.NFAs]
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]
pos_step [constructor, in OAut.SeqOperations]
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]
prepend [definition, in OAut.Seqs]
PrependFinLanguage_Automata.normW [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.initialW [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.autW [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.normV [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.finalV [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.initialV [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata.autV [variable, in OAut.NFAConstructions]
PrependFinLanguage_Automata [section, in OAut.NFAConstructions]
prepending_path_on_path_is_valid [lemma, in OAut.NFAs]
prepending_path_is_valid [lemma, in OAut.NFAs]
prepend_valid_path [lemma, in OAut.NFAs]
prepend_valid_run [lemma, in OAut.NFAs]
prepend_on_omega_iteration [lemma, in OAut.SeqOperations]
prepend_path_rest_correct2 [lemma, in OAut.Seqs]
prepend_path_rest_correct [lemma, in OAut.Seqs]
prepend_path_first [lemma, in OAut.Seqs]
prepend_path_begin_correct [lemma, in OAut.Seqs]
prepend_rest_correct2 [lemma, in OAut.Seqs]
prepend_rest_correct [lemma, in OAut.Seqs]
prepend_first_correct [lemma, in OAut.Seqs]
prepend_path [definition, in OAut.Seqs]
prepend_string_is_valid [lemma, in OAut.NFAConstructions]
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_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]
Prod_Card [lemma, in BA.FinTypes]
prod_enum_ok [lemma, in BA.FinTypes]
project_second_is_valid [lemma, in OAut.Buechi]
project_first_is_valid [lemma, in OAut.Buechi]
project_second [definition, in OAut.Buechi]
project_first [definition, in OAut.Buechi]
proj1_sig_fun [lemma, in BA.BasicDefinitions]
proveOne [lemma, in BA.FinTypes]
pure [definition, in BA.BasicDefinitions]
pure_le_k_if [lemma, in OAut.Utils]
pure_eq [lemma, in BA.BasicDefinitions]
pure_impure [lemma, in BA.BasicDefinitions]
pure_equiv [lemma, in BA.BasicDefinitions]
pure_W_final [definition, in OAut.Complement]
purify [lemma, in BA.BasicDefinitions]

Q

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

R

Ramsey [definition, in OAut.Buechi]
ramseyImpliesFiniteTypeSeq [lemma, in OAut.Buechi]
ramseyTotality [lemma, in OAut.Complement]
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]
rec_find_next_position [inductive, in OAut.SeqOperations]
refines [definition, in OAut.Complement]
refl [constructor, in BA.Automata]
relation [projection, in BA.External]
rel_XM [definition, in OAut.Buechi]
rem [definition, in BA.External]
Removal [section, in BA.External]
Removal.X [variable, in BA.External]
remove_circle_preserves_last_state [lemma, in OAut.NFAs]
remove_circle_preserves_first_state [lemma, in OAut.NFAs]
remove_circle_decrease [lemma, in OAut.NFAs]
remove_circle_correct [lemma, in OAut.NFAs]
remove_circle [definition, in OAut.NFAs]
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]
revert_concat_second [lemma, in OAut.Seqs]
revert_concat_first [lemma, in OAut.Seqs]
revert_drop_path [lemma, in OAut.Seqs]
revert_prepend_path [lemma, in OAut.Seqs]
rightResult [lemma, in BA.FinTypes]
right_congruent [definition, in OAut.Complement]
Run [definition, in OAut.NFAs]
r' [definition, in OAut.Complement]
R' [definition, in OAut.Complement]
R'k0_eq_Rk0 [lemma, in OAut.Complement]

S

s [projection, in BA.Automata]
S [projection, in BA.Automata]
saccepting [definition, in OAut.NFAs]
safe [inductive, in OAut.Utils]
safeB [constructor, in OAut.Utils]
safeS [constructor, in OAut.Utils]
safe_dclosed [lemma, in OAut.Utils]
sautomaton_normalized [definition, in OAut.NFAConstructions]
sclosure_complement [lemma, in OAut.fin_languages]
sclosure_diff [lemma, in OAut.fin_languages]
sclosure_intersection [lemma, in OAut.fin_languages]
sclosure_union [lemma, in OAut.fin_languages]
scomplement [definition, in OAut.fin_languages]
scomplement_correct [lemma, in OAut.fin_languages]
sdiff [definition, in OAut.fin_languages]
sdiff_correct [lemma, in OAut.fin_languages]
seaccepting [definition, in OAut.Complement]
selanguage [definition, in OAut.Complement]
seq [projection, in OAut.Seqs]
Seq [definition, in OAut.Seqs]
SeqLang [definition, in OAut.Seqs]
SeqOperations [section, in OAut.Seqs]
SeqOperations [library]
Seqs [library]
seqToList [definition, in OAut.fin_languages]
seqToListCorrect [lemma, in OAut.fin_languages]
seq_in_empty_aut_contradicts [lemma, in OAut.Buechi]
seq_prop_dec_exists_bounded [lemma, in OAut.Seqs]
seq_dec_exists_bounded [instance, in OAut.Seqs]
seq_equal [definition, in OAut.Seqs]
seq_map [definition, in OAut.Seqs]
sfinal [definition, in OAut.NFAs]
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]
sinitial [definition, in OAut.NFAs]
sintersect [definition, in OAut.fin_languages]
sintersect_correct [lemma, in OAut.fin_languages]
size_induction [lemma, in BA.External]
slanguage [definition, in OAut.NFAs]
slanguage_extensional [lemma, in OAut.NFAs]
sNFA_sNFA_to_omega_Buechi [lemma, in OAut.NFAConstructions]
SomeElement [lemma, in BA.FinTypes]
special_states [definition, in OAut.NFAConstructions]
split_path [lemma, in OAut.NFAs]
split_final_transforms [lemma, in OAut.Complement]
split_transforms [lemma, in OAut.Complement]
state [projection, in OAut.NFAs]
stateAfterFinalIsWait1 [lemma, in OAut.Buechi]
stateBeforeFinalIsWait2 [lemma, in OAut.Buechi]
states_trim_subtype [lemma, in OAut.DecLanguageEmpty]
states_in_final_path_are_trim [lemma, in OAut.DecLanguageEmpty]
states_do_not_mix [lemma, in OAut.Buechi]
state_trim [definition, in OAut.DecLanguageEmpty]
step [constructor, in BA.Automata]
step_reach_consistent [lemma, in BA.Automata]
step_reach [definition, 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]
Streicher_K [lemma, in BA.BasicDefinitions]
StrictlyMonotoneSeqs [section, in OAut.StrictlyMonotoneSeqs]
StrictlyMonotoneSeqs [library]
strict_bounded_exist [lemma, in OAut.Utils]
String [record, in OAut.Seqs]
StringLang [definition, in OAut.Seqs]
StringLang_Extensional [definition, in OAut.Seqs]
StringOperations [section, in OAut.Seqs]
StringsEq [section, in OAut.Seqs]
strings_equal [definition, in OAut.Seqs]
stringToList [definition, in OAut.fin_languages]
stringToListCorrect [lemma, in OAut.fin_languages]
stringToList_Size [lemma, in OAut.fin_languages]
string_valid [definition, in OAut.NFAs]
string_final_R' [lemma, in OAut.Complement]
string_equal_symmetric [lemma, in OAut.Seqs]
string_equal_reflexive [lemma, in OAut.Seqs]
substring [definition, in OAut.SeqOperations]
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]
sunion [definition, in OAut.fin_languages]
sunion_correct [lemma, in OAut.fin_languages]
surjective [definition, in BA.BasicDefinitions]
surjectiveApply [lemma, in BA.BasicDefinitions]
surj_sub [lemma, in BA.FinTypes]
svalid [definition, in OAut.NFAs]
switch_from_V_to_W [lemma, in OAut.NFAConstructions]
s_monotone_drop [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_ge_zero [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_order_preserving_backwards [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_order_preserving [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_strict_order_preserving [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_ge [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_unbouded_ge [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_unbouded [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone_id [lemma, in OAut.StrictlyMonotoneSeqs]
s_monotone [definition, in OAut.StrictlyMonotoneSeqs]
s_s'_pair_aut [definition, in OAut.Complement]
s_monotone_begin_in [lemma, in OAut.SeqOperations]

T

Test [section, in BA.FinTypes]
Test.X [variable, in BA.FinTypes]
Test.Y [variable, in BA.FinTypes]
# _ [notation, in BA.FinTypes]
tff_recognizes_transforms_final [lemma, in OAut.Complement]
tff_is_transforms_final [lemma, in OAut.Complement]
tff_accepts_tranforms_final [lemma, in OAut.Complement]
tff_aut [definition, in OAut.Complement]
tff_transition_dec [lemma, in OAut.Complement]
tff_state_final_dec [lemma, in OAut.Complement]
tff_state_initial_dec [lemma, in OAut.Complement]
tff_transition [definition, in OAut.Complement]
tff_state_final [definition, in OAut.Complement]
tff_state_initial [definition, in OAut.Complement]
tff_state [definition, in OAut.Complement]
tf_recognizes_transforms [lemma, in OAut.Complement]
tf_is_transforms [lemma, in OAut.Complement]
tf_accepts_tranforms [lemma, in OAut.Complement]
tf_aut [definition, in OAut.Complement]
tf_transition_dec [lemma, in OAut.Complement]
tf_state_final_dec [lemma, in OAut.Complement]
tf_state_initial_dec [lemma, in OAut.Complement]
tf_transition [definition, in OAut.Complement]
tf_state_final [definition, in OAut.Complement]
tf_state_initial [definition, in OAut.Complement]
tf_state [definition, in OAut.Complement]
there_are_infinite_final_aut1 [lemma, in OAut.Buechi]
there_is_aut1_final_in_between [lemma, in OAut.Buechi]
there_is_bigger_merging_index [lemma, in OAut.Complement]
there_is_final_index [lemma, in OAut.Complement]
there_is_rec_find_next_position [lemma, in OAut.SeqOperations]
there_is_initialW [lemma, in OAut.NFAConstructions]
TildeEquivalenceClass [definition, in OAut.Complement]
TildeEquivalenceRelation [section, in OAut.Complement]
TildeEquivalenceRelation.Compatibility [section, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.Acc [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.agree_R [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.agree_r0 [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.Eq [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.eqLengthv [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.EqR [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.Eq' [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.i [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.j [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.ow [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.ow' [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.R [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.r [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.r0 [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.V [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.v [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.valid_R [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.valid_r0 [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.V' [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.v' [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.W [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.w [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.W' [variable, in OAut.Complement]
TildeEquivalenceRelation.Compatibility.w' [variable, in OAut.Complement]
TildeEquivalenceRelation.Complement [section, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable [section, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable [section, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable.endS [variable, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable.startS [variable, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable [section, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable.endS [variable, in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable.startS [variable, in OAut.Complement]
TildeEquivalenceRelation.TildeEquivalenceClassRecognizableMyhillNerode [section, in OAut.Complement]
TildeEquivalenceRelation.Totality [section, in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability [section, in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability.k1 [variable, in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability.k2 [variable, in OAut.Complement]
_ ~~# _ [notation, in OAut.Complement]
_ ~~@ _ at _ [notation, in OAut.Complement]
_ ~~ _ [notation, in OAut.Complement]
_ =!=> _ on _ [notation, in OAut.Complement]
_ ===> _ on _ [notation, in OAut.Complement]
{[ _ ]} [notation, in OAut.Complement]
tilde_w_equiv_finite_index [lemma, in OAut.Complement]
tilde_w_equiv_finite_index_neq [lemma, in OAut.Complement]
tilde_equiv_finite_index_neq [lemma, in OAut.Complement]
tilde_equiv_finite_index [lemma, in OAut.Complement]
tilde_w_equiv_XM [lemma, in OAut.Complement]
tilde_w_equiv_bool_infinite_false [lemma, in OAut.Complement]
tilde_w_equiv_bool_remains_true [lemma, in OAut.Complement]
tilde_w_equiv_iff [lemma, in OAut.Complement]
tilde_w_index_equiv_iff [lemma, in OAut.Complement]
tilde_w_equiv_bool [definition, in OAut.Complement]
tilde_w_equivalence [lemma, in OAut.Complement]
tilde_w_transitive [lemma, in OAut.Complement]
tilde_w_index_transitive [lemma, in OAut.Complement]
tilde_w_symmetric [lemma, in OAut.Complement]
tilde_w_index_symmetric [lemma, in OAut.Complement]
tilde_w_reflexive [lemma, in OAut.Complement]
tilde_w_index_reflexive [lemma, in OAut.Complement]
tilde_w_extend [lemma, in OAut.Complement]
tilde_w_equiv [definition, in OAut.Complement]
tilde_equiv_class_NFA_recognizable [lemma, in OAut.Complement]
tilde_equiv_class_aut_is_equiv_class [lemma, in OAut.Complement]
tilde_equiv_class_aut_accepts_Equiv_class [lemma, in OAut.Complement]
tilde_equiv_class_aut [definition, in OAut.Complement]
tilde_equiv_class_NFA_recognizable_MyhillNerode [lemma, in OAut.Complement]
tilde_eq_class_congruence [lemma, in OAut.Complement]
tilde_eq_class_correct [lemma, in OAut.Complement]
tilde_eq_class [definition, in OAut.Complement]
tilde_extensional [lemma, in OAut.Complement]
tilde_congruence [lemma, in OAut.Complement]
tilde_equivalence [lemma, in OAut.Complement]
tilde_symmetric [lemma, in OAut.Complement]
tilde_transitive [lemma, in OAut.Complement]
tilde_reflexive [lemma, in OAut.Complement]
tilde_equiv [definition, in OAut.Complement]
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]
totality [lemma, in OAut.Complement]
to_seq_unchanged [lemma, in OAut.Utils]
to_bounded_unchanged [lemma, in OAut.Utils]
to_bounded [definition, in OAut.Utils]
to_seq [definition, in OAut.Utils]
transforms [definition, in OAut.Complement]
transforms_extensional [lemma, in OAut.Complement]
transforms_final [definition, in OAut.Complement]
transition [projection, in OAut.NFAs]
TransitionGraph [section, in OAut.NFAs]
transition_dec_public [instance, in OAut.NFAs]
transition_dec [projection, in OAut.NFAs]
trim [definition, in OAut.DecLanguageEmpty]
TrimAutomata [section, in OAut.DecLanguageEmpty]
trim_empty_buechi [lemma, in OAut.DecLanguageEmpty]
trim_state_implies_language_non_empty [lemma, in OAut.DecLanguageEmpty]
trim_accepts_same_as_aut [lemma, in OAut.DecLanguageEmpty]
trim_accepted_by_aut [lemma, in OAut.DecLanguageEmpty]
trim_aut [definition, in OAut.DecLanguageEmpty]
trim_final [definition, in OAut.DecLanguageEmpty]
trim_initial [definition, in OAut.DecLanguageEmpty]
trim_transition [definition, in OAut.DecLanguageEmpty]
trim_state [definition, in OAut.DecLanguageEmpty]
True_eq_dec [instance, in BA.BasicDefinitions]
True_dec [instance, in BA.External]
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]
union [definition, in OAut.Buechi]
union_correct [lemma, in OAut.Buechi]
union_final [definition, in OAut.Buechi]
union_initial [definition, in OAut.Buechi]
union_transition [definition, in OAut.Buechi]
union_state [definition, in OAut.Buechi]
unit_eq_dec [instance, in BA.BasicDefinitions]
unit_enum_ok [lemma, in BA.FinTypes]
universal_language [definition, in OAut.BasicDefs]
Utils [library]
U_correct [lemma, in BA.Automata]

V

valid_run_connects [lemma, in OAut.NFAs]
valid_path_cut [lemma, in OAut.NFAs]
valid_path_drop [lemma, in OAut.NFAs]
valid_run_drop [lemma, in OAut.NFAs]
valid_path_decrease [lemma, in OAut.NFAs]
valid_run_is_path_from_begin [lemma, in OAut.NFAs]
valid_run_is_path_everywhere [lemma, in OAut.NFAs]
valid_run_extensional [lemma, in OAut.NFAs]
valid_path_extensional [lemma, in OAut.NFAs]
valid_path [definition, in OAut.NFAs]
valid_run [definition, in OAut.NFAs]
valid_r' [lemma, in OAut.Complement]
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]
visits_final [definition, in OAut.NFAConstructions]
VW [definition, in OAut.Complement]
VW_part_of_complement [definition, in OAut.Complement]
VW_aut_correct [lemma, in OAut.Complement]
VW_aut [definition, in OAut.Complement]
vw_aut_correct [lemma, in OAut.NFAConstructions]
vw_aut_accepts_vw_omega [lemma, in OAut.NFAConstructions]
vw_aut_is_vw_omega [lemma, in OAut.NFAConstructions]
vw_aut [definition, in OAut.NFAConstructions]
vw_state_initial [definition, in OAut.NFAConstructions]
vw_state_final [definition, in OAut.NFAConstructions]
vw_transition [definition, in OAut.NFAConstructions]
vw_state [definition, in OAut.NFAConstructions]
v_transforms [lemma, in OAut.Complement]
v'_transforms [lemma, in OAut.Complement]

W

WaitFinal [inductive, in OAut.Buechi]
waitfinal_enum_ok [lemma, in OAut.Buechi]
waitfinal_eq_dec [instance, in OAut.Buechi]
Wait1 [constructor, in OAut.Buechi]
Wait2 [constructor, in OAut.Buechi]
Womega_aut [definition, in OAut.NFAConstructions]
Womega_state_initial [definition, in OAut.NFAConstructions]
Womega_state_final [definition, in OAut.NFAConstructions]
Womega_transition [definition, in OAut.NFAConstructions]
word [definition, in BA.Automata]
W_transforms [lemma, in OAut.Complement]
W_final_iff [lemma, in OAut.Complement]
W_final [definition, in OAut.Complement]
w_omega_one_initial_state [lemma, in OAut.NFAConstructions]
w_omega_aut_correct [lemma, in OAut.NFAConstructions]
W_Omega_Automata.normW [variable, in OAut.NFAConstructions]
W_Omega_Automata.finalW [variable, in OAut.NFAConstructions]
W_Omega_Automata.initialW [variable, in OAut.NFAConstructions]
W_Omega_Automata.autW [variable, in OAut.NFAConstructions]
W_Omega_Automata [section, in OAut.NFAConstructions]
W'_transforms [lemma, in OAut.Complement]

other

_ ** _ (EqTypeScope) [notation, in BA.BasicDefinitions]
_ == _ (string_scope) [notation, in OAut.Seqs]
_ +++ _ (string_scope) [notation, in OAut.Seqs]
_ ++ _ (string_scope) [notation, in OAut.Seqs]
_ [ _ ] (string_scope) [notation, in OAut.Seqs]
| _ | (string_scope) [notation, in OAut.Seqs]
Sigma _ .. _ , _ (type_scope) [notation, in BA.External]
_ ** _ [notation, in BA.BasicDefinitions]
_ o _ [notation, in OAut.SeqOperations]
_ ^002 [notation, in OAut.SeqOperations]
_ ^00 [notation, in OAut.SeqOperations]
_ to_omega [notation, in OAut.SeqOperations]
_ === _ [notation, in BA.External]
_ <<= _ [notation, in BA.External]
_ el _ [notation, in BA.External]
_ === _ [notation, in OAut.Seqs]
_ ^0$0 [notation, in OAut.Seqs]
_ ^ _ [notation, in BA.FinTypes]
_ --> _ [notation, in BA.FinTypes]
_ (+) _ [notation, in BA.FinTypes]
_ (x) _ [notation, in BA.FinTypes]
_ ^$~ [notation, in OAut.BasicDefs]
_ /$\ _ [notation, in OAut.BasicDefs]
_ \$/ _ [notation, in OAut.BasicDefs]
_ =$= _ [notation, in OAut.BasicDefs]
_ <$= _ [notation, in OAut.BasicDefs]
eq_dec _ [notation, in BA.External]
L_S [notation, in OAut.NFAs]
L_B [notation, in OAut.Buechi]
# _ [notation, in BA.FinTypes]
? _ [notation, in BA.FinTypes]
?? _ [notation, in BA.BasicDefinitions]
{} [notation, in OAut.BasicDefs]
| _ | [notation, in BA.External]

---

Notation Index

B

a [in OAut.Buechi]
b [in OAut.Buechi]
S1 [in OAut.Buechi]
S2 [in OAut.Buechi]

N

Final [in OAut.NFAConstructions]
Initial [in OAut.NFAConstructions]

T

# _ [in BA.FinTypes]
_ ~~# _ [in OAut.Complement]
_ ~~@ _ at _ [in OAut.Complement]
_ ~~ _ [in OAut.Complement]
_ =!=> _ on _ [in OAut.Complement]
_ ===> _ on _ [in OAut.Complement]
{[ _ ]} [in OAut.Complement]

other

_ ** _ (EqTypeScope) [in BA.BasicDefinitions]
_ == _ (string_scope) [in OAut.Seqs]
_ +++ _ (string_scope) [in OAut.Seqs]
_ ++ _ (string_scope) [in OAut.Seqs]
_ [ _ ] (string_scope) [in OAut.Seqs]
| _ | (string_scope) [in OAut.Seqs]
Sigma _ .. _ , _ (type_scope) [in BA.External]
_ ** _ [in BA.BasicDefinitions]
_ o _ [in OAut.SeqOperations]
_ ^002 [in OAut.SeqOperations]
_ ^00 [in OAut.SeqOperations]
_ to_omega [in OAut.SeqOperations]
_ === _ [in BA.External]
_ <<= _ [in BA.External]
_ el _ [in BA.External]
_ === _ [in OAut.Seqs]
_ ^0$0 [in OAut.Seqs]
_ ^ _ [in BA.FinTypes]
_ --> _ [in BA.FinTypes]
_ (+) _ [in BA.FinTypes]
_ (x) _ [in BA.FinTypes]
_ ^$~ [in OAut.BasicDefs]
_ /$\ _ [in OAut.BasicDefs]
_ \$/ _ [in OAut.BasicDefs]
_ =$= _ [in OAut.BasicDefs]
_ <$= _ [in OAut.BasicDefs]
eq_dec _ [in BA.External]
L_S [in OAut.NFAs]
L_B [in OAut.Buechi]
# _ [in BA.FinTypes]
? _ [in BA.FinTypes]
?? _ [in BA.BasicDefinitions]
{} [in OAut.BasicDefs]
| _ | [in BA.External]

---

Module Index

B

BuechiExample [in OAut.Buechi]

---

Variable Index

B

BuechiLanguage.A [in OAut.Buechi]

C

Cardinality.X [in BA.External]
Closed_Intersection.aut2 [in OAut.Buechi]
Closed_Intersection.aut1 [in OAut.Buechi]
Closed_Union.aut2 [in OAut.Buechi]
Closed_Union.aut1 [in OAut.Buechi]
ConcatInfPrependNFA.runs [in OAut.NFAConstructions]
ConcatInfPrependNFA.strings [in OAut.NFAConstructions]
ConvertToNFA.aut [in OAut.fin_languages]

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]
FindNextPosition.decP [in OAut.SeqOperations]
FindNextPosition.P [in OAut.SeqOperations]
FindNextPosition.w [in OAut.SeqOperations]
FiniteClosureIteration.step [in BA.FinTypes]
FiniteClosureIteration.step_dec [in BA.FinTypes]
FiniteClosureIteration.X [in BA.FinTypes]
FirstKFinType.DeclareFinType.k [in OAut.Utils]
First.p [in OAut.Utils]
First.p_dec [in OAut.Utils]
Fixedpoints.f [in BA.FinTypes]
Fixedpoints.X [in BA.FinTypes]

H

HistoryFilter.baseP [in OAut.SeqOperations]
HistoryFilter.decP [in OAut.SeqOperations]
HistoryFilter.extP [in OAut.SeqOperations]
HistoryFilter.P [in OAut.SeqOperations]
HistoryFilter.stepP [in OAut.SeqOperations]
HistoryFilter.w [in OAut.SeqOperations]

I

Inclusion.X [in BA.External]
InfiniteFilter.decP [in OAut.SeqOperations]
InfiniteFilter.infP [in OAut.SeqOperations]
InfiniteFilter.P [in OAut.SeqOperations]
InfiniteFilter.w [in OAut.SeqOperations]

L

LanguageLemmata.L [in OAut.BasicDefs]
LanguageLemmata.L_2 [in OAut.BasicDefs]
LanguageLemmata.L_1 [in OAut.BasicDefs]
LanguageLemmata.X [in OAut.BasicDefs]
Languages.X [in OAut.BasicDefs]

M

Membership.X [in BA.External]

N

NormalizeNFA.aut [in OAut.NFAConstructions]

O

OmegaIteration.l [in OAut.SeqOperations]

P

PowerRep.X [in BA.External]
PrependFinLanguage_Automata.normW [in OAut.NFAConstructions]
PrependFinLanguage_Automata.initialW [in OAut.NFAConstructions]
PrependFinLanguage_Automata.autW [in OAut.NFAConstructions]
PrependFinLanguage_Automata.normV [in OAut.NFAConstructions]
PrependFinLanguage_Automata.finalV [in OAut.NFAConstructions]
PrependFinLanguage_Automata.initialV [in OAut.NFAConstructions]
PrependFinLanguage_Automata.autV [in OAut.NFAConstructions]

R

Removal.X [in BA.External]

T

Test.X [in BA.FinTypes]
Test.Y [in BA.FinTypes]
TildeEquivalenceRelation.Compatibility.Acc [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.agree_R [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.agree_r0 [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.Eq [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.eqLengthv [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.EqR [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.Eq' [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.i [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.j [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.ow [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.ow' [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.R [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.r [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.r0 [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.V [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.v [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.valid_R [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.valid_r0 [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.V' [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.v' [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.W [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.w [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.W' [in OAut.Complement]
TildeEquivalenceRelation.Compatibility.w' [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable.endS [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable.startS [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable.endS [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable.startS [in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability.k1 [in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability.k2 [in OAut.Complement]

U

Undup.X [in BA.External]

W

W_Omega_Automata.normW [in OAut.NFAConstructions]
W_Omega_Automata.finalW [in OAut.NFAConstructions]
W_Omega_Automata.initialW [in OAut.NFAConstructions]
W_Omega_Automata.autW [in OAut.NFAConstructions]

---

Library Index

A

Automata

B

BasicDefinitions
BasicDefs
Buechi

C

Complement

D

DecLanguageEmpty

E

External

F

FinTypes
fin_languages

N

NFAConstructions
NFAs

S

SeqOperations
Seqs
StrictlyMonotoneSeqs

U

Utils

---

Lemma Index

A

accepting_run_for_W' [in OAut.Complement]
adjacent_paths_agree [in OAut.NFAs]
allSub [in BA.FinTypes]
all_Le_K_length_all_le_k [in OAut.Utils]
all_aut_accepts_everything [in OAut.fin_languages]
all_transition_dec [in OAut.fin_languages]
all_state_initial_dec [in OAut.fin_languages]
all_state_final_dec [in OAut.fin_languages]
appendNil [in BA.BasicDefinitions]
apply_vectorise_inverse [in BA.FinTypes]
autC_disjoint [in OAut.Complement]
autI_incl_aut2 [in OAut.Buechi]
autI_incl_aut1 [in OAut.Buechi]
autU_accepted_by_aut2 [in OAut.Buechi]
autU_accepted_by_aut1 [in OAut.Buechi]
aut_accepted_by_trim [in OAut.DecLanguageEmpty]
aut_is_w_omega [in OAut.NFAConstructions]
aut_accepts_w_omega [in OAut.NFAConstructions]
aut_accepts_norm_aut [in OAut.NFAConstructions]
aut1_inter_aut2_incl_autI [in OAut.Buechi]
aut1_incl_autU [in OAut.Buechi]
aut2_incl_autU [in OAut.Buechi]

B

boolOption_enum_ok [in BA.FinTypes]
bool_enum_ok [in BA.FinTypes]
bounded_unchanged [in OAut.Utils]
bounded_exist [in OAut.Utils]
bounded_type_exist [in OAut.Utils]
bounded_path_to_path [in OAut.NFAs]
bounded_string_is_valid_path [in OAut.NFAs]
bounded_run_is_valid_path [in OAut.NFAs]
bound_path_unchanged [in OAut.Complement]
BuechiExample.ab_omega_incl_aut [in OAut.Buechi]
BuechiExample.aut_incl_ab_omega [in OAut.Buechi]
BuechiExample.dec_final_state [in OAut.Buechi]
BuechiExample.dec_initial_state [in OAut.Buechi]
BuechiExample.dec_transition [in OAut.Buechi]

C

can_find_duplicate [in OAut.Utils]
can_find_next_position [in OAut.SeqOperations]
CardIn [in BA.FinTypes]
Cardinality_card_eq [in BA.FinTypes]
card_finType_Le_K [in OAut.Utils]
card_finTypeC_Le_K [in OAut.Utils]
card_length_leq [in BA.BasicDefinitions]
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_upper_bound [in BA.FinTypes]
Card_positiv [in BA.FinTypes]
cc_nat [in OAut.Utils]
closed_intersection [in OAut.Buechi]
closed_union [in OAut.Buechi]
Closure [in BA.FinTypes]
Closure_FCIter [in BA.FinTypes]
combine_final_transforms_right [in OAut.Complement]
combine_final_transforms_left [in OAut.Complement]
combine_transforms [in OAut.Complement]
common_merge_index [in OAut.Complement]
compatibility [in OAut.Complement]
compatibilityComplement [in OAut.Complement]
compatibility2 [in OAut.Complement]
complement_correct [in BA.Automata]
complement_correct2 [in OAut.Complement]
complement_correct [in OAut.Complement]
complement_complete [in OAut.Complement]
complete_induction [in OAut.BasicDefs]
compose_s_monotone [in OAut.StrictlyMonotoneSeqs]
compute_run_final_transforms [in OAut.Complement]
compute_run_transforms [in OAut.Complement]
compute_run [in OAut.NFAConstructions]
concat_paths [in OAut.NFAs]
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]
concat_inf_index_equal [in OAut.SeqOperations]
concat_inf_correct [in OAut.SeqOperations]
concat_inf_index_to_begin [in OAut.SeqOperations]
concat_inf_index_injective [in OAut.SeqOperations]
concat_inf_index_le [in OAut.SeqOperations]
concat_inf_index_step_correct [in OAut.SeqOperations]
concat_inf_index_in_bounds [in OAut.SeqOperations]
concat_inf_index_correct [in OAut.SeqOperations]
concat_inf_index_begin [in OAut.SeqOperations]
concat_inf_index_in_string [in OAut.SeqOperations]
concat_extract [in OAut.Seqs]
concat_inf_final_step [in OAut.NFAConstructions]
concat_inf_is_final_not_constructive [in OAut.NFAConstructions]
concat_inf_is_valid [in OAut.NFAConstructions]
concat_map_length [in BA.FinTypes]
consAppend [in BA.BasicDefinitions]
cons_incll [in BA.BasicDefinitions]
cons_correct [in BA.Automata]
convertFromNFA [in OAut.fin_languages]
convertoToNFA [in OAut.fin_languages]
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]
create_Le_K [in OAut.Utils]
cut_rest_correct [in OAut.Seqs]
cut_front_correct [in OAut.Seqs]
cyclic_path_connects [in OAut.NFAs]
cyclic_path_connects_on_path [in OAut.NFAs]

D

decFinEquivRel_RamseyImpliesFinEquivClasses [in OAut.Buechi]
decFinEquivRel_FiniteTypeSeqImpliesFinEquivClasses [in OAut.Buechi]
decision_false [in OAut.BasicDefs]
decision_true [in OAut.BasicDefs]
DecRef [in BA.BasicDefinitions]
dec_connected [in OAut.NFAs]
dec_bounded_path [in OAut.NFAs]
dec_language_empty [in OAut.DecLanguageEmpty]
dec_language_empty_informative [in OAut.DecLanguageEmpty]
dec_trim_final [in OAut.DecLanguageEmpty]
dec_trim_initial [in OAut.DecLanguageEmpty]
dec_trim_transition [in OAut.DecLanguageEmpty]
dec_state_trim [in OAut.DecLanguageEmpty]
dec_union_final [in OAut.Buechi]
dec_union_initial [in OAut.Buechi]
dec_union_transition [in OAut.Buechi]
dec_language_eq [in OAut.Complement]
dec_language_inclusion [in OAut.Complement]
dec_language_universal [in OAut.Complement]
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]
detlaQstar_convert_inverse [in OAut.fin_languages]
detlaQstar_convert [in OAut.fin_languages]
detlaQstar_decrease_step [in OAut.fin_languages]
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]
drop_preserves_finite [in OAut.Seqs]
drop_correct [in OAut.Seqs]
dummy [in OAut.Utils]
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]
dup_free_all_Le_K [in OAut.Utils]
dup_free_all_le_k [in OAut.Utils]

E

elementIn [in BA.FinTypes]
empty_reach [in BA.Automata]
empty_aut_correct [in OAut.Buechi]
Empty_set_enum_ok [in BA.FinTypes]
enum_ok_fromList [in BA.FinTypes]
Epsilon_autom_correct [in BA.Automata]
equalSELangImpliesEqualSLang [in OAut.Complement]
equivalence_class_closed [in OAut.Complement]
Equivalence_property_exists' [in BA.FinTypes]
Equivalence_property_exists [in BA.FinTypes]
Equivalence_property_all [in BA.FinTypes]
equivalent_drop [in OAut.Complement]
equivalent_if_same_equivalence_class [in OAut.Complement]
equivalent_in_equivalence_class [in OAut.Complement]
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_classes_extensional [in OAut.Complement]
eq_iff [in BA.FinTypes]
exactW_correct [in BA.Automata]
extensional_o_iter2_implies_iter1 [in OAut.SeqOperations]
extPow_length [in BA.FinTypes]
extract_from_drop [in OAut.Seqs]
extract_correct [in OAut.Seqs]

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]
finalW_does_not_appear_in_valid_run [in OAut.NFAConstructions]
final_coaccessible_iff_final_cycle [in OAut.DecLanguageEmpty]
final_valid_run_has_cycle [in OAut.DecLanguageEmpty]
final_cyclic_to_connected [in OAut.DecLanguageEmpty]
final_state_intersection_is_final_state_aut2 [in OAut.Buechi]
final_extensional [in OAut.Buechi]
final_prepend [in OAut.Buechi]
final_drop [in OAut.Buechi]
final_r' [in OAut.Complement]
final_transforms_extensional [in OAut.Complement]
final_transform_implies_transform [in OAut.Complement]
final_concat_inf_infinite_final_strings [in OAut.NFAConstructions]
fInduction [in BA.FinTypes]
find_final_aut1_correct [in OAut.Buechi]
find_final_aut1_less [in OAut.Buechi]
find_next_position_correct [in OAut.SeqOperations]
finEquivClassesImpliesFiniteTypeSeq [in OAut.Buechi]
finiteIndexImpliesFiniteIndexNeg [in OAut.Buechi]
finiteIndexNegAndXMImpliesFiniteIndex [in OAut.Buechi]
finite_type_predicate_seq [in OAut.Buechi]
finite_prefix_preserves_infinite [in OAut.Seqs]
finTypeEqEquiv [in OAut.Buechi]
finTypeEqFiniteIndex [in OAut.Buechi]
finTypeEqRelXM [in OAut.Buechi]
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_cc_sigma [in OAut.Complement]
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]
first_norm_is_initial [in OAut.NFAConstructions]
fix_first_zero_s_monotone [in OAut.StrictlyMonotoneSeqs]
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]
ge_to_le [in OAut.SeqOperations]

H

Hedberg [in BA.BasicDefinitions]
HelpApply [in BA.FinTypes]
history_filter_correct [in OAut.SeqOperations]
history_filter_proof_only_append [in OAut.SeqOperations]
history_filter_proof_only_append_step [in OAut.SeqOperations]
history_filter_zero [in OAut.SeqOperations]
history_filter_s_monotone [in OAut.SeqOperations]
history_filter_step [in OAut.SeqOperations]
history_filter_base [in OAut.SeqOperations]

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]
infinite_final_is_accepting_for_finite_automaton [in OAut.Buechi]
infinite_equiv_indices_merging [in OAut.Complement]
infinite_equiv_indices_equiv_begin [in OAut.Complement]
infinite_equiv_indices [in OAut.Complement]
infinite_final_strings_R [in OAut.Complement]
infinite_filter_zero [in OAut.SeqOperations]
infinite_filter_all [in OAut.SeqOperations]
infinite_filter_correct [in OAut.SeqOperations]
infinite_filter_s_monotone [in OAut.SeqOperations]
inImages [in BA.FinTypes]
initialW_always_final [in OAut.NFAConstructions]
initialW_partitions_in_W [in OAut.NFAConstructions]
initial_r' [in OAut.Complement]
injectiveApply [in BA.BasicDefinitions]
injective_dupfree [in BA.FinTypes]
inr_fix [in BA.Automata]
inr_fix_epsilon [in BA.Automata]
intersectionRunStaysWait1UntilNextFinalAut1 [in OAut.Buechi]
intersectionRunStaysWait2UntilNextFinalAut2 [in OAut.Buechi]
intersectionRunSwitchtesFromWait1ToWait2 [in OAut.Buechi]
intersectionRunSwitchtesFromWait2ToFinal [in OAut.Buechi]
intersection_run_is_valid [in OAut.Buechi]
intersection_run_does_not_change_states [in OAut.Buechi]
intersection_final_dec [in OAut.Buechi]
intersection_initial_dec [in OAut.Buechi]
intersection_transition_dec [in OAut.Buechi]
intersect_correct [in BA.Automata]
intersect_correct [in OAut.Buechi]
in_all_Le_K_ifLess [in OAut.Utils]
in_all_Le_K_if2 [in OAut.Utils]
in_all_Le_K_if [in OAut.Utils]
in_all_le_k_iff [in OAut.Utils]
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

language_intersection_comm [in OAut.BasicDefs]
language_union_comm [in OAut.BasicDefs]
language_eq_symmetric [in OAut.BasicDefs]
language_eq_iff [in OAut.BasicDefs]
language_universal_iff [in OAut.BasicDefs]
language_empty_iff [in OAut.BasicDefs]
lang_incl_iff [in BA.Automata]
last_norm_is_final [in OAut.NFAConstructions]
lengthEq [in BA.BasicDefinitions]
leq_to_distance [in OAut.Buechi]
leq_0 [in OAut.Complement]
Le_K_enum_ok [in OAut.Utils]
list_eq [in OAut.Utils]
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]

M

many_aut_union [in OAut.Buechi]
many_aut_intersection [in OAut.fin_languages]
max_of_nat_string_correct [in OAut.Utils]
max_le_right [in OAut.BasicDefs]
max_le_left [in OAut.BasicDefs]
merge_at_next_append [in OAut.Complement]
merge_at_next_extensional [in OAut.Complement]
minimize_path_correct [in OAut.NFAs]

N

nat_pair_le_not_equal [in OAut.SeqOperations]
negOr [in BA.BasicDefinitions]
nil_kleene [in BA.Automata]
NoneElement [in BA.FinTypes]
non_empty_cycle_is_valid [in OAut.NFAs]
normalize_aut [in OAut.NFAConstructions]
norm_aut_accepts_aut [in OAut.NFAConstructions]
notInMapCons [in BA.FinTypes]
notInZero [in BA.BasicDefinitions]
not_part_of_complement_implies_aut [in OAut.Complement]
not_tilde_w_extend [in OAut.Complement]
not_in_cons [in BA.External]
NullMul [in BA.BasicDefinitions]

O

omega_iteration_infinite [in OAut.SeqOperations]
onestate_correct [in BA.Automata]
Option_Card [in BA.FinTypes]
option_enum_ok [in BA.FinTypes]
other_norm_is_aut_state [in OAut.NFAConstructions]
o_iter_implies_o_iter2 [in OAut.SeqOperations]

P

partition_run_on_concat_inf [in OAut.NFAConstructions]
partition_run_on_prepend_string [in OAut.NFAConstructions]
part_of_complement_implies_complement [in OAut.Complement]
path_length_bounded [in OAut.NFAs]
path_extensional [in OAut.NFAs]
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]
prepending_path_on_path_is_valid [in OAut.NFAs]
prepending_path_is_valid [in OAut.NFAs]
prepend_valid_path [in OAut.NFAs]
prepend_valid_run [in OAut.NFAs]
prepend_on_omega_iteration [in OAut.SeqOperations]
prepend_path_rest_correct2 [in OAut.Seqs]
prepend_path_rest_correct [in OAut.Seqs]
prepend_path_first [in OAut.Seqs]
prepend_path_begin_correct [in OAut.Seqs]
prepend_rest_correct2 [in OAut.Seqs]
prepend_rest_correct [in OAut.Seqs]
prepend_first_correct [in OAut.Seqs]
prepend_string_is_valid [in OAut.NFAConstructions]
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_correct [in BA.Automata]
prod_delta_star [in BA.Automata]
Prod_Card [in BA.FinTypes]
prod_enum_ok [in BA.FinTypes]
project_second_is_valid [in OAut.Buechi]
project_first_is_valid [in OAut.Buechi]
proj1_sig_fun [in BA.BasicDefinitions]
proveOne [in BA.FinTypes]
pure_le_k_if [in OAut.Utils]
pure_eq [in BA.BasicDefinitions]
pure_impure [in BA.BasicDefinitions]
pure_equiv [in BA.BasicDefinitions]
purify [in BA.BasicDefinitions]

R

ramseyImpliesFiniteTypeSeq [in OAut.Buechi]
ramseyTotality [in OAut.Complement]
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]
remove_circle_preserves_last_state [in OAut.NFAs]
remove_circle_preserves_first_state [in OAut.NFAs]
remove_circle_decrease [in OAut.NFAs]
remove_circle_correct [in OAut.NFAs]
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]
revert_concat_second [in OAut.Seqs]
revert_concat_first [in OAut.Seqs]
revert_drop_path [in OAut.Seqs]
revert_prepend_path [in OAut.Seqs]
rightResult [in BA.FinTypes]
R'k0_eq_Rk0 [in OAut.Complement]

S

safe_dclosed [in OAut.Utils]
sclosure_complement [in OAut.fin_languages]
sclosure_diff [in OAut.fin_languages]
sclosure_intersection [in OAut.fin_languages]
sclosure_union [in OAut.fin_languages]
scomplement_correct [in OAut.fin_languages]
sdiff_correct [in OAut.fin_languages]
seqToListCorrect [in OAut.fin_languages]
seq_in_empty_aut_contradicts [in OAut.Buechi]
seq_prop_dec_exists_bounded [in OAut.Seqs]
sigT_proj2_fun [in BA.BasicDefinitions]
sigT_proj1_fun [in BA.BasicDefinitions]
sigT_enum_ok [in BA.FinTypes]
Sig_reach [in BA.Automata]
sintersect_correct [in OAut.fin_languages]
size_induction [in BA.External]
slanguage_extensional [in OAut.NFAs]
sNFA_sNFA_to_omega_Buechi [in OAut.NFAConstructions]
SomeElement [in BA.FinTypes]
split_path [in OAut.NFAs]
split_final_transforms [in OAut.Complement]
split_transforms [in OAut.Complement]
stateAfterFinalIsWait1 [in OAut.Buechi]
stateBeforeFinalIsWait2 [in OAut.Buechi]
states_trim_subtype [in OAut.DecLanguageEmpty]
states_in_final_path_are_trim [in OAut.DecLanguageEmpty]
states_do_not_mix [in OAut.Buechi]
step_reach_consistent [in BA.Automata]
step_consistent_least_fp [in BA.FinTypes]
step_trans_fp_incl [in BA.FinTypes]
step_iter_consistent [in BA.FinTypes]
Streicher_K [in BA.BasicDefinitions]
strict_bounded_exist [in OAut.Utils]
stringToListCorrect [in OAut.fin_languages]
stringToList_Size [in OAut.fin_languages]
string_final_R' [in OAut.Complement]
string_equal_symmetric [in OAut.Seqs]
string_equal_reflexive [in OAut.Seqs]
subtype_extensionality [in BA.BasicDefinitions]
subType_enum_ok [in BA.FinTypes]
SumCard [in BA.FinTypes]
sum_enum_ok [in BA.FinTypes]
sunion_correct [in OAut.fin_languages]
surjectiveApply [in BA.BasicDefinitions]
surj_sub [in BA.FinTypes]
switch_from_V_to_W [in OAut.NFAConstructions]
s_monotone_drop [in OAut.StrictlyMonotoneSeqs]
s_monotone_ge_zero [in OAut.StrictlyMonotoneSeqs]
s_monotone_order_preserving_backwards [in OAut.StrictlyMonotoneSeqs]
s_monotone_order_preserving [in OAut.StrictlyMonotoneSeqs]
s_monotone_strict_order_preserving [in OAut.StrictlyMonotoneSeqs]
s_monotone_ge [in OAut.StrictlyMonotoneSeqs]
s_monotone_unbouded_ge [in OAut.StrictlyMonotoneSeqs]
s_monotone_unbouded [in OAut.StrictlyMonotoneSeqs]
s_monotone_id [in OAut.StrictlyMonotoneSeqs]
s_monotone_begin_in [in OAut.SeqOperations]

T

tff_recognizes_transforms_final [in OAut.Complement]
tff_is_transforms_final [in OAut.Complement]
tff_accepts_tranforms_final [in OAut.Complement]
tff_transition_dec [in OAut.Complement]
tff_state_final_dec [in OAut.Complement]
tff_state_initial_dec [in OAut.Complement]
tf_recognizes_transforms [in OAut.Complement]
tf_is_transforms [in OAut.Complement]
tf_accepts_tranforms [in OAut.Complement]
tf_transition_dec [in OAut.Complement]
tf_state_final_dec [in OAut.Complement]
tf_state_initial_dec [in OAut.Complement]
there_are_infinite_final_aut1 [in OAut.Buechi]
there_is_aut1_final_in_between [in OAut.Buechi]
there_is_bigger_merging_index [in OAut.Complement]
there_is_final_index [in OAut.Complement]
there_is_rec_find_next_position [in OAut.SeqOperations]
there_is_initialW [in OAut.NFAConstructions]
tilde_w_equiv_finite_index [in OAut.Complement]
tilde_w_equiv_finite_index_neq [in OAut.Complement]
tilde_equiv_finite_index_neq [in OAut.Complement]
tilde_equiv_finite_index [in OAut.Complement]
tilde_w_equiv_XM [in OAut.Complement]
tilde_w_equiv_bool_infinite_false [in OAut.Complement]
tilde_w_equiv_bool_remains_true [in OAut.Complement]
tilde_w_equiv_iff [in OAut.Complement]
tilde_w_index_equiv_iff [in OAut.Complement]
tilde_w_equivalence [in OAut.Complement]
tilde_w_transitive [in OAut.Complement]
tilde_w_index_transitive [in OAut.Complement]
tilde_w_symmetric [in OAut.Complement]
tilde_w_index_symmetric [in OAut.Complement]
tilde_w_reflexive [in OAut.Complement]
tilde_w_index_reflexive [in OAut.Complement]
tilde_w_extend [in OAut.Complement]
tilde_equiv_class_NFA_recognizable [in OAut.Complement]
tilde_equiv_class_aut_is_equiv_class [in OAut.Complement]
tilde_equiv_class_aut_accepts_Equiv_class [in OAut.Complement]
tilde_equiv_class_NFA_recognizable_MyhillNerode [in OAut.Complement]
tilde_eq_class_congruence [in OAut.Complement]
tilde_eq_class_correct [in OAut.Complement]
tilde_extensional [in OAut.Complement]
tilde_congruence [in OAut.Complement]
tilde_equivalence [in OAut.Complement]
tilde_symmetric [in OAut.Complement]
tilde_transitive [in OAut.Complement]
tilde_reflexive [in OAut.Complement]
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]
totality [in OAut.Complement]
to_seq_unchanged [in OAut.Utils]
to_bounded_unchanged [in OAut.Utils]
transforms_extensional [in OAut.Complement]
trim_empty_buechi [in OAut.DecLanguageEmpty]
trim_state_implies_language_non_empty [in OAut.DecLanguageEmpty]
trim_accepts_same_as_aut [in OAut.DecLanguageEmpty]
trim_accepted_by_aut [in OAut.DecLanguageEmpty]
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]
union_correct [in OAut.Buechi]
unit_enum_ok [in BA.FinTypes]
U_correct [in BA.Automata]

V

valid_run_connects [in OAut.NFAs]
valid_path_cut [in OAut.NFAs]
valid_path_drop [in OAut.NFAs]
valid_run_drop [in OAut.NFAs]
valid_path_decrease [in OAut.NFAs]
valid_run_is_path_from_begin [in OAut.NFAs]
valid_run_is_path_everywhere [in OAut.NFAs]
valid_run_extensional [in OAut.NFAs]
valid_path_extensional [in OAut.NFAs]
valid_r' [in OAut.Complement]
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]
VW_aut_correct [in OAut.Complement]
vw_aut_correct [in OAut.NFAConstructions]
vw_aut_accepts_vw_omega [in OAut.NFAConstructions]
vw_aut_is_vw_omega [in OAut.NFAConstructions]
v_transforms [in OAut.Complement]
v'_transforms [in OAut.Complement]

W

waitfinal_enum_ok [in OAut.Buechi]
W_transforms [in OAut.Complement]
W_final_iff [in OAut.Complement]
w_omega_one_initial_state [in OAut.NFAConstructions]
w_omega_aut_correct [in OAut.NFAConstructions]
W'_transforms [in OAut.Complement]

---

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

Final [in OAut.Buechi]
FinType [in BA.FinTypes]
FinTypeC [in BA.FinTypes]
found_pos [in OAut.SeqOperations]

M

mknfa [in OAut.NFAs]
mkstring [in OAut.Seqs]

N

NFA [in BA.Automata]

P

pos_step [in OAut.SeqOperations]

R

refl [in BA.Automata]

S

safeB [in OAut.Utils]
safeS [in OAut.Utils]
step [in BA.Automata]

W

Wait1 [in OAut.Buechi]
Wait2 [in OAut.Buechi]

---

Axiom Index

F

finite_equiv_classes [in OAut.Buechi]
finite_type_seq [in OAut.Buechi]

---

Inductive Index

D

dupfree [in BA.External]

R

reachable [in BA.Automata]
rec_find_next_position [in OAut.SeqOperations]

S

safe [in OAut.Utils]

W

WaitFinal [in OAut.Buechi]

---

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]
final_state_dec [in OAut.NFAs]
final_state [in OAut.NFAs]

I

initial_state_dec [in OAut.NFAs]
initial_state [in OAut.NFAs]

L

lastindex [in OAut.Seqs]

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]
seq [in OAut.Seqs]
state [in OAut.NFAs]

T

transition [in OAut.NFAs]
transition_dec [in OAut.NFAs]
type [in BA.FinTypes]

---

Section Index

A

AllAutomaton [in OAut.fin_languages]

B

BuechiLanguage [in OAut.Buechi]

C

Cardinality [in BA.External]
Closed_Intersection [in OAut.Buechi]
Closed_Union [in OAut.Buechi]
ClosureProperties [in OAut.fin_languages]
ComplementCorollaries [in OAut.Complement]
ConcatInfPrependNFA [in OAut.NFAConstructions]
ConvertFinTypeToSeq [in OAut.Utils]
ConvertToNFA [in OAut.fin_languages]

D

DecConnected [in OAut.NFAs]
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

EmptyAut [in OAut.Buechi]
Equi [in BA.External]

F

FilterLemmas [in BA.External]
FilterLemmas_pq [in BA.External]
FinalCycle [in OAut.DecLanguageEmpty]
FindNextPosition [in OAut.SeqOperations]
FiniteClosureIteration [in BA.FinTypes]
First [in OAut.Utils]
FirstKFinType [in OAut.Utils]
FirstKFinType.DeclareFinType [in OAut.Utils]
Fixedpoints [in BA.FinTypes]

H

HistoryFilter [in OAut.SeqOperations]

I

Inclusion [in BA.External]
Infinite [in OAut.Seqs]
InfiniteConcat [in OAut.SeqOperations]
InfiniteFilter [in OAut.SeqOperations]

L

LanguageLemmata [in OAut.BasicDefs]
Languages [in OAut.BasicDefs]

M

Membership [in BA.External]

N

NecessaryAssumptions [in OAut.Buechi]
NFAStringLanguage [in OAut.NFAs]
NormalizeNFA [in OAut.NFAConstructions]

O

OmegaIteration [in OAut.SeqOperations]

P

PowerRep [in BA.External]
PrependFinLanguage_Automata [in OAut.NFAConstructions]

R

Removal [in BA.External]

S

SeqOperations [in OAut.Seqs]
StrictlyMonotoneSeqs [in OAut.StrictlyMonotoneSeqs]
StringOperations [in OAut.Seqs]
StringsEq [in OAut.Seqs]

T

Test [in BA.FinTypes]
TildeEquivalenceRelation [in OAut.Complement]
TildeEquivalenceRelation.Compatibility [in OAut.Complement]
TildeEquivalenceRelation.Complement [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsFinalRecognizable [in OAut.Complement]
TildeEquivalenceRelation.TildeEqivalenceClassRecognizable.TransformsRecognizable [in OAut.Complement]
TildeEquivalenceRelation.TildeEquivalenceClassRecognizableMyhillNerode [in OAut.Complement]
TildeEquivalenceRelation.Totality [in OAut.Complement]
TildeEquivalenceRelation.Totality.PropositionalDecidability [in OAut.Complement]
TransitionGraph [in OAut.NFAs]
TrimAutomata [in OAut.DecLanguageEmpty]

U

Undup [in BA.External]

W

W_Omega_Automata [in OAut.NFAConstructions]

---

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]
dec_pure_le_k_public [in OAut.Utils]
dec_pure_le_k [in OAut.Utils]
dec_le_k [in OAut.Utils]
dec_saccepting [in OAut.NFAs]
dec_sfinal [in OAut.NFAs]
dec_sinitial [in OAut.NFAs]
dec_svalid [in OAut.NFAs]
dec_connected_public [in OAut.NFAs]
dec_valid_path_public [in OAut.NFAs]
dec_valid_path [in OAut.NFAs]
dec_trim_states_empty [in OAut.DecLanguageEmpty]
dec_final_coaccessible [in OAut.DecLanguageEmpty]
dec_final_cyclic [in OAut.DecLanguageEmpty]
dec_finite_accessible [in OAut.DecLanguageEmpty]
dec_no_transition [in OAut.Buechi]
dec_no_state [in OAut.Buechi]
dec_VW_part_of_complement [in OAut.Complement]
dec_merge_at_next [in OAut.Complement]
dec_merge_at [in OAut.Complement]
dec_pure_W_final [in OAut.Complement]
dec_tilde_eq_class [in OAut.Complement]
dec_transforms_final [in OAut.Complement]
dec_transforms [in OAut.Complement]
dec_strict_bounded_nat_forall [in OAut.Seqs]
dec_bounded_nat_forall [in OAut.Seqs]
dec_vw_state_initial [in OAut.NFAConstructions]
dec_vw_state_final [in OAut.NFAConstructions]
dec_vw_transition [in OAut.NFAConstructions]
dec_Womega_state_initial [in OAut.NFAConstructions]
dec_Womega_state_final [in OAut.NFAConstructions]
dec_Womega_transition [in OAut.NFAConstructions]
dec_norm_transition [in OAut.NFAConstructions]
dec_norm_final_state [in OAut.NFAConstructions]
dec_norm_initial_state [in OAut.NFAConstructions]
dec_visits_final [in OAut.NFAConstructions]
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_eq_dec [in BA.BasicDefinitions]
False_dec [in BA.External]
final_dec_public [in OAut.NFAs]
FinTypeClass2 [in BA.FinTypes]
finTypeC_Le_K [in OAut.Utils]
finTypeC_WaitFinal [in OAut.Buechi]
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]
initial_dec_public [in OAut.NFAs]
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]
LE_K_eq_dec [in OAut.Utils]
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

seq_dec_exists_bounded [in OAut.Seqs]
Sig_dec [in BA.Automata]
subType_eq_dec [in BA.BasicDefinitions]
sum_eq_dec [in BA.BasicDefinitions]

T

toProp_dec [in BA.Automata]
transition_dec_public [in OAut.NFAs]
True_eq_dec [in BA.BasicDefinitions]
True_dec [in BA.External]

U

unit_eq_dec [in BA.BasicDefinitions]

V

vector_eq_dec [in BA.FinTypes]

W

waitfinal_eq_dec [in OAut.Buechi]

---

Abbreviation Index

I

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

---

Definition Index

A

accept [in BA.Automata]
accepting [in OAut.Buechi]
accessible [in OAut.DecLanguageEmpty]
admissible [in BA.FinTypes]
all_Le_K [in OAut.Utils]
all_le_k [in OAut.Utils]
all_aut [in OAut.fin_languages]
all_transition [in OAut.fin_languages]
all_state_initial [in OAut.fin_languages]
all_state_final [in OAut.fin_languages]
all_state [in OAut.fin_languages]
applyVect [in BA.FinTypes]
autC [in OAut.Complement]
autI [in OAut.Buechi]
autU [in OAut.Buechi]

B

begin_in [in OAut.SeqOperations]
bijective [in BA.BasicDefinitions]
BoundedPath [in OAut.NFAs]
BoundedString [in OAut.NFAs]
BuechiAut [in OAut.Buechi]
BuechiExample.ab_omega [in OAut.Buechi]
BuechiExample.alphabet [in OAut.Buechi]
BuechiExample.aut [in OAut.Buechi]
BuechiExample.final_state [in OAut.Buechi]
BuechiExample.initial_state [in OAut.Buechi]
BuechiExample.state [in OAut.Buechi]
BuechiExample.transition [in OAut.Buechi]

C

card [in BA.External]
Cardinality [in BA.FinTypes]
Card_X_eq [in BA.FinTypes]
classifier [in OAut.Complement]
complement [in BA.Automata]
complement [in OAut.Complement]
complement_auts [in OAut.Complement]
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]
concat_inf [in OAut.SeqOperations]
concat_inf_indices [in OAut.SeqOperations]
concat_strings [in OAut.Seqs]
congruence [in OAut.Complement]
connected [in OAut.NFAs]
cons [in BA.Automata]
count [in BA.BasicDefinitions]
cut [in OAut.Seqs]
cyclic [in OAut.NFAs]
cyclic_path [in OAut.NFAs]

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]
drop [in OAut.Seqs]
drop_string_end [in OAut.Seqs]
drop_string_begin [in OAut.Seqs]

E

econcat [in OAut.Complement]
elem [in BA.FinTypes]
empty [in BA.Automata]
empty_aut [in OAut.Buechi]
empty_state [in OAut.Buechi]
empty_language [in OAut.BasicDefs]
Epsilon_autom [in BA.Automata]
EqBool [in BA.BasicDefinitions]
EqEmpty_set [in BA.BasicDefinitions]
EqFalse [in BA.BasicDefinitions]
EqLe_K [in OAut.Utils]
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]
EquivalenceClassIndex [in OAut.Complement]
EqUnit [in BA.BasicDefinitions]
EqVect [in BA.FinTypes]
EqWaitFinal [in OAut.Buechi]
EString [in OAut.Complement]
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]
extract [in OAut.Seqs]

F

FCIter [in BA.FinTypes]
FCStep [in BA.FinTypes]
filter [in BA.External]
final [in OAut.Buechi]
final_cyclic [in OAut.DecLanguageEmpty]
final_cycle [in OAut.DecLanguageEmpty]
final_coaccessible [in OAut.DecLanguageEmpty]
find_final_aut1 [in OAut.Buechi]
find_next_position [in OAut.SeqOperations]
FiniteEquivClasses [in OAut.Buechi]
finiteIndex [in OAut.Buechi]
finiteIndexNeg [in OAut.Buechi]
FiniteTypeSeq [in OAut.Buechi]
finType_Le_K [in OAut.Utils]
finType_WaitFinal [in OAut.Buechi]
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]
first [in OAut.Utils]
fix_first_zero [in OAut.StrictlyMonotoneSeqs]
fp [in BA.FinTypes]

G

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

H

history_filter [in OAut.SeqOperations]
history_filter_proof [in OAut.SeqOperations]

I

image [in BA.FinTypes]
images [in BA.FinTypes]
inclp [in BA.External]
index [in BA.FinTypes]
infinite [in OAut.Seqs]
infinite_filter [in OAut.SeqOperations]
initial [in OAut.Buechi]
injective [in BA.BasicDefinitions]
intersect [in BA.Automata]
intersect [in OAut.Buechi]
intersection_run [in OAut.Buechi]
intersection_final [in OAut.Buechi]
intersection_initial [in OAut.Buechi]
intersection_transition [in OAut.Buechi]
intersection_state [in OAut.Buechi]

K

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

L

language [in OAut.Buechi]
Language [in OAut.BasicDefs]
language_difference [in OAut.BasicDefs]
language_complement [in OAut.BasicDefs]
language_intersection [in OAut.BasicDefs]
language_union [in OAut.BasicDefs]
language_eq [in OAut.BasicDefs]
language_inclusion [in OAut.BasicDefs]
lang_equiv [in BA.Automata]
lang_incl [in BA.Automata]
lang_prepend [in OAut.SeqOperations]
lang_o_iter2 [in OAut.SeqOperations]
lang_o_iter [in OAut.SeqOperations]
least_fp_containing [in BA.FinTypes]
Le_K [in OAut.Utils]
le_k [in OAut.Utils]

M

M [in OAut.NFAs]
m [in OAut.NFAs]
max_of_nat_string [in OAut.Utils]
mC [in BA.FinTypes]
merge_at_next [in OAut.Complement]
minimize_path [in OAut.NFAs]
mmC [in BA.FinTypes]
MyhillNerode [in OAut.Complement]

N

nat_pair_le [in OAut.SeqOperations]
neg_F [in BA.Automata]
norm_aut [in OAut.NFAConstructions]
norm_transition [in OAut.NFAConstructions]
norm_final_state [in OAut.NFAConstructions]
norm_initial_state [in OAut.NFAConstructions]
norm_state [in OAut.NFAConstructions]
no_transition [in OAut.Buechi]
no_state [in OAut.Buechi]
n_accept [in BA.Automata]

O

omega_iteration [in OAut.SeqOperations]
onestate [in BA.Automata]
orig_state [in OAut.DecLanguageEmpty]

P

path [in OAut.NFAs]
pickx [in BA.FinTypes]
power [in BA.External]
predCons [in BA.Automata]
prepend [in OAut.Seqs]
prepend_path [in OAut.Seqs]
prod [in BA.Automata]
prodLists [in BA.BasicDefinitions]
prod_F [in BA.Automata]
prod_pred [in BA.Automata]
prod_delta [in BA.Automata]
project_second [in OAut.Buechi]
project_first [in OAut.Buechi]
pure [in BA.BasicDefinitions]
pure_W_final [in OAut.Complement]

R

Ramsey [in OAut.Buechi]
reach [in BA.Automata]
reachable_with [in BA.Automata]
refines [in OAut.Complement]
rel_XM [in OAut.Buechi]
rem [in BA.External]
remove_circle [in OAut.NFAs]
rep [in BA.External]
right_congruent [in OAut.Complement]
Run [in OAut.NFAs]
r' [in OAut.Complement]
R' [in OAut.Complement]

S

saccepting [in OAut.NFAs]
sautomaton_normalized [in OAut.NFAConstructions]
scomplement [in OAut.fin_languages]
sdiff [in OAut.fin_languages]
seaccepting [in OAut.Complement]
selanguage [in OAut.Complement]
Seq [in OAut.Seqs]
SeqLang [in OAut.Seqs]
seqToList [in OAut.fin_languages]
seq_equal [in OAut.Seqs]
seq_map [in OAut.Seqs]
sfinal [in OAut.NFAs]
sinitial [in OAut.NFAs]
sintersect [in OAut.fin_languages]
slanguage [in OAut.NFAs]
special_states [in OAut.NFAConstructions]
state_trim [in OAut.DecLanguageEmpty]
step_reach [in BA.Automata]
step_consistent [in BA.FinTypes]
StringLang [in OAut.Seqs]
StringLang_Extensional [in OAut.Seqs]
strings_equal [in OAut.Seqs]
stringToList [in OAut.fin_languages]
string_valid [in OAut.NFAs]
substring [in OAut.SeqOperations]
subtype [in BA.BasicDefinitions]
success2 [in BA.FinTypes]
success3 [in BA.FinTypes]
sunion [in OAut.fin_languages]
surjective [in BA.BasicDefinitions]
svalid [in OAut.NFAs]
s_monotone [in OAut.StrictlyMonotoneSeqs]
s_s'_pair_aut [in OAut.Complement]

T

tff_aut [in OAut.Complement]
tff_transition [in OAut.Complement]
tff_state_final [in OAut.Complement]
tff_state_initial [in OAut.Complement]
tff_state [in OAut.Complement]
tf_aut [in OAut.Complement]
tf_transition [in OAut.Complement]
tf_state_final [in OAut.Complement]
tf_state_initial [in OAut.Complement]
tf_state [in OAut.Complement]
TildeEquivalenceClass [in OAut.Complement]
tilde_w_equiv_bool [in OAut.Complement]
tilde_w_equiv [in OAut.Complement]
tilde_equiv_class_aut [in OAut.Complement]
tilde_eq_class [in OAut.Complement]
tilde_equiv [in OAut.Complement]
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]
to_bounded [in OAut.Utils]
to_seq [in OAut.Utils]
transforms [in OAut.Complement]
transforms_final [in OAut.Complement]
trim [in OAut.DecLanguageEmpty]
trim_aut [in OAut.DecLanguageEmpty]
trim_final [in OAut.DecLanguageEmpty]
trim_initial [in OAut.DecLanguageEmpty]
trim_transition [in OAut.DecLanguageEmpty]
trim_state [in OAut.DecLanguageEmpty]

U

U [in BA.Automata]
undup [in BA.External]
union [in OAut.Buechi]
union_final [in OAut.Buechi]
union_initial [in OAut.Buechi]
union_transition [in OAut.Buechi]
union_state [in OAut.Buechi]
universal_language [in OAut.BasicDefs]

V

valid_path [in OAut.NFAs]
valid_run [in OAut.NFAs]
vector [in BA.FinTypes]
vectorise [in BA.FinTypes]
visits_final [in OAut.NFAConstructions]
VW [in OAut.Complement]
VW_part_of_complement [in OAut.Complement]
VW_aut [in OAut.Complement]
vw_aut [in OAut.NFAConstructions]
vw_state_initial [in OAut.NFAConstructions]
vw_state_final [in OAut.NFAConstructions]
vw_transition [in OAut.NFAConstructions]
vw_state [in OAut.NFAConstructions]

W

Womega_aut [in OAut.NFAConstructions]
Womega_state_initial [in OAut.NFAConstructions]
Womega_state_final [in OAut.NFAConstructions]
Womega_transition [in OAut.NFAConstructions]
word [in BA.Automata]
W_final [in OAut.Complement]

---

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 OAut.NFAs]
nfa [in BA.Automata]

S

String [in OAut.Seqs]

---

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

(1373 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

(47 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

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

(99 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

(15 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

(663 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

(20 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 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

(5 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

(27 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

(61 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

(111 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

(311 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

(9 entries)